aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in23
-rw-r--r--tools/coq_makefile.ml9
-rw-r--r--tools/coqdep_common.ml8
-rw-r--r--tools/ocamllibdep.mll4
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
| _ -> ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:48:59 +0000