Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 95 insertions, 47 deletions

diff --git a/INSTALL b/INSTALL
index df9e8552..bb41e490 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,6 +1,6 @@
 
-            INSTALLATION PROCEDURES FOR THE COQ V8.6 SYSTEM
-            -----------------------------------------------
+            INSTALLATION PROCEDURE
+            ----------------------
 
 
 WHAT DO YOU NEED ?
@@ -27,27 +27,52 @@ WHAT DO YOU NEED ?
 
      port install coq
 
-   To compile Coq V8.6 yourself, you need:
+   To compile Coq yourself, you need:
 
-   - Objective Caml version 4.01.0 or later
-     (available at http://caml.inria.fr/)
+   - OCaml (version >= 4.02.3)
+     (available at https://ocaml.org/)
+     (This version of Coq has been tested up to OCaml 4.07.0)
 
-   - Findlib (included in OCaml binary distribution under windows,
-     probably available in your distribution and for sure at
-     http://projects.camlcity.org/projects/findlib.html)
+   - The Num package, which used to be part of the OCaml standard library,
+     if you are using an OCaml version >= 4.06.0
 
-   - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be
-     less well supported, for instance, Objective Caml version 4.02.1
-     is then needed or a patched version of 4.01.0 as e.g. version
-     4.01.0-4 in Debian Jessie)
+   - Findlib (version >= 1.4.1)
+     (available at http://projects.camlcity.org/projects/findlib.html)
+
+   - Camlp5 (version >= 6.14)
+     (available at https://camlp5.github.io/)
 
    - GNU Make version 3.81 or later
 
    - a C compiler
 
    - for Coqide, the Lablgtk development files, and the GTK libraries
-     incuding gtksourceview, see INSTALL.ide for more details
+     including gtksourceview, see INSTALL.ide for more details
+
+   Note that num, camlp5 and lablgtk should be properly registered with
+   findlib/ocamlfind as Coq's makefile will use it to locate the
+   libraries during the build.
+
+   Opam (https://opam.ocaml.org/) is recommended to install OCaml and
+   the corresponding packages.
+
+   $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview
+
+   should get you a reasonable OCaml environment to compile Coq.
+
+   Nix users can also get all the required dependencies by running:
 
+   $ nix-shell
+
+   Advanced users may want to experiment with the OCaml Flambda
+   compiler as way to improve the performance of Coq. In order to
+   profit from Flambda, a special build of the OCaml compiler that has
+   the Flambda optimizer enabled must be installed. For OPAM users,
+   this amounts to installing a compiler switch ending in `+flambda`,
+   such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt
+   -config` reports that Flambda is available, some further
+   optimization options can be used; see the entry about -flambda-opts
+   below for more details.
 
 QUICK INSTALLATION PROCEDURE.
 =============================
@@ -55,29 +80,26 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
-4. make clean
-
 
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
 
-1- Check that you have the Objective Caml compiler installed on your
+1- Check that you have the OCaml compiler installed on your
    computer and that "ocamlc" (or, better, its native code version
    "ocamlc.opt") lies in a directory which is present in your $PATH
    environment variable. At the time of writing this sentence, all
-   versions of Objective Caml later or equal to 4.01.0 are
-   supported to the exception of Objective Caml 4.02.0.
+   versions of Objective Caml later or equal to 4.02.3 are
+   supported.
 
    To get Coq in native-code, (it runs 4 to 10 times faster than
    bytecode, but it takes more time to get compiled and the binary is
    bigger), you will also need the "ocamlopt" (or its native code version
    "ocamlopt.opt") command.
 
-2- Check that you have Camlp5 (or a supported Camlp4) installed on your
-   computer and that the command "camlp5" lies in a directory which
-   is present in your $PATH environment variable path.
-   (You need Camlp5/4 in both bytecode and native versions if
-   your platform supports it).
+2- Check that you have Camlp5 installed on your computer and that the
+   command "camlp5" lies in a directory which is present in your $PATH
+   environment variable path.  (You need Camlp5 in both bytecode and
+   native versions if your platform supports it).
 
 3- The uncompression and un-tarring of the distribution file gave birth
    to a directory named "coq-8.xx". You can rename this directory and put
@@ -128,14 +150,38 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 	Use <command> to open an URL in a browser. %s must appear in <command>,
 	and will be replaced by the URL.
 
+-flambda-opts <flags>
+        This experimental option will pass specific user flags to the
+        OCaml optimizing compiler. In most cases, this option is used
+        to tweak the flambda backend; for maximum performance we
+        recommend using
+
+        -flambda-opts `-O3 -unbox-closures`
+
+        but of course you are free to try with a different combination
+        of flags. You can read more at
+        https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+        There is a known problem with certain OCaml versions and
+        `native_compute`, that will make compilation to require
+        a large amount of RAM (>= 10GiB) in some particular files.
+
+        We recommend disabling native compilation (`-native-compiler no`)
+        with flambda unless you use OCaml >= 4.07.0.
+
+        c.f. https://caml.inria.fr/mantis/view.php?id=7630
+
 5- Still in the root directory, do
 
 	make
 
-   to compile Coq in Objective Caml bytecode (and native-code if supported).
+   to compile Coq in the best OCaml mode available (native-code if supported,
+   bytecode otherwise).
 
    This will compile the entire system. This phase can take more or less time,
-   depending on your architecture and is fairly verbose.
+   depending on your architecture and is fairly verbose. On a multi-core machine,
+   it is recommended to compile in parallel, via make -jN where N is your number
+   of cores.
 
 6- You can now install the Coq system. Executables, libraries, manual pages
    and emacs mode are copied in some standard places of your system, defined at
@@ -145,13 +191,20 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
        	make install
 
    Of course, you may need superuser rights to do that.
-   To use the Coq emacs mode you also need to put the following lines
-   in you .emacs file:
 
-        (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-        (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
+7- Optionally, you could build the bytecode version of Coq via:
+
+        make byte
+
+   and install it via
 
-7- You can now clean all the sources. (You can even erase them.)
+        make install-byte
+
+  This version is quite slower than the native code version of Coq, but could
+  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+  toplevel accessible via the Drop command.
+
+8- You can now clean all the sources. (You can even erase them.)
 
 	make clean
 
@@ -169,16 +222,10 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS.
    Then compile the sources as described in step 5 above. The resulting
    binaries will reside in the subdirectory bin/.
 
-   If you want to compile the sources for debugging (i.e. with the option
-   -g of the Caml compiler) then add the -debug option at configuration
-   step :
-
-	./configure -debug <other options>
-
-   and then compile the sources (step 5). Then you must make a Coq toplevel
-   including your own tactics, which must be compiled with -g, with coqmktop.
-   See the chapter 16 of the Coq Reference Manual for details about how
-   to use coqmktop and the Objective Caml debugger with Coq.
+   Unless you pass the -nodebug option to ./configure, the -g option of the
+   OCaml compiler will be used during compilation to allow debugging.
+   See the debugging file in dev/doc and the chapter 15 of the Coq Reference
+   Manual for details about how to use the OCaml debugger with Coq.
 
 
 THE AVAILABLE COMMANDS.
@@ -189,11 +236,14 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler
 
-   Under architecture where ocamlopt is available, there are actually two
-   binaries for the interactive system, coqtop.byte and coqtop (respectively
-   bytecode and native code versions of Coq).  coqtop is a link to coqtop.byte
-   otherwise. coqc also invokes the fastest version of Coq.  Options -opt and
-   -byte to coqtop and coqc selects a particular binary.
+   Under architecture where ocamlopt is available, coqtop is the native code
+   version of Coq. On such architecture, you could additionally request
+   the build of the bytecode version of Coq via 'make byte' and install it via
+   'make install-byte'. This will create  an extra binary named coqtop.byte,
+   that could be used for debugging purpose. If native code isn't available,
+   coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+   coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+   and coqc selects a particular binary.
 
     * `coqtop' launches Coq in the interactive mode. By default it loads
       basic logical definitions and tactics from the Init directory.
@@ -211,8 +261,6 @@ THE AVAILABLE COMMANDS.
    directory, or read online on http://coq.inria.fr/doc/)
    and in the corresponding manual pages.
 
-   There is also a tutorial and a FAQ; see http://coq.inria.fr/getting-started
-
 
 COMPILING FOR DIFFERENT ARCHITECTURES.
 ======================================