diff options
| -rw-r--r-- | Makefile | 46 | ||||
| -rw-r--r-- | Makefile.build | 90 | ||||
| -rw-r--r-- | dev/doc/build-system.dev.txt | 130 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 248 |
4 files changed, 172 insertions, 342 deletions
@@ -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. - |