Skip to content

Pull requests: agda/agda

New pull request New
58 Open 2,382 Closed
58 Open 2,382 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Made it possible to turn off the occurrence analysis for functions performance Slow type checking, interaction, compilation or execution of Agda programs positivity Positivity checking for data-type definitions
#8295 opened Dec 18, 2025 by nad Loading… 2.9.0
@nad
1
Literate forester without external tool backend: forester backends pr: squash-me This PR needs squashing
#8290 opened Dec 15, 2025 by dannypsnl Loading…
1
7
Qualified do and qualified idiom brackets do notation Checking and desuraging of do notation, idiom brackets, matching in `do` blocks idiom brackets Desugaring and checking of idiom brackets pr: squash-me This PR needs squashing syntax Bike-shedding of the surface syntax
#8280 opened Dec 12, 2025 by plt-amy Loading… 2.9.0
16
Library management: support defaults-X.Y.Z files pr: squash-me This PR needs squashing type: enhancement Issues and pull requests about possible improvements ux: library management Issues relating to the library management system
#8279 opened Dec 12, 2025 by gallais Loading… 2.9.0
8
Improve caching for (large) opaque blocks caching Recompilation avoidance, interface files opaque Issues about `opaque` definitions type: enhancement Issues and pull requests about possible improvements
#8278 opened Dec 12, 2025 by andreasabel • Draft 2.9.0
Fix #8273: Consider interface to merge imported in mergeInterface
#8274 opened Dec 8, 2025 by NathanielB123 • Draft
1
1
Track module usage in -WUnusedImports warnings
#8272 opened Dec 8, 2025 by Copilot AI • Draft
@andreasabel
Update -WUnusedImports to take modules into consideration import Issues to do with importing modules maculata Issue with a so far unreleased feature (not in changelog) ux: warnings Issues relating to the reporting of warnings
#8271 opened Dec 8, 2025 by andreasabel • Draft 2.9.0
2
More semantic structure of html generated from agda files
#8241 opened Nov 29, 2025 by marcinjangrzybowski • Draft
New Warning to Fix #5929 pr: squash-me This PR needs squashing rewriting Rewrite rules, rewrite rule matching singleton-types Issues related to conversion modulo eta-equality for singleton types
#8238 opened Nov 29, 2025 by NathanielB123 Loading… 2.9.0
1
20
new feature: quote metas meta Metavariables, insertion of implicit arguments, etc pr: squash-me This PR needs squashing reflection Elaborator reflection, macros, tactic arguments ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#8235 opened Nov 28, 2025 by rybla Loading…
4 tasks done
2.9.0
@rybla
27
AST based navigation/interaction in emacs
#8219 opened Nov 24, 2025 by marcinjangrzybowski • Draft
1
Xref support for Agda2-mode ux: emacs Issues relating to the Emacs agda2-mode
#8181 opened Nov 1, 2025 by phikal Loading… 2.9.0
22
Generate parts of the Agda input method procedurally ux: emacs Issues relating to the Emacs agda2-mode
#8180 opened Nov 1, 2025 by phikal Loading… 2.9.0
12
GHC 9.14 ghc-9.14
#8086 opened Sep 1, 2025 by andreasabel • Draft 2.9.0
1
Eldoc support in goals
#8077 opened Aug 25, 2025 by plt-amy • Draft
1
Double-checking meta solutions: fail hard on errors
#8061 opened Aug 9, 2025 by andreasabel • Draft
Link to latest readthedocs rather than to 2.9.0 ux: colors Concerning coloring of Agda's output ux: error reporting Issues to do with how Agda reports errors
#8032 opened Jul 28, 2025 by andreasabel • Draft 2.9.0
@andreasabel
4
Simplifications to blocked metas and postponed typechecking problems meta Metavariables, insertion of implicit arguments, etc refactor Changes to the code base which do not affect users (not in changelog)
#7899 opened May 27, 2025 by jespercockx • Draft 2.9.0
12
wip: fix ambiguous projection elaboration overloading Overloaded projections; Projection disambiguation projections Issues relating to the treatment of projections
#7897 opened May 26, 2025 by plt-amy • Draft
3
WIP: so far failing attempt at #7656 help wanted
#7844 opened May 1, 2025 by andreasabel • Draft
1
[opt] Lazy 'dontUnfold' in unfoldDefinition reduction status: do-not-merge So please don't merge
#7821 opened Apr 28, 2025 by andreasabel • Draft
Prefer name hints from constructor definitions type: discussion Discussions about Agda's design and implementation 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) ux: printing Issues relating to how terms are printed for display
#7754 opened Mar 21, 2025 by lawcho • Draft
8
Issue #7714: New cabal flag -f Werror to control -Werror build Concerning building of Agda release Concerning the release process and releases (not in changelog)
#7718 opened Feb 20, 2025 by andreasabel • Draft 2.9.0
1
@andreasabel
6
WIP: make agda-tests into its own package
#7717 opened Feb 20, 2025 by andreasabel • Draft
ProTip! Mix and match filters to narrow down what you’re looking for.