[Agda] installing agda-2.4.2.3

Sergei Meshveliani mechvel at botik.ru
Mon Jul 27 12:36:37 CEST 2015


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




More information about the Agda mailing list