cabal install Agda -- fails with executable-dynamic

[ulidtko]

cabal install Agda -- fails with executable-dynamic

[andreasabel]

As a user on "Step 2" of installation

https://agda.readthedocs.io/en/v2.6.4.1/getting-started/installation.html#step-2-installing-the-agda-and-the-agda-mode-programs

• complaining of Agda's Setup upper bound on text < 2.1 conflicting with text-2.1 that GHC 9.8 ships with.

That would be Cabal-3.8's upper bound on text < 2.1, not Agda's. Agda setup needs Cabal, but it does not constrain it...

cabal install Agda — fails for me in the .agdai post-compilation step.

It works for me:

$ cabal install Agda
...
Installing library in /Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/lib
Installing executable agda in /Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
Warning: The directory
/Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
is not in the system search path.
Generating Agda library interface files...
Installing executable agda-mode in /Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
Warning: The directory
/Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
is not in the system search path.
Installing library in /Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/lib
Installing executable agda in /Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
Warning: The directory
/Users/abel/.cabal/store/ghc-9.8.2/incoming/new-78835/Users/abel/.cabal/store/ghc-9.8.2/Agd-2.6.4.1-bd324cfb/bin
is not in the system search path.
Copying 'agda' to '/Users/abel/.cabal/bin/agda'
Copying 'agda-mode' to '/Users/abel/.cabal/bin/agda-mode'

$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 9.8.2

$ cabal -V
cabal-install version 3.10.2.1
compiled using version 3.10.2.1 of the Cabal library 

My possibly relevant (?) ~/.cabal/config settings:

installdir: /Users/abel/.cabal/bin
install-method: copy
overwrite-policy: always
write-ghc-environment-files: never

[ulidtko]

Yup; this did work:

$ cabal v2-install --disable-executable-dynamic --disable-documentation --ghc-options=-j  Agda
Resolving dependencies...
Build profile: -w ghc-9.8.1 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.4.1 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     Agda-2.6.4.1 (all, legacy fallback)
Building     Agda-2.6.4.1 (all, legacy fallback)
Installing   Agda-2.6.4.1 (all, legacy fallback)
Completed    Agda-2.6.4.1 (all, legacy fallback)
Symlinking 'agda' to '/home/ulidtko/.cabal/bin/agda'

Which makes sense — dynlibs won't load while dist/build/agda/agda resides somewhere at temporary limbo path 🤔 as that requires RPATH / LD_LIBRARY_PATH and such... Funny that RPATH won't be effective, as the executable is to be soon moved once again.

Some distributions insist on dynamic-only linking; so this failure mode is something to consider.

[ulidtko]

@andreasabel v1-install with executable-dynamic succeeds on my end.

Maximal action: get rid of Setup.hs.

Yep 👍 #7157 linked already.

---

Re: CI, seeing the 5s step time makes me suspicious that most of it got cached 😂

[andreasabel]

Alright, now with executable-dynamic: True in .cabal/config we have a reproducer: https://github.com/agda/agda/actions/runs/8184627336/job/22379417845?pr=7172

Upstream issue:

• haskell/cabal#9784

[andreasabel]

Since this is not a problem on macOS, I tend to put the blame upstream now.
We might warn in the docs about checking for executable-dynamic: True in the .cabal/config.
Or we recommend installation via stack, but this might have its own pitfalls.

[ulidtko]

@andreasabel I tried it... Naively, doesn't seem to help, the .so likewise can't be found:

