Set up CI minimization run for ci-metacoq #1910
Annotations
1 error and 10 warnings
|
Run minimizer
Universe inconsistency. Cannot enforce j < i because i < j.
|
|
Run minimizer
Using opam switch '4.09.0'
|
|
Run minimizer
which ocamlfind: '/root/.opamcache/4.09.0/bin/ocamlfind'
|
|
Run minimizer
ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.09.0
Standard library directory: /root/.opamcache/4.09.0/lib/ocaml
|
|
Run minimizer
download failing artifacts @ dc8315dd482007f5084bee93e95339388f69ff30 https://gitlab.inria.fr/coq/coq/-/jobs/4746792/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4746875/artifacts/download
|
|
Run minimizer
download passing artifacts @ 48db2360c32d779f948e110fdfbaae3d99c03fa3 https://gitlab.inria.fr/coq/coq/-/jobs/4740686/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4740769/artifacts/download
|
|
Run minimizer
/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/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQ_NATIVE_COMPILER_DEFAULT=yes
|
|
Run minimizer
/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/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQ_NATIVE_COMPILER_DEFAULT=yes
|
|
Run minimizer
Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --error-log=/github/workspace/build.log --temp-file-log=/github/workspace/cwd/tmp.log --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-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src --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 --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories MetaCoq.SafeChecker --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories MetaCoq.Erasure --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories MetaCoq.ErasurePlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MetaCoq.TestSuite --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-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /
|
|
Run minimizer
::warning::Failed to inline MetaCoq.Template.TemplateMonad.Common via Include, stripping Requires and preserve the error. The alternate coqc (/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig) was supposed to pass, but instead emitted an error.
The new error was:
File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 6, characters 8-21:
Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac.
[deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default]
File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 12, characters 7-20:
Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac.
[deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default]
File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 28, characters 0-28:
Warning: Library File Stdlib.Bool.Bvector is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
[deprecated-library-file-since-8.20,deprecated-since-8.20,deprecated-library-file,deprecated,default]
File "/tmp/tmpxoph8_a2/MetaCoq/TestSuite/univ.v", line 510, characters 0-96:
Error:
Anomaly
"Constant MetaCoq.Template.TemplateMonad.Common.my_projT2 does not appear in the environment."
Please report at http://coq.inria.fr/bugs/.
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" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-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" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src" "-top" "MetaCoq.TestSuite.univ") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 263 lines to 23 lines, then from 31 lines to 215 lines, then from 220 lines to 31 lines, then from 38 lines to 205 lines, then from 210 lines to 39 lines, then from 46 lines to 505 lines, then from 507 lines to 128 lines, then from 135 lines to 403 lines, then from 406 lines to 201 lines, then from 208 lines to 598 lines, then from 602 lines to 291 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.09.0
coqtop version runner-cabngxqim-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 46ba544a35489) (46ba544a3548941baad94eca61e125f289c5aa39)
Expected coqc runtime on this file: 1.610 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.
Require Ltac2.Init.
Require MetaCoq.Utils.MCEquality.
Require MetaCoq
|
|
Run minimizer
::warning::Failed to inline MetaCoq.Template.TemplateMonad.Common via Include, with Requires and preserve the error. The alternate coqc (/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig) was supposed to pass, but instead emitted an error.
The new error was:
File "/tmp/tmp5xu6vr4x/MetaCoq/TestSuite/univ.v", line 7, characters 8-21:
Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac.
[deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default]
File "/tmp/tmp5xu6vr4x/MetaCoq/TestSuite/univ.v", line 13, characters 7-20:
Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac.
[deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default]
File "/tmp/tmp5xu6vr4x/MetaCoq/TestSuite/univ.v", line 19, 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/tmp5xu6vr4x/MetaCoq/TestSuite/univ.v", line 20, characters 0-36:
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/tmp5xu6vr4x/MetaCoq/TestSuite/univ.v", line 377, characters 0-96:
Error:
Anomaly
"Constant MetaCoq.Template.TemplateMonad.Common.my_projT2 does not appear in the environment."
Please report at http://coq.inria.fr/bugs/.
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" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-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" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src" "-top" "MetaCoq.TestSuite.univ") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 263 lines to 23 lines, then from 31 lines to 215 lines, then from 220 lines to 31 lines, then from 38 lines to 205 lines, then from 210 lines to 39 lines, then from 46 lines to 505 lines, then from 507 lines to 128 lines, then from 135 lines to 403 lines, then from 406 lines to 201 lines, then from 208 lines to 598 lines, then from 602 lines to 291 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.09.0
coqtop version runner-cabngxqim-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 46ba544a35489) (46ba544a3548941baad94eca61e125f289c5aa39)
Expected coqc runtime on this file: 1.610 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.
Module MetaCo
|
Loading