Agda-2.6.4: doc/release-notes/2.5.2.md
Release notes for Agda version 2.5.2
====================================
Installation and infrastructure
-------------------------------
* Modular support for literate programming
Literate programming support has been moved out of the lexer and into the
`Agda.Syntax.Parser.Literate` module.
Files ending in `.lagda` are still interpreted as literate TeX.
The extension `.lagda.tex` may now also be used for literate TeX files.
Support for more literate code formats and extensions can be added
modularly.
By default, `.lagda.*` files are opened in the Emacs mode
corresponding to their last extension. One may switch to and from
Agda mode manually.
* reStructuredText
Literate Agda code can now be written in reStructuredText format, using
the `.lagda.rst` extension.
As a general rule, Agda will parse code following a line ending in `::`,
as long as that line does not start with `..`. The module name must
match the path of the file in the documentation, and must be given
explicitly. Several files have been converted already, for instance:
- `language/mixfix-operators.lagda.rst`
- `tools/compilers.lagda.rst`
Note that:
- Code blocks inside an rST comment block will be type-checked by Agda,
but not rendered in the documentation.
- Code blocks delimited by `.. code-block:: agda` will be rendered in
the final documenation, but not type-checked by Agda.
- All lines inside a codeblock must be further indented than the first line
of the code block.
- Indentation must be consistent between code blocks. In other
words, the file as a whole must be a valid Agda file if all the
literate text is replaced by white space.
* Documentation testing
All documentation files in the `doc/user-manual` directory that end
in `.lagda.rst` can be typechecked by running `make
user-manual-test`, and also as part of the general test suite.
* Support installation through Stack
The Agda sources now also include a configuration for the stack install tool
(tested through continuous integration).
It should hence be possible to repeatably build any future Agda version
(including unreleased commits) from source by checking out that version and
running `stack install` from the checkout directory.
By using repeatable builds, this should keep selecting the same dependencies
in the face of new releases on Hackage.
For further motivation, see
Issue [#2005](https://github.com/agda/agda/issues/2005).
* Removed the `--test` command-line option
This option ran the internal test-suite. This test-suite was
implemented using Cabal supports for
test-suites. [Issue [#2083](https://github.com/agda/agda/issues/2083)].
* The `--no-default-libraries` flag has been split into two flags
[Issue [#1937](https://github.com/agda/agda/issues/1937)]
- `--no-default-libraries`: Ignore the defaults file but still look for local
`.agda-lib` files
- `--no-libraries`: Don't use any `.agda-lib` files (the previous behaviour
of `--no-default-libraries`).
* If `agda` was built inside `git` repository, then the `--version` flag
will display the hash of the commit used, and whether the tree was
`-dirty` (i.e. there were uncommited changes in the working directory).
Otherwise, only the version number is shown.
Language
--------
* Dot patterns are now optional
Consider the following program
```agda
data Vec (A : Set) : Nat → Set where
[] : Vec A zero
cons : ∀ n → A → Vec A n → Vec A (suc n)
vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
vmap .zero f [] = []
vmap .(suc m) f (cons m x xs) = cons m (f x) (vmap m f xs)
```
If we don't care about the dot patterns they can (and could previously) be
replaced by wildcards:
```agda
vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
vmap _ f [] = []
vmap _ f (cons m x xs) = cons m (f x) (vmap m f xs)
```
Now it is also allowed to give a variable pattern in place of the dot
pattern. In this case the variable will be bound to the value of the dot
pattern. For our example:
```agda
vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
vmap n f [] = []
vmap n f (cons m x xs) = cons m (f x) (vmap m f xs)
```
In the first clause `n` reduces to `zero` and in the second clause
`n` reduces to `suc m`.
* Module parameters can now be refined by pattern matching
Previously, pattern matches that would refine a variable outside the
current left-hand side was disallowed. For instance, the following
would give an error, since matching on the vector would
instantiate `n`.
```agda
module _ {A : Set} {n : Nat} where
f : Vec A n → Vec A n
f [] = []
f (x ∷ xs) = x ∷ xs
```
Now this is no longer disallowed. Instead `n` is bound to the
appropriate value in each clause.
* With-abstraction now abstracts also in module parameters
The change that allows pattern matching to refine module parameters also
allows with-abstraction to abstract in them. For instance,
```agda
module _ (n : Nat) (xs : Vec Nat (n + n)) where
f : Nat
f with n + n
f | nn = ? -- xs : Vec Nat nn
```
Note: Any function argument or lambda-bound variable bound outside a given
function counts as a module parameter.
To prevent abstraction in a parameter you can hide it inside a definition. In
the above example,
```agda
module _ (n : Nat) (xs : Vec Nat (n + n)) where
ys : Vec Nat (n + n)
ys = xs
f : Nat
f with n + n
f | nn = ? -- xs : Vec Nat nn, ys : Vec Nat (n + n)
```
* As-patterns [Issue [#78](https://github.com/agda/agda/issues/78)].
As-patterns (`@`-patterns) are finally working and can be used to name a
pattern. The name has the same scope as normal pattern variables (i.e. the
right-hand side, where clause, and dot patterns). The name reduces to the
value of the named pattern. For example::
```agda
module _ {A : Set} (_<_ : A → A → Bool) where
merge : List A → List A → List A
merge xs [] = xs
merge [] ys = ys
merge xs@(x ∷ xs₁) ys@(y ∷ ys₁) =
if x < y then x ∷ merge xs₁ ys
else y ∷ merge xs ys₁
```
* Idiom brackets.
There is new syntactic sugar for idiom brackets:
`(| e a1 .. an |)` expands to
`pure e <*> a1 <*> .. <*> an`
The desugaring takes place before scope checking and only requires names
`pure` and `_<*>_` in scope. Idiom brackets work well with operators, for
instance
`(| if a then b else c |)` desugars to
`pure if_then_else_ <*> a <*> b <*> c`
Limitations:
- The top-level application inside idiom brackets cannot include
implicit applications, so `(| foo {x = e} a b |)` is illegal. In
the case `e` is pure you can write `(| (foo {x = e}) a b |)`
which desugars to
`pure (foo {x = e}) <*> a <*> b`
- Binding syntax and operator sections cannot appear immediately inside
idiom brackets.
* Layout for pattern matching lambdas.
You can now write pattern matching lambdas using the syntax
```agda
λ where false → true
true → false
```
avoiding the need for explicit curly braces and semicolons.
* Overloaded projections
[Issue [#1944](https://github.com/agda/agda/issues/1944)].
Ambiguous projections are no longer a scope error. Instead they get
resolved based on the type of the record value they are
eliminating. This corresponds to constructors, which can be
overloaded and get disambiguated based on the type they are
introducing. Example:
```agda
module _ (A : Set) (a : A) where
record R B : Set where
field f : B
open R public
record S B : Set where
field f : B
open S public
```
Exporting `f` twice from both `R` and `S` is now allowed. Then,
```agda
r : R A
f r = a
s : S A
f s = f r
```
disambiguates to:
```agda
r : R A
R.f r = a
s : S A
S.f s = R.f r
```
If the type of the projection is known, it can also be disambiguated
unapplied.
```agda
unapplied : R A -> A
unapplied = f
```
* Postfix projections
[Issue [#1963](https://github.com/agda/agda/issues/1963)].
Agda now supports a postfix syntax for projection application.
This style is more in harmony with copatterns. For example:
```agda
record Stream (A : Set) : Set where
coinductive
field head : A
tail : Stream A
open Stream
repeat : ∀{A} (a : A) → Stream A
repeat a .head = a
repeat a .tail = repeat a
zipWith : ∀{A B C} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C
zipWith f s t .head = f (s .head) (t .head)
zipWith f s t .tail = zipWith f (s .tail) (t .tail)
module Fib (Nat : Set) (zero one : Nat) (plus : Nat → Nat → Nat) where
{-# TERMINATING #-}
fib : Stream Nat
fib .head = zero
fib .tail .head = one
fib .tail .tail = zipWith plus fib (fib .tail)
```
The thing we eliminate with projection now is visibly the head,
i.e., the left-most expression of the sequence (e.g. `repeat` in
`repeat a .tail`).
The syntax overlaps with dot patterns, but for type correct left
hand sides there is no confusion: Dot patterns eliminate function
types, while (postfix) projection patterns eliminate record types.
By default, Agda prints system-generated projections (such as by
eta-expansion or case splitting) prefix. This can be changed with
the new option:
```agda
{-# OPTIONS --postfix-projections #-}
```
Result splitting in extended lambdas (aka pattern lambdas) always
produces postfix projections, as prefix projection pattern do not
work here: a prefix projection needs to go left of the head, but the
head is omitted in extended lambdas.
```agda
dup : ∀{A : Set}(a : A) → A × A
dup = λ{ a → ? }
```
Result splitting (`C-c C-c RET`) here will yield:
```agda
dup = λ{ a .proj₁ → ? ; a .proj₂ → ? }
```
* Projection parameters
[Issue [#1954](https://github.com/agda/agda/issues/1954)].
When copying a module, projection parameters will now stay hidden
arguments, even if the module parameters are visible.
This matches the situation we had for constructors since long.
Example:
```agda
module P (A : Set) where
record R : Set where
field f : A
open module Q A = P A
```
Parameter `A` is now hidden in `R.f`:
```agda
test : ∀{A} → R A → A
test r = R.f r
```
Note that a module parameter that corresponds to the record value
argument of a projection will not be hidden.
```agda
module M (A : Set) (r : R A) where
open R A r public
test' : ∀{A} → R A → A
test' r = M.f r
```
* Eager insertion of implicit arguments
[Issue [#2001](https://github.com/agda/agda/issues/2001)]
Implicit arguments are now (again) eagerly inserted in left-hand sides. The
previous behaviour of inserting implicits for where blocks, but not
right-hand sides was not type safe.
* Module applications can now be eta expanded/contracted without
changing their behaviour
[Issue #[1985](https://github.com/agda/agda/issues/1985)]
Previously definitions exported using `open public` got the
incorrect type for underapplied module applications.
Example:
```agda
module A where
postulate A : Set
module B (X : Set) where
open A public
module C₁ = B
module C₂ (X : Set) = B X
```
Here both `C₁.A` and `C₂.A` have type `(X : Set) → Set`.
* Polarity pragmas.
Polarity pragmas can be attached to postulates. The polarities express
how the postulate's arguments are used. The following polarities
are available:
`_`: Unused.
`++`: Strictly positive.
`+`: Positive.
`-`: Negative.
`*`: Unknown/mixed.
Polarity pragmas have the form
```
{-# POLARITY name <zero or more polarities> #-}
```
and can be given wherever fixity declarations can be given. The
listed polarities apply to the given postulate's arguments
(explicit/implicit/instance), from left to right. Polarities
currently cannot be given for module parameters. If the postulate
takes n arguments (excluding module parameters), then the number of
polarities given must be between 0 and n (inclusive).
Polarity pragmas make it possible to use postulated type formers in
recursive types in the following way:
```agda
postulate
∥_∥ : Set → Set
{-# POLARITY ∥_∥ ++ #-}
data D : Set where
c : ∥ D ∥ → D
```
Note that one can use postulates that may seem benign, together with
polarity pragmas, to prove that the empty type is inhabited:
```agda
postulate
_⇒_ : Set → Set → Set
lambda : {A B : Set} → (A → B) → A ⇒ B
apply : {A B : Set} → A ⇒ B → A → B
{-# POLARITY _⇒_ ++ #-}
data ⊥ : Set where
data D : Set where
c : D ⇒ ⊥ → D
not-inhabited : D → ⊥
not-inhabited (c f) = apply f (c f)
inhabited : D
inhabited = c (lambda not-inhabited)
bad : ⊥
bad = not-inhabited inhabited
```
Polarity pragmas are not allowed in safe mode.
* Declarations in a `where`-block are now
private. [Issue [#2101](https://github.com/agda/agda/issues/2101)]
This means that
```agda
f ps = body where
decls
```
is now equivalent to
```agda
f ps = body where
private
decls
```
This changes little, since the `decls` were anyway not in scope
outside `body`. However, it makes a difference for abstract
definitions, because private type signatures can see through
abstract definitions. Consider:
```agda
record Wrap (A : Set) : Set where
field unwrap : A
postulate
P : ∀{A : Set} → A → Set
abstract
unnamedWhere : (A : Set) → Set
unnamedWhere A = A
where -- the following definitions are private!
B : Set
B = Wrap A
postulate
b : B
test : P (Wrap.unwrap b) -- succeeds
```
The `abstract` is inherited in `where`-blocks from the parent (here:
function `unnamedWhere`). Thus, the definition of `B` is opaque and
the type equation `B = Wrap A` cannot be used to check type
signatures, not even of abstract definitions. Thus, checking the
type `P (Wrap.unwrap b)` would fail. However, if `test` is
private, abstract definitions are translucent in its type, and
checking succeeds. With the implemented change, all
`where`-definitions are private, in this case `B`, `b`, and `test`,
and the example succeeds.
Nothing changes for the named forms of `where`,
```agda
module M where
module _ where
```
For instance, this still fails:
```agda
abstract
unnamedWhere : (A : Set) → Set
unnamedWhere A = A
module M where
B : Set
B = Wrap A
postulate
b : B
test : P (Wrap.unwrap b) -- fails
```
* Private anonymous modules now work as expected
[Issue [#2199](https://github.com/agda/agda/issues/2199)]
Previously the `private` was ignored for anonymous modules causing
its definitions to be visible outside the module containing the
anonymous module. This is no longer the case. For instance,
```agda
module M where
private
module _ (A : Set) where
Id : Set
Id = A
foo : Set → Set
foo = Id
open M
bar : Set → Set
bar = Id -- Id is no longer in scope here
```
* Pattern synonyms are now expanded on left hand sides of DISPLAY
pragmas [Issue [#2132](https://github.com/agda/agda/issues/2132)].
Example:
```agda
data D : Set where
C c : D
g : D → D
pattern C′ = C
{-# DISPLAY C′ = C′ #-}
{-# DISPLAY g C′ = c #-}
```
This now behaves as:
```agda
{-# DISPLAY C = C′ #-}
{-# DISPLAY g C = c #-}
```
Expected error for
```agda
test : C ≡ g C
test = refl
```
is thus:
```
C′ != c of type D
```
* The built-in floats have new semantics to fix inconsistencies
and to improve cross-platform portability.
- Float equality has been split into two primitives.
``primFloatEquality`` is designed to establish
decidable propositional equality while
``primFloatNumericalEquality`` is intended for numerical
computations. They behave as follows:
```
primFloatEquality NaN NaN = True
primFloatEquality 0.0 -0.0 = False
primFloatNumericalEquality NaN NaN = False
primFloatNumericalEquality 0.0 -0.0 = True
```
This change fixes an inconsistency, see [Issue [#2169](https://github.com/agda/agda/issues/2169)].
For further detail see the [user manual](http://agda.readthedocs.io/en/v2.5.2/language/built-ins.html#floats).
- Floats now have only one `NaN` value. This is necessary
for proper Float support in the JavaScript backend,
as JavaScript (and some other platforms) only support
one `NaN` value.
- The primitive function `primFloatLess` was renamed
`primFloatNumericalLess`.
* Added new primitives to built-in floats:
- `primFloatNegate : Float → Float`
[Issue [#2194](https://github.com/agda/agda/issues/2194)]
- Trigonometric primitives
[Issue [#2200](https://github.com/agda/agda/issues/2200)]:
```agda
primCos : Float → Float
primTan : Float → Float
primASin : Float → Float
primACos : Float → Float
primATan : Float → Float
primATan2 : Float → Float → Float
```
* Anonymous declarations
[Issue [#1465](https://github.com/agda/agda/issues/1465)].
A module can contain an arbitrary number of declarations
named `_` which will scoped-checked and type-checked but
won't be made available in the scope (nor exported). They
cannot introduce arguments on the LHS (but one can use
lambda-abstractions on the RHS) and they cannot be defined
by recursion.
```agda
_ : Set → Set
_ = λ x → x
```
### Rewriting
* The REWRITE pragma can now handle several names. E.g.:
```agda
{-# REWRITE eq1 eq2 #-}
```
### Reflection
* You can now use macros in reflected terms
[Issue [#2130](https://github.com/agda/agda/issues/2130)].
For instance, given a macro
```agda
macro
some-tactic : Term → TC ⊤
some-tactic = ...
```
the term `def (quote some-tactic) []` represents a call to the
macro. This makes it a lot easier to compose tactics.
* The reflection machinery now uses normalisation less often:
* Macros no longer normalise the (automatically quoted) term
arguments.
* The TC primitives `inferType`, `checkType` and `quoteTC` no longer
normalise their arguments.
* The following deprecated constructions may also have been changed:
`quoteGoal`, `quoteTerm`, `quoteContext` and `tactic`.
* New TC primitive: `withNormalisation`.
To recover the old normalising behaviour of `inferType`, `checkType`,
`quoteTC` and `getContext`, you can wrap them inside a call to
`withNormalisation true`:
```agda
withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
```
* New TC primitive: `reduce`.
```agda
reduce : Term → TC Term
```
Reduces its argument to weak head normal form.
* Added new TC primitive: `isMacro`
[Issue [#2182](https://github.com/agda/agda/issues/2182)]
```agda
isMacro : Name → TC Bool
```
Returns `true` if the name refers to a macro, otherwise `false`.
* The `record-type` constructor now has an extra argument containing
information about the record type's fields:
```agda
data Definition : Set where
…
record-type : (c : Name) (fs : List (Arg Name)) → Definition
…
```
Type checking
-------------
* Files with open metas can be imported now
[Issue [#964](https://github.com/agda/agda/issues/964)]. This
should make simultaneous interactive development on several modules
more pleasant.
Requires option: `--allow-unsolved-metas`
Internally, before serialization, open metas are turned into postulates named
```
unsolved#meta.<nnn>
```
where `<nnn>` is the internal meta variable number.
* The performance of the compile-time evaluator has been greatly improved.
- Fixed a memory leak in evaluator
(Issue [#2147](https://github.com/agda/agda/issues/2147)).
- Reduction speed improved by an order of magnitude and is now
comparable to the performance of GHCi. Still call-by-name though.
* The detection of types that satisfy K added in Agda 2.5.1 has been
rolled back (see
Issue [#2003](https://github.com/agda/agda/issues/2003)).
* Eta-equality for record types is now only on after the positivity
checker has confirmed it is safe to have it. Eta-equality for
unguarded inductive records previously lead to looping of the type
checker.
[See Issue [#2197](https://github.com/agda/agda/issues/2197)]
```agda
record R : Set where
inductive
field r : R
loops : R
loops = ?
```
As a consequence of this change, the following example does not
type-check any more:
```agda
mutual
record ⊤ : Set where
test : ∀ {x y : ⊤} → x ≡ y
test = refl
```
It fails because the positivity checker is only run after the mutual
block, thus, eta-equality for `⊤` is not available when checking
test.
One can declare eta-equality explicitly, though, to make this
example work.
```agda
mutual
record ⊤ : Set where
eta-equality
test : ∀ {x y : ⊤} → x ≡ y
test = refl
```
* Records with instance fields are now eta expanded before instance search.
For instance, assuming `Eq` and `Ord` with boolean functions `_==_` and `_<_`
respectively,
```agda
record EqAndOrd (A : Set) : Set where
field {{eq}} : Eq A
{{ord}} : Ord A
leq : {A : Set} {{_ : EqAndOrd A}} → A → A → Bool
leq x y = x == y || x < y
```
Here the `EqAndOrd` record is automatically unpacked before instance search,
revealing the component `Eq` and `Ord` instances.
This can be used to simulate superclass dependencies.
* Overlappable record instance fields.
Instance fields in records can be marked as overlappable using the new
`overlap` keyword:
```agda
record Ord (A : Set) : Set where
field
_<_ : A → A → Bool
overlap {{eqA}} : Eq A
```
When instance search finds multiple candidates for a given instance goal and
they are **all** overlappable it will pick the left-most candidate instead of
refusing to solve the instance goal.
This can be use to solve the problem arising from shared "superclass"
dependencies. For instance, if you have, in addition to `Ord` above, a `Num`
record that also has an `Eq` field and want to write a function requiring
both `Ord` and `Num`, any `Eq` constraint will be solved by the `Eq` instance
from whichever argument that comes first.
```agda
record Num (A : Set) : Set where
field
fromNat : Nat → A
overlap {{eqA}} : Eq A
lessOrEqualFive : {A : Set} {{NumA : Num A}} {{OrdA : Ord A}} → A → Bool
lessOrEqualFive x = x == fromNat 5 || x < fromNat 5
```
In this example the call to `_==_` will use the `eqA` field from `NumA`
rather than the one from `OrdA`. Note that these may well be different.
* Instance fields can be left out of copattern matches
[Issue [#2288](https://github.com/agda/agda/issues/2288)]
Missing cases for instance fields (marked `{{` `}}`) in copattern matches
will be solved using instance search. This makes defining instances with
superclass fields much nicer. For instance, we can define `Nat` instances of
`Eq`, `Ord` and `Num` from above as follows:
```agda
instance
EqNat : Eq Nat
_==_ {{EqNat}} n m = eqNat n m
OrdNat : Ord Nat
_<_ {{OrdNat}} n m = lessNat n m
NumNat : Num Nat
fromNat {{NumNat}} n = n
```
The `eqA` fields of `Ord` and `Num` are filled in using instance search (with
`EqNat` in this case).
* Limited instance search depth
[Issue [#2269](https://github.com/agda/agda/issues/2269)]
To prevent instance search from looping on bad instances
(see [Issue #1743](https://github.com/agda/agda/issues/1743)) the search
depth of instance search is now limited. The maximum depth can be set with
the `--instance-search-depth` flag and the default value is `500`.
Emacs mode
----------
* New command `C-u C-u C-c C-n`: Use `show` to display the result of
normalisation.
Calling `C-u C-u C-c C-n` on an expression `e` (in a hole or at top level)
normalises `show e` and prints the resulting string, or an error message if
the expression does not normalise to a literal string.
This is useful when working with complex data structures for which you have
defined a nice `Show` instance.
Note that the name `show` is hardwired into the command.
* Changed feature: Interactively split result.
Make-case (`C-c C-c`) with no variables will now *either* introduce
function arguments *or* do a copattern split (or fail).
This is as before:
```agda
test : {A B : Set} (a : A) (b : B) → A × B
test a b = ?
-- expected:
-- proj₁ (test a b) = {!!}
-- proj₂ (test a b) = {!!}
testFun : {A B : Set} (a : A) (b : B) → A × B
testFun = ?
-- expected:
-- testFun a b = {!!}
```
This is has changed:
```agda
record FunRec A : Set where
field funField : A → A
open FunRec
testFunRec : ∀{A} → FunRec A
testFunRec = ?
-- expected (since 2016-05-03):
-- funField testFunRec = {!!}
-- used to be:
-- funField testFunRec x = {!!}
```
* Changed feature: Split on hidden variables.
Make-case (`C-c C-c`) will no longer split on the given hidden
variables, but only make them visible. (Splitting can then be
performed in a second go.)
```agda
test : ∀{N M : Nat} → Nat → Nat → Nat
test N M = {!.N N .M!}
```
Invoking splitting will result in:
```agda
test {N} {M} zero M₁ = ?
test {N} {M} (suc N₁) M₁ = ?
```
The hidden `.N` and `.M` have been brought into scope, the
visible `N` has been split upon.
* Non-fatal errors/warnings.
Non-fatal errors and warnings are now displayed in the info buffer
and do not interrupt the typechecking of the file.
Currently termination errors, unsolved metavariables, unsolved
constraints, positivity errors, deprecated BUILTINs, and empty
REWRITING pragmas are non-fatal errors.
* Highlighting for positivity check failures
Negative occurences of a datatype in its definition are now
highlighted in a way similar to termination errors.
* The abbrev for codata was replaced by an abbrev for code
environments.
If you type `c C-x '` (on a suitably standard setup), then Emacs
will insert the following text:
```agda
\begin{code}<newline> <cursor><newline>\end{code}<newline>.
```
* The LaTeX backend can now be invoked from the Emacs mode.
Using the compilation command (`C-c C-x C-c`).
The flag `--latex-dir` can be used to set the output directory (by
default: `latex`). Note that if this directory is a relative path,
then it is interpreted relative to the "project root". (When the
LaTeX backend is invoked from the command line the path is
interpreted relative to the current working directory.) Example: If
the module `A.B.C` is located in the file `/foo/A/B/C.agda`, then
the project root is `/foo/`, and the default output directory is
`/foo/latex/`.
* The compilation command (`C-c C-x C-c`) now by default asks for a
backend.
To avoid this question, set the customisation variable
`agda2-backend` to an appropriate value.
* The command `agda2-measure-load-time` no longer "touches" the file,
and the optional argument `DONT-TOUCH` has been removed.
* New command `C-u (C-u) C-c C-s`: Simplify or normalise the solution `C-c C-s` produces
When writing examples, it is nice to have the hole filled in with
a normalised version of the solution. Calling `C-c C-s` on
```agda
_ : reverse (0 ∷ 1 ∷ []) ≡ ?
_ = refl
```
used to yield the non informative `reverse (0 ∷ 1 ∷ [])` when we would
have hopped to get `1 ∷ 0 ∷ []` instead. We can now control finely the
degree to which the solution is simplified.
* Changed feature: Solving the hole at point
Calling `C-c C-s` inside a specific goal does not solve *all* the goals
already instantiated internally anymore: it only solves the one at hand
(if possible).
* New bindings: All the blackboard bold letters are now available
[Pull Request [#2305](https://github.com/agda/agda/pull/2305)]
The Agda input method only bound a handful of the blackboard bold letters
but programmers were actually using more than these. They are now all
available: lowercase and uppercase. Some previous bindings had to be
modified for consistency. The naming scheme is as follows:
* `\bx` for lowercase blackboard bold
* `\bX` for uppercase blackboard bold
* `\bGx` for lowercase greek blackboard bold (similar to `\Gx` for
greeks)
* `\bGX` for uppercase greek blackboard bold (similar to `\GX` for
uppercase greeks)
* Replaced binding for go back
Use `M-,` (instead of `M-*`) for go back in Emacs ≥ 25.1 (and
continue using `M-*` with previous versions of Emacs).
Compiler backends
-----------------
* JS compiler backend
The JavaScript backend has been (partially) rewritten. The
JavaScript backend now supports most Agda features, notably
copatterns can now be compiled to JavaScript. Furthermore, the
existing optimizations from the other backends now apply to the
JavaScript backend as well.
* GHC, JS and UHC compiler backends
Added new primitives to built-in floats
[Issues [#2194](https://github.com/agda/agda/issues/2194) and
[#2200](https://github.com/agda/agda/issues/2200)]:
```agda
primFloatNegate : Float → Float
primCos : Float → Float
primTan : Float → Float
primASin : Float → Float
primACos : Float → Float
primATan : Float → Float
primATan2 : Float → Float → Float
```
LaTeX backend
-------------
* Code blocks are now (by default) surrounded by vertical space.
[Issue [#2198](https://github.com/agda/agda/issues/2198)]
Use `\AgdaNoSpaceAroundCode{}` to avoid this vertical space, and
`\AgdaSpaceAroundCode{}` to reenable it.
Note that, if `\AgdaNoSpaceAroundCode{}` is used, then empty lines
before or after a code block will not necessarily lead to empty
lines in the generated document. However, empty lines *inside* the
code block do (by default) lead to empty lines in the output.
If you prefer the previous behaviour, then you can use the `agda.sty`
file that came with the previous version of Agda.
* `\AgdaHide{...}` now eats trailing spaces (using `\ignorespaces`).
* New environments: `AgdaAlign`, `AgdaSuppressSpace` and
`AgdaMultiCode`.
Sometimes one might want to break up a code block into multiple
pieces, but keep code in different blocks aligned with respect to
each other. Then one can use the `AgdaAlign` environment. Example
usage:
```latex
\begin{AgdaAlign}
\begin{code}
code
code (more code)
\end{code}
Explanation...
\begin{code}
aligned with "code"
code (aligned with (more code))
\end{code}
\end{AgdaAlign}
```
Note that `AgdaAlign` environments should not be nested.
Sometimes one might also want to hide code in the middle of a code
block. This can be accomplished in the following way:
```latex
\begin{AgdaAlign}
\begin{code}
visible
\end{code}
\AgdaHide{
\begin{code}
hidden
\end{code}}
\begin{code}
visible
\end{code}
\end{AgdaAlign}
```
However, the result may be ugly: extra space is perhaps inserted
around the code blocks.
The `AgdaSuppressSpace` environment ensures that extra space is only
inserted before the first code block, and after the last one (but
not if `\AgdaNoSpaceAroundCode{}` is used).
The environment takes one argument, the number of wrapped code
blocks (excluding hidden ones). Example usage:
```latex
\begin{AgdaAlign}
\begin{code}
code
more code
\end{code}
Explanation...
\begin{AgdaSuppressSpace}{2}
\begin{code}
aligned with "code"
aligned with "more code"
\end{code}
\AgdaHide{
\begin{code}
hidden code
\end{code}}
\begin{code}
also aligned with "more code"
\end{code}
\end{AgdaSuppressSpace}
\end{AgdaAlign}
```
Note that `AgdaSuppressSpace` environments should not be nested.
There is also a combined environment, `AgdaMultiCode`, that combines
the effects of `AgdaAlign` and `AgdaSuppressSpace`.
Tools
-----
### agda-ghc-names
The `agda-ghc-names` now has its own repository at
https://github.com/agda/agda-ghc-names
and is no longer distributed with Agda.