aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extraction_plugin.mlpack
Commit message (Collapse)AuthorAge
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
| | | | | | | | | | | | | | | | | | | | Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512.
* Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
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.