Since July 2007, Coq features a build system overhauled by Pierre Corbineau and Lionel Elie Mamane. 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 ---------- .ml files corresponding to .ml4 files are created to keep ocamldep happy only. To ensure they are not used for compilation, they contain invalid OCaml. multi-stage build ----------------- Le processus de construction est séparé en trois étapes qui correspondent aux outils nécessaires pour calculer les dépendances de cette étape: stage1: ocamldep, sed , camlp4 sans fichiers de Coq stage2: camlp4 avec grammar.cma et/ou q_constr.cmo stage3: coqdep (.vo) Le Makefile a été séparé en plusieurs fichiers : - Makefile: coquille vide qui délègue les cibles à la bonne étape sauf clean et les fichiers pour emacs (car ils sont en quelque sorte en "stage0": aucun calcul de dépendance nécessaire). - Makefile.common : définitions des variables (essentiellement des listes de fichiers) - Makefile.build : les règles de compilation sans inclure de dépendances - Makefile.stage* : fichiers qui incluent les dépendances calculables à cette étape ainsi que Makefile.build. The build needs to be cut in stages because make will not take into account one include when making another include. Parallélisation --------------- Le découpage en étapes veut dire que le makefile est un petit peu moins parallélisable que strictement possible en théorie: par exemple, certaines choses faites en stage2 pourraient être faites en parallèle avec des choses de stage1. Nous essayons de minimiser cet effet, mais nous ne l'avons pas complètement éliminé parce que cela mènerait à un makefile très complexe. La minimisation est principalement que si on demande un objet spécifique (par exemple "make parsing/g_constr.cmx"), il est fait dans l'étape la plus basse possible (simplement), mais si un objet est fait comme dépendance de la cible demandée (par exemple dans un "make world"), il est fait le plus tard possible (par exemple, tout code OCaml non nécessaire pour coqdep ni grammar.cma ni q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet le parallélisme de compilation de code OCaml et de fichiers Coq (.v)). Le "(simplement)" ci-dessus veut dire que savoir si un fichier non nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en stage1 est compliqué avec make, alors nous retombons en général sur le stage2. La séparation entre le stage2 et stage3 est plus facile, donc l'optimisation ci-dessus s'y applique pleinement. En d'autres mots, nous avons au niveau conceptuel deux assignations d'étape pour chaque fichier: - l'étape la plus petite où nous savons qu'il peut être fait. - l'étape la plus grande où il peut être fait. Mais seule la première est gérée explicitement, la seconde est implicite. 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' ')'"