lukaszcz / coqhammer

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

opam installation failure: bad checksum #85

Closed lukaszcz closed 4 years ago

lukaszcz commented 4 years ago

When I try to use opam to install CoqHammer 1.3 for Coq 8.12 on macOS I get the following (after typing "opam install coq-hammer").

The following actions will be performed:

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ERROR] The sources of the following couldn't be obtained, aborting:

The issue is not limited to my configuration: I got a report about the same problem from another user.

@palmskog could you look into this?

lukaszcz commented 4 years ago

BTW, I changed the 1.3 release package for Coq 8.12 on github a few days ago, because for Coq 8.12 I forgot to include one commit. Maybe that's the problem? (I'm not sure how opam works - if it somehow tries to access the package on github).

palmskog commented 4 years ago

@lukaszcz indeed the problem is that when you change a release, the package checksum in the Coq opam archive needs to be updated. I will take care of this. Please open an issue and ping me in when you change a release in the future.

palmskog commented 4 years ago

Now that coq/opam-coq-archive#1393 has been merged, please do opam update and the installation on 8.12 should work as expected. Otherwise, let me know here.