[Agda] Building Agda on GHC 7.9

Ulf Norell ulf.norell at gmail.com
Sun Mar 30 21:39:47 CEST 2014


You always need the template-haskell that comes with the compiler, so you
should change Agda.cabal to allow your installed template-haskell.

/ Ulf


On Sun, Mar 30, 2014 at 5:57 PM, Mateusz Kowalczyk
<fuuzetsu at fuuzetsu.co.uk>wrote:

> Hi,
>
> I'm trying to look into http://trac.haskell.org/haddock/ticket/295 but I
> can't build darcs version of Agda with GHC 7.9 so that I can actually
> try and fix the issue with current Haddock.
>
> Does anyone have tips on getting Agda to compile? Is there just no
> incentive to have Agda compile with 7.9 at all? I am using darcs version
> of Agda, the Hackage version would not even begin to compile due to
> version bounds.
>
> The error is below:
>
> Preprocessing library template-haskell-2.8.0.0...
> [1 of 6] Compiling Language.Haskell.TH.Syntax (
> Language/Haskell/TH/Syntax.hs,
> dist/dist-sandbox-a07c4207/build/Language/Haskell/TH/Syntax.o )
>
> Language/Haskell/TH/Syntax.hs:721:37:
>     Couldn't match expected type ‘Bool’ with actual type ‘Int#’
>     In the expression: u1 <# u2
>     In a stmt of a pattern guard for
>                    an equation for ‘compare’:
>       u1 <# u2
>     In an equation for ‘compare’:
>         (NameU u1) `compare` (NameU u2)
>           | u1 <# u2 = LT
>           | u1 ==# u2 = EQ
>           | otherwise = GT
>
> Language/Haskell/TH/Syntax.hs:722:37:
>     Couldn't match expected type ‘Bool’ with actual type ‘Int#’
>     In the expression: u1 ==# u2
>     In a stmt of a pattern guard for
>                    an equation for ‘compare’:
>       u1 ==# u2
>     In an equation for ‘compare’:
>         (NameU u1) `compare` (NameU u2)
>           | u1 <# u2 = LT
>           | u1 ==# u2 = EQ
>           | otherwise = GT
>
> Language/Haskell/TH/Syntax.hs:729:37:
>     Couldn't match expected type ‘Bool’ with actual type ‘Int#’
>     In the expression: u1 <# u2
>     In a stmt of a pattern guard for
>                    an equation for ‘compare’:
>       u1 <# u2
>     In an equation for ‘compare’:
>         (NameL u1) `compare` (NameL u2)
>           | u1 <# u2 = LT
>           | u1 ==# u2 = EQ
>           | otherwise = GT
>
> Language/Haskell/TH/Syntax.hs:730:37:
>     Couldn't match expected type ‘Bool’ with actual type ‘Int#’
>     In the expression: u1 ==# u2
>     In a stmt of a pattern guard for
>                    an equation for ‘compare’:
>       u1 ==# u2
>     In an equation for ‘compare’:
>         (NameL u1) `compare` (NameL u2)
>           | u1 <# u2 = LT
>           | u1 ==# u2 = EQ
>           | otherwise = GT
> Failed to install template-haskell-2.8.0.0
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140330/49b9c6c0/attachment.html


More information about the Agda mailing list