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.

1 files changed, 20 insertions, 23 deletions

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)