diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 12:03:35 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-08 14:41:55 +0200 |
| commit | 509c30c93dca8ca8c78f1da1eefc056226d90346 (patch) | |
| tree | 9cc58803b234a38efd0cda5ca70b5105e08dd8d6 | |
| parent | d060577f274658dd8189fceb92316b3cd37417b9 (diff) | |
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.
47 files changed, 141 insertions, 102 deletions
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 @@ -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.mlpack index 319a9c302..2410f906a 100644 --- a/plugins/btauto/btauto_plugin.mllib +++ b/plugins/btauto/btauto_plugin.mlpack @@ -1,3 +1,2 @@ Refl_btauto G_btauto -Btauto_plugin_mod diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack index 1bcfc5378..27e903fd3 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mlpack @@ -2,4 +2,3 @@ Ccalgo Ccproof Cctac G_congruence -Cc_plugin_mod diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack index 39342dbd1..1b84a0790 100644 --- a/plugins/decl_mode/decl_mode_plugin.mllib +++ b/plugins/decl_mode/decl_mode_plugin.mlpack @@ -3,4 +3,3 @@ Decl_interp Decl_proof_instr Ppdecl_proof G_decl_mode -Decl_mode_plugin_mod 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.mlpack index 5ee0fc6da..5ee0fc6da 100644 --- a/plugins/derive/derive_plugin.mllib +++ b/plugins/derive/derive_plugin.mlpack 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.mlpack index ad3212434..9184f6501 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mlpack @@ -9,4 +9,3 @@ Scheme Json Extract_env G_extraction -Extraction_plugin_mod 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.mlpack index 447a1fb51..65fb2e9a1 100644 --- a/plugins/firstorder/ground_plugin.mllib +++ b/plugins/firstorder/ground_plugin.mlpack @@ -5,4 +5,3 @@ Rules Instances Ground G_ground -Ground_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack index 0383b1a80..b6262f8ae 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mlpack @@ -1,4 +1,3 @@ Fourier FourierR G_fourier -Fourier_plugin_mod 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.mlpack index ec1f5436c..2b443f2a1 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mlpack @@ -8,4 +8,3 @@ Invfun Indfun Merge G_indfun -Recdef_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack index f53a9e379..ed253da3f 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mlpack @@ -7,4 +7,3 @@ Certificate Persistent_cache Coq_micromega G_micromega -Micromega_plugin_mod diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack index e991fb76f..b55adf43c 100644 --- a/plugins/nsatz/nsatz_plugin.mllib +++ b/plugins/nsatz/nsatz_plugin.mlpack @@ -3,4 +3,3 @@ Polynom Ideal Nsatz G_nsatz -Nsatz_plugin_mod diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mlpack index 2b387fdce..df7f1047f 100644 --- a/plugins/omega/omega_plugin.mllib +++ b/plugins/omega/omega_plugin.mlpack @@ -1,4 +1,3 @@ Omega Coq_omega G_omega -Omega_plugin_mod 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.mlpack index 1625009d0..38d0e9411 100644 --- a/plugins/romega/romega_plugin.mllib +++ b/plugins/romega/romega_plugin.mlpack @@ -1,4 +1,3 @@ Const_omega Refl_omega G_romega -Romega_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mlpack index 0e3460449..61c5e945b 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -1,4 +1,3 @@ Proof_search Refl_tauto G_rtauto -Rtauto_plugin_mod 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 () } |