Agda is a dependently typed programming language / interactive theorem prover.
glue1
bindings by @ncfavier in https://github.com/agda/agda/pull/7021
user-manual
to stdlib-v2.0 by @jamesmckinna in https://github.com/agda/agda/pull/7043
flake.nix
by @lawcho in https://github.com/agda/agda/pull/7032
defBlocked
as neverUnblock
by @andreasabel in https://github.com/agda/agda/pull/7046
cancel-workflow-action
by @L-TChen in https://github.com/agda/agda/pull/7074
.agda-lib
for Agda builtins by @ibbem in https://github.com/agda/agda/pull/6988
let
by @UlfNorell in https://github.com/agda/agda/pull/7078
instantiateFull
before with-abstraction. by @andreasabel in https://github.com/agda/agda/pull/7151
__IMPOSSIBLE__
for nullary syntax by @andreasabel in https://github.com/agda/agda/pull/7160
unquote
applications by @ncfavier in https://github.com/agda/agda/pull/6570
INJECTIVE_FOR_INFERENCE
pragma by @WhatisRT in https://github.com/agda/agda/pull/6640
Full Changelog: https://github.com/agda/agda/compare/v2.6.4.3...nightly
This release fixes a regression in 2.6.4.3 and one in 2.6.4. It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.
Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.
For 2.6.4.3, the following issues were closed (see bug tracker):
with
rewrite
with instancesFull Changelog: https://github.com/agda/agda/compare/v2.6.4.2...v2.6.4.3
This is a bug-fix release. It aims to be API-compatible with 2.6.4.1. Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1.
opaque
: Issue #6972
-f debug-serialisation
: Issue #7081
For 2.6.4.2, the following issues were closed (see bug tracker):
Data.Nat.DivMod.DivMod
?IsString
instance with debug flags enabledwith
-abstraction failureThese PRs not corresponding to issues were merged:
.agda-lib
for Agda builtinsFull Changelog: https://github.com/agda/agda/compare/v2.6.4.1...v2.6.4.2
This is a minor release of Agda 2.6.4 featuring a few changes:
debug
.getInstances
.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)
A : Prop ℓ
, has been reverted.
It is possible again to use proofs as termination arguments. (See issue #6930.)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 for further motivation.
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
).
For 2.6.4.1, the following issues were also closed (see bug tracker):
opaque
and let open
primLockUniv
-sorted functionsunquoteDecl
/unquoteDef
x-partial
by @andreasabel in https://github.com/agda/agda/pull/6906
split < 0.3
by @andreasabel in https://github.com/agda/agda/pull/6912
cache-hit
as string by @andreasabel in https://github.com/agda/agda/pull/6924
getLockVar
. by @andreasabel in https://github.com/agda/agda/pull/6938
getOutputTypeName
by @jespercockx in https://github.com/agda/agda/pull/6942
agda --version
output to new cabal flags by @andreasabel in https://github.com/agda/agda/pull/6985
string-trim
to combat recent change in pp.el
adding newlines by @andreasabel in https://github.com/agda/agda/pull/6995
Full Changelog: https://github.com/agda/agda/compare/v2.6.4...v2.6.4.1