Since July 2007, Coq features a build system overhauled by Pierre Corbineau and Lionel Elie Mamane. --------------------------------------------------------------------- WARNING: In March 2010 this build system has been heavily adapted by Pierre Letouzey. In particular there no more explicit stage1,2. Stage3 was removed some time ago when coqdep was splitted into coqdep_boot and full coqdep. Ideas are still similar to what is describe below, but: 1) .ml4 are explicitely turned into .ml files, which stay after build 2) we let "make" handle the inclusion of .d without trying to guess what could be done at what time. Some initial inclusions hence _fail_, but "make" tries again later and succeed. TODO: remove obsolete sections below and better describe the new approach ----------------------------------------------------------------------- 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 . The build system is not at its optimal state, see TODO 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, but doesn't care if this build fails. This can be quite surprising, see in particular the -include in Makefile.stage* Stages in build system ---------------------- The build system is separated into three stages, corresponding to the tool(s) necessary to compute the dependencies necessary at this stage: stage1: ocamldep, sed, camlp4 without Coq extensions stage2: camlp4 with grammar.cma and/or q_constr.cmo stage3: coqdep (.vo) The file "Makefile" itself serves as minimum stage for targets that should not need any dependency (such as *clean*). 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. This will try to minimise the stage at which what you ask for is done (instead of maximising it in order to maximise parallelism of the build process). For example, if you only want to test whether bin/coqtop still builds (and eventually start it to test your bugfix or new feature), don't do "make world" and interrupt it when bin/coqtop is built. Use "make bin/coqtop" or "make coqbinaries" or something like that. This will avoid entering the stage 3, and cut build system overhead by 50% (1.2s instead of 2.4 on writer's machine). - You can turn off rebuilding of the standard library each time bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1. - If you want to avoid all .ml4 files being recompiled only because grammar.cma was rebuilt, do "make ml4depclean" once and then use NO_RECOMPILE_ML4=1. - The CM_STAGE1=1 option to make will build all .cm* files mentioned as targets on the command line in stage1. Whether this will work is your responsibility. It should work for .ml files that don't depend (nor directly nor indirectly through transitive closure of the dependencies) on any .ml4 file, or where those dependencies can be safely ignored in the current situation (e.g. all these .ml4 files don't need to be recompiled). This will avoid entering the stage2 (a reduction of 33% in overhead, 0.4s on the writer's machine). - To jump directly into a stage (e.g. because you know nothing is to be done in stage 1 or (1 and 2) or because you know that the target you give can be, in this situation, done in a lower stage than the build system dares to), use GOTO_STAGE=n. This will jump into stage n and try to do the targets you gave in that stage. - 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. General speed improvements: - When building both the native and bytecode versions, the KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time by running camlp4o only once on every .ml4 file, at the expense of readability of compilation error messages for .ml4 files. 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 camlp4 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 files ---------- The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and can be obtained with: make FOO.ml4-preprocessed If a .ml4 file uses a grammar extension from Coq (such as grammar.cma or q_constr.cmo), it must contain a line like: (*i camlp4deps: "grammar.cma q_constr.cmo" i*) If it uses a standard grammar extension, it must contain a line like: (*i camlp4use: "pa_ifdef.cmo" i*) It can naturally contain both a camlp4deps and a camlp4use line. Both are used for preprocessing. It is thus _not_ necessary to add a specific rule for a .ml4 file in the Makefile.build just because it uses grammar extensions. By default, the build system is geared towards development that may use the Coq grammar extensions, but not development of Coq's grammar extensions themselves. This means that .ml4 files are compiled directly (using ocamlc/opt's -pp option), without use of an intermediary .ml (or .ml4-preprocessed) file. This is so that if a compilation error occurs, the location in the error message is a location in the .ml4 file. If you are modifying the grammar extensions, you may be more interested in the location of the error in the .ml4-preprocessed file, so that you can see what your new grammar extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1 option. This will make compilation of a .ml4 file a two-stage process: 1) create the .ml4-preprocessed file with camlp4o 2) compile it with straight ocamlc/opt without preprocessor and will instruct make not to delete .ml4-preprocessed files automatically just because they are intermediary files, so that you can inspect them. If you add a _new_ grammar extension to Coq: - if it can be built at stage1, that is the .ml4 file does not use a Coq grammar extension itself, then add it, and all .cmo files it needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the handling of grammar.cma and q_constr.cmo for an example. - if it cannot be built at stage1, that is the .ml4 file itself needs to be preprocessed with a Coq camlp4 grammar extension, then, congratulations, you need to add a new stage between stage1 and stage2. New files --------- For a new file, in most cases, you just have to add it to the proper file list(s) in Makefile.common, such as ARITHVO or TACTICS. The list of all ml4 files is not handled manually anymore. Exceptions are: - The file is necessary at stage1, that it is necessary to build the Coq camlp4 grammar extensions. In this case, make sure it ends up in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of grammar.cma and/or q_constr.cmo for an example. - if the file needs to be compiled with -rectypes, add it to RECTYPESML in Makefile.common. If it is a .ml4 file, implement RECTYPESML4 or '(*i ocamlflags i*)'; see TODO. - the file needs a specific Makefile entry; add it to Makefile.build - the files produced from the added file do not match an existing pattern or entry in "Makefile". (All the common cases of .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively) .cm[iox], .vo, .glob, .o, ... files with the same basename are already covered.) In this case, see section "New targets". New targets ----------- If you want to add: - a new PHONY target to the build system, that is a target that is not the name of the file it creates, - a normal target is not already mapped to a stage by "Makefile" then: - add the necessary rule to Makefile.build, if any - add the target to STAGEn_TARGETS, with n being the smallest stage it can be built at, that is: * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension * 2 for OCaml code that uses (directly or indirectly) a Coq camlp4 grammar extension. Indirectly means a dependency of it does. * 3 for Coq (.v) code. *or* add a pattern matching the target to the pattern lists for the smallest stage it can be built at in "Makefile". TODO ---- delegate pa_extend.cmo to camlp4use statements and remove it from standard camlp4 options. maybe manage compilation flags (such as -rectypes or the CoqIDE ones) from a (*i ocamlflags: "-rectypes" i*) statement in the .ml(4) files themselves, like camlp4use. The CoqIDE files could have (*i ocamlflags: "${COQIDEFLAGS}" i*) and COQIDEFLAGS is still defined (and exported by) the Makefile.build. Clean up doc/Makefile config/Makefile looks like it contains a lot of unused variables, clean that up (are any maybe used by nightly scripts on pauillac?). Also, the COQTOP variable from config/Makefile (and used in contribs) has a very poorly chosen name, because "coqtop" is the name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used to refer to that executable. Promote the granular .glob handling to official way of doing things for Coq developments, that is implement it in coq_makefile and the contribs. Here are a few hints: >> Les fichiers de constantes produits par -dump-glob sont maintenant >> produits par fichier et sont ensuite concaténés dans >> glob.dump. Ilsont produits par défaut (avec les bonnes >> dépendances). > C'est une chose que l'on voulait faire aussi. (J'ai testé et débogué ce concept sur CoRN dans les derniers mois.) > Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de > la même façon Dans cette optique, il serait alors plus propre de changer coqdep pour qu'il produise directement l'output que nous mettons maintenant dans les .v.d (qui est celui de coqdoc post-processé avec sed). Si cette manière de gérer les glob devient le standard béni officiellement par "the Coq development team", ne voudrions nous pas changer coqc pour qu'il produise FOO.glob lors de la compilation de FOO.v par défaut (sans argument "-dump-glob")? > et que la production de a.html par coqdoc n'ait une dépendance qu'en > les a.v et a.glob correspondant ? Je crois que coqdoc exige un glob-dump unique, il convient donc de concaténer les .glob correspondants. Soit un glob-dump global par projet (par Makefile), soit un glob-dump global par .v(o), qui contient son .glob et ceux de tous les .v(o) atteignables par le graphe des dépendances. CoRN contient déjà un outil de calcul de partie atteignable du graphe des dépendances (il y est pour un autre usage, pour calculer les .v à mettre dans les différents tarballs sur http://corn.cs.ru.nl/download.html; les parties partielles sont définies par liste de fichiers .v + toutes leurs dépendances (in)directes), il serait alors adéquat de le mettre dans les tools de Coq.