On Mon, Sep 07, 2020 at 09:50:51AM -0400, Timothy Sample wrote: > Hi Jakub, > > Jakub Kądziołka writes: > > > I am trying to set up Agda, and I have reduced it to a simpler problem: > > > > $ cat test.hs > > import Numeric.IEEE > > > > main = return () > > $ genv --pure --ad-hoc ghc@8.6 ghc-ieee754 gcc-toolchain > > % ghc test.hs > > Linking test ... > > ld: cannot find -lHSieee754-0.8.0-IfCS1Dp7pQVIOQRslM6kD > > collect2: error: ld returned 1 exit status > > `gcc' failed in phase `Linker'. (Exit code: 1) > > > > How can I fix this error? Am I doing something wrong, or is this a > > packaging bug? > > GHC needs a special flag to link shared libraries. We recently starting > building shared libraries for our Haskell packages. The static ones are > still being built, but they go to a separate output. I think you can > fix your problem in one of two ways: > > 1. Pass the “-dynamic” flag to GHC (and maybe “-fPIC”); > 2. Use “ghc-ieee754:static”. ghc-ieee754:static doesn't seem to exist, but passing -dynamic does indeed work. The workaround also translates to Agda, with $ agda --ghc-flag=-dynamic --compile hello-world.agda I'd really rather this wasn't necessary, though. I can already imagine having to figure out how to pass this flag to agda through build systems and editor plugins. On a related note, shouldn't it be possible to use agda without specifying ghc (and transitively, gcc) in your profile? Regards, Jakub Kądziołka