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/firstorder/g_ground.ml4 | 2 ++ plugins/firstorder/ground_plugin.mllib | 8 -------- plugins/firstorder/ground_plugin.mlpack | 7 +++++++ 3 files changed, 9 insertions(+), 8 deletions(-) delete mode 100644 plugins/firstorder/ground_plugin.mllib create mode 100644 plugins/firstorder/ground_plugin.mlpack (limited to 'plugins/firstorder') 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 -- cgit v1.2.3