Stream: coq-community devs & users

Topic: Alectryon

Bas Spitters (Apr 27 2022 at 12:25):

The HoTT library provides nice documentation using alectryon.
https://github.com/HoTT/HoTT/wiki#an-interactive-reference-manual-autogenerated-by-alectryon
It's also integrated into the CI. I imagine most of this is canonical and can be included in the CI templates for other projects.
Did anyone look at the obstacles for doing this already?

Karl Palmskog (Apr 27 2022 at 12:37):

the main drawback with Alectryon currently is the lack of crossreferences and no automatic generation of table of contents.

I think multiple people have set up Alectryon generation boilerplate, here is the one I use: https://github.com/runtimeverification/vlsm/blob/master/Makefile.coq.local#L37-L48

Karl Palmskog (Apr 27 2022 at 12:49):

Alectryon is not currently part of the Docker Coq images, but most of its dependencies like SerAPI are. So it should be simple and fast to build Alectryon documentation using Docker-Coq-Action directly instead of the custom CI HoTT uses

Karl Palmskog (Apr 27 2022 at 12:50):

my suggestion is to adapt something like this: https://github.com/coq-community/aac-tactics/blob/master/.github/workflows/deploy-coqdoc.yml

Bas Spitters (Apr 29 2022 at 11:30):

Thanks! In fact, I found out that coqdocjs is probably easier for our particular use case.

Karl Palmskog (Apr 29 2022 at 11:32):

in that case, the above link shows how to set up ci and this Makefile.coq.local may be relevant: https://github.com/coq-community/aac-tactics/blob/master/Makefile.coq.local

Last updated: Jun 06 2023 at 22:01 UTC