aboutsummaryrefslogtreecommitdiff
path: root/plugins/quote/quote_plugin.mlpack
AgeCommit message (Collapse)Author
2018-09-12Remove quote pluginMaxime Dénès
As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore.
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
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.