Installed versions of Agda libraries are incompatible

[JasonGross]

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 doctor output says Your system is ready to brew. and am still able to reproduce my issue.
• I ran brew update and am still able to reproduce my issue.
• I have resolved all warnings from brew doctor and 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

[daeho-ro]

I have opened an issue for that,

• Support for stdlib 2.1? agda/agda-categories#437

And here is a related PR with this issue.

• agda 2.7.0.1 #193315

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs.

[JasonGross]

Has it been resolved?