Header and footer for new website (rocq-prover.org) integration

[mattam82]

This allows to integrate the generated HTML smoothly into the new rocq-prover.org website.
Fixes coq/coq#19976

[mattam82]

@proux01 This changes the styling but it is not definitive (@BastienSozeau needs to adapt it still). Am I understanding correctly that this won't anyway affect released versions (e.g. 8.20.1) if we break things (visually) by modifying the html.

[Zimmi48]

Right, the master branch is only for Rocq 9.0 and future versions.

[Zimmi48]

This is a bit weird. This means that by default, the produced HTML will not be valid. We have to keep in mind that some people would like to view the doc locally. In this case, it is fine to not have any header / footer, but not to have broken HTML.

[mattam82]

@BastienSozeau

[Zimmi48]

Ah sorry, I didn't realize that this is closing tags that are opened in the header!

[mattam82]

FTR, it looks like this:

[proux01]

@proux01 This changes the styling but it is not definitive (@BastienSozeau needs to adapt it still). Am I understanding correctly that this won't anyway affect released versions (e.g. 8.20.1) if we break things (visually) by modifying the html.

Indeed, the current stdlib repo is only used for the v9.0 and master branches of coq repo.
Once the current PR merged, this will be deployed once anything is pushed on the v9.0 or master branch of coq repo.
Thus, if you want an easier way to try it, I'd recommend doing it first for Corelib in the coq repo, then you'll just have to copy it here for Stdlib.

[proux01]

@mattam82 what is the status of this? should it be merged? what about Corelib in the core repo?

[mattam82]

This can be merged already and improved upon afterwards.

[mattam82]

I'll make a PR for Corelib as well

[mattam82]

Failures seem unrelated.

[proux01]

Thanks