segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 48/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
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.
Written by the indexing model from the issue text.
Description
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)
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 23h 57m
- Merged PRs (30d)
- 264
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
bug priority: P2
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
Maintainers usually reply within 1 day
-
bug grammar sev-0
Difficulty 1/5 Under an hour Newbie friendliness 86/100
-
crash lld:MachO
Difficulty 2/5 1-3 hours Newbie friendliness 62/100
llvm/llvm-project#233265 · 1 comment ·
Maintainers usually reply within 1 day