[ news ] Announce release of Idris2 v0.8.0

Idris2 version 0.8.0 has been released almost 2 years after the previous
release.  This puts the tarball on the website, alongside a little
announcement for folk who follow the atom feed or who check the website
for news.

The tarball and its SHA256-checksum are different from the ones found on
GitHub, because the `mkdist.sh` script removes some unnecessary files
and directories before bundling.

Author: CodingCellist

src/content/pages/download.rst

@@ -29,16 +29,16 @@ If you already use ``pack``, you can update your Idris version to the latest ver
 in development by using ``pack switch latest`` ([#f1]_). If you wish to use a specific
 release with ``pack``, currently the only way to do this is to find the release
 date, and then switch to its nightly collection by using, for example,
-``pack switch nightly-231222`` (which would switch to the 0.7.0 release).
+``pack switch nightly-251031`` (which would switch to the 0.8.0 release).
 
-The latest formally released version is Idris2-0.7.0,
-`released 2023-12-22 <{filename}../posts/idris2-0-7-0-released.rst>`_,
+The latest formally released version is Idris2-0.8.0,
+`released 2025-10-31 <{filename}../posts/idris2-0-8-0-released.rst>`_,
 with its associated source tarball, which could alternatively be used for
 installation, forgoing ``pack`` (packages would have to be managed manually, via
 scripts, or via other software):
 
-* `idris2-0.7.0.tgz <{static}../releases/idris2-0.7.0.tgz>`_
-  `(SHA 256 hash) <{static}../releases/idris2-0.7.0.tgz.sha256>`__
+* `idris2-0.8.0.tgz <{static}../releases/idris2-0.8.0.tgz>`_
+  `(SHA 256 hash) <{static}../releases/idris2-0.8.0.tgz.sha256>`__
 
 Both ``pack`` and the release tarball include generated Scheme sources
 sufficient for bootstrapping, so you don't need an existing Idris 2 system to
@@ -51,6 +51,8 @@ You can always find the latest development version `on github
 
 Previous releases are also available:
 
+* `idris2-0.7.0.tgz <{static}../releases/idris2-0.7.0.tgz>`_
+  `(SHA 256 hash) <{static}../releases/idris2-0.7.0.tgz.sha256>`__
 * `idris2-0.6.0.tgz <{static}../releases/idris2-0.6.0.tgz>`_ `(SHA 256 hash) <{static}../releases/idris2-0.6.0.tgz.sha256>`__
 * `idris2-0.5.1.tgz <{static}../releases/idris2-0.5.1.tgz>`_ `(SHA 256 hash) <{static}../releases/idris2-0.5.1.tgz.sha256>`__
 * `idris2-0.4.0.tgz <{static}../releases/idris2-0.4.0.tgz>`_ `(SHA 256 hash) <{static}../releases/idris2-0.4.0.tgz.sha256>`__

src/content/posts/idris2-0-8-0-released.rst

@@ -0,0 +1,44 @@
+Idris 2 version 0.8.0 Released
+##############################
+
+:date: 2025-10-31 21:00
+:tags: Release
+:category: News
+:author: CodingCellist
+
+A new version (0.8.0) of Idris 2 has been released. You can download the source
+(including generated Scheme and Racket files for bootstrapping) from the
+`download page <{filename}../pages/download.rst>`_.
+
+Highlights include:
+
+* Autobind and Typebind modifier on operators allow the user to customise the
+  syntax of operator to look more like a binder.
+* Totality checking will now look under data constructors, so ``Just xs`` will
+  be considered smaller than ``Just (x :: xs)``.
+* `Typst <https://typst.app/>`_ files can be compiled as Literate Idris.
+* Constructors with certain tags (``CONS``, ``NIL``, ``JUST``, ``NOTHING``) are
+  replaced with ``_builtin.<TAG>`` (eg ``_builtin.CONS``).  This allows the
+  identity optimisation to optimise conversions between list-shaped things.
+* Refactored ``Uninhabited`` implementation for ``Data.List.Elem``,
+  ``Data.List1.Elem``, ``Data.SnocList.Elem``, and ``Data.Vect.Elem`` so it can
+  be used for homogeneous (``===``) and heterogeneous (``~=~``) equality.
+* The ``RefC`` backend compiler can emit precise reference counting instructions
+  where a reference is dropped as soon as possible. This allows you to reuse
+  unique variables and optimize memory consumption.
+* Fix memory leaks of ``IORef`` in ``RefC`` backend.  Now that ``IORef`` holds
+  values by itself, ``global_IORef_Storage`` is no longer needed.
+* The NodeJS executable output to ``build/exec/`` now has its executable bit
+  set.  That file already had a NodeJS shebang at the top, so now it is fully
+  ready to go after compilation.
+
+For a detailed list of changes, see the
+`CHANGELOG <https://github.com/idris-lang/Idris2/blob/15a3e4e70843f7a34100f6470c04b791330788df/CHANGELOG.md>`_.
+
+Thanks to the many people who have contributed, both old and new, whether by
+adding features, fixing code, reporting issues, or anything else. You can find a
+list of
+`contributors <https://github.com/idris-lang/Idris2/blob/15a3e4e70843f7a34100f6470c04b791330788df/CONTRIBUTORS>`_
+in the `GitHub repository <https://github.com/idris-lang/Idris2>`_.
+
+Happy Hallowe'en! Have fun!

src/content/releases/idris2-0.8.0.tgz

@@ -0,0 +1 @@
+940a283cb66b0097cab0d24fe10341274fab75cb3af58dc715944d6ca7230665  idris2-0.8.0.tgz