Commit e7e1c856 authored by POTTIER Francois's avatar POTTIER Francois

New installation instructions in README.

parent 67b9845e
# CFML : a characteristic formula generator for OCaml
# CFML : a tool for proving OCaml programs in Separation Logic
Description
===========
CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.
CFML consists of two parts:
- a tool, implemented in OCaml, which parses OCaml source code
and generates Coq files containing characteristic formulae;
- a Coq library, which exports definitions, lemmas and tactics
used to manipulate characteristic formulae.
Status:
- The current version of CFML is known to work with Coq 8.6
- a tool, implemented in OCaml, parses OCaml source code and generates Coq
files that contain characteristic formulae, that is, logical descriptions
of the behavior of the OCaml code.
- a Coq library exports definitions, lemmas, and tactics that are used
to reason inside Coq about the code. In short, these tactics allow
the reasoning rules of Separation Logic to be applied to the OCaml code.
Compilation
Installation
============
The recommended way is by using `opam` to pin the repository:
The current version of CFML requires Coq 8.6 (*not* 8.6.1).
The simplest way of installing the *latest released version* of CFML is via `opam`.
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
It is recommended to create a new switch, whose name you can choose;
in the following, we use `cfml86`.
Note that you will need in particular a working installation
of [TLC](https://gitlab.inria.fr/charguer/tlc/).
```sh
opam switch cfml86 -A 4.05.0
eval `opam config env`
opam install -j4 coq.8.6
opam install -j4 coq-cfml
```
If instead you wish to use *the development version* of CFML,
then the last line above should be replaced by the following:
```sh
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
```
Getting started
============
......@@ -35,7 +53,7 @@ make
coqide Tuto_proof.v
```
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to setup a
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to set up a
new project that uses CFML.
Documentation
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment