From 509c30c93dca8ca8c78f1da1eefc056226d90346 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 1 Jun 2016 12:03:35 +0200 Subject: Compilation via pack for plugins of the stdlib For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts. --- .gitignore | 3 +- Makefile | 6 +-- Makefile.build | 41 +++++++++++++------- Makefile.common | 52 ++++++++++++------------- plugins/btauto/btauto_plugin.mllib | 3 -- plugins/btauto/btauto_plugin.mlpack | 2 + plugins/cc/cc_plugin.mllib | 5 --- plugins/cc/cc_plugin.mlpack | 4 ++ plugins/decl_mode/decl_mode_plugin.mllib | 6 --- plugins/decl_mode/decl_mode_plugin.mlpack | 5 +++ plugins/decl_mode/g_decl_mode.ml4 | 2 + plugins/derive/derive_plugin.mllib | 2 - plugins/derive/derive_plugin.mlpack | 2 + plugins/derive/g_derive.ml4 | 2 + plugins/extraction/extraction_plugin.mllib | 12 ------ plugins/extraction/extraction_plugin.mlpack | 11 ++++++ plugins/extraction/g_extraction.ml4 | 2 + plugins/firstorder/g_ground.ml4 | 2 + plugins/firstorder/ground_plugin.mllib | 8 ---- plugins/firstorder/ground_plugin.mlpack | 7 ++++ plugins/fourier/fourier_plugin.mllib | 4 -- plugins/fourier/fourier_plugin.mlpack | 3 ++ plugins/funind/recdef.ml | 2 +- plugins/funind/recdef_plugin.mllib | 11 ------ plugins/funind/recdef_plugin.mlpack | 10 +++++ plugins/micromega/micromega_plugin.mllib | 10 ----- plugins/micromega/micromega_plugin.mlpack | 9 +++++ plugins/nsatz/nsatz_plugin.mllib | 6 --- plugins/nsatz/nsatz_plugin.mlpack | 5 +++ plugins/omega/omega_plugin.mllib | 4 -- plugins/omega/omega_plugin.mlpack | 3 ++ plugins/quote/quote_plugin.mllib | 3 -- plugins/quote/quote_plugin.mlpack | 2 + plugins/romega/refl_omega.ml | 2 +- plugins/romega/romega_plugin.mllib | 4 -- plugins/romega/romega_plugin.mlpack | 3 ++ plugins/rtauto/rtauto_plugin.mllib | 4 -- plugins/rtauto/rtauto_plugin.mlpack | 3 ++ plugins/setoid_ring/newring.ml | 1 + plugins/setoid_ring/newring_plugin.mllib | 3 -- plugins/setoid_ring/newring_plugin.mlpack | 2 + plugins/syntax/ascii_syntax.ml | 4 ++ plugins/syntax/ascii_syntax_plugin.mllib | 2 - plugins/syntax/ascii_syntax_plugin.mlpack | 1 + plugins/syntax/nat_syntax.ml | 4 ++ plugins/syntax/nat_syntax_plugin.mllib | 2 - plugins/syntax/nat_syntax_plugin.mlpack | 1 + plugins/syntax/numbers_syntax.ml | 6 ++- plugins/syntax/numbers_syntax_plugin.mllib | 2 - plugins/syntax/numbers_syntax_plugin.mlpack | 1 + plugins/syntax/r_syntax.ml | 4 ++ plugins/syntax/r_syntax_plugin.mllib | 2 - plugins/syntax/r_syntax_plugin.mlpack | 1 + plugins/syntax/string_syntax.ml | 6 ++- plugins/syntax/string_syntax_plugin.mllib | 2 - plugins/syntax/string_syntax_plugin.mlpack | 1 + plugins/syntax/z_syntax.ml | 4 ++ plugins/syntax/z_syntax_plugin.mllib | 2 - plugins/syntax/z_syntax_plugin.mlpack | 1 + tools/ocamllibdep.mll | 60 ++++++++++++++++++----------- 60 files changed, 208 insertions(+), 169 deletions(-) delete mode 100644 plugins/btauto/btauto_plugin.mllib create mode 100644 plugins/btauto/btauto_plugin.mlpack delete mode 100644 plugins/cc/cc_plugin.mllib create mode 100644 plugins/cc/cc_plugin.mlpack delete mode 100644 plugins/decl_mode/decl_mode_plugin.mllib create mode 100644 plugins/decl_mode/decl_mode_plugin.mlpack delete mode 100644 plugins/derive/derive_plugin.mllib create mode 100644 plugins/derive/derive_plugin.mlpack delete mode 100644 plugins/extraction/extraction_plugin.mllib create mode 100644 plugins/extraction/extraction_plugin.mlpack delete mode 100644 plugins/firstorder/ground_plugin.mllib create mode 100644 plugins/firstorder/ground_plugin.mlpack delete mode 100644 plugins/fourier/fourier_plugin.mllib create mode 100644 plugins/fourier/fourier_plugin.mlpack delete mode 100644 plugins/funind/recdef_plugin.mllib create mode 100644 plugins/funind/recdef_plugin.mlpack delete mode 100644 plugins/micromega/micromega_plugin.mllib create mode 100644 plugins/micromega/micromega_plugin.mlpack delete mode 100644 plugins/nsatz/nsatz_plugin.mllib create mode 100644 plugins/nsatz/nsatz_plugin.mlpack delete mode 100644 plugins/omega/omega_plugin.mllib create mode 100644 plugins/omega/omega_plugin.mlpack delete mode 100644 plugins/quote/quote_plugin.mllib create mode 100644 plugins/quote/quote_plugin.mlpack delete mode 100644 plugins/romega/romega_plugin.mllib create mode 100644 plugins/romega/romega_plugin.mlpack delete mode 100644 plugins/rtauto/rtauto_plugin.mllib create mode 100644 plugins/rtauto/rtauto_plugin.mlpack delete mode 100644 plugins/setoid_ring/newring_plugin.mllib create mode 100644 plugins/setoid_ring/newring_plugin.mlpack delete mode 100644 plugins/syntax/ascii_syntax_plugin.mllib create mode 100644 plugins/syntax/ascii_syntax_plugin.mlpack delete mode 100644 plugins/syntax/nat_syntax_plugin.mllib create mode 100644 plugins/syntax/nat_syntax_plugin.mlpack delete mode 100644 plugins/syntax/numbers_syntax_plugin.mllib create mode 100644 plugins/syntax/numbers_syntax_plugin.mlpack delete mode 100644 plugins/syntax/r_syntax_plugin.mllib create mode 100644 plugins/syntax/r_syntax_plugin.mlpack delete mode 100644 plugins/syntax/string_syntax_plugin.mllib create mode 100644 plugins/syntax/string_syntax_plugin.mlpack delete mode 100644 plugins/syntax/z_syntax_plugin.mllib create mode 100644 plugins/syntax/z_syntax_plugin.mlpack diff --git a/.gitignore b/.gitignore index 116f88dd7..1cbf56e3c 100644 --- a/.gitignore +++ b/.gitignore @@ -44,7 +44,6 @@ TAGS .pc bin/ _build -plugins/*/*_mod.ml myocamlbuild_config.ml config/Makefile config/coq_config.ml @@ -114,7 +113,7 @@ tools/ocamllibdep.ml tools/coqdoc/cpretty.ml ide/xml_lexer.ml -# .ml4 files +# .ml4 / .mlp files g_*.ml diff --git a/Makefile b/Makefile index aeb54fba8..93b89a489 100644 --- a/Makefile +++ b/Makefile @@ -66,7 +66,7 @@ endef ## Files in the source tree LEXFILES := $(call find, '*.mll') -export MLLIBFILES := $(call find, '*.mllib') +export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') @@ -80,9 +80,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(GENPLUGINSMOD) \ - tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) diff --git a/Makefile.build b/Makefile.build index 69228e379..4eafe1d61 100644 --- a/Makefile.build +++ b/Makefile.build @@ -502,6 +502,16 @@ endif $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) +# For plugin packs : + +%.cmo: %.mlpack + $(SHOW)'OCAMLC -pack -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) + +%.cmx: %.mlpack + $(SHOW)'OCAMLOPT -pack -o $@' + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) + COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) @@ -537,18 +547,22 @@ $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo +# NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep +# The only exceptions are the sources of the csdpcert binary. +# To avoid warnings, we set them manually here: +plugins/micromega/sos_lib_FORPACK:= +plugins/micromega/sos_FORPACK:= +plugins/micromega/sos_print_FORPACK:= +plugins/micromega/csdpcert_FORPACK:= + +plugins/%.cmx: plugins/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< + %.cmx: %.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< -%.cmxs: %.cmxa - $(SHOW)'OCAMLOPT -shared -o $@' -ifeq ($(HASNATDYNLINK),os5fixme) - $(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@ -else - $(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $< -endif - %.cmxs: %.cmx $(SHOW)'OCAMLOPT -shared -o $@' $(HIDE)$(OCAMLOPT) -shared -o $@ $< @@ -557,11 +571,6 @@ endif $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -plugins/%_mod.ml: plugins/%.mllib - $(SHOW)'ECHO... > $@' - $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ - $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ - %.ml: %.ml4 | $(CAMLP4DEPS) $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \ @@ -573,7 +582,7 @@ plugins/%_mod.ml: plugins/%.mllib ########################################################################### # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) -OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' @@ -587,6 +596,10 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 $(SHOW)'OCAMLLIBDEP $<' $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) + ########################################################################### # Compilation of .v files ########################################################################### diff --git a/Makefile.common b/Makefile.common index 463006c49..4742bb51e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -97,28 +97,28 @@ OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) # plugins object files ########################################################################### -OMEGACMA:=plugins/omega/omega_plugin.cma -ROMEGACMA:=plugins/romega/romega_plugin.cma -MICROMEGACMA:=plugins/micromega/micromega_plugin.cma -QUOTECMA:=plugins/quote/quote_plugin.cma -RINGCMA:=plugins/setoid_ring/newring_plugin.cma -NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -FOURIERCMA:=plugins/fourier/fourier_plugin.cma -EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma -FUNINDCMA:=plugins/funind/recdef_plugin.cma -FOCMA:=plugins/firstorder/ground_plugin.cma -CCCMA:=plugins/cc/cc_plugin.cma -BTAUTOCMA:=plugins/btauto/btauto_plugin.cma -RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma -NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma +OMEGACMA:=plugins/omega/omega_plugin.cmo +ROMEGACMA:=plugins/romega/romega_plugin.cmo +MICROMEGACMA:=plugins/micromega/micromega_plugin.cmo +QUOTECMA:=plugins/quote/quote_plugin.cmo +RINGCMA:=plugins/setoid_ring/newring_plugin.cmo +NSATZCMA:=plugins/nsatz/nsatz_plugin.cmo +FOURIERCMA:=plugins/fourier/fourier_plugin.cmo +EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cmo +FUNINDCMA:=plugins/funind/recdef_plugin.cmo +FOCMA:=plugins/firstorder/ground_plugin.cmo +CCCMA:=plugins/cc/cc_plugin.cmo +BTAUTOCMA:=plugins/btauto/btauto_plugin.cmo +RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cmo +NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cmo OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ - z_syntax_plugin.cma \ - numbers_syntax_plugin.cma \ - r_syntax_plugin.cma \ - ascii_syntax_plugin.cma \ - string_syntax_plugin.cma ) -DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -DERIVECMA:=plugins/derive/derive_plugin.cma + z_syntax_plugin.cmo \ + numbers_syntax_plugin.cmo \ + r_syntax_plugin.cmo \ + ascii_syntax_plugin.cmo \ + string_syntax_plugin.cmo ) +DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo +DERIVECMA:=plugins/derive/derive_plugin.cmo PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ @@ -131,17 +131,17 @@ ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs) PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) + PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs) else ifeq ($(BEST),byte) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs) PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) + PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs) else STATICPLUGINS:=$(PLUGINSCMA) INITPLUGINS:= @@ -152,7 +152,7 @@ endif endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) -LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) +LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ########################################################################### # vo files diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mllib deleted file mode 100644 index 319a9c302..000000000 --- a/plugins/btauto/btauto_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Refl_btauto -G_btauto -Btauto_plugin_mod diff --git a/plugins/btauto/btauto_plugin.mlpack b/plugins/btauto/btauto_plugin.mlpack new file mode 100644 index 000000000..2410f906a --- /dev/null +++ b/plugins/btauto/btauto_plugin.mlpack @@ -0,0 +1,2 @@ +Refl_btauto +G_btauto diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib deleted file mode 100644 index 1bcfc5378..000000000 --- a/plugins/cc/cc_plugin.mllib +++ /dev/null @@ -1,5 +0,0 @@ -Ccalgo -Ccproof -Cctac -G_congruence -Cc_plugin_mod diff --git a/plugins/cc/cc_plugin.mlpack b/plugins/cc/cc_plugin.mlpack new file mode 100644 index 000000000..27e903fd3 --- /dev/null +++ b/plugins/cc/cc_plugin.mlpack @@ -0,0 +1,4 @@ +Ccalgo +Ccproof +Cctac +G_congruence diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib deleted file mode 100644 index 39342dbd1..000000000 --- a/plugins/decl_mode/decl_mode_plugin.mllib +++ /dev/null @@ -1,6 +0,0 @@ -Decl_mode -Decl_interp -Decl_proof_instr -Ppdecl_proof -G_decl_mode -Decl_mode_plugin_mod diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack new file mode 100644 index 000000000..1b84a0790 --- /dev/null +++ b/plugins/decl_mode/decl_mode_plugin.mlpack @@ -0,0 +1,5 @@ +Decl_mode +Decl_interp +Decl_proof_instr +Ppdecl_proof +G_decl_mode diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 78a95143d..0feba6365 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "decl_mode_plugin" + open Compat open Pp open Decl_expr diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mllib deleted file mode 100644 index 5ee0fc6da..000000000 --- a/plugins/derive/derive_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Derive -G_derive diff --git a/plugins/derive/derive_plugin.mlpack b/plugins/derive/derive_plugin.mlpack new file mode 100644 index 000000000..5ee0fc6da --- /dev/null +++ b/plugins/derive/derive_plugin.mlpack @@ -0,0 +1,2 @@ +Derive +G_derive diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 39cad4d03..d4dc7e0ee 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -10,6 +10,8 @@ open Constrarg (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "derive_plugin" + let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib deleted file mode 100644 index ad3212434..000000000 --- a/plugins/extraction/extraction_plugin.mllib +++ /dev/null @@ -1,12 +0,0 @@ -Table -Mlutil -Modutil -Extraction -Common -Ocaml -Haskell -Scheme -Json -Extract_env -G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/extraction_plugin.mlpack b/plugins/extraction/extraction_plugin.mlpack new file mode 100644 index 000000000..9184f6501 --- /dev/null +++ b/plugins/extraction/extraction_plugin.mlpack @@ -0,0 +1,11 @@ +Table +Mlutil +Modutil +Extraction +Common +Ocaml +Haskell +Scheme +Json +Extract_env +G_extraction diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 0a8cb0ccd..19fda4aea 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "extraction_plugin" + (* ML names *) open Genarg diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index a78532e33..cec3505a9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -153,6 +153,8 @@ TACTIC EXTEND gintuition END open Proofview.Notations +open Cc_plugin +open Decl_mode_plugin let default_declarative_automation = Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *) diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib deleted file mode 100644 index 447a1fb51..000000000 --- a/plugins/firstorder/ground_plugin.mllib +++ /dev/null @@ -1,8 +0,0 @@ -Formula -Unify -Sequent -Rules -Instances -Ground -G_ground -Ground_plugin_mod diff --git a/plugins/firstorder/ground_plugin.mlpack b/plugins/firstorder/ground_plugin.mlpack new file mode 100644 index 000000000..65fb2e9a1 --- /dev/null +++ b/plugins/firstorder/ground_plugin.mlpack @@ -0,0 +1,7 @@ +Formula +Unify +Sequent +Rules +Instances +Ground +G_ground diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib deleted file mode 100644 index 0383b1a80..000000000 --- a/plugins/fourier/fourier_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Fourier -FourierR -G_fourier -Fourier_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack new file mode 100644 index 000000000..b6262f8ae --- /dev/null +++ b/plugins/fourier/fourier_plugin.mlpack @@ -0,0 +1,3 @@ +Fourier +FourierR +G_fourier diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 80866e8b8..95b4967fa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib deleted file mode 100644 index ec1f5436c..000000000 --- a/plugins/funind/recdef_plugin.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Indfun_common -Glob_termops -Recdef -Glob_term_to_relation -Functional_principles_proofs -Functional_principles_types -Invfun -Indfun -Merge -G_indfun -Recdef_plugin_mod diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack new file mode 100644 index 000000000..2b443f2a1 --- /dev/null +++ b/plugins/funind/recdef_plugin.mlpack @@ -0,0 +1,10 @@ +Indfun_common +Glob_termops +Recdef +Glob_term_to_relation +Functional_principles_proofs +Functional_principles_types +Invfun +Indfun +Merge +G_indfun diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib deleted file mode 100644 index f53a9e379..000000000 --- a/plugins/micromega/micromega_plugin.mllib +++ /dev/null @@ -1,10 +0,0 @@ -Sos_types -Mutils -Micromega -Polynomial -Mfourier -Certificate -Persistent_cache -Coq_micromega -G_micromega -Micromega_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mlpack b/plugins/micromega/micromega_plugin.mlpack new file mode 100644 index 000000000..ed253da3f --- /dev/null +++ b/plugins/micromega/micromega_plugin.mlpack @@ -0,0 +1,9 @@ +Sos_types +Mutils +Micromega +Polynomial +Mfourier +Certificate +Persistent_cache +Coq_micromega +G_micromega diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mllib deleted file mode 100644 index e991fb76f..000000000 --- a/plugins/nsatz/nsatz_plugin.mllib +++ /dev/null @@ -1,6 +0,0 @@ -Utile -Polynom -Ideal -Nsatz -G_nsatz -Nsatz_plugin_mod diff --git a/plugins/nsatz/nsatz_plugin.mlpack b/plugins/nsatz/nsatz_plugin.mlpack new file mode 100644 index 000000000..b55adf43c --- /dev/null +++ b/plugins/nsatz/nsatz_plugin.mlpack @@ -0,0 +1,5 @@ +Utile +Polynom +Ideal +Nsatz +G_nsatz diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib deleted file mode 100644 index 2b387fdce..000000000 --- a/plugins/omega/omega_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Omega -Coq_omega -G_omega -Omega_plugin_mod diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack new file mode 100644 index 000000000..df7f1047f --- /dev/null +++ b/plugins/omega/omega_plugin.mlpack @@ -0,0 +1,3 @@ +Omega +Coq_omega +G_omega diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib deleted file mode 100644 index d1b3ccbe1..000000000 --- a/plugins/quote/quote_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Quote -G_quote -Quote_plugin_mod diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack new file mode 100644 index 000000000..2e9be09d8 --- /dev/null +++ b/plugins/quote/quote_plugin.mlpack @@ -0,0 +1,2 @@ +Quote +G_quote diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 007a9ec67..a059512d8 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -9,7 +9,7 @@ open Pp open Util open Const_omega -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* \section{Useful functions and flags} *) diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib deleted file mode 100644 index 1625009d0..000000000 --- a/plugins/romega/romega_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Const_omega -Refl_omega -G_romega -Romega_plugin_mod diff --git a/plugins/romega/romega_plugin.mlpack b/plugins/romega/romega_plugin.mlpack new file mode 100644 index 000000000..38d0e9411 --- /dev/null +++ b/plugins/romega/romega_plugin.mlpack @@ -0,0 +1,3 @@ +Const_omega +Refl_omega +G_romega diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib deleted file mode 100644 index 0e3460449..000000000 --- a/plugins/rtauto/rtauto_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Proof_search -Refl_tauto -G_rtauto -Rtauto_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mlpack b/plugins/rtauto/rtauto_plugin.mlpack new file mode 100644 index 000000000..61c5e945b --- /dev/null +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -0,0 +1,3 @@ +Proof_search +Refl_tauto +G_rtauto diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 154ec6e1b..7af72b07c 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -106,6 +106,7 @@ let protect_tac_in map id = (****************************************************************************) let closed_term t l = + let open Quote_plugin in let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib deleted file mode 100644 index 7d6c49588..000000000 --- a/plugins/setoid_ring/newring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Newring -Newring_plugin_mod -G_newring diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack new file mode 100644 index 000000000..23663b409 --- /dev/null +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -0,0 +1,2 @@ +Newring +G_newring diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 67c9dd0a3..03b49e333 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "ascii_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + open Pp open Errors open Util diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib deleted file mode 100644 index b00f92506..000000000 --- a/plugins/syntax/ascii_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Ascii_syntax -Ascii_syntax_plugin_mod diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack new file mode 100644 index 000000000..7b9213a0e --- /dev/null +++ b/plugins/syntax/ascii_syntax_plugin.mlpack @@ -0,0 +1 @@ +Ascii_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index fe9386039..3142c8cf0 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "nat_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* This file defines the printer for natural numbers in [nat] *) (*i*) diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib deleted file mode 100644 index 69b0cb20f..000000000 --- a/plugins/syntax/nat_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Nat_syntax -Nat_syntax_plugin_mod diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack new file mode 100644 index 000000000..39bdd62f4 --- /dev/null +++ b/plugins/syntax/nat_syntax_plugin.mlpack @@ -0,0 +1 @@ +Nat_syntax diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index fe9f1319e..57cb2f897 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "numbers_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint @@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n = let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] - else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] + else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] in GApp (dloc, ref_constructor, args) diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib deleted file mode 100644 index ebc0bb202..000000000 --- a/plugins/syntax/numbers_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Numbers_syntax -Numbers_syntax_plugin_mod diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack new file mode 100644 index 000000000..e48c00a0d --- /dev/null +++ b/plugins/syntax/numbers_syntax_plugin.mlpack @@ -0,0 +1 @@ +Numbers_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 05d73f9ec..3ae2d45f3 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -10,6 +10,10 @@ open Util open Names open Globnames +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "r_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib deleted file mode 100644 index 5c173a140..000000000 --- a/plugins/syntax/r_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -R_syntax -R_syntax_plugin_mod diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack new file mode 100644 index 000000000..d4ee75ea4 --- /dev/null +++ b/plugins/syntax/r_syntax_plugin.mlpack @@ -0,0 +1 @@ +R_syntax diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 2e696f391..de0fa77ef 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -7,10 +7,14 @@ (***********************************************************************) open Globnames -open Ascii_syntax +open Ascii_syntax_plugin.Ascii_syntax open Glob_term open Coqlib +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "string_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_string (* make a string term from the string s *) diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib deleted file mode 100644 index b108c9e00..000000000 --- a/plugins/syntax/string_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -String_syntax -String_syntax_plugin_mod diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack new file mode 100644 index 000000000..45d6e0fa2 --- /dev/null +++ b/plugins/syntax/string_syntax_plugin.mlpack @@ -0,0 +1 @@ +String_syntax diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 53c1b5d7a..ce86c0a65 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -12,6 +12,10 @@ open Util open Names open Bigint +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "z_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib deleted file mode 100644 index 36d41acc2..000000000 --- a/plugins/syntax/z_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Z_syntax -Z_syntax_plugin_mod diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack new file mode 100644 index 000000000..411260c04 --- /dev/null +++ b/plugins/syntax/z_syntax_plugin.mlpack @@ -0,0 +1 @@ +Z_syntax diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 670ff487c..57fcd5dd2 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -33,10 +33,6 @@ rule mllib_list = parse open Printf open Unix -(** [coqdep_boot] is a stripped-down version of [coqdep] used to treat - with mllib files. -*) - (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while backslashes themselves must be escaped only if part of a sequence @@ -132,6 +128,7 @@ let add_ml_known, search_ml_known = mkknown () let add_mlpack_known, search_mlpack_known = mkknown () 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 @@ -148,18 +145,15 @@ let traite_fichier_modules md ext = let chan = open_in (md ^ ext) in let list = mllib_list (Lexing.from_channel chan) in List.fold_left - (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire^" "^file - | None -> + (fun acc str -> + match search_mlpack_known str with + | Some mldir -> (file_name str mldir) :: acc + | None -> match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire^" "^file - | None -> a_faire) "" list + | Some mldir -> (file_name str mldir) :: acc + | None -> acc) [] (List.rev list) with - | Sys_error _ -> "" + | Sys_error _ -> [] | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) let addQueue q v = q := v :: !q @@ -167,22 +161,43 @@ let addQueue q v = q := v :: !q let treat_file old_name = let name = Filename.basename old_name in let dirname = Some (Filename.dirname old_name) in - match get_extension name [".mllib"] with + match get_extension name [".mllib";".mlpack"] with | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> () let mllib_dependencies () = List.iter (fun (name,dirname) -> let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mllib" in + let deps = traite_fichier_modules fullname ".mllib" in + let sdeps = String.concat " " deps in let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; - printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname; + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname sdeps; + printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" + efullname efullname; + printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" + efullname efullname efullname; flush Pervasives.stdout) (List.rev !mllibAccu) +let mlpack_dependencies () = + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let modname = String.capitalize name in + let deps = traite_fichier_modules fullname ".mlpack" in + let sdeps = String.concat " " deps in + let efullname = escape fullname in + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps; + List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps; + printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" + efullname efullname; + printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" + efullname efullname efullname; + flush Pervasives.stdout) + (List.rev !mlpackAccu) + let rec parse = function | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) @@ -192,10 +207,11 @@ let rec parse = function | f :: ll -> treat_file f; parse ll | [] -> () -let coqdep_boot () = +let main () = if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - mllib_dependencies () + mllib_dependencies (); + mlpack_dependencies () -let _ = Printexc.catch coqdep_boot () +let _ = Printexc.catch main () } -- cgit v1.2.3