Owner

agda

Sign in to follow

5 indexed repositories · View on GitHub

Beginner friendly Everything
Open All

Issues somebody may already be working on are listed last. List everything by date

  • JS backend: Word64 values wrap modulo 18446744073709552000 instead of 2^64, unlike the type checker and the GHC backend
    Open
    • Is something wrong?

    Difficulty 2/5 1-3 hours Newbie friendliness 70/100

    agda/agda#8913 ·

    Maintainers usually reply within 1 day

  • JS backend: `primStringToList` and `primStringUncons` split strings into UTF-16 code units, so a character outside the BMP becomes two `Char`s
    Open
    • Is something wrong?

    Difficulty 2/5 1-3 hours Newbie friendliness 66/100

    agda/agda#8911 ·

    Maintainers usually reply within 1 day

  • Support existential types
    Open
    • Is something wrong?
    enhancement

    Difficulty 5/5 Over a week Newbie friendliness 8/100

    agda/agda2hs#492 ·

    Maintainers usually reply within 1 day

  • Upstreaming things from `categorical-crypto`
    Open
    • Is something wrong?

    Difficulty 5/5 Over a week Newbie friendliness 25/100

    agda/agda-categories#559 · 1 comment ·

  • Testsuite latex/html: do not allow to overwrite golden value when Agda run fails
    Open
    • Is something wrong?
    infra: test suite

    Difficulty 2/5 1-3 hours Newbie friendliness 72/100

    agda/agda#8909 ·

    Maintainers usually reply within 1 day

  • `iLawfulOrdDouble` is refuted by NaN and gives a proof of `⊥`
    Open
    • Is something wrong?
    bug library

    Difficulty 4/5 3-5 days Newbie friendliness 45/100

    agda/agda2hs#488 · 1 comment ·

    Maintainers usually reply within 1 day

  • `prop-member-map` in `Haskell.Data.Set` is false for non-injective functions and gives a proof of `⊥`
    Open
    • Is something wrong?
    bug library

    Difficulty 4/5 3-5 days Newbie friendliness 49/100

    agda/agda2hs#487 · 3 comments ·

    Maintainers usually reply within 1 day

  • What is `DoubleDot` notation
    Open
    • Is something wrong?
    irrelevance modalities shape-irrelevance user-manual

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    agda/agda#8903 · 5 comments ·

    Maintainers usually reply within 1 day

  • `primShowChar` / `primShowString` give different strings in the type checker, the GHC backend and the JS backend
    Open
    • Is something wrong?
    backend: js bug or feature? builtin literals type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    agda/agda#8902 · 1 comment ·

    Maintainers usually reply within 1 day

  • Deprecate `Float`s
    Open
    • Is something wrong?
    float type: discussion warning-on-usage

    Difficulty 5/5 Over a week Newbie friendliness 25/100

    agda/agda#8901 · 5 comments · 1 reaction ·

    Maintainers usually reply within 1 day

  • JS backend: `primFloatToRatio` is approximate and `primFloatToWord64` throws, unlike the type checker and the GHC backend
    Open
    • Is something wrong?
    backend: ghc backend: js backends float type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 55/100

    agda/agda#8899 · 2 comments ·

    Maintainers usually reply within 1 day

  • Builtin imports fail with "COMPILE pragma not allowed in safe mode" when the data directory's `lib` or `lib/prim` is a symlink
    Open
    • Is something wrong?

    Difficulty 2/5 1-3 hours Newbie friendliness 72/100

    agda/agda#8897 ·

    Maintainers usually reply within 1 day

  • `opaque unfolding` and `REWRITE` rules breaks subject reduction
    Open
    • Is something wrong?
    confluence opaque subject reduction

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    agda/agda#8893 · 4 comments · 3 reactions ·

    Maintainers usually reply within 1 day

  • Warning that has been turned off is reported
    Open
    • Is something wrong?
    PR welcome type: bug ux: warnings

    Difficulty 4/5 1-2 days Newbie friendliness 55/100

    agda/agda#8886 · 2 comments ·

    Maintainers usually reply within 1 day

  • 2.8.0: slow "undefined" report
    Open
    • Is something wrong?
    status: MWE needed

    Difficulty 4/5 3-5 days Newbie friendliness 25/100

    agda/agda#8885 · 3 comments ·

    Maintainers usually reply within 1 day

  • Compare things with α-equivalence
    Open
    • Is something wrong?
    bug

    Difficulty 3/5 1-2 days Newbie friendliness 57/100

    agda/agda2hs#479 ·

    Maintainers usually reply within 1 day

  • Bulk hidden arguments
    Open
    • Is something wrong?
    hidden arguments type: enhancement

    Difficulty 5/5 Over a week Newbie friendliness 24/100

    agda/agda#8872 · 1 comment ·

    Maintainers usually reply within 1 day

  • Support type operators in rewrite rules
    Open
    • Is something wrong?
    enhancement

    Difficulty 4/5 1-2 days Newbie friendliness 45/100

    agda/agda2hs#473 ·

    Maintainers usually reply within 1 day

  • `COMPILE to` definitions from `Haskell.*` modules
    Open
    • Is something wrong?
    enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    agda/agda2hs#472 · 1 reaction ·

    Maintainers usually reply within 1 day

  • Compile abstract datatype/record
    Open
    • Is something wrong?
    enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    agda/agda2hs#471 · 1 reaction ·

    Maintainers usually reply within 1 day

  • `haskell-src-exts` currently on life support
    Open
    • Is something wrong?

    Difficulty 5/5 Over a week Newbie friendliness 25/100

    agda/agda2hs#468 ·

    Maintainers usually reply within 1 day

  • Opaque control from reflection API
    Open
    • Is something wrong?
    opaque reflection type: enhancement

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    agda/agda#8861 · 1 reaction ·

    Maintainers usually reply within 1 day

  • Control over reduction during elaboration
    Open
    • Is something wrong?
    performance type: discussion type: enhancement

    Difficulty 5/5 Over a week Newbie friendliness 25/100

    agda/agda#8860 · 4 comments · 6 reactions ·

    Maintainers usually reply within 1 day

  • Macro defined in a module does not respect parameter binding
    Open
    • Is something wrong?
    parameters reflection

    Difficulty 5/5 Over a week Newbie friendliness 15/100

    agda/agda#8844 · 1 comment ·

    Maintainers usually reply within 1 day

  • When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?
    Open
    • Is something wrong?
    injectivity type: enhancement ux: error reporting

    Difficulty 4/5 3-5 days Newbie friendliness 30/100

    agda/agda#8814 ·

    Maintainers usually reply within 1 day

  • Improve "refine" interactive command: currently fails with more than 10 arguments
    Open
    • Is something wrong?
    type: enhancement ux: interaction

    Difficulty 4/5 3-5 days Newbie friendliness 32/100

    agda/agda#8813 ·

    Maintainers usually reply within 1 day

  • Better error reporting for failed meta instantiations
    May be free again Open
    • Is something wrong?
    meta ux: error reporting

    agda/agda#8796 · 1 reaction · 1 assignee ·

    Maintainers usually reply within 1 day

  • `ClashesViaRenaming` too strict
    Open
    • Is something wrong?
    difficulty: easy import ux: warnings

    Difficulty 4/5 3-5 days Newbie friendliness 35/100

    agda/agda#8786 ·

    Maintainers usually reply within 1 day

  • Positivity checker loses information through module applications
    May be free again Open
    • Is something wrong?
    polarity positivity type: enhancement

    agda/agda#8773 · 1 comment · 1 assignee ·

    Maintainers usually reply within 1 day

  • The strict GHC backend generates code that segfaults
    Open
    • Is something wrong?
    backend: ghc ghc issue upstream

    Difficulty 5/5 Over a week Newbie friendliness 8/100

    agda/agda#8764 · 6 comments ·

    Maintainers usually reply within 1 day

  • Compare agda2hs to the GHC backend
    Open
    • Is something wrong?
    backend: ghc performance

    Difficulty 4/5 3-5 days Newbie friendliness 25/100

    agda/agda#8761 · 2 comments ·

    Maintainers usually reply within 1 day

  • Documentation: group pages in "Language Reference" by topic
    Open
    • Is something wrong?
    type: enhancement ux: documentation

    Difficulty 3/5 Half a day Newbie friendliness 35/100

    agda/agda#8760 · 1 comment · 4 reactions ·

    Maintainers usually reply within 1 day

  • Erasure-aware pattern matching
    Open
    • Is something wrong?
    erasure language change pattern matching

    Difficulty 5/5 Over a week Newbie friendliness 6/100

    agda/agda#8758 ·

    Maintainers usually reply within 1 day

  • Quality-of-life improvements to opaque
    Open
    • Is something wrong?
    opaque type: enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 30/100

    agda/agda#8757 · 3 reactions ·

    Maintainers usually reply within 1 day

  • Strange bug w/ indexed HITs in --cubical
    Open
    • Is something wrong?

    Difficulty 5/5 Over a week Newbie friendliness 8/100

    agda/agda#8753 · 3 comments ·

    Maintainers usually reply within 1 day

  • Associativity declarations for pre and post fix operators
    Open
    • Is something wrong?
    operators type: discussion

    Difficulty 5/5 Over a week Newbie friendliness 15/100

    agda/agda#8750 · 6 comments ·

    Maintainers usually reply within 1 day

  • Should we allow λ with empty `where` block as absurd lambda?
    Open
    • Is something wrong?
    absurd clauses parser type: enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 22/100

    agda/agda#8747 · 8 comments ·

    Maintainers usually reply within 1 day

  • Shiki highlighting: contribute Agda grammar
    Open
    • Is something wrong?
    type: enhancement ux: highlighting

    Difficulty 3/5 1-2 days Newbie friendliness 35/100

    agda/agda#8742 ·

    Maintainers usually reply within 1 day

  • JS backend does not check type of `main`
    Open
    • Is something wrong?
    backend: js

    Difficulty 3/5 1-2 days Newbie friendliness 45/100

    agda/agda#8741 · 1 comment ·

    Maintainers usually reply within 1 day

  • Refuse to compile unsupported `LitMeta` to JS
    Open
    • Is something wrong?
    backend: js reflection

    Difficulty 2/5 1-3 hours Newbie friendliness 56/100

    agda/agda#8735 · 1 comment ·

    Maintainers usually reply within 1 day

  • JS backend still removes some function parameters
    Open
    • Is something wrong?
    backend: js erasure projection-like

    Difficulty 4/5 3-5 days Newbie friendliness 25/100

    agda/agda#8734 · 2 comments ·

    Maintainers usually reply within 1 day

  • Cannot give in types of `variable`s
    May be free again Open
    • Is something wrong?
    generalize ux: interaction

    agda/agda#8728 · 1 assignee ·

    Maintainers usually reply within 1 day

  • Broken precondition in the termination checker
    Open
    • Is something wrong?
    debug status: MWE needed termination

    Difficulty 5/5 Over a week Newbie friendliness 22/100

    agda/agda#8721 · 2 comments ·

    Maintainers usually reply within 1 day

  • [Moderate fix] The internal type checker does not check the boundary conditions of cubical terms
    Open
    • Is something wrong?
    cubical false with

    Difficulty 5/5 Over a week Newbie friendliness 8/100

    agda/agda#8689 · 4 comments ·

    Maintainers usually reply within 1 day

  • Option `-WerrorWarningName`
    Open
    • Is something wrong?
    ux: options ux: warnings

    Difficulty 4/5 3-5 days Newbie friendliness 30/100

    agda/agda#8684 · 4 comments · 2 reactions ·

    Maintainers usually reply within 1 day

  • GS-Monoidal categories
    Open
    • Is something wrong?

    Difficulty 4/5 3-5 days Newbie friendliness 22/100

    agda/agda-categories#547 · 1 comment ·

  • Snippet causing Agda to loop
    Open
    • Is something wrong?
    Agda loops workaround exists

    Difficulty 5/5 Over a week Newbie friendliness 12/100

    agda/agda#8641 · 1 comment ·

    Maintainers usually reply within 1 day

  • Remove odd syntax from Categories.Category.Construction.Core
    May be free again Open
    • Is something wrong?

    agda/agda-categories#536 · 1 assignee ·

  • findFile'': nubOn id does not resolve symlinks, causing false AmbiguousTopLevelModuleName
    Open
    • Is something wrong?
    file system

    Difficulty 3/5 1-2 days Newbie friendliness 64/100

    agda/agda#8608 · 2 comments ·

    Maintainers usually reply within 1 day

  • When .agda and .agdai are updated on disk, highlighting is from the future
    Open
    • Is something wrong?
    ux: emacs ux: highlighting

    Difficulty 4/5 3-5 days Newbie friendliness 30/100

    agda/agda#8597 ·

    Maintainers usually reply within 1 day

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.