Anomaly "Uncaught exception Not_found."

Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/neural-net-coq-interp/theories/bug_search_anom_not_found_03.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=/home/coq/.opam/4.13.1+flambda/bin/coqc.orig --coqtop=/home/coq/.opam/4.13.1+flambda/bin/coqtop.orig --coq_makefile=/home/coq/.opam/4.13.1+flambda/bin/coq_makefile --coqdep /home/coq/.opam/4.13.1+flambda/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 --arg=-q --arg=-w --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 --arg=-w --arg=-deprecated-native-compiler-option --arg=-native-compiler --arg=no -R /github/workspace/neural-net-coq-interp/theories NeuralNetInterp -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

::warning::Failed to inline Ltac2.Array via Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmp5ygtevid/NeuralNetInterp/bug_search_anom_not_found_03.v", line 335, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp5ygtevid/NeuralNetInterp/bug_search_anom_not_found_03.v", line 337, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp5ygtevid/NeuralNetInterp/bug_search_anom_not_found_03.v", line 337, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp5ygtevid/NeuralNetInterp/bug_search_anom_not_found_03.v", line 389, characters 2-238: Error: Anomaly "Missing hardwired primitive Ltac2.Array.get" 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/neural-net-coq-interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.bug_search_anom_not_found_03") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 220 lines to 39 lines, then from 52 lines to 522 lines, then from 524 lines to 229 lines, then from 699 lines to 216 lines, then from 228 lines to 118 lines, then from 131 lines to 665 lines, then from 670 lines to 135 lines, then from 148 lines to 1326 lines, then from 1331 lines to 173 lines, then from 186 lines to 747 lines, then from 752 lines to 498 lines, then from 511 lines to 883 lines, then from 887 lines to 744 lines, then from 757 lines to 844 lines, then from 849 lines to 749 lines, then from 762 lines to 829 lines, then from 834 lines to 761 lines, then from 774 lines to 850 lines, then from 855 lines to 774 lines, then from 787 lines to 837 lines, then from 842 lines to 790 lines, then from 803 lines to 1422 lines, then from 1427 lines to 811 lines *) (* coqc version 8.19+alpha compiled with OCaml 4.13.1 coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (61ee398ed32f9334dd664ea8ed2697178e6e3844) Expected coqc runtime on this file: 1.377 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 NeuralNetInterp.Util.Classes.RelationPairs.Dependent. Require NeuralNetInterp.Util.Option. Require NeuralNetInterp.Torch.Tensor.Instances. Require NeuralNetInterp.Torch.Slicing. Require NeuralNetInterp.TransformerLens.HookedTransformer.Config. Require Ltac2.Constr. Require Ltac2.Printf. Require Ltac2.List. Require Ltac2.Std. Require Ltac2.Pattern. Require Ltac2.Init. Require Ltac2.Bool. Require Ltac2.Int. Require Ltac2.Message. Require Ltac2.Control. Module Ltac2_DOT_Array_WRAPPED. Module Array. (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control

::warning::Failed to inline Ltac2.Array via Include, with Requires and preserve the error. The new error was: File "/tmp/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 45, characters 0-26: 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/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 46, characters 0-18: 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/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 47, characters 0-22: 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/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 48, characters 0-19: 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/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 49, characters 0-22: 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/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 335, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 337, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 337, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpy6pt6g0l/NeuralNetInterp/bug_search_anom_not_found_03.v", line 389, characters 2-238: Error: Anomaly "Missing hardwired primitive Ltac2.Array.get" 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/neural-net-coq-interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.bug_search_anom_not_found_03") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 220 lines to 39 lines, then from 52 lines to 522 lines, then from 524 lines to 229 lines, then from 699 lines to 216 lines, then from 228 lines to 118 lines, then from 131 lines to 665 lines, then from 670 lines to 135 lines, then from 148 lines to 1326 lines, then from 1331 lines to 173 lines, then from 186 lines to 747 lines, then from 752 lines to 498 lines, then from 511 lines to 883 lines, then from 887 lines to 744 lines, then from 757 lines to 844 lines, then from 849 lines to 749 lines, then from 762 lines to 829 lines, then from 834 lines to 761 lines, then from 774 lines to 850 lines, then from 855 lines to 774 lines, then from 787 lines to 837 lines, then from 842 lines to 790 lines, then from 803 lines to 1422 lines, then from

