Stream: Coq Platform devs & users

Topic: Documenting Platform packages


view this post on Zulip Karl Palmskog (Apr 21 2022 at 14:40):

we should check in the survey, but unfortunately still few users depend on CoqHammer and QuickChick

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 21 2022 at 17:12):

a beginner's tutorial might be:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"?)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 22 2022 at 12:45):

Sure. Or create a new folder "tutorials" right away.

view this post on Zulip Karl Palmskog (Apr 22 2022 at 12:46):

OK, then my old regular expression matching example might work

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 22 2022 at 16:13):

I am looking forward to it.


Last updated: Jan 30 2023 at 11:03 UTC