[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate
Sergei Meshveliani
mechvel at botik.ru
Fri Dec 18 13:53:14 CET 2015
On Tue, 2015-12-15 at 08:32 -0500, Andrés Sicard-Ramírez wrote:
> On 14 December 2015 at 16:10, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > You can use the test of DoCon-A-0.03:
> >
> > http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/
>
> DoCon-A-0.03 doesn't type-check with the development version (i.e. the
> master branch), so it's not possible to test Jesper's new unifier.
>
> >
> > I am not sure that I would try it now, because it is very difficult to
> > advance the project when trying different tool versions.
> >
>
> It's not difficult to test Jesper's new unifier. By running
>
> $ git clone https://github.com/jespercockx/agda.git agda-unification
> $ cd agda-unification
> $ git checkout --track origin/unification
> $ make install-bin
>
> you get a version of Agda including Jesper' new unifier (Agda 2.5).
> After type-checking you code, you remove the agda-unification
> directory and you re-install Agda from your current directory.
>
I have managed now to install this on a machine with ghc-7.10.2.
I use Development Standard library of December 18, 2015.
Then, applying
agda $agdaLibOpt +RTS -M... -RTS List/Sorting.agda
to my program, I observe that Agda first type-checks Standard library.
At this stage it reports
-----------------------------------------------
Checking Data.Bin
(/home/mechvel/agda/stLib/dec18-2015/src/Data/Bin.agda).
Finished Data.Bin.
Checking Data.List.All.Properties
(/home/mechvel/agda/stLib/dec18-2015/src/Data/List/All/Properties.agda).
/home/mechvel/agda/stLib/dec18-2015/src/Data/List/All/Properties.agda:140,8-14
Failed to solve the following constraints:
[1147] (x₁ ∷ xs₂) = (_740 ext x xs ¬p) : (List (_738 ext x xs ¬p))
when checking that the pattern (here p) has type
(Any (_739 ext x xs ¬p) (_740 ext x xs ¬p))
------------------------------------------------
So, agda-unification is not compatible with
Development Standard library of December 18, 2015
(?)
Regards,
------
Sergei
More information about the Agda
mailing list