Bas Spitters (Aug 18 2020 at 07:20): Bas Spitters (Aug 18 2020 at 07:20):What is meant here? Pierre does not seem to be on Zulip.
https://github.com/coq-community/manifesto
Collaborative writing of documentation
We will propose a format for the documentation packages based on a preliminary work by Pierre Castéran.
Bas Spitters (Aug 18 2020 at 07:23):BTW The page also misses a comparison with the Coq platform.
Karl Palmskog (Aug 18 2020 at 08:21):you can see some stuff about the documentation here: https://github.com/coq-community/manifesto/issues/108
I agree that there should be a FAQ question+pointer to the Coq Platform, but one could also argue that not enough people even know what the platform is
Bas Spitters (Aug 18 2020 at 08:37):Is the main idea to use \href to link latex and Coq ?
Karl Palmskog (Aug 18 2020 at 08:38):maybe @Théo Zimmermann can comment on Pierre's Hydra Battles work, I have no idea what the technical ideas are
Théo Zimmermann (Aug 18 2020 at 16:07):There were no particular technical ideas. This was more a proposal of a style of documentation based on code. However, the idea is now to use @Clément Pit-Claudel's new documentation tool (Alectryon).
Théo Zimmermann (Aug 18 2020 at 16:07):Regarding an FAQ item on the platform, yes, but this should probably wait for the transfer of the coq-platform repo to the coq organization (which should be done soon).
Bas Spitters (Aug 18 2020 at 16:13):That's interesting, what would the workflow be for crowd sourcing documenting existing formalizations?
Théo Zimmermann (Aug 18 2020 at 16:21):In the case of Pierre Castéran's work, he considered from the beginning of this formalization that this was an interesting example to use as documentation. However, we can also identify some existing formalizations that have a good pedagogical potential and encourage their authors to produce documentation out of it (or find another volunteer to do it)...
Bas Spitters (Aug 18 2020 at 16:26):Most formalizations are badly documented. If we provide an easy way for people to add documentation, some people might actually do it (think wikipedia, nlab, ...), as the reviewing process will be quick.
Karl Palmskog (Aug 18 2020 at 19:24):if we want better documentation, I think we also need better automation for deploying it, see for example here: https://github.com/coq/bot/issues/85
Karl Palmskog (Aug 18 2020 at 20:21):as of recently, we seem to have four different solutions to HTML documentation: coqdoc and its variants, coq2html, Alectryon, and jsCoq. Unfortunately, I think some of them don't play that well with each other, e.g., what is supported in coqdoc is not always supported by coq2html, and some coq2html stuff is not supported by Alectryon, etc.
Karl Palmskog (Aug 18 2020 at 21:01):I did an experiment with a recent project and converted all its comments to coq2html-compatible comments: https://github.com/runtimeverification/algorand-verification/tree/master/theories
It was quite a lot of work, and both coqdoc and coq2html are fragile in how simple omissions of space affects HTML typesetting. Basically, one needs to be aware of all the quirks when doing these kinds of comment refactorings.
Li-yao (Aug 18 2020 at 21:45):I would imagine that in the near future these tools will all be merged into one, and the fragility is just a matter of properly specifying the semantics of documentation comments (the implementation will follow).
Karl Palmskog (Aug 18 2020 at 21:51):Li-yao said:
I would imagine that in the near future these tools will all be merged into one, and the fragility is just a matter of properly specifying the semantics of documentation comments (the implementation will follow).
I personally believe any merging of these tools is unlikely in the near future. For example, work on jsCoq (and by extension SerAPI) started in 2016, and only now are we seeing large-scale applications. The integration path would probably be:
and all of these would be serious engineering efforts (in particular the last one).
Karl Palmskog (Aug 18 2020 at 21:53):for coq2html integration it would probably take a diplomatic effort (and engineering) to ensure the needs of CompCert documentation are met
Karl Palmskog (Aug 18 2020 at 21:55):in terms of engineering, Alectryon is currently Python-based, which would not fly in either SerAPI or Coq
Karl Palmskog (Aug 18 2020 at 21:56):I'm not saying integration is inherently bad, just that in a setting like ours there are several factors working against it (not least that there is not a lot of "research value" here)
Li-yao (Aug 18 2020 at 22:11):Hmm, maybe integration is too much to ask for. How about a unified format then? There should be a single way to write your documentation comments and all the tools will parse the same thing. Are there conflicting interests at play there too?
Karl Palmskog (Aug 18 2020 at 22:14):coq2html and Alectryon essentially follow the coqdoc "format", but at least coq2html introduces its own extensions and variations.
Li-yao (Aug 18 2020 at 22:15):I guess I also have a hard time grasping what ideal documentation should be like in the first place...
Karl Palmskog (Aug 18 2020 at 22:17):in the ITP world, there is at least the distinction between "literate code" and "proof movies". Literate code would be SF + jsCoq or SF + regular HTML. Background of literate code: https://en.wikipedia.org/wiki/Literate_programming
Karl Palmskog (Aug 18 2020 at 22:18):proof movies would be Alectryon or Proviola, more here: https://arxiv.org/abs/1005.2672
Li-yao (Aug 18 2020 at 22:19):I could imagine every library with HTML docs; even if that's just the source code, it could benefit from cross-project hyperlinking at the very least, so you don't have to install a package and its dependencies to know what a name means.
Karl Palmskog (Aug 18 2020 at 22:21):crosslinking is possible today with coqdoc and coq2html, but since very few projects publish authoritative HTML, few use it (besides for stdlib which is done by default)
Karl Palmskog (Aug 18 2020 at 22:22):for example, a magical incantation in coq2html I used is: COQ2HTMLFLAGS = -base Algorand -external https://math-comp.github.io/htmldoc/ mathcomp, yet, this doesn't even give me the references to finmap constants, since the HTML documentation for finmap is not found at that URL
Karl Palmskog (Aug 18 2020 at 22:27):moreover, one typically wants documentation references to the exact version of the dependency used in the project. This means one needs an URL convention for different documentation versions to be adopted in big projects.
Karl Palmskog (Aug 18 2020 at 22:47):I still think the best thing we can do is to introduce coqdoc in every coq-community project, and then also make sure it's possible to add coq2html and Alectryon documentation to coq-community projects as appropriate. The file structure for the gh-pages branch (using GitHub pages for HTML deployment) I describe in https://github.com/coq/bot/issues/85 is carefully designed to support this. Nevertheless, we have already seen different conventions being adopted in various projects that can only support, say, Alectryon by reorganizing theirgh-pages branch...
Li-yao (Aug 18 2020 at 22:52):That sounds like an ambitious but well-scoped project to reach a baseline for further documentation efforts.
Paolo Giarrusso (Aug 19 2020 at 05:32):Alectryon also introduces its extensions, since it’s related to Coqrst AFAIK?
Anton Trunov (Aug 19 2020 at 10:13):Does anyone have the link to Alectryon? This one turns up when googling, but it does not work for me https://people.csail.mit.edu/cpitcla/blog/alectryon.html
Karl Palmskog (Aug 19 2020 at 10:21):@Anton Trunov you should private-Zulip-message or email its author for access, the code is under wraps for the time being
Bas Spitters (Aug 19 2020 at 10:21):@Clément Pit-Claudel Might be interested to join this discussion.
Théo Zimmermann (Aug 19 2020 at 10:21):It's not been publicly announced yet :frown: The best you can do at this point is to request access / info to @Clément Pit-Claudel by private mail.
Clément Pit-Claudel (Aug 19 2020 at 13:19):I wonder if it's OK to make the repo public as long as I don't advertise it broadly. It's under review so I'm not supposed to publicize it, and I assumed this meant not making the repo public :frowning: . @Anton Trunov I invited you to the repo.
Paolo Giarrusso (Aug 19 2020 at 13:21):@Clément Pit-Claudel depends on venue but your reading seems too strict compared to usual SIGPLAN guidelines https://icfp19.sigplan.org/track/icfp-2019-papers#a7
Paolo Giarrusso (Aug 19 2020 at 13:21):however
Paolo Giarrusso (Aug 19 2020 at 13:23):clearly allowed: public link on your homepage.
Clearly discouraged: arXiv paper (that sends notifications to subscribers, which might include reviewers)
Anton Trunov (Aug 19 2020 at 13:24):Awesome! Thanks a lot @Clément Pit-Claudel
Anton Trunov (Aug 19 2020 at 13:30):I've read README and must say that Alectryon looks absolutely amazing!
Clément Pit-Claudel (Aug 19 2020 at 13:32):Paolo Giarrusso said:
clearly allowed: public link on your homepage.
Clearly discouraged: arXiv paper (that sends notifications to subscribers, which might include reviewers)
Right, I worry a bit about the notifications that Github sends to subscribers. I think it's best to play it safe for a few weeks.
Pierre-Marie Pédrot (Aug 19 2020 at 13:33):Technically, a lot of people are reading this thread right now :/
Last updated: Jun 03 2023 at 15:31 UTC