Stream: Coq users

Topic: Minimal working examples of Coq code


view this post on Zulip Karl Palmskog (Oct 03 2023 at 14:00):

https://proofassistants.stackexchange.com/questions/2481/how-do-i-write-a-minimal-working-example-mwe-in-coq-to-demonstrate-some-proble

To get help with some incomplete proof script or definition in Coq, or demonstrate some failing (e.g., Ltac) tactic or command, I am often asked to write a minimal working example (MWE) of Coq vernacular code. That is, I am asked to write, in as few and self-contained Coq sentences as possible, code that when executed by Coq leads to the error message I am seeing, such as a type inference failure.

How should I produce my MWE when the actual sentence that fails is in the middle of many lines of other Coq code? Specifically, is there any methodology or tools I can use to extract (and possibly generalize) the code leading up to the failure?

Any takers to write some initial answer(s)? Here are some directions:

view this post on Zulip Notification Bot (Oct 03 2023 at 14:11):

This topic was moved here from #Coq devs & plugin devs > Minimal working examples of Coq code by Karl Palmskog.

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 16:27):

I like the idea, but are those tools beginner-friendly enough? Adding them to the platform seems necessary, not sure if sufficient

view this post on Zulip Karl Palmskog (Oct 03 2023 at 17:02):

coq-dpdgraph and its tools are already part of the Platform

view this post on Zulip Karl Palmskog (Oct 03 2023 at 17:02):

but indeed, it would probably be best to divide up answer into basic and advanced techniques (which include bug minimizer), I may do this as a self-answer

view this post on Zulip Karl Palmskog (Oct 03 2023 at 18:29):

they apparently did a small writeup for Lean, but very basic in my view: https://leanprover-community.github.io/mwe.html

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 19:13):

That's very interesting idea! I think we have some stuff in place to actually help the users to get to these examples, in Haifa I did talk a bit to @Jason Gross about integration of the minimizer with Flèche / coq-lsp.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 19:14):

If someone would like to do this kind of project I'd be happy to help, and have a few tools already in place.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 19:15):

The way I see things now is that using the programmable error recovery of Flèche + some slicing tool, we can try to understand how to build such examples with incremental checking that works, so things are actually fast (and more steps are sound thus cutting the search tree)

view this post on Zulip Karl Palmskog (Oct 03 2023 at 19:15):

for beginners to be able to use the bug minimizer, at minimum it'd have to be packaged, e.g., to be installable via Python's pip

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 19:16):

Yes, that'd be great

view this post on Zulip Jason Gross (Oct 03 2023 at 22:52):

Please make an issue on coq-tools to release the minimizer on pip, I'll see what I can do to get it on there when I find time

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 23:03):

Done, does this help? https://github.com/JasonGross/coq-tools/issues/165

view this post on Zulip Jason Gross (Oct 04 2023 at 05:19):

Yes, thank you

view this post on Zulip Jason Gross (Oct 21 2023 at 06:39):

There's now a pip / PyPi package: https://pypi.org/project/coq-tools/

view this post on Zulip Karl Palmskog (Oct 21 2023 at 07:35):

great, I'll try to highlight this when writing self-answer to the StackExchange question


Last updated: Jun 23 2024 at 03:02 UTC