Set up CI minimization resumption run for ci-metacoq #1608
coqbot
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
Annotations
1 error and 10 warnings
|
build
(in proof inversion_Rel): Attempt to save an incomplete proof
|
|
build
Using opam switch '4.09.0'
|
|
build
which ocamlfind: '/root/.opamcache/4.09.0/bin/ocamlfind'
|
|
build
ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.09.0
Standard library directory: /root/.opamcache/4.09.0/lib/ocaml
|
|
build
download failing artifacts @ b4f4318750a45958de37a1e7bd7aa0c83a2ed42d https://gitlab.inria.fr/coq/coq/-/jobs/3683657/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3683741/artifacts/download
|
|
build
download passing artifacts @ a38dada98c4de252b85be886f5a67a141992c582 https://gitlab.inria.fr/coq/coq/-/jobs/3683066/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3683150/artifacts/download
|
|
build
/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc -config: COQLIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/
COQCORELIB=/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/../coq-core/
DOCDIR=/builds/coq/coq/_install_ci/share/doc/
OCAMLFIND=/root/.opamcache/4.09.0/bin/ocamlfind
CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
WARN=-warn-error +a-3
HASNATDYNLINK=true
COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQ_NATIVE_COMPILER_DEFAULT=yes
|
|
build
/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc -config: COQLIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/
COQCORELIB=/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../coq-core/
DOCDIR=/builds/coq/coq/_install_ci/share/doc/
OCAMLFIND=/root/.opamcache/4.09.0/bin/ocamlfind
CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
WARN=-warn-error +a-3
HASNATDYNLINK=true
COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQ_NATIVE_COMPILER_DEFAULT=yes
|
|
build
Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/cwd/bug_01.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --no-deps --ignore-coq-prog-args --inline-user-contrib --coqc=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --coqtop=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqtop.orig --coq_makefile=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coq_makefile --coqdep /github/workspace/builds/coq/coq-passing/_install_ci/bin/coqdep --base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/ -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline
--nonpassing-arg=-q --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=no --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories MetaCoq.Utils --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories MetaCoq.Common --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --passing-coqc=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig --passing-coqtop=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqtop.orig --passing-base-dir=/github/workspace/builds/coq/coq-passing/_build_ci/ --passing-arg=-q --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=no --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/utils/theories MetaCoq.Utils --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/common/theories MetaCoq.Common --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log
|
|
build
::warning::Failed to inline Equations.Prop.Equations via Include, stripping Requires and preserve the error.
The new error was:
File "/tmp/tmpuv91cgnp/Top/bug_01.v", line 116, characters 7-31:
Error: Cannot find module Equations.Prop.Equations
The file generating the error was:
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 406 lines to 79 lines, then from 92 lines to 4252 lines, then from 4249 lines to 89 lines, then from 102 lines to 901 lines, then from 906 lines to 127 lines, then from 140 lines to 1768 lines, then from 1773 lines to 2117 lines, then from 2107 lines to 389 lines, then from 402 lines to 1300 lines, then from 1304 lines to 550 lines, then from 563 lines to 2362 lines, then from 2361 lines to 555 lines, then from 568 lines to 1055 lines, then from 1060 lines to 562 lines, then from 575 lines to 2873 lines, then from 2875 lines to 659 lines, then from 672 lines to 2567 lines, then from 2571 lines to 2380 lines, then from 2352 lines to 834 lines, then from 847 lines to 1437 lines, then from 1440 lines to 958 lines, then from 971 lines to 2213 lines, then from 2212 lines to 973 lines, then from 986 lines to 1399 lines, then from 1404 lines to 976 lines, then from 989 lines to 2449 lines, then from 2450 lines to 1233 lines, then from 1246 lines to 1504 lines, then from 1509 lines to 1251 lines, then from 1268 lines to 1242 lines, then from 1255 lines to 3288 lines, then from 3289 lines to 1428 lines, then from 1441 lines to 2827 lines, then from 2828 lines to 1575 lines, then from 1579 lines to 1561 lines, then from 1574 lines to 1665 lines, then from 1670 lines to 1563 lines, then from 1576 lines to 2146 lines, then from 2148 lines to 1568 lines, then from 1581 lines to 4426 lines, then from 4402 lines to 2092 lines, then from 2082 lines to 1899 lines, then from 1912 lines to 2790 lines, then from 2792 lines to 1979 lines, then from 1992 lines to 2585 lines, then from 2590 lines to 2047 lines, then from 2060 lines to 2192 lines, then from 2197 lines to 2061 lines, then from 2074 lines to 2386 lines, then from 2389 lines to 2340 lines, then from 2346 lines to 2080 lines, then from 2093 lines to 6088 lines, then from 6083 lines to 2114 lines, then from 2127 lines to 2424 lines, then from 2426 lines to 2123 lines, then from 2136 lines to 3670 lines, then from 3668 lines to 3051 lines, then from 3058 lines to 2143 lines, then from 2156 lines to 2332 lines, then from 2337 lines to 2154 lines, then from 2167 lines to 2395 lines, then from 2397 lines to 2155 lines, then from 2168 lines to 2315 lines, then from 2319 lines to 2161 lines, then from 2174 lines to 2729 lines, then from 2734 lines to 2214 lines, then from 2227 lines to 2395 lines, then from 2400 lines to 2216 lines, then from 2229 lines to 2511 lines, then from 2515 lines to 2425 lines, then from 2428 lines to 2288 lines, then from 2301 lines to 2555 lines, then from 2557 lines to 2307 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.09.0
coqtop version c74786003383:/builds/coq/coq/_build/default,(HEAD detached at f7aaed9) (f7aaed98877033e8fd8c34e63e9c7269aff2f1c7)
Expected coqc runtime on this file: 1.791 sec *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Re
|
|
build
::warning::Failed to inline Equations.Prop.Equations via Include, with Requires and preserve the error.
The new error was:
File "/tmp/tmpfn_k2bk1/Top/bug_01.v", line 28, characters 0-37:
Warning: Use of “Require” inside a module is fragile. It is not recommended
to use this functionality in finished proof scripts.
[require-in-module,fragile,default]
File "/tmp/tmpfn_k2bk1/Top/bug_01.v", line 29, characters 0-41:
Warning: Use of “Require” inside a module is fragile. It is not recommended
to use this functionality in finished proof scripts.
[require-in-module,fragile,default]
File "/tmp/tmpfn_k2bk1/Top/bug_01.v", line 33, characters 0-35:
Warning: Use of “Require” inside a module is fragile. It is not recommended
to use this functionality in finished proof scripts.
[require-in-module,fragile,default]
File "/tmp/tmpfn_k2bk1/Top/bug_01.v", line 90, characters 7-31:
Error: Cannot find module Equations.Prop.Equations
The file generating the error was:
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 406 lines to 79 lines, then from 92 lines to 4252 lines, then from 4249 lines to 89 lines, then from 102 lines to 901 lines, then from 906 lines to 127 lines, then from 140 lines to 1768 lines, then from 1773 lines to 2117 lines, then from 2107 lines to 389 lines, then from 402 lines to 1300 lines, then from 1304 lines to 550 lines, then from 563 lines to 2362 lines, then from 2361 lines to 555 lines, then from 568 lines to 1055 lines, then from 1060 lines to 562 lines, then from 575 lines to 2873 lines, then from 2875 lines to 659 lines, then from 672 lines to 2567 lines, then from 2571 lines to 2380 lines, then from 2352 lines to 834 lines, then from 847 lines to 1437 lines, then from 1440 lines to 958 lines, then from 971 lines to 2213 lines, then from 2212 lines to 973 lines, then from 986 lines to 1399 lines, then from 1404 lines to 976 lines, then from 989 lines to 2449 lines, then from 2450 lines to 1233 lines, then from 1246 lines to 1504 lines, then from 1509 lines to 1251 lines, then from 1268 lines to 1242 lines, then from 1255 lines to 3288 lines, then from 3289 lines to 1428 lines, then from 1441 lines to 2827 lines, then from 2828 lines to 1575 lines, then from 1579 lines to 1561 lines, then from 1574 lines to 1665 lines, then from 1670 lines to 1563 lines, then from 1576 lines to 2146 lines, then from 2148 lines to 1568 lines, then from 1581 lines to 4426 lines, then from 4402 lines to 2092 lines, then from 2082 lines to 1899 lines, then from 1912 lines to 2790 lines, then from 2792 lines to 1979 lines, then from 1992 lines to 2585 lines, then from 2590 lines to 2047 lines, then from 2060 lines to 2192 lines, then from 2197 lines to 2061 lines, then from 2074 lines to 2386 lines, then from 2389 lines to 2340 lines, then from 2346 lines to 2080 lines, then from 2093 lines to 6088 lines, then from 6083 lines to 2114 lines, then from 2127 lines to 2424 lines, then from 2426 lines to 2123 lines, then from 2136 lines to 3670 lines, then from 3668 lines to 3051 lines, then from 3058 lines to 2143 lines, then from 2156 lines to 2332 lines, then from 2337 lines to 2154 lines, then from 2167 lines to 2395 lines, then from 2397 lines to 2155 lines, then from 2168 lines to 2315 lines, then from 2319 lines to 2161 lines, then from 2174 lines to 2729 lines, then from 2734 lines to 2214 lines, then from 2227 lines to 2395 lines, then from 2400 lines to
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
artifact
Expired
|
3.49 GB |
|
|
bug.log
Expired
|
163 KB |
|
|
bug.v
Expired
|
21.7 KB |
|
|
bug.verbose.log
Expired
|
989 MB |
|
|
build.log
Expired
|
284 KB |
|
|
metadata
Expired
|
561 Bytes |
|
|
tmp.v
Expired
|
24.6 KB |
|