segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block
I maintainer di solito rispondono entro 1 giorno
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 48/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Attiva
- Ambito
- compilers
Direzione di ricerca
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.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
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)
- Lingua principale
- Lean
- Stelle
- 9.6k
- Fork
- 1.1k
- Merge medio
- 1g 4h
- PR unite (30g)
- 290
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di leanprover/lean4
-
`IO.appPath` fails when `/proc` belongs to another PID namespaceForse già presa @treiher l’ha presa 2 giorni fa. Apertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
leanprover/lean4#15692 · 3 reazioni ·
I maintainer di solito rispondono entro 1 giorno
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Apertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 66/100
leanprover/lean4#15683 ·
I maintainer di solito rispondono entro 1 giorno
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Apertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 70/100
leanprover/lean4#15681 ·
I maintainer di solito rispondono entro 1 giorno
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
leanprover/lean4#15677 ·
I maintainer di solito rispondono entro 1 giorno
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupApertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
leanprover/lean4#15674 ·
I maintainer di solito rispondono entro 1 giorno
Tutte le issue di leanprover/lean4
Issue simili
-
generated by fuzzer llvm:transforms miscompilation
Difficoltà 2/5 1-3 ore Idoneità per principianti 68/100
llvm/llvm-project#234047 ·
I maintainer di solito rispondono entro 1 giorno
-
area:codegen backend:hlsl bug coverage direction:output
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
WebAssembly/spec#2284 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
ProvableHQ/leo#29657 ·