agda

誰かが対応中かもしれないイシューは最後に並べています。 すべて日付順に表示

• Skipping compilation for up-to-date files results in mis-compilation

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 3/5 1〜2日 初心者へのやさしさ 52/100

  agda/agda2hs#486 · コメント 2 件 · 2026年11月6日 に作成

  メンテナーはふだん 1 日以内に返信

• `opaque unfolding` and `REWRITE` rules breaks subject reduction

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  confluence opaque subject reduction

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  agda/agda#8893 · コメント 4 件 · リアクション 3 件 · 2026年11月5日 に作成

  メンテナーはふだん 1 日以内に返信

• Warning that has been turned off is reported

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  PR welcome type: bug ux: warnings

  難易度 4/5 1〜2日 初心者へのやさしさ 55/100

  agda/agda#8886 · コメント 2 件 · 2026年11月1日 に作成

  メンテナーはふだん 1 日以内に返信

• 2.8.0: slow "undefined" report

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  status: MWE needed

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  agda/agda#8885 · コメント 3 件 · 2026年10月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Compare things with α-equivalence

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 3/5 1〜2日 初心者へのやさしさ 57/100

  agda/agda2hs#479 · 2026年10月27日 に作成

  メンテナーはふだん 1 日以内に返信

• Bulk hidden arguments

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  hidden arguments type: enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 24/100

  agda/agda#8872 · コメント 1 件 · 2026年10月22日 に作成

  メンテナーはふだん 1 日以内に返信

• Support type operators in rewrite rules

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 4/5 1〜2日 初心者へのやさしさ 45/100

  agda/agda2hs#473 · 2026年10月22日 に作成

  メンテナーはふだん 1 日以内に返信

• `COMPILE to` definitions from `Haskell.*` modules

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 4/5 3〜5日 初心者へのやさしさ 48/100

  agda/agda2hs#472 · リアクション 1 件 · 2026年10月22日 に作成

  メンテナーはふだん 1 日以内に返信

• Compile abstract datatype/record

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 4/5 3〜5日 初心者へのやさしさ 48/100

  agda/agda2hs#471 · リアクション 1 件 · 2026年10月22日 に作成

  メンテナーはふだん 1 日以内に返信

• `haskell-src-exts` currently on life support

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  agda/agda2hs#468 · 2026年10月22日 に作成

  メンテナーはふだん 1 日以内に返信

• Opaque control from reflection API

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  opaque reflection type: enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  agda/agda#8861 · リアクション 1 件 · 2026年10月21日 に作成

  メンテナーはふだん 1 日以内に返信

• Control over reduction during elaboration

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  performance type: discussion type: enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  agda/agda#8860 · コメント 4 件 · リアクション 6 件 · 2026年10月21日 に作成

  メンテナーはふだん 1 日以内に返信

• macOS deploy broken (macos-26-arm64, image version 20261013.0424.1)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  infra: github workflows upstream

  難易度 3/5 1〜2日 初心者へのやさしさ 20/100

  agda/agda#8845 · コメント 5 件 · 2026年10月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Macro defined in a module does not respect parameter binding

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  parameters reflection

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  agda/agda#8844 · コメント 1 件 · 2026年10月15日 に作成

  メンテナーはふだん 1 日以内に返信

• When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  injectivity type: enhancement ux: error reporting

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  agda/agda#8814 · 2026年10月6日 に作成

  メンテナーはふだん 1 日以内に返信

• Improve "refine" interactive command: currently fails with more than 10 arguments

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  type: enhancement ux: interaction

  難易度 4/5 3〜5日 初心者へのやさしさ 32/100

  agda/agda#8813 · 2026年10月6日 に作成

  メンテナーはふだん 1 日以内に返信

• Better error reporting for failed meta instantiations

  再び着手できるかも @jespercockx が 37 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  meta ux: error reporting

  agda/agda#8796 · リアクション 1 件 · 担当者 1 名 · 2026年10月1日 に作成

  メンテナーはふだん 1 日以内に返信

