From f33310c1d3d29f05f23ffd34e15e668e6d402914 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 3 Dec 2015 07:30:19 +0100 Subject: OPAM currently not supported --- INSTALL.md | 110 +++++++++++++++++-------------------------------------------- 1 file changed, 31 insertions(+), 79 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index e384583..9de0b49 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -7,34 +7,45 @@ clone) operating system. It is known to work under GNU/Linux (i386 and amd64). -## Quick installation +## Installation from the sources + +Currently, SMTCoq can be built only from the sources, using the +[version of Coq with native data-structures](https://github.com/maximedenes/native-coq). The design of an opam package is under progress. -The simplest way to install SMTCoq is to use the OPAM package, available -in the -[Coq unstable repository](https://github.com/coq/repo-unstable.git). -Once you have OPAM installed on your system: +1. Download the git version of Coq with native compilation: +``` +git clone git://github.com/maximedenes/native-coq.git ``` -opam repo add coq-stable https://github.com/coq/repo-stable.git -opam repo add coq-unstable https://github.com/coq/repo-unstable.git -opam update -opam install coq coq:smtcoq + and compile it by following the instructions available in the + repository. We recommand that you do not install it, but only compile + it in local: +``` +./configure -local +make ``` -For more information of opam packages for Coq, see -[Use OPAM for Coq](http://coq-blog.clarus.me/use-opam-for-coq.html). -This version is sufficient to check small certificates and to solve -small goals. However, if you want to check larger certificates, we -recommend using SMTCoq with the -[version of Coq with native data-structures](https://github.com/maximedenes/native-coq), -following the instructions in Section "Installation from the sources". +2. Set an environment variable COQBIN to the directory where Coq's + binaries are; for instance: +``` +export COQBIN=/home/jdoe/native-coq/bin/ +``` + (the final slash is mandatory). + +3. Compile and install SMTCoq by using the commands: +``` +./configure.sh +make +make install +``` + in the src directory. ## Installation of the provers -To use SMTCoq, you also need one or more solvers supported by SMTCoq. +To use SMTCoq, you need one or more solvers supported by SMTCoq. Currently, these solvers are: -- [veriT](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz) +- [veriT](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz) - [zChaff](http://www.princeton.edu/~chaff/zchaff.html) @@ -47,7 +58,7 @@ proof production mode**, as detailed below. ### veriT The -[above link](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz) +[above link](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/verit2c2b43b.tar.gz) points to a snapshot of veriT which is known to be compatible with SMTCoq, and is already in proof production mode. If you encounter problems to compile it, please report an issue. @@ -57,68 +68,9 @@ problems to compile it, please report an issue. zChaff is not actively maintained, so you might encounter problems to compile it on modern platforms. -[This patch](http://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Smtcoq/zchaff64.patch) +[This patch](https://www.lri.fr/~keller/Documents-recherche/Smtcoq/zchaff64.patch) might solve your problems (thanks to Sylvain Boulmé for it); if not, please report an issue. To turn proof production on, you need to uncomment the line `// #define VERIFY_ON ` in `zchaff_solver.cpp`. - - -## Installation from the sources - -From the sources, SMTCoq can be built either with the standard version -of Coq or with the -[version of Coq with native data-structures](https://github.com/maximedenes/native-coq). -We recommend this latter for efficiency. - - -### With the version of Coq with native data-structures - -1. Download the git version of Coq with native compilation: -``` -git clone git://github.com/maximedenes/native-coq.git -``` - and compile it by following the instructions available in the - repository. We recommand that you do not install it, but only compile - it in local: -``` -./configure -local -make -``` - -2. Set an environment variable COQBIN to the directory where Coq's - binaries are; for instance: -``` -export COQBIN=/home/jdoe/native-coq/bin/ -``` - (the final slash is mandatory). - -3. Compile and install SMTCoq by using the commands: -``` -./configure.sh -make -make install -``` - in the src directory. - - -### With the standard version of Coq - -1. Install the standard version of Coq (>= 8.4) by any means that give - access to the sources (e.g. via OPAM or from the sources). - -2. Set an environment variable COQBIN to the directory where Coq's - binaries are; for instance: -``` -export COQBIN=/home/jdoe/coq-8.4pl5/bin/ -``` - (the final slash is mandatory). - -3. Compile and install SMTCoq by using the commands: -``` -./configure.sh -standard -make -make install -``` - in the src directory. -- cgit