search

lukaszcz / coqhammer

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

The opam is down #123

Closed xqyww123 closed 2 years ago

xqyww123 commented 2 years ago

Hi, the opam command to install the coq hammer is currently down

$ opam install coq-hammer

#=== ERROR while fetching sources for coq-hammer-tactics.1.3.2+8.15 ===========#
OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

#=== ERROR while fetching sources for coq-hammer.1.3.2+8.15 ===================#
OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

I visited the page https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz and it returns an error:

the given path has multiple possibilities: #<Git::Ref:0x00007f6457d24f98>, #<Git::Ref:0x00007f6457cefa28>

I guess it's the reason why the opam failed, and it looks like some wrong configuration in the git repo.

lukaszcz commented 2 years ago

Try "opam update" and tell me if it still fails.

On Sun, 13 Mar 2022, 03:39 Xero Essential, @.***> wrote:

Hi, the opam command to install the coq hammer is currently down

$ opam install coq-hammer

=== ERROR while fetching sources for coq-hammer-tactics.1.3.2+8.15 ===========

OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

=== ERROR while fetching sources for coq-hammer.1.3.2+8.15 ===================

OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

I visited the page https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz and it returns an error:

the given path has multiple possibilities: #, #

I guess it's the reason why the opam failed, and it looks like some wrong configuration in the git repo.

— Reply to this email directly, view it on GitHub https://github.com/lukaszcz/coqhammer/issues/123, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH2WYFWLYJ3EFXUINCDU7VIMNANCNFSM5QSW23XQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

lukaszcz commented 2 years ago

Closing due to lack of response.