<div dir="ltr"><div><div>You need to run the 'git pull' command in the main agda-unification directory.<br><br></div>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.<br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Dec 18, 2015 at 2:00 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, 2015-12-18 at 13:48 +0100, Jesper Cockx wrote:<br>
> I pushed a patch to my branch that should fix compilation with GHC<br>
> <7.10. Can you please pull this patch (with 'git pull') and try<br>
> installing again?<br>
><br>
<br>
<br>
</span>In what directory need I to command<br>
<br>
> git pull<br>
<br>
?<br>
<br>
Also, please, read my last letter about agda-unification<br>
and Development Standard library of December 18<br>
(this is for another attempt, for a machine with ghc-7.10.2).<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
><br>
> On Fri, Dec 18, 2015 at 1:10 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
> On Tue, 2015-12-15 at 18:11 -0500, Andrés Sicard-Ramírez wrote<br>
><br>
> (about installing the agda-unification version):<br>
><br>
><br>
> > On 15 December 2015 at 15:23, Sergei Meshveliani<br>
> <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> > > Installed regex-tdfa-text-1.0.0.3<br>
> > > cabal: Error: some packages failed to install:<br>
> > > Agda-2.5 depends on clock-0.6.0.1 which failed to install.<br>
> ><br>
> > GHC version?<br>
><br>
><br>
> 7.8.3<br>
><br>
><br>
> > regex-tdfa-text is needed by the Cabal test-suite. You can<br>
> avoid to<br>
> > install this test-suit using<br>
> ><br>
> > $ make install-bin CABAL_OPTS=--disable-tests<br>
> ><br>
><br>
> This end with<br>
><br>
> ---------------------------<br>
> ...<br>
><br>
> [246 of 331] Compiling Agda.TypeChecking.Rules.LHS.Problem<br>
> ( src/full/Agda/TypeChecking/Rules/LHS/Problem.hs,<br>
> dist-2.5/build/Agda/TypeChecking/Rules/LHS/Problem.o )<br>
><br>
> src/full/Agda/TypeChecking/Rules/LHS/Problem.hs:65:10:<br>
> Not in scope: type constructor or class ‘Monoid’<br>
> Perhaps you meant ‘Monad’ (imported from Prelude)<br>
> ---------------------------<br>
><br>
><br>
> ------<br>
> Sergei<br>
><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br></div>