Merge PR #9088: Add CI job running test suite with `async-proofs on`

6 files changed, 15 insertions, 4 deletions

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:
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
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.
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).