Can diagnostics be more resilient to unfinished proofs?

Stream: lean4 dev

[Dan Abramov]

I've basically trained myself to write code like this now:

Screenshot 2025-07-12 at 19.53.25.png

(Note a bunch of sorrys I put before starting to type in the middle.)

Otherwise I'm flooded with diagnostics:

Screenshot 2025-07-12 at 19.53.17.png

I wonder if there's any way to reduce the noise here?

I think I understand the reasoning (we want to make it clear which goals are unclosed) but somehow it still feels very distracting. If the diagnostics can't be more resilient to typing an unfinished proof, maybe sorrys could automatically inserted when you indent, or something?

What is the ideal user experience here?

[Dan Abramov]

Is there a downside to only reporting the diagnostic for the innermost unsolved proof(s)?

[Kevin Buzzard]

FWIW I have also trained myself to write code like that now (and I did this many years ago)

[Dan Abramov]

Another example of a similar issue.

I have to do this:

Screenshot 2025-07-13 at 00.27.28.png

Otherwise the parser just chokes:

Screenshot 2025-07-13 at 00.27.36.png

Can the parser be modified to understand that I'm probably going to type at the indentation?

[Dan Abramov]

I guess maybe my feature request is to treat

  constructor
  ·
  -- ...

analogous to

  constructor
  · {}
  -- ...

and

  have : y = g (Function.invFun g y) := by

  -- ...

analogous to

  have : y = g (Function.invFun g y) := by
    {}
  -- ...

So, assume there's an implicit empty block there.

[Joachim Breitner]

That would be https://github.com/leanprover/lean4/issues/3555, I think

[Dan Abramov]

Related, this is just as annoying with fun:

Screenshot 2025-07-16 at 18.42.06.png

I can't see any context because the parser dies.

[Johan Commelin]

But if you add the , will it come back to life?

[Dan Abramov]

Nope

Screenshot 2025-07-17 at 14.18.34.png

[Dan Abramov]

In general non-tactic mode feels like second class citizen, e.g. let bindings don't display in InfoView

Screenshot 2025-07-17 at 14.33.06.png

[Damiano Testa]

I find that underscores _ "capture" more: does , _ get you in a better state?

[Damiano Testa]

Do you get the let if you move the cursor further away?

[Damiano Testa]

I have noticed that in some situations, something does not show up in the infoview at a position where it should, but it does show if I move to the next "relevant" position.

[Dan Abramov]

Ah yeah you're right. It shows up at the beginning of the next non-empty line.

And yes _ does help for parsing.

[Damiano Testa]

I do not know why sometimes the infoview does not show something that it should, but I have noticed it quite often.

[Dan Abramov]

Actually _ or sorry at the end is not even a good workaround because the last expression may consume it.

Screenshot 2025-07-17 at 21.03.30.png

Screenshot 2025-07-17 at 21.03.38.png

So this is just.. kinda borked.

[Dax Fohl]

Is it just that the span is too long? Python does the same, but the squigglies are mostly limited to a single word or character:
image.png

[Dan Abramov]

My main problem is the InfoView being effectively broken.

In Python, there's nothing like the InfoView to guide you writing code, whereas in Lean it's pretty essential to see the current proof state to know what to write next. So parser errors during the general writing flow (at least after every line) are IMO unacceptable if they break the InfoView.

[Dan Abramov]

To be fair, InfoView doesn't get borked as much anymore, i.e. during a theorem it still works (despite the diagnostics being overly noisy).

But in the last case I showed (inside a function definition), it does actually break completely.

[Dan Abramov]

Is it just that the span is too long?

It's not just that. It's that it misdiagnoses the problem and highlights valid lines.

This is misleading — the next line is fine:

Screenshot 2025-07-19 at 16.56.57.png

The next line shouldn't lose syntax highlight because of this.
Instead it should behave like this:

Screenshot 2025-07-19 at 17.00.50.png

Similarly, I find this to be very misleading:

Screenshot 2025-07-19 at 17.01.27.png

