Skip to content

CHANGELOG.md

Latest commit

 

History

History
184 lines (135 loc) · 5.09 KB

CHANGELOG.md

File metadata and controls

184 lines (135 loc) · 5.09 KB

Release notes for Agda version 2.8.0

Highlights

Installation

  • Dropped support for GHC 8.6.
  • Agda supports GHC versions 8.8.4 to 9.10.1.

Pragmas and options

  • New warning InvalidDisplayForm instead of hard error when a display form is illegal (and thus ignored).

  • New warning UnusedVariablesInDisplayForm when DISPLAY pragma binds variables that are not used. Example:

    {-# DISPLAY List (Fin n) = ListFin #-}

    Since pattern variable n is not used on the right hand side ListFin, Agda throws a warning and recommeds to rewrite it as:

    {-# DISPLAY List (Fin _) = ListFin #-}

  • New warning WithClauseProjectionFixityMismatch instead of hard error when in a with-clause a projection is used in a different fixity (prefix vs. postfix) than in its parent clause.

  • New error warning TooManyArgumentsToSort instead of hard error.

  • New warning EmptyPolarityPragma for POLARITY pragma without polarities. E.g. triggered by {-# POLARITY F #-}.

  • Warning AbsurdPatternRequiresNoRHS has been renamed to AbsurdPatternRequiresAbsentRHS.

  • New option --js-es6 for generating JavaScript with ES6 module syntax.

  • DISPLAY pragmas can now define display forms that match on defined names beyond constructors (issue #7533). Example:

    {-# DISPLAY Irrelevant Empty = ⊥ #-}

    Empty used to be interpreted as a pattern variable, effectively installing the display form Irrelevant _ = ⊥. Now Empty is treated as a matchable name, as one would intuitively expect from a display form. As a consequence, only Irrelevant Empty is displayed as ⊥, not just any Irrelevant A.

Syntax

Additions to the Agda syntax.

  • Add new literate agda: forester, see #7403

  • Records can now be created using module-like syntax in place of curly braces and semicolons.

    p : Pair Nat Nat
p = record where
  fst = 2
  snd = 3

    In a record where block, definitions have the semantics of let-bindings: they can refer to earlier bindings and may include other definitions than the fields of the record, including opening of modules. For instance,

    p₁ : Pair Nat Nat
p₁ = record where
  open Pair p using (fst)
  n   = fst * 2
  snd = n * n

    The syntax also works for record updates

    p₂ : Pair Nat Nat
p₂ = record p₁ where
  snd = snd p₁ + 1

    See #4275 for the proposal.

  • It is now always possible to refer to the name of a record type's constructor, even if a name was not explicitly specified. This is done using the new (Record name).constructor syntax; See issue #6964 for the motivation.

  • The left-hand-sides of functions bound in a let expression can now contain the same types of patterns that are allowed in lambda expressions, in dependent function types, and in other let bindings.

    This means that

    let
  f : A → B → C
  f p1 p2 = ...
in ...

    should be accepted exactly when, and have the same meaning as,

    let
  f : A → B → C
  f = λ p1 p2 → ...

    See #7572.

Language

Changes to type checker and other components defining the Agda language.

Reflection

Changes to the meta-programming facilities.

  • New reflection primitive: checkFromStringTC : String → Type → TC Term

    Parse and type check the given string against the given type, returning the resulting term (when successful).

Library management

Interaction and emacs mode

  • Agda's error messages now follow the GNU standard. To comply with this policy, line and column are now separated by a dot instead of comma. The format of regular errors and error warnings follows this template:

    sourcefile:line1.column1-line2.column2: error: [ErrorName] ... error message ... when error context

    line2 or even column2 can be missing, in some cases even the entire error location. Internal errors might follow a different format.

    Warnings are printed in a similar format:

    sourcefile:line1.column1-line2.column2: warning: -W[no]WarningName ... warning text ... when warning context

  • Emacs: new face agda2-highlight-cosmetic-problem-face for highlighting the new aspect CosmeticProblem.

  • Emacs: new face agda2-highlight-instance-problem-face for highlighting the new aspect InstanceProblem.

Backends

Other issues closed

For 2.8.0, the following issues were also closed (see bug tracker):

NOTE: This section will be filled by output produced with closed-issues-for-milestone 2.8.0.