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/funind/recdef.ml | 2 +- plugins/funind/recdef_plugin.mllib | 11 ----------- plugins/funind/recdef_plugin.mlpack | 10 ++++++++++ 3 files changed, 11 insertions(+), 12 deletions(-) delete mode 100644 plugins/funind/recdef_plugin.mllib create mode 100644 plugins/funind/recdef_plugin.mlpack (limited to 'plugins/funind') 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 -- cgit v1.2.3