From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- INSTALL | 142 +++++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 95 insertions(+), 47 deletions(-) (limited to 'INSTALL') 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 to open an URL in a browser. %s must appear in , and will be replaced by the URL. +-flambda-opts + 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 - - 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. ====================================== -- cgit v1.2.3