Changelog for Agda-2.6.2.2
Release notes for Agda version 2.6.2.2
Highlights
-
Agda 2.6.2.2 catches up to changes in the Haskell ecosystem (
bytestring-0.11.2.0
,mtl-2.3-rc3/4
,text-icu-0.8.0.1
, stackagelts-19.0
andnightly
). -
Fixes inconsistency #5838 in
--cubical
. -
Fixes some regressions introduced in 2.6.1:
- #5809:
internal error with
--irrelevant-projections
.
- #5809:
internal error with
-
Fixes some regressions introduced in 2.6.2:
-
Other fixes and improvements (see below).
Installation and infrastructure
Agda supports GHC versions 8.0.2 to 9.2.2.
- UTF-8 encoding is now used for the
libraries
andexecutables
configuration files (issue #5741).
Language
-
macro
definitions can now be used even when they are declared as erased (PR #5744). For example, this is now accepted:macro @0 trivial : Term → TC ⊤ trivial = unify (con (quote refl) []) test : 42 ≡ 42 test = trivial
-
Fixed inconsistent
--cubical
reductions fortransp
: issue #5838. -
Fixed issues with reflection:
-
Fixed issues with instance search:
-
Fixed issue #5683 with generalization in
let
.
Compiler backends
-
.hs
files generated by the GHC backend now switch off thewarn-overlapping-patterns
warning (issue #5758). -
The GHC backend now calls
ghc
with environment settingGHC_CHARENC=UTF-8
(issue #5742).