Karl Palmskog (Aug 25 2020 at 19:47): Karl Palmskog (Aug 25 2020 at 19:47):Another long-term issue for the platform: make all platform package maintainers cryptographically sign their releases that become part of a platform release. I documented here how one can check that a Coq tarball was actually signed by a Coq release manager, and similar practices should apply to the platform: https://github.com/coq/coq/wiki/VerifyingReleases
Karl Palmskog (Aug 25 2020 at 19:50):unfortunately, a "Coq platform key signing party" to increase trust may be some time off in the future, and not only due to the time it takes to get the platform established...
Théo Zimmermann (Aug 26 2020 at 07:54):Why does this page explain how to verify the signature of the commit instead of the signature of the tag itself?
Karl Palmskog (Aug 26 2020 at 07:57):@Théo Zimmermann as far as I can tell, there is no dedicated git command for verifying a tag, git verify-commit is all there is (or maybe it was added recently)
Karl Palmskog (Aug 26 2020 at 08:17):also, it seems the V8.11.0, V8.11.1 and V8.11.2 tags were never signed :shrug:
Théo Zimmermann (Aug 26 2020 at 09:48):Sigh! This is despite the release documentation giving exactly the commands to use to prepare the tags.
Karl Palmskog (Aug 26 2020 at 10:14):I guess I can update for 8.12 and add a note about instructions (for verifying release locally) not working for 8.11. It's not really feasible to describe both workflows at the same time (verifying a tag vs. verifying a commit)
Théo Zimmermann (Aug 26 2020 at 10:55):We could also ask @Pierre-Marie Pédrot (not subscribed to this stream) to recreate the tags for 8.11.
Karl Palmskog (Aug 26 2020 at 11:23):but wouldn't that change the tarballs/checksums and lead to a lot of work in opam, etc.?
Théo Zimmermann (Aug 26 2020 at 12:24):I don't think so. The tarballs only depend on the content in there, not the tag meta-data AFAIK.
Michael Soegtrop (Aug 26 2020 at 14:10):I think it would make sense to have a meta field in opam to specify how sure one can be about the authorship and check this. Btw.: interestingly opam does not fail when the given hashes are wrong. It spits an an error, but continues happily.
Karl Palmskog (Aug 26 2020 at 14:16):@Théo Zimmermann so should I open a Coq issue about the missing tags? it may become a problem in the future if we integrate authorship verification in some pipeline
Théo Zimmermann (Aug 26 2020 at 14:17):Sure!
Last updated: Jun 03 2023 at 05:01 UTC