Links to corelib on rocq-prover.org broken

[mattam82]

E.g. on https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Strings.PrimString.html# we have a link to https://rocq-prover.org/doc/V9.0.0/stdlib/Corelib.Strings.PrimString.html which should rather be https://rocq-prover.org/doc/V9.0.0/corelib/Corelib.Strings.PrimString.html

Where / how do we fix this?

[proux01]

I guess we should give a config option to coqdoc somewhere in the stdlib-html target in stdlib. Maybe something like --external https://rocq-prover.org/doc/V9.0.0/corelib+Corelib

[SkySkimmer]

What does +Corelib mean? Seems like it should be rather --external Corelib https://rocq-prover.org/doc/V9.0.0/corelib

[proux01]

That's what rocq doc --help tells:

  --external <url>+<d> set URL for external library <d>

but you may be right. Anyway, the fix https://github.com/rocq-prover/stdlib/pull/129/files went for --coqlib_url working around the issue.

[SkySkimmer]

That's a weird command line interface that I wasn't aware of, but OK.

[proux01]

According to the code, the + in the help message actually stands for spaces.

[proux01]

Should be fixed by rocq-prover/rocq#20485

[mattam82]

Yeah, thanks for fixing the help message, I got surprised as well.