aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-24 04:40:34 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-30 17:47:28 +0200
commit419e7cac23d7b8ac97d46a6c0d3228d591273d2b (patch)
tree17c794fa4f3b39170067fbabc6d73d0d4a13967b /INSTALL
parentfd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff)
Makefile: no bytecode compilation in make world, see make byte instead
On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see a future commit about coq_makefile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
Diffstat (limited to 'INSTALL')
-rw-r--r--INSTALL36
1 files changed, 26 insertions, 10 deletions
diff --git a/INSTALL b/INSTALL
index eacbec299..39fb1849a 100644
--- a/INSTALL
+++ b/INSTALL
@@ -55,8 +55,6 @@ QUICK INSTALLATION PROCEDURE.
1. ./configure
2. make
3. make install (you may need superuser rights)
-4. make clean
-
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
=================================================
@@ -131,10 +129,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
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
@@ -150,7 +151,19 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
-7- You can now clean all the sources. (You can even erase them.)
+7- 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.
+
+8- You can now clean all the sources. (You can even erase them.)
make clean
@@ -182,11 +195,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.