8000 Releases · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Releases: agda/agda

d15a8eb@master

28 May 20:10
@github-actions github-actions
nightly
d15a8eb
Compare
Choose a tag to compare
d15a8eb@master Pre-release
Pre-release

What's Changed

Read more

Contributors

nad, markusschlegel, and 26 other contributors
Loading

v2.8.0-rc1 Agda 2.8.0 release candidate 1

12 May 05:04
@github-actions github-actions
v2.8.0-rc1
b89aacf
Compare
Choose a tag to compare
v2.8.0-rc1 Agda 2.8.0 release candidate 1 Pre-release
Pre-release

Release notes for Agda version 2.8.0

Highlights

  • Agda is now a self-contained single binary.

  • Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.

  • Experimental support for polarity annotations with new flag --polarity.

  • Compile to JavaScript with ES6 module syntax with new flag --js-es6.

  • Errors now have an identifier and follow the GNU standard.

Installation

  • Dropped support for GHC 8.6, added support for GHC 9.12.

  • Agda supports GHC versions 8.8.4 to 9.12.2.

  • The agda binary now contains everything to set itself up,
    it need not be shipped with additional files.

    1. The functionality of the agda-mode executable has been replicated
      under the new option --emacs-mode.
      The agda-mode executable is now deprecated.
      References to agda-mode in your .emacs file should be replaced
      by agda --emacs-mode.

    2. Agda now contains all its data files,
      like primitive and builtin modules,
      supplements for the HTML and LaTeX backends,
      the runtimes for the JS and GHC backends,
      and the emacs mode.

      These will be written to ${Agda_datadir}/${VERSION}
      on the first invocation of agda or an invocation of
      agda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
      Herein, ${VERSION} is the Agda version and ${Agda_datadir}
      the Agda data directory, on Unix-like systems
      defaulting to ${HOME}/.local/share/agda.

    The Cabal/Stack custom installation Setup.hs has been removed
    that previously generated the .agdai files for the builtin and primitive modules.
    These will now be generated by Agda whenever they are needed,
    just as for ordinary modules.

    This change is breaking for packagers of Agda
    as the packaging routines might need to be updated
    (but should become simpler).

  • Added cabal build flag dump-core to save the optimised GHC Core code during
    compilation of Agda. This can be useful for people working on improving the
    performance of the Agda implementation.

Pragmas and options

  • New main mode of operation --build-library (issue #4338).
    Invoking agda --build-library will look for an .agda-lib file starting in the current directory.
    It will then extract the include directories of this library,
    collect all Agda files in these directories and their subdirectories,
    and check all these files.

  • New option --setup that writes out the Agda data files (see above)
    and can be used to regenerate them.

  • New option --emacs-mode to administer the Emacs mode
    as previously done by the agda-mode executable.

  • Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.

  • 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.

Warnings

  • New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance
    when wrong user-written attribute was corrected automatically by Agda.

  • New deadcode 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 #-}

  • Unused CATCHALL pragmas now trigger UselessPragma warnings.

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

  • New deadcode warning TooManyPolarities instead of hard error
    when a POLARITY pragma gives polarities that exceed the known
    arity of the postulate.

  • New deadcode warning UselessTactic when a @tactic attribute has no effect,
    typically when it is attached to a non-hidden or instance argument.

  • 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.

  • Warning AbsurdPatternRequiresNoRHS has been renamed to
    AbsurdPatternRequiresAbsentRHS.

  • Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced
    by new warnings OpenImportAbstract and OpenImportPrivate.

  • Warning NoGuardednessFlag has been removed.
    Instead Agda gives a hint when --guardedness would help with termination checking,
    unless options --sized-types or --no-guardedness are set.

Polarity

  • Support for polarity annotations can be enabled by the feature flag
    --polarity.

    This flag is infective.

    Uses of variables bound with polarity annotations are checked through modal
    typing rules, and the positivity checker has been expanded to take annotations
    into account. This means that the following is now definable:

    {-# OPTIONS --polarity #-}

data Mu (F : @++ Set → Set) : Set where
  fix : F (Mu F) → Mu F

Syntax

Additions to the Agda syntax.

  • Add new literate agda: forester, see #7403

  • 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.

  • BREAKING: The primitive "cubical identity type", previously
    exported from Agda.Builtin.Cubical.Id, has been removed. Its
    computational behaviour is exactly replicated by the user-definable
    identity type, which is also exported from Agda.Builtin.Equality.

    See agda/cubical#1005 for
    the PR removing it from the library, and
    #7652 for the compiler.

  • Inlining constructors no longer happens on the right-hand-sides of
    INLINE functions. This allows using INLINE functions to define
    "smart constructors" for record types which have the same reduction
    behaviour as using the actual constructor would. Small example:

    triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }

ex = triple 1 2 3

    Here, constructor inlining happens on the right hand side of ex
    rather than of triple.

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

  • BREAKING: Agda no longer accepts several .agda-lib files in the root
    of an Agda project.
    (Previously, it allowed this and took the union of their contents.)

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.

  • When generating clauses after case splitting on a datatype defined in a parameterised module,
    Agda now prints constructor names without a module prefix rather than fully qualified (see issue #3209).
    This is only a surface-level fix, since Agda might still fail to find the properly qualified name for
    the constructor in scope, but should at least make more sense in most situations.

  • New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack ...

Read more

Contributors

nad, markusschlegel, and 26 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 8000 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
0