[Agda] installing agda-2.4.2.3

[Jacques Carette]

1. do make sure you have the 'right' cabal in your path, i.e. issue
cabal --version
and make sure it is the version you installed.

2. also update happy and alex before install Agda.  [Why cabal does not 
do this mystifies me]

And then try again.

On 2015-07-27 6:36 AM, Sergei Meshveliani wrote:
> On Sun, 2015-07-26 at 17:43 -0500, Andrés Sicard-Ramírez wrote:
>> On 26 July 2015 at 13:30, Sergei Meshveliani <mechvel at botik.ru> wrote:
>>>> cabal install cabal-install
>> I suggest to run the above command with a previous version of GHC.
>>
> 1. I command now
>
>    > cabal install cabal-install
>
> under  ghc-7.8.2.  And it succeeds.
>
> 2. Then I return to  ghc-7.10.1,  and command
>
>    > cabal install Agda
>
> to install  Agda-2.4.2.3.
> First, it installs many packages, and then, reports
>
> -----------------------------------------------------------------
> ...
> ...
> [19 of 22] Compiling Language.Haskell.Exts.InternalParser
> ( dist/build/Language/Haskell/Exts/InternalParser.hs,
> dist/build/Language/Haskell/Exts/InternalParser.o )
>
> templates/GenericTemplate.hs:104:22:
>      Couldn't match expected type ‘Bool’
>                  with actual type ‘Happy_GHC_Exts.Int#’
>      In the expression:
>        (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#))
>      In a stmt of a pattern guard for
>                     a case alternative:
>        (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#))
>      In a case alternative:
>          n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#))
>            -> (happyReduceArr Happy_Data_Array.! rule) i tk st
>            where
>                rule
>                  = (Happy_GHC_Exts.I#
>                       ((Happy_GHC_Exts.negateInt#
>                           ((n Happy_GHC_Exts.+# (1# ::
> Happy_GHC_Exts.Int#))))))
> ...
> ...
>
> templates/GenericTemplate.hs:219:14:
>      Pattern bindings containing unlifted types should use an outermost
> bang pattern:
>        (sts1@((HappyCons (st1@(action)) (_))))
>          = happyDrop k (HappyCons (st) (sts))
>      In an equation for ‘happyMonad2Reduce’:
>          happyMonad2Reduce k nt fn j tk st sts stk
>            = happyThen1
>                (fn stk tk)
>                (\ r -> happyNewToken new_state sts1 (r `HappyStk`
> drop_stk))
>            where
>                (sts1@((HappyCons (st1@(action)) (_))))
>                  = happyDrop k (HappyCons (st) (sts))
>                drop_stk = happyDropStk k stk
>                (off) = indexShortOffAddr happyGotoOffsets st1
>                (off_i) = (off Happy_GHC_Exts.+# nt)
>                ....
>
> Failed to install haskell-src-exts-1.16.0.1
> cabal: Error: some packages failed to install:
> ...
> ---------------------------------------------------------------------------
>
>
> I wonder, how to fix.
> Regards,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda