v2.6.4.1
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 thedebug
cabal flag.
Withoutdebug
, no code is generated for verbose printing, which makes building Agda faster and Agda itself faster as well. (PR #6863)
Language
- A change in 2.6.4 that prevented all recursion on proofs, i.e., members of a type
A : Prop ℓ
, has been reverted.
It is possible again to use proofs as termination arguments. (See issue #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 candidatec1 : T
has a type which is a substitution instance of that of another candidatec2 : S
,c1
will appear earlier in the list.As a concrete example, if you have instances
F (Nat → Nat)
,F (Nat → a)
, andF (a → b)
, they will be returned in this order.
See issue #6944 for further motivation.
Library management
-
Agda now follows the XDG base directory standard on Unix-like systems, see PR #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 (see bug tracker):
- #6745: Strange interaction between
opaque
andlet open
- #6746: Support GHC 9.8
- #6852: Follow XDG Base Directory Specification
- #6913: Internal error on
primLockUniv
-sorted functions - #6930: Termination checking with --prop: change in 2.6.4 compared with 2.6.3
- #6931: Internal error with an empty parametrized module from a different file
- #6941: Interaction between opaque and instance arguments
- #6944: Order instances by specificity for reflection
- #6953: Emacs 30 breaks agda mode
- #6957: Agda stdlib installation instructions broken link
- #6959: Warn about opaque
unquoteDecl
/unquoteDef
- #6983: Refine command does not work on Emacs 30
What's Changed (auto-generated)
- LHS Error Refactor by @AlexHarsani in #6862
- Serialization optimizations by @AndrasKovacs in #6892
- test-suite: Pacify GHC 9.8's new warning
x-partial
by @andreasabel in #6906 - Code specialization by @AndrasKovacs in #6894
- Fix #6905: work around a bug in process-1.6.14..17 by @andreasabel in #6907
- Bump styfle/cancel-workflow-action from 0.11.0 to 0.12.0 by @dependabot in #6909
- Relax dependency bound to
split < 0.3
by @andreasabel in #6912 - Fix the spelling of "ambiguous" by @liesnikov in #6903
- hard drop GHC 8.4 by @andreasabel in #6917
- toggle debug reporting via CPP by @AndrasKovacs in #6863
- Perf fixes and more benchmark data in TypeChecking.DeadCode by @AndrasKovacs in #6899
- CI: bump submodules + cosmetics by @andreasabel in #6920
- doc installation Fedora: fixup rst link markup by @juhp in #6922
- [ #6746 ] Using GHC 9.8.1 on stack. by @asr in #6923
- Re #6746: bump CI to GHC 9.8.1; treat
cache-hit
as string by @andreasabel in #6924 - Re #6746: bump tested-with etc to GHC 9.8.1; bump deps in tools by @andreasabel in #6925
- Cosmetics: activate warning operator-whitespace by @andreasabel in #6929
- Fix #6931: dead code: include module telescopes in reachability analysis by @andreasabel in #6932
- Bump teatimeguest/setup-texlive-action from 2 to 3 by @dependabot in #6937
- Instantiate all metas before retrieving blockers in
getLockVar
. by @andreasabel in #6938 - Record UnifyIndices bench cost under Coverage by @AndrasKovacs in #6921
- Fix issue #6930: Allow recursion on proofs again by @andreasabel in #6936
- [ fix #6941 ] Ignore abstract mode in
getOutputTypeName
by @jespercockx in #6942 - Separate parameters with space when pretty-printing by @szumixie in #6946
- Bump cubical submodule to latest master by @andreasabel in #6947
- remove mysteriously failing SPECIALIZE below ghc-9.x by @AndrasKovacs in #6949
- Fix highlight-hover.js by @ncfavier in #6948
- Remove whitespace around substrings before concatenation by @kutsurak in #6954
- Order instance candidates for getInstances by @plt-amy in #6955
- Add book to documentation by @scholablade in #6952
- Add XDG Base Directory support by @4e554c4c in #6858
- User-facing debug printing in reflection also without -fdebug by @UlfNorell in #6965
- Add missing changelogs for #6858 and #6955 by @plt-amy in #6967
- Bugfixes for opaque definitions by @plt-amy in #6971
- prepare 2.6.4.1 by @andreasabel in #6968
- Fix #6957: user-manual: link to std-lib installation instructions by @andreasabel in #6973
- Rewriting Error Refactor by @AlexHarsani in #6984
- Fixes issue 6234 by updating documentation for Cubical Agda and removing links by @mortberg in #6977
- Add a note about tc.unquote.decl/def verbosity to user manual by @UlfNorell in #6981
- #6958: Clarify documentation by @plt-amy in #6982
- CI deploy breaks with GHC 9.4.8 so stay on 9.4.7 by @andreasabel in #6986
- Ad #6863: update
agda --version
output to new cabal flags by @andreasabel in #6985 - Data Error Refactor by @AlexHarsani in #6987
- [ emacs ]
string-trim
to combat recent change inpp.el
adding newlines by @andreasabel in #6995 - prep 2.6.4.1 by @andreasabel in #6996
- Bump stack-*.yaml files to latest resolvers by @andreasabel in #6997
New Contributors
- @AndrasKovacs made their first contribution in #6892
- @rhendric made their first contribution in #6603
- @scholablade made their first contribution in #6952
- @4e554c4c made their first contribution in #6858
Full Changelog: v2.6.4...v2.6.4.1