From 797736bbd7975926cc028a9f7c9c577e9c1e476b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 11:02:02 +0100
Subject: 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.
---
 test-suite/Makefile             |  7 +++++++
 test-suite/output/MExtraction.v | 12 ++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 test-suite/output/MExtraction.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6865dcc768..ff5e3a317b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -312,6 +312,13 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	  rm $$tmpoutput; \
 	} > "$@"
 
+# the expected output for the MExtraction test is
+# /plugins/micromega/micromega.ml except with additional newline
+output/MExtraction.out: ../plugins/micromega/micromega.ml
+	$(SHOW) GEN $@
+	$(HIDE) cp $< $@
+	$(HIDE) echo >> $@
+
 $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
new file mode 100644
index 0000000000..352e422cf7
--- /dev/null
+++ b/test-suite/output/MExtraction.v
@@ -0,0 +1,12 @@
+Require Import micromega.MExtraction.
+Require Import RingMicromega.
+Require Import QArith.
+Require Import VarMap.
+Require Import ZMicromega.
+Require Import QMicromega.
+Require Import RMicromega.
+
+Recursive Extraction
+  List.map RingMicromega.simpl_cone (*map_cone  indexes*)
+  denorm Qpower vm_add
+  n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-- 
cgit v1.2.3