Skip to content

Releases: agda/agda

a70b851@master

27 Feb 12:27
@github-actions github-actions
nightly
a70b851
Compare
Choose a tag to compare
a70b851@master Pre-release
Pre-release

What's Changed

Read more

Contributors

nad, markusschlegel, and 25 other contributors
Loading

v2.7.0.1

12 Sep 18:39
@github-actions github-actions
v2.7.0.1
a6fc20c
Compare
Choose a tag to compare
v2.7.0.1 Latest
Latest

Release notes for Agda version 2.7.0.1

This is a minor release of Agda fixing some bugs and regressions.

Installation

  • During installation, Agda type-checks its built-in modules and installs the generated .agdai files.
    (This step is now skipped when the Agda executable is not installed, e.g. cabal install --lib Agda.)
    Should the generation for (some of) these files fail, the names of the missing ones are now printed,
    but installation continues nevertheless (PR #7465).
    Rationale: installation of these files is only crucial when installing Agda in super-user mode.

  • Agda supports GHC versions 8.6.5 to 9.10.1.

Pragmas and options

  • The release notes of 2.7.0 claimed that the option --exact-split was now on by default
    (Issue #7443).
    This is actually not the case, the documentation has been suitably reverted.

  • Default option --save-metas has been reverted to --no-save-metas because of performance regressions
    (Issue #7452).

Bug fixes

  • Fixed an internal error related to interface files
    (Issue #7436).

  • Fixed two internal errors in Mimer:
    (Issue #7402 and
    Issue #7484).

  • Fixed a regression causing needless re-checking of files
    (Issue #7199).

  • Improved printing of terms by fixing a display form bug
    (PR #7480).

List of closed issues

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

  • Issue #7199: Agda re-checks a file with an up-to-date interface file
  • Issue #7402: Mimer internal error in hole with constraint
  • Issue #7436: Code only reachable from display forms not serialised in Agda 2.7.0
  • Issue #7442: Regression: emptiness check fails when erased constructors are involved
  • Issue #7443: --exact-split is not default in 2.7.0, contrary to claims
  • Issue #7452: Performance regression caused by making --save-metas the default
  • Issue #7455: Both stack and cabal fail to install Agda
  • Issue #7484: Internal error using Mimer in where block

These pull requests were merged for 2.7.0.1:

  • PR #7427: #7402: mimer failing on higher order goal
  • PR #7444: Fix #7436: make display forms of imported names DeadCode roots
  • PR #7445: Remove disclaimer that Agda would not follow the Haskell PVP
  • PR #7454: Fixed #7199
  • PR #7456: Actually, --exact-split is not really on by default
  • PR #7457: Revert default to --no-save-metas
  • PR #7465: Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files
  • PR #7471: setup: Don't assume exe is built on --lib
  • PR #7475: Hotfix for #7442
  • PR #7476: Bump std-lib to latest (v2.1.1) and cubical to latest
  • PR #7480: Match display forms in the right context
  • PR #7487: Mimer shouldn't try to use existing pattern lambdas in solutions

What's Changed (auto-generated)

Full Changelog: v2.7.0...v2.7.0.1

Contributors

andreasabel
Assets 5
Loading

v2.7.0

16 Aug 12:31
@andreasabel andreasabel
v2.7.0
df1a26d
Compare
Choose a tag to compare
v2.7.0

Release notes for Agda version 2.7.0

Highlights

  • Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.

  • New syntax using x ← e to bind values on the left-hand-side of a function clause.

  • Instance search is more performant thanks to a new indexing structure.
    Additionally, users can now control how instances should be selected
    in the case multiple candidates exist.

  • User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
    are now on by default.

Installation

  • Agda versioning scheme switches to the Haskell Package Versioning Policy
    so Agda can be more reliably used as a library.
    Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...

  • When the creation of the Agda library interface files fails during installation,
    a warning is emitted rather than aborting installation.
    The absence of these interface files is not a problem if the Agda installation
    resides in user space; they will be created on the fly then.
    Yet for system-wide installations in root space or packaging,
    the interface files should be created.
    This can be achieved by a manual invocation of Agda on the library source files
    (i.e., primitive and builtin modules Agda.*).
    (See Issue #7401 and PR #7404.)

  • Agda supports GHC versions 8.6.5 to 9.10.1.

Pragmas and options

  • [Breaking] The option --overlapping-instances, which allows
    backtracking during instance search, has been renamed to
    --backtracking-instance-search.

  • These options are now on by default:

    • --exact-split: Warn about clauses that are not definitional equalities.
    • --keep-pattern-variables: Do not introduce dot patterns in interactive splitting.
    • --postfix-projections: Print projections and projection patterns in postfix.
    • --save-metas: Try to not unfold metavariable solutions in interface files.

    To revert to the old behavior, use options --no-....

  • Option --rewriting is now considered infective.
    This means that if a module has this flag enabled,
    then all modules importing it must also have that flag enabled.

  • New warnings:

    • CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
      Used to be a hard error; now Agda continues, ignoring eta-equality.

    • ConflictingPragmaOptions if giving both --this and --that
      when --this implies --no-that (and analogous for --no-this implies
      --that, etc).

    • ConstructorDoesNotFitInData when a constructor parameter
      is too big (in the sense of universe level) for the target data type of the constructor.
      Error warning, used to be a hard error.

    • DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
      or declared inductive twice.

    • UselessMacro when a macro block does not contain any function definitions.

    • WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
      Used to be a hard error.

  • Rejected rewrite rules no longer cause a hard error but instead cause
    an error warning. The following warnings were added to document the
    various reasons for rejection:

    • RewriteLHSNotDefinitionOrConstructor
    • RewriteVariablesNotBoundByLHS
    • RewriteVariablesBoundMoreThanOnce
    • RewriteLHSReduces
    • RewriteHeadSymbolIsProjection
    • RewriteHeadSymbolIsProjectionLikeFunction
    • RewriteHeadSymbolIsTypeConstructor
    • RewriteHeadSymbolContainsMetas
    • RewriteConstructorParametersNotGeneral
    • RewriteContainsUnsolvedMetaVariables
    • RewriteBlockedOnProblems
    • RewriteRequiresDefinitions
    • RewriteDoesNotTargetRewriteRelation
    • RewriteBeforeFunctionDefinition
    • RewriteBeforeMutualFunctionDefinition

Lossy unification

  • New option --require-unique-meta-solutions
    (turned on by default).
    Disabling it with --no-require-unique-meta-solutions allows the type checker
    to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
    The --lossy-unification flag implies --no-require-unique-meta-solutions.

  • New pragma INJECTIVE_FOR_INFERENCE
    which treats functions as injective for inferring implicit arguments if
    --no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
    file where the function is used, and not necessarily in the file where it is defined.
    For example:

    postulate
  reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'

[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})

    does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
    If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.

Syntax

Additions to the Agda syntax.

  • Left-hand side let:
    using x ← e
    (PR #7078)

    This new construct can be use in left-hand sides together with with and
    rewrite to give names to subexpressions. It is the left-hand side
    counterpart of a let-binding and supports the same limited form of pattern
    matching on eta-expandable record values.

    It can be quite useful when you have a function doing a series of nested
    withs that share some expressions. Something like

    fun : A → B
fun x using z ← e with foo z
... | p with bar z
...   | q = r

    Here the expression e doesn't have to be repeated in the two with-expressions.

    As in a with, multiple bindings can be separated by a |, and variables to
    the left are in scope in bindings to the right.

  • Pattern synonyms can now expose existing instance arguments
    (PR 7173).
    Example:

    data D : Set where
  c : {{D}} → D

pattern p {{d}} = c {{d}}

    This allows us to explicitly bind these argument in a pattern match
    and supply them explicitly when using the pattern synonym in an expression.

    f : D → D
f (p {{d = x}}) = p {{d = x}}

    We cannot create new instance arguments this way, though.
    The following is rejected:

    data D : Set where
  c : D → D

pattern p {{d}} = c d

Language

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

  • Agda now uses discrimination trees to store and look up instance
    definitions, rather than linearly searching through all instances for
    a given "class" (PR #7109).

    This is a purely internal change, and should not result in any change
    to which programs are accepted or rejected. However, it significantly
    improves the performance of instance search, especially for the case
    of a "type class" indexed by a single type argument. The new lookup
    procedure should never be slower than the previous implementation.

Reflection

Changes to the meta-programming facilities.

  • [Breaking] Erased constructors are now supported in reflection machinery.
    Quantity argument was added to data-cons. For erased constructors this
    argument has a value of quantity-0, otherwise it's quantity-ω.
    defineData now requires setting quantity for each constructor.

  • Add new primitive to run instance search from reflection code:

      -- Try to solve open instance constraints. When wrapped in `noConstraints`,
  -- fails if there are unsolved instance constraints left over that originate
  -- from the current macro invokation. Outside constraints are still attempted,
  -- but failure to solve them are ignored by `noConstraints`.
  solveInstanceConstraints : TC ⊤

  • A new reflection primitive workOnTypes : TC A → TC A was added to
    Agda.Builtin.Reflection. This runs the given computation at the type level,
    which enables the use of erased things. In particular, this is needed when
    working with (dependent) function types with erased arguments. For example,
    one can get the type of the tuple constructor _,_ (which now takes its type
    parameters as erased arguments, see above) and unify it with the current goal
    as follows:

    macro
  testM : Term → TC ⊤
  testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))

typeOfComma = testM

Interaction and emacs mode

  • [Breaking] The Auto command
    Agsy has been replaced by an entirely new implementation Mimer
    (PR #6410).
    This fixes problems where Auto would fail in the presence of language features
    it did not know about, such as copatterns or anything cubical.

    The reimplementation does not support case splitting (-c), disproving
    (-d) or refining (-r).

  • The Agda input method for Emacs has been extended by several character bindings.
    The list of changes can be obtained with a git diff on the sources:

    git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el

API

Highlighting some changes to Agda as a library.

  • New module Agda.Syntax.Common.KeywordRange providing type `KwRange...
Read more

Contributors

WhatisRT, Mic92, and 28 other contributors
Loading

Agda 2.7.0 release candidate 2

01 Aug 07:16
@andreasabel andreasabel
v2.7.0-rc2
06aa522
Compare
Choose a tag to compare
Agda 2.7.0 release candidate 2 Pre-release
Pre-release

Changes over release candidate 1

  • Reverted PR #5627 which had made options like --type-in-type infective.

  • Fixed issues #7382 (internal error in deserialization) and #7401 (cabal install --lib).

Release notes for Agda version 2.7.0

Highlights

  • Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.

  • New syntax using x ← e to bind values on the left-hand-side of a function clause.

  • Instance search is more performant thanks to a new indexing structure.
    Additionally, users can now control how instances should be selected
    in the case multiple candidates exist.

  • User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
    are now on by default.

Installation

  • Agda versioning scheme switches to the Haskell Package Versioning Policy
    so Agda can be more reliably used as a library.
    Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...

  • When the creation of the Agda library interface files fails during installation,
    a warning is emitted rather than aborting installation.
    The absence of these interface files is not a problem if the Agda installation
    resides in user space; they will be created on the fly then.
    Yet for system-wide installations in root space or packaging,
    the interface files should be created.
    This can be achieved by a manual invocation of Agda on the library source files
    (i.e., primitive and builtin modules Agda.*).
    (See Issue #7401 and PR #7404.)

  • Agda supports GHC versions 8.6.5 to 9.10.1.

Pragmas and options

  • [Breaking] The option --overlapping-instances, which allows
    backtracking during instance search, has been renamed to
    --backtracking-instance-search.

  • These options are now on by default:

    • --exact-split: Warn about clauses that are not definitional equalities.
    • --keep-pattern-variables: Do not introduce dot patterns in interactive splitting.
    • --postfix-projections: Print projections and projection patterns in postfix.
    • --save-metas: Try to not unfold metavariable solutions in interface files.

    To revert to the old behavior, use options --no-....

  • Option --rewriting is now considered infective.
    This means that if a module has this flag enabled,
    then all modules importing it must also have that flag enabled.

  • New warnings:

    • CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
      Used to be a hard error; now Agda continues, ignoring eta-equality.

    • ConflictingPragmaOptions if giving both --this and --that
      when --this implies --no-that (and analogous for --no-this implies
      --that, etc).

    • ConstructorDoesNotFitInData when a constructor parameter
      is too big (in the sense of universe level) for the target data type of the constructor.
      Error warning, used to be a hard error.

    • DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
      or declared inductive twice.

    • UselessMacro when a macro block does not contain any function definitions.

    • WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
      Used to be a hard error.

  • Rejected rewrite rules no longer cause a hard error but instead cause
    an error warning. The following warnings were added to document the
    various reasons for rejection:

    • RewriteLHSNotDefinitionOrConstructor
    • RewriteVariablesNotBoundByLHS
    • RewriteVariablesBoundMoreThanOnce
    • RewriteLHSReduces
    • RewriteHeadSymbolIsProjection
    • RewriteHeadSymbolIsProjectionLikeFunction
    • RewriteHeadSymbolIsTypeConstructor
    • RewriteHeadSymbolContainsMetas
    • RewriteConstructorParametersNotGeneral
    • RewriteContainsUnsolvedMetaVariables
    • RewriteBlockedOnProblems
    • RewriteRequiresDefinitions
    • RewriteDoesNotTargetRewriteRelation
    • RewriteBeforeFunctionDefinition
    • RewriteBeforeMutualFunctionDefinition

Lossy unification

  • New option --require-unique-meta-solutions
    (turned on by default).
    Disabling it with --no-require-unique-meta-solutions allows the type checker
    to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
    The --lossy-unification flag implies --no-require-unique-meta-solutions.

  • New pragma INJECTIVE_FOR_INFERENCE
    which treats functions as injective for inferring implicit arguments if
    --no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
    file where the function is used, and not necessarily in the file where it is defined.
    For example:

    postulate
  reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'

[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})

    does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
    If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.

Syntax

Additions to the Agda syntax.

  • Left-hand side let:
    using x ← e
    (PR #7078)

    This new construct can be use in left-hand sides together with with and
    rewrite to give names to subexpressions. It is the left-hand side
    counterpart of a let-binding and supports the same limited form of pattern
    matching on eta-expandable record values.

    It can be quite useful when you have a function doing a series of nested
    withs that share some expressions. Something like

    fun : A → B
fun x using z ← e with foo z
... | p with bar z
...   | q = r

    Here the expression e doesn't have to be repeated in the two with-expressions.

    As in a with, multiple bindings can be separated by a |, and variables to
    the left are in scope in bindings to the right.

  • Pattern synonyms can now expose existing instance arguments
    (PR 7173).
    Example:

    data D : Set where
  c : {{D}} → D

pattern p {{d}} = c {{d}}

    This allows us to explicitly bind these argument in a pattern match
    and supply them explicitly when using the pattern synonym in an expression.

    f : D → D
f (p {{d = x}}) = p {{d = x}}

    We cannot create new instance arguments this way, though.
    The following is rejected:

    data D : Set where
  c : D → D

pattern p {{d}} = c d

Language

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

  • Agda now uses discrimination trees to store and look up instance
    definitions, rather than linearly searching through all instances for
    a given "class" (PR #7109).

    This is a purely internal change, and should not result in any change
    to which programs are accepted or rejected. However, it significantly
    improves the performance of instance search, especially for the case
    of a "type class" indexed by a single type argument. The new lookup
    procedure should never be slower than the previous implementation.

Reflection

Changes to the meta-programming facilities.

  • [Breaking] Erased constructors are now supported in reflection machinery.
    Quantity argument was added to data-cons. For erased constructors this
    argument has a value of quantity-0, otherwise it's quantity-ω.
    defineData now requires setting quantity for each constructor.

  • Add new primitive to run instance search from reflection code:

      -- Try to solve open instance constraints. When wrapped in `noConstraints`,
  -- fails if there are unsolved instance constraints left over that originate
  -- from the current macro invokation. Outside constraints are still attempted,
  -- but failure to solve them are ignored by `noConstraints`.
  solveInstanceConstraints : TC ⊤

  • A new reflection primitive workOnTypes : TC A → TC A was added to
    Agda.Builtin.Reflection. This runs the given computation at the type level,
    which enables the use of erased things. In particular, this is needed when
    working with (dependent) function types with erased arguments. For example,
    one can get the type of the tuple constructor _,_ (which now takes its type
    parameters as erased arguments, see above) and unify it with the current goal
    as follows:

    macro
  testM : Term → TC ⊤
  testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))

typeOfComma = testM

Interaction and emacs mode

  • [Breaking] The Auto command
    Agsy has been replaced by an entirely new implementation Mimer
    (PR #6410).
    This fixes problems where Auto would fail in the presence of language features
    it did not know about, such as copatterns or anything cubical.

    The reimplementation does not support case splitting (-c), disproving
    (-d) or refining (-r).

  • The Agda input method for Emacs has been extended by several character bindings.
    The lis...

Read more

Contributors

WhatisRT, Mic92, and 28 other contributors
Loading

Agda 2.7.0 release candidate 1

14 Jul 16:45
@andreasabel andreasabel
v2.6.20240714
18cc539
Compare
Choose a tag to compare
Agda 2.7.0 release candidate 1 Pre-release
Pre-release

Release notes for Agda version 2.7.0

Highlights

  • Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.

  • New syntax using x ← e to bind values on the left-hand-side of a function clause.

  • Instance search is more performant thanks to a new indexing structure.
    Additionally, users can now control how instances should be selected
    in the case multiple candidates exist.

  • User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
    are now on by default.

Installation

  • Agda versioning scheme switches to the Haskell Package Versioning Policy
    so Agda can be more reliably used as a library.
    Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...

  • Agda supports GHC versions 8.6.5 to 9.10.1.

Pragmas and options

  • [Breaking] The option --overlapping-instances, which allows
    backtracking during instance search, has been renamed to
    --backtracking-instance-search.

  • These options are now on by default:

    • --exact-split: Warn about clauses that are not definitional equalities.
    • --keep-pattern-variables: Do not introduce dot patterns in interactive splitting.
    • --postfix-projections: Print projections and projection patterns in postfix.
    • --save-metas: Try to not unfold metavariable solutions in interface files.

    To revert to the old behavior, use options --no-....

  • The following options are now considered infective:
    (Issue #5264)

    • --allow-exec
    • --cumulativity
    • --experimental-irrelevance
    • --injective-type-constructors
    • --omega-in-omega
    • --rewriting
    • --type-in-type

    This means that if a module has one of these flags enabled,
    then all modules importing it must also have that flag enabled.

  • New warnings:

    • CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
      Used to be a hard error; now Agda continues, ignoring eta-equality.

    • ConflictingPragmaOptions if giving both --this and --that
      when --this implies --no-that (and analogous for --no-this implies
      --that, etc).

    • ConstructorDoesNotFitInData when a constructor parameter
      is too big (in the sense of universe level) for the target data type of the constructor.
      Error warning, used to be a hard error.

    • DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
      or declared inductive twice.

    • UselessMacro when a macro block does not contain any function definitions.

    • WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
      Used to be a hard error.

  • Rejected rewrite rules no longer cause a hard error but instead cause
    an error warning. The following warnings were added to document the
    various reasons for rejection:

    • RewriteLHSNotDefinitionOrConstructor
    • RewriteVariablesNotBoundByLHS
    • RewriteVariablesBoundMoreThanOnce
    • RewriteLHSReduces
    • RewriteHeadSymbolIsProjection
    • RewriteHeadSymbolIsProjectionLikeFunction
    • RewriteHeadSymbolIsTypeConstructor
    • RewriteHeadSymbolContainsMetas
    • RewriteConstructorParametersNotGeneral
    • RewriteContainsUnsolvedMetaVariables
    • RewriteBlockedOnProblems
    • RewriteRequiresDefinitions
    • RewriteDoesNotTargetRewriteRelation
    • RewriteBeforeFunctionDefinition
    • RewriteBeforeMutualFunctionDefinition

Lossy unification

  • New option --require-unique-meta-solutions
    (turned on by default).
    Disabling it with --no-require-unique-meta-solutions allows the type checker
    to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
    The --lossy-unification flag implies --no-require-unique-meta-solutions.

  • New pragma INJECTIVE_FOR_INFERENCE
    which treats functions as injective for inferring implicit arguments if
    --no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
    file where the function is used, and not necessarily in the file where it is defined.
    For example:

    postulate
  reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'

[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})

    does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
    If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.

Syntax

Additions to the Agda syntax.

  • Left-hand side let:
    using x ← e
    (PR #7078)

    This new construct can be use in left-hand sides together with with and
    rewrite to give names to subexpressions. It is the left-hand side
    counterpart of a let-binding and supports the same limited form of pattern
    matching on eta-expandable record values.

    It can be quite useful when you have a function doing a series of nested
    withs that share some expressions. Something like

    fun : A → B
fun x using z ← e with foo z
... | p with bar z
...   | q = r

    Here the expression e doesn't have to be repeated in the two with-expressions.

    As in a with, multiple bindings can be separated by a |, and variables to
    the left are in scope in bindings to the right.

  • Pattern synonyms can now expose existing instance arguments
    (PR 7173).
    Example:

    data D : Set where
  c : {{D}} → D

pattern p {{d}} = c {{d}}

    This allows us to explicitly bind these argument in a pattern match
    and supply them explicitly when using the pattern synonym in an expression.

    f : D → D
f (p {{d = x}}) = p {{d = x}}

    We cannot create new instance arguments this way, though.
    The following is rejected:

    data D : Set where
  c : D → D

pattern p {{d}} = c d

Language

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

  • Agda now uses discrimination trees to store and look up instance
    definitions, rather than linearly searching through all instances for
    a given "class" (PR #7109).

    This is a purely internal change, and should not result in any change
    to which programs are accepted or rejected. However, it significantly
    improves the performance of instance search, especially for the case
    of a "type class" indexed by a single type argument. The new lookup
    procedure should never be slower than the previous implementation.

Reflection

Changes to the meta-programming facilities.

  • [Breaking] Erased constructors are now supported in reflection machinery.
    Quantity argument was added to data-cons. For erased constructors this
    argument has a value of quantity-0, otherwise it's quantity-ω.
    defineData now requires setting quantity for each constructor.

  • Add new primitive to run instance search from reflection code:

      -- Try to solve open instance constraints. When wrapped in `noConstraints`,
  -- fails if there are unsolved instance constraints left over that originate
  -- from the current macro invokation. Outside constraints are still attempted,
  -- but failure to solve them are ignored by `noConstraints`.
  solveInstanceConstraints : TC ⊤

  • A new reflection primitive workOnTypes : TC A → TC A was added to
    Agda.Builtin.Reflection. This runs the given computation at the type level,
    which enables the use of erased things. In particular, this is needed when
    working with (dependent) function types with erased arguments. For example,
    one can get the type of the tuple constructor _,_ (which now takes its type
    parameters as erased arguments, see above) and unify it with the current goal
    as follows:

    macro
  testM : Term → TC ⊤
  testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))

typeOfComma = testM

Interaction and emacs mode

  • [Breaking] The Auto command
    Agsy has been replaced by an entirely new implementation Mimer
    (PR #6410).
    This fixes problems where Auto would fail in the presence of language features
    it did not know about, such as copatterns or anything cubical.

    The reimplementation does not support case splitting (-c), disproving
    (-d) or refining (-r).

  • The Agda input method for Emacs has been extended by several character bindings.
    The list of changes can be obtained with a git diff on the sources:

    git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el

API

Highlighting some changes to Agda as a library.

  • New module Agda.Syntax.Common.KeywordRange providing type KwRange isomorphic to Range
    to indicate source positions that just span keywords (PR #7162).
    The motivation for KwRange is to distinguish such ranges from ranges for whole subtrees,
    e.g. in data type Agda.Syntax.Concrete.Declaration.

    API:

    module Agda.Syntax.Common.KeywordRange where

type KwRa...
Read more

Contributors

WhatisRT, Mic92, and 28 other contributors
Loading

v2.6.4.3

06 Mar 10:34
@andreasabel andreasabel
v2.6.4.3
714c7d2
Compare
Choose a tag to compare
v2.6.4.3

Release notes for Agda version 2.6.4.3

This release fixes a regression in 2.6.4.3 and one in 2.6.4.
It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.

Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.

Closed issues

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

  • Issue #7148: Regression in 2.6.4.2 concerning with
  • Issue #7150: Regression in 2.6.4 in rewrite with instances

Full Changelog: v2.6.4.2...v2.6.4.3

Loading

v2.6.4.2

24 Feb 09:54
@andreasabel andreasabel
v2.6.4.2
3a34310
Compare
Choose a tag to compare
v2.6.4.2 Pre-release
Pre-release

Release notes for Agda version 2.6.4.2

This is a bug-fix release. It aims to be API-compatible with 2.6.4.1.
Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1.

Highlights

List of closed issues

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

  • Issue #6972: Unfolding fails when code is split up into multiple files
  • Issue #6999: Unification failure for function type with erased argument
  • Issue #7020: question: haskell backend extraction of Data.Nat.DivMod.DivMod?
  • Issue #7029: Internal error on confluence check when rewriting a defined symbol with a hole
  • Issue #7033: transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥
  • Issue #7034: Internal error with --two-level due to blocking on solved meta
  • Issue #7044: Serializer crashes on blocked definitions when using --allow-unsolved-metas
  • Issue #7048: hcomp symbols in interface not hidden under --cubical-compatible
  • Issue #7059: Don't recompile if --keep-pattern-variables option changes
  • Issue #7070: Don't set a default maximum heapsize for Agda runs
  • Issue #7081: Missing IsString instance with debug flags enabled
  • Issue #7095: Agda build flags appear as "automatic", but they are all "manual"
  • Issue #7104: Warning "there are two interface files" should not be serialized
  • Issue #7105: Internal error in generate-helper (C-c C-h)
  • Issue #7113: Instance resolution runs too late, leads to with-abstraction failure

These PRs not corresponding to issues were merged:

  • PR #6988: Provide a .agda-lib for Agda builtins
  • PR #7065: Some documentation fixes
  • PR #7072: Add 'Inference in Agda' to the list of tutorials
  • PR #7091: Add course to “Courses using Agda”

What's Changed (merged PRs, auto-generated)

Full Changelog: v2.6.4.1...v2.6.4.2

Contributors

WhatisRT, nad, and 3 other contributors
Loading

v2.6.4.1

30 Nov 18:14
@andreasabel andreasabel
v2.6.4.1
4293e0a
Compare
Choose a tag to compare
v2.6.4.1

Release notes for Agda version 2.6.4.1

This is a minor release of Agda 2.6.4 featuring a few changes:

  • Make recursion on proofs legal again.
  • Improve performance, e.g. by removing debug printing unless built with cabal flag debug.
  • Switch to XDG directory convention.
  • Reflection: change to order of results returned by getInstances.
  • Fix some internal errors.

Installation

  • Agda supports GHC versions 8.6.5 to 9.8.1.

  • Verbose output printing via -v or --verbose is now only active if Agda is built with the debug cabal flag.
    Without debug, no code is generated for verbose printing, which makes building Agda faster and Agda itself faster as well. (PR #6863)

Language

  • A change in 2.6.4 that prevented all recursion on proofs, i.e., members of a type A : Prop ℓ, has been reverted.
    It is possible again to use proofs as termination arguments. (See issue #6930.)

Reflection

Changes to the meta-programming facilities.

  • The reflection primitive getInstances will now return instance candidates ordered by specificity, rather than in unspecified order:
    If a candidate c1 : T has a type which is a substitution instance of that of another candidate c2 : S, c1 will appear earlier in the list.

    As a concrete example, if you have instances F (Nat → Nat), F (Nat → a), and F (a → b), they will be returned in this order.
    See issue #6944 for further motivation.

Library management

  • Agda now follows the XDG base directory standard on Unix-like systems, see PR #6858.
    This means, it will look for configuration files in ~/.config/agda rather than ~/.agda.

    For backward compatibility, if you still have an ~/.agda directory, it will look there first.

    No change on Windows, it will continue to use %APPDATA% (e.g. C:/Users/USERNAME/AppData/Roaming/agda).

Other issues closed

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

  • #6745: Strange interaction between opaque and let open
  • #6746: Support GHC 9.8
  • #6852: Follow XDG Base Directory Specification
  • #6913: Internal error on primLockUniv-sorted functions
  • #6930: Termination checking with --prop: change in 2.6.4 compared with 2.6.3
  • #6931: Internal error with an empty parametrized module from a different file
  • #6941: Interaction between opaque and instance arguments
  • #6944: Order instances by specificity for reflection
  • #6953: Emacs 30 breaks agda mode
  • #6957: Agda stdlib installation instructions broken link
  • #6959: Warn about opaque unquoteDecl/unquoteDef
  • #6983: Refine command does not work on Emacs 30

What's Changed (auto-generated)

New Contributors

Full Changelog: v2.6.4...v2.6.4.1

Contributors

juhp, UlfNorell, and 15 other contributors
Loading

v2.6.4

06 Oct 12:23
@andreasabel andreasabel
v2.6.4
f42acb6
Compare
Choose a tag to compare
v2.6.4

Release notes for Agda version 2.6.4

Highlights

  • Cubical Agda now displays boundary conditions in interactive mode
    (PR #6529).

  • An inconsistency in the treatment of large indices has been fixed
    (Issue #6654).

  • Unfolding of definitions can now be fine-controlled via opaque definitions.

  • Additions to the sort system: LevelUniv and Propω.

  • New flag --erasure with several improvements to erasure (declared run-time irrelevance).

  • New reflection primitives for meta-programming.

Installation

  • Removed the cabal flag cpphs that enabled building Agda with cpphs instead of the default C preprocessor.

  • Agda supports GHC versions 8.6.5 to 9.6.3.

Pragmas and options

  • New command-line option --numeric-version to just print the version number of Agda.

  • Option --version now also prints the cabal flags active in this build of Agda
    (e.g. whether Agda was built with -f enable-cluster-counting).

  • New command-line option --trace-imports to switch on notification messages
    on the end of compilation of an imported module
    or on access to an interface file during the type-checking.

    See --trace-imports
    in the documentation for more.

  • New option --no-infer-absurd-clauses to simplify coverage checking and case splitting:
    Agda will then no longer attempt to automatically eliminate absurd clauses which can be a costly operation.
    This means that these absurd clauses have to be written out in the Agda text.
    Try this option if you experience type checking performance degradation with omitted absurd clauses.

    Opposite: --infer-absurd-clauses.

  • Benign warnings are now printed together with their warning name, to give a hint how they can be disabled
    (see #6229).

  • New option --level-universe to make Level inhabit its own universe LevelUniv:
    When this option is turned on, Level can now only depend on terms of type Level.

    Note: While compatible with the --cubical option, this option is currently not compatible with cubical builtin files, and an error will be raised when trying to import them in a file using --level-universe.

    Opposite: --no-level-universe.

  • Most boolean options now have their opposite, e.g., --allow-unsolved-metas is complemented by --no-allow-unsolved-metas.
    With the opposite one can override a previously given option.
    Options given on the command line are overwritten by options given in the .agda-lib file,
    which in turn get overwritten by options given in the individual .agda file.

    New options (all on by default):

    • --no-allow-exec
    • --no-allow-incomplete-matches
    • --no-allow-unsolved-metas
    • --no-call-by-name
    • --no-cohesion
    • --no-count-clusters
    • --no-erased-matches
    • --no-erasure
    • --no-experimental-irrelevance
    • --no-flat-split
    • --no-guarded
    • --no-injective-type-constructors
    • --no-keep-covering-clauses
    • --no-lossy-unification
    • --no-keep-pattern-variables
    • --no-omega-in-omega
    • --no-postfix-projections
    • --no-rewriting
    • --no-show-identity-substitutions
    • --no-show-implicit
    • --no-show-irrelevant
    • --no-two-level
    • --no-type-in-type
    • --eta-equality
    • --fast-reduce
    • --forcing
    • --import-sorts
    • --load-primitives
    • --main
    • --pattern-matching
    • --positivity-check
    • --print-pattern-synonyms
    • --projection-like
    • --termination-check
    • --unicode

  • Option --flat-split again implies --cohesion.
    Reverts change introduced in Agda 2.6.3 where --cohesion was a prerequisite for --flat-split.

  • Pragma INLINE may now be applied to constructors of types supporting co-pattern matching.
    It enables translation of right-hand-side constructor applications to left-hand-side co-pattern splits (see PR #6682).
    For example, this translation allows the nats function to pass termination checking:

      record Stream (A : Set) : Set where
    coinductive; constructor _∷_
    field head : A
          tail : Stream A
  open Stream
  {-# INLINE _∷_ #-}

  nats : Nat → Stream Nat
  nats n = n ∷ nats (1 + n)

    Inlining transforms the definition of nats to the following definition by copattern matching:

      nats n .head = n
  nats n .tail = nats (1 + n)

    This form is accepted by the termination checker;
    unlike the form before inlining, it does not admit any infinite reduction sequences.

    If option --exact-split is on, the inlining will trigger a InlineNoExactSplit warning for nats.
    This warning can be disabled as usual, with -WnoInlineNoExactSplit.

  • New option --large-indices, controlling whether constructors of
    indexed data types are allowed to refer to data that would be "too
    large" to fit in their declared sort. Large indices are disallowed by
    default; see the language changes for details.

  • New option --forced-argument-recursion, on by default, controlling
    whether forced constructor arguments are usable for termination
    checking. This flag may be necessary for Agda to accept nontrivial
    uses of induction-induction.

  • The suffix Warning has been dropped from the warning names
    DuplicateFieldsWarning and TooManyFieldsWarning.

  • The warning GenericUseless has been split into the three warnings
    UselessPragma, FaceConstraintCannotBeHidden and FaceConstraintCannotBeNamed.

  • New warning PatternShadowsConstructor which used to be an error.

Library management

  • [Breaking] One can no longer have .agda-lib files that are
    located below the "project root", on the path to the file that is
    being type-checked (see
    #6465).

    For instance, if you have a module called A.B.C in the directory
    Root/A/B, then an error is raised if there are .agda-lib files
    in Root/A or Root/A/B.

    Previously such .agda-lib files were ignored.

Interaction and emacs mode

  • Agda now supports reading files with extension .lagda.typ, and use the parser for
    markdown files to parse them.
    To edit such files in Emacs with Agda support, one needs to add the line

    (add-to-list 'auto-mode-alist '("\\.lagda.typ\\'" . agda2-mode))

    to .emacs.

    Generation for highlighted code like HTML is unsupported for Typst.
    One may generate HTML with typst input, but that makes little sense,
    and markdown is recommended instead when HTML export is desired.

  • Helper function (C-c C-h) does not abstract over module parameters anymore
    (see #2271)
    and neither over generalized variables
    (see #6689).

  • New Agda input mode prefix box for APL boxed operators, e.g. \box= for ⌸;
    see PR #6510 for full list of bindings.

  • Cubical Agda will now report boundary information for interaction
    points which are not at the top-level of their respective clauses.
    This includes bodies of Path-typed values, the faces of a partial
    element, arguments to functions returning paths, etc.

    Since this information is available in a structured way during
    interaction    , the "goal type, context, and inferred type" command will
    also display the value of the expression at each relevant face.

    See also PR #6529 for a
    deeper explanation and a demo video.

Syntax

  • Agda now skips the UTF8 byte order mark (BOM) at beginning of files
    (see #6524).
    Previously, the BOM caused a parse error.

  • If the new option --hidden-argument-puns is used, then the pattern
    {x} is interpreted as {x = x}, and the pattern ⦃ x ⦄ is
    interpreted as ⦃ x = x ⦄ (see
    #6325). Here x must be
    an unqualified name that does not refer to a constructor that is in
    scope: if x is qualified, then the pattern is not interpreted as a
    pun, and if x is unqualified and refers to a constructor that is
    in scope, then the code is rejected.

    This feature can be turned off using --no-hidden-argument-puns.

    Note that {(x)} and ⦃ (x) ⦄ are not interpreted as puns.

    Note also that {x} is not interpreted as a pun in λ {x} → … or
    syntax f {x} = …. However, {x} is interpreted as a pun in
    λ (c {x}) → ….

  • postulate blocks may now contain private declarations
    (see #1702).

Language

  • [Breaking] Constructor arguments are no longer allowed to store
    values of a type larger than their own sort, even when these values
    are forced by the indices of a constructor.

    This fixes a particular instance of the incompatibility between
    structural recursion and impredicativity, which could previously be
    exploited through the use of large data-type indices.
    (see #6654).

    This behaviour can be controlled with the flag --large-indices. Note
    that, when --large-indices is enabled, forced constructor arguments
    should not be used for termination checking. The flag
    --[no-]forced-argument-recursion makes the termination checker skip
    these arguments entirely. When --safe is given, --large-indices is
    incompatible...

Read more

Contributors

juhp, julianmendez, and 42 other contributors
Loading

v2.6.3

06 Oct 12:31
@andreasabel andreasabel
v2.6.3
b499d12
Compare
Choose a tag to compare
v2.6.3

Release notes for Agda version 2.6.3

Highlights

  • Added support for Erased Cubical Agda, a variant of Cubical Agda that is supported by the GHC backend, under the flag --erased-cubical.

  • Added a new flag --cubical-compatible to turn on generation of Cubical Agda-specific support code (previously this behaviour was part of --without-K).

    Since --cubical-compatible mode implies that functions should work with the preliminary support for indexed inductive types in Cubical Agda, many pattern matching functions will now emit an UnsupportedIndexedMatch warning, indicating that the function will not compute when applied to transports (from --cubical code).

    This warning can be disabled with -WnoUnsupportedIndexedMatch, which can be used either in an OPTIONS pragma or in your agda-lib file.
    The latter is recommended if your project is only --cubical-compatible, or if it is already making extensive use of indexed types.

    Note that code that uses (only) --without-K can no longer be imported from code that uses --cubical. Thus it may make sense to
    replace --without-K with --cubical-compatible in library code, if possible.

    Note also that Agda tends to be quite a bit faster if --without-K is used instead of --cubical-compatible.

  • Agda 2.6.3 seems to type-check one variant of the standard library about 30% faster than Agda 2.6.2.2 (on one system; the library was changed in a small way between the tests to accommodate changes to Agda). In that test the standard library did not use the new flag --cubical-compatible. With that flag enabled in all the files that used to use --without-K (and the warning UnsupportedIndexedMatch turned off) Agda 2.6.3 was still about 10% faster.

  • New primitives declareData, defineData, and unquoteDecl data for generating new data types have been added to the reflection API.

Installation and infrastructure

Agda supports GHC versions 8.0.2 to 9.4.4.

Erasure

  • The new option --erased-cubical turns on a variant of Cubical Agda (see #4701).

    When this variant of Cubical Agda is used glue (and some related builtins) may only be used in erased settings. One can import
    regular Cubical Agda code from this variant of Cubical Agda, but names defined using Cubical Agda are (mostly) treated as if they had
    been marked as erased. See the reference manual for more details.

    The GHC backend can compile code that uses --erased-cubical if the top-level module uses this flag.

    This feature is experimental.

  • Added an option --erase-record-parameters that marks parameters to record fields and definitions in a record module as erased (see #4786 and #5770). For example:

    {-# OPTIONS --erase-record-parameters #-}

record R (A : Set) : Set where
  field
    f : A

test : {@0 A : Set} → R A → A
test = R.f

Cubical Agda

  • [Breaking] The generation of Cubical Agda-specific support code was removed from --without-K and transferred to its own flag, --cubical-compatible (see #5843 and #6049 for the rationale).

  • Cubical Agda now has experimental support for indexed inductive types (#3733).
    See the user guide for caveats.

  • The cubical interval I now belongs to its own sort, IUniv, rather than SSet.

  • For J : IUniv and A : J → Set l, we have (j : J) → A j : Set l, that is, the type of functions from a type in IUniv to a fibrant type is fibrant.

  • The option --experimental-irrelevance is now perhaps incompatible with Cubical Agda and perhaps also postulated univalence (see #5611 and #5861).

    This is not meant to imply that the option was not already incompatible with those things.
    Note that --experimental-irrelevance cannot be used together with --safe.

  • A new built-in constructor REFLID was added to the cubical identity types.
    This is definitionally equal to the reflexivity identification built with conid, with the difference being that matching on REFLID is allowed.

    symId : ∀ {a} {A : Set a} {x y : A} → Id x y → Id y x
symId reflId = reflId

  • Definitions which pattern match on higher-inductive types are no longer considered for injectivity analysis.
    (#6219)

  • [Breaking] Higher constructors are no longer considered as guarding in the productivity check.
    (#6108)

  • Rewrite rules with interval arguments are now supported.
    (#4384)

The flat modality

  • [Breaking] The @flat/@♭ modality is now by default disabled (see
    #4927).

    It can be enabled using the infective flag --cohesion.

  • [Breaking] Matching on @flat arguments is now disabled by default, the flag
    --no-flat-split has been removed, and the flag --flat-split is
    now infective (see #6238
    and #6263).

    Matching can be enabled using the --flat-split flag. Note that in
    Cubical Agda functions that match on an argument marked with @flat
    trigger the UnsupportedIndexedMatch warning, and the code might
    not compute properly.

Reflection

  • Two new reflection primitives

    declareData      : Name → Nat → Type → TC ⊤
defineData       : Name → List (Σ Name (λ _ → Type)) → TC ⊤

    are added for declaring and defining datatypes, similar to
    declareDef and defineDef.

  • The construct unquoteDecl is extended with the ability of bringing
    a datatype d and its constructors c₁ ... cₙ given by a TC
    computation m into scope by the following syntax:

    unquoteDecl data x constructor c₁ .. cₙ = m

  • A new reflection primitive getInstances : Meta → TC (List Term)
    was added to Agda.Builtin.Reflection. This operation returns the
    list of all possibly valid instance candidates for a given
    metavariable. For example, the following macro instantiates the goal
    with the first instance candidate, even if there are several:

    macro
  pickWhatever : Term → TC ⊤
  pickWhatever hole@(meta m _) = do
    (cand ∷ _) ← getInstances m
      where [] -> typeError (strErr "No candidates!" ∷ [])
    unify hole cand
  pickWhatever _ = typeError (strErr "Already solved!" ∷ [])

  • [Breaking] The reflection primitives getContext and inContext use a nominal context
    List (Σ String λ _ → Arg Type) instead of List (Arg Type) for printing
    type information better. Similarly, extendContext takes an extra argument
    of type String.

  • macro definitions can now be used even when they are declared as erased.
    For example, this is now accepted:

    macro
  @0 trivial : Term → TC ⊤
  trivial = unify (con (quote refl) [])

test : 42 ≡ 42
test = trivial

  • A new reflection primitive formatErrorParts : List ErrorPart → TC String
    is added. It takes a list of ErrorPart and return its formatted string.

  • [Breaking] A new constructor pattErr : Pattern → ErrorPart of ErrorPart for reflection
    is added.

  • [Breaking] The reflection primitives getType and
    getDefinition respect the module context they are invoked from
    instead of returning information that would be expected in the top
    context.

  • [Breaking] The reflection primitive inContext cannot step
    outside of the context that the TC computation is invoked from
    anymore. The telescope is now relative to that context instead.

Syntax

  • It is now OK to put lambda-bound variables anywhere in the
    right-hand side of a syntax declaration. However, there must always
    be at least one "identifier" between any two regular "holes". For
    instance, the following syntax declaration is accepted because -
    is between the holes B and D.

    postulate
  F : (Set → Set) → (Set → Set) → Set

syntax F (λ A → B) (λ C → D) = B A C - D

  • Syntax can now use lambdas with multiple arguments
    (#394).

    Example:

    postulate
  Σ₂ : (A : Set) → (A → A → Set) → Set

syntax Σ₂ A (λ x₁ x₂ → P) = [ x₁ x₂ ⦂ A ] × P

Builtins

  • [Breaking] Change primFloatToWord64 to return Maybe Word64.
    (See #6093.)

    The new type is

      primFloatToWord64 : Float → Maybe Word64

    and it returns nothing for NaN.

  • [Breaking] The type expected by the builtin EQUIVPROOF has been changed to
    properly encode the condition that EQUVIFUN is an equivalence.
    (#5661,
    #6032)

  • [**Breaking...

Read more

Contributors

phadej, Saizan, and 44 other contributors
Loading