Jan Menz (Nov 10 2020 at 13:27): 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.
Théo Zimmermann (Nov 10 2020 at 13:32):I don't know what this error means. However, note that:
So feel free to open an issue regarding this error message, to have it documented at least, or improved (even better).
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.
Karl Palmskog (Nov 10 2020 at 13:37):see the coq bug minimizer here: https://github.com/JasonGross/coq-tools
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.
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.
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.
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.
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.
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).
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: Sep 26 2023 at 12:02 UTC