There's no problem with the rintro line! The problem is the proof is unfinished. Again, I think it should behave like this instead:

Screenshot 2025-07-19 at 17.02.09.png

Show me unfinished goals at the place where it's actionable. Unsolved goals are actionable when you've stopped trying to prove them, not where they're declared.

[Dan Abramov]

One litmus test is — when you see a squiggle, does the squiggle highlight the place that is broken and needs to be edited. If it doesn't (and in the vast majority of Lean diagnostics today, it doesn't) — the squiggle needs to be moved to the place that actually needs to be fixed.

[Dan Abramov]

Sometimes there's ambiguity there (e.g. "is the goal wrong or is the proof incomplete"), just like with types, so I understand it may be more delicate than I'm describing. But as a user, I am certainly feeling that I can't trust the squiggles in Lean the same way I trust them in TypeScript etc. It's just always highlighting the wrong place for the fix and it's very annoying.

[Kyle Miller]

The empty cdot problem is issue lean4#3555, and there's also lean4#4181

[Kyle Miller]

I'm not sure I understand what #lean4 dev > Can diagnostics be more resilient to unfinished proofs? @ 💬 is demonstrating. What does putting sorry after a term meant to do? That's passing sorry as an extra argument to the previous term

[Dan Abramov]

Right, I'm just trying to do anything to fix the parsing error so that the InfoView starts working again. I agree it doesn't make sense to put sorry there but I'm not sure how else to unbreak the InfoView.

[Dan Abramov]

Basically I need InfoView to work at all times while I'm writing a new line of code. It can't disappear because I rely on it in writing.

[Kyle Miller]

What was broken with the infoview in that case? That's what I'm missing. Without the sorry it looks like it's parsing correctly.

[Dan Abramov]

I start typing. The quantifier breaks the InfoView:

Screenshot 2025-07-19 at 17.12.39.png

I want to fix it so I know what to type. So I add a sorry to kick the parser:

Screenshot 2025-07-19 at 17.14.16.png

Then I forget about that sorry and keep typing. So now I have an extra sorry.

Of course I can remove that sorry now...

Except now InfoView breaks again:

Screenshot 2025-07-19 at 17.14.54.png

So I add the sorry back and later I'll again forget to remove it. Et cetera.

[Dan Abramov]

I think the design constraint here should be something like "the InfoView is never allowed to disappear if the parsing error is local to a single line and wouldn't break the entire document". You need to be able to trust that this thing sticks around.

[Kyle Miller]

Dan Abramov said:

There's no problem with the rintro line!

Yeah, this error position is quite annoying. A little background here: the entire focus dot proof has an error associated to it, but there's a heuristic that the error range is restricted to just the first line. It looks like it's complaining about rintro, but that's just because it's part of the first line. It used to highlight the entire subproof, which wasn't very usable.

Maybe part of lean4#3555 is to have a parser at the end of a tactic sequence that's just looking for a blank line with enough space to make it to the expected column.

I wonder though: if that blank line isn't there, the natural place for the "unsolved goals" error is back at the focus dot. Would it be confusing if the error jumps from the focus dot to the end of the subproof by virtue of hitting enter then tab?

[Dan Abramov]

Is there a downside to placing it at the last line of the (incomplete) proof instead? Basically, put the squiggle at the place that, when I focus on it, has an "abandoned" goal that's pending more work.

[Kyle Miller]

Dan Abramov said:

You need to be able to trust that this thing sticks around.

I don't think you should feel like you need to put much energy into convincing anyone that this should be the goal! We definitely want that to be the case. (Did you look at lean4#4181 yet? That's the issue recording this. Feel free to weigh in there.)

[Kyle Miller]

Dan Abramov said:

Is there a downside to placing it at the last line of the (incomplete) proof instead?

Do you mean that it should blame the last tactic for not completing the subproof?

[Dan Abramov]

Yup yup, I think it has actually drastically improved since the last time I complained about it! It's much better in tactic mode, but in the term mode it's still flaky.

