# \[ANN\] Agda 2.6.4 released

**URL:** <https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810>\
**Category:** Announcements\
**Created:** [October 6, 2023, 1:56pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810 "2023-10-06T13:56:35Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![andreasabel](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/andreasabel/32/1764_2.png) [@andreasabel](https://discourse.haskell.org/u/andreasabel)\
**Post date:** [October 6, 2023, 1:56pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/1 "2023-10-06T13:56:35Z")

</div>

The Agda Team is very pleased to announce the release of Agda 2.6.4.

# Highlights of Agda 2.6.4

- Cubical Agda now displays boundary conditions in interactive mode  
(PR [#6529](https://github.com/agda/agda/pull/6529)).

- An inconsistency in the treatment of large indices has been fixed  
(Issue [#6654](https://github.com/agda/agda/issues/6654)).

- Unfolding of definitions can now be fine-controlled via `opaque` definitions.

- Additions to the sort system: `LevelUniv` and `Propω`.

- New flag `--erasure` with several improvements to erasure (declared run-time irrelevance).

- New reflection primitives for meta-programming.

# GHC supported versions

Agda 2.6.4 has been tested with GHC 9.6.3, 9.4.7, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows.

# Installation

Agda 2.6.4 can be installed using cabal-install or stack:

1. Getting the tarball

2. a. Using cabal-install

3. b. Using stack

replacing `a.b.c` with your version of GHC.

The flags mean:

```
- optimise-heavily:
  Turn on extra optimisation for a faster Agda.
  Takes large resources during compilation of Agda.

- enable-cluster-counting:
  Enable unicode clusters for alignment in the LaTeX backend.
  Requires the ICU lib to be installed and known to pkg-config.

```

These flags can be dropped from the install if causing trouble.

# Standard library

You can use standard library v1.7.2 or the `master` branch of the  
standard library with Agda 2.6.4. This branch is available at

```
    https://github.com/agda/agda-stdlib/

```

# Fixed issues over Agda 2.6.3

[Changelog for Agda-2.6.4 | Hackage](https://hackage.haskell.org/package/Agda-2.6.4/changelog)

Enjoy Agda!

---

<div class="post-metadata">

**Author:** ![hasufell](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/hasufell/32/1250_2.png) [@hasufell](https://discourse.haskell.org/u/hasufell)\
**Post date:** [October 6, 2023, 2:54pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/2 "2023-10-06T14:54:17Z")

</div>

@andreasabel what’s the best introductory material for Agda?

---

<div class="post-metadata">

**Author:** ![arpl](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arpl/32/1713_2.png) [@arpl](https://discourse.haskell.org/u/arpl)\
**Post date:** [October 7, 2023, 1:27pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/3 "2023-10-07T13:27:42Z")

</div>

Wadlers : [Programming Language Foundations in Agda](https://plfa.github.io/)?

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [October 7, 2023, 2:09pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/4 "2023-10-07T14:09:11Z")

</div>

The problem I run inti immediately is the standard library. It is all so abstract and I haven’t found an easy way to search it.

All the Agda learning materials I’ve seen, including that one, introduces each concept from scratch without explaining how to use the existing abstractions from the standard library.

---

<div class="post-metadata">

**Author:** ![HeinrichApfelmus](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/heinrichapfelmus/32/117_2.png) [@HeinrichApfelmus](https://discourse.haskell.org/u/HeinrichApfelmus)\
**Post date:** [October 15, 2023, 9:43am UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/5 "2023-10-15T09:43:48Z")

</div>

I think that Part 1 of Wadler’s [Programming Language Foundations in Agda](https://plfa.github.io/) is an excellent introduction to Agda when combined with general overviews of natural deduction, e.g. Wadler’s [Proofs are Programs](https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf).

However, Part 2 and later of Wadler’s book are somewhat specific to lambda calculi and not as interesting to “general Haskellers”. For that, I think that Aaron Stumps’ book [Verified Functional Programming in Agda](https://dl.acm.org/doi/book/10.1145/2841316) covers more relevant material.

Finally, the material (documentation, tutorials, examples, …) accompanying [Agda2hs](https://github.com/agda/agda2hs) is probably the most relevant for Haskellers.

---

<div class="post-metadata">

**Author:** ![juhp](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/juhp/32/323_2.png) [@juhp](https://discourse.haskell.org/u/juhp)\
**Post date:** [October 16, 2023, 5:03pm UTC](https://discourse.haskell.org/t/ann-agda-2-6-4-released/7810/6 "2023-10-16T17:03:24Z")

</div>

> [@andreasabel](#):
>
> ```haskell
> - optimise-heavily:
> Turn on extra optimisation for a faster Agda.
> Takes large resources during compilation of Agda.
> 
> ```

So is `optmise-heavily` recommended now for production builds/usage?  
How much impact does it have for build-time and runtime?  
(_edit_: I see it induces ` ghc-options: -fexpose-all-unfoldings -fspecialise-aggressively`)

I am wondering if I should turn it on for Fedora builds…