Agda

A dependently typed functional programming language and proof assistant

https://wiki.portal.chalmers.se/agda/

Version on this page:2.7.0.1
LTS Haskell 22.39:2.6.4.3@rev:1
Stackage Nightly 2024-10-31:2.7.0.1@rev:2
Latest on Hackage:2.7.0.1@rev:2

See all snapshots Agda appears in

MIT licensed by The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
Maintained by The Agda Team
This version can be pinned in stack with:Agda-2.7.0.1@sha256:de2cd86b8bc48a4db277f14bb39c63ffc95ea6b79ff2aa266eccf52b2045e909,29553

Module documentation for 2.7.0.1

Agda 2

Hackage version Stackage version Test Documentation Status Agda Zulip

The official Agda logo

Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.

Documentation

Getting Started

Contributing to Agda

Changes

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