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 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
----------

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*)

The use of (*i camlp4use: ... i*) to mention uses of standard
extension such as IFDEF has been discontinued, the Makefile now
always calls camlp4 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.
 - 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.