[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Jesper Cockx]

You need to run the 'git pull' command in the main agda-unification
directory.

The problem with the standard library is because of one of the problems I
mentioned in the other thread about my new unifier (about the solution of
metavariables during unification). I now pushed another patch that reverts
to the default Agda behaviour. This fixes the issue with the standard
library, so if you pull the new version now you should be able to typecheck
it.

Jesper

On Fri, Dec 18, 2015 at 2:00 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Fri, 2015-12-18 at 13:48 +0100, Jesper Cockx wrote:
> > I pushed a patch to my branch that should fix compilation with GHC
> > <7.10. Can you please pull this patch (with 'git pull') and try
> > installing again?
> >
>
>
> In what directory need I to command
>
>    > git pull
>
> ?
>
> Also, please, read my last letter about  agda-unification
> and  Development Standard library of December 18
> (this is for another attempt, for a machine with ghc-7.10.2).
>
> ------
> Sergei
>
>
>
>
> >
> > On Fri, Dec 18, 2015 at 1:10 PM, Sergei Meshveliani <mechvel at botik.ru>
> > wrote:
> >         On Tue, 2015-12-15 at 18:11 -0500, Andrés Sicard-Ramírez wrote
> >
> >         (about installing the  agda-unification  version):
> >
> >
> >         > On 15 December 2015 at 15:23, Sergei Meshveliani
> >         <mechvel at botik.ru> wrote:
> >         > > Installed regex-tdfa-text-1.0.0.3
> >         > > cabal: Error: some packages failed to install:
> >         > > Agda-2.5 depends on clock-0.6.0.1 which failed to install.
> >         >
> >         > GHC version?
> >
> >
> >         7.8.3
> >
> >
> >         > regex-tdfa-text is needed by the Cabal test-suite. You can
> >         avoid to
> >         > install this test-suit using
> >         >
> >         >   $ make install-bin CABAL_OPTS=--disable-tests
> >         >
> >
> >         This end with
> >
> >         ---------------------------
> >         ...
> >
> >         [246 of 331] Compiling Agda.TypeChecking.Rules.LHS.Problem
> >         ( src/full/Agda/TypeChecking/Rules/LHS/Problem.hs,
> >         dist-2.5/build/Agda/TypeChecking/Rules/LHS/Problem.o )
> >
> >         src/full/Agda/TypeChecking/Rules/LHS/Problem.hs:65:10:
> >             Not in scope: type constructor or class ‘Monoid’
> >             Perhaps you meant ‘Monad’ (imported from Prelude)
> >         ---------------------------
> >
> >
> >         ------
> >         Sergei
> >
> >
> >         _______________________________________________
> >         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/20151218/04ad1caf/attachment.html