Given that Coq's refman has a different license than Coq (ODL vs. LGPL-2.0-only), and that people sometimes want to cite the Coq refman separately from Coq itself (e.g., when talking about some feature such as SProp), how about putting the refman as a separate "Publication" artifact on Zenodo [for a major release]?
For example, the MathComp book is on Zenodo, which provides:
FWIW the correct SPDX code for Coq's refman seems to be OPUBL-1.0.
I'm fine with this idea of publishing the refman to Zenodo but it also happened in the past that the refman was published to HAL.
right, but HAL doesn't (yet) provide DOIs
Right, though it may have other benefits that people may have been looking for (e.g., easier to cite in Inria's project-team reports).
also, isn't the version handling on Zenodo a better fit? They put a user-defined version number directly in the metadata
Yes, I agree with your preference.
I'd just like to know what is the opinion of @Matthieu Sozeau on this question since I think he was the one who published the refman on HAL for the last time.
And if we decide to publish the refman on Zenodo, it's easy for me to do it as part of the (for now manual) Zenodo archiving pipeline.
in the Zenodo archiving pipeline, maybe we can add the
Coq keyword, this is similar to GitHub topics: https://zenodo.org/search?q=keywords%3A%22Coq%22
Théo Zimmermann said:
I'd just like to know what is the opinion of Matthieu Sozeau on this question since I think he was the one who published the refman on HAL for the last time.
Zenodo is definitely better, last time I checked HAL still handled refman publications poorly
Last updated: Dec 01 2023 at 07:01 UTC