Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/test_bug.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=/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 -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline --arg=-q -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

::warning::Failed to inline Wasm.binary_format_parser via Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmpcpglkphf/test_bug.v", line 79, characters 7-13: Error: Cannot find module leb128 The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-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/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines *) (* coqc version 8.19.2 compiled with OCaml 4.13.1 coqtop version 8.19.2 Expected coqc runtime on this file: 1.021 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 Coq.Arith.PeanoNat. Require Coq.Arith.Wf_nat. Require Coq.Lists.List. Require Coq.NArith.BinNat. Require Coq.NArith.NArith. Require Coq.NArith.Ndec. Require Coq.PArith.BinPos. Require Coq.Strings.Ascii. Require Coq.Strings.Byte. Require Coq.Strings.String. Require Coq.Vectors.Vector. Require Coq.ZArith.BinInt. Require Coq.micromega.Lia. Require Coq.setoid_ring.Ring. Require Coq.ssr.ssrbool. Require Coq.ssr.ssreflect. Require Coq.ssr.ssrfun. Require ExtLib.Core.Any. Require Wasm.array. Require Wasm.datatypes_properties. Require Wasm.numerics. Require compcert.common.Memdata. Require compcert.lib.Floats. Require compcert.lib.Integers. Require mathcomp.ssreflect.ssrnotations. Require parseque.Indexed. Require ExtLib.Structures.Functor. Require Wasm.memory. Require mathcomp.ssreflect.ssreflect. Require parseque.Category. Require parseque.NEList. Require ExtLib.Structures.Applicative. Require parseque.EqDec. Require parseque.Induction. Require ExtLib.Structures.Monad. Require parseque.Sized. Require parseque.StringAsList. Require mathcomp.ssreflect.ssrfun. Require Wasm.list_extra. Require parseque.Success. Require mathcomp.ssreflect.ssrbool. Require mathcomp.ssreflect.eqtype. Require parseque.Combinators. Require mathcomp.ssreflect.ssrnat. Require mathcomp.ssreflect.seq. Require parseque.Numbers. Require Wasm.bytes. Require parseque.Char. Require Wasm.common. Require parseque.Parseque. Require Wasm.memory_list. Require Wasm.datatypes. Require Wasm.operations. Require Wasm.typing. Module Wasm_DOT_binary_format_parser_WRAPPED. Module binary_format_parser. (** Parser for the binary Wasm format. **) (* (C) J. Pichon - see LICENSE.txt *) (* TODO: all the numeric stuff is in dire need of testing *) Import Wasm.datatypes Wasm.datatypes_properties Wasm.typing. Import compcert.lib.Integers. Import parseque.Parseque. Import Coq.Strings.Byte. Import leb128

