VSCode small feature requests/observations?

Stream: lean4

[Tom]

As a new Lean user, I have some minor QoL suggestions around the Lean Infoview. I looked at the vscode-lean4 repo and it said to have a discussion here first, so here I am. I didn't find any related feature requests either. I am going to split each into a separate message to people can react to them/thumb up independently.

[Tom]

1. I work with the "All Messages" window open. As I scroll through code and the "expected type/goal view" updates, the rest of the pane jumps all over the place, which makes me lose track of where I was in the "messages" pane.

Would it be possible to put the "expected type/goals" into a statically sized, resizable pane so that even though it updates, the rest of the view doesn't skip around madly?

[Tom]

2. Would it be possible to make the "All Messages" pane stay in "lock step" with the location of the editing cursor?

[Tom]

3. Related to 2., would it be possible to add a small visual highlight/ribbon to indicate the current message under the cursor?

[Tom]

4. It would be really great - instead of just the expected type - to have another pane which can display more info about the symbol under the cursor, rather than just its type, e.g. its Repr if valid, (at least) the function signature (e.g. as displayed by #print) etc.

As I'm learning, I am mostly looking at and trying to understand other people's code but I have to keep adding/removing #eval statements in the current file to get a sense of the values involved. (I know about hovers)

[Tom]

Thanks for reading!

[Kim Morrison]

I think the problem with 1. is that most people do not work with All Messages open, and having the goal view has static size would be problematic, but very often it occupies the entire infoview, and scrolling is painful.

[Kim Morrison]

Could you explain in more detail what you mean in 2.?

[Kim Morrison]

For 4. could you say in more detail what "more info" you want, that isn't already in a hover?

[Tom]

I see what you mean about 1. It could be optional, or the pane could be set to be dynamic or static, in which case it would retain the current behavior.

[Tom]

Regarding 2: Maybe an demonstration: Open a file and put in a bunch of eval statements that are spaced by a few lines, just e.g.

#eval 1


#eval 2


#eval 3
...

etc so that the All Messages view becomes bigger than your editor window. Keep it open and scroll throw the file visiting the #eval statements. First, the movement is seizure-inducing :laughing: . But second, note the pane will only display the #evals near the top of the file, rather than providing the context around the place where I'm editing - i.e. it doesn't move in lock-step with the editing window.

Maybe a similar example would be when you do diffs in an editor: You want a scroll action to move both the files your diffing so you can see the context simultaneously.

I hope that that explains it better.

[Damiano Testa]

Have you tried using the VSCode extension Error lens?

[Tom]

A hover displays the types (and perhaps doc strings) of the functions but doesn't show the Repr of values. Having said that, I think it would still be more ergonomic for the exploration of a new code base to be able to just navigate around the code and simply have a "perma-hover" window that shows me the symbols as I navigate over them.

Second is more related to learning, and perhaps this is just me:

As I learn a programming language, I write a lot of Micky Mouse programs to explore how things work. In something like Python, which has a debugger, I can step through some code and inspect values.

With lean, it's different. Without a debugger, I write a lot of top-level definitions (e.g. as I'm working through "Functional Programming in Lean" and other materials) and then write a ton of #eval/#check/#print etc statements to get an idea what's going on.

So I guess I'm asking for a feature to make this a little easier for myself (and hopefully others) - so e.g. rather than just seeing the type of an expression in the view, there could be another (optional?) section that tries to show the Repr etc of the value, if available.

Does that make sense?

[Tom]

Damiano Testa said:

Have you tried using the VSCode extension Error lens?

Sorry, I've not. Which of these things would it help with?

[Damiano Testa]

I think 2: it shows the output of stuff like #eval in the window where you type the code, not in the infoview.

[Johan Commelin]

Yeah, Error Lens is a big QoL improvement (-;

[Kim Morrison]

Can we set it as an automatically installed dependency of the Lean extension or something? Or suggest it prominently during setup?

[Johan Commelin]

cc @Marc Huisinga I guess?

[Shreyas Srinivas]

Extensions can be bundled together as a recommendation.

[Shreyas Srinivas]

When installing such a bundle, all recommended extensions are installed. The trouble with bundling third party extensions is more social: how is a decision to include or exclude an extension made and which extensions are deemed "useful" or not. Everybody might want their favourite QoL extension as part of the bundle.

[Shreyas Srinivas]

Sorry the term is not bundling. It is "extension pack" https://code.visualstudio.com/blogs/2017/03/07/extension-pack-roundup

[Tom]

@Damiano Testa @Johan Commelin

Thanks for the suggestions, that plugin is helpful.