Generate Documentation with Alectryon

[JasonGross]

On top of #1453

Closes #1435

Currently uses my fork of Alectryon, until cpitclaudel/alectryon#25 gets merged.

I've set this up as a Docker action (which requires running the bulk of the action in a single step, unfortunately), so that I have access to opam with a pre-installed Coq, so that I can install coq-serapi without having to build it manually on the CI.

This action will upload an artifact containing the HTML on PRs, so it's possible (if a tad bit annoying) to browse the generated documentation on PRs. (Unless there's a way to browse the inside of .zip files from inside a browser without downloading them locally?) Additionally, it'll push the docs to gh-pages on master (hopefully I didn't screw this up).

Here's some pictures:

It would be nice if Alectryon had --toc / --index options (cc @cpitclaudel), because right now I'm just copying over the jank TOC and index generated by coqdoc:

[JasonGross]

This is by far the slowest build job at 32 minutes, but I think that's okay. Documentation now at https://github.com/HoTT/HoTT/suites/2489508125/artifacts/53701473

[Alizter]

@JasonGross Perhaps it is worth having a gitlab mirror so we can at least have better artefacts?

[JasonGross]

Having a GitLab mirror sounds good, though I don't know how to set it up. Do you have experience setting up GitLab mirrors/CI?

[Alizter]

I have no idea how to but I can look into it.

[JasonGross]

I've just rebased this. Should we merge it as-is, and we can improve it / move it to GitLab later?

[Alizter]

I had a look at the documentation files, but they are not formatted (I guess no css?) Perhaps I am not looking at them correctly?

Also is this still using proviola? I am unsure if the CI is taking long to use Alectryon or because its still messing around with proviola?

[JasonGross]

There should be css files included in the relevant directory, if not I'll have to debug.

This job is completely independent from the proviola one, and should be running in parallel. It seems that it takes about 10 minutes to build the repo and then about 20 minutes after that to build the alectryon doc. Unfortunately I'm not aware of any way to do them simultaneously. @cpitclaudel do you think we can get a mode where alectryon replaces coqc and dumps both the html and the vo for each file?

[Alizter]

@JasonGross Actually I think it's fine. I was peaking in the zip before which is why the css wasn't working. After extracting it it works fine.

[Alizter]

But looking at the documentation, this is really nice! If we can make it more accessible from a PR it will be very useful!

[JasonGross]

If we can make it more accessible from a PR it will be very useful!

That's my hope, too! We may even be able to set up @coqbot or similar to stick a link to the generated documentation in the checks/status.

[jdchristensen]

How do you build the new documentation locally? I did apt-get install python3-dominate and then make alectryon and make alectryon-html, but only got three files in the alectryon-html directory: coqdoc.css index.html toc.html.

There were various warnings like:

Line 17, character 6, warning: unterminated inline ">>"

[jdchristensen]

(I also did the build fresh from the start, with autogen, make clean, etc.)

[JasonGross]

Documentation is now live on the wiki:

An interactive reference manual autogenerated by Alectryon; hovering over a line of code will display the feedback given by Coq at that point in the code. (index) (table of contents)

[JasonGross]

How do you build the new documentation locally?

@jdchristensen Assuming you have coq-serapi set up in a way that ocamlfind query coq-serapi can find it (note that it only builds with v8.13, not master) and you have updated the submodules (git submodule update --init --recursive) and you have also installed pygments dominate beautifulsoup4 docutils with python3 (for example python3 -m pip install --user --upgrade pygments dominate beautifulsoup4 docutils), then you should first build the whole library (with ./autogen.sh && ./configure && make), and then running make alectryon should work (expect it to take about 20 minutes, unfortunately). If you want, I can set up separate targets for each .html / .v file.

[cpitclaudel]

Wonderful work, Jason! :)

@cpitclaudel do you think we can get a mode where alectryon replaces coqc and dumps both the html and the vo for each file?

That would be nice! But I don't know to which extend Coq knows how to do this (we have this come up from time to time in PG too, where we're asked whether we could just dump a .vo using a command. Do you know if that's something the STM can do? If yes, it would just be a matter of calling the right command.

[JasonGross]

There were various warnings like:

Line 17, character 6, warning: unterminated inline ">>"

Indeed, we should probably switch to whatever rst uses for verbatim blocks so they get rendered nicely, or otherwise figure out how to fix the warnings.

[cpitclaudel]

That's a Coqdoc warning, right? I'm surprised that it pops up — maybe Alectryon isn't feeding the coqdoc comments to coqdoc the right way?

[JasonGross]

Ah, this is because we're reusing the coqdoc files for the toc and index. Once Alectryon can generate a toc and index for us, we'll stop using coqdoc.