Stream: Coq devs & plugin devs

Topic: Serious Stdlib coqdoc regression in 8.12 with links


view this post on Zulip Karl Palmskog (Jul 15 2020 at 19:29):

Not sure if this is the right place to post this, but it seems all file links in deployed Stdlib coqdoc has gone dead. Compare the two following pages:

In the first link, none of the Require Export module names are clickable. In the second link, they are. Unless this is some fluke it looks pretty serious to me - but may not be a bug with coqdoc itself, just with how stdlib documentation is deployed.

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:30):

It's definitely worth opening an issue about so that we don't release 8.12.0 with this issue.

view this post on Zulip Karl Palmskog (Jul 15 2020 at 19:32):

OK, I will do a report, but I unfortunately don't have time to investigate much further this week.

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:44):

no worries, thanks for raising the issue anyway

view this post on Zulip Karl Palmskog (Jul 15 2020 at 19:45):

if anyone not watching the Coq repo wants to follow this: https://github.com/coq/coq/issues/12699

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:11):

Hi folks so we have two choices to fix this in the CI: to revert the deployment to makefile or just do a rm -rf _build in the coqdoc job

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:11):

the advantage of the latter is that is much less invasive while I prepare a fix upstream

view this post on Zulip Théo Zimmermann (Jul 16 2020 at 13:25):

Emilio Jesús Gallego Arias said:

Hi folks so we have two choices to fix this in the CI: to revert the deployment to makefile or just do a rm -rf _build in the coqdoc job

Any solution suits me.

view this post on Zulip Karl Palmskog (Jul 16 2020 at 16:58):

I guess the latter solution is more future proof? No clear preference here though.


Last updated: Oct 16 2021 at 07:02 UTC