diff options
| author | Gaëtan Gilbert | 2019-03-11 13:25:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-11 13:25:39 +0100 |
| commit | 74534f84a782f5de740c52cb97b3ca3a02eb6aa2 (patch) | |
| tree | 687ef46d8bff6daa1e9106f150e141175a2f9732 | |
| parent | f72e9df57b6bf600037282dbb257613199cd5b78 (diff) | |
| parent | 6188c34dd35b9d0f3a8fef6ec2c87a93614cfad8 (diff) | |
Merge PR #9698: Remove last random failures
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.v | 28 |
2 files changed, 2 insertions, 28 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c5038d3bb0..6448095dd8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -252,12 +252,14 @@ build:base+async: variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" + allow_failure: true # See https://github.com/coq/coq/issues/9658 build:quick: <<: *build-template variables: COQ_EXTRA_CONF: "-native-compiler no" QUICK: "1" + allow_failure: true # See https://github.com/coq/coq/issues/9637 windows64: <<: *windows-template diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v deleted file mode 100644 index b7c98aa134..0000000000 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ /dev/null @@ -1,28 +0,0 @@ -(* -*- 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). - - Ltac foo0 := idtac; sleep. - Ltac foo1 := sleep; foo0. - Ltac foo2 := sleep; foo1. - Goal True. - foo2. - Show Ltac Profile CutOff 47. - constructor. - Qed. -End WithIdTac. - -Module TestEval. - Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac. - - Ltac foo0 := idtac; do 50 (idtac; sleep). - Ltac foo1 := sleep; foo0. - Ltac foo2 := sleep; foo1. - Goal True. - Reset Ltac Profile. - foo2. - Show Ltac Profile CutOff 47. - constructor. - Qed. -End TestEval. |