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]). 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]). 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]).

Bug fixes

• Fixed an internal error related to interface files (Issue [#7436]).

• Fixed two internal errors in Mimer: (Issue [#7402] and Issue [#7484]).

• Fixed a regression causing needless re-checking of files (Issue [#7199]).

• Improved printing of terms by fixing a display form bug (PR [#7480]).

List of closed issues

For 2.7.0.1, the following issues were closed (see bug tracker):

• Issue [#7199]: Agda re-checks a file with an up-to-date interface file
• Issue [#7402]: Mimer internal error in hole with constraint
• Issue [#7436]: Code only reachable from display forms not serialised in Agda 2.7.0
• Issue [#7442]: Regression: emptiness check fails when erased constructors are involved
• Issue [#7443]: --exact-split is not default in 2.7.0, contrary to claims
• Issue [#7452]: Performance regression caused by making --save-metas the default
• Issue [#7455]: Both stack and cabal fail to install Agda
• Issue [#7484]: Internal error using Mimer in where block

These pull requests were merged for 2.7.0.1:

• PR [#7427]: [#7402]: mimer failing on higher order goal
• PR [#7444]: Fix [#7436]: make display forms of imported names DeadCode roots
• PR [#7445]: Remove disclaimer that Agda would not follow the Haskell PVP
• PR [#7454]: Fixed [#7199]
• PR [#7456]: Actually, --exact-split is not really on by default
• PR [#7457]: Revert default to --no-save-metas
• PR [#7465]: Re [#7455]: Setup.hs: catch when Agda did not produce (all) agdai files
• PR [#7471]: setup: Don't assume exe is built on --lib
• PR [#7475]: Hotfix for [#7442]
• PR [#7476]: Bump std-lib to latest (v2.1.1) and cubical to latest
• PR [#7480]: Match display forms in the right context
• PR [#7487]: Mimer shouldn't try to use existing pattern lambdas in solutions

What's Changed (auto-generated)

• Release 2.7.0.1 by @andreasabel in https://github.com/agda/agda/pull/7469

Full Changelog: https://github.com/agda/agda/compare/v2.7.0...v2.7.0.1