diff options
| author | Enrico Tassi | 2020-06-29 17:38:15 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-06-29 17:38:15 +0200 |
| commit | 397fb9dfbe09b85d8cbeed5854134a6491372ae4 (patch) | |
| tree | 1d685494e5a413ddabff32e6e4b40043fe434c19 | |
| parent | a039e78c821ba6a0da5d3364b98491707eab8add (diff) | |
[test-suite] async-proofs off in tests with Fail Timeout
Apparently the `Timeout` exception is raised by a signal handled, and
that can happen when the running thread is a worker manager, rather than
the main thread (the one that should be interrupted).
Given that the point of these tests is to test *auto and not the STM,
we disable async proofs forcibly.
| -rw-r--r-- | test-suite/success/Typeclasses.v | 1 | ||||
| -rw-r--r-- | test-suite/success/auto.v | 1 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 66305dfefa..563651cfa5 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) Module applydestruct. Class Foo (A : Type) := { bar : nat -> A; diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 62a66daf7d..98e2917300 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) (* Wish #2154 by E. van der Weegen *) (* auto was not using f_equal-style lemmas with metavariables occurring diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index cea7d92c0b..9577d63f61 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-async-proofs" "off") *) Require Import Program.Tactics. Module Backtracking. Class A := { foo : nat }. |