<div dir="ltr"><div>I'm not sure what made the memory usage spike in 2.5.4, but I've made a pull request [1] fixing the problem in your code.</div><div>Om my machine it now checks in 7s instead of 45s.<br></div><div><br></div><div>/ Ulf</div><div><br></div><div>[1] <a href="https://github.com/Rotsor/Primes/pull/1">https://github.com/Rotsor/Primes/pull/1</a><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 26, 2018 at 5:19 AM, Arseniy Alekseyev <span dir="ltr"><<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I tried the RC on my <a href="https://github.com/Rotsor/Primes" target="_blank">Primes</a> repo and the new version is much more memory-hungry (I want to say ~2x) and slightly slower (~60 seconds instead of 53) compared to Agda 2.5.3.<div><br></div><div>It's totally unimportant to have this specific thing work well, but I thought people might find the slowdown surprising.</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 25 May 2018 at 20:26, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 25 May 2018 at 12:56, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br>
> On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:<br>
</span><span>>> The Agda Team is very pleased to announce the first release candidate<br>
>> of Agda 2.5.4. We plan to release 2.5.4 in one week.<br>
>><br>
><br>
><br>
> Can you please delay it a bit?<br>
<br>
</span>We have decided not to release Agda 2.5.4 this week but next week.<br>
<span class="m_2611526353717044428HOEnZb"><font color="#888888"><br>
-- <br>
Andrés<br>
</font></span><div class="m_2611526353717044428HOEnZb"><div class="m_2611526353717044428h5">______________________________<wbr>_________________<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/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>