Andrew Appel (Feb 01 2023 at 19:58): 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: https://github.com/coq/platform/blob/2022.09.1/doc/README_macOS.md#installation-by-compiling-from-sources-using-opam. 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("https://github.com/coq/coq/archive/refs/tags/V8.16.1.tar.gz (Bad checksum, expected sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b)")
#=== ERROR while fetching sources for coq.8.16.1 ==============================# OpamSolution.Fetch_fail("https://github.com/coq/coq/archive/refs/tags/V8.16.1.tar.gz (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
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...)
Michael Soegtrop (Feb 03 2023 at 09:22):@Andrew Appel : does it work now?
Last updated: Jun 03 2023 at 05:01 UTC