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 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' ')'"