segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block
メンテナーはふだん 1 日以内に返信
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 48/100
- issue の種類
- バグ
- 明瞭さ
- おおむね明確
- 活発さ
- 活発
- 領域
- compilers
調査の方向性
Start with the reproducer in the issue and inspect how @[try_suggestion] handles suggester declarations inside a mutual block, especially when a type gains section variables. Run the reproducer to confirm the segfault, then trace the relevant elaboration or registration path. Done means the example completes without a segfault and the suggestion behavior remains correct; the issue names no source file or test.
索引モデルが issue の本文から書いたものです。
説明
The following code:
import Lean.Elab.Tactic.Try
open Lean Meta Elab Tactic
opaque P : Prop
axiom p : P
variable {α : Type} [Inhabited α]
mutual
def usesVar : α := default
@[try_suggestion]
def sugg (goal : MVarId) (_ : Try.Info) : MetaM (Array (TSyntax `tactic)) := goal.withContext do
let term ← PrettyPrinter.delab (mkConst ``p)
return #[← `(tactic| exact $term)]
end
example : P := by try?
Resulted in this output:
Segmentation fault (core dumped) (exit code 139)
- 主要言語
- Lean
- スター
- 9.6k
- フォーク
- 1.1k
- 平均マージ
- 1日 35分
- マージ済み PR（30日）
- 269
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
leanprover/lean4 のほかの issue
-
`IO.appPath` fails when `/proc` belongs to another PID namespace対応中かも @treiher が 1 日前に担当しました。 オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
leanprover/lean4#15692 · リアクション 3 件 ·
メンテナーはふだん 1 日以内に返信
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 66/100
leanprover/lean4#15683 ·
メンテナーはふだん 1 日以内に返信
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 70/100
leanprover/lean4#15681 ·
メンテナーはふだん 1 日以内に返信
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 76/100
leanprover/lean4#15677 ·
メンテナーはふだん 1 日以内に返信
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupオープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
leanprover/lean4#15674 ·
メンテナーはふだん 1 日以内に返信
leanprover/lean4 の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
swc-project/swc#12576 ·
メンテナーはふだん 1 日以内に返信
-
bug priority: P2
難易度 1/5 1〜3時間 初心者へのやさしさ 84/100
メンテナーはふだん 1 日以内に返信
-
documentation stdlib
難易度 2/5 1〜3時間 初心者へのやさしさ 67/100
メンテナーはふだん 1 日以内に返信
-
clang:static analyzer
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
llvm/llvm-project#233598 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信