Stream: Coq Platform devs & users

Topic: Failed to get sources ... bad checksum

view this post on Zulip Andrew Appel (Feb 01 2023 at 19:58):

I'm teaching using Coq 8.16.1, and I've instructed students to install the Coq Platform. One student writes as follows. Could this be related to the GitHub tarball-hash problem? But he writes it today, and I thought GitHub had fixed this by yesterday.

I've been trying to install Coq from source on my Apple Silicon Macbook Pro, following the instructions here: My Mac has homebrew installed and I attempted reinstalling its packages following the instructions in the "Homebrew issues and workarounds" section.

When I attempt to do so, however, I end up getting the following errors:

[ERROR] Failed to get sources of coq.8.16.1: Bad checksum
[ERROR] Failed to get sources of coqide.8.16.1: Bad checksum

#=== ERROR while fetching sources for coqide.8.16.1 ===========================# OpamSolution.Fetch_fail(" (Bad checksum, expected sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b)")

#=== ERROR while fetching sources for coq.8.16.1 ==============================# OpamSolution.Fetch_fail(" (Bad checksum, expected sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b)")

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> ๐Ÿซ

โ”Œโ”€ The following actions failed

โ”‚ โฌ‡ fetch coq 8.16.1

โ”‚ โฌ‡ fetch coqide 8.16.1


โ”€ No changes have been performed

view this post on Zulip Karl Palmskog (Feb 01 2023 at 20:02):

This is likely due to the student attempting the installation at the time GitHub had not rolled back the tarball changes. I'd just give the advice to try again (e.g., I just checked that V8.16.1.tar.gz now indeed has checksum 5834...)

view this post on Zulip Michael Soegtrop (Feb 03 2023 at 09:22):

@Andrew Appel : does it work now?

Last updated: Jun 03 2023 at 05:01 UTC