Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Anomaly "Uncaught exception Failure("hd")." #18004

Closed
doside opened this issue Sep 1, 2023 · 3 comments · Fixed by #18005
Closed

Anomaly "Uncaught exception Failure("hd")." #18004

doside opened this issue Sep 1, 2023 · 3 comments · Fixed by #18005
Milestone
8.19+rc1

Comments

@doside
Copy link

doside commented Sep 1, 2023 •
edited by SkySkimmer

Description of the problem

I meet the report from COQIDE:
Anomaly "Uncaught exception Failure("hd")."
Please report at http://coq.inria.fr/bugs/.

@coqbot minimize

	Inductive U :=
	| p :nat->nat->U.
	Check  match p 1 2 with
	  | (p n 0 | p n (S n)) => 0
	  | _ =>1
	end.

Coq Version

Coq 8.16.1 on windows10 x64 platform.

This is the ouput of coqtop -d:

Coq < Inductive U :=
| p :nat->nat->U.
Check match p 1 2 with
| (p n 0 | p n (S n)) => 0
| _ =>1
end.Coq < Debug: [vernacinterp] interpreting: Inductive U :=
p : nat -> nat -> U
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Set|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Set|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<nat -> nat -> U|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<nat -> U|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<U|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<U|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Set|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Set|>>
Debug: [RAKAM] <><><><><>
Debug: [RAKAM] <<Type|>>
Debug: [RAKAM] <><><><><>
U is defined
Debug: [RAKAM] <<U|>>
Debug: [RAKAM] <><><><><>
U_rect is defined
Debug: [RAKAM] <<U|>>
Debug: [RAKAM] <><><><><>
U_ind is defined
U_rec is defined
Debug: [RAKAM] <<U|>>
Debug: [RAKAM] <><><><><>
U_sind is defined

Coq < Coq < Coq < Coq <
Debug:
[vernacinterp] interpreting: Check
match p 1 2 with
| (p n 0 | p n (S n)) => 0
| _ => 1
end
Debug: [Cbv] Unfolding Coq.Init.Nat.of_num_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint_acc
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_mul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_addmul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.of_num_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint_acc
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_mul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_addmul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.of_num_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint
Debug: [Cbv] Unfolding Coq.Init.Nat.of_uint_acc
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_mul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_addmul
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Debug: [Cbv] Unfolding Coq.Init.Nat.tail_add
Toplevel input, characters 1-71:

Check match p 1 2 with
| (p n 0 | p n (S n)) => 0
| _ =>1
end.
Error: Anomaly "Uncaught exception Failure("hd")."
Please report at http://coq.inria.fr/bugs/.
Raised at Stdlib.failwith in file "stdlib.ml" (inlined), line 29, characters 17-33
Called from Stdlib__List.hd in file "list.ml" (inlined), line 30, characters 10-23
Called from Constrintern.check_or_pat_variables in file "interp/constrintern.ml", line 1471, characters 16-31
Called from Constrintern.intern_pat in file "interp/constrintern.ml", line 1905, characters 6-51
Called from Constrintern.internalize.intern_multiple_pattern in file "interp/constrintern.ml" (inlined), line 2346, characters 28-103
Called from CList.map in file "clib/cList.ml" (inlined), line 431, characters 21-24
Called from Constrintern.internalize.intern_multiple_pattern in file "interp/constrintern.ml" (inlined), line 2346, characters 19-106
Called from Constrintern.internalize.intern_multiple_pattern in file "interp/constrintern.ml", line 2346, characters 19-106
Called from Constrintern.internalize.intern_multiple_pattern in file "interp/constrintern.ml" (inlined), line 2344, characters 30-351
Called from Constrintern.internalize.intern_disjunctive_multiple_pattern in file "interp/constrintern.ml" (inlined), line 2354, characters 24-55
Called from CList.map in file "clib/cList.ml" (inlined), line 431, characters 21-24
Called from Constrintern.internalize.intern_disjunctive_multiple_pattern in file "interp/constrintern.ml" (inlined), line 2354, characters 15-59
Called from Constrintern.internalize.intern_disjunctive_multiple_pattern in file "interp/constrintern.ml", line 2354, characters 15-59
Called from Constrintern.internalize.intern_eqn in file "interp/constrintern.ml", line 2362, characters 22-71
Called from Constrintern.internalize.intern.(fun) in file "interp/constrintern.ml" (inlined), line 2246, characters 29-63
Called from CList.map in file "clib/cList.ml" (inlined), line 431, characters 21-24
Called from Constrintern.internalize.intern.(fun) in file "interp/constrintern.ml" (inlined), line 2246, characters 20-68
Called from Constrintern.internalize.intern.(fun) in file "interp/constrintern.ml", line 2246, characters 20-68
Called from Constrintern.intern_gen in file "interp/constrintern.ml" (inlined), line 2554, characters 2-290
Called from Constrintern.interp_open_constr in file "interp/constrintern.ml" (inlined), line 2587, characters 27-65
Called from Vernacentries.vernac_check_may_eval in file "vernac/vernacentries.ml", line 1967, characters 17-106
Called from Vernacextend.vtreadproofopt.(fun) in file "vernac/vernacextend.ml", line 170, characters 29-44
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 205, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml" (inlined), line 17, characters 14-17
Called from Flags.without_option in file "lib/flags.ml" (inlined), line 27, characters 27-82
Called from Flags.verbosely in file "lib/flags.ml", line 65, characters 20-44
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 255, characters 18-43
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml" (inlined), line 253, characters 21-276
Called from Vernacinterp.vernac_timeout in file "vernac/vernacinterp.ml" (inlined), line 62, characters 4-7
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml" (inlined), line 253, characters 6-279
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml" (inlined), line 253, characters 6-279
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml" (inlined), line 267, characters 2-57
Called from Stm.stm_vernac_interp in file "stm/stm.ml", line 1043, characters 4-58
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2177, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2319, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2420, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 123, characters 2-60
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 431, characters 17-62
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 1, 2023