• `ClashesViaRenaming` too strict

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  difficulty: easy import ux: warnings

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  agda/agda#8786 · 2026年9月27日 に作成

  メンテナーはふだん 1 日以内に返信

• Positivity checker loses information through module applications

  再び着手できるかも @andreasabel が 44 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  polarity positivity type: enhancement

  agda/agda#8773 · コメント 1 件 · 担当者 1 名 · 2026年9月24日 に作成

  メンテナーはふだん 1 日以内に返信

• The strict GHC backend generates code that segfaults

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  backend: ghc ghc issue upstream

  難易度 5/5 1週間以上 初心者へのやさしさ 8/100

  agda/agda#8764 · コメント 6 件 · 2026年9月20日 に作成

  メンテナーはふだん 1 日以内に返信

• Compare agda2hs to the GHC backend

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  backend: ghc performance

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  agda/agda#8761 · コメント 2 件 · 2026年9月18日 に作成

  メンテナーはふだん 1 日以内に返信

• Documentation: group pages in "Language Reference" by topic

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  type: enhancement ux: documentation

  難易度 3/5 半日 初心者へのやさしさ 35/100

  agda/agda#8760 · コメント 1 件 · リアクション 4 件 · 2026年9月18日 に作成

  メンテナーはふだん 1 日以内に返信

• Erasure-aware pattern matching

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  erasure language change pattern matching

  難易度 5/5 1週間以上 初心者へのやさしさ 6/100

  agda/agda#8758 · 2026年9月17日 に作成

  メンテナーはふだん 1 日以内に返信

• Quality-of-life improvements to opaque

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  opaque type: enhancement

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  agda/agda#8757 · リアクション 3 件 · 2026年9月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Strange bug w/ indexed HITs in --cubical

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 8/100

  agda/agda#8753 · コメント 3 件 · 2026年9月13日 に作成

  メンテナーはふだん 1 日以内に返信

• Associativity declarations for pre and post fix operators

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  operators type: discussion

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  agda/agda#8750 · コメント 6 件 · 2026年9月12日 に作成

  メンテナーはふだん 1 日以内に返信

• Should we allow λ with empty `where` block as absurd lambda?

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  absurd clauses parser type: enhancement

  難易度 4/5 3〜5日 初心者へのやさしさ 22/100

  agda/agda#8747 · コメント 8 件 · 2026年9月10日 に作成

  メンテナーはふだん 1 日以内に返信

• Shiki highlighting: contribute Agda grammar

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  type: enhancement ux: highlighting

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  agda/agda#8742 · 2026年9月9日 に作成

  メンテナーはふだん 1 日以内に返信

• JS backend does not check type of `main`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  backend: js

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  agda/agda#8741 · コメント 1 件 · 2026年9月8日 に作成

  メンテナーはふだん 1 日以内に返信

• Refuse to compile unsupported `LitMeta` to JS

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  backend: js reflection

  難易度 2/5 1〜3時間 初心者へのやさしさ 56/100

  agda/agda#8735 · コメント 1 件 · 2026年9月7日 に作成

  メンテナーはふだん 1 日以内に返信

• JS backend still removes some function parameters

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  backend: js erasure projection-like

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  agda/agda#8734 · コメント 2 件 · 2026年9月7日 に作成

  メンテナーはふだん 1 日以内に返信

• Cannot give in types of `variable`s

  再び着手できるかも @andreasabel が 64 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  generalize ux: interaction

  agda/agda#8728 · 担当者 1 名 · 2026年9月4日 に作成

  メンテナーはふだん 1 日以内に返信

• Broken precondition in the termination checker

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  debug status: MWE needed termination

  難易度 5/5 1週間以上 初心者へのやさしさ 22/100

  agda/agda#8721 · コメント 2 件 · 2026年9月2日 に作成

  メンテナーはふだん 1 日以内に返信

