coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

GitHub autogenerated tarballs not considered stable #2458

Open palmskog opened 1 year ago

palmskog commented 1 year ago

Due to GitHub changing compression approach on Jan 30, 2023, every auto-generated GitHub hosted tarball now has a different checksum. The archive content is the same.

The following is GitHub's message to anyone affected by this, like us:

GitHub doesn't guarantee the stability of checksums for automatically generated archives. If you need to rely on a consistent checksum, you may upload archives directly to GitHub Releases.

So it seems we have to both (1) ensure checksums are refreshed for all GitHub tarballs in the archive and (2) ensure that only stable archives are used in packages going forward...

palmskog commented 1 year ago

If anyone is looking for a workaround, the following may be used:

opam install <package> --no-checksums

@erikmd maybe we can use this by default in the Coq Docker? Unless checksums get rolled back (unlikely) this will take the whole OCaml and Coq ecosystem some time to work around.

palmskog commented 1 year ago

GitHub may be in the process of reverting the change:

We're sorry for the breakage, we're reverting the change, and we'll communicate better about such changes in the future (including timelines).

palmskog commented 1 year ago

From what I can tell, GitHub has now rolled back the tarball checksum changes. But the central problem remains in the long term: autogenerated GitHub tarballs are probably not trustworthy for preservation of code in the OCaml and Coq ecosystem.

LasseBlaauwbroek commented 1 year ago

I just saw that an official request for feedback on this problem was opened: https://github.com/community/community/discussions/46034?sort=new Could be a good idea to add Coq's or OCaml's usecase there.

LasseBlaauwbroek commented 1 year ago

https://github.blog/2023-02-21-update-on-the-future-stability-of-source-code-archives-and-hashes/

ybertot commented 1 year ago

What I understand from reeding this link is that the problem needs to be handled by opam. A solution that comes to mind is to hash, not on the compressed archive, but on the uncompressed one (or any result given by a chosen filter).

gares commented 1 year ago

Opam could hash the uncompressed, and be future proof. But we have a lot of packages which declare the hash of the compressed archive. For these we would need some automation to update the hash, once opam understands the new hashing schema.