-
Notifications
You must be signed in to change notification settings - Fork 6
Generating and deploying coqdoc HTML documentation
This is a short tutorial on how to continuously generate and deploy HTML documentation for a Coq project by leveraging the coqdoc tool, GitHub Pages, and CoqdocJS scripts adapted for coq-community.
The idea is that the source HTML files produced by coqdoc, which are deployed to GitHub's servers along with custom pages, live in the gh-pages branch of the repository, e.g., for a release named v1.1, in the docs/v1.1/coqdoc directory of this branch. Since HTML is not particularly compact, maintainers are recommended to only update the gh-pages branch with new coqdoc output when a new project version is released, to keep repository size small.
The files in CoqdocJS are meant to be copied into other repositories. Here, we assume the CoqdocJS repository is cloned from the directory above the project's repository directory:
git clone https://github.com/palmskog/coqdocjs.git
We assume a delegating top-level Makefile using coq_makefile as described here.
Go to the repository and copy the CoqdocJS file Makefile.coq.local :
cp ../coqdocjs/Makefile.coq.local .
If you already have a Makefile.coq.local, you will have to manually merge it with the contents of the file from CoqdocJS.
Copy the resources directory from CoqdocJS into your project:
cp -r ../coqdocjs/resources .
It may also be worthwhile to store a generic website index page in the directory. For example, one can use a corresponding mustache template to generate a basic Markdown file:
mustache meta.yml ../templates/index.md.mustache > resources/index.md
When index.md is as required, one can generate the corresponding index.html using pandoc:
pandoc -s -o resources/index.html resources/index.md
Finally, commit all new files to your repo.
The contents is generated as follows:
make coqdoc
For an example repository following the above conventions, see the Huffman project, and in particular its deployed website and coqdoc documentation.