Regression in cabal-3.12.1.0: cabal install --lib Adga no longer works.

[andreasabel]

Downstream issue: agda/agda#7401
cabal-3.10.3.0 install --lib Agda still works.
cabal-3.12.1.0 communicates a wrong build dir to Agda's Setup.hs:

dist/build/agda/agda: readCreateProcess: posix_spawnp: does not exist (No such file or directory)

https://github.com/agda/agda/blob/5da3f3f2be5fc0d4ed6a2b828bd751e44e29292f/Setup.hs#L92-L101

P.S.: Here is a MWE showing the difference between 3.10 and 3.12: https://github.com/andreasabel/cabal-issue-10235/actions/runs/10163928863/job/28108067382

[JaSpa]

I think the passed build directory is fine. But looking at the build logs you can see that

• cabal 3.10 builds the library and the two executables (agda-mode, agda) defined in the package
• cabal 3.12 builds only the library

The install step with cabal 3.12 then fails because the agda executable simply doesn't exist.

This happens either when using cabal install --lib Agda or when Agda appears as a dependency in build-depends.

[andreasabel]

@JaSpa: Thanks for the analysis and figuring out the root cause!

I think issues like this one are the reasons that stack always builds all components regardless what the user commanded.

We can now speculate as to whether this was an intended change in cabal install --lib or an accidental one. I guess the latter, since the changelog does not mention any change, at least not explicitly: https://github.com/haskell/cabal/blob/356c2f4cc8d205de4b79c28e287735f457924ab4/release-notes/cabal-install-3.12.1.0.md

[sheaf]

I believe this is the same issue as #9777, which tracks with what @JaSpa reports in #10235 (comment).

[gbaz]

This seems very tricky to disentangle, because to "complete" the install of the agda lib, the executable is presumed to be already built. Is it possible to move the generate-interfaces portion of the setup.hs to the hooks of the agda executable? what would be the consequences?

[andreasabel]

Agda's Setup.hs calls the agda executable to generate interface files (*.agdai) for the Agda core modules.
The idea is that if you cabal install Agda in sudo mode, you are in sudo mode when writing these interface files, so they can be written into root space along with the rest of the Agda binaries and data files.
Moving this code into the Agda executable would make the Agda installation a two-step process, rather than a single call to cabal. E.g. packagers would have to change their routine for packaging Agda.

[sheaf]

@andreasabel I'm trying to better understand the needs of the Agda package.

I don't understand why it is not sufficient to only install the Agda standard library interface files when the executable is installed, and not when the library is installed.

If it is indeed the case that you only need the Agda interface files for the executable, then I would think updating the Agda Setup.hs script to only install them when one wants the executable should suffice. Something like the following (somewhat simplified from the actual Agda Setup.hs):

copyHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> CopyFlags -> IO ()
copyHook' pd lbi hooks flags = do
  copyHook simpleUserHooks pd lbi hooks flags
  when (wantInterfaces flags) $ do
    generateInterfaces pd lbi
    copyHook simpleUserHooks pd lbi hooks flags

wantInterfaces :: CopyFlags -> Bool
wantInterfaces _flags =
#if MIN_VERSION_Cabal(3,11,0)
  any isAgdaExe (copyArgs _flags)
    where
      isAgdaExe "exe:agda" = True
      isAgdaExe _ = False
#else
  True
#endif

I think this would be an improvement for people who depend on Agda, as it means that:

• if you depend on the library, you don't need to build the executable,
• if you have a build-tool-depends on Agda, you will get the interface files as expected.

With this approach, you can still install both the library and executable in a single invocation of cabal-install, so I don't think the user experience regresses. So it seems to me that this is a better way forward than simply reverting the change in Cabal (although that change will still need to be documented). I hope you agree.

[gbaz]

Moving this code into the Agda executable would make the Agda installation a two-step process, rather than a single call to cabal. E.g. packagers would have to change their routine for packaging Agda.

Sorry, I meant perhaps moving the generate-interfaces portion of the setup into the executable install section of the setup.hs script not just the executable per-se. So when you generated the executable, it would be in the post-hook for the executable build that files were built, where you could be guaranteed the executable was already built. But this would still all be invoked by cabal install Agda.

[andreasabel]

@gbaz: Which of the hooks would that be? https://downloads.haskell.org/ghc/latest/docs/libraries/Cabal-3.12.0.0-0d16/Distribution-Simple-UserHooks.html

[alt-romes]

I'm going to close this in favour of #9777, which should be fixed by #10311 plus agda/agda#7471 (which fixes this one more directly, upstream.)