|
HISTORY:
-------
* July 2007 (Pierre Corbineau & Lionel Elie Mamane).
Inclusion of a build system with 3 explicit phases:
- Makefile.stage1: ocamldep, sed, camlp4 without Coq grammar extension
- Makefile.stage2: camlp4 with grammar.cma or q_constr.cmo
- Makefile.stage3: coqdep (.vo)
* March 2010 (Pierre Letouzey).
Revised build system. In particular, no more stage1,2,3 :
- Stage3 was removed some time ago when coqdep was split into
coqdep_boot and full coqdep.
- Stage1,2 were replaced by brutal inclusion of all .d at the start
of Makefile.build, without trying to guess what could be done at
what time. Some initial inclusions hence _fail_, but "make" tries
again later and succeed.
- Btw, .ml4 are explicitly turned into .ml files, which stay after build.
By default, they are in binary ast format, see READABLE_ML4 option.
* February 2014 (Pierre Letouzey).
Another revision of the build system. We avoid relying on the awkward
include-which-fails-but-works-finally-after-a-retry feature of gnu make.
This was working, but was quite hard to understand. Instead, we reuse
the idea of two explicit phases, but in a lighter way than in 2007.
The main Makefile calls Makefile.build twice :
- first for building grammar.cma (and q_constr.cmo), with a
restricted set of .ml4 (see variable BUILDGRAMMAR).
- then on the true target asked by the user.
* June 2016 (Pierre Letouzey)
The files in grammar/ are now self-contained, we could compile
grammar.cma (and q_constr.cmo) directly, no need for a separate
subcall to make nor awkward include-failed-and-retry.
* February - September 2018 (Emilio Jesús Gallego Arias)
Dune support added.
The build setup is mostly vanilla for the OCaml part, however the
`.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper
that will generate the necessary `dune` files.
As a developer, you should not have to deal with Dune configuration
files on a regular basis unless adding a new library or plugin.
The vanilla setup declares all the Coq libraries and binaries [we
must respect proper containment/module implementation rules as to
allow packing], and we build custom preprocessors (based on `camlp5`
and `coqpp`) that will process the `ml4`/`mlg` files.
This suffices to build `coqtop` and `coqide`, all that remains to
handle is `.vo` compilation.
To teach Dune about the `.vo`, we use a small utility `coq_dune`,
that will generate a `dune` file for each directory in `plugins` and
`theories`. The code is pretty straightforward and declares build
and install rules for each `.v` straight out of `coqdep`. Thus, our
build strategy looks like this:
1. Use `dune` to build `coqdep` and `coq_dune`.
2. Use `coq_dune` to generate `dune` files for each directory with `.v` files.
3. ?
4. Profit! [Seriously, at this point Dune has all the information to build Coq]
---------------------------------------------------------------------------
This file documents internals of the implementation of the make-based
build system. For what a Coq developer needs to know about the build
system, see build-system.txt and build-system.dune.md .
.ml4 files
----------
.ml4 are converted to .ml by camlp5. By default, they are produced
in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
Pros:
- faster than parsing clear-text source file.
- no risk of editing them by mistake instead of the .ml4
- the location in the binary .ml are those of the initial .ml4,
hence errors are properly reported in the .ml4.
Cons:
- This format may depend on your ocaml version, they should be
cleaned if you change your build environment.
- Unreadable in case you want to inspect this generated code.
For that, use make with the READABLE_ML4=1 option to switch to
clear-text generated .ml.
Makefiles hierarchy
-------------------
The Makefile is separated in several files :
- Makefile: wrapper that triggers a call to Makefile.build, except for
clean and a few other little things doable without dependency analysis.
- Makefile.common : variable definitions (mostly lists of files or
directories)
- Makefile.build : contains compilation rules, and the "include" of dependencies
- Makefile.doc : specific rules for compiling the documentation.
FIND_SKIP_DIRS
--------------
The recommended style of using FIND_SKIP_DIRS is for example
find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print
1)
The parentheses even in the one-criteria case is so that if one adds
other conditions, e.g. change the first example to the second
find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
one is not tempted to write
find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
ends with an -or, and how it combines with what comes later depends on
operator precedence and all that. Much safer to override it with
parentheses.
In short, it protects against the -or one doesn't see.
2)
As to the -print at the end, yes it is necessary. Here's why.
You are used to write:
find . -name '*.example'
and it works fine. But the following will not:
find . $(FIND_SKIP_DIRS) -name '*.example'
it will also list things directly matched by FIND_SKIP_DIRS
(directories we want to prune, in which we don't want to find
anything). C'est subtil... Il y a effectivement un -print implicite à
la fin, qui fait que la commande habituelle sans print fonctionne
bien, mais dès que l'on introduit d'autres commandes dans le lot (le
-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
parenthèses du -print implicite par rapport au parenthésage dans la
forme recommandée d'utilisation:
Si on explicite le -print et les parenthèses implicites, cela devient:
find . '(' '(' '(' -name .git -or -name debian ')' -prune ')' -or \
'(' -name '*.example' ')'
')'
-print
Le print agit TOUT ce qui précède, soit sur ce qui matche "'(' -name
.git -or -name debian ')'" ET sur ce qui matche "'(' -name '*.example' ')'".
alors qu'ajouter le print explicite change cela en
find . '(' '(' -name .git -or -name debian ')' -prune ')' -or \
'(' '(' -name '*.example' ')' -print ')'
Le print n'agit plus que sur ce qui matche "'(' -name '*.example' ')'"
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
