More agressive `with` in Agda 2.4.3 [Re: [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!]

[Sergei Meshveliani]

I have tested this  2.4.3+issue1692  on the current DoCon-A application
(a large program, which uses `with' widely). 
The type check is all right.

------
Sergei 


On Mon, 2015-11-23 at 10:24 +0100, Andreas Abel wrote:
> Thanks for all the replies I got so far!
> 
> It seems that many use Agda 2.4.3 (master development branch) already, 
> so I merged my changes into a fork of the master branch.  Here are the 
> installation instructions for 2.4.3+issue1692:
> 
>    git clone https://github.com/andreasabel/agda-issue-1692.git
>    cd agda-issue-1692
>    # by default, we are on the master branch in a fresh clone
>    make install-bin
> 
> Cheers,
> Andreas
> 
> On 19.11.2015 14:16, Andreas Abel wrote:
> > Dear Agda users and developers,
> >
> > please check your larger Agda-2.4.2 developments with the version at
> >
> >    https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2
> >
> > You can get it with
> >
> >    git clone https://github.com/andreasabel/agda-issue-1692.git
> >    cd agda-issue-1692
> >    git checkout maint-2.4.2
> >    make install-bin
> >
> > This version is making `with` more agressive and hopefully more
> > intuitive (at least it removes the stumbling block reported in issue
> > #1692).
> >
> > The change is not fully backwards compatible. However, the breakage
> > should be small. Nothing broke for the std-lib. Only a single test case
> > broke, which uses with on a function argument (a variable):
> > https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99
> >
> > The breakage was easy to fix, the new `with` is simpler: the `with` on
> > the variable could be removed.
> >
> > Please check the amount of breakage on your Agda developments and report
> > back, with self-contained test-cases (e.g. as tar-balls and repo links) on
> >
> >    https://github.com/agda/agda/issues/1692
> >
> > This let's me evaluate whether this commit can go into the maintenance
> > version or not (in case the breakage is too big).
> >
> > Response time: 5 work days.
> >
> > Cheers,
> > Andreas
> >
> 
>