::warning::Failed to inline Ltac2.Array via Include, with Requires and preserve the error. The new error was: File "/tmp/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 54, characters 0-26: 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/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 55, characters 0-18: 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/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 56, characters 0-22: 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/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 57, characters 0-19: 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/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 58, characters 0-22: 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/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 334, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 336, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 336, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpu56tijow/NeuralNetInterp/bug_search_anom_not_found_03.v", line 388, characters 2-238: Error: Anomaly "Missing hardwired primitive Ltac2.Array.get" 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/neural-net-coq-interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.bug_search_anom_not_found_03") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 220 lines to 39 lines, then from 52 lines to 522 lines, then from 524 lines to 229 lines, then from 699 lines to 216 lines, then from 228 lines to 118 lines, then from 131 lines to 665 lines, then from 670 lines to 135 lines, then from 148 lines to 1326 lines, then from 1331 lines to 173 lines, then from 186 lines to 747 lines, then from 752 lines to 498 lines, then from 511 lines to 883 lines, then from 887 lines to 744 lines, then from 757 lines to 844 lines, then from 849 lines to 749 lines, then from 762 lines to 829 lines, then from 834 lines to 761 lines, then from 774 lines to 850 lines, then from 855 lines to 774 lines, then from 787 lines to 837 lines, then from 842 lines to 790 lines, then from 803 lines to 1422 lines, then from

::warning::Failed to inline Ltac2.Array without Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmp2ymxwlge/NeuralNetInterp/bug_search_anom_not_found_03.v", line 329, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp2ymxwlge/NeuralNetInterp/bug_search_anom_not_found_03.v", line 331, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp2ymxwlge/NeuralNetInterp/bug_search_anom_not_found_03.v", line 331, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmp2ymxwlge/NeuralNetInterp/bug_search_anom_not_found_03.v", line 383, characters 2-238: Error: Anomaly "Missing hardwired primitive Ltac2.Array.get" 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/neural-net-coq-interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.bug_search_anom_not_found_03") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 220 lines to 39 lines, then from 52 lines to 522 lines, then from 524 lines to 229 lines, then from 699 lines to 216 lines, then from 228 lines to 118 lines, then from 131 lines to 665 lines, then from 670 lines to 135 lines, then from 148 lines to 1326 lines, then from 1331 lines to 173 lines, then from 186 lines to 747 lines, then from 752 lines to 498 lines, then from 511 lines to 883 lines, then from 887 lines to 744 lines, then from 757 lines to 844 lines, then from 849 lines to 749 lines, then from 762 lines to 829 lines, then from 834 lines to 761 lines, then from 774 lines to 850 lines, then from 855 lines to 774 lines, then from 787 lines to 837 lines, then from 842 lines to 790 lines, then from 803 lines to 1422 lines, then from 1427 lines to 811 lines *) (* coqc version 8.19+alpha compiled with OCaml 4.13.1 coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (61ee398ed32f9334dd664ea8ed2697178e6e3844) Expected coqc runtime on this file: 1.377 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 NeuralNetInterp.Util.Classes.RelationPairs.Dependent. Require NeuralNetInterp.Util.Option. Require NeuralNetInterp.Torch.Tensor.Instances. Require NeuralNetInterp.Torch.Slicing. Require NeuralNetInterp.TransformerLens.HookedTransformer.Config. Require Ltac2.Constr. Require Ltac2.Printf. Require Ltac2.List. Require Ltac2.Std. Require Ltac2.Pattern. Require Ltac2.Init. Require Ltac2.Bool. Require Ltac2.Int. Require Ltac2.Message. Require Ltac2.Control. Module Export Ltac2_DOT_Array. Module Export Ltac2. Module Array. (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,

::warning::Failed to inline Ltac2.Array without Include, with Requires and preserve the error. The new error was: File "/tmp/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 46, characters 0-26: 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/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 47, characters 0-18: 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/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 48, characters 0-22: 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/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 49, characters 0-19: 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/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 50, characters 0-22: 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/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 329, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 331, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 331, characters 0-11: Warning: Trying to mask the absolute name "Ltac2.Constr.Unsafe"! [masking-absolute-name,deprecated-since-8.8,deprecated,default] File "/tmp/tmpq5jk0i3_/NeuralNetInterp/bug_search_anom_not_found_03.v", line 383, characters 2-238: Error: Anomaly "Missing hardwired primitive Ltac2.Array.get" 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,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/neural-net-coq-interp/theories" "NeuralNetInterp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "NeuralNetInterp.bug_search_anom_not_found_03") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 220 lines to 39 lines, then from 52 lines to 522 lines, then from 524 lines to 229 lines, then from 699 lines to 216 lines, then from 228 lines to 118 lines, then from 131 lines to 665 lines, then from 670 lines to 135 lines, then from 148 lines to 1326 lines, then from 1331 lines to 173 lines, then from 186 lines to 747 lines, then from 752 lines to 498 lines, then from 511 lines to 883 lines, then from 887 lines to 744 lines, then from 757 lines to 844 lines, then from 849 lines to 749 lines, then from 762 lines to 829 lines, then from 834 lines to 761 lines, then from 774 lines to 850 lines, then from 855 lines to 774 lines, then from 787 lines to 837 lines, then from 842 lines to 790 lines, then from 803 lines to 1422 lines, then