Hey @doside, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 1, 2023

@doside, Minimized File /github/workspace/thebug.v (full log on GitHub Actions)

Minimized Coq File (consider adding this file to the test-suite) 
(* -*- 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/Ltac2" "Ltac2" "-top" "thebug") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 21 lines to 8 lines, then from 13 lines to 8 lines *)
(* coqc version 8.17.1 compiled with OCaml 4.13.1
   coqtop version 8.17.1
   Expected coqc runtime on this file: 0.099 sec *)
Inductive U :=
	| p :nat->nat->U.
	Check  match p 1 2 with
	  | (p n 0 | p n (S n)) => 0
	  | _ =>1
	end.
Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) 




Build Log (contains the Coq error message)

+ �[33;1m(/github/workspace/run-script.sh @ line 47) $�[0m ocamlc -config
version: 4.13.1
standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml
standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml
ccomp_type: cc
c_compiler: gcc
ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC 
ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 
ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC 
ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 
bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC  -D_FILE_OFFSET_BITS=64 
native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC  -D_FILE_OFFSET_BITS=64 
bytecomp_c_libraries: -lm -ldl  -lpthread
native_c_libraries: -lm -ldl 
native_pack_linker: ld -r -o 
ranlib: ranlib
architecture: amd64
model: default
int_size: 63
word_size: 64
system: linux
asm: as
asm_cfi_supported: true
with_frame_pointers: false
ext_exe: 
ext_obj: .o
ext_asm: .s
ext_lib: .a
ext_dll: .so
os_type: Unix
default_executable_name: a.out
systhread_supported: true
host: x86_64-pc-linux-gnu
target: x86_64-pc-linux-gnu
flambda: true
safe_string: true
default_safe_string: true
flat_float_array: true
function_sections: true
afl_instrument: false
windows_unicode: false
supports_shared_libraries: true
exec_magic_number: Caml1999X030
cmi_magic_number: Caml1999I030
cmo_magic_number: Caml1999O030
cma_magic_number: Caml1999A030
cmx_magic_number: Caml1999y030
cmxa_magic_number: Caml1999z030
ast_impl_magic_number: Caml1999M030
ast_intf_magic_number: Caml1999N030
cmxs_magic_number: Caml1999D030
cmt_magic_number: Caml1999T030
linear_magic_number: Caml1999L030
+ �[33;1m(/github/workspace/run-script.sh @ line 48) $�[0m coqc --config
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.DGCYDYSnmG
MINIMIZER_DEBUG: files: 
COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/
COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/
DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/
OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind
CAMLFLAGS=-thread -rectypes -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=no
+ �[33;1m(/github/workspace/run-script.sh @ line 49) $�[0m coqc --version
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.0zRQZvEBIY
MINIMIZER_DEBUG: files: 
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.13.1
+ �[33;1m(/github/workspace/run-script.sh @ line 50) $�[0m true
+ �[33;1m(/github/workspace/run-script.sh @ line 50) $�[0m coqtop
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.WPdnAEqshP
MINIMIZER_DEBUG: files: 
Welcome to Coq 8.17.1

Coq < 
+ �[33;1m(/github/workspace/run-script.sh @ line 52) $�[0m source /github/workspace/coqbot.sh
++ �[33;1m(/github/workspace/run-script.sh @ line 2) $�[0m cat
++ �[33;1m(/github/workspace/run-script.sh @ line 10) $�[0m coqc -q thebug.v
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q thebug.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.1Lbkbh1YR3
MINIMIZER_DEBUG: files:  thebug.v
File "./thebug.v", line 3, characters 1-71:
Error: Anomaly "Uncaught exception Failure("hd")."
Please report at http://coq.inria.fr/bugs/.





Minimization Log (truncated to last 8.0KiB; full 26KiB file on GitHub Actions Artifacts under bug.log)

d in stripping comments.�[0m

Now, I will attempt to factor out all of the [Require]s...
getting bug_01.v (/github/workspace/cwd/bug_01.v)
NOTE: The file bug_01.v is very new (1693584281, 0 seconds old), delaying until it's a bit older
/home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -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 -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/Ltac2 Ltac2 -top thebug -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
�[92m
Succeeded in normalizing Requires.�[0m

Now, I will attempt to split up [Require] statements...
getting /github/workspace/cwd/bug_01.v
NOTE: The file /github/workspace/cwd/bug_01.v is very new (1693584283, 0 seconds old), delaying until it's a bit older
getting /github/workspace/cwd/bug_01.glob
getting /github/workspace/cwd/bug_01.glob

No Requires to split.

In order to efficiently manipulate the file, I have to break it into statements.  I will attempt to do this by matching on periods.
�[92m
Splitting successful.�[0m

I will now attempt to remove any lines after the line which generates the error.

No lines to trim.

In order to efficiently manipulate the file, I have to break it into definitions.  I will now attempt to do this.
Sending statements to coqtop...
Done.  Splitting to definitions...
�[92m
Splitting to definitions successful.�[0m

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Qed Obligation with Admit Obligations
�[92m
Admitting Qed Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qed Obligations unsuccessful.
No successful changes.

I will now attempt to replace Qeds with Admitteds
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to replace Qeds with admit. Defined.
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to admit [abstract ...]s
�[92m
Admitting [abstract ...] successful.�[0m
�[92m
Admitting [abstract ...] successful.�[0m
Admitting [abstract ...] unsuccessful.
Admitting [abstract ...] unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Obligation with Admit Obligations
�[92m
Admitting Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Obligations unsuccessful.
No successful changes.

I will now attempt to admit lemmas with Admitted
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with Admitted
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with admit. Defined
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with admit. Defined
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to export modules
Module exportation unsuccessful.

I will now attempt to split imports and exports
Import/Export splitting unsuccessful.

I will now attempt to split := definitions
One-line definition splitting unsuccessful.

I will now attempt to remove all lines, one at a time
Line removal unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
File "/tmp/tmpndxqyzug/thebug.v", line 1, characters 14-15:
Error: The reference p was not found in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to remove empty sections

No empty sections to remove.

Now, I will attempt to strip repeated newlines and trailing spaces from this file...

No strippable newlines or spaces.





If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).

If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

      		
    

  





        


            

              
            

        

      


      

            
  

    
  
  

  

  



    












      

  
          


  
    
  
  

    
  herbelin 

      added a commit
        to herbelin/github-coq
      that referenced
      this issue

    
      Sep 1, 2023
    
    

      


  

    

      


  

      
        @herbelin
  





      

        
          Fixes coq#18004: check linearity before disjunctive patterns.
        

          
            
          

      


      

          

    
    
    

  

      


      

          

    
    

  

  

    
  



      


      
      

        
          46f8247
        
      

    

  

    

      
This happens to be another instance of a problem partially addressed
in coq#17854.

    




    

  




  


  
    
  
  

    
  herbelin 

      added a commit
        to herbelin/github-coq
      that referenced
      this issue

    
      Sep 1, 2023
    
    

      


  

    

      


  

      
        @herbelin
  





      

        
          Fixes coq#18004: check linearity before disjunctive patterns.
        

          
            
          

      


      

          

    
    
    

  

      


      

          

    
    

  

  

    
  



      


      
      

        
          9809b27
        
      

    

  

    

      
This happens to be another instance of a problem partially addressed
in coq#17854.

    




    

  




  

  

    
  


  

      

    @herbelin
herbelin



    mentioned this issue
    
      Sep 1, 2023
    





  


  

      
   Merged

  





  
  

      
        
      
      

  
    
    
  


    2 tasks
  





  




  


  
    
  
  

    
  herbelin 

      added a commit
        to herbelin/github-coq
      that referenced
      this issue

    
      Sep 1, 2023
    
    

      


  

    

      


  

      
        @herbelin
  





      

        
          Fixes coq#18004: check linearity before disjunctive patterns.
        

          
            
          

      


      

          

    
    
    

  

      


      

          

    
    

  

  

    
  



      


      
      

        
          2e27bd4
        
      

    

  

    

      
This happens to be another instance of a problem partially addressed
in coq#17854.

    




    

  









      

  
      



  

  @herbelin





  


    

      

  

    

        
    
    

  


      
          
    
            Copy link

      
    

  


  

      

      

  
  Member


      

  


  

    

      

      
          herbelin
  

      

      

      commented


        Sep 1, 2023


      
    


  





      


        


  
    

      
          
Thanks a lot for reporting! Fixed in PR #18005.

      		
    

  





        


            

              
            

        

      


      

            
  

    
  
  

  

  



    












      

  
          


  
    
  
  

    
  herbelin 

      added a commit
        to herbelin/github-coq
      that referenced
      this issue

    
      Sep 2, 2023
    
    

      


  

    

      


  

      
        @herbelin
  





      

        
          Fixes coq#18004: check linearity before disjunctive patterns.
        

          
            
          

      


      

          

    
    
    

  

      


      

          

    
    

  

  

    
  



      


      
      

        
          b7151f3
        
      

    

  

    

      
This happens to be another instance of a problem partially addressed
in coq#17854.

    




    

  




  

  


  

  

    
  

  


    

        @coqbot-app
coqbot-app
bot



        added this to the   8.19+rc1 milestone


    Sep 4, 2023

  





  


  
    
  
  

    
  coqbot-app bot

      added a commit
      that referenced
      this issue

    
      Sep 4, 2023
    
    

      


  

    

      


  

      
        @coqbot-app
      
        @proux01
  





      

        
          Merge PR #18005: Fixes #18004: linearity check before inner disjuncti…
        

          
            
          

      


      

          

    
    
    

  

    


      


      

          

    
    

  

  

    
  



      


      
      

        
          83ffc51
        
      

    

  

    

      
…ve patterns

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

    




    

  




  


  
    
  
  

    
  Villetaneuse 

      pushed a commit
        to Villetaneuse/coq
      that referenced
      this issue

    
      Sep 9, 2023
    
    

      


  

    

      


  

      
        @herbelin
      
        @Villetaneuse
  





      

        
          Fixes coq#18004: check linearity before disjunctive patterns.
        

          
            
          

      


      

          

    
    
    

  

      


      

      


      
      

        
          45505c1
        
      

    

  

    

      
This happens to be another instance of a problem partially addressed
in coq#17854.

    




    

  













  
  

    

      

  





  




  
  

              

  
    Sign up for free
    to join this conversation on GitHub.
    Already have an account?
    Sign in to comment


  



  






  
                  




    

  


      
  

    Assignees
  



        

    No one assigned







      


  


  

    Labels
  



    

    None yet







      

  

    

        

    Projects
  


        




    None yet




  



      

  

    
  

    Milestone
  


      
    
  
    8.19+rc1
  





    
      
          


  

    
      

        
    

    Development
  




            
Successfully merging a pull request may close this issue.





    


  
          
      Fixes #18004: linearity check before inner disjunctive patterns

    
      herbelin/github-coq
    





    
  




        
      

    

  
      

  

    

      2 participants
    

    

        
          @herbelin 
        
          @doside