aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.gitignore1
-rw-r--r--Makefile1
-rw-r--r--Makefile.build43
-rw-r--r--plugins/micromega/MExtraction.v5
4 files changed, 26 insertions, 24 deletions
diff --git a/.gitignore b/.gitignore
index db12a9de2..58e1d346c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,6 +52,7 @@ config/Info-*.plist
dev/ocamldebug-coq
dev/camlp4.dbg
plugins/micromega/csdpcert
+plugins/micromega/.micromega.ml.generated
kernel/byterun/dllcoqrun.so
coqdoc.sty
.csdp.cache
diff --git a/Makefile b/Makefile
index 66721a3ad..a6a73d249 100644
--- a/Makefile
+++ b/Makefile
@@ -190,6 +190,7 @@ indepclean:
rm -f test-suite/check.log
rm -f glob.dump
rm -f config/revision.ml revision
+ rm -f plugins/micromega/.micromega.ml.generated
$(MAKE) -C test-suite clean
docclean:
diff --git a/Makefile.build b/Makefile.build
index 99541243a..484673e17 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -78,27 +78,6 @@ include Makefile.install
include Makefile.dev ## provides the 'printers' and 'revision' rules
###########################################################################
-# Adding missing pieces of information not discovered by ocamldep
-# due to the fact that:
-# - plugins/micromega/micromega_plugin.ml
-# - plugins/micromega/micromega_plugin.mli
-# are generated (and not yet present when we run "ocamldep").
-###########################################################################
-
-plugins/micromega/micromega_plugin.cmo : plugins/micromega/micromega.cmo
-plugins/micromega/micromega_plugin.cmx : plugins/micromega/micromega.cmx
-
-plugins/micromega/certificate.cmo plugins/micromega/coq_micromega.cmo plugins/micromega/csdpcert.cmo plugins/micromega/mfourier.cmo plugins/micromega/mutils.cmo plugins/micromega/polynomial.cmo : plugins/micromega/micromega.cmo
-
-plugins/micromega/certificate.cmx plugins/micromega/coq_micromega.cmx plugins/micromega/csdpcert.cmx plugins/micromega/mfourier.cmx plugins/micromega/mutils.cmx plugins/micromega/polynomial.cmx : plugins/micromega/micromega.cmx
-
-plugins/micromega/micromega.cmx plugins/micromega/micromega.cmo : plugins/micromega/micromega.cmi
-plugins/micromega/micromega.cmi : plugins/micromega/micromega.mli
-
-plugins/micromega/generated_micromega.mli plugins/micromega/generated_micromega.ml : plugins/micromega/MExtraction.vo
- @:
-
-###########################################################################
# This include below will lauch the build of all .d.
# The - at front is for disabling warnings about currently missing ones.
@@ -110,8 +89,6 @@ DEPENDENCIES := \
-include $(DEPENDENCIES)
-plugins/micromega/micromega_FORPACK:= -for-pack Micromega_plugin
-
# All dependency includes must be declared secondary, otherwise make will
# delete them if it decided to build them by dependency instead of because
# of include, and they will then be automatically deleted, leading to an
@@ -617,6 +594,26 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
$(HIDE)rm -f theories/Init/$*.glob
$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
+# MExtraction.v generates the ml core file of the micromega tactic.
+# We check that this generated code is still in sync with the version
+# of micromega.ml in the archive.
+
+# Note: we now dump to stdout there via "Recursive Extraction" for better
+# control on the name of the generated file, and avoid a .ml that
+# would end in our $(MLFILES). The "sed" below is to kill the final
+# blank line printed by Recursive Extraction (unlike Extraction "foo").
+
+MICROMEGAV:=plugins/micromega/MExtraction.v
+MICROMEGAML:=plugins/micromega/micromega.ml
+MICROMEGAGEN:=plugins/micromega/.micromega.ml.generated
+
+$(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelude.vo $(VO_TOOLS_DEP)
+ $(SHOW)'COQC $<'
+ $(HIDE)rm -f $*.glob
+ $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN)
+ $(HIDE)cmp -s $(MICROMEGAML) $(MICROMEGAGEN) || \
+ echo "Warning: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !"
+
# The general rule for building .vo files :
%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 2451aeada..135a71520 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -48,7 +48,10 @@ Extract Constant Rmult => "( * )".
Extract Constant Ropp => "fun x -> - x".
Extract Constant Rinv => "fun x -> 1 / x".
-Extraction "plugins/micromega/generated_micromega.ml"
+(** We now extract to stdout, see comment in Makefile.build *)
+
+(*Extraction "plugins/micromega/micromega.ml" *)
+Recursive Extraction
List.map simpl_cone (*map_cone indexes*)
denorm Qpower vm_add
n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.