Stream: Coq users

Topic: Minimal working examples of Coq code

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:

• aim to provide a vernacular file f.v that can be run with only coqc, as in coqc f.v
  • remove any unecessary require-imports from the file, inline any necessary local dependent code
  • try to require only Stdlib and other big libraries from the Coq Platform
• use coq-dpdgraph to visualize transitive dependencies (Coq constants) for some particular definition or theorem
• if there is a Coq error message use the Coq Bug minimizer on the file with the error to remove unnecessary code in the original file

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.

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

Karl Palmskog (Oct 03 2023 at 17:02):

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

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

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

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.

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.

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)

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

Emilio Jesús Gallego Arias (Oct 03 2023 at 19:16):

Yes, that'd be great

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

Paolo Giarrusso (Oct 03 2023 at 23:03):

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

Jason Gross (Oct 04 2023 at 05:19):

Yes, thank you

Jason Gross (Oct 21 2023 at 06:39):

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

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: Oct 13 2024 at 01:02 UTC