Add generated HTML documentation to gh-pages branch for tags

[palmskog]

It's currently a considerably manual chore to generate HTML documentation for Coq project releases and commit it to the gh-pages branch of a repo. This is something that coqbot could automate.

As one recent example of how to automate this, we used Jenkins to generate coqdoc for every commit for a Coq project, see this commit.

[Zimmi48]

@palmskog Could you specify more clearly what is the expected workflow for generating and committing this documentation? AFAICT it is not documented anywhere in the templates repository and people have been quite inconsistent in their use of the generated index.md.

[palmskog]

I think the workflow is quite well specified in the commit I referenced. However, I can recapitulate briefly:

• we only care about deploying Coq code documentation, index.md is a different concern
• all kinds of code documentation lives in docs in the gh-pages branch, organized by tags, e.g.,
  • docs/V8.10.0/coqdoc
  • docs/V8.11.0/coqdoc
  • docs/V8.11.0/coq2html
• there is a symlink latest to the most recent tag, e.g.,
  • docs/latest -> docs/V8.11.0
• when a tag V8.12.0 is created, the bot checks out the tag source, and creates and copies the docs, e.g.,
  • make coqdoc && cp -r docs/coqdoc /path/to/gh-pages/docs/V8.12.0
  • make coq2html && cp -r docs/coq2html /path/to/gh-pages/docs/V8.12.0
• finally, the bot updates the latest symlink and commits the changes to gh-pages

[Zimmi48]

I wonder if this case wouldn't be better served (at least partially) by a GitHub Action because of the need to compile the documentation using the right set of dependencies. What about making a feature request to https://github.com/coq-community/docker-coq-action (cc @erikmd) so that:

1. docs are built using coqdoc/coq2html
2. docs are deployed as an artifact

Then, as a second step, the workflow can send a request to a new coqbot endpoint to retrieve the artifact and copy them to the right location, update the symlink and push to the gh-pages branch. This second step could alternatively be taken care of directly inside the workflow using custom scripts or dedicated Actions (such as https://github.com/marketplace/actions/push-git-subdirectory-as-branch, but this action will override the whole content of the gh-pages branch, so one would have to first prepare the exact content that needs to be pushed).

[palmskog]

I'm willing to work on this issue, for example during CUDW this year, but I'm going to need quite a few pointers how we should handle the GitHub Actions part. It sounds like we have to do some kind of specialized GitHub action that relies on Docker-Coq-Action.

[Zimmi48]

I'm not sure that creating Actions that depend on others is really supported. But adding specific optional features to the main Docker-Coq-Action wouldn't be a problem, I think...