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
|
Release notes for Agda version 2.7.0.1
======================================
This is a minor release of Agda fixing some bugs and regressions.
Installation
------------
* During installation, Agda type-checks its built-in modules and installs the generated `.agdai` files.
(This step is now skipped when the Agda executable is not installed, e.g. `cabal install --lib Agda`.)
Should the generation for (some of) these files fail, the names of the missing ones are now printed,
but installation continues nevertheless ([PR #7465](https://github.com/agda/agda/pull/7465)).
Rationale: installation of these files is only crucial when installing Agda in super-user mode.
* Agda supports GHC versions 8.6.5 to 9.10.1.
Pragmas and options
-------------------
* The release notes of 2.7.0 claimed that the option `--exact-split` was now on by default
([Issue #7443](https://github.com/agda/agda/issues/7443)).
This is actually not the case, the documentation has been suitably reverted.
* Default option `--save-metas` has been reverted to `--no-save-metas` because of performance regressions
([Issue #7452](https://github.com/agda/agda/issues/7452)).
Bug fixes
---------
* Fixed an internal error related to interface files
([Issue #7436](https://github.com/agda/agda/issues/7436)).
* Fixed two internal errors in Mimer:
([Issue #7402](https://github.com/agda/agda/issues/7402) and
[Issue #7484](https://github.com/agda/agda/issues/7484)).
* Fixed a regression causing needless re-checking of files
([Issue #7199](https://github.com/agda/agda/issues/7199)).
* Improved printing of terms by fixing a display form bug
([PR #7480](https://github.com/agda/agda/issues/7480)).
List of closed issues
---------------------
For 2.7.0.1, the following issues were
[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.7.0.1+is%3Aclosed)
(see [bug tracker](https://github.com/agda/agda/issues)):
- [Issue #7199](https://github.com/agda/agda/issues/7199): Agda re-checks a file with an up-to-date interface file
- [Issue #7402](https://github.com/agda/agda/issues/7402): Mimer internal error in hole with constraint
- [Issue #7436](https://github.com/agda/agda/issues/7436): Code only reachable from display forms not serialised in Agda 2.7.0
- [Issue #7442](https://github.com/agda/agda/issues/7442): Regression: emptiness check fails when erased constructors are involved
- [Issue #7443](https://github.com/agda/agda/issues/7443): `--exact-split` is not default in 2.7.0, contrary to claims
- [Issue #7452](https://github.com/agda/agda/issues/7452): Performance regression caused by making `--save-metas` the default
- [Issue #7455](https://github.com/agda/agda/issues/7455): Both stack and cabal fail to install Agda
- [Issue #7484](https://github.com/agda/agda/issues/7484): Internal error using Mimer in where block
These pull requests were merged for 2.7.0.1:
- [PR #7427](https://github.com/agda/agda/issues/7427): #7402: mimer failing on higher order goal
- [PR #7444](https://github.com/agda/agda/issues/7444): Fix #7436: make display forms of imported names DeadCode roots
- [PR #7445](https://github.com/agda/agda/issues/7445): Remove disclaimer that Agda would not follow the Haskell PVP
- [PR #7454](https://github.com/agda/agda/issues/7454): Fixed #7199
- [PR #7456](https://github.com/agda/agda/issues/7456): Actually, --exact-split is not really on by default
- [PR #7457](https://github.com/agda/agda/issues/7457): Revert default to `--no-save-metas`
- [PR #7465](https://github.com/agda/agda/issues/7465): Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files
- [PR #7471](https://github.com/agda/agda/issues/7471): setup: Don't assume exe is built on --lib
- [PR #7475](https://github.com/agda/agda/issues/7475): Hotfix for #7442
- [PR #7476](https://github.com/agda/agda/issues/7476): Bump std-lib to latest (v2.1.1) and cubical to latest
- [PR #7480](https://github.com/agda/agda/issues/7480): Match display forms in the right context
- [PR #7487](https://github.com/agda/agda/issues/7487): Mimer shouldn't try to use existing pattern lambdas in solutions
|
