aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 18:45:41 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 18:45:41 +0200
commitf78a39499ef210456dd96ecb9896874c9ce300ae (patch)
tree55314f202e1a892599071ccd7758b086de1fb5ec
parentaa14c4352393c11ea6ecfb08936f3ae2f8b22fd5 (diff)
parent3510612550c32c790447b45ee01efbcf855815b9 (diff)
Merge PR #1093: [doc] Update INSTALL to match reality.
-rw-r--r--.travis.yml7
-rw-r--r--INSTALL25
2 files changed, 19 insertions, 13 deletions
diff --git a/.travis.yml b/.travis.yml
index 8d85ffc68..6c77f0059 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -31,6 +31,7 @@ env:
# system is == 4.02.3
- COMPILER="system"
- CAMLP5_VER="6.14"
+ - FINDLIB_VER="1.4.1"
- NATIVE_COMP="yes"
- COQ_DEST="-local"
# Main test suites
@@ -92,6 +93,7 @@ matrix:
- env:
- TEST_TARGET="test-suite"
- COMPILER="4.05.0"
+ - FINDLIB_VER="1.7.3"
- CAMLP5_VER="7.01"
- EXTRA_CONF="-coqide opt -with-doc yes"
- EXTRA_OPAM="lablgtk-extras hevea"
@@ -122,6 +124,7 @@ matrix:
- TEST_TARGET="coqocaml"
- COMPILER="4.05.0"
- CAMLP5_VER="7.01"
+ - FINDLIB_VER="1.7.3"
- EXTRA_CONF="-coqide opt -warn-error"
- EXTRA_OPAM="lablgtk-extras hevea"
# dummy target
@@ -137,7 +140,7 @@ matrix:
env:
- TEST_TARGET="test-suite"
- COMPILER="4.02.3"
- - CAMLP5_VER="6.17"
+ - CAMLP5_VER="6.17"
- NATIVE_COMP="no"
- COQ_DEST="-local"
before_install:
@@ -186,7 +189,7 @@ install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
- opam config list
-- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
+- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM}
- opam list
script:
diff --git a/INSTALL b/INSTALL
index 39fb1849a..b3ab33228 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,5 +1,5 @@
- INSTALLATION PROCEDURES FOR THE COQ V8.6 SYSTEM
+ INSTALLATION PROCEDURES FOR THE COQ V8.7 SYSTEM
-----------------------------------------------
@@ -27,19 +27,16 @@ WHAT DO YOU NEED ?
port install coq
- To compile Coq V8.6 yourself, you need:
+ To compile Coq V8.7 yourself, you need:
- - OCaml version 4.02.1 or later
- (available at http://caml.inria.fr/)
+ - OCaml version 4.02.3 or later
+ (available at https://ocaml.org/)
- OCaml version 4.02.0 is not supported because of a severe performance
- issue increasing compilation time.
+ - Findlib (version >= 1.4.1)
+ (available at http://projects.camlcity.org/projects/findlib.html)
- - Findlib (included in OCaml binary distribution under windows,
- probably available in your distribution and for sure at
- http://projects.camlcity.org/projects/findlib.html)
-
- - Camlp5 (version >= 6.02)
+ - Camlp5 (version >= 6.14)
+ (available at https://camlp5.github.io/)
- GNU Make version 3.81 or later
@@ -48,6 +45,12 @@ WHAT DO YOU NEED ?
- for Coqide, the Lablgtk development files, and the GTK libraries
incuding gtksourceview, see INSTALL.ide for more details
+ Opam (https://opam.ocaml.org/) is recommended to install ocaml and
+ the corresponding packages.
+
+ $ opam install ocamlfind camlp5 lablgtk-extras
+
+ should get you a reasonable Ocaml enviroment to compile Coq.
QUICK INSTALLATION PROCEDURE.
=============================