Skip to content

Issues: agda/agda

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

964 Open 4,438 Closed
964 Open 4,438 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

INJECTIVE_FOR_INFERENCE silently ignored on non-functions lossy unification maculata Issue with a so far unreleased feature (not in changelog) release blocker Issues blocking the next Agda release ux: warnings Issues relating to the reporting of warnings
#7245 opened May 3, 2024 by andreasabel 2.7.0
Release Agda 2.7.0 release Concerning the release process and releases (not in changelog)
#7242 opened May 2, 2024 by jespercockx 2.7.0
makefile hlint target needs cabal_macros.h
#7240 opened Apr 29, 2024 by philderbeast
CI Stack Windows fails to install build-tools (permission denied) infra: github workflows Issues related to GitHub workflows and actions (not in changelog) platform: windows Any issue specific to Microsoft Windows stack Concerning building with stack
#7232 opened Apr 20, 2024 by andreasabel
1
Save-metas causes OOM during macro execution dead-code Concerning the dead-code removal optimization type: bug Issues and pull requests about actual bugs
#7227 opened Apr 17, 2024 by plt-amy
1
2
No reproducer for error raised in telePiPath GenericError Concerning GenericError and GenericDocError infra: test suite Issues relating to the test suite (not in changelog) ux: error reporting Issues to do with how Agda reports errors
#7226 opened Apr 15, 2024 by andreasabel
Named errors instead of Generic[Doc]Error GenericError Concerning GenericError and GenericDocError
#7225 opened Apr 15, 2024 by andreasabel
1 of 50 tasks
OptionWarnings are emitted twice type: bug Issues and pull requests about actual bugs ux: warnings Issues relating to the reporting of warnings
#7221 opened Apr 13, 2024 by andreasabel
2
semantically unjustified coinduction coinduction Coinductive records, musical coinduction guardedness Problems of the guardedness checker for coinduction. status: duplicate Duplicate issue (not in changelog) type: bug Issues and pull requests about actual bugs
#7220 opened Apr 11, 2024 by mikeshulman
24
Agda prints hidden function type in hidden argument as {{... and then fails to parse it hidden arguments Insertion of hidden arguments and implicit lambdas instance Instance resolution parser Problems with the parser's implementation (rather than with decisions about syntax) type: bug Issues and pull requests about actual bugs ux: printing Issues relating to how terms are printed for display
#7214 opened Mar 30, 2024 by andreasabel 2.7.0
1
Mimer doesn't fill with simplified solution auto Issues to do with the Auto proof search (Mimer, Agsy) Mimer Issue with the Mimer proof search engine
#7212 opened Mar 30, 2024 by leoydm 2.7.0
@UlfNorell
3
Changelog for #7183 type: task Concerning the development of Agda (not in changelog)
#7207 opened Mar 27, 2024 by plt-amy 2.8.0
@plt-amy
Hole/postulate asymmetry in @++ checker meta Metavariables, insertion of implicit arguments, etc modalities polarity positivity Positivity checking for data-type definitions postulate Concerning postulates.
#7205 opened Mar 27, 2024 by lawcho
Agda re-checks a file with an up-to-date interface file performance Slow type checking, interaction, compilation or execution of Agda programs regression in 2.6.2 Regression that first appeared in Agda 2.6.2 type: bug Issues and pull requests about actual bugs
#7199 opened Mar 21, 2024 by nad 2.7.0
Agda always has irrelevant projections cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp false Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type) irrelevance Issues to do with irrelevance annotations irrelevant-projections Irrelevant projections and irrelevant definitions release blocker Issues blocking the next Agda release type: bug Issues and pull requests about actual bugs
#7193 opened Mar 16, 2024 by dolio 2.7.0
@andreasabel
6
show does not respect abstract/opaque when normalising a term in a hole type: bug Issues and pull requests about actual bugs
#7191 opened Mar 15, 2024 by Sean-Watters
3
Unhelpful @++ errors mutual polarity positivity Positivity checking for data-type definitions ux: error reporting Issues to do with how Agda reports errors
#7189 opened Mar 13, 2024 by lawcho
2
Module parameter @++ annotations bug or feature? It may be a bug, it may be a feature. modules Issues relating to the module system parameters Module parameters polarity
#7188 opened Mar 12, 2024 by lawcho
3
Termination checking is not stable under copattern translation record-expression-to-copatterns Concerning the translation of rhss which are record expressions to copattern matching. termination Issues relating to the termination checker type: bug Issues and pull requests about actual bugs
#7186 opened Mar 12, 2024 by plt-amy
getDefinition gives wrong constructor for record from applied parameterised module reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
#7182 opened Mar 11, 2024 by UlfNorell 2.7.0
@UlfNorell
Sized types allow defining inconsistent data false Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type) sized types Sized types, termination checking with sized types, size inference
#7178 opened Mar 10, 2024 by knisht icebox
1
Feature Request: Prefix arg for Case split introducing implicit arguments type: enhancement Issues and pull requests about possible improvements ux: case splitting Issues relating to the case split ("C-c C-c") command ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#7174 opened Mar 8, 2024 by maxsnew icebox
No tests for tagged releases infra: test suite Issues relating to the test suite (not in changelog) release Concerning the release process and releases (not in changelog)
#7164 opened Mar 4, 2024 by wenkokke
5
cabal install Agda -- fails with executable-dynamic cabal Build problems specifically related to cabal-install dynamic linking Problems compiling Agda using dynamic linking Setup.hs Concerning the Custom build type of Agda upstream ux: installation Getting Agda set up on your machine
#7163 opened Mar 3, 2024 by ulidtko 2.7.0
1
17
Future: cabal build-type Setup will be phased out in favor of Hooks cabal Build problems specifically related to cabal-install Setup.hs Concerning the Custom build type of Agda
#7157 opened Feb 29, 2024 by andreasabel later
ProTip! Type g i on any issue or pull request to go back to the issue listing page.