[Dan Abramov]

Do you mean that it should blame the last tactic for not completing the subproof?

That would be my intuition, yeah.

[Kyle Miller]

Dan Abramov said:

Yup yup, I think it has actually drastically improved since the last time I complained about it! It's much better in tactic mode, but in the term mode it's still flaky.

I don't remember there being any changes, so unfortunately it might be that you're getting used to it :upside_down:

[Dan Abramov]

I don't remember there being any changes, so unfortunately it might be that you're getting used to it 

Actually you might be right... I realize that I now just type rintro \<a, b, c\> without looking and then drill down into a, b, and c separately, etc.

[Kyle Miller]

Re parsing errors: the parsing error recovery isn't particularly robust; e.g. it doesn't try very hard to re-sync. There's some limited support where missing terms can be skipped and parsing continues.

What's really hit-or-miss is that the elaborators aren't all very error-tolerant. The let elaborator can handle a missing body, but the Exists elaborator can't. That means in the first case you get an infoview, but in the second case you don't.

[Kyle Miller]

(I might be wrong about Exists, I'd have to check actually. It's just that many elaborators are defined as macros, and the syntax matches tend to require complete-ish syntax. The let elaborator I know for sure doesn't use syntax matches, instead indexing into the syntax objects directly to get different components.)

[Dan Abramov]

Another option is to make InfoView slightly "stateful" so it remembers the last successful state (and displays pending errors). But as you surely know, this can also lead to highly unintuitive and frustrating experiences.

[Kyle Miller]

Maybe you're right about having tactic sequences blame the last tactic in a sequence for not finishing a proof. That would be a good first approximation, and the cherry on top could be to blame the whitespace right after that line if there's a blank line with enough spaces.

There's also the project to go through the parsers and elaborators systematically and make them more tolerant to errors, and to be able to resynchronize in some intelligent way. The main resynchronization is the top-level command parser, which on failure starts consuming tokens until a command parses again.

[Dan Abramov]

I wonder if there's anything that can be done at a higher level that doesn't require all pieces to "be smart", especially when so much syntax is user-programmable.

E.g. I wonder if InfoView could show the state for the program "excluding" the broken block if some block is broken, or something like that. Usually that's good enough and better than nothing?

[Kyle Miller]

Something that Python does that Lean doesn't is that Python has two parsers: one for the happy path, and another to go through again and try to diagnose parsing errors. Sometimes I wonder what we might be able to do if we had such a system. Right now we do add some incorrect parses here and there into the grammar so that something smarter can happen at elaboration time. One example that comes to mind is trailing dots in identifiers (a.b.) which then is used to trigger completions.

[Kyle Miller]

Some internals for you: during elaboration, each bit of syntax can be annotated with some ElabInfo, including one kind of ElabInfo called TermInfo. The TermInfo is thus already nested, or even overlapping. The LSP has heuristics to decide which TermInfo to use at a particular cursor point to then create the "Expected Type" view, with the local context and the expected type at that point.

Tactics create TacticInfo, which records the before/after goal lists rather than an expected type, but it's similar. (E.g. the entire focus dot syntax, including all the contained tactics, gets a TacticInfo covering the entire block, as do each of the individual contained tactics.)

With your idea about excluding TermInfo for broken syntax, I worry that this would easily go up too far, and not show you the closer of the TermInfo that you want to see. Think about let with a missing body: it's broken, but you've said you want to be sure you see the scope for the body of the let.

[Dan Abramov]

Something that Python does that Lean doesn't is that Python has two parsers: one for the happy path, and another to go through again and try to diagnose parsing errors

This sounds like maybe similar to what C# (Roslyn) is doing? I don't have any domain knowledge there so don't know what SOTA is and how far Lean is from it, but my impression is that both C# and TypeScript are pretty good at parser error recovery these days.

[Kyle Miller]

Part of the deal is that Lean's grammar is extensible, using a parser combinator approach rather than a hand-written recursive-descent parser, and it also doesn't use a parser generator (here's Python's grammar, and an explanation in the reference). Python uses a PEG grammar, and you can see there are a whole lot of "invalid" rules.

That said, it's plausible for there to be a metaprogram that generates an error recovery version of each parser (there could be annotations for alternatives that are specifically for error recovery that are stripped out for the main parser). It seems tricky though, since you need to make sure that the error recovery parser still parses correct programs correctly, but a benefit is that you can match on common mistakes and explain the issue in the error message, and also decide to commit to certain parses that you might not want to commit to normally, for sake of error recovery.

[Dan Abramov]

Maybe you're right about having tactic sequences blame the last tactic in a sequence for not finishing a proof. That would be a good first approximation, and the cherry on top could be to blame the whitespace right after that line if there's a blank line with enough spaces.

How much work would it be to prototype this?

[Kyle Miller]

For a prototype that affects just cdot blocks, you'd need to modify Lean.Elab.Tactic.evalTacticCDot to instead of using withCaseRef, use withRef and the last tactic in the sequence, I believe.

[Dax Fohl]

I was playing with the parser last week. It does seem to do two passes, as any traces I add will get hit twice (usually). I think that's managed by leadingParser and trailingLoop here. Though I am still trying to figure it all out, and not sure if that's what you mean above by two passes.

[Dax Fohl]

The main struggle while trying to ramp up on it though has been the dev loop. So far it's been "play with Lean in VSCode, look at info panel for a unique-looking message, copy the text, search for it in lean source, try to back trace it to a plausible call point, add a trace log there to see if that's what's calling it, recompile, wait, go back to Lean in VSCode, reload, see if the trace showed up, repeat", and so on up the stack. So if there's a faster way to iterate on things like that, it'd be good to know.

[Niklas Halonen]

Dan Abramov said:

Is there a downside to placing it at the last line of the (incomplete) proof instead? Basically, put the squiggle at the place that, when I focus on it, has an "abandoned" goal that's pending more work.

Let's say we have an incomplete proof ending in a subproof, e.g. suffices ... by, the error span would be the last line under the suffices, which to me seems misleading. To demonstrate:

example : 1 - 1 < 1 := by
  suffices 1 - 1 = 0 by
    rw [this]
    exact Nat.zero_lt_one -- the error span is here and this line would be red

One option could be to somehow have the error indicate the indentation depth and have maybe a little red triangle there to indicate whether it's the main proof or subproof which is incomplete. However, I don't think current diagnostic tools have support for this (or at least I've never seen it myself).

[Kyle Miller]

That's a good example to keep in mind. I was think "last line" would be "first line of the last tactic in a tactic sequence". It's suffices that's the reason for the main by not being complete.

[Dan Abramov]

I was think "last line" would be "first line of the last tactic in a tactic sequence". It's suffices that's the reason for the main by not being complete.

Yeah, that's a good clarification. And, if there's an empty line with some indentation after, ideally the squiggle would move to it.

[Dax Fohl]

In other language plugins, I've found it more common that type hints are inlaid rather than showing up in a side view that follows the cursor. Would it be possible / desirable to do something similar here, where the remaining goal is inlaid after each line? (assuming the completed section above the cursor is resilient to parse errors below it and doesn't stutter the whole screen as you type). Or is the goal state of the previous line not usually that useful if you're in the middle of typing something? Does the LSP return enough info to make that possible?

[Dax Fohl]

In terms of recovery, here's the behavior in the C# plugin. In the first case it looks like it can recover within the current function; it deletes the type inlays of the things that it can't figure out, and leaves the rest. Then when the error is fixed, it recalculates the type in the background (leaving the inlay as "...") and adds it when it's finished. In the second case it looks like it can't recover the current function, so it just grays everything below the error point out, but leaves the type hint inlays as they were. Would this be useful behavior to mimic?

ScreenRecording2025-07-21at5.41.16PM.gif

[Marc Huisinga]

Here's the existing proposal for better diagnostic ranges in unfinished proofs, but it's different from the one suggested in this thread: lean4#8919
I think that both proposals are reasonable. Note that you won't be able to implement either one as-is because we definitely want the fullRange of the error to be the full block (which our messages currently aren't capable of), so there are some more architectural changes required. I'll definitely look into this at some point. It will also require some adjustments to our custom diagnostic decorations in the extension.

