Can't build agda2hs with recent GHC version(s)

[abailly]

I am trying to install agda2hs following the tutorial and failed no matter which way I tried:

• doing cabal install agda2hs
• cloning and building it locally
• using GHC 9.8.2, 9.6.3, 9.6.6
• within or without nix shell
• at master or at tag v1.3

The error I get is

[147 of 433] Compiling Agda.Syntax.Parser.Parser ( dist/build/Agda/Syntax/Parser/Parser.hs, dist/build/Agda/Syntax/Parser/Parser.o, dist/build/Agda/Syntax/Parser/Parser.dyn_o )

dist/build/Agda/Syntax/Parser/Parser.hs:8298:12: error: [GHC-76037]
    Not in scope: ‘Prelude.null’
    Suggested fixes:
      • Perhaps use one of these:
          ‘Prelude.all’ (imported from Prelude),
          ‘Prelude.not’ (imported from Prelude),
          ‘Prelude.sum’ (imported from Prelude)
      • Perhaps you want to remove ‘null’ from the explicit hiding list
        in the import of ‘Prelude’
        (dist/build/Agda/Syntax/Parser/Parser.hs:41:1-30).
     |
8298 |         if Prelude.null catch_frames_new
     |            ^^^^^^^^^^^^

dist/build/Agda/Syntax/Parser/Parser.hs:8309:13: error: [GHC-76037]
    Not in scope: ‘Prelude.null’
    Suggested fixes:
      • Perhaps use one of these:
          ‘Prelude.all’ (imported from Prelude),
          ‘Prelude.not’ (imported from Prelude),
          ‘Prelude.sum’ (imported from Prelude)
      • Perhaps you want to remove ‘null’ from the explicit hiding list
        in the import of ‘Prelude’
        (dist/build/Agda/Syntax/Parser/Parser.hs:41:1-30).
     |
8309 |             Prelude.null (Prelude.filter (\(HappyCons _ (HappyCons h _),_) -> EQ(st,h)) catch_frames)
     |             ^^^^^^^^^^^^

What am I doing wrong?

[jespercockx]

This seems to be a problem with installing the Agda prerequisite of agda2hs, not agda2hs itself. Probably the problem is the bad release of happy-2.1.1, as reported in https://github.com/agda/agda/issues/7585. Since this version has now been deprecated, I think it would be sufficient to do a cabal update so Cabal knows not to install it?

[abailly]

I honestly did not thought about cabal update as the error seemed to point to something from Prelude and I thought this could be an issue with base package and ghc versions.

[abailly]

So it goes over the aforementioned issue, but then fails with

[429 of 429] Compiling Agda.Main        ( src/full/Agda/Main.hs, dist/build/Agda/Main.o, dist/build/Agda/Main.dyn_o )
Installing library in /Users/arnaudbailly/.cabal/store/ghc-9.6.6/incoming/new-83847/Users/arnaudbailly/.cabal/store/ghc-9.6.6/Agd-2.6.4.3-ce06ac54/lib
Generating Agda library interface files...
dist/build/agda/agda: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
Error: [Cabal-7125]
Failed to build Agda-2.6.4.3 (which is required by exe:agda2hs from agda2hs-1.2). See the build log above for details.

[jespercockx]

It seems to be complaining that it cannot find an agda executable in dist/build/agda (despite the fact that it should just have installed it there), weird. Which version of Cabal are you using? Also, please try installing agda2hs 1.3 (instead of 1.2) since that relies on Agda 2.7.0.1 which might include some fixes relative to 2.6.4.3.