Set up CI minimization resumption run for ci-fiat_crypto #1512
coqbotAnnotations
2 errors and 10 warnings
|
build
Some unresolved existential variables remain
|
|
build
Some unresolved existential variables remain
|
|
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 @ cecd17315cceead371ebd704ec97df139dad33e8 https://gitlab.com/coq/coq/-/jobs/4437684128/artifacts/download https://gitlab.com/coq/coq/-/jobs/4437684172/artifacts/download
|
|
build
download passing artifacts @ 6e739ce1f8ec685f7e409f0799a894c45c4325ea https://gitlab.com/coq/coq/-/jobs/4436252752/artifacts/download https://gitlab.com/coq/coq/-/jobs/4436253439/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/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=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --nonpassing-arg=-w --nonpassing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --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/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler compiler --nonpassing-Q /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src Crypto --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=+implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+unexpected-implicit-declaration\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive\,+undeclared-scope\,+deprecated-hint-rewrite-without-locality\,+deprecated-hint-without-locality\,+deprecated-instance-without-locality\,+deprecated-typeclasses-transparency-without-locality\,unsupported-attributes --passing-arg=-w --passing-arg=-notation-overridden\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths\,-masking-absolute-name --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/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples --passing-Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compil
|
|
build
::warning::Failed to inline Rewriter.Util.plugins.RewriterBuildRegistry via Include, stripping Requires and preserve the error.
The new error was:
File "/tmp/tmpf961f53s/Top/bug_01.v", line 237, characters 2-230:
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
The file generating the error was:
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Expected coqc runtime on this file: 8.728 sec *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Crypto.Util.Tactics.SubstEvars.
Require Crypto.Util.ListUtil.Filter.
Require Crypto.Language.IdentifierParameters.
Require Coq.Arith.Arith.
Require Coq.Arith.Peano_dec.
Require Coq.Bool.Bool.
Require Coq.Classes.CMorphisms.
Require Coq.Classes.Morphisms.
Require Coq.Classes.RelationClasses.
Require Coq.FSets.FMapPositive.
Require Coq.Lists.List.
Require Coq.Lists.SetoidList.
Require Coq.Logic.Eqdep_dec.
Require Coq.MSets.MSetFacts.
Require Coq.MSets.MSetPositive.
Require Coq.NArith.BinNat.
Require Coq.NArith.NArith.
Require Coq.Numbers.BinNums.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.Program.Tactics.
Require Coq.Relations.Relation_Definitions.
Require Coq.Relations.Relations.
Require Coq.Setoids.Setoid.
Require Coq.Strings.Ascii.
Require Coq.St
|
|
build
::warning::Failed to inline Rewriter.Util.plugins.RewriterBuildRegistry via Include, with Requires and preserve the error.
The new error was:
File "/tmp/tmpfivou07r/Top/bug_01.v", line 18, characters 0-66:
Warning: Use of “Require” inside a module is fragile. It is not recommended
to use this functionality in finished proof scripts.
[require-in-module,fragile,default]
File "/tmp/tmpfivou07r/Top/bug_01.v", line 68, characters 2-230:
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
The file generating the error was:
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes" "-w" "-notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1498 lines to 11 lines, then from 24 lines to 324 lines, then from 329 lines to 52 lines, then from 65 lines to 384 lines, then from 389 lines to 57 lines, then from 70 lines to 840 lines, then from 845 lines to 118 lines, then from 131 lines to 380 lines, then from 385 lines to 130 lines, then from 143 lines to 339 lines, then from 344 lines to 132 lines, then from 150 lines to 132 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.14.1
coqtop version runner-vxtc-u6t-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at d7ce6d9) (d7ce6d9deac92848bd8420d857a18a96a87da88b)
Expected coqc runtime on this file: 8.728 sec *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Module Rewriter_DOT_Util_DOT_plugins_DOT_RewriterBuildRegistry_WRAPPED.
Module RewriterBuildRegistry.
Require Export Rewriter.Util.plugins.RewriterBuildRegistryImports.
Register Basic.GoalType.package_with_args as rewriter.basic_package_with_args.type.
Register Basic.GoalType.base_elim_with_args as rewriter.base_elim_with_args.type.
Register Basic.GoalType.ident_elim_with_args as rewriter.ident_elim_with_args.type.
Register Basic.GoalType.ident_elim_with_args as rewriter.pattern_ident_elim_with_args.type.
Register Basic.GoalType.ident_elim_with_
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
artifact
Expired
|
4.22 GB |
|
|
bug.log
Expired
|
493 KB |
|
|
bug.v
Expired
|
34.1 KB |
|
|
bug.verbose.log
Expired
|
186 MB |
|
|
build.log
Expired
|
7.37 MB |
|
|
metadata
Expired
|
786 Bytes |
|
|
tmp.v
Expired
|
14.8 KB |
|