$ cabal v2-install --enable-executable-dynamic --verbose .
[...]
Installing executable dist/build/libHSAgda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3-ghc9.6.4.so to /home/ulidtko/.cabal/store/ghc-9.6.4/incoming/new-3043174/home/ulidtko/.cabal/store/ghc-9.6.4/Agda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3/lib/libHSAgda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3-ghc9.6.4.so
Installing executable agda in /home/ulidtko/.cabal/store/ghc-9.6.4/incoming/new-3043174/home/ulidtko/.cabal/store/ghc-9.6.4/Agda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3/bin
Warning: The directory /home/ulidtko/.cabal/store/ghc-9.6.4/incoming/new-3043174/home/ulidtko/.cabal/store/ghc-9.6.4/Agda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3/bin is not in the system search path.
dist/build/agda/agda: error while loading shared libraries: libHSAgda-2.6.5-a88d61781dc99162e02d5d6d176b13f1418efc8b30ce081e297f0204e18346d3-ghc9.6.4.so: cannot open shared object file: No such file or directory

This is with Agda's Setup.hs patched to invoke the agda executable from postCopy hook, instead of copyHook. The exact diff I tried is here: ulidtko@ab8bab6

cc @UlfNorell @nad

[andreasabel]

@ulidtko : From which directory are you running cabal install Agda?

[ulidtko]

@andreasabel conversely, my ~/.cabal/config without the comments:

nix: disable
remote-repo-cache: /home/ulidtko/.cabal/packages
executable-dynamic: True
extra-prog-path: /home/ulidtko/.cabal/bin
documentation: True
build-summary: /home/ulidtko/.cabal/logs/build.log
remote-build-reporting: none
jobs: $ncpus
installdir: /home/ulidtko/.cabal/bin

doesn't seem much different...

From which directory are you running cabal install Agda?

That was from a project directory, a clone of https://github.com/ikedaisuke/Pythagoras (i.e. there's no cabal.project)

[andreasabel]

That was from a project directory, a clone of ikedaisuke/Pythagoras (i.e. there's no cabal.project)

Ok, this does not have a .cabal file either, so there couldn't be any influence...

Could you try with executable-dynamic: False?

What looks weird in your log is this line:

dist/build/agda/agda: error while loading shared libraries: libHSAgda-2.6.4.1-09dc1b9df47955cb7746201b1496a137c6ec49dc27a449ca2b956cfbcaf36039-ghc9.6.3.so:

[andreasabel]

Thanks for digging!

Is your executable built with cabal v1-install dynamically linked or does cabal simply ignore the executable-dynamic setting there?

[andreasabel]

Minimal action: alert of installation failure in documentation.
Maximal action: get rid of Setup.hs.

[andreasabel]

I failed to reproduce the issue here on my mac. I will try to reproduce it in CI.

• #7172

[andreasabel]

Thanks for the alert!
Amazing, on my machine cabal install will always recompile every single source file...

[andreasabel]

@ulidtko : Also succeeds with a fresh cache...: https://github.com/agda/agda/actions/runs/8184356501/job/22378664111?pr=7172

[andreasabel]

@nad: @UlfNorell suggested that we could try the postCopy hook rather than the copyHook when we invoke agda in Setup.hs. https://hackage.haskell.org/package/Cabal-3.10.2.1/docs/Distribution-Simple.html#g:2
Maybe this fixes the cabal v2-install problem with executable-dynamic: True on Linux. Could you try this? (You have a Linux machine, that's why I am asking you.)

[andreasabel]

@ulidtko wrote:

I tried it... Naively, doesn't seem to help, the .so likewise can't be found:

Great may thanks, Maxim, for lending a hand!
Somehow this confirms my suspicion that Ulf's suggestion would not help here.

Or we recommend installation via stack, but this might have its own pitfalls.

Maybe worth a shot, but I have some recollections that e.g. stack install Agda-2.6.4.3 might ignore the 2.6.4.3 request when choosing the resolver and instead use the system default resolver.

• commercialhaskell/stack#6068

My pleas to the Stack Gods were not answered in this case.

[ulidtko]

Hi again @andreasabel, glad to help, and thanks for acknowledging the issue at all 😃

My hunch so far anticipates a trip into cabal rabbit hole... I'll try to contribute in haskell/cabal#9784.

We might warn in the docs about checking for executable-dynamic: True in the .cabal/config.

This sounds perfect 👍