Skip to content

Releases: agda/agda

Nightly Build (0ff0741@master)

06 May 14:34
@github-actions github-actions
nightly
0ff0741
Compare
Choose a tag to compare
Nightly Build (0ff0741@master) Latest
Latest

What's Changed

Read more

Contributors

WhatisRT, 0, and 21 other contributors
Assets 5

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

Assets 2

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
Assets 2

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
Assets 2

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
Assets 2

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
Assets 2