search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

SHA code of many GIT tar balls changed last night -> opam broken #121

Closed MSoegtropIMC closed 2 years ago

MSoegtropIMC commented 2 years ago

Dear Coq Hammer team,

over night the SHA code of many coq hammer git tarballs used by opam packages changed. I tested:

https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.13.tar.gz
https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.14.tar.gz
https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz

All 3 packages have as of today a different hash code than given in opam. Since this breaks Coq Platform I will fix the opam package, but I would ask you to avoid changing tags after the facts without prior notice and without adjusting the opam packages pretty much at the same time.

Best regards,

Michael

MSoegtropIMC commented 2 years ago

See (https://github.com/coq/opam-coq-archive/pull/2107)

MSoegtropIMC commented 2 years ago

Please note that I only fixed a few current opam packages. I would ask you to fix the remaining ones.

MSoegtropIMC commented 2 years ago

Actually it is more weird: when I download the tar ball given in opam I get a text file like:

the given path has multiple possibilities:
#<Git::Ref:0x00007f2ec9b890d0>,
#<Git::Ref:0x00007f2ec9b8ed50>

and as if this wouldn't be weird enough, each time I download the tar ball, the refs shown are different.

MSoegtropIMC commented 2 years ago

Actually not the SHA code changed - one has to adjust the git URL in order to tell github that one wants to have the tag and not the branch with the same name.

Did you add all the branches with the same names as tags on purpose?

MSoegtropIMC commented 2 years ago

This is now fixed by

https://github.com/coq/opam-coq-archive/pull/2107 https://github.com/coq/opam-coq-archive/pull/2108