Skip to content

Set up CI minimization resumption run for ci-mathcomp #1923

Set up CI minimization resumption run for ci-mathcomp

Set up CI minimization resumption run for ci-mathcomp #1923

Triggered via push September 20, 2024 09:36
Status Cancelled
Total duration 32m 15s
Artifacts 4

main.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

4 errors and 12 warnings
build
The run was canceled by @SkySkimmer.
build
The LHS of scalerAr
build
The operation was canceled.
build
Process completed with exit code 1.
build
Runner GitHub Actions 3 did not respond to a cancelation request with 00:05:00.
build
No files were found with the provided path: tmp.log. No artifacts will be uploaded.
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 @ 3b9bd6745971505391ac994e9a57f7d1686716fb https://gitlab.inria.fr/coq/coq/-/jobs/4753187/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4753260/artifacts/download
build
download passing artifacts @ 2d2e5a5c1468ac55b5a31cd7abc23a981fccd610 https://gitlab.inria.fr/coq/coq/-/jobs/4749631/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/4749704/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/cwd/bug_01.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --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=-projection-no-head-constant --nonpassing-arg=-w --nonpassing-arg=-redundant-canonical-projection --nonpassing-arg=-w --nonpassing-arg=-notation-overridden --nonpassing-arg=-w --nonpassing-arg=+duplicate-clear --nonpassing-arg=-w --nonpassing-arg=-ambiguous-paths --nonpassing-arg=-w --nonpassing-arg=+non-primitive-record --nonpassing-arg=-w --nonpassing-arg=+undeclared-scope --nonpassing-arg=-w --nonpassing-arg=+deprecated-hint-without-locality --nonpassing-arg=-w --nonpassing-arg=+deprecated-hint-rewrite-without-locality --nonpassing-arg=-w --nonpassing-arg=-elpi.add-const-for-axiom-or-sectionvar --nonpassing-arg=-w --nonpassing-arg=-opaque-let --nonpassing-arg=-w --nonpassing-arg=-argument-scope-delimiter --nonpassing-arg=-w --nonpassing-arg=-overwriting-delimiting-key --nonpassing-arg=-w --nonpassing-arg=-closed-notation-not-level-0 --nonpassing-arg=-w --nonpassing-arg=-postfix-notation-not-level-1 --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=ondemand --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/mathcomp/mathcomp --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/mathcomp/mathcomp mathcomp --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=-projection-no-head-constant --passing-arg=-w --passing-arg=-redundant-canonical-projection --passing-arg=-w --passing-arg=-notation-overridden --passing-arg=-w --passing-arg=+duplicate-clear --passing-arg=-w --passing-arg=-ambiguous-paths --passing-arg=-w --passing-arg=+non-primitive-record --passing-arg=-w --passing-arg=+undeclared-scope --passing-arg=-w --passing-arg=+deprecated-hint-without-locality --passing-arg=-w --passing-arg=+deprecated-hint-rewrite-without-locality --passing-arg=-w --passing-arg=-elpi.add-const-for-axiom-or-sectionvar --passing-arg=-w --passing-arg=-opaque-let --passing-arg=-w --passing-arg=-argument-scope-delimiter --passing-arg=-w --passing-arg=-overwriting-delimiting-key --passing-arg=-w --passing-arg=-closed-notation-not-level-0 --passing-arg=-w --passing-arg=-postfix-notation-not-level-1 --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=ondemand --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/mathcomp/mathcomp --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/mathcomp/mathcomp mathcomp -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log
build
No files were found with the provided path: tmp.v. No artifacts will be uploaded.
build
No files were found with the provided path: metadata. No artifacts will be uploaded.

Artifacts

Produced during runtime
Name Size
bug.log Expired
4.14 KB
bug.v Expired
21.2 KB
bug.verbose.log Expired
11.8 MB
build.log Expired
350 KB