search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
441 stars 134 forks source link

`make` fails on macOS Sonoma 14.2.1 with Apple Silicon #1090

Closed jordydickinson closed 5 months ago

jordydickinson commented 5 months ago

Output of make:

% make
/Library/Developer/CommandLineTools/usr/bin/make AGDA_EXEC=agda gen-everythings check
runhaskell ./Everythings.hs gen-except Core Foundations Codata Experiments
agda +RTS -H6G -RTS Cubical/README.agda
/Users/jordydickinson/.agda/libraries:1:
Failed to read library file /usr/local/Cellar/agda/2.6.3/lib/agda/standard-library.agda-lib.
Reason: /usr/local/Cellar/agda/2.6.3/lib/agda/standard-library.agda-lib: openBinaryFile: does not exist (No such file or directory)
make[1]: *** [check] Error 42
make: *** [build] Error 2

I believe the problem to be that I'm using Homebrew's installation of Agda. Before Apple Silicon, Agda would have been installed in /usr/local, but is now installed in /opt/homebrew so that Intel binaries using Rosetta2 can live in /usr/local. The missing file can be found at the path /opt/homebrew/Cellar/agda/2.6.4.1_2/lib/agda/standard-library.agda-lib. It's also worthwhile to note that the path not found seems to indicate that make thinks Agda 2.6.3 is installed when in fact Agda 2.6.4.1 is installed.

felixwellen commented 5 months ago

It looks like this should happen with any agda file you want to check. I'm pretty sure you can fix that by deleting line 1 of /Users/jordydickinson/.agda/libraries which should contain the path to the non-existent file mentioned in the error. The libraries-file just lists all the libraries you have installed and you can just managed that manually.