Changelog for Agda-2.6.4.2
Release notes for Agda version 2.6.4.2
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.
Highlights
- Fix an inconsistency in Cubical Agda related to catch-all clauses: Issue #7033
- Fix a regression in instance search introduced in 2.6.4.2: Issue #7113
- Fix a bug related to
opaque: Issue #6972 - Fix some internal errors:
- Fix building with cabal flag
-f debug-serialisation: Issue #7081
List of closed issues
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"
- Issue #7104: Warning "there are two interface files" should not be serialized
- Issue #7105: Internal error in generate-helper (C-c C-h)
- Issue #7113: Instance resolution runs too late, leads to
with-abstraction failure
These PRs not corresponding to issues were merged: