diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | Makefile.build | 43 | ||||
| -rw-r--r-- | plugins/micromega/MExtraction.v | 5 |
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 @@ -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. |