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. --- Makefile | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index aeb54fba8..93b89a489 100644 --- a/Makefile +++ b/Makefile @@ -66,7 +66,7 @@ endef ## Files in the source tree LEXFILES := $(call find, '*.mll') -export MLLIBFILES := $(call find, '*.mllib') +export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') @@ -80,9 +80,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(GENPLUGINSMOD) \ - tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) -- cgit v1.2.3