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 camlp5. 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_SKIP_DIRS
---------------

The recommended style of using FIND_SKIP_DIRS is for example

 find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
 find . $(FIND_SKIP_DIRS) '(' -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_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print

one is not tempted to write

 find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print

because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
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_SKIP_DIRS) -name '*.example'
it will also list things directly matched by FIND_SKIP_DIRS
(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_SKIP_DIRS), ç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' ')'"