Release notes for Agda version 2.5.3
====================================

Installation and infrastructure
-------------------------------

* Added support for GHC 8.0.2 and 8.2.1.

* Removed support for GHC 7.6.3.

* Markdown support for literate Agda
  \[PR [#2357](https://github.com/agda/agda/pull/2357)].

  Files ending in `.lagda.md` will be parsed as literate Markdown files.

  + Code blocks start with  ```` ``` ```` or ```` ```agda ```` in its own line, and end with
    ```` ``` ````, also in its own line.
  + Code blocks which should be type-checked by Agda but should not be visible
    when the Markdown is rendered may be enclosed in HTML comment delimiters
    (`<!--`  and `-->`).
  + Code blocks which should be ignored by Agda, but rendered in the final
    document may be indented by four spaces.
  + Note that inline code fragments are not supported due to the difficulty of
    interpreting their indentation level with respect to the rest of the file.

Language
--------

### Pattern matching

* Dot patterns.

  The dot in front of an inaccessible pattern can now be skipped if the
  pattern consists entirely of constructors or literals. For example:
  ```agda
    open import Agda.Builtin.Bool

    data D : Bool → Set where
      c : D true

    f : (x : Bool) → D x → Bool
    f true c = true

  ```
  Before this change, you had to write `f .true c = true`.

* With-clause patterns can be replaced by _
  [Issue [#2363](https://github.com/agda/agda/issues/2363)].
  Example:
  ```agda
    test : Nat → Set
    test zero    with zero
    test _       | _ = Nat
    test (suc x) with zero
    test _       | _ = Nat
  ```
  We do not have to spell out the pattern of the parent clause
  (`zero` / `suc x`) in the with-clause if we do not need the
  pattern variables.  Note that `x` is not in scope in the
  with-clause!

  A more elaborate example, which cannot be reduced to
  an ellipsis `...`:
  ```agda
    record R : Set where
      coinductive -- disallow matching
      field f : Bool
            n : Nat

    data P (r : R) : Nat → Set where
      fTrue  : R.f r ≡ true → P r zero
      nSuc   : P r (suc (R.n r))

    data Q : (b : Bool) (n : Nat) →  Set where
      true! : Q true zero
      suc!  : ∀{b n} → Q b (suc n)

    test : (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
    test r nSuc       = suc!
    test r (fTrue p)  with R.f r
    test _ (fTrue ()) | false
    test _ _          | true = true!  -- underscore instead of (isTrue _)
  ```

* Pattern matching lambdas (also known as extended lambdas) can now be
  nullary, mirroring the behaviour for ordinary function definitions.
  [Issue [#2671](https://github.com/agda/agda/issues/2671)]

  This is useful for case splitting on the result inside an
  expression: given
  ```agda
  record _×_ (A B : Set) : Set where
    field
      π₁ : A
      π₂ : B
  open _×_
  ```
  one may case split on the result (C-c C-c RET) in a hole
  ```agda
    λ { → {!!}}
  ```
  of type A × B to produce
  ```agda
    λ { .π₁ → {!!} ; .π₂ → {!!}}
  ```

* Records with a field of an empty type are now recognized as empty by Agda.
  In particular, they can be matched against with an absurd pattern ().
  For example:
  ```agda
    data ⊥ : Set where

    record Empty : Set where
      field absurdity : ⊥

    magic : Empty → ⊥
    magic ()
  ```

* Injective pragmas.

  Injective pragmas can be used to mark a definition as injective for the
  pattern matching unifier. This can be used as a version of
  `--injective-type-constructors` that only applies to specific datatypes.
  For example:
  ```agda
    open import Agda.Builtin.Equality
    data Fin : Nat → Set where
      zero : {n : Nat} → Fin (suc n)
      suc  : {n : Nat} → Fin n → Fin (suc n)

    {-# INJECTIVE Fin #-}

    Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
    Fin-injective refl = refl
  ```
  Aside from datatypes, this pragma can also be used to mark other definitions
  as being injective (for example postulates).

* Metavariables can no longer be instantiated during case splitting. This means
  Agda will refuse to split instead of taking the first constructor it finds.
  For example:
  ```agda
    open import Agda.Builtin.Nat

    data Vec (A : Set) : Nat → Set where
      nil : Vec A 0
      cons : {n : Nat} → A → Vec A n → Vec A (suc n)

    foo : Vec Nat _ → Nat
    foo x = {!x!}
  ```
  In Agda 2.5.2, case splitting on `x` produced the single clause
  `foo nil = {!!}`, but now Agda refuses to split.

### Reflection

* New TC primitive: `debugPrint`.

  ```agda
    debugPrint : String → Nat → List ErrorPart → TC ⊤
  ```

  This maps to the internal function `reportSDoc`. Debug output is enabled with
  the `-v` flag at the command line, or in an `OPTIONS` pragma. For instance,
  giving `-v a.b.c:10` enables printing from `debugPrint "a.b.c.d" 10 msg`. In the
  Emacs mode, debug output ends up in the `*Agda debug*` buffer.

### Built-ins

* BUILTIN REFL is now superfluous, subsumed by BUILTIN EQUALITY
  [Issue [#2389](https://github.com/agda/agda/issues/2389)].

* BUILTIN EQUALITY is now more liberal
  [Issue [#2386](https://github.com/agda/agda/issues/2386)].
  It accepts, among others, the following new definitions of equality:
  ```agda
    -- Non-universe polymorphic:
    data _≡_ {A : Set} (x : A) : A → Set where
      refl : x ≡ x

    -- ... with explicit argument to refl;
    data _≡_ {A : Set} : (x y : A) → Set where
      refl : {x : A} → x ≡ x

    -- ... even visible
    data _≡_ {A : Set} : (x y : A) → Set where
      refl : (x : A) → x ≡ x

    -- Equality in a different universe than domain:
    -- (also with explicit argument to refl)
    data _≡_ {a} {A : Set a} (x : A) : A → Set where
      refl : x ≡ x

  ```
  The standard definition is still:
  ```agda
    -- Equality in same universe as domain:
    data _≡_ {a} {A : Set a} (x : A) : A → Set a where
      refl : x ≡ x
  ```

### Miscellaneous

* Rule change for omitted top-level module headers.
  [Issue [#1077](https://github.com/agda/agda/issues/1077)]

  If your file is named `Bla.agda`, then the following content
  is rejected.
  ```agda
    foo = Set
    module Bla where
      bar = Set
  ```
  Before the fix of this issue, Agda would add the missing module
  header `module Bla where` at the top of the file.
  However, in this particular case it is more likely the user
  put the declaration `foo = Set` before the module start in error.
  Now you get the error
  ```
    Illegal declaration(s) before top-level module
  ```
  if the following conditions are met:

    1. There is at least one non-import declaration or non-toplevel pragma
       before the start of the first module.

    2. The module has the same name as the file.

    3. The module is the only module at this level
       (may have submodules, of course).

  If you should see this error, insert a top-level module
  before the illegal declarations, or move them inside the
  existing module.

Emacs mode
----------

* New warnings:

  - Unreachable clauses give rise to a simple warning. They are
    highlighted in gray.

  - Incomplete patterns are non-fatal warnings: it is possible
    to keep interacting with the file (the reduction will simply
    be stuck on arguments not matching any pattern).
    The definition with incomplete patterns are highlighted in
    wheat.

* Clauses which do not hold definitionally are now highlighted in white smoke.

* Fewer commands have the side effect that the buffer is saved.

* Aborting commands.

  Now one can (try to) abort an Agda command by using `C-c C-x C-a` or
  a menu entry. The effect is similar to that of restarting Agda (`C-c
  C-x C-r`), but some state is preserved, which could mean that it
  takes less time to reload the module.

  Warning: If a command is aborted while it is writing data to disk
  (for instance `.agdai` files or Haskell files generated by the GHC
  backend), then the resulting files may be corrupted. Note also that
  external commands (like GHC) are not aborted, and their output may
  continue to be sent to the Emacs mode.

* New bindings for the Agda input method:

  - All the bold digits are now available. The naming scheme is `\Bx` for digit `x`.

  - Typing `\:` you can now get a whole slew of colons.

    (The Agda input method originally only bound the standard unicode colon,
    which looks deceptively like the normal colon.)

* Case splitting now preserves underscores.
  [Issue [#819](https://github.com/agda/agda/issues/819)]
  ```agda
    data ⊥ : Set where

    test : {A B : Set} → A → ⊥ → B
    test _ x = {! x !}
  ```
  Splitting on `x` yields
  ```agda
    test _ ()
  ```

* Interactively expanding ellipsis.
  [Issue [#2589](https://github.com/agda/agda/issues/2589)]
  An ellipsis in a with-clause can be expanded by splitting on "variable" "." (dot).
  ```agda
    test0 : Nat → Nat
    test0 x with zero
    ... | q = {! . !}  -- C-c C-c
  ```
  Splitting on dot here yields:
  ```agda
    test0 x | q = ?
  ```

* New command to check an expression against the type of the hole
  it is in and see what it elaborates to.
  [Issue [#2700](https://github.com/agda/agda/issues/2700)]
  This is useful to determine e.g. what solution typeclass resolution yields.
  The command is bound to `C-c C-;` and respects the `C-u` modifier.

  ```agda
    record Pointed (A : Set) : Set where
      field point : A

    it : ∀ {A : Set} {{x : A}} → A
    it {{x}} = x

    instance _ = record { point = 3 - 4 }

    _ : Pointed Nat
    _ = {! it !} -- C-u C-u C-c C-;
  ```
  yields
  ```agda
    Goal: Pointed Nat
    Elaborates to: record { point = 0 }
  ```

* If `agda2-give` is called with a prefix, then giving is forced,
  i.e., the safety checks are skipped,
  including positivity, termination, and double type-checking.
  [Issue [#2730](https://github.com/agda/agda/issues/2730)]

  Invoke forced giving with key sequence `C-u C-c C-SPC`.


Library management
------------------

* The `name` field in an `.agda-lib` file is now optional.
  [Issue [#2708](https://github.com/agda/agda/issues/2708)]

  This feature is convenient if you just want to specify the dependencies
  and include pathes for your local project in an `.agda-lib` file.

  Naturally, libraries without names cannot be depended on.


Compiler backends
-----------------

* Unified compiler pragmas

  The compiler pragmas (`COMPILED`, `COMPILED_DATA`, etc.) have been unified across
  backends into two new pragmas:

  ```
    {-# COMPILE <Backend> <Name> <Text> #-}
    {-# FOREIGN <Backend> <Text> #-}
  ```

  The old pragmas still work, but will emit a warning if used. They will be
  removed completely in Agda 2.6.

  The translation of old pragmas into new ones is as follows:

  Old | New
  --- | ---
  `{-# COMPILED f e #-}` | `{-# COMPILE GHC f = e #-}`
  `{-# COMPILED_TYPE A T #-}` | `{-# COMPILE GHC A = type T #-}`
  `{-# COMPILED_DATA A D C1 .. CN #-}` | `{-# COMPILE GHC A = data D (C1 \| .. \| CN) #-}`
  `{-# COMPILED_DECLARE_DATA #-}` | obsolete, removed
  `{-# COMPILED_EXPORT f g #-}` | `{-# COMPILE GHC f as g #-}`
  `{-# IMPORT M #-}` | `{-# FOREIGN GHC import qualified M #-}`
  `{-# HASKELL code #-}` | `{-# FOREIGN GHC code #-}`
  `{-# COMPILED_UHC f e #-}` | `{-# COMPILE UHC f = e #-}`
  `{-# COMPILED_DATA_UHC A D C1 .. CN #-}` | `{-# COMPILE UHC A = data D (C1 \| .. \| CN) #-}`
  `{-# IMPORT_UHC M #-}` | `{-# FOREIGN UHC __IMPORT__ M #-}`
  `{-# COMPILED_JS f e #-}` | `{-# COMPILE JS f = e #-}`

* GHC Haskell backend

  The COMPILED pragma (and the corresponding COMPILE GHC pragma) is now also
  allowed for functions. This makes it possible to have both an Agda
  implementation and a native Haskell runtime implementation.

  The GHC file header pragmas `LANGUAGE`, `OPTIONS_GHC`, and `INCLUDE`
  inside a `FOREIGN GHC` pragma are recognized and printed correctly
  at the top of the generated Haskell file.
  [Issue [#2712](https://github.com/agda/agda/issues/2712)]


* UHC compiler backend

  The UHC backend has been moved to its own repository
  [https://github.com/agda/agda-uhc] and is no longer part of the Agda
  distribution.

* Haskell imports are no longer transitively inherited from imported modules.

  The (now deprecated) IMPORT and IMPORT_UHC pragmas no longer cause import
  statements in modules importing the module containing the pragma.

  The same is true for the corresponding FOREIGN pragmas.

* Support for stand-alone backends.

  There is a new API in `Agda.Compiler.Backend` for creating stand-alone
  backends using Agda as a library. This allows prospective backend writers to
  experiment with new backends without having to change the Agda code base.

HTML backend
------------

* Anchors for identifiers (excluding bound variables) are now the
  identifiers themselves rather than just the file position
  [Issue [#2604](https://github.com/agda/agda/issues/2604)].

  Symbolic anchors look like
  ```html
  <a id="test1">
  <a id="M.bla">
  ```
  while other anchors just give the character position in the file:
  ```html
  <a id="42">
  ```

  Top-level module names do not get a symbolic anchor, since the position of
  a top-level module is defined to be the beginning of the file.

  Example:

  ```agda
  module Issue2604 where   -- Character position anchor

  test1 : Set₁             -- Issue2604.html#test1
  test1 = bla
    where
    bla = Set              -- Character position anchor

  test2 : Set₁             -- Issue2604.html#test2
  test2 = bla
    where
    bla = Set              -- Character position anchor

  test3 : Set₁             -- Issue2604.html#test3
  test3 = bla
    module M where         -- Issue2604.html#M
    bla = Set              -- Issue2604.html#M.bla

  module NamedModule where -- Issue2604.html#NamedModule
    test4 : Set₁           -- Issue2604.html#NamedModule.test4
    test4 = M.bla

  module _ where           -- Character position anchor
    test5 : Set₁           -- Character position anchor
    test5 = M.bla
  ```

* Some generated HTML files now have different file names [Issue
  [#2725](https://github.com/agda/agda/issues/2725)].

  Agda now uses an encoding that amounts to first converting the
  module names to UTF-8, and then percent-encoding the resulting
  bytes. For instance, HTML for the module `Σ` is placed in
  `%CE%A3.html`.

LaTeX backend
-------------

* The LaTeX backend now handles indentation in a different way [Issue
  [#1832](https://github.com/agda/agda/issues/1832)].

  A constraint on the indentation of the first token *t* on a line is
  determined as follows:
  * Let *T* be the set containing every previous token (in any code
    block) that is either the initial token on its line or preceded by
    at least one whitespace character.
  * Let *S* be the set containing all tokens in *T* that are not
    *shadowed* by other tokens in *T*. A token *t₁* is shadowed by
    *t₂* if *t₂* is further down than *t₁* and does not start to the
    right of *t₁*.
  * Let *L* be the set containing all tokens in *S* that start to the
    left of *t*, and *E* be the set containing all tokens in *S* that
    start in the same column as *t*.
  * The constraint is that *t* must be indented further than every
    token in *L*, and aligned with every token in *E*.

  Note that if any token in *L* or *E* belongs to a previous code
  block, then the constraint may not be satisfied unless (say) the
  `AgdaAlign` environment is used in an appropriate way.

  If custom settings are used, for instance if `\AgdaIndent` is
  redefined, then the constraint discussed above may not be satisfied.
  (Note that the meaning of the `\AgdaIndent` command's argument has
  changed, and that the command is now used in a different way in the
  generated LaTeX files.)

  Examples:
  * Here `C` is indented further than `B`:

    ```agda
    postulate
      A  B
          C : Set
    ```

  * Here `C` is not (necessarily) indented further than `B`, because
    `X` shadows `B`:

    ```agda
    postulate
      A  B  : Set
      X
          C : Set
    ```

  The new rule is inspired by, but not identical to, the one used by
  lhs2TeX's poly mode (see Section 8.4 of the [manual for lhs2TeX
  version 1.17](https://www.andres-loeh.de/lhs2tex/Guide2-1.17.pdf)).

* Some spacing issues
  [[#2353](https://github.com/agda/agda/issues/2353),
  [#2441](https://github.com/agda/agda/issues/2441),
  [#2733](https://github.com/agda/agda/issues/2733),
  [#2740](https://github.com/agda/agda/issues/2740)] have been fixed.

* The user can now control the typesetting of (certain) individual tokens
  by redefining the `\AgdaFormat` command. Example:
  ```latex
  \usepackage{ifthen}

  % Insert extra space before some tokens.
  \DeclareRobustCommand{\AgdaFormat}[2]{%
    \ifthenelse{
      \equal{#1}{≡⟨} \OR
      \equal{#1}{≡⟨⟩} \OR
      \equal{#1}{∎}
    }{\ }{}#2}
  ```
  Note the use of `\DeclareRobustCommand`. The first argument to
  `\AgdaFormat` is the token, and the second argument the thing to
  be typeset.

* One can now instruct the agda package not to select any fonts.

  If the `nofontsetup` option is used, then some font packages are
  loaded, but specific fonts are not selected:
  ```latex
  \usepackage[nofontsetup]{agda}
  ```

* The height of empty lines is now configurable
  [[#2734](https://github.com/agda/agda/issues/2734)].

  The height is controlled by the length `\AgdaEmptySkip`, which by
  default is `\baselineskip`.

* The alignment feature regards the string `+̲`, containing `+` and a
  combining character, as having length two. However, it seems more
  reasonable to treat it as having length one, as it occupies a single
  column, if displayed "properly" using a monospace font. The new flag
  `--count-clusters` is an attempt at fixing this. When this flag is
  enabled the backend counts ["extended grapheme
  clusters"](http://www.unicode.org/reports/tr29/#Grapheme_Cluster_Boundaries)
  rather than code points.

  Note that this fix is not perfect: a single extended grapheme
  cluster might be displayed in different ways by different programs,
  and might, in some cases, occupy more than one column. Here are some
  examples of extended grapheme clusters, all of which are treated as
  a single character by the alignment algorithm:
  ```
  │ │
  │+̲│
  │Ö̂│
  │நி│
  │ᄀힰᇹ│
  │ᄀᄀᄀᄀᄀᄀힰᇹᇹᇹᇹᇹᇹ│
  │ │
  ```

  Note also that the layout machinery does not count extended grapheme
  clusters, but code points. The following code is syntactically
  correct, but if `--count-clusters` is used, then the LaTeX backend
  does not align the two `field` keywords:
  ```agda
    record +̲ : Set₁ where  field A : Set
                            field B : Set
  ```

  The `--count-clusters` flag is not enabled in all builds of Agda,
  because the implementation depends on the
  [ICU](http://site.icu-project.org) library, the installation of
  which could cause extra trouble for some users. The presence of this
  flag is controlled by the Cabal flag `enable-cluster-counting`.

* A faster variant of the LaTeX backend: QuickLaTeX.

  When this variant of the backend is used the top-level module is not
  type-checked, only scope-checked. This implies that some
  highlighting information is not available. For instance, overloaded
  constructors are not resolved.

  QuickLaTeX can be invoked from the Emacs mode, or using `agda
  --latex --only-scope-checking`. If the module has already been
  type-checked successfully, then this information is reused; in this
  case QuickLaTeX behaves like the regular LaTeX backend.

  The `--only-scope-checking` flag can also be used independently, but
  it is perhaps unclear what purpose that would serve. (The flag can
  currently not be combined with `--html`, `--dependency-graph` or
  `--vim`.) The flag is not allowed in safe mode.

Pragmas and options
-------------------

* The `--safe` option is now a valid pragma.

  This makes it possible to declare a module as being part of the safe
  subset of the language by stating `{-# OPTIONS --safe #-}` at the top
  of the corresponding file. Incompatibilities between the `--safe` option
  and other options or language constructs are non-fatal errors.

* The `--no-main` option is now a valid pragma.

  One can now suppress the compiler warning about a missing main function by
  putting
  ```agda
    {-# OPTIONS --no-main #-}
  ```
  on top of the file.

* New command-line option and pragma `--warning=MODE` (or `-W MODE`) for
  setting the warning mode. Current options are
  - `warn` for displaying warnings (default)
  - `error` for turning warnings into errors
  - `ignore` for not displaying warnings

List of fixed issues
--------------------

For 2.5.3, the following issues have been fixed
(see [bug tracker](https://github.com/agda/agda/issues)):

  - [#142](https://github.com/agda/agda/issues/142): Inherited dot patterns in with functions are not checked
  - [#623](https://github.com/agda/agda/issues/623): Error message points to importing module rather than imported module
  - [#657](https://github.com/agda/agda/issues/657): Yet another display form problem
  - [#668](https://github.com/agda/agda/issues/668): Ability to stop, or restart, typechecking somehow
  - [#705](https://github.com/agda/agda/issues/705): confusing error message for ambiguous datatype module name
  - [#719](https://github.com/agda/agda/issues/719): Error message for duplicate module definition points to external module instead of internal module
  - [#776](https://github.com/agda/agda/issues/776): Unsolvable constraints should give error
  - [#819](https://github.com/agda/agda/issues/819): Case-splitting doesn't preserve underscores
  - [#883](https://github.com/agda/agda/issues/883): Rewrite loses type information
  - [#899](https://github.com/agda/agda/issues/899): Instance search fails if there are several definitionally equal values in scope
  - [#1077](https://github.com/agda/agda/issues/1077): problem with module syntax, with parametric module import
  - [#1126](https://github.com/agda/agda/issues/1126): Port optimizations from the Epic backend
  - [#1175](https://github.com/agda/agda/issues/1175): Internal Error in Auto
  - [#1544](https://github.com/agda/agda/issues/1544): Positivity polymorphism needed for compositional positivity analysis
  - [#1611](https://github.com/agda/agda/issues/1611): Interactive splitting instantiates meta
  - [#1664](https://github.com/agda/agda/issues/1664): Add Reflection primitives to expose precedence and fixity
  - [#1817](https://github.com/agda/agda/issues/1817): Solvable size constraints reported as unsolvable
  - [#1832](https://github.com/agda/agda/issues/1832): Insufficient indentation in LaTeX-rendered Agda code
  - [#1834](https://github.com/agda/agda/issues/1834): Copattern matching: order of clauses should not matter here
  - [#1886](https://github.com/agda/agda/issues/1886): Second copies of telescopes not checked?
  - [#1899](https://github.com/agda/agda/issues/1899): Positivity checker does not treat datatypes and record types in the same way
  - [#1975](https://github.com/agda/agda/issues/1975): Type-incorrect instantiated overloaded constructor accepted in pattern
  - [#1976](https://github.com/agda/agda/issues/1976): Type-incorrect instantiated projection accepted in pattern
  - [#2035](https://github.com/agda/agda/issues/2035): Matching on string causes solver to fail with internal error
  - [#2146](https://github.com/agda/agda/issues/2146): Unicode syntax for instance arguments
  - [#2217](https://github.com/agda/agda/issues/2217): Abort Agda without losing state
  - [#2229](https://github.com/agda/agda/issues/2229): Absence or presence of top-level module header affects scope
  - [#2253](https://github.com/agda/agda/issues/2253): Wrong scope error for abstract constructors
  - [#2261](https://github.com/agda/agda/issues/2261): Internal error in Auto/CaseSplit.hs:284
  - [#2270](https://github.com/agda/agda/issues/2270): Printer does not use sections.
  - [#2329](https://github.com/agda/agda/issues/2329): Size solver does not use type `Size< i` to gain the necessary information
  - [#2354](https://github.com/agda/agda/issues/2354): Interaction between instance search, size solver, and ordinary constraint solver.
  - [#2355](https://github.com/agda/agda/issues/2355): Literate Agda parser does not recognize TeX comments
  - [#2360](https://github.com/agda/agda/issues/2360): With clause stripping chokes on ambiguous projection
  - [#2362](https://github.com/agda/agda/issues/2362): Printing of parent patterns when with-clause does not match
  - [#2363](https://github.com/agda/agda/issues/2363): Allow underscore in with-clause patterns
  - [#2366](https://github.com/agda/agda/issues/2366): With-clause patterns renamed in error message
  - [#2368](https://github.com/agda/agda/issues/2368): Internal error after refining a tactic @ MetaVars.hs:267
  - [#2371](https://github.com/agda/agda/issues/2371): Shadowed module parameter crashes interaction
  - [#2372](https://github.com/agda/agda/issues/2372): problems when instances are declared with inferred types
  - [#2374](https://github.com/agda/agda/issues/2374): Ambiguous projection pattern could be disambiguated by visibility
  - [#2376](https://github.com/agda/agda/issues/2376): Termination checking interacts badly with eta-contraction
  - [#2377](https://github.com/agda/agda/issues/2377): open public is useless before module header
  - [#2381](https://github.com/agda/agda/issues/2381): Search (`C-c C-z`) panics on pattern synonyms
  - [#2386](https://github.com/agda/agda/issues/2386): Relax requirements of BUILTIN EQUALITY
  - [#2389](https://github.com/agda/agda/issues/2389): BUILTIN REFL not needed
  - [#2400](https://github.com/agda/agda/issues/2400): LaTeX backend error on LaTeX comments
  - [#2402](https://github.com/agda/agda/issues/2402): Parameters not dropped when reporting incomplete patterns
  - [#2403](https://github.com/agda/agda/issues/2403): Termination checker should reduce arguments in structural order check
  - [#2405](https://github.com/agda/agda/issues/2405): instance search failing in parameterized module
  - [#2408](https://github.com/agda/agda/issues/2408): DLub sorts are not serialized
  - [#2412](https://github.com/agda/agda/issues/2412): Problem with checking  with sized types
  - [#2413](https://github.com/agda/agda/issues/2413): Agda crashes on x@y pattern
  - [#2415](https://github.com/agda/agda/issues/2415): Size solver reports "inconsistent upper bound" even though there is a solution
  - [#2416](https://github.com/agda/agda/issues/2416): Cannot give size as computed by solver
  - [#2422](https://github.com/agda/agda/issues/2422): Overloaded inherited projections don't resolve
  - [#2423](https://github.com/agda/agda/issues/2423): Inherited projection on lhs
  - [#2426](https://github.com/agda/agda/issues/2426): On just warning about missing cases
  - [#2429](https://github.com/agda/agda/issues/2429): Irrelevant lambda should be accepted when relevant lambda is expected
  - [#2430](https://github.com/agda/agda/issues/2430): Another regression related to parameter refinement?
  - [#2433](https://github.com/agda/agda/issues/2433): rebindLocalRewriteRules re-adds global rewrite rules
  - [#2434](https://github.com/agda/agda/issues/2434): Exact split analysis is too strict when matching on eta record constructor
  - [#2441](https://github.com/agda/agda/issues/2441): Incorrect alignement in latex using the new ACM format
  - [#2444](https://github.com/agda/agda/issues/2444): Generalising compiler pragmas
  - [#2445](https://github.com/agda/agda/issues/2445): The LaTeX backend is slow
  - [#2447](https://github.com/agda/agda/issues/2447): Cache loaded interfaces even if a type error is encountered
  - [#2449](https://github.com/agda/agda/issues/2449): Agda depends on additional C library icu
  - [#2451](https://github.com/agda/agda/issues/2451): Agda panics when attempting to rewrite a typeclass Eq
  - [#2456](https://github.com/agda/agda/issues/2456): Internal error when postulating instance
  - [#2458](https://github.com/agda/agda/issues/2458): Regression: Agda-2.5.3 loops where Agda-2.5.2 passes
  - [#2462](https://github.com/agda/agda/issues/2462): Overloaded postfix projection does not resolve
  - [#2464](https://github.com/agda/agda/issues/2464): Eta contraction for irrelevant functions breaks subject reduction
  - [#2466](https://github.com/agda/agda/issues/2466): Case split to make hidden variable visible does not work
  - [#2467](https://github.com/agda/agda/issues/2467): REWRITE without BUILTIN REWRITE crashes
  - [#2469](https://github.com/agda/agda/issues/2469): "Partial" pattern match causes segfault at runtime
  - [#2472](https://github.com/agda/agda/issues/2472): Regression related to the auto command
  - [#2477](https://github.com/agda/agda/issues/2477): Sized data type analysis brittle, does not reduce size
  - [#2478](https://github.com/agda/agda/issues/2478): Multiply defined labels on the user manual (pdf)
  - [#2479](https://github.com/agda/agda/issues/2479): "Occurs check" error in generated Haskell code
  - [#2480](https://github.com/agda/agda/issues/2480): Agda accepts incorrect (?) code, subject reduction broken
  - [#2482](https://github.com/agda/agda/issues/2482): Wrong counting of data parameters with new-style mutual blocks
  - [#2483](https://github.com/agda/agda/issues/2483): Files are sometimes truncated to a size of 201 bytes
  - [#2486](https://github.com/agda/agda/issues/2486): Imports via FOREIGN are not transitively inherited anymore
  - [#2488](https://github.com/agda/agda/issues/2488): Instance search inhibits holes for instance fields
  - [#2493](https://github.com/agda/agda/issues/2493): Regression: Agda seems to loop when expression is given
  - [#2494](https://github.com/agda/agda/issues/2494): Instance fields sometimes have incorrect goal types
  - [#2495](https://github.com/agda/agda/issues/2495): Regression: termination checker of Agda-2.5.3 seemingly loops where Agda-2.5.2 passes
  - [#2500](https://github.com/agda/agda/issues/2500): Adding fields to a record can cause Agda to reject previous definitions
  - [#2510](https://github.com/agda/agda/issues/2510): Wrong error with --no-pattern-matching
  - [#2517](https://github.com/agda/agda/issues/2517): "Not a variable error"
  - [#2518](https://github.com/agda/agda/issues/2518): CopatternReductions in TreeLess
  - [#2523](https://github.com/agda/agda/issues/2523): The documentation of `--without-K` is outdated
  - [#2529](https://github.com/agda/agda/issues/2529): Unable to install Agda on Windows.
  - [#2537](https://github.com/agda/agda/issues/2537): case splitting with 'with' creates {_} instead of replicating the arguments it found.
  - [#2538](https://github.com/agda/agda/issues/2538): Internal error when parsing as-pattern
  - [#2543](https://github.com/agda/agda/issues/2543): Case splitting with ellipsis produces spurious parentheses
  - [#2545](https://github.com/agda/agda/issues/2545): Race condition in api tests
  - [#2549](https://github.com/agda/agda/issues/2549): Rewrite rule for higher path constructor does not fire
  - [#2550](https://github.com/agda/agda/issues/2550): Internal error in Agda.TypeChecking.Substitute
  - [#2552](https://github.com/agda/agda/issues/2552): Let bindings in module telescopes crash Agda.Interaction.BasicOps
  - [#2553](https://github.com/agda/agda/issues/2553): Internal error in Agda.TypeChecking.CheckInternal
  - [#2554](https://github.com/agda/agda/issues/2554): More flexible size-assignment in successor style
  - [#2555](https://github.com/agda/agda/issues/2555): Why does the positivity checker care about non-recursive occurrences?
  - [#2558](https://github.com/agda/agda/issues/2558): Internal error in Warshall Solver
  - [#2560](https://github.com/agda/agda/issues/2560): Internal Error in Reduce.Fast
  - [#2564](https://github.com/agda/agda/issues/2564): Non-exact-split highlighting makes other highlighting disappear
  - [#2568](https://github.com/agda/agda/issues/2568): agda2-infer-type-maybe-toplevel (in hole) does not respect "single-solution" requirement of instance resolution
  - [#2571](https://github.com/agda/agda/issues/2571): Record pattern translation does not eta contract
  - [#2573](https://github.com/agda/agda/issues/2573): Rewrite rules fail depending on unrelated changes
  - [#2574](https://github.com/agda/agda/issues/2574): No link attached to module without toplevel name
  - [#2575](https://github.com/agda/agda/issues/2575): Internal error, related to caching
  - [#2577](https://github.com/agda/agda/issues/2577): deBruijn fail for higher order instance problem
  - [#2578](https://github.com/agda/agda/issues/2578): Catch-all clause face used incorrectly for parent with pattern
  - [#2579](https://github.com/agda/agda/issues/2579): Import statements with module instantiation should not trigger an error message
  - [#2580](https://github.com/agda/agda/issues/2580): Implicit absurd match is NonVariant, explicit not
  - [#2583](https://github.com/agda/agda/issues/2583): Wrong de Bruijn index introduced by absurd pattern
  - [#2584](https://github.com/agda/agda/issues/2584): Duplicate warning printing
  - [#2585](https://github.com/agda/agda/issues/2585): Definition by copatterns not modulo eta
  - [#2586](https://github.com/agda/agda/issues/2586): "λ where" with single absurd clause not parsed
  - [#2588](https://github.com/agda/agda/issues/2588): `agda --latex` produces invalid LaTeX when there are block comments
  - [#2592](https://github.com/agda/agda/issues/2592): Internal Error in Agda/TypeChecking/Serialise/Instances/Common.hs
  - [#2597](https://github.com/agda/agda/issues/2597): Inline record definitions confuse the reflection API
  - [#2602](https://github.com/agda/agda/issues/2602): Debug output messes up AgdaInfo buffer
  - [#2603](https://github.com/agda/agda/issues/2603): Internal error in MetaVars.hs
  - [#2604](https://github.com/agda/agda/issues/2604): Use QNames as anchors in generated HTML
  - [#2605](https://github.com/agda/agda/issues/2605): HTML backend generates anchors for whitespace
  - [#2606](https://github.com/agda/agda/issues/2606): Check that LHS of a rewrite rule doesn't reduce is too strict
  - [#2612](https://github.com/agda/agda/issues/2612): `exact-split` documentation is outdated and incomplete
  - [#2613](https://github.com/agda/agda/issues/2613): Parametrised modules, with-abstraction and termination
  - [#2620](https://github.com/agda/agda/issues/2620): Internal error in auto.
  - [#2621](https://github.com/agda/agda/issues/2621): Case splitting instantiates meta
  - [#2626](https://github.com/agda/agda/issues/2626): triggered internal error with sized types in MetaVars module
  - [#2629](https://github.com/agda/agda/issues/2629): Exact splitting should not complain about absurd clauses
  - [#2631](https://github.com/agda/agda/issues/2631): docs for auto aren't clear on how to use flags/options
  - [#2632](https://github.com/agda/agda/issues/2632): some flags to auto dont seem to work in current agda 2.5.2
  - [#2637](https://github.com/agda/agda/issues/2637): Internal error in Agda.TypeChecking.Pretty, possibly related to sized types
  - [#2639](https://github.com/agda/agda/issues/2639): Performance regression, possibly related to the size solver
  - [#2641](https://github.com/agda/agda/issues/2641): Required instance of FromNat when compiling imported files
  - [#2642](https://github.com/agda/agda/issues/2642): Records with duplicate fields
  - [#2644](https://github.com/agda/agda/issues/2644): Wrong substitution in expandRecordVar
  - [#2645](https://github.com/agda/agda/issues/2645): Agda accepts postulated fields in a record
  - [#2646](https://github.com/agda/agda/issues/2646): Only warn if fixities for undefined symbols are given
  - [#2649](https://github.com/agda/agda/issues/2649): Empty list of "previous definition" in duplicate definition error
  - [#2652](https://github.com/agda/agda/issues/2652): Added a new variant of the colon to the Agda input method
  - [#2653](https://github.com/agda/agda/issues/2653): agda-mode: "cannot refine" inside instance argument even though term to be refined typechecks there
  - [#2654](https://github.com/agda/agda/issues/2654): Internal error on result splitting without --postfix-projections
  - [#2664](https://github.com/agda/agda/issues/2664): Segmentation fault with compiled programs using mutual record
  - [#2665](https://github.com/agda/agda/issues/2665): Documentation: Record update syntax in wrong location
  - [#2666](https://github.com/agda/agda/issues/2666): Internal error at Agda/Syntax/Abstract/Name.hs:113
  - [#2667](https://github.com/agda/agda/issues/2667): Panic error on unbound variable.
  - [#2669](https://github.com/agda/agda/issues/2669): Interaction: incorrect field variable name generation
  - [#2671](https://github.com/agda/agda/issues/2671): Feature request: nullary pattern matching lambdas
  - [#2679](https://github.com/agda/agda/issues/2679): Internal error at "Typechecking/Abstract.hs:133" and "TypeChecking/Telescope.hs:68"
  - [#2682](https://github.com/agda/agda/issues/2682): What are the rules for projections of abstract records?
  - [#2684](https://github.com/agda/agda/issues/2684): Bad error message for abstract constructor
  - [#2686](https://github.com/agda/agda/issues/2686): Abstract constructors should be ignored when resolving overloading
  - [#2690](https://github.com/agda/agda/issues/2690): [regression?] Agda engages in deep search instead of immediately failing
  - [#2700](https://github.com/agda/agda/issues/2700): Add a command to check against goal type (and normalise)
  - [#2703](https://github.com/agda/agda/issues/2703): Regression: Internal error for underapplied indexed constructor
  - [#2705](https://github.com/agda/agda/issues/2705): The GHC backend might diverge in infinite file creation
  - [#2708](https://github.com/agda/agda/issues/2708): Why is the `name` field in .agda-lib files mandatory?
  - [#2710](https://github.com/agda/agda/issues/2710): Type checker hangs
  - [#2712](https://github.com/agda/agda/issues/2712): Compiler Pragma for headers
  - [#2714](https://github.com/agda/agda/issues/2714): Option --no-main should be allowed as file-local option
  - [#2717](https://github.com/agda/agda/issues/2717): internal error at DisplayForm.hs:197
  - [#2718](https://github.com/agda/agda/issues/2718): Interactive 'give' doesn't insert enough parenthesis
  - [#2721](https://github.com/agda/agda/issues/2721): Without-K doesn't prevent heterogeneous conflict between literals
  - [#2723](https://github.com/agda/agda/issues/2723): Unreachable clauses in definition by copattern matching trip clause compiler
  - [#2725](https://github.com/agda/agda/issues/2725): File names for generated HTML files
  - [#2726](https://github.com/agda/agda/issues/2726): Old regression related to with
  - [#2727](https://github.com/agda/agda/issues/2727): Internal errors related to rewrite
  - [#2729](https://github.com/agda/agda/issues/2729): Regression: case splitting uses variable name variants instead of the unused original names
  - [#2730](https://github.com/agda/agda/issues/2730): Command to give in spite of termination errors
  - [#2731](https://github.com/agda/agda/issues/2731): Agda fails to build with happy 1.19.6
  - [#2733](https://github.com/agda/agda/issues/2733): Avoid some uses of \AgdaIndent?
  - [#2734](https://github.com/agda/agda/issues/2734): Make height of empty lines configurable
  - [#2736](https://github.com/agda/agda/issues/2736): Segfault using Alex 3.2.2 and cpphs
  - [#2740](https://github.com/agda/agda/issues/2740): Indenting every line of code should be a no-op