[Kyle Miller]

@Marc Huisinga For being able to put errors into the whitespace, I wonder if tacticSeq could end in a special parser that doesn't consume characters, but instead steals some of the whitespace of the last tactic if it starts with a newline indented to the current savedPos? That would support multiple levels of indentation, since each dedent would give an opportunity to steal the next bit of whitespace. (I'm sure you've got your own ideas here, given all the work you've done with diagnostics in whitespace.)

[Marc Huisinga]

I think I still like the idea of putting the squiggly exclusively on the symbol that introduces the block more at this point for those reasons :-)
We've already got the unsolved goals symbol to mark the "end" of the block without having to attach it to any specific symbol in the code, after all.

[Dan Abramov]

I like the conceptual simplicity of moving it to “by” but what’s the intended workflow when coming back to a broken proof? Ideally I want to avoid the need to glance “up and down”. More concretely, I want the mental operation of “deciding where to put the cursor” to be O(1).

[Marc Huisinga]

Does the unsolved goals symbol not provide that information?

[Dan Abramov]

Ahh, the "tools" icon means "unsolved goals"? I would've never guessed that!

When I first noticed it a couple of weeks ago (while making screenshots for this thread), I assumed it's a VS Code bug or some kind of a linter autofix prompt that wasn't working. I didn't make any connection to unsolved goals. It looked like the kind of thing you'd press to get linter suggestions — except that hovering it didn't give any hint about what it is. The "tools" icon generally evokes "settings" but pressing it also didn't do anything. So I stopped guessing what it is then and forgot about it.

