A Compilation of Short Interactive Tutorials and How-To Guides for Coq #91
Conversation
text/XXX-A-Compilation-of-Short-Interactive-Tutorials-and-How-To-Guides-for-Coq.md
Outdated
Show resolved
Hide resolved
| ### 3.2 Horizontal Documentation | ||
| Such a documentation has by nature the potential to be horizontal as most pairs of tutorials have no reason to be linked. Ensuring it by design is very important for the documentation to be accessible, and will allow by nature differentiated learning. |
There was a problem hiding this comment.
I'm not entirely sure what you mean by "horizontal documentation". Could you explain this?
There was a problem hiding this comment.
It is not an exactly defined concept but it is to think in opposition to books that read often cover to cover, or by chapter. Here, on average, you should have as very little dependencies. Typically, there is no reason why the tutorials Search / Equations basics / Lia should be linked. Quite the opposite, you should be able to read them independently
|
|
||
| Each core functionality and plugin of Coq and the Coq Platform should have (short) pedagogical tutorials and/or how-to guides demonstrating how to use the functionality, with practical examples. Tutorials and how-to guides serve different purposes and are complementary: tutorials guide a user to discover a specific feature like "Notations in Coq", by going through predetermined examples, and introducing notions gradually, whereas how-to guides are use-case-oriented and use examples to show what to do in front of a specific problem (and possibly the various alternatives to address it). See https://diataxis.fr/ for a reference definition of tutorial vs how-to guide (in particular, https://diataxis.fr/tutorials-how-to/ for a comparison). | ||
|
|
||
| Compared to the reference manual, such a documentation is not meant to be complete or going into low level details. It is meant to be pedagogical and action-oriented, so that it enables users to learn how to use new features autonomously and horizontally : these tutorials and how-to guides should be as self-contained as possible to have only a short (if any) list of prerequisites. Moreover, by being horizontal, such a documentation could provide different tutorials (for some specific features) to cover the needs of users with different backgrounds. |
There was a problem hiding this comment.
Will tutorials identify their prerequisites, perhaps linking to them through hyperlinks?
"as self-contained as possible" - I wonder how this will work in practice. It doesn't make sense to repeat the same basic information about Coq in multiple tutorials. Some tutorials should be read before others. For example, repeating the basics of the proof context would make for a lot more writing. Repeated info would be boring to read (or skip over) after the first encounter.
There was a problem hiding this comment.
Will tutorials identify their prerequisites, perhaps linking to them through hyperlinks?
Clearly, for the moment we only have a prototype
There was a problem hiding this comment.
Some tutorials should be read before others.
Off course, and it is the case for Equations. Simply, you should not hesitate to recall a concept in 20 lines if it avoid having to read a 1000 lines tutorial.
Typically, I have read papers with bad practices, e.g. "it is not possible cf [32]" so you spend 3h looking for it, and in the end the answer is one line, so then please write "it is not possible because constructors do not preserve variables [32]" .
That is basically the idea.
|
|
||
|
|
||
| ### 2.2 Why it is important | ||
| Not having a central collection of short and action-oriented documentation pieces is a real obstacle to getting more users outside of expert academic fields, and for Coq's popularity. |
There was a problem hiding this comment.
What do you mean by "short"? A page? 3, 5, 10 pages?
There was a problem hiding this comment.
Fixing an exact length would not be useful because it really depends on the topic and on the density of the content. Yet, for indication, so far, we have kept all tutorials below 1000 lines in the file and that seems reasonable.
But to me, a better way to decide is to:
- Check the structure of the content. If it starts branching out in different directions,
- Also when the writer or the reviewer have trouble getting around the code and the concepts
Then it's a good indication it is too long / should be divided.
| Not having a central collection of short and action-oriented documentation pieces is a real obstacle to getting more users outside of expert academic fields, and for Coq's popularity. | ||
|
|
||
| #### Accessibility | ||
| Having an easy to access documentation is of utmost importance to engage new users, and keep current users. Although it does work for some experts, we cannot expect from all potential new users to have to dig through a (possibly outdated) 600 pages book, or the reference manual to learn how to use a particular feature that appeals to them. Most particularly as these sources may not contain the basic answers they are looking for due to their nature. Similarly, having to say "try to look in the GitHub repository of the package, there might be some documentation there" is not possible if we wish for our software to be usable by all. Practical and pedagogical information must be easily accessible through a **nice** centralized online interface. This is especially true, at a time when new proof assistants emerge and attract new users outside computer science research. |
There was a problem hiding this comment.
IMO the issue is more that the reference manual is woefully incomplete. It's often necessary to do a lot of experimentation and sometimes look at the source code to figure out how some feature works. I'm very used to digging through reference manuals--most software packages don't have anything beyond a reference manual (of varying quality).
There was a problem hiding this comment.
It is true that the reference manual is not complete, but it is different questions. As discussed, this are different forms of documentation that address different users: the reference manual is how it works / this project is how to use in practice. Both are complementary. Actually, this project will also be an opportunity to complete the refman when we notice it misses stuffs.
| Having an easy to access documentation is of utmost importance to engage new users, and keep current users. Although it does work for some experts, we cannot expect from all potential new users to have to dig through a (possibly outdated) 600 pages book, or the reference manual to learn how to use a particular feature that appeals to them. Most particularly as these sources may not contain the basic answers they are looking for due to their nature. Similarly, having to say "try to look in the GitHub repository of the package, there might be some documentation there" is not possible if we wish for our software to be usable by all. Practical and pedagogical information must be easily accessible through a **nice** centralized online interface. This is especially true, at a time when new proof assistants emerge and attract new users outside computer science research. | ||
|
|
||
| #### A documentation focused on practical usages | ||
| Furthermore, not having such a documentation prevents people from actually learning by themselves, and discovering new amazing features of Coq that rival proof assistants may not have, as well as the richness of our ecosystem. While a lot of progress has been made on the ecosystem side with pages like [Awesome Coq](https://github.com/coq-community/awesome-coq) and the Coq Platform, there is still work to be done for the documentation that is hard to access. Many amazing features are still currently under-documented, and the existing documentation is often scattered out in the reference manual, books, or individual GitHub repositories, making it difficult to access. A symptom of that is the trouble that students are currently facing to discover new functionalities by themselves, compared to other software. In particular, in our experience, it is quite common that users (have to) rely on expert users they know to learn Coq. |
There was a problem hiding this comment.
Useful information is scattered across many places in a variety of formats. It would be very helpful to have a comprehensive detailed index in one place.
There was a problem hiding this comment.
They already are some resources like Coq Tricks / Awsome Coq but it is by nature incomplete and the content is always what you want.
Moreover, it is a bit of a weak implementation because:
- it is scattered across many websites, which are more or less stable (there is important turn over)
- more or less updated
- it creates duplication of effort as people can't check it all out
There is a reason we have a refman. Here it is the same but just for a different kind of documentation. Information should be centralized, updated, easy to access and people can easily contribute if stuffs are missing.
| Even for fluent Coq users, it can be challenging to keep up to date with the many recent interesting developments inside Coq (template polymorphism, universe polymorphism, SProp, Ltac2, ...) or around Coq (coq-elpi, metacoq, hierarchy builder, ...) | ||
|
|
||
| Also, many users are currently unaware of the extent of what has been formalized and is available in Coq. There are many libraries, and it is not easy to know which library to use, or to know on which axioms they rely or their compatibilities. | ||
| This is obviously not just a documentation issue, but having a clear documentation of what we have and where would help. |
| - As mentioned in section 4.3, there is real work to be done on the interface side. | ||
| - There is a need for someone interacting with the community, reviewing etc. | ||
|
|
||
| Thomas Lamiaux should be employed part-time on this project as a 3 years expertise mission included in his PhD. His task should be developing the project, writing and reviewing tutorials, and interacting with the community, ensuring at least some people-power in the beginning of this project. |
There was a problem hiding this comment.
Is this effort an integral part of your PhD work? If so, what is your planned PhD work (just curious).
There was a problem hiding this comment.
It is not, feel free to check my webpage
|
|
||
| ### 3.3 Online interface | ||
|
|
||
| The documentation would be interactive and available online, in a format more or less similar to [Pierre Rousselin's class](https://www.math.univ-paris13.fr/~rousselin/ipf/2023/RInegalit%C3%A9s_sujet.html). |
There was a problem hiding this comment.
I don't see how the linked webpage is interactive.
Making interactive pages such as for the Natural Number Game above seems like a lot more work than just writing a non-interactive tutorial. What are the relative priorities of interactive and non-interactive tutorials?
There was a problem hiding this comment.
You have to click on the JsCoq button on the right of your screen and enable JavaScript
| Other tutorials will have to be written from scratch. We will organise directed calls for contributions to avoid having multiple overlapping / rival tutorials. | ||
| Among other possibilities, we will be in touch with plugins designers and expert users for the tutorials and how-to guides of their plugins. | ||
|
|
||
| As a base to work on, we suggest an [informal list](https://github.com/Zimmi48/platform-docs/blob/main/draft_structure_doc.md) of tutorials and how-to guides that we could have. This list has been established through informal discussions. It will necessarily evolve with the projects, contributions and user feedback. We further plan to go to CUDW and other similar events to discuss the project and the needs of the community. |
There was a problem hiding this comment.
That's quite a long laundry list. It would be interesting to identify the highest priority tutorials that you or others plan to work on first.
There was a problem hiding this comment.
The list is mostly there to give an idea of what is possible to people that would like to contribute. The ecosystem is vast: people have different priority and strengths, so I don't think it is important to fix priorities. I would rather have people having fun contribute on what they want.
This being said, my personal proprieties is to finish tutorials for Equations and then to tackle Ltac2 as I am interested in both, I am in close contact with developers of both, and that is a recurrent request.
There was a problem hiding this comment.
For priorities, I mean identifying what will provide the greatest benefit to users. That may usefully influence volunteers, but of course each makes their own choices.
There was a problem hiding this comment.
I guess we can but also it is hard to say what are the priorities. There is a wishlist on zulip. I guess we'll see what people want as we go.
| We already have some technical answers: | ||
| - [Alectryon](https://github.com/cpitclaudel/alectryon) provides means to interpret restructured text inside Coq files (and conversely). | ||
| - `jsCoq` and `waCoq` enable Coq to be executed inside a web browser, so there is a priori no insurmountable difficulty there. | ||
|
|
||
| Yet, it will require some real technical work: | ||
| - waCoq or jsCoq need to evolve to more recent versions of Coq and their usage with external libraries needs to be smoother, | ||
| - we have not tested yet how to use Alectryon and jsCoq/waCoq together. |
There was a problem hiding this comment.
Will tutorial writing commence immediately or are these technical changes a necessary prerequisite? Are they somewhat independent tasks?
Do you plan to use any of the Sphinx infrastructure used to generate the reference manual? It would be good if you could build on that rather than inventing yet another documentation format.
There was a problem hiding this comment.
Alextryon should be able to convert coqdoc automatically to ReStructured text, should it be retrocompatible. The rest is just UI so it does not matter and we can progress on it independently from the rest.
For Sphinx, maybe @Zimmi48 has an idea ?
| @@ -0,0 +1,257 @@ | |||
| - Title: A Compilation of Short Interactive Tutorials and How-To Guides for Coq | |||
There was a problem hiding this comment.
You may want to change "XXX" in the filename to the CEP number. I believe that is a convention.
There was a problem hiding this comment.
In the PR they are many conventions used about that
|
BTW, it would be nice to split the long lines of the text to, say, a max of 80 chars. |
|
I agree, I do not know why the file got refactored like that |
|
@thomas-lamiaux @Zimmi48 I think you should add a separate subsection on facilitating outside contributions and incentivizing contributors (besides the main maintainers). For example, regular Coq users should be able and recommended to:
In return, they could be credited on the Coq website and have their names listed in tutorials, like in SF. |
|
As discussed on Zulip, you may want to consider widening the scope a bit to include longer-form tutorials like the "proof pearls" that are invited for submission at the annual ITP conference:
As an example, consider Laurent Thery's 2x2x2 Rubik's cube pearl. This is a ten-page paper accompanied by a Coq code repository. In contrast to short tutorials, these proof pearls fall more into the "explanation" quadrant of Diataxis. |
Hi, it took a lot of effort to write, hope you think it is good.
Rendered