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
|
Release notes for Agda version 2.6.4.1
======================================
This is a minor release of Agda 2.6.4 featuring a few changes:
- Make recursion on proofs legal again.
- Improve performance, e.g. by removing debug printing unless built with cabal flag `debug`.
- Switch to XDG directory convention.
- Reflection: change to order of results returned by `getInstances`.
- Fix some internal errors.
Installation
------------
* Agda supports GHC versions 8.6.5 to 9.8.1.
* Verbose output printing via `-v` or `--verbose` is now only active if Agda is built with the `debug` cabal flag.
Without `debug`, no code is generated for verbose printing, which makes building Agda faster and Agda itself
faster as well. (PR [#6863](https://github.com/agda/agda/pull/6863))
Language
--------
* A [change](https://github.com/agda/agda/pull/6639) in 2.6.4 that prevented all recursion on proofs,
i.e., members of a type `A : Prop ℓ`, has been [reverted](https://github.com/agda/agda/pull/6936).
It is possible again to use proofs as termination arguments.
(See [issue #6930](https://github.com/agda/agda/issues/6930).)
Reflection
----------
Changes to the meta-programming facilities.
* The reflection primitive `getInstances` will now return instance
candidates ordered by _specificity_, rather than in unspecified order:
If a candidate `c1 : T` has a type which is a substitution instance of
that of another candidate `c2 : S`, `c1` will appear earlier in the
list.
As a concrete example, if you have instances `F (Nat → Nat)`, `F (Nat
→ a)`, and `F (a → b)`, they will be returned in this order. See
[issue #6944](https://github.com/agda/agda/issues/6944) for further
motivation.
Library management
------------------
* Agda now follows the XDG base directory standard on Unix-like systems,
see [PR #6858](https://github.com/agda/agda/pull/6858).
This means, it will look for configuration files in `~/.config/agda` rather than `~/.agda`.
For backward compatibility, if you still have an `~/.agda` directory, it will look there first.
No change on Windows, it will continue to use `%APPDATA%` (e.g. `C:/Users/USERNAME/AppData/Roaming/agda`).
Other issues closed
-------------------
For 2.6.4.1, the following issues were also
[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.1+is%3Aclosed)
(see [bug tracker](https://github.com/agda/agda/issues)):
- [#6745](https://github.com/agda/agda/issues/6745): Strange interaction between `opaque` and `let open`
- [#6746](https://github.com/agda/agda/issues/6746): Support GHC 9.8
- [#6852](https://github.com/agda/agda/issues/6852): Follow XDG Base Directory Specification
- [#6913](https://github.com/agda/agda/issues/6913): Internal error on `primLockUniv`-sorted functions
- [#6930](https://github.com/agda/agda/issues/6930): Termination checking with --prop: change in 2.6.4 compared with 2.6.3
- [#6931](https://github.com/agda/agda/issues/6931): Internal error with an empty parametrized module from a different file
- [#6941](https://github.com/agda/agda/issues/6941): Interaction between opaque and instance arguments
- [#6944](https://github.com/agda/agda/issues/6944): Order instances by specificity for reflection
- [#6953](https://github.com/agda/agda/issues/6953): Emacs 30 breaks agda mode
- [#6957](https://github.com/agda/agda/issues/6957): Agda stdlib installation instructions broken link
- [#6959](https://github.com/agda/agda/issues/6959): Warn about opaque `unquoteDecl`/`unquoteDef`
- [#6983](https://github.com/agda/agda/issues/6983): Refine command does not work on Emacs 30
|
