Can Lean InfoView be more resilient to unfinished lines?

Stream: general

[Dan Abramov]

I'm relatively new to Lean but if I may complain about something, the experience of typing the line while trying to resolve the goal is very distracting and somewhat unpleasant.

notfun.mov

In particular, the moment I start typing, the goal "shifts away" from under me — initially it disappears due to "unknown tactic", then it says I have no goals (but still some unsolved goals), then it displays a parser error, then a type mismatch (my goal is still gone), then unknown identifier, etc. Of course by this point I have completely forgotten what my goal was.

What behavior I'd expect:

• I'd expect parsing to be more permissive, similar as in other modern language servers. I.e. it shouldn't completely give up just because I haven't finished typing the line
• Ideally, I'd like to keep seeing my goal (or the last successfully parsed goal) while I'm in the middle of typing. The fact that it jumps around (between "current goal", "no current goal + unsolved goals", "parser error") is very distracting.

I was wondering if this is something that's on the roadmap or is being considered. I think it would be a very significant improvement if this "current state" pane was a tiny bit more resilient and forgiving to ongoing typing — at least while I'm still in the middle of a word.

Thank you!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Not exactly a solution, but you can use the pause button to prevent the goal from changing; there is also a corresponding command, 'Toggle Updating'. Of course it's not ideal to have to keep pause-unpausing, and maybe a better UX would be to add another 'Update Once' command. Then you could keep it paused forever, and only see new information when it's desirable.

But I broadly agree with you that e.g. on typing us, the goal should still show up.

[Bryan Gin-ge Chen]

This is maybe just a workaround for what you really want, but there is a "Pause updating" button in the upper right corner of the infoview which will freeze the contents of the infoview; you can also bind a keyboard shortcut to lean4.infoView.toggleUpdating which makes using it slightly more ergonomic.

[Damiano Testa]

Would it be hard to have a setting where the infoview updates only when the Syntax of the command was successfully parsed? I feel like that could be a good compromise.

[Dan Abramov]

Not sure settings are the way to go (this is most useful to beginners — who wouldn't know to turn the setting on).

I wonder if it would be possible to display the previous state on parser error but fade it out or dim it, while displaying the parser error below. So that you see the last successful state, but its staleness is communicated and the error is clearly visible. I think this could be decent until it's possible to make parsing itself more resilient.

Thanks for the suggestions re: pausing.

[Dan Abramov]

I do think that "pausing" (while handy in the meantime) is not the right way to think about this. It's a known problem in many other languages / IDEs, and I'm sure it has been satisfactorily solved by now for those. E.g. it's worth looking at how Visual Studio handles half-valid C# lines, or how VS Code handles half-valid TS. I would expect it to not choke on it. (As I'm sure the Lean team knows there's plenty of prior art in this area.)

So my broader point is that I as a user shouldn't need to manually direct the tool's attention. If the architecture is right, the tool should be able to just "do the right thing", ofc with some question of what the "right thing" is in each incomplete state.

[Damiano Testa]

Btw, what I sometimes do in this situation, is to toggle between commenting/uncommenting the current line. This, combined with sprinkling sorries and underscores in the "right places" is usually enough for me.

[Floris van Doorn]

related: lean4#4181 (please upvote that issue if you find this annoying)

[Notification Bot]

This topic was moved here from #lean4 dev > Can Lean InfoView be more resilient to unfinished lines? by Sebastian Ullrich.

[Sebastian Ullrich]

I moved this thread since it's a feature request of interest to general users

[Peter Nelson]

I think that improving this would be a great idea. Having the infoview paused the majority of the time is so ingrained in my workflow that it hadn't occurred to me that things could be better some other way.

[Oliver Nash]

Would it be crazy if Lean only fired (and updated the InfoView) when I saved the file? That's what my LaTeX compiler does, and I like it.

[Ruben Van de Velde]

As long as you don't make me work like that :)

[Matthew Ballard]

If you write your Lean code in notepad, this is (almost) the default behavior! :)