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. --- 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 + 18 files changed, 32 insertions(+), 14 deletions(-) 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 (limited to 'plugins/syntax') 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 -- cgit v1.2.3