Comments (7)
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.
from coq-tricks.
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.
from coq-tricks.
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.
from coq-tricks.
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.
from coq-tricks.
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.
from coq-tricks.
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
from coq-tricks.
About proviola, see also coq-community/manifesto#16.
from coq-tricks.
Related Issues (14)
- Arguments HOT 3
- Mention small inversions HOT 2
- Give a minimal example of using sections with some of the tricks described
- convoy pattern
- Gallina function application in Ltac
- Inaccuracy in Search explanations HOT 1
- Trick suggestion: apply tactic to all subgoals HOT 2
- Trick suggestion
- info_trivial has been fixed? HOT 1
- `dependent destruction` and `dependent induction` entry HOT 1
- Introduce categories for tricks? HOT 3
- Build process is unnecessarily complicated HOT 1
- Test against multiple Coq versions HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-tricks.