Set up CI minimization run for ci-stdlib #2075
Annotations
3 errors and 10 warnings
|
Run minimizer
Tactic failure: Cannot solve this goal.
|
|
Run minimizer
Tactic failure: Cannot solve this goal.
|
|
Run minimizer
Tactic failure: Cannot solve this goal.
|
|
Run minimizer
Using opam switch '4.14.1+flambda'
|
|
Run minimizer
which ocamlfind: '/root/.opamcache/4.14.1+flambda/bin/ocamlfind'
|
|
Run minimizer
ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.14.1
Standard library directory: /root/.opamcache/4.14.1+flambda/lib/ocaml
|
|
Run minimizer
download failing artifacts @ 01959148c9a3711e03392900b622507fc874d42c https://gitlab.inria.fr/coq/coq/-/jobs/5305102/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5305067/artifacts/download
|
|
Run minimizer
download passing artifacts @ c9151ded11e3960158722e095daf39122a5e92f9 https://gitlab.inria.fr/coq/coq/-/jobs/5304981/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/5304946/artifacts/download
|
|
Run minimizer
(/github/workspace/builds/coq/coq-failing) /builds/coq/coq/_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/../rocq-runtime/
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
|
|
Run minimizer
(/github/workspace/builds/coq/coq-failing) setting up coq_environment.txt: COQLIB="/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/"
COQCORELIB="/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/../rocq-runtime/"
DOCDIR="/github/workspace/builds/coq/coq-failing/_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"
OCAMLPATH=""
|
|
Run minimizer
(/github/workspace/builds/coq/coq-passing) /builds/coq/coq/_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/../rocq-runtime/
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
|
|
Run minimizer
(/github/workspace/builds/coq/coq-passing) setting up coq_environment.txt: COQLIB="/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/"
COQCORELIB="/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/../rocq-runtime/"
DOCDIR="/github/workspace/builds/coq/coq-passing/_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"
OCAMLPATH=""
|
|
Run minimizer
Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/stdlib/_build/default/theories/Numbers/Integer/NatPairs/ZNatPairs.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/stdlib/_build/default -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline %0A --nonpassing-arg=-q --nonpassing-arg=-w --nonpassing-arg=+default --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-output-dir --nonpassing-arg=. --nonpassing-arg=-native-compiler --nonpassing-arg=on --nonpassing-arg=-nI --nonpassing-arg=/github/workspace/builds/coq/coq-failing/_build_ci/stdlib/.wrappers/kernel --nonpassing-arg=-nI --nonpassing-arg=theories --nonpassing-arg=-nI --nonpassing-arg=theories/Arith --nonpassing-arg=-nI --nonpassing-arg=theories/Array --nonpassing-arg=-nI --nonpassing-arg=theories/BinNums --nonpassing-arg=-nI --nonpassing-arg=theories/Bool --nonpassing-arg=-nI --nonpassing-arg=theories/Classes --nonpassing-arg=-nI --nonpassing-arg=theories/Compat --nonpassing-arg=-nI --nonpassing-arg=theories/FSets --nonpassing-arg=-nI --nonpassing-arg=theories/Floats --nonpassing-arg=-nI --nonpassing-arg=theories/Init --nonpassing-arg=-nI --nonpassing-arg=theories/Lists --nonpassing-arg=-nI --nonpassing-arg=theories/Logic --nonpassing-arg=-nI --nonpassing-arg=theories/MSets --nonpassing-arg=-nI --nonpassing-arg=theories/NArith --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Cyclic --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Cyclic/Abstract --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Cyclic/Int63 --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Integer --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Integer/Abstract --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Integer/Binary --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Integer/NatPairs --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/NatInt --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Natural --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Natural/Abstract --nonpassing-arg=-nI --nonpassing-arg=theories/Numbers/Natural/Binary --nonpassing-arg=-nI --nonpassing-arg=theories/PArith --nonpassing-arg=-nI --nonpassing-arg=theories/Program --nonpassing-arg=-nI --nonpassing-arg=theories/QArith --nonpassing-arg=-nI --nonpassing-arg=theories/Reals --nonpassing-arg=-nI --nonpassing-arg=theories/Reals/Abstract --nonpassing-arg=-nI --nonpassing-arg=theories/Reals/Cauchy --nonpassing-arg=-nI --nonpassing-arg=theories/Relations --nonpassing-arg=-nI --nonpassing-arg=theories/Setoids --nonpassing-arg=-nI --nonpassing-arg=theories/Sets --nonpassing-arg=-nI --nonpassing-arg=theories/Sorting --nonpassing-arg=-nI --nonpassing-arg=theories/Streams --nonpassing-arg=-nI --nonpassing-arg=theories/Strings --nonpassing-arg=-nI --nonpassing-arg=theories/Structures --nonpassing-arg=-nI --nonpassing-arg=theories/Unicode --nonpassing-arg=-nI --nonpassing-arg=theories/Vectors --nonpassing-arg=-nI --nonpassing-arg=theories/Wellfounded --nonpassing-arg=-nI --nonpassing-arg=theories/ZArith --nonpassing-arg=-nI --nonpassing-arg=theories/btauto --nonpassing-arg=-nI --nonpassing-arg=theories/derive --nonpassing-arg=-nI --nonpassing-arg=theories/extraction --nonpassing-arg=-nI --nonpassing-arg=theories/funind --nonpassing-arg=-nI --nonpassing-arg=theories/micromega --nonpassing-arg=-n
|
Loading