Karl Palmskog (Apr 21 2022 at 14:40): Karl Palmskog (Apr 21 2022 at 14:40):we should check in the survey, but unfortunately still few users depend on CoqHammer and QuickChick
Karl Palmskog (Apr 21 2022 at 14:43):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
Karl Palmskog (Apr 21 2022 at 14:44):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
Michael Soegtrop (Apr 21 2022 at 14:59):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.
Michael Soegtrop (Apr 21 2022 at 15:00):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.
Théo Zimmermann (Apr 21 2022 at 15:01):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.
Michael Soegtrop (Apr 21 2022 at 16:30):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.
Théo Zimmermann (Apr 21 2022 at 16:31):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.
Théo Zimmermann (Apr 21 2022 at 16:31):Then we would put the videos on YouTube and this would provide introductions for these packages.
Notification Bot (Apr 21 2022 at 16:33):This topic was moved here from #Coq devs & plugin devs > Documenting Platform packages by Théo Zimmermann.
Michael Soegtrop (Apr 21 2022 at 16:36):It is quite a bit of work to produce good tutorial videos - many are unedited and stretch the users patience quite a bit
Karl Palmskog (Apr 21 2022 at 17:12):a beginner's tutorial might be:
Karl Palmskog (Apr 21 2022 at 17:13):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
Karl Palmskog (Apr 21 2022 at 20:05):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.
Michael Soegtrop (Apr 22 2022 at 10:50):I could do a QuickChick demo, but not now (moving homes for a few months). But I guess this is not that urgent.
Karl Palmskog (Apr 22 2022 at 10:53):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"?)
Karl Palmskog (Apr 22 2022 at 10:54):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
Michael Soegtrop (Apr 22 2022 at 12:03):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 tutorials and/or 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.
Karl Palmskog (Apr 22 2022 at 12:05):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?
Michael Soegtrop (Apr 22 2022 at 12:45):Sure. Or create a new folder "tutorials" right away.
Karl Palmskog (Apr 22 2022 at 12:46):OK, then my old regular expression matching example might work
Karl Palmskog (Apr 22 2022 at 12:47):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
Michael Soegtrop (Apr 22 2022 at 16:13):I am looking forward to it.
Last updated: Jun 03 2023 at 04:30 UTC