I've actually had to take a few seconds now to notice it in my code — apparently I haven't noticed it even once since those two weeks ago. I presume my brain has learned to completely tune it out because I didn't understand its purpose.

[Dan Abramov]

I do like the idea of this marker. But I think:

• "Tools" is a completely wrong metaphor for it — the icon needs to be something else
• It must have a hover state that explains what it is and/or shows the actual goals

Otherwise it comes across as noise or a bug

[Dan Abramov]

It's also just hard to notice in the first place because it has so much less visual "weight" compared to the actual "error". So it's hard to notice and hard to imagine that it has something to do with the red thing.

Screenshot 2025-07-25 at 20.28.22.png

[Dan Abramov]

I guess the "error lens" extension is my own choice and maybe that shouldn't be taken into consideration. If we assume people don't have it on then the current behavior is this:

Screenshot 2025-07-25 at 20.41.40.png

If I correctly understand it, your proposed change would turn it into this:

Screenshot 2025-07-25 at 20.42.08.png

Which makes me wonder, what about something like this?

Screenshot 2025-07-25 at 20.42.08.png

So, replacing the "tools" marker with an actual statement of the unsolved goal.

[Marc Huisinga]

Dan Abramov said:

• "Tools" is a completely wrong metaphor for it — the icon needs to be something else

Happy to hear about potential alternatives. Due to VS Code limitations, it has to be an emoji (or text); we can't put a custom .svg there.

Dan Abramov said:

• It must have a hover state that explains what it is and/or shows the actual goals

I wish it was, but this is unfortunately not possible due to VS Code limitations.

See vscode-lean4#585.

Dan Abramov said:

It's also just hard to notice in the first place because it has so much less visual "weight" compared to the actual "error".

I think this is in part due to the fact that you are using the Error Lens extension, which highlights the entire line :-)

Dan Abramov said:

So, replacing the "tools" marker with an actual statement of the unsolved goal.

Most Lean goals are far too large in practice to render them in an editor decoration.

[Dan Abramov]

