This is a bug-fix release. It aims to be API-compatible with 2.6.4.1. Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1.
- Fix an inconsistency in Cubical Agda related to catch-all clauses: Issue #7033
- Fix a bug related to
opaque: Issue #6972 - Fix some internal errors:
- Fix building with cabal flag
-f debug-serialisation: Issue #7081
For 2.6.4.2, the following issues were closed (see bug tracker):
- Issue #6972: Unfolding fails when code is split up into multiple files
- Issue #6999: Unification failure for function type with erased argument
- Issue #7020: question: haskell backend extraction of
Data.Nat.DivMod.DivMod? - Issue #7029: Internal error on confluence check when rewriting a defined symbol with a hole
- Issue #7033: transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥
- Issue #7034: Internal error with --two-level due to blocking on solved meta
- Issue #7044: Serializer crashes on blocked definitions when using --allow-unsolved-metas
- Issue #7048: hcomp symbols in interface not hidden under --cubical-compatible
- Issue #7059: Don't recompile if --keep-pattern-variables option changes
- Issue #7070: Don't set a default maximum heapsize for Agda runs
- Issue #7081: Missing
IsStringinstance with debug flags enabled - Issue #7095: Agda build flags appear as "automatic", but they are all "manual"
These PRs not corresponding to issues were merged: