From ded46fc00ee76c3f2568619e1a48034b5865a8f2 Mon Sep 17 00:00:00 2001 From: lmamane Date: Wed, 13 Feb 2008 16:32:07 +0000 Subject: Implement KEEP_ML4_PREPROCESSED option in build system git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 6 +++--- Makefile.build | 29 ++++++++++++++++++++--------- dev/doc/build-system.txt | 30 ++++++++++++++++++++++++++++-- 3 files changed, 51 insertions(+), 14 deletions(-) diff --git a/Makefile b/Makefile index 0da3ac091..be1ee4ef2 100644 --- a/Makefile +++ b/Makefile @@ -112,10 +112,10 @@ ifdef CM_STAGE1 $(CAML_OBJECT_PATTERNS): always $(call stage-template,1) -%.ml4.preprocessed: stage1 +%.ml4-preprocessed: stage1 $(call stage-template,2) else -$(CAML_OBJECT_PATTERNS) %.ml4.preprocessed: stage1 +$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1 $(call stage-template,2) endif @@ -177,7 +177,7 @@ clean-ide: rm -f ide/utf8_convert.ml ml4clean: - rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4.preprocessed) + rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed) ml4depclean: find . -name '*.ml4.d' | xargs rm -f diff --git a/Makefile.build b/Makefile.build index 08a8a7cbc..86211d0c3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -721,11 +721,11 @@ toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here define rectypes-rules-template $(1:.ml=.cmo): $(1) | $(1).d - $(SHOW)'OCAMLC -rectypes $$<' + $(SHOW)'OCAMLC -rectypes $$<' $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $$< $(1:.ml=.cmx): $(1) | $(1).d - $(SHOW)'OCAMLOPT -rectypes $$<' + $(SHOW)'OCAMLOPT -rectypes $$<' $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $$< endef @@ -776,10 +776,25 @@ endif $(SHOW)'CC $<' $(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES) -c $< +ifdef KEEP_ML4_PREPROCESSED +.PRECIOUS: %.ml4-preprocessed +%.cmo: %.ml4-preprocessed | %.ml4.ml.d + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< + +%.cmx: %.ml4-preprocessed | %.ml4.ml.d + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< +else %.cmo: %.ml4 | %.ml4.ml.d %.ml4.d $(SHOW)'OCAMLC4 $<' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< +%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d + $(SHOW)'OCAMLOPT4 $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< +endif + %.cmo: %.ml | %.ml.d $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< @@ -788,10 +803,6 @@ endif $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< -%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d - $(SHOW)'OCAMLOPT4 $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< - %.cmx: %.ml | %.ml.d $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c $< @@ -804,8 +815,8 @@ endif $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) $< -%.ml4.preprocessed: %.ml4 | %.ml4.d - $(SHOW)'CAMLP4O $<' +%.ml4-preprocessed: %.ml4 | %.ml4.d + $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) @@ -827,7 +838,7 @@ else endif %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(SHOW)'CAMLP4DEPS $<' - $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \ + $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) %.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index e4ecf9e5f..f43e21963 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -90,6 +90,13 @@ save precious time: still created, but it is not updated every time the source file (e.g. .ml) is changes. +General speed improvements: + + - When building both the native and bytecode versions, the + KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time + by running camp4o only once on every .ml4 file, at the expense of + readability of compilation error messages for .ml4 files. + Dependencies ------------ @@ -126,9 +133,9 @@ Targets for cleaning various parts: .ml4 files ---------- -The camlp4-preprocessed version of FOO.ml4 is FOO.ml4.preprocessed and +The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and can be obtained with: - make FOO.ml4.preprocessed + 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: @@ -142,6 +149,25 @@ 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 -- cgit v1.2.3