::warning::Failed to inline Wasm.binary_format_parser via Include, with Requires and preserve the error. The new error was: File "/tmp/tmphmve5olp/test_bug.v", line 22, characters 0-68: 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/tmphmve5olp/test_bug.v", line 23, characters 0-37: 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/tmphmve5olp/test_bug.v", line 24, characters 0-33: 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/tmphmve5olp/test_bug.v", line 25, characters 0-32: 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/tmphmve5olp/test_bug.v", line 26, characters 0-22: Error: Cannot find a physical path bound to logical path leb128. The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-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/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines *) (* coqc version 8.19.2 compiled with OCaml 4.13.1 coqtop version 8.19.2 Expected coqc runtime on this file: 1.021 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 Wasm_DOT_binary_format_parser_WRAPPED. Module binary_format_parser. (** Parser for the binary Wasm format. **) (* (C) J. Pichon - see LICENSE.txt *) (* TODO: all the numeric stuff is in dire need of testing *) Require Import Wasm.datatypes Wasm.datatypes_properties Wasm.typing. Require Import compcert.lib.Integers. Require Import parseque.Parseque. Require Import Coq.Strings.Byte. Require Import leb128.

::warning::Failed to inline Wasm.binary_format_parser via Include, with Requires and preserve the error. The new error was: File "/tmp/tmpz_olct1u/test_bug.v", line 21, characters 0-68: 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/tmpz_olct1u/test_bug.v", line 22, characters 0-37: 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/tmpz_olct1u/test_bug.v", line 23, characters 0-33: 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/tmpz_olct1u/test_bug.v", line 24, characters 0-32: 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/tmpz_olct1u/test_bug.v", line 25, characters 0-22: Error: Cannot find a physical path bound to logical path leb128. The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-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/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines *) (* coqc version 8.19.2 compiled with OCaml 4.13.1 coqtop version 8.19.2 Expected coqc runtime on this file: 1.021 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 Wasm_DOT_binary_format_parser_WRAPPED. Module binary_format_parser. (** Parser for the binary Wasm format. **) (* (C) J. Pichon - see LICENSE.txt *) (* TODO: all the numeric stuff is in dire need of testing *) Require Import Wasm.datatypes Wasm.datatypes_properties Wasm.typing. Require Import compcert.lib.Integers. Require Import parseque.Parseque. Require Import Coq.Strings.Byte. Require Import leb128.

::warning::Failed to inline Wasm.binary_format_parser without Include, stripping Requires and preserve the error. The new error was: File "/tmp/tmpdiry7ar6/test_bug.v", line 80, characters 7-13: Error: Cannot find module leb128 The file generating the error was: (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-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/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines *) (* coqc version 8.19.2 compiled with OCaml 4.13.1 coqtop version 8.19.2 Expected coqc runtime on this file: 1.021 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 Coq.Arith.PeanoNat. Require Coq.Arith.Wf_nat. Require Coq.Lists.List. Require Coq.NArith.BinNat. Require Coq.NArith.NArith. Require Coq.NArith.Ndec. Require Coq.PArith.BinPos. Require Coq.Strings.Ascii. Require Coq.Strings.Byte. Require Coq.Strings.String. Require Coq.Vectors.Vector. Require Coq.ZArith.BinInt. Require Coq.micromega.Lia. Require Coq.setoid_ring.Ring. Require Coq.ssr.ssrbool. Require Coq.ssr.ssreflect. Require Coq.ssr.ssrfun. Require ExtLib.Core.Any. Require Wasm.array. Require Wasm.datatypes_properties. Require Wasm.numerics. Require compcert.common.Memdata. Require compcert.lib.Floats. Require compcert.lib.Integers. Require mathcomp.ssreflect.ssrnotations. Require parseque.Indexed. Require ExtLib.Structures.Functor. Require Wasm.memory. Require mathcomp.ssreflect.ssreflect. Require parseque.Category. Require parseque.NEList. Require ExtLib.Structures.Applicative. Require parseque.EqDec. Require parseque.Induction. Require ExtLib.Structures.Monad. Require parseque.Sized. Require parseque.StringAsList. Require mathcomp.ssreflect.ssrfun. Require Wasm.list_extra. Require parseque.Success. Require mathcomp.ssreflect.ssrbool. Require mathcomp.ssreflect.eqtype. Require parseque.Combinators. Require mathcomp.ssreflect.ssrnat. Require mathcomp.ssreflect.seq. Require parseque.Numbers. Require Wasm.bytes. Require parseque.Char. Require Wasm.common. Require parseque.Parseque. Require Wasm.memory_list. Require Wasm.datatypes. Require Wasm.operations. Require Wasm.typing. Module Export Wasm_DOT_binary_format_parser. Module Export Wasm. Module binary_format_parser. (** Parser for the binary Wasm format. **) (* (C) J. Pichon - see LICENSE.txt *) (* TODO: all the numeric stuff is in dire need of testing *) Import Wasm.datatypes Wasm.datatypes_properties Wasm.typing. Import compcert.lib.Integers. Import parseque.Parseque. Import Coq.Strings.Byte. Import leb128