• [Moderate fix] The internal type checker does not check the boundary conditions of cubical terms

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  cubical false with

  難易度 5/5 1週間以上 初心者へのやさしさ 8/100

  agda/agda#8689 · コメント 4 件 · 2026年8月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Option `-WerrorWarningName`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  ux: options ux: warnings

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  agda/agda#8684 · コメント 4 件 · リアクション 2 件 · 2026年8月25日 に作成

  メンテナーはふだん 1 日以内に返信

• GS-Monoidal categories

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 22/100

  agda/agda-categories#547 · コメント 1 件 · 2026年8月4日 に作成

• Snippet causing Agda to loop

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Agda loops workaround exists

  難易度 5/5 1週間以上 初心者へのやさしさ 12/100

  agda/agda#8641 · コメント 1 件 · 2026年7月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Remove odd syntax from Categories.Category.Construction.Core

  再び着手できるかも @JacquesCarette が 116 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  agda/agda-categories#536 · 担当者 1 名 · 2026年7月14日 に作成

• findFile'': nubOn id does not resolve symlinks, causing false AmbiguousTopLevelModuleName

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  file system

  難易度 3/5 1〜2日 初心者へのやさしさ 64/100

  agda/agda#8608 · コメント 2 件 · 2026年7月2日 に作成

  メンテナーはふだん 1 日以内に返信

• When .agda and .agdai are updated on disk, highlighting is from the future

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  ux: emacs ux: highlighting

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  agda/agda#8597 · 2026年6月13日 に作成

  メンテナーはふだん 1 日以内に返信

• A strange message about "unsolved" thing

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  meta type: enhancement ux: error reporting

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  agda/agda#8595 · コメント 1 件 · 2026年6月12日 に作成

  メンテナーはふだん 1 日以内に返信

• Make a release to match stdlib v2.4

  再び着手できるかも @JacquesCarette が 149 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  agda/agda-categories#529 · 担当者 1 名 · 2026年6月11日 に作成

• Typechecking certain parametrized modules is much slower than expected

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  modules parameters performance

  難易度 4/5 3〜5日 初心者へのやさしさ 20/100

  agda/agda#8589 · コメント 1 件 · 2026年6月10日 に作成

  メンテナーはふだん 1 日以内に返信

• Instance-search instances get inlined

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  agda/agda2hs#458 · コメント 2 件 · 2026年6月8日 に作成

  メンテナーはふだん 1 日以内に返信

• OOM with deep-matching / with(?)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  performance status: duplicate with

  難易度 4/5 3〜5日 初心者へのやさしさ 20/100

  agda/agda#8582 · コメント 2 件 · 2026年6月4日 に作成

  メンテナーはふだん 1 日以内に返信

• agda2hs cannot compile Traversable instances defined with `traverse=_`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug library

  難易度 4/5 1〜2日 初心者へのやさしさ 50/100

  agda/agda2hs#457 · コメント 1 件 · 2026年6月1日 に作成

  メンテナーはふだん 1 日以内に返信

• Inconsistency with univalence because of termination checker

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  cubical false termination type: bug univalence

  難易度 5/5 1週間以上 初心者へのやさしさ 5/100

  agda/agda#8572 · 2026年5月20日 に作成

  メンテナーはふだん 1 日以内に返信

• Proposal: allow `with` to give up

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  performance type: discussion with

  難易度 5/5 1週間以上 初心者へのやさしさ 18/100

  agda/agda#8571 · コメント 4 件 · 2026年5月20日 に作成

  メンテナーはふだん 1 日以内に返信

• Incorrect handling of simplicial sets and Kan complexes.

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  agda/agda-categories#526 · コメント 1 件 · 2026年5月17日 に作成

• Kan extension functor

  再び着手できるかも @JacquesCarette が 163 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  agda/agda-categories#525 · コメント 1 件 · 担当者 1 名 · 2026年5月17日 に作成