Unsolved goal in the middle

Stream: lean4

[Patrick Massot]

In the series of potential improvements to error reporting, it would be nice to put red squiggles under the example or theorem keyword when there is am unsolved goal in the middle of the proof. Compare:

example (x y : Nat) : x = y := by -- yellow squiggle
  calc x = x := rfl
  _ = y := sorry
  _ = y := rfl

with

example (x y : Nat) : x = y := by -- no squiggle at all
  calc x = x := rfl
  _ = y := by apply Eq.symm
  _ = y := rfl

Note this little UX inconsistency was already present in Lean 3.

[Henrik Böving]

Why red squiggles? Those usually show an error in our current UX concept right? But yellow squiggles seem sensible :thumbs_up:

[Patrick Massot]

Red squiggles would be consistent with what you get when the whole proof is incomplete. But I agree this is debatable. And any case a yellow squiggles would already be better than the current status.

[Sebastian Ullrich]

Yes, this seems very much debatable (meaning, I'm not rejecting it but would like to hear more opinions). The problem with more error/warning messages is that it's less clear which one to focus on first - and a squiggle necessarily must come with a message.

[Damiano Testa]

Would it be possible to (also) underline the sorry, when declaration uses 'sorry'?

For me, this would be an improvement: it highlights which declaration has a problem and where the problem is.