`cabal install Agda` fails in `Setup.hs` with `executable-dynamic: True` in config file (Linux)

[andreasabel]

cabal install Agda fails with executable-dynamic: True in config file:

• cabal install Agda fails with executable-dynamic agda/agda#7163
• Reproducer on Linux: Re #7163: test installing with --enable-executable-dynamic in CI agda/agda#7172

What is puzzling that cabal install Agda --enable-executable-dynamic (instead of setting in the config file) succeeds: https://github.com/agda/agda/actions/runs/8184356501/job/22378664111?pr=7172

Agda fails in the copyHook in its Setup.hs when it tries to invoke the just-built executable: https://github.com/agda/agda/blob/dee0d2e1300b43ac91517c3a5c58cae6b6af3a3d/Setup.hs#L134-L140
This situation has been discussed elsewhere in this issue tracker:

• Change in behaviour in HEAD w.r.t copying and installation of executables in packages with Custom setups #9777

The current issue highlights the discrepancy in behavior between passing the command-line flag and changing the config setting for dynamic linking.

Related:

• the opposite problem, but for ghc-options: -dynamic: v2-build does not pass ghc-options in .cabal/config to ghc when building custom Setup.hs #6505

[alt-romes]

What is puzzling that cabal install Agda --enable-executable-dynamic (instead of setting in the config file) succeeds: https://github.com/agda/agda/actions/runs/8184356501/job/22378664111?pr=7172

The definition of succeeds here is important: does it succeed in building a dynamically linked executable, or does it succeed because the flag is simply ignored? I'm pretty certain it is the latter, since before #9697 command line options to install are simply ignored (where as options in config will be applied)...

[alt-romes]

The current issue highlights the discrepancy in behavior between passing the command-line flag and changing the config setting for dynamic linking.

So, in light of #9697 (and my previous comment), if this is it then the ticket can be closed. However, why does Agda fail when compiled with --enable-executable-dynamic? Is it because of Cabal? Could you please re-phrase the ticket in terms of why exectuable dynamic makes Agda fail to build?

[andreasabel]

The definition of succeeds here is important: does it succeed in building a dynamically linked executable, or does it succeed because the flag is simply ignored?

Indeed, the flag is ignored. Agda isn't linked in dynamically, see: https://github.com/agda/agda/actions/runs/8213327362/job/22464590517?pr=7172

Two more insights:

• on macOS, dynamic linking is not a problem, so the OP does not apply to macOS: https://github.com/agda/agda/actions/runs/8213327362/job/22464590232?pr=7172
• on Windows, with executable-dynamic: True, already installing the dependency alex fails: https://github.com/agda/agda/actions/runs/8213327362/job/22464590326?pr=7172#step:9:258

  Error:     Could not load module ‘Prelude’.
    Perhaps you haven't installed the "dyn" libraries for package ‘base-4.19.1.0’?
  

[ulidtko]

Hi @alt-romes,

why does Agda fail when compiled with --enable-executable-dynamic?

It's because:

1. the just-compiled agda executable gets invoked from Setup hook;
2. to run the (dynamically-linked) executable, the OS must be able to find .so libraries, including libHSAgda*.so;
3. at this point of the build, libHSAgda*.so is under a weird path like /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
   • this path is cumbersome to even talk about; you noticed it too, in Weird store path dir #9654
4. the weird path can't be found by OS — thus we get the fatal error while loading shared libraries.

The usual ways to specify library path are:

• creating a permanent location in /etc/ld.so.conf.d/something.conf;
• setting LD_LIBRARY_PATH environment variable temporarily;
• adding compiler options to bake appropriate RPATH into the executable;
• using patchelf to edit an executable's RPATH post-hoc.

Unfortunately I'm not seeing the ~/.cabal/store/ghc-*/incoming/new-* subdir — is it possible to ask Cabal to not delete it?..

Also notice, that v1-install with --enable-executable-dynamic succeeds on the same package.
I.e. this is only an issue in v2-install.

[alt-romes]

@ulidtko Ah, I see.

Ultimately, I don't think this is Cabal's fault, but rather Agda's use of a custom Setup, which will work in some situations but won't be robust to every one (like with executable-dynamic).

I suspect that the reason why it does not work with v2-install is that the assumptions about the system required for the Custom Setup to be successful in the presence of enable-executable-dynamic do not hold true for the nix-style v2 Cabal, for reasons inherit to its design (e.g. the fact that the whole package is built in this temporary directory before being installed to the store atomically).

[ulidtko]

Can Cabal provide perhaps a "post-atomic-store-install" hook, to enable use-cases like Agda's?