Homebrew / homebrew-core

🍻 Default formulae for the missing package manager for macOS (or Linux)
https://brew.sh
BSD 2-Clause "Simplified" License
13.71k stars 12.41k forks source link

Installed versions of Agda libraries are incompatible #194414

Open JasonGross opened 1 week ago

JasonGross commented 1 week ago

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

What were you trying to do (and why)?

I'm trying to use agda. It seems that https://github.com/Homebrew/homebrew-core/pull/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 commented 2 days ago

I have opened an issue for that,

And here is a related PR with this issue.