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 +++++++++++++++++++++++++++++++++++++++++++++++++
 README.md  |  4 +---
 2 files changed, 50 insertions(+), 3 deletions(-)
 create mode 100644 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.
diff --git a/README.md b/README.md
index ce42d3d..fff1054 100644
--- a/README.md
+++ b/README.md
@@ -16,9 +16,7 @@ The current stable version is the version 1.2.
 
 ### Installation
 
-To come.
-
-<!-- See the INSTALL.md file for instructions. -->
+See the INSTALL.md file for instructions.
 
 
 ### License
-- 
cgit