Right, I guess I was assuming that the Lean plugin could use a similar approach for this marker as the Error Lens extension does? (Maybe that's a wrong assumption)

I think I enabled Error Lens because some Lean tutorial encouraged it. I'll probably turn it off for myself.

[Marc Huisinga]

I personally think that the Error Lens extension (both the red line background and the squashed text after it) are too noisy to enable them by default in the Lean extension. This is essentially why we have the error markers on the left (the cross and the line are a Lean feature!) as a less noisy alternative that also provides more context than Error Lens, namely where the full range of the error ends.

[Patrick Massot]

The error lens extension used to be completely essential for Lean use, but Marc’s recent work made it much less crucial, and even maybe harmful.

[Kyle Miller]

(I don't remember if you considered :construction: @Marc Huisinga. It might give somewhat more of a construction site feel than :working_on_it:, though Zulip calls :working_on_it: "working on it" and it makes enough sense.)

[Patrick Massot]

Dan, the standard description of :working_on_it: on this zulip is “working on it”. It is the way you type it and the way it is used here.

[Patrick Massot]

So in the VSCode extension it means: you still have work to do here.

[Patrick Massot]

I’m not saying we can’t find a better one, only explaining the rational.

[Patrick Massot]

I don’t know universal is this “working on it” description.

[Marc Huisinga]

(I sympathize with the point that it's a bit obscure without the hover though. I really wish the editor decoration API was capable of this.)

[Marc Huisinga]

Dan Abramov said:

If I correctly understand it, your proposed change would turn it into this:

For by, it will look the same way as it does now. But in your dot case example, it will put a squiggly under the dot instead of the full line with the rintro tactic, so that it won't suggest that something is wrong with the tactic anymore.

[Dan Abramov]

I see. I think that's a pretty unorthodox name for this icon. (Seems like it's just "hammer and wrench" in Unicode?) Maybe familiar to Zulip users but not very discoverable or clear to someone who wasn't already taught that.

I agree Error Lens seems like maybe a poor recommendation at this point. I'm not sure where I saw it. I thought either Kevin's course or MIL but can't find it there either. Maybe it's safe to assume most beginners won't have that.

I didn't realize the left pane is already custom. If we have control over it, then I don't see much point in the emoji decoration. Maybe left pane could just be a bit clearer about what's going on? Could we do more custom stuff there?

IMO the most intuitive icon for "unfinished goal" would just be the goal icon. So if we have more control over the left pane, maybe something like this would make sense?

Screenshot 2025-07-25 at 20.42.08.png

[Patrick Massot]

I don’t remember whether we mention error lens in MIL, but it may very well be the case. Do you know this extension is very configurable?

[Patrick Massot]

I checked and the word lens does not appear in the source of MIL.

[Patrick Massot]

So we won’t have to decide whether to remove it or not.

[Dan Abramov]

OK I think a lot of my beef was actually with Error Lens. It's not as distracting without it. And if the squigglies are also slightly reined in, it would be a further improvement.

The "working on it" icon feels like pure noise to me now since it's duplicating the information in the left pane.

Screenshot 2025-07-25 at 21.08.31.png

If the left pane is always as clear as in this screenshot (note that's not always true — earlier examples in this thread showed it's sometimes very noisy with multiple circles) I think that would be enough.

[Dan Abramov]

However, if you don't have sorry at the end, the left pane is red for the entirety of the proof and that makes it sort of useless.

Screenshot 2025-07-25 at 21.11.38.png

I wonder if that specific pattern could be improved.

[Marc Huisinga]

Dan Abramov said:

IMO the most intuitive icon for "unfinished goal" would just be the goal icon. So if we have more control over the left pane, maybe something like this would make sense?

The reason for why we put it at the end of the line is two-fold:

1. It's closer to the idea of "this is where you should continue typing" than a decoration on the left (also known as "the gutter" in VS Code). It's still not optimal in this regard, since you'd really like it to be on the next empty line in multi-line blocks, but this is quite tricky for complicated technical reasons.
2. Each icon on the left side should interact nicely with other icons on the left side. If there is both an error and the end of an unsolved goals error on that line, which icon should we display? Having it on the right automatically disambiguates this.

We could have ⊢ instead of :working_on_it:. I vaguely remember rejecting it for some reason, perhaps because it blended into the text too easily, since it is just a regular Unicode symbol. I don't remember exactly.

Dan Abramov said:

The "working on it" icon feels like pure noise to me now since it's duplicating the information in the left pane.

Note that the design language in the left pane isn't entirely unambiguous when there are multiple overlapping error ranges, but it's the best I could come up with given the limited space in the gutter. Removing the unsolved goals symbol would certainly make it harder to spot the end of an "unsolved goals" range in this case, but also in general because you first have to identify the bend to the right as being one from an "unsolved goals" error at the top.

Dan Abramov said:

However, if you don't have sorry at the end, the left pane is red for the entirety of the proof and that makes it sort of useless.

Well, there's an error spanning from the first by all the way to the end of the block in this case after all, so that's what the gutter decorations display :-)

[Dan Abramov]

I see. I guess the question is — what's the recommended workflow when typing? Do you want to encourage people to type sorry ASAP to make the left gutter useful? Because if they don't, it's perpetually in a state where multiple things will overlap. I understand that technically they "should" overlap because you "do" have a range error, but for me that's an argument to not treat it as a range.

[Dan Abramov]

This, while losing the "range" information, feels more immediately useful to me:

Screenshot 2025-07-25 at 21.14.12.png

Because it accurately portrays the actionable points.

[Dan Abramov]

Another argument against ranges is that as soon as you have >1, the nesting looks so confusing that it doesn't convey the actual ranges anymore anyway. It feels like multiple overlapping ranges should be a corner case, but right now that's the default behavior unless you always add sorrys.

[Marc Huisinga]

I think the "unsolved goals" error is fairly unique in the sense that only its start line and its end line are relevant. For most other errors that span multiple lines, I don't think this holds - you really want a signal that a line is part of an error, and the fact that an error range ends at a line is secondary information.

Could you clarify again why the :working_on_it: symbols aren't sufficient for unsolved goals errors in particular? You stated that they duplicate the information on the left, but I don't think they do, and I believe that they express the position where you should continue typing more nicely than a decoration in the gutter.

[Dan Abramov]

I agree "unsolved goals" is special. Partially because, like you said, only the first and the last lines are relevant. Partially because it's expected that the space between them will likely keep expanding (and so the range will likely get longer and nested). And partially because unlike many other errors, this one is "expected" while you're typing. So it's bad if it distracts you from... typing.

I see your point about decorations. Maybe you're right. I don't feel like :working_on_it: conveys what it's doing, so I'm not sure if other users broadly understand what it is. I see your point re: goal indicator maybe blending in too much. (I'm not sure if you can choose the color or font there btw?) It is hard for me to offer alternatives for without actually playing with a real setup and plugging different options.

[Dan Abramov]

To sum up my complaints at this point, it would be that the :working_on_it:s are too hard to visually scan for when the entire gutter panel is shouting at me with red lines (and 90% of the area these red lines cover have no errors). So :working_on_it: are informative but hard to see, and the gutter is not informative but is in my face.

[Dan Abramov]

Also, just having three sources of information (gutter, squiggles, and :working_on_it:s) that aren't quite conveying the same thing (but are somewhat related) feels like a lot. My eyes keep darting between them whenever something changes.

[Dan Abramov]

I still feel like whatever the outcome, I'll just keep adding sorrys manually so that I can stay focused on actual, real errors — and not have my attention destroyed by screaming red lines. Which is maybe fine. But then I wish the tooling just embraced that. E.g. insert sorry for me or something.

[Marc Huisinga]

You can choose a font, font weight, color, background color, etc. The problem with the background color one is that it will end up looking a bit weird since the bounding box is not a square.

Ultimately, I think that using \vdash (no matter where) for an unsolved goal might also be pretty confusing to some people, so perhaps that's part of why I rejected it :-)

Dan Abramov said:

I'll just keep adding sorrys manually so that I can stay focused on actual, real errors — and not have my attention destroyed by screaming red lines.

I think this depends entirely on whether you're trying to find errors in your code at a glance or whether you're editing and just want to proceed at the moment. I certainly operate in both of these "modes" at different times while working on code. In a modal editor, I'd probably even explicitly distinguish the two in terms of how we display diagnostics.
We introduced the red lines and the other gutter decorations because students kept missing squigglies in their code when they were looking for errors, and also because the squiggly isn't necessarily an accurate depiction of the range of the error, even outside of "unsolved goals". Certainly, covering the editor in squigglies is also not a reasonable option.

RE: Displaying different kinds of diagnostic when editing vs browsing like would be possible in a modal editor, I do have some ideas for adding an optional purely client-side mode to vscode-lean4 at some point that allows switching between these two modes with a shortcut without it affecting the actual editing experience, only diagnostics and the InfoView, so that there is less flickering and noise while you're editing. It's not that far up on my endless backlog, though :-)

[Patrick Massot]

Yes, using a modal editor is indeed better.

[Patrick Massot]

And, Dan, most people write sorry very often, and I think you already asked this question not long ago.

[Damiano Testa]

I also constantly add sorrys and focusing dots: I am always very suspicious of what lean tells me, when there are errors around.

[Dan Abramov]

Patrick Massot said:

And, Dan, most people write sorry very often, and I think you already asked this question not long ago.

Yea I don't have much to add here without going in circles. I want to clarify that I'm not asking about customizations for myself, I'm just saying the default experience (and it's the default experience I care about) of writing Lean code feels (to me) worse than the default experience of writing Python, TypeScript, or most other modern languages with IDE integration, and the reason it feels worse is because during the natural course of writing (left to right, top to bottom), the IDE integration is "more paranoid" (highlighting things in red, adding squigglies) than other languages — calling attention to "issues" that aren't actual issues and are expected in the process of writing. Maybe I'm "holding it wrong" and this is best "fixed" by writing "not exactly top down" and adding sorrys whenever I indent. But again, this reminds me of how modern language integrations automatically insert matching curlies, or recover more gracefully from incomplete lines, etc.

