[Agda] problem installing agda (template Haskell ?)
Thorsten Altenkirch
Thorsten.Altenkirch at nottingham.ac.uk
Fri May 24 09:37:26 CEST 2019
Yes thank you - I came to the same conclusion and installed a more recent version of ghost and it worked.
I was confused because I was using the same version of ghc recently without problems but some changes triggered a reinstall of packages that didn’t compile anymore.
Sorry for missing the obvious.
Thorsten
Sent from my iPhone
On 24 May 2019, at 08:34, Liang-Ting Chen <liang.ting.chen.tw at gmail.com<mailto:liang.ting.chen.tw at gmail.com>> wrote:
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<mailto: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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda
--
Best regards,
Liang-Ting
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190524/5d023f5c/attachment.html>
More information about the Agda
mailing list