Changelog for Agda-2.5.4

Release notes for Agda version 2.5.4

Installation and infrastructure

Language

Syntax

Pattern matching

Builtins

Reflection

Pragmas and options

Emacs mode

Compiler backends

LaTeX backend

HTML backend

List of closed issues

For 2.5.4, the following issues have been closed (see bug tracker):

Release notes for Agda version 2.5.3

Installation and infrastructure

Language

Pattern matching

Reflection

Built-ins

Miscellaneous

Emacs mode

Library management

Compiler backends

HTML backend

LaTeX backend

Pragmas and options

List of fixed issues

For 2.5.3, the following issues have been fixed (see bug tracker):

Release notes for Agda version 2.5.2

Installation and infrastructure

Language

Rewriting

Reflection

Type checking

Emacs mode

Compiler backends

LaTeX backend

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.

Release notes for Agda version 2.5.1.2

Release notes for Agda version 2.5.1.1

Installation and infrastructure

Bug fixes

Compiler backends

Release notes for Agda version 2.5.1

Documentation

Installation and infrastructure

Pragmas and options

Language

Operator syntax

Reflection

Literals and built-ins

Modules

Records

Instance search

Other changes

Type checking

Compiler backends

Emacs mode and interaction

Tools

LaTeX-backend

agda-ghc-names

Highlighting and textual backends

Fixed issues

See bug tracker (milestone 2.5.1)

Release notes for Agda version 2.4.2.5

Installation and infrastructure

Pragmas and options

Type checking

Fixed issues

See bug tracker

#1407

#1518

#1670

#1677

#1698

#1701

#1710

#1718

Release notes for Agda version 2.4.2.4

Installation and infrastructure

Pragmas and options

Language

Type checking

Interaction

Performance

Bug fixes

Issues fixed (see bug tracker):

#1546 (copattern matching and with-clauses)

#1560 (positivity checker inefficiency)

#1584 (let pattern with trailing implicit)

Release notes for Agda version 2.4.2.3

Installation and infrastructure

Language

Type checking

Emacs mode

Error messages

Compiler backends

Bug fixes

Release notes for Agda version 2.4.2.2

Bug fixes

Release notes for Agda version 2.4.2.1

Pragmas and options

Language

Type checking

Termination checking

Tools

LaTeX-backend

Bug fixes

Release notes for Agda version 2.4.2

Pragmas and options

Language

Type checking

Tools

Emacs mode

LaTeX-backend

Release notes for Agda 2 version 2.4.0.2

Release notes for Agda 2 version 2.4.0.1

Release notes for Agda 2 version 2.4.0

Installation and infrastructure

Pragmas and options

Language

Goal and error display

Type checking

Termination checking

Compiler backends

Tools

Emacs mode

LaTeX-backend

Release notes for Agda 2 version 2.3.2.2

Release notes for Agda 2 version 2.3.2.1

Installation

Type checking

Release notes for Agda 2 version 2.3.2

Installation

Pragmas and options

Language

Goal and error display

Type checking

Compiler backends

Tools

Emacs mode

LaTeX-backend

An experimental LaTeX-backend which does precise highlighting a la the HTML-backend and code alignment a la lhs2TeX has been added.

Here is a sample input literate Agda file:

\documentclass{article}

\usepackage{agda}

\begin{document}

The following module declaration will be hidden in the output.

\AgdaHide{
\begin{code}
module M where
\end{code}
}

Two or more spaces can be used to make the backend align stuff.

\begin{code}
data ℕ : Set where
  zero  : ℕ
  suc   : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero   + n = n
suc m  + n = suc (m + n)
\end{code}

\end{document}

To produce an output PDF issue the following commands:

agda --latex -i . <file>.lagda
pdflatex latex/<file>.tex

Only the top-most module is processed, like with lhs2tex and unlike with the HTML-backend. If you want to process imported modules you have to call agda --latex manually on each of those modules.

There are still issues related to formatting, see the bug tracker for more information:

https://code.google.com/p/agda/issues/detail?id=697

The default agda.sty might therefore change in backwards-incompatible ways, as work proceeds in trying to resolve those problems.

Implemented features:

Release notes for Agda 2 version 2.3.0

Language

Universe polymorphism

Meta-variables and unification

Irrelevance

Reflection

Compiler backends

MAlonzo

Epic

JavaScript

Tools

Release notes for Agda 2 version 2.2.10

Language

Tools

Release notes for Agda 2 version 2.2.8

Language

Tools

Release notes for Agda 2 version 2.2.6

Language

Tools

Release notes for Agda 2 version 2.2.4

Important changes since 2.2.2:

Release notes for Agda 2 version 2.2.2

Tools

Infrastructure

Release notes for Agda 2 version 2.2.0

Important changes since 2.1.2 (which was released 2007-08-16):

Language

Tools

Libraries

Documentation

Infrastructure