[dune] Simple rule to generate Stdlib's documentation.

[ejgallego]

Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.

I am not sure what should be done w.r.t. style files.

[SkySkimmer]

Compcert failed due to AbsInt/CompCert#275 (comment)
Should be fixed now

[SkySkimmer]

Not sure why bedrock failed
Linter error is spurious (#9653) and in the per-commit part, we can ignore it.

Do we merge without the .glob dependencies?

[ejgallego]

Do we merge without the .glob dependencies?

Nope, let me fix that indeed, and rebase on top of #9648

[SkySkimmer]

I'll let @Zimmi48 as dune secondary assign.

[ejgallego]

Rebased, but I am not sure how to test the deploy job (@vbgl ?)

[vbgl]

To test deploy jobs, I’ve manually started a CI pipeline with the appropriate credentials. I can do it for you if you think its necessary.

[ejgallego]

To test deploy jobs, I’ve manually started a CI pipeline with the appropriate credentials. I can do it for you if you think its necessary.

Yup but that would overwrite the main Coq repos, right?

I guess I'll deploy to my own repos, and make the clone target a variable then.

[vbgl]

It will not overwrite, but put you artifact in a separate directory (named as your branch: dune+coqdoc).

[ejgallego]

It will not overwrite, but put you artifact in a separate directory (named as your branch: dune+coqdoc).

Ah Ok, cool then!

[ejgallego]

I'd appreciate indeed if you can push a build to see whether that works.

[vbgl]

Pipeline started. Result should appear in a few hours there: https://coq.github.io/doc/dune+coqdoc

[ejgallego]

Pipeline started. Result should appear in a few hours there: https://coq.github.io/doc/dune+coqdoc

Muchas gracias @vbgl

[ejgallego]

Will wait for the deploy build to finish before the rebase.

[Zimmi48]

There is also a problem with the artifacts (which should in principle make the deploy job fail): _build/default/doc/stdlib/html/ is not exported. See https://gitlab.com/coq/coq/-/jobs/167795044/artifacts/browse/_build/default/doc/.

[ejgallego]

Well-spotted @Zimmi48 ahhh; indeed @SkySkimmer was right, I've added an extra CI job which should help consistency.

Fixed version uploaded, deploy job needs relaunch.

[vbgl]

Pipeline launched for 7ba806b.

[vbgl]

The deploy jobs went through (also for the last update). There are some issues with the documentation of the stdlib. E.g., at https://coq.github.io/doc/dune+coqdoc/stdlib/, in the “navigation” part, there is a dead link to genindex.html.

[ejgallego]

The deploy jobs went through (also for the last update). There are some issues with the documentation of the stdlib. E.g., at https://coq.github.io/doc/dune+coqdoc/stdlib/, in the “navigation” part, there is a dead link to genindex.html.

It seems to work well here @vbgl , are you sure you were not looking to an older build [which had this problem]

So far, the docs looks pretty good to me.

[vbgl]

My bad. It looks good indeed.

[ejgallego]

Thanks to all for the help!