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
|
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 splitted 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 explicitely 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.
---------------------------------------------------------------------------
This file documents internals of the implementation of the build
system. For what a Coq developer needs to know about the build system,
see build-system.txt .
.ml4 files
----------
.ml4 are converted to .ml by camlp4. 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 hierachy
------------------
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_VCS_CLAUSE
---------------
The recommended style of using FIND_VCS_CLAUSE is for example
find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
find . $(FIND_VCS_CLAUSE) '(' -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_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
one is not tempted to write
find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
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_VCS_CLAUSE) -name '*.example'
it will also list things directly matched by FIND_VCS_CLAUSE
(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_VCS_CLAUSE), ç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' ')'"
|
