List view

Dispose of special handling of SafeFlagPragma

safeSubset of Agda features which is expected to be consistentSubset of Agda features which is expected to be consistent

ux: optionsIssues relating to Agda's command line optionsIssues relating to Agda's command line options

ux: warningsIssues relating to the reporting of warningsIssues relating to the reporting of warnings

Status: Draft (not ready).

agda/agdanumber 7493

#7493 In agda/agda;

· andreasabel opened on Sep 13, 2024

Issue #7714: New cabal flag -f Werror to control -Werror

buildConcerning building of AgdaConcerning building of Agda

releaseConcerning the release process and releases (not in changelog)Concerning the release process and releases (not in changelog)

Status: Draft (not ready).

agda/agdanumber 7718

#7718 In agda/agda;

· andreasabel opened on Feb 20, 2025

Restrict pattern matching in binding position to eta-equality records (#6845 reopened)

etaη-expansion of metavariables and unification modulo ηη-expansion of metavariables and unification modulo η

language changeChanges to the language which can be observed by Agda's userbaseChanges to the language which can be observed by Agda's userbase

letIssues relating to let expressionsIssues relating to let expressions

pattern binderIssues with record patterns in binders.Issues with record patterns in binders.

pr: squash-meThis PR needs squashingThis PR needs squashing

Status: Open (in progress).

agda/agdanumber 6848

#6848 In agda/agda;

· andreasabel opened on Sep 13, 2023

Create release version with Cabal flag instead of by editing files

cabalBuild problems specifically related to cabal-installBuild problems specifically related to cabal-install

releaseConcerning the release process and releases (not in changelog)Concerning the release process and releases (not in changelog)

Status: Open.

#7714 In agda/agda;

· wenkokke opened on Feb 18, 2025

Mimer has problems instantiating predicates

MimerIssue with the Mimer proof search engineIssue with the Mimer proof search engine

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

Status: Open.

#7972 In agda/agda;

· andreasabel opened on Jun 30, 2025

Normalise does not normalize Level (anymore ?)

levels

reduction

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

Status: Open.

Bug

#8060 In agda/agda;

· andreasabel opened on Aug 9, 2025

Non-normalized level printed for interactive "show constraints" and "solve"

levels

ux: interactionIssues to do with interactive development (holes, case splitting, etc)Issues to do with interactive development (holes, case splitting, etc)

Status: Open.

#8100 In agda/agda;

· andreasabel opened on Sep 12, 2025

On warning about redundant imports

importIssues to do with importing modulesIssues to do with importing modules

interfaceSerialization and loading of interface filesSerialization and loading of interface files

modulesIssues relating to the module systemIssues relating to the module system

type: enhancementIssues and pull requests about possible improvementsIssues and pull requests about possible improvements

ux: warningsIssues relating to the reporting of warningsIssues relating to the reporting of warnings

Status: Open.

#2503 In agda/agda;

· gallais opened on Mar 19, 2017

M-. does not work in the information buffer

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open.

#8256 In agda/agda;

· nad opened on Dec 2, 2025

Update -WUnusedImports to take modules into consideration

importIssues to do with importing modulesIssues to do with importing modules

maculataIssue with a so far unreleased feature (not in changelog)Issue with a so far unreleased feature (not in changelog)

ux: warningsIssues relating to the reporting of warningsIssues relating to the reporting of warnings

Status: Draft (not ready).

agda/agdanumber 8271

#8271 In agda/agda;

· andreasabel opened on Dec 8, 2025

Editing a file while it is being checked causes misnumbered holes.

regression on masterUnreleased regression in development version (Change to "regression in ..." should it be released!)Unreleased regression in development version (Change to "regression in ..." should it be released!)

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

ux: interactionIssues to do with interactive development (holes, case splitting, etc)Issues to do with interactive development (holes, case splitting, etc)

Status: Open.

#8275 In agda/agda;

· oskeri opened on Dec 10, 2025

Putting a pattern record in an index kills canonicity for cubical

cubicalCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transpCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp

etaη-expansion of metavariables and unification modulo ηη-expansion of metavariables and unification modulo η

language changeChanges to the language which can be observed by Agda's userbaseChanges to the language which can be observed by Agda's userbase

recordsRecord declarations, literals, constructors and updatesRecord declarations, literals, constructors and updates

Status: Open.

Bug

#8370 In agda/agda;

· howtonotwin opened on Feb 5, 2026

Go-to-definition fails for certain parts of certain names

agda-modeIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

regression on masterUnreleased regression in development version (Change to "regression in ..." should it be released!)Unreleased regression in development version (Change to "regression in ..." should it be released!)

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open.

#8419 In agda/agda;

· nad opened on Feb 24, 2026

experiment: check cubical in parallel

infra: github workflowsIssues related to GitHub workflows and actions (not in changelog)Issues related to GitHub workflows and actions (not in changelog)

parallelRelated to parallel type-checkingRelated to parallel type-checking

type: taskConcerning the development of Agda (not in changelog)Concerning the development of Agda (not in changelog)

Status: Open (in progress).

agda/agdanumber 8396

#8396 In agda/agda;

· plt-amy opened on Feb 13, 2026

-WUnusedImports fails to find uses related to pattern matching

Status: Open.

#8294 In agda/agda;

· oskeri opened on Dec 18, 2025

The Emacs mode does not jump to errors in imported files

regression on masterUnreleased regression in development version (Change to "regression in ..." should it be released!)Unreleased regression in development version (Change to "regression in ..." should it be released!)

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open.

#8452 In agda/agda;

· nad opened on Mar 5, 2026

Agda hanging on cyclic meta instantiation

Agda loopsNon-termination of Agda (e.g. type-checker loops)Non-termination of Agda (e.g. type-checker loops)

regression on masterUnreleased regression in development version (Change to "regression in ..." should it be released!)Unreleased regression in development version (Change to "regression in ..." should it be released!)

Status: Open.

#8457 In agda/agda;

· AndrasKovacs opened on Mar 5, 2026

Mark all non-delimiter characters as word constituents in agda2-mode-syntax-table

agda-modeIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open (in progress).

agda/agdanumber 8450

#8450 In agda/agda;

· TOTBWF opened on Mar 4, 2026

[ #8452 ] Make agda2-maybe-goto jump across files

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

ux: emacsIssues relating to the Emacs agda2-modeIssues relating to the Emacs agda2-mode

Status: Open (in progress).

agda/agdanumber 8458

#8458 In agda/agda;

· TOTBWF opened on Mar 5, 2026

Lack of subject reduction because the SIGMA builtin accepts types that are not Σ-types

builtinEnhancements to the builtin modules and builtin definitionsEnhancements to the builtin modules and builtin definitions

falseProof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type)Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type)

reflectionElaborator reflection, macros, tactic argumentsElaborator reflection, macros, tactic arguments

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

Status: Open.

#8453 In agda/agda;

· nad opened on Mar 5, 2026

Repeated type-checking when -j is used

parallelRelated to parallel type-checkingRelated to parallel type-checking

type: bugIssues and pull requests about actual bugsIssues and pull requests about actual bugs

Status: Open.

#8477 In agda/agda;

· nad opened on Mar 21, 2026

Make Agda go faster

performanceSlow type checking, interaction, compilation or execution of Agda programsSlow type checking, interaction, compilation or execution of Agda programs

Status: Open (in progress).

agda/agdanumber 8473

#8473 In agda/agda;

· AndrasKovacs opened on Mar 17, 2026

re. #8457: only ask if meta is an IP if cubical

cubicalCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transpCubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp

Status: Open (in progress).

agda/agdanumber 8460

#8460 In agda/agda;

· plt-amy opened on Mar 5, 2026

Deprecate non-ES6 JS module styles

backend: jsJavaScript generation backendJavaScript generation backend

Status: Open (in progress).

agda/agdanumber 8447

#8447 In agda/agda;

· lawcho opened on Mar 4, 2026