Makefile.build : cleanup now that micromega.ml isn't generated + sync check of this file

 There is now a warning if the content of micromega.ml isn't what MExtraction.v would
 produce.

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.