Commit c656bbc2 authored by Armaël Guéneau's avatar Armaël Guéneau

Refresh installation instructions

- remove the INSTALL file which was mostly outdated
- document the installation process using opam
- put a link to "cfml-skeleton" which provides a template for projects using
  cfml
parent cefdc226
#################################################################
# Requirements
# you'll need the "pprint" ocaml package installed.
# (optional) you'll need "pandoc" to build the html documentation.
#################################################################
# install coq8.5pl2 if you don't have it yet, either manually or using opam
# Manual installation, on ubuntu or similar:
- download https://coq.inria.fr/distrib/8.5pl2/files/coq-8.5pl2.tar.gz
- extract the archive into ~/softs/coq-8.5pl2/ (else you'll need to adapt paths)
- then execute the following commands:
cd ~/softs/coq-8.5pl2/
./configure -local
make -j 4
# Using opam:
opam install coq.8.5.2 && opam pin add coq 8.5.2
#################################################################
# download the files and configure paths
git clone https://gforge.inria.fr/git/cfml/cfml.git ~/cfml
git clone https://gforge.inria.fr/git/tlc/tlc.git ~/tlc
# adapt the path below if coq8.5 is installed elsewhere
# (or skip the commands if it is in your path or installed via opam)
# [make sure to include the trailing slash after bin]
echo COQBIN=~/softs/coq-8.5pl2/bin/ > ~/cfml/settings.sh
echo COQBIN=~/softs/coq-8.5pl2/bin/ > ~/tlc/src/settings.sh
# adapt the path below if ~/cfml is not the path used
echo CFML=~/cfml >> ~/cfml/settings.sh
echo TLC=~/tlc/src >> ~/cfml/settings.sh
#################################################################
# Remark: if you have errors of the form "Unbound module NTLC_LibTactics"
during compilation, then try "make clean; make", without the "-j" option.
# setup tlc (takes about 30s, only needed once)
cd ~/tlc
make -j 4
# setup cfml (takes about 30s, only needed once)
cd ~/cfml
make -j 4
make doc # optional, requires pandoc
# open a test program
cd ~/cfml/examples/Tuto
make
coqide Tuto_proof.v &
% CFML : a characteristic formula generator for OCaml
% Arthur Charguéraud, with contributions from others.
% License : GNU GPL v3.
# CFML : a characteristic formula generator for OCaml
Description
===========
CFML consists of two parts:
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
- 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
Compilation
============
The recommended way is by using `opam` to pin the repository:
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml
Note that you will need in particular a working installation
of [TLC](https://gitlab.inria.fr/charguer/tlc/).
Getting started
============
Once CFML is installed, you can:
- Step through the tutorial. Clone the CFML git repository, then:
```sh
cd cfml/examples/Tuto
make
coqide Tuto_proof.v
```
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to setup a
new project that uses CFML.
Documentation
-
============
Some documentation can be found in [doc/doc.html](doc/doc.html).
Note that it is currently somewhat outdated and needs updating.
License
======
All files are distributed under the GNU-GPL v3 license.
See doc/doc.html.
If you need a more permissive license, please contact the author.
Authors: Arthur Charguéraud,
with contributions from others.
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