diff options
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/INSTALL.md b/INSTALL.md index 3d05fd65ab..f672bb45d3 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -15,9 +15,6 @@ To compile Coq yourself, you need: - [OCaml](https://ocaml.org/) (version >= 4.05.0) (This version of Coq has been tested up to OCaml 4.11.1) -- The [num](https://github.com/ocaml/num) library; note that it is - included in the OCaml distribution for OCaml versions < 4.06.0 - - The [ZArith library](https://github.com/ocaml/Zarith) >= 1.10 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0) @@ -35,15 +32,15 @@ To compile Coq yourself, you need: (version >= 3.1.0), and the corresponding GTK 3.x libraries, as of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18) -The IEEE-754 compliance is required by primitive floating-point -numbers (`Require Import Floats`). Common sources of incompatibility -are checked at configure time, preventing compilation. In the, -unlikely, event an incompatibility remains undetected, using Floats -would enable to prove False on this architecture. +Primitive floating-point numbers require IEEE-754 compliance +(`Require Import Floats`). Common sources of incompatibility +are checked at configure time, preventing compilation. In the +unlikely event an incompatibility remains undetected, using `Floats` +would enable proving `False` on this architecture. -Note that `num` and `lablgtk3-sourceview3` should be properly -registered with `findlib/ocamlfind` as Coq's makefile will use it to -locate the libraries during the build. +Note that OCaml dependencies (`zarith` and `lablgtk3-sourceview3` at +this moment) must be properly registered with `findlib/ocamlfind` +since Coq's build system uses `findlib` to locate them. Debian / Ubuntu users can get the necessary system packages for CoqIDE with: @@ -55,7 +52,7 @@ the corresponding packages. $ opam switch create coq 4.11.1+flambda $ eval $(opam env) - $ opam install num ocamlfind lablgtk3-sourceview3 + $ opam install ocamlfind zarith lablgtk3-sourceview3 should get you a reasonable OCaml environment to compile Coq. See the OPAM documentation for more help. |