[Agda] problem installing agda (template Haskell ?)

[Liang-Ting Chen]

Hi Thorsten,

It seems that there is a bug in GHC 8.0.? hit by the recent commits as
there is also another issue on GitHub

https://github.com/agda/agda/issues/3792

when Agda is compiled with 8.0.2.

I have compiled successfully the latest Agda with GHC 8.6.5 using stack on
a macOS 10.14.4. Hope this helps.

Best regards,
Liang-Ting

On Wed, 22 May 2019 at 16:30, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Hi guys,
>
>
>
> Has anybody encountered a problem installing agda in the moment? Cabal
> install fails with some error messages to do with template Haskell. First
> it says
>
>
>
> Use --force-reinstalls if you want to install anyway.
>
>
>
> But when I do it it runs into an error
>
>
>
> Building geniplate-mirror-0.7.6...
>
> Preprocessing library geniplate-mirror-0.7.6...
>
> [1 of 1] Compiling Data.Generics.Geniplate ( Data/Generics/Geniplate.hs,
> dist/dist-sandbox-d9c30c4b/build/Data/Generics/Geniplate.o )
>
>
>
> Data/Generics/Geniplate.hs:264:33: error:
>
>     • Can't find interface-file declaration for type constructor or class
> Language.Haskell.TH.Lib.ExpQ
>
>         Probable cause: bug in .hi-boot file, or inconsistent .hi file
>
>         Use -ddump-if-trace to get an idea of which file caused the error
>
>
>
> …
>
>
>
> I am using
>
> sean:agda txa$ ghc --version
>
> The Glorious Glasgow Haskell Compilation System, version 8.0.1
>
> on a mac and the latest version of the agda repo.
>
>
>
> I attach a dump from the terminal. I tried this on 2 different machines.
>
>
>
> Thorsten
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190522/442330a2/attachment.html>