Stream: Coq users

Topic: coq.inria.fr in zenodo entry


view this post on Zulip Yannick Forster (Dec 10 2020 at 13:09):

@Andrej Dudenhefner and I just noticed that Coq's zenodo entry (https://zenodo.org/record/4021912) which is the one Coq's doi links to does not mention Coq's offical website coq.inria.fr, and in particular it's not obvious how to download Coq from there. That's unfortunate since it might be the first link a reviewer who does not know about Coq clicks - and then sees lots of links to VST, CompCert and GitHub, but not Coq itself

view this post on Zulip Enrico Tassi (Dec 10 2020 at 13:10):

CC @Théo Zimmermann

view this post on Zulip Théo Zimmermann (Dec 10 2020 at 13:33):

Thanks for the feedback. Will fix.

view this post on Zulip Karl Palmskog (Dec 10 2020 at 15:00):

some more feedback: I thought the canonical link to the refman was https://coq.inria.fr/distrib/V8.12.0/refman rather than https://coq.github.io/doc/v8.12/refman

view this post on Zulip Karl Palmskog (Dec 10 2020 at 15:01):

it seems very shaky to depend on GitHub for what is basically the only way to directly reference the Coq manual

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

I've just copied the release notes.

view this post on Zulip Théo Zimmermann (Dec 10 2020 at 16:15):

I think I missed your point.

view this post on Zulip Karl Palmskog (Dec 11 2020 at 13:57):

Microsoft closes down GitHub or changes how GitHub pages work, all links to refman in zenodo and release notes become dead (github.io). The .inria.fr links could still live on.

view this post on Zulip Théo Zimmermann (Dec 11 2020 at 14:38):

Yes, the coq.inria.fr links still do live on. The refman is currently hosted on GitHub pages but you can access it through a coq.inria.fr facade. It's the case for all these links:

view this post on Zulip Théo Zimmermann (Dec 11 2020 at 14:39):

For moving versions, like v8.13 (https://coq.github.io/doc/v8.13/refman/), it's less important and thus we do not provide a coq.inria.fr URL.


Last updated: Feb 06 2023 at 12:04 UTC