Release notes for Agda version 2.6.2.1

Highlights

• Agda 2.6.2.1 catches up to changes in the Haskell ecosystem (GHC 9.2.1, aeson-2.0, hashable-1.4.).

• Fixes some regressions introduced in 2.6.1: #5283 #5506 #5610

• Fixes some regressions introduced in 2.6.2: #5508 #5544 #5565 #5584 #5620 #5638 #5657

• Improvements to the compiler backends (see below).

• Feature preview: --ghc-strict.

Installation and infrastructure

Agda 2.6.2.1 is expected to build with GHC versions 8.0 to 9.2. It has been tested with the latest minor version releases of GHC for each of these major versions:

• 8.0.2
• 8.2.2
• 8.4.4
• 8.6.5
• 8.8.4
• 8.10.7: Issue #5539.
• 9.0.1
• 9.2.1: Issue #5442, stackage issue #6318.

Agda 2.6.2.1 has been adapted to recent changes in the Haskell ecosystem, including:

• Cabal-3.6.2
• aeson-2.0: Issue #5593, stackage issue #6217.
• hashable-1.4: Stackage issue #6268.
• transformers-0.6

Compiler backends

• Both the GHC and JS backends now refuse to compile code that uses --cubical.

• The new option --ghc-strict-data, which is inspired by the GHC language extension StrictData, makes the GHC backend compile inductive data and record constructors to constructors with strict arguments.

  This does not apply to certain builtin types—lists, the maybe type, and some types related to reflection—and might not apply to types with COMPILE GHC … = data … pragmas.

  This feature is experimental.

• The new option --ghc-strict, which is inspired by the GHC language extension Strict, makes the GHC backend generate mostly strict code.

  Functions might not be strict in unused arguments.

  Function definitions coming from COMPILE GHC pragmas are not affected.

  This flag implies --ghc-strict-data, and the exceptions of that flag applies to this flag as well.

  Note that this option requires the use of GHC 9 or later.

  This feature is experimental.

• JS backend now uses the native BigInt instead of the biginteger.js. Fixes #4878.

LaTeX backend

• Files agda.sty and postprocess-latex.pl are now found in the latex/ subdirectory of the Agda data directory (agda --print-agda-dir).

• agda.sty is now versioned (printed to the .log file by latex) (see #5473).

• Italics correction (inserted by \textit e.g. in \AgdaBound) now works, thanks to moving the \textcolor wrapping to the outside in agda.sty (see #5471).

List of closed issues

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

• #4878: Replace biginteger.js with native BigInt
• #5283: Tactic command runs forever
• #5291: match doesn't work for non-prefix-free cases
• #5302: building tests with cabal
• #5396: Internal error for rewriting without --confluence-check
• #5398: Problem with LaTeX code for multi-line comments with blank lines
• #5420: The JS backend generates incorrect code for Agda code that uses reflection
• #5421: The GHC backend generates incorrect code for Agda code that uses reflection
• #5431: --ghc-strict-data and --ghc-strict
• #5433: The JS backend "installs" highlight-hover.js
• #5440: (Re)Documenting catchfilebetweentags method of building latex files with Agda
• #5442: Support GHC 9.2
• #5463: Hole in the middle of a record is malformed
• #5465: Compilation of Parser.y depends on the locale on Debian too
• #5469: onlyReduceDefs should not prevent evaluation of macros
• #5470: Internal error when using REWRITE in private block
• #5471: LaTeX backend: italics correction
• #5473: agda.sty has no version
• #5478: Open goal inside record causes internal error (eta-contraction)
• #5481: Pattern-matching on records in Prop allows eliminating into Set
• #5489: C-c C-x C-a (abort) does not communicate well
• #5490: Why does abort (C-c C-x C-a) remove highlighting from the buffer?
• #5506: Agda panic: Pattern match failure
• #5508: Internal error typechecking non-terminating function on case-insensitive filesystem
• #5514: Support GHC 8.10.6
• #5531: Internal bug: TypeChecking/Sort
• #5532: "The module was successfully compiled" should mention with which backend
• #5539: Support GHC 8.10.7
• #5544: Internal error caused by addition of Checkpoints to OpenThing
• #5557: Allow Agda to output data files
• #5565: Internal error in Agda.TypeChecking.MetaVars
• #5593: Compilation failure with aeson-2
• #5602: The JS backend does not reduce constructor type signatures
• #5610: Panic when checking pragma BUILTIN SHARP
• #5620: Seemingly incorrect warning for abstract definition without type signature
• #5633: Case splitting inserts one with pattern too much (regression in 2.6.2)
• #5657: Internal error with postfix projection