coq-tricks
coq-tricks copied to clipboard
tchajed
Integrate into the general coq-community ?
It would be great to move these tips to a more central place. @zimmi48 is doing great work organizing these things.
Sure, I'd be happy to move these to coq-community if others would find them useful. I think the best way to use these tricks is for someone reasonably familiar with Coq to read through all of them and then use the repo as a reference when the need arises (I do this, too, since I often forget the specifics of something but know I've documented it before).
Given this usage, I'm not sure where or how to give them visibility. coq-community sort of makes sense but this is really documentation, not a coq package.
It would indeed make sense to have this be part of coq-community: this could give it more visibility and possibly help get some more contributions. Collaborative writing of documentation is explicitly listed as one of the goals of coq-community. It's not just about maintaining packages.
BTW there is a section of the Coq FAQ (https://github.com/coq/coq/wiki/Talkin'-with-the-Rooster) that partially overlaps in purpose with this repo. It would be good to copy what is still worth in there and delete the page, as the structure (and CI) of the coq-tricks repository makes it a better place to ensure that the listed advice does not become obsolete.
Ah, just noticed that section in the manifesto - this repo is a perfect example.
I integrated some things in that FAQ. I think Eddie Kohler's Naive Coq tutorial from his verified systems class is a good (and more succinct) introduction to the basic Coq tactics.
I think CI is great and could be made even more useful by adding even more short code samples. I'd also really like a tool fairly similar to coqdoc which generates a single doc page from a literate Coq file and includes actual Coq output at selected points (the difference with coqdoc is that it should be documentation with several embedded Coq files, not a Coq file with embedded documentation - eg, see how the Rust book looks). Even without proof contexts that would be useful, and a good start to an "advanced Coq" book which includes larger examples.
I'd also really like a tool fairly similar to coqdoc which generates a single doc page from a literate Coq file and includes actual Coq output at selected points
How does that compare to @cpitclaudel's coqrst (i.e. what is used to display Coq snippets in the user manual, see https://github.com/coq/coq/tree/master/doc/sphinx#coq-directives)?
Note that coqrst has serious limitations compared for instance with your Rust example (see in particular coq/coq#7755).
Even without proof contexts that would be useful, and a good start to an "advanced Coq" book which includes larger examples.
Unfortunately, coqrst does not seem adequate for larger examples spanning over multiple Coq files. I don't see yet what is the good middle ground between coqrst and coqdoc for this kind of work.
Yeah, looks like I could use coqrst with a reset directive after every example, generating a page just like the Coq reference manual. I'll give that a try at some point.
There is also proviola, which may not be what you want, but let's you display the Coq state on hover. See the HoTT wiki for an example: http://hott.github.io/HoTT/proviola-html/HoTT.Fibrations.html
About proviola, see also https://github.com/coq-community/manifesto/issues/16.