agda/doc/release-notes/2.5.1.1.md

Release notes for Agda version 2.5.1.1

Installation and infrastructure

• Added support for GHC 8.0.1.

• Documentation is now built with Python >=3.3, as done by readthedocs.org.

Bug fixes

• Fixed a serious performance problem with instance search

Issues #1952 and #1998. Also related: #1955 and #2025

• Interactively splitting variable with C-c C-c no longer introduces new trailing patterns. This fixes Issue #1950.

  data Ty : Set where
    _⇒_ : Ty → Ty → Ty

  ⟦_⟧ : Ty → Set
  ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

  data Term : Ty → Set where
    K : (A B : Ty) → Term (A ⇒ (B ⇒ A))

  test : (A : Ty) (a : Term A) → ⟦ A ⟧
  test A a = {!a!}

Before change, case splitting on a would give

  test .(A ⇒ (B ⇒ A)) (K A B) x x₁ = ?

Now, it yields

  test .(A ⇒ (B ⇒ A)) (K A B) = ?

• In literate TeX files, \begin{code} and \end{code} can be preceded (resp. followed) by TeX code on the same line. This fixes Issue #2077.

• Other issues fixed (see bug tracker):

#1951 (mixfix binders not working in 'syntax')

#1967 (too eager insteance search error)

#1974 (lost constraint dependencies)

#1982 (internal error in unifier)

#2034 (function type instance goals)

Compiler backends

• UHC compiler backend

Added support for UHC 1.1.9.4.