File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed.

[satnam6502]

Description of the problem

I get the following error message:

"File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed."

I suspect I have done something wrong :-(

Repo:

$ git clone https://github.com/satnam6502/oak-hardware
$ git checkout 38971a7d0f8aa04b6fa4e21d1dfda3990ecf2c66
$ cd oak-hardware/cava/cava
$ make coq
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQDEP VFILES
*** Warning: in file Cava/Arrow/Instances/Netlist.v,
    required library Netlist matches several files in path
    (found Netlist.v in Cava/Arrow/Instances and Cava; used the latter)
COQC Cava/BitArithmetic.v
COQC Cava/Signal.v
COQC Cava/Types.v
COQC Cava/Netlist.v
COQC Cava/Monad/Cava.v
COQC Cava/Monad/Combinators.v
COQC Cava/Monad/UnsignedAdders.v
COQC Cava/Monad/XilinxAdder.v
COQC Cava/Arrow/Arrow.v
COQC Cava/Arrow/Instances/Constructive.v
COQC Cava/Arrow/Instances/Combinational.v
COQC Cava/Arrow/Instances/Netlist.v
File "./Cava/Arrow/Instances/Netlist.v", line 111, characters 2-1820:
Error:
Anomaly
"File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Coq Version

$ coqtop -v
The Coq Proof Assistant, version 8.11.0 (January 2020)
compiled on Jan 27 2020 17:46:49 with OCaml 4.09.0

[ejgallego]

Sorry I was not careful about testing this bug, I tested the wrong commit.

I did reproduce on master:

File "./Cava/Arrow/Instances/Netlist.v", line 111, characters 2-1820:
Error:
Anomaly
"File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at file "pretyping/cases.ml", line 1719, characters 29-41
Called from file "pretyping/cases.ml", line 1756, characters 12-36
Called from file "pretyping/cases.ml", line 1772, characters 23-79
Called from file "pretyping/cases.ml", line 1270, characters 17-79
Called from file "pretyping/cases.ml", line 1472, characters 19-35
Called from file "pretyping/cases.ml", line 1901, characters 17-47
Called from file "pretyping/cases.ml", line 2070, characters 27-89
Called from file "pretyping/cases.ml", line 2666, characters 14-105
Called from file "pretyping/pretyping.ml", line 932, characters 20-87
Called from file "pretyping/pretyping.ml" (inlined), line 779, characters 36-103
Called from file "pretyping/pretyping.ml", line 860, characters 14-39
Called from file "pretyping/pretyping.ml", line 883, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 779, characters 36-103
Called from file "pretyping/pretyping.ml", line 860, characters 14-39
Called from file "pretyping/pretyping.ml", line 883, characters 50-94
Called from file "pretyping/pretyping.ml", line 932, characters 20-87
Called from file "pretyping/pretyping.ml", line 932, characters 20-87
Called from file "pretyping/pretyping.ml", line 932, characters 20-87
Called from file "pretyping/pretyping.ml" (inlined), line 1288, characters 2-81
Called from file "pretyping/pretyping.ml", line 1309, characters 21-85
Called from file "pretyping/pretyping.ml", line 1354, characters 20-71
Called from file "vernac/classes.ml", line 290, characters 26-91
Called from file "vernac/classes.ml", line 443, characters 6-102
Called from file "vernac/classes.ml", line 450, characters 23-93
Called from file "vernac/classes.ml", line 485, characters 4-76
Called from file "vernac/classes.ml", line 578, characters 2-98
Called from file "vernac/vernacentries.ml", line 1160, characters 4-59
Called from file "vernac/vernacinterp.ml", line 28, characters 19-23
Called from file "vernac/vernacinterp.ml", line 210, characters 20-60
Called from file "lib/flags.ml", line 17, characters 14-17
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "vernac/vernacinterp.ml", line 253, characters 18-43
Called from file "vernac/vernacinterp.ml", line 251, characters 6-279
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "stm/stm.ml", line 2428, characters 16-43
Called from file "stm/stm.ml", line 1006, characters 6-10
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "stm/stm.ml", line 2569, characters 4-105
Called from file "stm/stm.ml", line 2750, characters 4-60
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "lib/flags.ml", line 17, characters 14-17
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "toplevel/vernac.ml", line 111, characters 8-69
Called from file "toplevel/vernac.ml", line 115, characters 6-19
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "toplevel/vernac.ml", line 171, characters 30-88
Called from file "toplevel/ccompile.ml", line 148, characters 18-89
Called from file "toplevel/ccompile.ml", line 214, characters 2-39
Called from file "list.ml", line 106, characters 12-15
Called from file "toplevel/coqc.ml", line 45, characters 2-81
Called from file "toplevel/coqc.ml", line 67, characters 4-25

[satnam6502]

I am sure this is the result of me doing something wrong and when I finish the refactor correctly the crash goes away, but I thought I would report it anyway in case it is useful for you.

[satnam6502]

Oh, and thank you. I will switch to using master!

[JasonGross]

Assertion failures are always bugs in Coq, even if you're code is not supposed to work anyway. Thank you for reporting.

[ejgallego]

Indeed, sorry for the false lead @satnam6502 ; I tested the wrong commit, this is a bug, and still present on master so you may not get any benefit from upgrading.

[herbelin]

Fixed in #12422. Thanks for reporting.