Set up CI minimization run for ci-metacoq #1902
coqbotAnnotations
2 errors and 9 warnings
|
build
Process completed with exit code 1.
|
|
build
Universe inconsistency. Cannot enforce j < i because i < j.
|
|
build
No files were found with the provided path: bug.v. No artifacts will be uploaded.
|
|
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 @ dc8315dd482007f5084bee93e95339388f69ff30 https://gitlab.inria.fr/coq/coq/-/jobs/4746792/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4746875/artifacts/download
|
|
build
download passing artifacts @ 48db2360c32d779f948e110fdfbaae3d99c03fa3 https://gitlab.inria.fr/coq/coq/-/jobs/4740686/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4740769/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/ltac2_ltac1 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/ltac2_ltac1 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/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 /
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
artifact
|
2.73 GB |
|
|
bug.log
|
1.36 KB |
|
|
bug.verbose.log
|
10.7 KB |
|
|
build.log
|
329 KB |
|
|
metadata
|
305 Bytes |
|
|
tmp.log
|
388 Bytes |
|
|
tmp.v
|
2.75 KB |
|