Stream: Coq users

Topic: Coq 8.19 -- assert failure in "kernel/cClosure.ml"


view this post on Zulip Jerome Hugues (Feb 21 2024 at 23:41):

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.

view this post on Zulip Karl Palmskog (Feb 22 2024 at 08:25):

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

view this post on Zulip Karl Palmskog (Feb 22 2024 at 08:37):

arguably the "standard approach" to obtaining minimized examples is using coq-bug-minimizer


Last updated: Jun 13 2024 at 19:02 UTC