Installed versions of Agda libraries are incompatible #194414
Closed
Description
brew gist-logs <formula> link OR brew config AND brew doctor output
% brew gist-logs agda
Error: No logs.% brew config
HOMEBREW_VERSION: 4.4.1
ORIGIN: https://github.com/Homebrew/brew
HEAD: 70672606c6ac07a5e8f75abeda7b8736e8285dbe
Last commit: 20 hours ago
Core tap JSON: 15 Oct 02:53 UTC
Core cask tap JSON: 15 Oct 02:53 UTC
HOMEBREW_PREFIX: /opt/homebrew
HOMEBREW_CASK_OPTS: []
HOMEBREW_MAKE_JOBS: 11
Homebrew Ruby: 3.3.5 => /opt/homebrew/Library/Homebrew/vendor/portable-ruby/3.3.5/bin/ruby
CPU: 11-core 64-bit arm_lobos
Clang: 16.0.0 build 1600
Git: 2.39.5 => /Library/Developer/CommandLineTools/usr/bin/git
Curl: 8.7.1 => /usr/bin/curl
macOS: 15.0.1-arm64
CLT: 16.0.0.0.1.1724870825
Xcode: 16.0
Rosetta 2: false
% brew doctor
Your system is ready to brew.
Verification
- My
brew doctoroutput saysYour system is ready to brew.and am still able to reproduce my issue. - I ran
brew updateand am still able to reproduce my issue. - I have resolved all warnings from
brew doctorand that did not fix my problem. - I searched for recent similar issues at https://github.com/Homebrew/homebrew-core/issues?q=is%3Aissue and found no duplicates.
What were you trying to do (and why)?
I'm trying to use agda. It seems that #178590 updated the standard library to 2.1 without updating agda categories to a version compatible with standard-library 2.1. I guess there is no test of these instructions and the defaults file?
What happened (include all command output)?
Testing:
% echo 'module test where' > /tmp/test.agda
% agda /tmp/test.agda
Library 'standard-library-2.0' not found.
Add the path to its .agda-lib file to
'/Users/jason/.config/agda/libraries'
to install.
Installed libraries:
standard-library-2.1
(/opt/homebrew/opt/agda/lib/agda/standard-library.agda-lib)
standard-library-doc
(/opt/homebrew/opt/agda/lib/agda/doc/standard-library-doc.agda-lib)
standard-library-tests
(/opt/homebrew/opt/agda/lib/agda/tests/standard-library-tests.agda-lib)
cubical-0.7
(/opt/homebrew/opt/agda/lib/agda/cubical/cubical.agda-lib)
agda-categories
(/opt/homebrew/opt/agda/lib/agda/categories/agda-categories.agda-lib)
agda2hs (/opt/homebrew/opt/agda/lib/agda/agda2hs/agda2hs.agda-lib)
Debugging:
% which agda
/opt/homebrew/bin/agda
% cat ~/.config/agda/defaults
standard-library
cubical
agda-categories
agda2hs
% cat ~/.config/agda/libraries
/opt/homebrew/opt/agda/lib/agda/standard-library.agda-lib
/opt/homebrew/opt/agda/lib/agda/doc/standard-library-doc.agda-lib
/opt/homebrew/opt/agda/lib/agda/tests/standard-library-tests.agda-lib
/opt/homebrew/opt/agda/lib/agda/cubical/cubical.agda-lib
/opt/homebrew/opt/agda/lib/agda/categories/agda-categories.agda-lib
/opt/homebrew/opt/agda/lib/agda/agda2hs/agda2hs.agda-lib
% find /opt/homebrew/opt/agda/lib/agda/ -type f | xargs grep 'standard-library-2.0'
/opt/homebrew/opt/agda/lib/agda//categories/agda-categories.agda-lib:depend: standard-library-2.0
What did you expect to happen?
The default instructions should not break the running of agda on basic examples.
Step-by-step reproduction instructions (by running brew commands)
Installation:
% brew install agda
[...]
To use the installed Agda libraries, execute the following commands:
mkdir -p $HOME/.config/agda
cp /opt/homebrew/opt/agda/lib/agda/example-libraries $HOME/.config/agda/libraries
cp /opt/homebrew/opt/agda/lib/agda/example-defaults $HOME/.config/agda/defaults
You can then inspect the copied files and customize them as needed.
[...]
% mkdir -p $HOME/.config/agda
% cp /opt/homebrew/opt/agda/lib/agda/example-libraries $HOME/.config/agda/libraries
% cp /opt/homebrew/opt/agda/lib/agda/example-defaults $HOME/.config/agda/defaults