Adapt coq_makefile to handle coqpp-based macro files.

4 files changed, 30 insertions, 14 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 403ad61798..e3fa0c24fe 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -21,6 +21,7 @@ VFILES            := $(COQMF_VFILES)
 MLIFILES          := $(COQMF_MLIFILES)
 MLFILES           := $(COQMF_MLFILES)
 ML4FILES          := $(COQMF_ML4FILES)
+MLGFILES          := $(COQMF_MLGFILES)
 MLPACKFILES       := $(COQMF_MLPACKFILES)
 MLLIBFILES        := $(COQMF_MLLIBFILES)
 CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
@@ -87,6 +88,7 @@ COQTOP   ?= "$(COQBIN)coqtop"
 COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
 COQDOC   ?= "$(COQBIN)coqdoc"
+COQPP    ?= "$(COQBIN)coqpp"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
 
 # Timing scripts
@@ -241,6 +243,7 @@ VDFILE := .coqdeps
 
 ALLSRCFILES := \
 	$(ML4FILES) \
+	$(MLGFILES) \
 	$(MLFILES) \
 	$(MLPACKFILES) \
 	$(MLLIBFILES) \
@@ -262,6 +265,7 @@ TEXFILES = $(VFILES:.v=.tex)
 GTEXFILES = $(VFILES:.v=.g.tex)
 CMOFILES = \
 	$(ML4FILES:.ml4=.cmo) \
+	$(MLGFILES:.mlg=.cmo) \
 	$(MLFILES:.ml=.cmo) \
 	$(MLPACKFILES:.mlpack=.cmo)
 CMXFILES = $(CMOFILES:.cmo=.cmx)
@@ -277,7 +281,7 @@ CMXSFILES = \
 	$(MLPACKFILES:.mlpack=.cmxs) \
 	$(CMXAFILES:.cmxa=.cmxs) \
 	$(if $(MLPACKFILES)$(CMXAFILES),,\
-		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+		$(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
 
 # files that are packed into a plugin (no extension)
 PACKEDFILES = \
@@ -555,6 +559,7 @@ clean::
 	$(HIDE)rm -f $(CMXSFILES)
 	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(MLGFILES:.mlg=.ml)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
@@ -602,11 +607,17 @@ $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
 	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
 	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
 
-$(MLFILES:.ml=.cmo): %.cmo: %.ml
+$(MLGFILES:.mlg=.ml): %.ml: %.mlg
+	$(SHOW)'COQPP $<'
+	$(HIDE)$(COQPP) $<
+
+# Stupid hack around a deficient syntax: we cannot concatenate two expansions
+$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
 	$(SHOW)'CAMLC -c $<'
 	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
 
-$(MLFILES:.ml=.cmx): %.cmx: %.ml
+# Same hack
+$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
 	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
 	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
 
@@ -647,7 +658,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
 # This rule is for _CoqProject with no .mllib nor .mlpack
-$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
 		-shared -o $@ $<
@@ -716,6 +727,10 @@ $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
 	$(SHOW)'CAMLDEP -pp $<'
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
 
+$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
 $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
 	$(SHOW)'CAMLDEP $<'
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 7bb1390cad..ca5a232edb 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -218,7 +218,7 @@ let generate_conf_coq_config oc =
 ;;
 
 let generate_conf_files oc
-  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; }
+  { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; }
 =
   let module S = String in
   let map = map_sourced_list in
@@ -227,6 +227,7 @@ let generate_conf_files oc
   fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
   fprintf oc "COQMF_MLFILES = %s\n"     (S.concat " " (map quote ml_files));
   fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
+  fprintf oc "COQMF_MLGFILES = %s\n"    (S.concat " " (map quote mlg_files));
   fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
   fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
   let cmdline_vfiles = filter_cmdline v_files in
@@ -283,7 +284,7 @@ let generate_conf oc project args  =
 
 let ensure_root_dir
   ({ ml_includes; r_includes; q_includes;
-     v_files; ml_files; mli_files; ml4_files;
+     v_files; ml_files; mli_files; ml4_files; mlg_files;
      mllib_files; mlpack_files } as project)
   =
   let exists f = List.exists (forget_source > f) in
@@ -293,8 +294,8 @@ let ensure_root_dir
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
   || (not_tops v_files &&
-      not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
-      not_tops mllib_files && not_tops mlpack_files)
+      not_tops mli_files && not_tops ml4_files && not_tops mlg_files &&
+      not_tops ml_files && not_tops mllib_files && not_tops mlpack_files)
   then
     project
   else
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 6a913ea894..713b2ad2b6 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -496,9 +496,9 @@ let rec suffixes = function
 
 let add_caml_known phys_dir _ f =
   let basename,suff =
-    get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in
+    get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in
   match suff with
-    | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
     | ".mli" -> add_mli_known basename (Some phys_dir) suff
     | ".mllib" -> add_mllib_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
@@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name =
 	   in
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
-	(match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
+        (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with
 	   | (base,".v") ->
 	       let name = file_name base dirname
 	       and absname = absolute_file_name base dirname in
 	       addQueue vAccu (name, absname)
-	   | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname)
+           | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
 	   | (base,".mli") -> addQueue mliAccu (base,dirname)
 	   | (base,".mllib") -> addQueue mllibAccu (base,dirname)
 	   | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 053a0435ce..155296362f 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -145,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list)
 let mlpackAccu = ref ([] : (string * dir) list)
 
 let add_caml_known phys_dir f =
-  let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in
+  let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in
   match suff with
-    | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()