Generating coqdoc on merge to master

[palmskog]

@Zimmi48 could it be a good idea to generate coqdoc HTML on all merges to master in the same CI job as the LaTeX one? Maybe this approach to documentation could be used for additional projects until we have more automation for releases?

[Zimmi48]

What does coqdoc need to produce HTML? Does it need to compile the project?

[palmskog]

coqdoc can work without having to compile the project, but it will then not have any cross-references between files/projects. For that, the .glob files are needed which can only be obtained after compilation. But maybe coqdoc without cross-references is good enough for now?

[Casteran]

Coqdoc uses the .glob files to generate links between different .v files. If the .glob are absent (or too old ?), it generates a warning.

…

Le 5 janv. 2021 à 17:14, Théo Zimmermann ***@***.***> a écrit : What does coqdoc need to produce HTML? Does it need to compile the project? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#19 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCVDG7QVHNCTQXSEXWDSYM3ERANCNFSM4VVCMZEA>.

[Zimmi48]

This was fixed by @start974 in #40.