aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-02-27 18:03:49 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-02-27 18:48:23 +0100
commite372b7244bcb8cc449196c29a7dabee6f7f84aa2 (patch)
treed249777e9bdc9ba03aaf1f4455f1a1aee3e8c274
parentca64cc032a3f03381d00d7c9b128688f3f920844 (diff)
Makefile: re-introduce 2 phases to avoid make strange -include's
Yet 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 (as in 2007 and its stage{1,2,3}), but in a lighter way. The main Makefile calls Makefile.build twice : - first for building grammar.cma (and q_constr.cmo), with a restricted set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES). - then on the true target(s) asked by the user (using the special variable MAKECMDGOALS). In pratice, this should change very little to the concrete developper's life, let me know otherwise. A few more messages of make due to the explicit first sub-call, but no more strange "not ready yet" messages... Btw: we should handle correctly now the parallel compilation of multiple targets (e.g. make -jX foo bar). As reported by Pierre B, this was triggering earlier two separate sub-calls to Makefile.build, one for foo, the other for bar, with possibly nasty interactions in case of parallelism. In addition, some cleanup of Makefile.build, removal of useless :: rules, etc etc.
-rw-r--r--Makefile46
-rw-r--r--Makefile.build90
-rw-r--r--dev/doc/build-system.dev.txt130
-rw-r--r--dev/doc/build-system.txt248
4 files changed, 172 insertions, 342 deletions
diff --git a/Makefile b/Makefile
index 10fb51f62..6c03ae05f 100644
--- a/Makefile
+++ b/Makefile
@@ -59,11 +59,20 @@ define find
$(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
endef
+define findx
+ $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
+endef
+
+# We now discriminate .ml4 files according to their need of grammar.cma
+# or q_constr.cmo
+USEGRAMMAR := '(\*.*camlp4deps.*grammar'
+
## Files in the source tree
YACCFILES:=$(call find, '*.mly')
LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
+export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')
@@ -77,13 +86,13 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
GENML4FILES:= $(ML4FILES:.ml4=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
- tools/tolink.ml kernel/copcodes.ml
GENMLIFILES:=$(YACCFILES:.mly=.mli)
GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+ tools/tolink.ml kernel/copcodes.ml $(GENPLUGINSMOD)
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
# NB: all files in $(GENFILES) can be created initially, while
# .ml files in $(GENML4FILES) might need some intermediate building.
@@ -95,8 +104,7 @@ define diff
$(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef
-export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
-export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
include Makefile.common
@@ -107,7 +115,7 @@ include Makefile.common
NOARG: world
-.PHONY: NOARG help always
+.PHONY: NOARG help noconfig submake
help:
@echo "Please use either"
@@ -131,17 +139,27 @@ endif
# Apart from clean and tags, everything will be done in a sub-call to make
# on Makefile.build. This way, we avoid doing here the -include of .d :
-# since they trigger some compilations, we do not want them for a mere clean
+# since they trigger some compilations, we do not want them for a mere clean.
+# Moreover, we regroup this sub-call in a common target named 'submake'.
+# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
+# trigger multiple (possibly parallel) make sub-calls
ifdef COQ_CONFIGURED
-%:: always
- $(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@"
+%:: submake ;
else
-%:: always
- @echo "Please run ./configure first" >&2; exit 1
+%:: noconfig ;
endif
-always : ;
+MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
+
+GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo
+
+submake:
+ $(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS)
+ $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
+
+noconfig:
+ @echo "Please run ./configure first" >&2; exit 1
# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
@@ -165,7 +183,7 @@ cruftclean: ml4clean
indepclean:
rm -f $(GENFILES)
- rm -f $(COQTOPBYTE) $(CHICKENBYTE) bin/fake_ide
+ rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE)
find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
rm -f */*.pp[iox] plugins/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
@@ -234,7 +252,7 @@ devdocclean:
# Emacs tags
###########################################################################
-.PHONY: tags
+.PHONY: tags printenv
tags:
echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
diff --git a/Makefile.build b/Makefile.build
index 312db8ec9..760a4db72 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -14,7 +14,9 @@
###########################################################################
# build the different subsystems: coq, coqide
-world: revision coq coqide
+world: revision coq coqide documentation
+
+.PHONY: world
###########################################################################
# Includes
@@ -23,40 +25,29 @@ world: revision coq coqide
include Makefile.common
include Makefile.doc
-ifeq ($(LOCAL),true)
-install:
- @echo "Nothing to install in a local build!"
+# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+
+ifdef BUILDGRAMMAR
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
+ CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
else
-install: install-coq install-coqide install-doc-$(WITHDOC)
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+ CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
endif
-install-doc-all: install-doc
-install-doc-no:
-
-world: doc-$(WITHDOC)
-doc-all: doc
-doc-no:
-
-.PHONY: world install install-doc-all install-doc-no doc-all doc-no
+CURDEPS:=$(addsuffix .d, $(CURFILES))
# All dependency includes must be declared secondary, otherwise make will
# delete them if it decided to build them by dependency instead of because
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
-MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
-
-ALLDEPS:=$(addsuffix .d, \
- $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
+.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
+# This include below will lauch the build of all concerned .d.
+# The - at front is for disabling warnings about currently missing ones.
-# NOTA: the -include below will lauch the build of all .d. Some of them
-# will _fail_ at first, this is to be expected (no grammar.cma initially).
-# These errors (see below "not ready yet") do not discourage make to
-# try again and finally succeed.
-
--include $(ALLDEPS)
+-include $(CURDEPS)
###########################################################################
@@ -205,11 +196,11 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
.PHONY: coqbinaries coq coqlib coqlight states
-coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
+coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
coq: coqlib tools coqbinaries
-coqlib:: theories plugins
+coqlib: theories plugins
coqlight: theories-light tools coqbinaries
@@ -300,7 +291,7 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
# target to build CoqIde
-coqide:: coqide-files coqide-binaries theories/Init/Prelude.vo
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
@@ -385,7 +376,7 @@ $(ALLSTDLIB).v:
MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
-check:: validate test-suite
+check: validate test-suite
test-suite: world $(ALLSTDLIB).v
$(MAKE) $(MAKE_TSOPTS) clean
@@ -493,7 +484,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g
printers: $(DEBUGPRINTERS)
-tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
+tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
# coqdep_boot : a basic version of coqdep, with almost no dependencies.
@@ -564,9 +555,31 @@ tools/compat5b.cmo: tools/compat5b.ml
endif
###########################################################################
+# Documentation : cf Makefile.doc
+###########################################################################
+
+documentation: doc-$(WITHDOC)
+doc-all: doc
+doc-no:
+
+.PHONY: documentation doc-all doc-no
+
+###########################################################################
# Installation
###########################################################################
+ifeq ($(LOCAL),true)
+install:
+ @echo "Nothing to install in a local build!"
+else
+install: install-coq install-coqide install-doc-$(WITHDOC)
+endif
+
+install-doc-all: install-doc
+install-doc-no:
+
+.PHONY: install install-doc-all install-doc-no
+
#These variables are intended to be set by the caller to make
#COQINSTALLPREFIX=
#OLDROOT=
@@ -605,7 +618,7 @@ install-binaries: install-tools
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
-install-tools::
+install-tools:
$(MKDIR) $(FULLBINDIR)
# recopie des fichiers de style pour coqide
$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
@@ -683,18 +696,18 @@ install-latex:
source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
-$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
+$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@
-mli-doc:: $(DOCMLIS:.mli=.cmi)
+mli-doc: $(DOCMLIS:.mli=.cmi)
$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
-ml-dot:: $(MLEXTRAFILES)
+ml-dot: $(MLFILES)
$(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
@@ -884,11 +897,8 @@ plugins/%_mod.ml: plugins/%.mllib
%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
$(SHOW)'CAMLP4O $<'
- $(HIDE)\
- DEPS="$(call CAMLP4DEPS,$<)"; \
- if ls $${DEPS} > /dev/null 2>&1; then \
- $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
- else echo $< : Dependency $${DEPS} not ready yet; false; fi
+ $(HIDE)$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo \
+ $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
$(SHOW)'COQC $<'
@@ -966,6 +976,10 @@ otags:
###########################################################################
+# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
+
+Makefile Makefile.build Makefile.common config/Makefile : ;
+
# For emacs:
# Local Variables:
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index 3d9cba143..af1120e97 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,21 +1,38 @@
-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
------------------------------------------------------------------------
+
+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.
+
+
+---------------------------------------------------------------------------
+
This file documents internals of the implementation of the build
system. For what a Coq developer needs to know about the build system,
@@ -24,68 +41,47 @@ 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.
-
+.ml4 are converted to .ml by camlp4. 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.
-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)
+Makefiles hierachy
+------------------
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: coquille vide qui lançant Makefile.build sauf pour
+ clean et quelques petites choses ne nécessitant par de calculs
+ de dépendances.
- 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.
+- Makefile.build : contient les regles de compilation, ainsi que
+ le "include" des dépendances (restreintes ou non selon la variable
+ BUILDGRAMMAR).
+- Makefile.doc : regles specifiques à la compilation de la documentation.
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.
+Il y a actuellement un double appel interne à "make -f Makefile.build",
+d'abord pour construire grammar.cma/q_constr.cmo, puis le reste.
+Cela signifie que ce makefile est un petit peu moins parallélisable
+que strictement possible en théorie: par exemple, certaines choses
+faites lors du second make pourraient être faites en parallèle avec
+le premier. En pratique, ce premier make va suffisemment vite pour
+que cette limitation soit peu gênante.
FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index d7cf396ff..31d9875ad 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -1,26 +1,8 @@
-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.
+about its implementation details), see build-system.dev.txt, and in
+particular its initial HISTORY section.
FAQ: special features used in this Makefile
@@ -51,22 +33,10 @@ $(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*).
+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)
------------------------
@@ -97,37 +67,11 @@ 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).
-
+ 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), 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).
-
- - 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.
+ 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
@@ -135,12 +79,6 @@ save precious time:
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
------------
@@ -178,166 +116,30 @@ Targets for cleaning various parts:
.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.
+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) in Makefile.common, such as ARITHVO or TACTICS.
+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.
-
-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.
-