<div dir="ltr">agda-prelude: no breakage<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 19, 2015 at 2:16 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda users and developers,<br>
<br>
please check your larger Agda-2.4.2 developments with the version at<br>
<br>
<a href="https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2" rel="noreferrer" target="_blank">https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2</a><br>
<br>
You can get it with<br>
<br>
git clone <a href="https://github.com/andreasabel/agda-issue-1692.git" rel="noreferrer" target="_blank">https://github.com/andreasabel/agda-issue-1692.git</a><br>
cd agda-issue-1692<br>
git checkout maint-2.4.2<br>
make install-bin<br>
<br>
This version is making `with` more agressive and hopefully more intuitive (at least it removes the stumbling block reported in issue #1692).<br>
<br>
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):<br>
<a href="https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99</a><br>
The breakage was easy to fix, the new `with` is simpler: the `with` on the variable could be removed.<br>
<br>
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<br>
<br>
<a href="https://github.com/agda/agda/issues/1692" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1692</a><br>
<br>
This let's me evaluate whether this commit can go into the maintenance version or not (in case the breakage is too big).<br>
<br>
Response time: 5 work days.<br>
<br>
Cheers,<br>
Andreas<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</font></span></blockquote></div><br></div>