VS Code lightbulb bug

Stream: lean4

[Martin Dvořák]

import Mathlib.Data.Real.Basic

example (P Q : Prop) (hyp : P ∨ Q) : False :=
by
  cases hyp
  sorry

Now I press Quick Fix:
image.png

import Mathlib.Data.Real.Basic

example (P Q : Prop) (hyp : P ∨ Q) : False :=
by
  cases hyp with
  | a => sorry
  | b => sorry
  | inl h => sorry
  | inr h => sorry
  sorry

The generated code isn't desirable.

[Patrick Massot]

This is a recent bug. I can reproduce on Mathlib master but not in MIL.

[Patrick Massot]

And it has nothing to do with Mathlib:

import Std.CodeAction

example (P Q : Prop) (hyp : P ∨ Q) : False :=
by
  cases hyp
  sorry

[Martin Dvořák]

Thanks for the minimization! I didn't know what the necessary import was.

[Martin Dvořák]

FYI it seems to be fine on the newest toolchain.

[Eric Wieser]

Still broken for me in the web editor

[Eric Wieser]

The lightbulb on the sorry works, but not on the cases

[Mario Carneiro]

this is fixed on master

[Mario Carneiro]

std master, not mathlib master

[Scott Morrison]

Dependency bump incoming at #7393, looks promising locally.