Karl Palmskog (Aug 05 2020 at 10:13): Karl Palmskog (Aug 05 2020 at 10:13):As it turns out, Xavier's coq2html program (https://github.com/xavierleroy/coq2html) is currently the only standalone way to get HTML documentation for Coq files with foldable proofs (by default, coqdoc writes them out fully or removes them completely). By standalone, I mean it doesn't require any fiddling with custom JavaScript, but provides all HTML+CSS+etc. in one command invocation. @Michael Soegtrop how do you feel about including tools like this in the platform?
Karl Palmskog (Aug 05 2020 at 10:14):(My view is that foldable proofs are essential for documenting large-scale projects in a reasonable way, see e.g., https://cozy.ece.utexas.edu/~palmskog/coq2html/Algorand.algorand_model.html)
Karl Palmskog (Aug 05 2020 at 10:17):would also be interested in general opinion of @Théo Zimmermann for platform + similar tools
Théo Zimmermann (Aug 05 2020 at 10:17):Tools are definitely welcome as part of the platform.
Théo Zimmermann (Aug 05 2020 at 10:21):Why not include coq2html indeed? But another tool exists already that gives you HTML documents with foldable proofs (without even relying on Javascript). It just hasn't been publicly announced yet (cf. https://coq.discourse.group/t/plv-has-a-new-blog/925 for a trailer) and cc @Clément Pit-Claudel.
Bas Spitters (Aug 05 2020 at 10:21):@Karl Palmskog We use proviola and jscoq for the HoTT library. How do they compare to coq2html ?
https://github.com/HoTT/HoTT/wiki
Karl Palmskog (Aug 05 2020 at 10:23):@Bas Spitters to my knowledge, Proviola doesn't provide foldable proofs, but it does provide "reanimation" of proofs, which is a unique functionality. So I would consider it to be somewhat orthogonal to coq2html for this reason
Bas Spitters (Aug 05 2020 at 10:24):So, do we add proviola to platform too? @Théo Zimmermann ?
Karl Palmskog (Aug 05 2020 at 10:24):jsCoq would be nice, but I have no idea of how it can/should be packaged. To my knowledge, there is as yet no workflow ordinary mortals can use to produce the static files required.
Karl Palmskog (Aug 05 2020 at 10:25):@Bas Spitters I can open issues for both coq2html and Proviola and we can take it from there. But in my view Proviola is in need of consolidation/maintenance, e.g., I don't even know if the coq-community repo version is the one you use in HoTT.
Bas Spitters (Aug 05 2020 at 10:25):@Emilio Jesús Gallego Arias knows about jscoq
Théo Zimmermann (Aug 05 2020 at 10:26):Bas Spitters said:
So, do we add proviola to platform too? Théo Zimmermann ?
Not if we don't have clear maintenance plans for it. Proviola has been migrated to coq-community with @Jason Gross as a maintainer, but it was done mostly because the repository was about to disappear, and its maintenance status is still unclear.
Karl Palmskog (Aug 05 2020 at 10:28):one strong point of coq2html in my mind is its packagability, it's just one ordinary executable that can be compiled by the OCaml compiler. I think this matters a lot to the platform.
Théo Zimmermann (Aug 05 2020 at 10:28):I don't quite get the point of adding jscoq to the platform though. jscoq is mainly useful as a way to avoid installing Coq. In fact, I would say jscoq being a Coq distribution, its maintainers could decide to bundle the Coq platform with it (the other way around thus).
Bas Spitters (Aug 05 2020 at 10:29):It comes from @Jason Gross ' github. It would be good to move it to a more standard place.
https://github.com/HoTT/HoTT/blob/master/etc/ci/install_proviola.sh
@Ali Caglayan has been working on the HoTT installation. Moving things to platform will certainly facilitate his work.
Karl Palmskog (Aug 05 2020 at 10:30):how I could see it work for platform bundling is if the jsCoq maintainers made something like an executable jscoqify that produced a set of static files to run a Coq development via a browser. This would be useful for teaching and presenting Coq code.
Karl Palmskog (Aug 05 2020 at 10:33):Bas Spitters said:
It comes from Jason Gross ' github. It would be good to move it to a more standard place.
https://github.com/HoTT/HoTT/blob/master/etc/ci/install_proviola.sh
Ali Caglayan has been working on the HoTT installation. Moving things to platform will certainly facilitate his work.
I don't think the platform inclusion in itself would facilitate this. What you (the HoTT team) could do to set Proviola on a path to platform inclusion is to propose a plan for consolidating different versions and maintaining it (actively) long term.
Bas Spitters (Aug 05 2020 at 10:59):Not sure why HoTT doesn't use proviola from the coq-community.
@Jason Gross do you want to open an issue on platform to have proviola included.
https://github.com/coq-community/proviola
Théo Zimmermann (Aug 05 2020 at 11:13):Probably because the move of the repository to coq-community is still very recent and despite @Jason Gross being its official maintainer, his patches to proviola have not yet been applied to this repository.
Clément Pit-Claudel (Aug 05 2020 at 16:22):Karl Palmskog said:
how I could see it work for platform bundling is if the jsCoq maintainers made something like an executable
jscoqifythat produced a set of static files to run a Coq development via a browser. This would be useful for teaching and presenting Coq code.
Ideally I think this should be a JavaScript program on top of coqdoc; you would include one line in the HTML generated by coqdoc and it would load a script that can parse the page and set up jscoq.
Clément Pit-Claudel (Aug 05 2020 at 16:31):Théo Zimmermann said:
But another tool exists already that gives you HTML documents with foldable proofs (without even relying on Javascript). It just hasn't been publicly announced yet (cf. https://coq.discourse.group/t/plv-has-a-new-blog/925 for a trailer) and cc Clément Pit-Claudel.
I think it depends on what is meant by foldable proofs (my tool doesn't let you hide the stuff between Proof and Qed, though it'd be easy to add if it's something people care a lot about; is it?).
The stuff I built is closer to proviola; you can see a demo of it on Flocq to get a sense of what it does: https://people.csail.mit.edu/cpitcla/alectryon/flocq/Core/Ulp.html . It's built on top of SerAPI, which doesn't currently support -indices-matter, but I opened a feature request on the SerAPI repo just now.
Bas Spitters (Aug 05 2020 at 16:41):@Clément Pit-Claudel That looks very nice. If folding and indeces-matter are included, I think it subsumes proviola.
Clément Pit-Claudel (Aug 05 2020 at 16:51):I think it needs hyperlinking as well to be a complete replacement; Alectryon (my tool) will need a bit of help from SerAPI for that too, but it's in the works (https://github.com/ejgallego/coq-serapi/issues/217).
Clément Pit-Claudel (Aug 05 2020 at 16:52):Does coq2html do something smart to find foldable sections, or does it just look for Proof … Qed/Defined/Admitted?
Karl Palmskog (Aug 05 2020 at 17:10):coq2html does very simple things for folding proofs like looking for Proof.
Karl Palmskog (Aug 05 2020 at 17:12):Clément Pit-Claudel said:
Ideally I think this should be a JavaScript program on top of coqdoc; you would include one line in the HTML generated by coqdoc and it would load a script that can parse the page and set up jscoq.
But in this case, don't you have to bundle NodeJS or something similar in the Coq Platform? The platform can't generally assume users have a CLI-level JavaScript engine installed. Or do you mean "program" in the sense of something executed by the browser? In any case, there are other things that need setting up like copying .vo files to the right location.
Clément Pit-Claudel (Aug 05 2020 at 19:49):Karl Palmskog said:
But in this case, don't you have to bundle NodeJS or something similar in the Coq Platform? The platform can't generally assume users have a CLI-level JavaScript engine installed. Or do you mean "program" in the sense of something executed by the browser?
I meant something run by the browser, not a server-side program written in Javascript ( :fear:). It would work the same way that MathJax or other enhancement plugins work.
Karl Palmskog said:
In any case, there are other things that need setting up like copying
.vofiles to the right location.
Yup, definitely.
Last updated: Jun 03 2023 at 05:01 UTC