Skip to content
CI

Set up CI minimization run for ci-analysis #1592

Sign in to view logs

Set up CI minimization run for ci-analysis

Set up CI minimization run for ci-analysis #1592

Triggered via push November 15, 2023 23:08
@coqbotcoqbot
pushed 260c14f
run-coq-bug-minimizer-61440685032
Status Failure
Total duration 5h 40m 28s
Artifacts 7

main.yml

on: push
build
5h 40m
build
Fit to window
Zoom out
Zoom in

Annotations

1 error and 8 warnings
build
No applicable tactic.
build
Using opam switch '4.14.1+flambda'
build
which ocamlfind: '/root/.opamcache/4.14.1+flambda/bin/ocamlfind'
build
ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.14.1 Standard library directory: /root/.opamcache/4.14.1+flambda/lib/ocaml
build
download failing artifacts @ df45fd0bea8b9b8ec8e48dd5d8716094c57e9ad9 https://gitlab.inria.fr/coq/coq/-/jobs/3600455/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3600507/artifacts/download
build
download passing artifacts @ 56a7f9c955047588cff110e5441999f6cd5e0582 https://gitlab.inria.fr/coq/coq/-/jobs/3599446/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3599498/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.14.1+flambda/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.14.1+flambda/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/analysis/theories/trigo.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=-parsing --nonpassing-arg=-w --nonpassing-arg=+undeclared-scope --nonpassing-arg=-w --nonpassing-arg=+non-primitive-record --nonpassing-arg=-w --nonpassing-arg=-ambiguous-paths --nonpassing-arg=-w --nonpassing-arg=-redundant-canonical-projection --nonpassing-arg=-w --nonpassing-arg=-projection-no-head-constant --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=ondemand --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/analysis/classical mathcomp.classical --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/analysis/theories mathcomp.analysis --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=-parsing --passing-arg=-w --passing-arg=+undeclared-scope --passing-arg=-w --passing-arg=+non-primitive-record --passing-arg=-w --passing-arg=-ambiguous-paths --passing-arg=-w --passing-arg=-redundant-canonical-projection --passing-arg=-w --passing-arg=-projection-no-head-constant --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=ondemand --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/analysis/classical mathcomp.classical --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/analysis/theories mathcomp.analysis -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

Artifacts

Produced during runtime
Name Size
artifact Expired
3.34 GB
bug.log Expired
334 KB
bug.v Expired
181 KB
bug.verbose.log Expired
609 MB
build.log Expired
4.07 MB
metadata Expired
770 Bytes
tmp.v Expired
0 Bytes