1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
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' ')'"
|
