1
Since July 2007, Coq features a build system overhauled by Pierre
2
Corbineau and Lionel Elie Mamane.
4
This file documents what a Coq developer needs to know about the build
5
system. If you want to enhance the build system itself (or are curious
6
about its implementation details), see build-system.dev.txt .
8
The build system is not at its optimal state, see TODO section.
10
Stages in build system
11
----------------------
13
The build system is separated into three stages, corresponding to the
14
tool(s) necessary to compute the dependencies necessary at this stage:
16
stage1: ocamldep, sed, camlp4 without Coq extensions
17
stage2: camlp4 with grammar.cma and/or q_constr.cmo
20
The file "Makefile" itself serves as minimum stage for targets that
21
should not need any dependency (such as *clean*).
23
Changes (for old-timers)
24
------------------------
26
The contents of the old Makefile has been mostly split into:
28
- variable declarations for file lists in Makefile.common.
30
These declarations are now static (for faster Makefile execution),
31
so their definitions are order-dependent.
33
- actual building rules and compiler flags variables in
37
The handling of globals is now: the globals of FOO.v are in FOO.glob
38
and the global glob.dump is created by concatenation of all .glob
39
files. In particular, .glob files are now always created.
41
See also section "cleaning targets"
43
Reducing build system overhead
44
------------------------------
46
When you are actively working on a file in a "make a change, make to
47
test, make a change, make to test", etc mode, here are a few tips to
50
- Always ask for what you want directly (e.g. bin/coqtop,
51
foo/bar.cmo, ...), don't do "make world" and interrupt
52
it when it has done what you want. This will try to minimise the
53
stage at which what you ask for is done (instead of maximising it
54
in order to maximise parallelism of the build process).
56
For example, if you only want to test whether bin/coqtop still
57
builds (and eventually start it to test your bugfix or new
58
feature), don't do "make world" and interrupt it when bin/coqtop is
59
built. Use "make bin/coqtop" or "make coqbinaries" or something
60
like that. This will avoid entering the stage 3, and cut build
61
system overhead by 50% (1.2s instead of 2.4 on writer's machine).
63
- You can turn off rebuilding of the standard library each time
64
bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1.
66
- If you want to avoid all .ml4 files being recompiled only because
67
grammar.cma was rebuilt, do "make ml4depclean" once and then use
70
- The CM_STAGE1=1 option to make will build all .cm* files mentioned
71
as targets on the command line in stage1. Whether this will work is
72
your responsibility. It should work for .ml files that don't depend
73
(nor directly nor indirectly through transitive closure of the
74
dependencies) on any .ml4 file, or where those dependencies can be
75
safely ignored in the current situation (e.g. all these .ml4 files
76
don't need to be recompiled).
78
This will avoid entering the stage2 (a reduction of 33% in
79
overhead, 0.4s on the writer's machine).
81
- To jump directly into a stage (e.g. because you know nothing is to
82
be done in stage 1 or (1 and 2) or because you know that the target
83
you give can be, in this situation, done in a lower stage than the
84
build system dares to), use GOTO_STAGE=n. This will jump into stage
85
n and try to do the targets you gave in that stage.
87
- To disable all dependency recalculation, use the NO_RECALC_DEPS=1
88
option. It disables REcalculation of dependencies, not calculation
89
of dependencies. In other words, if a .d file does not exist, it is
90
still created, but it is not updated every time the source file
91
(e.g. .ml) is changed.
93
General speed improvements:
95
- When building both the native and bytecode versions, the
96
KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
97
by running camlp4o only once on every .ml4 file, at the expense of
98
readability of compilation error messages for .ml4 files.
103
There are no dependencies in the archive anymore, they are always
104
bootstrapped. The dependencies of a file FOO are in FOO.d . This
105
enables partial recalculation of dependencies (only the dependencies
106
of changed files are recomputed).
108
If you add a dependency to a Coq camlp4 extension (grammar.cma or
109
q_constr.cmo), then see sections ".ml4 files" and "new files".
114
Targets for cleaning various parts:
116
- distclean: clean everything; must leave only what should end up in
117
distribution tarball and/or is in a svn checkout.
119
- clean: clean everything except effect of "./configure" and documentation.
121
- cleanconfig: clean effect of "./configure" only
123
- archclean: remove all architecture-dependent generated files
124
- indepclean: remove all architecture-independent generated files
127
- objclean: clean all generated files, but not Makefile meta-data
128
(e.g. dependencies), nor debugging/development information nor
129
other cruft (e.g. editor backup files), nor documentation
131
- docclean: clean documentation
136
The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
137
can be obtained with:
138
make FOO.ml4-preprocessed
140
If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
141
or q_constr.cmo), it must contain a line like:
142
(*i camlp4deps: "grammar.cma q_constr.cmo" i*)
144
If it uses a standard grammar extension, it must contain a line like:
145
(*i camlp4use: "pa_ifdef.cmo" i*)
147
It can naturally contain both a camlp4deps and a camlp4use line. Both
148
are used for preprocessing. It is thus _not_ necessary to add a
149
specific rule for a .ml4 file in the Makefile.build just because it
150
uses grammar extensions.
152
By default, the build system is geared towards development that may
153
use the Coq grammar extensions, but not development of Coq's grammar
154
extensions themselves. This means that .ml4 files are compiled
155
directly (using ocamlc/opt's -pp option), without use of an
156
intermediary .ml (or .ml4-preprocessed) file. This is so that if a
157
compilation error occurs, the location in the error message is a
158
location in the .ml4 file. If you are modifying the grammar
159
extensions, you may be more interested in the location of the error in
160
the .ml4-preprocessed file, so that you can see what your new grammar
161
extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1
162
option. This will make compilation of a .ml4 file a two-stage process:
164
1) create the .ml4-preprocessed file with camlp4o
165
2) compile it with straight ocamlc/opt without preprocessor
167
and will instruct make not to delete .ml4-preprocessed files
168
automatically just because they are intermediary files, so that you
171
If you add a _new_ grammar extension to Coq:
173
- if it can be built at stage1, that is the .ml4 file does not use a
174
Coq grammar extension itself, then add it, and all .cmo files it
175
needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the
176
handling of grammar.cma and q_constr.cmo for an example.
178
- if it cannot be built at stage1, that is the .ml4 file itself needs
179
to be preprocessed with a Coq camlp4 grammar extension, then,
180
congratulations, you need to add a new stage between stage1 and
186
For a new file, in most cases, you just have to add it to the proper
187
file list(s) in Makefile.common, such as ARITHVO or TACTICS.
189
The list of all ml4 files is not handled manually anymore.
193
- The file is necessary at stage1, that it is necessary to build the
194
Coq camlp4 grammar extensions. In this case, make sure it ends up
195
in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of
196
grammar.cma and/or q_constr.cmo for an example.
198
- if the file needs to be compiled with -rectypes, add it to
199
RECTYPESML in Makefile.common. If it is a .ml4 file, implement
200
RECTYPESML4 or '(*i ocamlflags i*)'; see TODO.
202
- the file needs a specific Makefile entry; add it to Makefile.build
204
- the files produced from the added file do not match an existing
205
pattern or entry in "Makefile". (All the common cases of
206
.ml{,i,l,y,4}, .v, .c, ... files that produces (respectively)
207
.cm[iox], .vo, .glob, .o, ... files with the same basename are
208
already covered.) In this case, see section "New targets".
215
- a new PHONY target to the build system, that is a target that is
216
not the name of the file it creates,
218
- a normal target is not already mapped to a stage by "Makefile"
222
- add the necessary rule to Makefile.build, if any
223
- add the target to STAGEn_TARGETS, with n being the smallest stage
224
it can be built at, that is:
225
* 1 for OCaml code that doesn't use any Coq camlp4 grammar extension
226
* 2 for OCaml code that uses (directly or indirectly) a Coq
227
camlp4 grammar extension. Indirectly means a dependency of it
229
* 3 for Coq (.v) code.
233
add a pattern matching the target to the pattern lists for the
234
smallest stage it can be built at in "Makefile".
239
delegate pa_extend.cmo to camlp4use statements and remove it from
240
standard camlp4 options.
242
maybe manage compilation flags (such as -rectypes or the CoqIDE ones)
244
(*i ocamlflags: "-rectypes" i*)
245
statement in the .ml(4) files themselves, like camlp4use. The CoqIDE
247
(*i ocamlflags: "${COQIDEFLAGS}" i*)
248
and COQIDEFLAGS is still defined (and exported by) the Makefile.build.
250
Clean up doc/Makefile
252
config/Makefile looks like it contains a lot of unused variables,
253
clean that up (are any maybe used by nightly scripts on
254
pauillac?). Also, the COQTOP variable from config/Makefile (and used
255
in contribs) has a very poorly chosen name, because "coqtop" is the
256
name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
257
to refer to that executable.
259
Promote the granular .glob handling to official way of doing things
260
for Coq developments, that is implement it in coq_makefile and the
261
contribs. Here are a few hints:
263
>> Les fichiers de constantes produits par -dump-glob sont maintenant
264
>> produits par fichier et sont ensuite concaténés dans
265
>> glob.dump. Ilsont produits par défaut (avec les bonnes
268
> C'est une chose que l'on voulait faire aussi.
270
(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.)
272
> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de
275
Dans cette optique, il serait alors plus propre de changer coqdep pour
276
qu'il produise directement l'output que nous mettons maintenant dans
277
les .v.d (qui est celui de coqdoc post-processé avec sed).
279
Si cette manière de gérer les glob devient le standard béni
280
officiellement par "the Coq development team", ne voudrions nous pas
281
changer coqc pour qu'il produise FOO.glob lors de la compilation de
282
FOO.v par défaut (sans argument "-dump-glob")?
284
> et que la production de a.html par coqdoc n'ait une dépendance qu'en
285
> les a.v et a.glob correspondant ?
287
Je crois que coqdoc exige un glob-dump unique, il convient donc de
288
concaténer les .glob correspondants. Soit un glob-dump global par
289
projet (par Makefile), soit un glob-dump global par .v(o), qui
290
contient son .glob et ceux de tous les .v(o) atteignables par le
291
graphe des dépendances. CoRN contient déjà un outil de calcul de
292
partie atteignable du graphe des dépendances (il y est pour un autre
293
usage, pour calculer les .v à mettre dans les différents tarballs sur
294
http://corn.cs.ru.nl/download.html; les parties partielles sont
295
définies par liste de fichiers .v + toutes leurs dépendances
296
(in)directes), il serait alors adéquat de le mettre dans les tools de
added
removed
dev/doc/build-system.txt
