[Agda] Building Agda on GHC 7.9

kyra kyrab at mail.ru
Mon Mar 31 07:49:13 CEST 2014


More specifically, it's geniplate, which wants TH-2.8 here, so it is 
necessary to install geniplate separately, changing it's .cabal file.

Kyra

On 3/30/2014 23:39, Ulf Norell wrote:
> 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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda



More information about the Agda mailing list