Stream: Coq users

Topic: What does my error mean?


view this post on Zulip Jan Menz (Nov 10 2020 at 13:27):

I already asked this questions on the Coq-Club mailing list, but was told it might be a good idea to try here as well.

When changing one of my inductive definitions I get the following error
when generating an induction principle using "Combined Scheme":

Error: decompose_prod_n: not enough products

What does this error mean? According to the Index of Errors and Warnings
in the reference manual (https://coq.inria.fr/refman/coq-exnindex.html)
this error doesn't even exist.

Cheers,
Jan.

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 13:32):

I don't know what this error means. However, note that:

  1. the error message index of the reference manual is far from exhaustive
  2. when error messages are bad, we should try to improve them.

So feel free to open an issue regarding this error message, to have it documented at least, or improved (even better).

view this post on Zulip Jan Menz (Nov 10 2020 at 13:37):

Would it be fine to submit the issue even without an example? The example depends on several large files and I do not know how to reproduce the error with a smaller example yet.

view this post on Zulip Karl Palmskog (Nov 10 2020 at 13:37):

see the coq bug minimizer here: https://github.com/JasonGross/coq-tools

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 13:42):

@Jan Menz Looks like an internal issue in the tactic code generating the scheme. Maybe your inductive has a shape that is not recognized by the scheme generator.

view this post on Zulip Jan Menz (Nov 10 2020 at 13:45):

@Pierre-Marie Pédrot I would be surprised if the shape wasn't recognised at all. A different "Combined Scheme" definition using a larger subset of the mutually inductively defined propositions works just fine.

view this post on Zulip Pierre-Marie Pédrot (Nov 10 2020 at 13:48):

If you have a minimal example, as e.g. generated by the minimizer, it could be scrutinized.

view this post on Zulip Jan Menz (Nov 10 2020 at 13:50):

I'm looking at the minimizer at the moment trying to figure out how it works. It'll probably take a while. I'll probably be running into the known problem with python in Windows.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 14:18):

That's more like an anomaly actually, so indeed not an error but a bug in Coq likely.

view this post on Zulip Théo Zimmermann (Nov 10 2020 at 14:27):

Note that it is also fine to point to a large example if this is something that you have somewhere in a public branch (if you don't manage to do the minimization yourself).

view this post on Zulip Jan Menz (Nov 10 2020 at 16:00):

I wasn't able to get the minimizer to work, but I was able to minimize the example to a reasonable size by hand. I submitted the issue here: https://github.com/coq/coq/issues/13342


Last updated: Feb 06 2023 at 13:03 UTC