If I can use a math metaphor, imagine taking an integral over the cumulative amount of noise as you type a proof top to bottom and left to right, where noise is defined as red lines and squiggles that don't actually demand switching attention to them (with extra noise "points" for squiggles and red lines that are downright misleading, i.e. failing to parse). Then compare the amount of noise to a similar integral taken over writing a TypeScript function. Then maybe there is something actionable there — I think reducing that cumulative amount "as you type" is a good idea, with attention paid to what happens at every single keystroke. That's all I was trying to say.

[Mario Carneiro]

Marc Huisinga said:

We could have ⊢ instead of :working_on_it:. I vaguely remember rejecting it for some reason, perhaps because it blended into the text too easily, since it is just a regular Unicode symbol. I don't remember exactly.

Bad idea. Imagine if the last tactic was simp at h and you stuck a faded ⊢ after it...

[Marc Huisinga]

Dan Abramov said:

I want to clarify that I'm not asking about customizations for myself, I'm just saying the default experience (and it's the default experience I care about) of writing Lean code feels (to me) worse than the default experience of writing Python, TypeScript, or most other modern languages with IDE integration, and the reason it feels worse is because during the natural course of writing (left to right, top to bottom), the IDE integration is "more paranoid" (highlighting things in red, adding squigglies) than other languages — calling attention to "issues" that aren't actual issues and are expected in the process of writing.

I suspect that part of the reason for this is also just that some of these issues are a bit harder in Lean than in other languages (e.g. due to Lean's extensibility, or due to the fact that practically everything is just some sort of nested expression). For example, here's the kind of diagnostic highlighting I get in TypeScript when there's a type error in a larger expression:
image.png
I don't think this is great, either :-)

(To be clear, I still definitely agree with your points that we could and should do much better in regards to error recovery and where errors are reported in plenty of examples.)