diff options
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 326 |
1 files changed, 326 insertions, 0 deletions
diff --git a/INSTALL b/INSTALL new file mode 100644 index 0000000000..e02439c54b --- /dev/null +++ b/INSTALL @@ -0,0 +1,326 @@ + + INSTALLATION PROCEDURE + ---------------------- + + +WHAT DO YOU NEED ? +================== + + Your OS may already contain Coq under the form of a precompiled + package or ready-to-compile port. In this case, and if the supplied + version suits you, follow the usual procedure for your OS to + install it. E.g.: + + - Debian GNU/Linux derivatives (or Debian GNU/k*BSD or ...): + + aptitude install coq + + - Gentoo GNU/Linux: + + emerge sci-mathematics/coq + + - Fedora GNU/Linux: + + urpmi coq + + - MacPorts for MacOS X + + port install coq + + To compile Coq yourself, you need: + + - OCaml (version >= 4.05.0) + (available at https://ocaml.org/) + (This version of Coq has been tested up to OCaml 4.07.0) + + - The Num package, which used to be part of the OCaml standard library, + if you are using an OCaml version >= 4.06.0 + + - Findlib (version >= 1.4.1) + (available at http://projects.camlcity.org/projects/findlib.html) + + - GNU Make version 3.81 or later + + - a C compiler + + - for CoqIDE, the lablgtk development files (version >= 3.0.0), + and the GTK 3.x libraries including gtksourceview3. + + Note that num 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 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. +============================= + +1. ./configure +2. make +3. make install (you may need superuser rights) + +INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). +================================================= + +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.05.0 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- 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 + it wherever you want. Just keep in mind that you will need some spare + space during the compilation (reckon on about 300 Mb of disk space + for the whole system in native-code compilation). Once installed, the + binaries take about 30 Mb, and the library about 200 Mb. + +3- First you need to configure the system. It is done automatically with + the command: + + ./configure <options> + + The "configure" script will ask you for directories where to put + the Coq binaries, standard library, man pages, etc. It will propose + you some default values. + + For a list of options accepted by the "configure" script, run + "./configure -help". The main options accepted are: + +-prefix <dir> + Binaries, library, and man pages will be respectively + installed in <dir>/bin, <dir>/lib/coq, and <dir>/man + +-bindir <dir> (default: /usr/local/bin) + Directory where the binaries will be installed + +-libdir <dir> (default: /usr/local/lib/coq) + Directory where the Coq standard library will be installed + +-mandir <dir> (default: /usr/local/share/man) + Directory where the Coq manual pages will be installed + +-arch <value> (default is the result of the command "arch") + An arbitrary architecture name for your machine (useful when + compiling Coq on two different architectures for which the + result of "arch" is the same, e.g. Sun OS and Solaris) + +-local + Compile Coq to run in its source directory. The installation (step 6) + is not necessary in that case. + +-browser <command> + 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 + +4- Still in the root directory, do + + make + + 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. On a multi-core machine, + it is recommended to compile in parallel, via make -jN where N is your number + of cores. + +5- You can now install the Coq system. Executables, libraries, and + manual pages are copied in some standard places of your system, + defined at configuration time (step 3). Just do + + umask 022 + make install + + Of course, you may need superuser rights to do that. + +6- Optionally, you could build the bytecode version of Coq via: + + make byte + + and install it via + + 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. + +7- You can now clean all the sources. (You can even erase them.) + + make clean + + +INSTALLATION PROCEDURE FOR ADVANCED USERS. +========================================== + + If you wish to write plugins you *must* keep the Coq sources, without + cleaning them. Therefore, to avoid a duplication of binaries and library, + it is not necessary to do the installation step (6- above). You just have + to tell it at configuration step (4- above) with the option -local : + + ./configure -local <other options> + + Then compile the sources as described in step 5 above. The resulting + binaries will reside in the subdirectory bin/. + + 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. +======================= + + There are two Coq commands: + + coqtop The Coq toplevel + coqc The Coq compiler + + 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. + + * `coqc' allows compilation of Coq files directly from the command line. + To compile a file foo.v, do: + + coqc foo.v + + It will produce a file foo.vo, that you can now load through the Coq + command "Require". + + A detailed description of these commands and of their options is given + in the Reference Manual (which you can get in the doc/ + directory, or read online on http://coq.inria.fr/doc/) + and in the corresponding manual pages. + + +COMPILING FOR DIFFERENT ARCHITECTURES. +====================================== + + This section explains how to compile Coq for several architecture, sharing + the same sources. The important fact is that some files are architecture + dependent (.cmx, .o and executable files for instance) but others are not + (.cmo and .vo). Consequently, you can : + + o save some time during compilation by not cleaning the architecture + independent files; + + o save some space during installation by sharing the Coq standard + library (which is fully architecture independent). + + So, in order to compile Coq for a new architecture, proceed as follows: + + * Omit step 7 above and clean only the architecture dependent files: + it is done automatically with the command + + make archclean + + * Configure the system for the new architecture: + + ./configure <options> + + You can specify the same directory for the standard library but you + MUST specify a different directory for the binaries (of course). + + * Compile and install the system as described in steps 5 and 6 above. + + +MOVING BINARIES OR LIBRARY. +=========================== + + If you move both the binaries and the library in a consistent way, + Coq should be able to still run. Otherwise, Coq may be "lost", + running "coqtop" would then return an error message of the kind: + + Error during initialization : + Error: cannot guess a path for Coq libraries; please use -coqlib option + + You can then indicate the new places to Coq, using the options -coqlib : + + coqtop -coqlib <new directory> + + See also next section. + + +DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. +====================================================== + + Some bytecode executables of Coq use the OCaml runtime, which dynamically + loads a shared library (.so or .dll). When it is not installed properly, you + can get an error message of this kind: + + Fatal error: cannot load shared library dllcoqrun + Reason: dllcoqrun.so: cannot open shared object file: No such file or directory + + In this case, you need either: + - to set the CAML_LD_LIBRARY_PATH environment variable to point to the + directory where dllcoqrun.so is; this is suitable when you want to run + the command a limited number of times in a controlled environment (e.g. + during compilation of binary packages); + - install dllcoqrun.so in a location listed in the file ld.conf that is in + the directory of the standard library of OCaml; + - recompile your bytecode executables after reconfiguring the location + of the shared library: + ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ... + where <path> is the directory where the dllcoqrun.so is installed; + - (not recommended) compile bytecode executables with a custom OCaml + runtime by using: + ./configure -custom ... + be aware that stripping executables generated this way, or performing + other executable-specific operations, will make them useless. |