Changelog for Agda-2.4.0.1

If this renders badly as markdown, see the plain text version

-- Release notes for Agda 2 version 2.4.0.1

Important changes since 2.4.0:


-- Release notes for Agda 2 version 2.4.0

Important changes since 2.3.2:

Installation and Infrastructure

Pragmas and Options

Language

-- State is an instance of Monad
-- Demonstrates the interleaving of projection and application patterns

stateMonad : {S : Set} → Monad (State S)
runState (Monad.return stateMonad a  ) s  = a , s
runState (Monad._>>=_  stateMonad m k) s₀ =
  let a , s₁ = runState m s₀
  in  runState (k a) s₁

module MonadLawsForState {S : Set} where

  open Monad (stateMonad {S})

  leftId : {A B : Set}(a : A)(k : A → State S B) →
    (return a >>= k) ≡ k a
  leftId a k = refl

  rightId : {A B : Set}(m : State S A) →
    (m >>= return) ≡ m
  rightId m = refl

  assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
    ((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
  assoc m k l = refl

Copatterns are yet experimental and the following does not work:

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

Important changes since 2.3.2.1:


-- Release notes for Agda 2 version 2.3.2.1

Important changes since 2.3.2:

Installation

Type checking


-- Release notes for Agda 2 version 2.3.2

Important changes since 2.3.0:

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

Important changes since 2.2.10:

Language

Universe polymorphism

Meta-variables and unification

Instance argument resolution is not recursive. As an example, consider the following "parametrised instance":

eq-List : {A : Set} → Eq A → Eq (List A)
eq-List {A} eq = record { equal = eq-List-A }
  where
  eq-List-A : List A → List A → Bool
  eq-List-A []       []       = true
  eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs
  eq-List-A _        _        = false

Assume that the only Eq instances in scope are eq-List and eq-ℕ. Then the following code does not type-check:

test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])

However, we can make the code work by constructing a suitable instance manually:

test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
  where eq-List-ℕ = eq-List eq-ℕ

By restricting the "instance search" to be non-recursive we avoid introducing a new, compile-time-only evaluation model to Agda.

For more information about instance arguments, see Devriese & Piessens [ICFP 2011]. Some examples are also available in the examples/instance-arguments subdirectory of the Agda distribution.

Irrelevance

Reflection

Compiler backends

MAlonzo

Epic

JavaScript

Tools


-- Release notes for Agda 2 version 2.2.10

Important changes since 2.2.8:

Language

Tools


-- Release notes for Agda 2 version 2.2.8

Important changes since 2.2.6:

Language

Tools


-- Release notes for Agda 2 version 2.2.6

Important changes since 2.2.4:

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

Important changes since 2.2.0:

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