Owner

agda

登录后关注

已索引 5 个仓库 · 在 GitHub 查看

适合新手 全部
未关闭 全部

可能已有人在做的 issue 排在最后。 全部按时间排序

  • Builtin imports fail with "COMPILE pragma not allowed in safe mode" when the data directory's `lib` or `lib/prim` is a symlink
    未关闭
    • 哪里不对？

    难度 2/5 1-3 小时 新手友好度 72/100

    agda/agda#8897 ·

    维护者通常 1 天内回复

  • Skipping compilation for up-to-date files results in mis-compilation
    未关闭
    • 哪里不对？
    bug

    难度 3/5 1-2 天 新手友好度 52/100

    agda/agda2hs#486 · 2 条评论 ·

    维护者通常 1 天内回复

  • `opaque unfolding` and `REWRITE` rules breaks subject reduction
    未关闭
    • 哪里不对？
    confluence opaque subject reduction

    难度 5/5 一周以上 新手友好度 35/100

    agda/agda#8893 · 4 条评论 · 3 个 reaction ·

    维护者通常 1 天内回复

  • Warning that has been turned off is reported
    未关闭
    • 哪里不对？
    PR welcome type: bug ux: warnings

    难度 4/5 1-2 天 新手友好度 55/100

    agda/agda#8886 · 2 条评论 ·

    维护者通常 1 天内回复

  • 2.8.0: slow "undefined" report
    未关闭
    • 哪里不对？
    status: MWE needed

    难度 4/5 3-5 天 新手友好度 25/100

    agda/agda#8885 · 3 条评论 ·

    维护者通常 1 天内回复

  • Compare things with α-equivalence
    未关闭
    • 哪里不对？
    bug

    难度 3/5 1-2 天 新手友好度 57/100

    agda/agda2hs#479 ·

    维护者通常 1 天内回复

  • Bulk hidden arguments
    未关闭
    • 哪里不对？
    hidden arguments type: enhancement

    难度 5/5 一周以上 新手友好度 24/100

    agda/agda#8872 · 1 条评论 ·

    维护者通常 1 天内回复

  • Support type operators in rewrite rules
    未关闭
    • 哪里不对？
    enhancement

    难度 4/5 1-2 天 新手友好度 45/100

    agda/agda2hs#473 ·

    维护者通常 1 天内回复

  • `COMPILE to` definitions from `Haskell.*` modules
    未关闭
    • 哪里不对？
    enhancement

    难度 4/5 3-5 天 新手友好度 48/100

    agda/agda2hs#472 · 1 个 reaction ·

    维护者通常 1 天内回复

  • Compile abstract datatype/record
    未关闭
    • 哪里不对？
    enhancement

    难度 4/5 3-5 天 新手友好度 48/100

    agda/agda2hs#471 · 1 个 reaction ·

    维护者通常 1 天内回复

  • `haskell-src-exts` currently on life support
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 25/100

    agda/agda2hs#468 ·

    维护者通常 1 天内回复

  • Opaque control from reflection API
    未关闭
    • 哪里不对？
    opaque reflection type: enhancement

    难度 5/5 一周以上 新手友好度 35/100

    agda/agda#8861 · 1 个 reaction ·

    维护者通常 1 天内回复

  • Control over reduction during elaboration
    未关闭
    • 哪里不对？
    performance type: discussion type: enhancement

    难度 5/5 一周以上 新手友好度 25/100

    agda/agda#8860 · 4 条评论 · 6 个 reaction ·

    维护者通常 1 天内回复

  • macOS deploy broken (macos-26-arm64, image version 20261013.0424.1)
    未关闭
    • 哪里不对？
    infra: github workflows upstream

    难度 3/5 1-2 天 新手友好度 20/100

    agda/agda#8845 · 5 条评论 ·

    维护者通常 1 天内回复

  • Macro defined in a module does not respect parameter binding
    未关闭
    • 哪里不对？
    parameters reflection

    难度 5/5 一周以上 新手友好度 15/100

    agda/agda#8844 · 1 条评论 ·

    维护者通常 1 天内回复

  • When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?
    未关闭
    • 哪里不对？
    injectivity type: enhancement ux: error reporting

    难度 4/5 3-5 天 新手友好度 30/100

    agda/agda#8814 ·

    维护者通常 1 天内回复

  • Improve "refine" interactive command: currently fails with more than 10 arguments
    未关闭
    • 哪里不对？
    type: enhancement ux: interaction

    难度 4/5 3-5 天 新手友好度 32/100

    agda/agda#8813 ·

    维护者通常 1 天内回复

  • Better error reporting for failed meta instantiations
    可能重新可做 未关闭
    • 哪里不对？
    meta ux: error reporting

    agda/agda#8796 · 1 个 reaction · 已指派 1 人 ·

    维护者通常 1 天内回复

  • `ClashesViaRenaming` too strict
    未关闭
    • 哪里不对？
    difficulty: easy import ux: warnings

    难度 4/5 3-5 天 新手友好度 35/100

    agda/agda#8786 ·

    维护者通常 1 天内回复

  • Positivity checker loses information through module applications
    可能重新可做 未关闭
    • 哪里不对？
    polarity positivity type: enhancement

    agda/agda#8773 · 1 条评论 · 已指派 1 人 ·

    维护者通常 1 天内回复

  • The strict GHC backend generates code that segfaults
    未关闭
    • 哪里不对？
    backend: ghc ghc issue upstream

    难度 5/5 一周以上 新手友好度 8/100

    agda/agda#8764 · 6 条评论 ·

    维护者通常 1 天内回复

  • Compare agda2hs to the GHC backend
    未关闭
    • 哪里不对？
    backend: ghc performance

    难度 4/5 3-5 天 新手友好度 25/100

    agda/agda#8761 · 2 条评论 ·

    维护者通常 1 天内回复

  • Documentation: group pages in "Language Reference" by topic
    未关闭
    • 哪里不对？
    type: enhancement ux: documentation

    难度 3/5 半天 新手友好度 35/100

    agda/agda#8760 · 1 条评论 · 4 个 reaction ·

    维护者通常 1 天内回复

  • Erasure-aware pattern matching
    未关闭
    • 哪里不对？
    erasure language change pattern matching

    难度 5/5 一周以上 新手友好度 6/100

    agda/agda#8758 ·

    维护者通常 1 天内回复

  • Quality-of-life improvements to opaque
    未关闭
    • 哪里不对？
    opaque type: enhancement

    难度 4/5 3-5 天 新手友好度 30/100

    agda/agda#8757 · 3 个 reaction ·

    维护者通常 1 天内回复

  • Strange bug w/ indexed HITs in --cubical
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 8/100

    agda/agda#8753 · 3 条评论 ·

    维护者通常 1 天内回复

  • Associativity declarations for pre and post fix operators
    未关闭
    • 哪里不对？
    operators type: discussion

    难度 5/5 一周以上 新手友好度 15/100

    agda/agda#8750 · 6 条评论 ·

    维护者通常 1 天内回复

  • Should we allow λ with empty `where` block as absurd lambda?
    未关闭
    • 哪里不对？
    absurd clauses parser type: enhancement

    难度 4/5 3-5 天 新手友好度 22/100

    agda/agda#8747 · 8 条评论 ·

    维护者通常 1 天内回复

  • Shiki highlighting: contribute Agda grammar
    未关闭
    • 哪里不对？
    type: enhancement ux: highlighting

    难度 3/5 1-2 天 新手友好度 35/100

    agda/agda#8742 ·

    维护者通常 1 天内回复

  • JS backend does not check type of `main`
    未关闭
    • 哪里不对？
    backend: js

    难度 3/5 1-2 天 新手友好度 45/100

    agda/agda#8741 · 1 条评论 ·

    维护者通常 1 天内回复

  • Refuse to compile unsupported `LitMeta` to JS
    未关闭
    • 哪里不对？
    backend: js reflection

    难度 2/5 1-3 小时 新手友好度 56/100

    agda/agda#8735 · 1 条评论 ·

    维护者通常 1 天内回复

  • JS backend still removes some function parameters
    未关闭
    • 哪里不对？
    backend: js erasure projection-like

    难度 4/5 3-5 天 新手友好度 25/100

    agda/agda#8734 · 2 条评论 ·

    维护者通常 1 天内回复

  • Cannot give in types of `variable`s
    可能重新可做 未关闭
    • 哪里不对？
    generalize ux: interaction

    agda/agda#8728 · 已指派 1 人 ·

    维护者通常 1 天内回复

  • Broken precondition in the termination checker
    未关闭
    • 哪里不对？
    debug status: MWE needed termination

    难度 5/5 一周以上 新手友好度 22/100

    agda/agda#8721 · 2 条评论 ·

    维护者通常 1 天内回复

  • [Moderate fix] The internal type checker does not check the boundary conditions of cubical terms
    未关闭
    • 哪里不对？
    cubical false with

    难度 5/5 一周以上 新手友好度 8/100

    agda/agda#8689 · 4 条评论 ·

    维护者通常 1 天内回复

  • Option `-WerrorWarningName`
    未关闭
    • 哪里不对？
    ux: options ux: warnings

    难度 4/5 3-5 天 新手友好度 30/100

    agda/agda#8684 · 4 条评论 · 2 个 reaction ·

    维护者通常 1 天内回复

  • GS-Monoidal categories
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 22/100

    agda/agda-categories#547 · 1 条评论 ·

  • Snippet causing Agda to loop
    未关闭
    • 哪里不对？
    Agda loops workaround exists

    难度 5/5 一周以上 新手友好度 12/100

    agda/agda#8641 · 1 条评论 ·

    维护者通常 1 天内回复

  • Remove odd syntax from Categories.Category.Construction.Core
    可能重新可做 未关闭
    • 哪里不对？

    agda/agda-categories#536 · 已指派 1 人 ·

  • findFile'': nubOn id does not resolve symlinks, causing false AmbiguousTopLevelModuleName
    未关闭
    • 哪里不对？
    file system

    难度 3/5 1-2 天 新手友好度 64/100

    agda/agda#8608 · 2 条评论 ·

    维护者通常 1 天内回复

  • When .agda and .agdai are updated on disk, highlighting is from the future
    未关闭
    • 哪里不对？
    ux: emacs ux: highlighting

    难度 4/5 3-5 天 新手友好度 30/100

    agda/agda#8597 ·

    维护者通常 1 天内回复

  • A strange message about "unsolved" thing
    未关闭
    • 哪里不对？
    meta type: enhancement ux: error reporting

    难度 4/5 3-5 天 新手友好度 30/100

    agda/agda#8595 · 1 条评论 ·

    维护者通常 1 天内回复

  • Make a release to match stdlib v2.4
    可能重新可做 未关闭
    • 哪里不对？

    agda/agda-categories#529 · 已指派 1 人 ·

  • Typechecking certain parametrized modules is much slower than expected
    未关闭
    • 哪里不对？
    modules parameters performance

    难度 4/5 3-5 天 新手友好度 20/100

    agda/agda#8589 · 1 条评论 ·

    维护者通常 1 天内回复

  • Instance-search instances get inlined
    未关闭
    • 哪里不对？
    enhancement

    难度 4/5 3-5 天 新手友好度 45/100

    agda/agda2hs#458 · 2 条评论 ·

    维护者通常 1 天内回复

  • OOM with deep-matching / with(?)
    未关闭
    • 哪里不对？
    performance status: duplicate with

    难度 4/5 3-5 天 新手友好度 20/100

    agda/agda#8582 · 2 条评论 ·

    维护者通常 1 天内回复

  • agda2hs cannot compile Traversable instances defined with `traverse=_`
    未关闭
    • 哪里不对？
    bug library

    难度 4/5 1-2 天 新手友好度 50/100

    agda/agda2hs#457 · 1 条评论 ·

    维护者通常 1 天内回复

  • Inconsistency with univalence because of termination checker
    未关闭
    • 哪里不对？
    cubical false termination type: bug univalence

    难度 5/5 一周以上 新手友好度 5/100

    agda/agda#8572 ·

    维护者通常 1 天内回复

  • Proposal: allow `with` to give up
    未关闭
    • 哪里不对？
    performance type: discussion with

    难度 5/5 一周以上 新手友好度 18/100

    agda/agda#8571 · 4 条评论 ·

    维护者通常 1 天内回复

  • Incorrect handling of simplicial sets and Kan complexes.
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 25/100

    agda/agda-categories#526 · 1 条评论 ·

只显示最新的 100 条

这个页面只列出最近收录的部分。完整清单在高级筛选里，可以按语言、难度和预计耗时筛选。

前往高级筛选

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。