How-to-document.md

How to edit the LAProof documentation

Rocq documentation (in .v files)

0. Because Makefile.coq's "make clean" removes the entire html directory, we cannot store the reference copy of index.html there. Instead, index.html is in the root directory, and copied into the html directory by "make html2".

1. Edit index.html as you see fit. Do not edit any files of the form html/LAProof.*, as these are automatically generated by coqdoc.

2. Edit the comments in any of the .v files, using Coqdoc markup.

3. make html2 creates all the Coqdoc output in the html/ directory. Browse and review these local files (by doing open file in your browser) and edit the .v files until this looks the way you want it.

4. make publish sends all those html files (including index.html if you have edited it) to the Github pages site at https://verinum.org/LAProof/. The way it does this is by committing them to the special gh-pages branch of this repo, which contains only a docs directory with those HTML files. After you do make publish, it will take several minutes before the changes appear at verinum.org/LAProof.

5. Don't forget to git-commit and git-push all your changes in the main branch (or whatever branch you're working in).

C documentation (in .c, .h files)

1. Edit comments in those .c and .h files that are mentioned in line CDOCS line of Makefile.coq.local. Write comments in a form that can be processed by Quarto.

2. If you add a new .c and/or .h file, update the CDOCS line, and add a link in html/index.html in the C programs section.

3. Build the HTML from C by doing make cdocs. This puts individual .html files in the cdocs directory. You can inspect them there using open file in your browser. Unfortunately, when viewing this way, the links in the C programs section go to the wrong place; the make publish command will put them in the right place when publishing.

4. make publish handles the cdoc files as well as the coqdoc files (as described above).