From 1e10dcc783b82269cc3fe3bb7419b9c1cc9e0fa7 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Fri, 9 Jan 2015 17:29:26 +0100
Subject: Installation instructions

---
 INSTALL.md | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 INSTALL.md

(limited to 'INSTALL.md')

diff --git a/INSTALL.md b/INSTALL.md
new file mode 100644
index 0000000..58f5370
--- /dev/null
+++ b/INSTALL.md
@@ -0,0 +1,49 @@
+# Installation procedures for SMTCoq
+
+## What do you need?
+
+SMTCoq is designed to work on computers equipped with a POSIX (Unix or a
+clone) operating system. It is known to work under GNU/Linux (i386 and
+amd64).
+
+It relies on the
+[git version of Coq with native compilation](https://github.com/maximedenes/native-coq),
+and its dependencies (OCaml, camlp5, GNU/Make). We explain below how to
+compile it (but not the dependencies).
+
+To use SMTCoq, you also 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)
+
+- [zChaff](http://www.princeton.edu/~chaff/zchaff.html)
+
+Please download the solvers you would like to use via the above links
+(since SMTCoq might not support later versions), and follow the
+instructions available for each solver in order to compile them **in a
+proof production mode**.
+
+
+## Installation of native-coq and SMTCoq
+
+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:
+```
+make
+make install
+```
+   in the src directory.
-- 
cgit