Hi,
I am experiencing the following error with Coq 8.19 + coq-ext lib + coq-equations.
The no so minimum reproducer is available here https://gist.github.com/jjhugues/6747d65e38a99ed85db35ad4565b0fe6
Error: Anomaly
"File "kernel/cClosure.ml", line 134, characters 26-32: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
This code is reduced from https://github.com/ConorReynolds/coq-institutions, it embeds the minimum set of definitions that trigger the issue.
Since the offending code is a coq kernel error, and also involves coq equation, I wonder where to submit it. Should it be a coq issue or a coq-equations one?
I would prefer to submit a smaller reproducer, yet I do not know how to start.
Thanks for your guidance.
based on seeing many earlier issues of a similar flavor, it's very likely this is caused by Equations, e.g., by some bug in Equations. You may want to report a minimized example as an issue, or look if someone has already reported: https://github.com/mattam82/Coq-Equations/issues
arguably the "standard approach" to obtaining minimized examples is using coq-bug-minimizer
Last updated: Oct 13 2024 at 01:02 UTC