diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 11:02:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-28 12:31:04 +0100 |
| commit | 797736bbd7975926cc028a9f7c9c577e9c1e476b (patch) | |
| tree | 551f4a6b277b0cb976b53032748ffec44d35c509 /Makefile.build | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Make the micromega extraction check a regular output test.
This allows us to enforce that it works without breaking the build
when it doesn't.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/Makefile.build b/Makefile.build index 39b793d2b..e518b7e22 100644 --- a/Makefile.build +++ b/Makefile.build @@ -717,26 +717,6 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) -# 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)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ - (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) - # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) |