From d61f17be123b1d7f2aaba3291ad4c51c78e63df5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 10:55:44 +0100
Subject: Make it possible to pass flags to coq when running test suite

---
 test-suite/Makefile | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 34a1900bbc..37091a49e5 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,9 +36,10 @@ include ../Makefile.common
 # easily overridden
 LIB := ..
 BIN := $(shell cd ..; pwd)/bin/
+COQFLAGS?=
 
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
-coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS)
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
 coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 coqdoc := $(BIN)coqdoc
 coqtopbyte := $(BIN)coqtop.byte
-- 
cgit v1.2.3


From 48ae6cec009554a337f64b0402daea2c653e25e2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 10:56:09 +0100
Subject: Add a CI job running test suite with `-async-proofs on`

---
 .gitlab-ci.yml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f54f64bf28..c11ba11fc5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -151,7 +151,7 @@ after_script:
     - BIN=$(readlink -f ../_install_ci/bin)/
     - LIB=$(readlink -f ../_install_ci/lib/coq)/
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
+    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
@@ -427,6 +427,13 @@ test-suite:edge+trunk+dune:
     expire_in: 1 week
   allow_failure: true
 
+test-suite:base+async:
+  <<: *test-suite-template
+  dependencies:
+    - build:base
+  variables:
+    COQFLAGS: "-async-proofs on"
+
 validate:base:
   <<: *validate-template
   dependencies:
-- 
cgit v1.2.3


From 62ece342f56380e54ecfe2b403159e9b115a8406 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Dec 2018 15:11:17 +0100
Subject: Test ltacprof in sequential mode

Scripting these commands in async mode does not really make sense.
---
 test-suite/output-modulo-time/ltacprof_cutoff.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index ae5d51bae8..b7c98aa134 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
 Require Coq.ZArith.BinInt.
 Module WithIdTac.
   Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
-- 
cgit v1.2.3


From 36500daa3efb746d3b19f288741c46b09b6d2632 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Dec 2018 15:11:52 +0100
Subject: Make some tests more robust by adding missing proof terminators

---
 test-suite/bugs/opened/bug_3166.v | 1 +
 test-suite/bugs/opened/bug_3754.v | 1 +
 test-suite/bugs/opened/bug_3938.v | 1 +
 3 files changed, 3 insertions(+)

diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v
index e1c29a954c..baf87631f0 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/opened/bug_3166.v
@@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
   Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+Abort.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v
index a717bbe735..18820b1a4c 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/opened/bug_3754.v
@@ -282,3 +282,4 @@ Defined.
       rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
       Set Debug Tactic Unification.
       Fail rewrite (concat_Ap ff2).
+    Abort.
diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v
index 2d0d1930f1..3c7c945ed8 100644
--- a/test-suite/bugs/opened/bug_3938.v
+++ b/test-suite/bugs/opened/bug_3938.v
@@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
   intros a b f H.
   rewrite H. (* Toplevel input, characters 15-25:
 Anomaly: Evar ?X11 was not declared. Please report. *)
+Abort.
-- 
cgit v1.2.3