8000 Both stack and cabal fail to install Agda · Issue #7455 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Both stack and cabal fail to install Agda #7455

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
ningcng opened this issue Aug 27, 2024 · 5 comments · Fixed by #7465
Closed

Both stack and cabal fail to install Agda #7455

ningcng opened this issue Aug 27, 2024 · 5 comments · Fixed by #7465
Labels
regression in 2.6.4.2 status: info-needed More information is needed from the bug reporter to confirm the issue. ux: installation Getting Agda set up on your machine
Milestone
2.7.0.1

Comments

@ningcng
Copy link
ningcng commented Aug 27, 2024 •
edited
Loading

Tried cabal 3.12.1.0/3.10.3.0 and ghc 9.6.6 on macOS Sonoma Kernel 23.6.0 (Hardware: M3 Max)
cabal install Agda

[2 of 2] Linking dist/build/agda/agda
Installing executable agda-mode in /Users/ningcng/.local/state/cabal/store/ghc-9.6.6/incoming/new-26892/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/Agd-2.7.0-12a325e8/bin
Warning: The directory
/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/incoming/new-26892/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/Agd-2.7.0-12a325e8/bin
is not in the system search path.
Installing library in /Users/ningcng/.local/state/cabal/store/ghc-9.6.6/incoming/new-26892/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/Agd-2.7.0-12a325e8/lib
Installing executable agda in /Users/ningcng/.local/state/cabal/store/ghc-9.6.6/incoming/new-26892/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/Agd-2.7.0-12a325e8/bin
Warning: The directory
/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/incoming/new-26892/Users/ningcng/.local/state/cabal/store/ghc-9.6.6/Agd-2.7.0-12a325e8/bin
is not in the system search path.
Generating Agda library interface files...
Error: setup: filepath wildcard
'lib/prim/_build/2.7.0/agda/Agda/Builtin/Bool.agdai' does not match any files.

Stack fails with Agda 2.6.4.3 with the same error.

Installing 2.6.3 works fine.
@andreasabel andreasabel added the ux: installation Getting Agda set up on your machine label Aug 27, 2024
@agda agda deleted a comment Aug 27, 2024
@andreasabel
Copy link
Member

Thanks, @ningcng for the report!
It is not easy to find the cause of the problem because I do not have access to your machine.

One lead to explore is whether this is connected to the new support for the XDG directory structure that cabal implemented in 3.10.

/Users/ningcng/.local/state/cabal/store/

Maybe we are looking for the generated .agdai files in the wrong place now.

'lib/prim/_build/2.7.0/agda/Agda/Builtin/Bool.agdai' does not match any files.

Could you try whether installation succeeds with cabal 3.8?

@andreasabel andreasabel added the status: info-needed More information is needed from the bug reporter to confirm the issue. label Aug 27, 2024
@andreasabel andreasabel modified the milestones: 2.8.0, 2.7.0.1 Aug 27, 2024
@andreasabel
Copy link
Member

@ningcng wrote:

Installing 2.6.3 works fine.

Could you please try installing 2.6.4 or 2.6.4.1 (with cabal 3.12)?

That would test whether PR #6988, released with Agda 2.6.4.2, is connected to this issue.

@ningcng
Copy link
Author
ningcng commented Aug 27, 2024 •
edited
Loading

Installing 2.6.4.1 with cabal 3.10/3.12 works.

@andreasabel
Copy link
Member

Thanks!

I tried to install Agda-2.7.0 with cabal-3.12 and GHC 9.10 on a fresh user account so as to get the XDG directory layout. It succeeded. So unfortunately I could not reproduce the problem yet.

@ningcng : Could you try to provide more information? E.g. supplying -v3 to cabal could give some context around the failure that could help localize the problem.

@andreasabel andreasabel mentioned this issue Sep 2, 2024
Merged
andreasabel added a commit that referenced this issue Sep 2, 2024
@andreasabel
Re #7455: Setup.hs: catch when Agda did not produce all agdai files
8f8d152 
The cause of #7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
@andreasabel andreasabel mentioned this issue Sep 2, 2024
Merged
andreasabel added a commit that referenced this issue Sep 3, 2024
@andreasabel
Re #7455: Setup.hs: catch when Agda did not produce all agdai files
7e6ddcc 
The cause of #7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
@andreasabel
Copy link
Member

Without further information, I could not reproduce the issue. However, PR #7465 might help working around the problem.
@ningcng Please reopen a new issue with more information should the installation problem persist in Agda 2.7.0.1.

andreasabel added a commit that referenced this issue Sep 3, 2024
@andreasabel
Re #7455: Setup.hs: catch when Agda did not produce all agdai files
94dfec3 
The cause of #7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
@andreasabel andreasabel mentioned this issue Sep 3, 2024
Merged
andreasabel added a commit that referenced this issue Sep 3, 2024
@andreasabel
Re #7455: Setup.hs: catch when Agda did not produce all agdai files
03f5abe 
The cause of #7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Re agda#7455: Setup.hs: catch when Agda did not produce all agdai files
33fec42 
The cause of agda#7455 is atm still unclear to me, but this patch adds a
check that all .agdai files we ask cabal to copy do actually exist.
If they do not, we skip the copy step.

Rationale: Unless the user does a sudo install, copying the interface files isn't
essential at the time of installation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
regression in 2.6.4.2 status: info-needed More information is needed from the bug reporter to confirm the issue. ux: installation Getting Agda set up on your machine
Projects
None yet
Milestone
2.7.0.1
Development

Successfully merging a pull request may close this issue.

Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files agda/agda
2 participants
@andreasabel @ningcng
0