<meta http-equiv="Content-Type" content="text/html; charset=utf-8"><div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Dear all,<br>
<br>
The Agda Team is very pleased to <span class="gmail-il">announce</span> a release candidate of Agda 2.6.2. We plan to release 2.6.2 in a few days.<br>
</div><div><br></div><div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"># Highlights<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">* Several improvements and bug-fixes related to Run-time Irrelevance (<a href="https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html">https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html</a>).<br><br>* Several improvements and bug-fixes related to the JavaScript Backend (<a href="https://agda.readthedocs.io/en/latest/tools/compilers.html#javascript-backend">https://agda.readthedocs.io/en/latest/tools/compilers.html#javascript-backend</a>).<br><br>* Added experimental support for Guarded Cubical Agda (<a href="https://agda.readthedocs.io/en/latest/language/guarded-cubical.html">https://agda.readthedocs.io/en/latest/language/guarded-cubical.html</a>).<br><br>* The Primitive Sorts (<a href="https://agda.readthedocs.io/en/latest/language/built-ins.html#sorts">https://agda.readthedocs.io/en/latest/language/built-ins.html#sorts</a>) of Agda (`Set` and `Prop`) are no longer keywords and can be renamed when importing `Agda.Primitive`.<br><br>* Added native support for the Inspect Idiom (<a href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-abstraction-equality">https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-abstraction-equality</a>).<br><br>* Added support for making System Calls (<a href="https://agda.readthedocs.io/en/latest/language/reflection.html#system-calls">https://agda.readthedocs.io/en/latest/language/reflection.html#system-calls</a>) from the reflection API.<br></div></div><div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"># GHC supported versions<br>
<br>
Agda 2.6.2 RC has been tested with GHC 9.0.1, 8.10.4, 8.8.4, 8.6.5, 8.4.4, 8.2.2 and 8.0.2 on Linux, macOS and Windows.</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"># Installation<br><br>
Agda 2.6.2 RC can be installed using cabal-install or stack:<br>
</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">* Getting the release candidate<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    $ cabal get <a href="http://hackage.haskell.org/package/Agda-2.6.1.3.20210524/candidate/Agda-2.6.1.3.20210524.tar.gz">http://hackage.haskell.org/package/Agda-2.6.1.3.20210524/candidate/Agda-2.6.1.3.20210524.tar.gz</a></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    $ cd Agda-2.6.1.3.20210524.tar.gz
</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">* Using cabal-install<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    $ cabal install</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">* Using stack</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    $ stack --stack-yaml stack-a.b.c.yaml install</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">replacing `a.b.c` with your version of GHC.<br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"># Standard library<br><br>
For the time being, you can use the *experimental* branch of the standard library with Agda 2.6.2 RC. This branch is available at</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    <a href="https://github.com/agda/agda-stdlib/">https://github.com/agda/agda-stdlib/</a></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"># Fixed issues</div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">    <a href="http://hackage.haskell.org/package/Agda-2.6.1.3.20210524/candidate/changelog">http://hackage.haskell.org/package/Agda-2.6.1.3.20210524/candidate/changelog</a></div></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default">Enjoy Agda 2.6.2 RC and please test as much as possible.</div><div><br><div style="font-family:arial,helvetica,sans-serif;font-size:small" class="gmail_default"><br></div>-- <br></div><br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">Andrés<span class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">,  on behalf of the Agda Team</span></div></div>