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
|
This file documents what a Coq developer needs to know about the build
system. If you want to enhance the build system itself (or are curious
about its implementation details), see build-system.dev.txt, and in
particular its initial HISTORY section.
FAQ: special features used in this Makefile
-------------------------------------------
* Order-only dependencies: |
Dependencies placed after a bar (|) should be built before
the current rule, but having one of them is out-of-date do not
trigger a rebuild of the current rule.
See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types
* Annotation before commands: +/-/@
a command starting by - is always successful (errors are ignored)
a command starting by + is runned even if option -n is given to make
a command starting by @ is not echoed before being runned
* Custom functions
Definition via "define foo" followed by commands (arg is $(1) etc)
Call via "$(call foo,arg1)"
* Useful builtin functions
$(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...)
* Behavior of -include
If the file given to -include doesn't exist, make tries to build it,
and even retries again if necessary, but doesn't care if this build
finally fails. We used to rely on this "feature", but this should not
be the case anymore. We kept "-include" instead of "include" for
avoiding warnings about initially non-existant files.
Changes (for old-timers)
------------------------
The contents of the old Makefile has been mostly split into:
- variable declarations for file lists in Makefile.common.
These declarations are now static (for faster Makefile execution),
so their definitions are order-dependent.
- actual building rules and compiler flags variables in
Makefile.build
The handling of globals is now: the globals of FOO.v are in FOO.glob
and the global glob.dump is created by concatenation of all .glob
files. In particular, .glob files are now always created.
See also section "cleaning targets"
Reducing build system overhead
------------------------------
When you are actively working on a file in a "make a change, make to
test, make a change, make to test", etc mode, here are a few tips to
save precious time:
- Always ask for what you want directly (e.g. bin/coqtop,
foo/bar.cmo, ...), don't do "make world" and interrupt
it when it has done what you want.
For example, if you only want to test whether bin/coqtop still
builds (and eventually start it to test your bugfix or new
feature), use "make bin/coqtop" or "make coqbinaries" or something
like that.
- To disable all dependency recalculation, use the NO_RECALC_DEPS=1
option. It disables REcalculation of dependencies, not calculation
of dependencies. In other words, if a .d file does not exist, it is
still created, but it is not updated every time the source file
(e.g. .ml) is changed.
Dependencies
------------
There are no dependencies in the archive anymore, they are always
bootstrapped. The dependencies of a file FOO are in FOO.d . This
enables partial recalculation of dependencies (only the dependencies
of changed files are recomputed).
If you add a dependency to a Coq camlp5 extension (grammar.cma or
q_constr.cmo), then see sections ".ml4 files" and "new files".
Cleaning Targets
----------------
Targets for cleaning various parts:
- distclean: clean everything; must leave only what should end up in
distribution tarball and/or is in a svn checkout.
- clean: clean everything except effect of "./configure" and documentation.
- cleanconfig: clean effect of "./configure" only
- archclean: remove all architecture-dependent generated files
- indepclean: remove all architecture-independent generated files
(not documentation)
- objclean: clean all generated files, but not Makefile meta-data
(e.g. dependencies), nor debugging/development information nor
other cruft (e.g. editor backup files), nor documentation
- docclean: clean documentation
.ml4/.mlp files
---------------
There is now two kinds of preprocessed files :
- a .mlp do not need grammar.cma (they are in grammar/)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
This classification replaces the old mechanism of declaring the use
of a grammar extension via a line of the form:
(*i camlp4deps: "grammar.cma q_constr.cmo" i*)
The use of (*i camlp4use: ... i*) to mention uses of standard
extension such as IFDEF has also been discontinued, the Makefile now
always calls camlp5 with pa_macros.cmo and a few others by default.
For debugging a Coq grammar extension, it could be interesting
to use the READABLE_ML4=1 option, otherwise the generated .ml are
in an internal binary format (see build-system.dev.txt).
New files
---------
For a new file, in most cases, you just have to add it to the proper
file list(s):
- For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
These files are also used by the experimental ocamlbuild plugin,
which is quite touchy about them : be careful with order,
duplicated entries, whitespace errors, and do not mention .mli there.
If module B depends on module A, then B should be after A in the .mllib
file.
- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
- The definitions in Makefile.common might have to be adapted too.
- If your file needs a specific rule, add it to Makefile.build
The list of all ml4 files is not handled manually anymore.
|
