we should check in the survey, but unfortunately still few users depend on CoqHammer and QuickChick
for overall Coq productivity and advertising reasons, would be great if we had tons of users of complex proof automation stuff, but I worry the support burden could be heavy
for some, I think Equations could be the "killer app" rather than hammer/chick, but I think there is already a support burden there: https://github.com/mattam82/Coq-Equations/issues
I think Quickchick is a bit special - one doesn't really depend on it in the sense that a development would break down if one wouldn't have it. But I use it quite regularly to check if tricky lemmas are likely true before I try to prove them. This has been a big help recently and it is quite smooth. I just have quick chick wrappers for my stuff and I do these "is this provable" queries right in these wrappers.
Coq hammer I didn't use in production stuff as yet. I guess most of the numerics stuff I am doing is too tricky for an ATP.
I think we need Platform tutorials, i.e., tutorials that would exercise several Platform projects (and maybe centralized documentation as well) and this would really help making Platform packages more widely used.
I thought about something like a Coq Platform magazine, maybe bi monthly, which highlights one or two packages and gives a few examples. One could also make good content from certain zulip discussions.
We could also revive our idea of regular Coq webinars and target specifically at promoting the Coq Platform by inviting Coq Platform package maintainers and users.
Then we would put the videos on YouTube and this would provide introductions for these packages.
This topic was moved here from #Coq devs & plugin devs > Documenting Platform packages by Théo Zimmermann.
It is quite a bit of work to produce good tutorial videos - many are unedited and stretch the users patience quite a bit
a beginner's tutorial might be:
I would personally like to see a "power user MathComp tutorial", that blitzes from Hierarchy Builder canonical structures to algebra tactics/mathcomp-zify, CoqEAL and perhaps even mathcomp-analysis
I can probably write a script and source files for the beginner one, if we keep it short (5 min?), using examples I've accumulated. Not much experience with QuickChick though.
I could do a QuickChick demo, but not now (moving homes for a few months). But I guess this is not that urgent.
if we do some example code that could be used in a tutorial, should/could it be hosted in the Platform repo? (Something like a "smoke integration test"?)
as we have discussed with Lean community members, there is a difference between "integrated" and "integrated with itself", i.e., some packages do not play well with each other out of the box, or they can break over time
There is already the (https://github.com/coq/platform/tree/main/test_files) where I put in test files, e.g. for coq-hammer test files which test specific ATPs.
I think it would also make sense to have an
examples folder which contains the main example for each package, but for licensing reasons I would create such a folder on the fly as I do for the smoke test.
so if I have good tutorial code that spans multiple packages, I can submit that as a PR? And you decide where to put it on-the-fly?
Sure. Or create a new folder "tutorials" right away.
OK, then my old regular expression matching example might work
arguably regexps are the most computer sciency structure there is - they have some metatheory with nontrivial induction/recursion, and you can actually compute something in the end
I am looking forward to it.
Last updated: Feb 22 2024 at 04:02 UTC