Using opam switch '4.09.0'

which ocamlfind: '/root/.opamcache/4.09.0/bin/ocamlfind'

ocamlfind ocamlopt -v: The OCaml native-code compiler, version 4.09.0 Standard library directory: /root/.opamcache/4.09.0/lib/ocaml

download failing artifacts @ d1323021b789596896d9d5bb76f48cff1caea95a https://gitlab.inria.fr/coq/coq/-/jobs/3498631/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3498686/artifacts/download

download passing artifacts @ be8726c0a5d49673132a687b815fb3f68a243127 https://gitlab.inria.fr/coq/coq/-/jobs/3498440/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3498495/artifacts/download

/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.09.0/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

/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.09.0/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

Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/neural_net_interp/theories/TransformerLens/HookedTransformer.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=+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\,-ltac2-missing-notation-var\,unsupported-attributes --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/neural_net_interp/theories NeuralNetInterp --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\,-ltac2-missing-notation-var\,unsupported-attributes --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/neural_net_interp/theories NeuralNetInterp -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

::warning::Failed to inline Ltac2.Notations via Include, stripping Requires and preserve the error. The alternate coqc (/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig) was supposed to pass, but instead emitted an error. The new error was: File "/tmp/tmphqz7wz7m/HookedTransformer.v", line 499, characters 6-28: Error: Unbound value Constr.Pretype.pretype 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/neural_net_interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.TransformerLens.HookedTransformer") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 473 lines to 51 lines, then from 64 lines to 441 lines, then from 445 lines to 322 lines, then from 335 lines to 1735 lines, then from 1740 lines to 476 lines, then from 489 lines to 648 lines, then from 653 lines to 476 lines, then from 489 lines to 788 lines, then from 793 lines to 467 lines, then from 480 lines to 1012 lines, then from 1017 lines to 469 lines, then from 482 lines to 847 lines, then from 852 lines to 477 lines, then from 490 lines to 718 lines, then from 723 lines to 501 lines, then from 514 lines to 548 lines, then from 553 lines to 512 lines, then from 525 lines to 559 lines, then from 564 lines to 513 lines, then from 526 lines to 560 lines, then from 565 lines to 519 lines, then from 532 lines to 637 lines, then from 642 lines to 522 lines, then from 535 lines to 624 lines, then from 629 lines to 527 lines, then from 540 lines to 609 lines, then from 614 lines to 539 lines, then from 552 lines to 630 lines, then from 635 lines to 552 lines, then from 565 lines to 617 lines, then from 622 lines to 568 lines *) (* coqc version 8.19+alpha compiled with OCaml 4.09.0 coqtop version 8b9980c1a092:/builds/coq/coq/_build/default,(HEAD detached at 2564ef3) (2564ef398cf18455f1f1b63024e337c08cfbab26) Expected coqc runtime on this file: 0.602 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 Ltac2.Constr. Require Ltac2.Printf. Require Ltac2.List. Require Ltac2.Init. Require Ltac2.Bool. Require Ltac2.Ind. Require Ltac2.Int. Require Ltac2.Message. Require Ltac2.Std. Require Ltac2.Constr. Require Ltac2.Control. Require Ltac2.Pattern. Require Ltac2.Array. Module Ltac2_DOT_Notations_WRAPPED. Module Notations. (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Import Ltac2.Init. (** Constr matching *) Ltac2 Notation "lazy_match!" t(tactic(6)) "with" m(constr_matching) "end" := Pattern.lazy_match0 t m. Ltac2 Nota