Agda v2.6.3 Release Notes

  • Installation and infrastructure

    πŸ‘ Agda supports GHC versions 8.0.2 to 9.2.3.

    Language

    • 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 and JS backends can compile code that uses --erased-cubical if the top-level module uses this flag.

    This feature is experimental.

    • The parameter arguments of constructors and record fields are now marked as erased (#4786).

    For instance, the type of the constructor c below is now {@0 A : Set} β†’ D A, and the type of the record field R.f is {@0 A : Set} β†’ R A β†’ A:

      data D (A : Set) : Set where
        c : D A
    
      record R (A : Set) : Set where
        field
          f : A
    
    • βž• Added an option --erase-record-parameters that additionally marks parameters to definitions in a record module as erased (#5770). For example:
      {-# OPTIONS --erase-record-parameters #-}
    
      postulate A : Set
      postulate a : A
    
      record R (x : A) : Set where
        y : A
        y = a
    
      f : (@0 x : A) β†’ R x β†’ A
      f x r = R.y {x} r
    
    • 🚚 The options --subtyping and --no-subtyping have been removed (see #5427).

    • The cubical interval I now belongs to its own sort, IUniv, rather than SSet. For J : ISet and A : J β†’ Set l, we have (j : J) β†’ A : Set l, that is, the type of functions from a type in ISet 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 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 [email protected](meta m _) = do
        (cand ∷ _) ← getInstances m
          where [] -> typeError (strErr "No candidates!" ∷ [])
        unify hole cand
      pickWhatever _ = typeError (strErr "Already solved!" ∷ [])
      
    • 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.
    
    * A new constructor `pattErr : Pattern β†’ ErrorPart` of `ErrorPart` for reflection
      is added.
    
    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`.
    
      ```agda
      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
    

    Library management

    • Library files below the "project root" are now ignored (see #5644).

    For instance, if you have a module called A.B.C in the directory Root/A/B, then .agda-lib files in Root/A or Root/A/B do not affect what options are used to type-check A.B.C: .agda-lib files for A.B.C have to reside in Root, or further up the directory hierarchy.

    Pragmas and options

    • It is now possible to declare several BUILTIN REWRITE relations. Example: ```agda {-# OPTIONS --rewriting #-}

    open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite -- 1st rewrite relation

    postulate R : (A : Set) β†’ A β†’ A β†’ Set A : Set a b c : A foo : R A a b -- using 2nd rewrite relation bar : b ≑ c -- using 1st rewrite relation

    {-# BUILTIN REWRITE R #-} -- 2nd rewrite relation {-# REWRITE foo bar #-}

    test : a ≑ c test = refl

    
    * πŸ†• New verbosity `-v debug.time:100` adds time stamps to debugging output.
    
    * Profiling options are now turned on with a new `--profile` flag instead of
      abusing the debug verbosity option. (See [#5781](https://github.com/agda/agda/issues/5731).)
    
    * πŸ‘€ The option `--without-K` has been renamed `--cubical-compatible` (See
      [#5843](https://github.com/agda/agda/issues/5843).)
    
      The old name is retained for backwards compatibility.
    
    🐎 Performance
    -----------
    
    * Meta-variables can now be saved in `.agdai` files, instead
      of being expanded. This can affect performance. (See
      [#5731](https://github.com/agda/agda/issues/5731).)
    
      Meta-variables are saved if the pragma option `--save-metas` is
      used. This option can be overridden by `--no-save-metas`.
    
    * The new option `--syntactic-equality[=FUEL]` can be used to limit
      how many times the syntactic equality shortcut is allowed to fail
      (see [#5801](https://github.com/agda/agda/issues/5801)).
    
      If `FUEL` is omitted, then the syntactic equality shortcut is
      enabled without any restrictions.
    
      If `FUEL` is given, then the syntactic equality shortcut is given
      `FUEL` units of fuel. The exact meaning of this is
      implementation-dependent, but successful uses of the shortcut do not
      affect the amount of fuel. Currently the fuel is decreased in the
      failure continuations of the implementation of the syntactic
      equality shortcut. When a failure continuation completes the fuel is
      restored to its previous amount.
    
      The idea for this option comes from AndrΓ‘s KovΓ‘cs'
      [smalltt](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#approximate-conversion-checking).
    
    Compiler backends
    -----------------
    
    * Both the GHC and JS backends now refuse to compile code that uses
      `--cubical`.
    
      Note that support for compiling code that uses `--erased-cubical`
      has been added to both backends (see above).
    
    LaTeX backend
    -------------
    
    DOT backend
    -----------
    
    * The new option `--dependency-graph-include=LIBRARY` can be used to
      restrict the dependency graph to modules from one or more libraries
      (see [#5634](https://github.com/agda/agda/issues/5634)).
    
      Note that the module given on the command line might not be
      included.
    
    * The generated graphs no longer contain "redundant" edges: if a
      module is imported both directly and indirectly, then the edge
      corresponding to the direct import is omitted.
    
    JSON API
    --------
    
    * The JSON API now represents meta-variables differently, using
      objects containing two keys, `id` and `module`, both with values
      that are (natural) numbers. See
      [#5731](https://github.com/agda/agda/issues/5731).