1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
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`,
stackage `lts-19.0` and `nightly`).
* Fixes inconsistency [#5838](https://github.com/agda/agda/issues/5838)
in `--cubical`.
* Fixes some regressions introduced in 2.6.1:
- [#5809](https://github.com/agda/agda/issues/5809):
internal error with `--irrelevant-projections`.
* Fixes some regressions introduced in 2.6.2:
- [#5705](https://github.com/agda/agda/issues/5705) and
[#5706](https://github.com/agda/agda/issues/5706):
inconsistency from universe level `Int` overflow.
- [#5784](https://github.com/agda/agda/issues/5784):
`primEraseEquality` does not compute.
- [#5805](https://github.com/agda/agda/issues/5805):
internal error involving holes and `with`.
- [#5819](https://github.com/agda/agda/issues/5819):
internal error when reducing in termination checker.
* Other
[fixes](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.2+is%3Aclosed)
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` and `executables`
configuration files (issue
[#5741](https://github.com/agda/agda/issues/5741)).
Language
--------
* `macro` definitions can now be used even when they are declared as erased
(PR [#5744](https://github.com/agda/agda/pull/5744)).
For example, this is now accepted:
```agda
macro
@0 trivial : Term → TC ⊤
trivial = unify (con (quote refl) [])
test : 42 ≡ 42
test = trivial
```
* Fixed inconsistent `--cubical` reductions for `transp`:
issue [#5838](https://github.com/agda/agda/issues/5838).
* Fixed issues with reflection:
- [#5762](https://github.com/agda/agda/issues/5762):
do not eagerly check existence of commands in `executables` file.
- [#5695](https://github.com/agda/agda/issues/5695):
fix `elaborate-and-give` interaction command.
- [#5700](https://github.com/agda/agda/issues/5700):
scope of metas created during macro expansion.
- [#5712](https://github.com/agda/agda/issues/5712):
internal error with tactics on record fields of function type.
* Fixed issues with instance search:
- [#5583](https://github.com/agda/agda/issues/5583):
constructor instances from parameterized modules.
- [#5787](https://github.com/agda/agda/issues/5787):
erased instance arguments.
* Fixed issue [#5683](https://github.com/agda/agda/issues/5683) with
generalization in `let`.
Compiler backends
-----------------
* `.hs` files generated by the GHC backend now switch off the
`warn-overlapping-patterns` warning (issue
[#5758](https://github.com/agda/agda/issues/5758)).
* The GHC backend now calls `ghc` with environment setting
`GHC_CHARENC=UTF-8` (issue
[#5742](https://github.com/agda/agda/issues/5742)).
Performance
-----------
* Better caching of interfaces
(issue [#2767](https://github.com/agda/agda/issues/2767)).
* Various performance improvements concerning meta-variables:
issue [#5388](https://github.com/agda/agda/issues/5388)
and PR [#5733](https://github.com/agda/agda/pull/5733).
|
