Skip to content
CI

Set up CI minimization run for ci-deriving #1896

Sign in to view logs

Set up CI minimization run for ci-deriving

Set up CI minimization run for ci-deriving #1896

Triggered via push September 16, 2024 22:38
@coqbotcoqbot
pushed 08c7e12
run-coq-bug-minimizer-364509732672
Status Success
Total duration 2h 49m 15s
Artifacts 8

main.yml

on: push
build
2h 49m
build
Fit to window
Zoom out
Zoom in

Annotations

8 warnings
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 @ dc8315dd482007f5084bee93e95339388f69ff30 https://gitlab.inria.fr/coq/coq/-/jobs/4746794/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4746892/artifacts/download
build
download passing artifacts @ 48db2360c32d779f948e110fdfbaae3d99c03fa3 https://gitlab.inria.fr/coq/coq/-/jobs/4740688/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4740786/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/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.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/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/deriving/theories/ind.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=-notation-overridden --nonpassing-arg=-w --nonpassing-arg=-non-reversible-notation --nonpassing-arg=-w --nonpassing-arg=-ssr-search-moved --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-Q /github/workspace/builds/coq/coq-failing/_build_ci/deriving/theories deriving --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=-notation-overridden --passing-arg=-w --passing-arg=-non-reversible-notation --passing-arg=-w --passing-arg=-ssr-search-moved --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-Q /github/workspace/builds/coq/coq-passing/_build_ci/deriving/theories deriving -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

Artifacts

Produced during runtime
Name Size
artifact
3.4 GB
bug.log
7.84 KB
bug.v
1.66 KB
bug.verbose.log
226 MB
build.log
357 KB
metadata
300 Bytes
tmp.log
130 Bytes
tmp.v
126 Bytes