Skip to content
CI

Set up CI minimization run for ci-metacoq #1591

Sign in to view logs

Set up CI minimization run for ci-metacoq

Set up CI minimization run for ci-metacoq #1591

Triggered via push November 14, 2023 07:11
@coqbotcoqbot
pushed ae8a409
run-coq-bug-minimizer-391899341207
Status Success
Total duration 3h 11m 49s
Artifacts 7

main.yml

on: push
build
3h 11m
build
Fit to window
Zoom out
Zoom in

Annotations

1 error and 8 warnings
build
[Focus] Wrong bullet -: No more goals.
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 @ a6df8f61caaa26b1df354402e503a4f5ebe56ffa https://gitlab.inria.fr/coq/coq/-/jobs/3591790/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3592598/artifacts/download
build
download passing artifacts @ b10573deb4f3e0aecf74692af95f84127576c8d9 https://gitlab.inria.fr/coq/coq/-/jobs/3591527/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3591611/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/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories/PCUICReduction.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --error-log=/github/workspace/build.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-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

Artifacts

Produced during runtime
Name Size
artifact Expired
2.61 GB
bug.log Expired
162 KB
bug.v Expired
2.1 KB
bug.verbose.log Expired
427 MB
build.log Expired
3.84 MB
metadata Expired
231 Bytes
tmp.v Expired
0 Bytes