[fuzz-tested] segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block
Les mainteneurs répondent en général sous 1 jour
Personne n'a encore pris cette issue.
Évaluation
- Difficulté
- 4/5
- Temps estimé
- 3-5 jours
- Accessibilité débutants
- 48/100
- Type d'issue
- Bug
- Clarté
- Plutôt claire
- Activité
- Active
- Domaine
- compilers
Piste de recherche
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.
Rédigé par le modèle d'indexation à partir du texte de l'issue.
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)
- Langage dominant
- Lean
- Étoiles
- 9.8k
- Forks
- 1.1k
- Merge moyen
- 14 h 10 min
- PR mergées (30 j)
- 348
Préparer son environnement
- Aucun Dockerfile ni fichier Docker Compose
- Propose un modèle de pull request
- Lire le guide de contribution
Par où commencer
- Lisez l'issue en entier, puis le guide de contribution du projet.
- Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
- Forkez le dépôt et travaillez sur une branche.
- Ouvrez une pull request qui référence le numéro de l'issue.
Autres issues de leanprover/lean4
-
Difficulté 2/5 1-3 heures Accessibilité débutants 74/100
leanprover/lean4#15982 · 2 commentaires ·
Les mainteneurs répondent en général sous 1 jour
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePeut-être pris @treiher l’a pris il y a 15 jours. Ouvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
leanprover/lean4#15692 · 3 réactions ·
Les mainteneurs répondent en général sous 1 jour
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Ouvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 66/100
leanprover/lean4#15683 ·
Les mainteneurs répondent en général sous 1 jour
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Ouvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 70/100
leanprover/lean4#15681 ·
Les mainteneurs répondent en général sous 1 jour
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOuvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
leanprover/lean4#15674 ·
Les mainteneurs répondent en général sous 1 jour
Toutes les issues de leanprover/lean4
Issues similaires
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 85/100
rubys/roundhouse#1757 ·
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
JakeChampion/lang#14091 ·
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 77/100
povik/sv-elab#413 · 3 commentaires ·
Les mainteneurs répondent en général sous 1 jour