Commit 51bbc4e3 authored by charguer's avatar charguer
Browse files

fix readme

parent b3770156
# CFML : a tool for proving OCaml programs in Separation Logic
Description
---
===========
This is CFML 1.0, not to be confused with CFML 2.0.
**This is CFML 1.0, not to be confused with CFML 2.0.**
CFML 1.0 is expected to be entirely subsumed by CFML 2.0 by the end of 2020.
**CFML 1.0 is expected to be entirely subsumed by CFML 2.0 by the end of 2020.**
Description
===========
CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.
......@@ -29,9 +32,9 @@ CFML 1.0 only works with Coq v8.8. Using OPAM, you might succeed in installing
CFML using the following commands.
```
opam switch create cfml_switch ocaml-base-compiler.4.07.0
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
opam switch create coq_8.8.2 ocaml-base-compiler.4.07.0
opam pin add coq 8.8.2
opam install pprint ocamlformat coq coqide coq-tlc coq-cfml coq-aac-tactics.8.8.0
```
......@@ -52,9 +55,9 @@ Once CFML is installed, you can replay the demo from the ICFP script.
or play with files accompanying a tutorial on CFML.
```sh
cd cfml/examples/Tuto
make
coqide Tuto_proof.v
cd cfml/examples/Tuto
make
coqide Tuto_proof.v
```
......
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