VScode goodies

Stream: general

[Johan Commelin]

Would it be possible to configure a hotkey in VScode that grabs the first output from suggest and prepends/replaces the suggest that generated it?

[Johan Commelin]

Bonus points if the replace/prepending is automatically chosen depending on whether the suggestion is an exact/refine

[Bryan Gin-ge Chen]

This should be possible with some ugly tactic state parsing hacks, but I wonder if there might be a better way to do this using a hole command.

[Johan Commelin]

@Bryan Gin-ge Chen I had also hoped that hole commands would help. But see the other thread about hole commands in tactic mode. It doesn't really seem to work, as far as I can see.

[Johan Commelin]

I think these sort of UI improvements would break down another entry barrier for new users. But I lack the skills of implementing this.

[Patrick Massot]

Globally there is a big need for more structured tactic state information. Currently the Lean server returns tactic state as a single string that you see in the Lean message panel in VScode. Even syntax highlighting there is based on a hack. It would be really nice to see this changing in Lean 4, but I don't know what are the plans here.

[Sebastien Gouezel]

It would be amazing if hovering and clicking on definitions worked in the tactic state...

[Kevin Buzzard]

Even hovering on notation in the tactic state to see the keyboard shortcut would be useful! But it would be much better for definitions because sometimes they're much harder to cut and paste into something syntactically valid in a .lean file (especially if you're in the middle of something else)

[Sebastian Ullrich]

It would be amazing if hovering and clicking on definitions worked in the tactic state...

It will.

[Sebastian Ullrich]

Even hovering on notation in the tactic state to see the keyboard shortcut would be useful!

That part is on the editor. Works out of the box in Emacs for example (describe-char).

[Bryan Gin-ge Chen]

Even hovering on notation in the tactic state to see the keyboard shortcut would be useful!

That part is on the editor. Works out of the box in Emacs for example (describe-char).

I think I can see how to implement this for the VS Code extension (but no ETA promise). It will require implementing some custom tooltip functionality for the info view; we can't reuse VS Code's built-in "hover provider".

@Sebastian Ullrich Is it too early to ask how much the Lean server interface will change from Lean 3 to Lean 4?

[Sebastian Ullrich]

Is it too early to ask how much the Lean server interface will change from Lean 3 to Lean 4?

We'll implement LSP, so... completely

[Bryan Gin-ge Chen]

I think these sort of UI improvements would break down another entry barrier for new users.

+1 from me. I for one would be happy to see more ideas and discussion of UI here.

[Simon Cruanes]

I heard that LSP lacked some features generally required by proof assistants. Have you written a plan/design somewhere?

[Johan Commelin]

@Simon Cruanes Can you be more specific? What kind of features are you thinking of? (I don't know anything about LSP...)

[Simon Cruanes]

Anything interactive, I'd say, since it's designed for "normal" programming languages in mind. But then the world is moving away from Coq-style display of tactics, so it might be doable, idk.

[Mario Carneiro]

I wrote an LSP server for MM0, and there isn't really anything like the goal view, but the format is extensible so you can always just add a custom extension

[Simon Cruanes]

You should put screenshots on the github page @Mario Carneiro :grinning_face_with_smiling_eyes:

[Mario Carneiro]

I really should

[Bryan Gin-ge Chen]

But then the world is moving away from Coq-style display of tactics, so it might be doable, idk.

What is the world moving towards instead?

[Mario Carneiro]

I mostly rely on diagnostics and hovers

[Mario Carneiro]

but getting the goal state via diagnostics is a bit exasperating

[Bryan Gin-ge Chen]

I think taking away the tactic state display would be a pretty hard sell here.

[Mario Carneiro]

it's not clear to me how to improve LSP to support our use case better though

[Mario Carneiro]

once upon a time, the goal state was displayed via "output" (maybe it still does in emacs)

[Simon Cruanes]

What is the world moving towards instead?

I meant with the "checked" area on top. You still need a way of displaying the proof state, using an extension I guess yeah.

[Bryan Gin-ge Chen]

Hmm, I'm not familiar with Coq. What is the "checked" area?

[Mario Carneiro]

There is a big colored highlight covering the top half of the file, above the cursor, and you "step" the checker through lines

[Johan Commelin]

In Coq the proof state doesn't reflect the state of where your cursor is, but the point up to some "checkpoint".

[Simon Cruanes]

https://en.wikipedia.org/wiki/Proof_assistant#/media/File:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png

[Johan Commelin]

I guess you could view this "checkpoint" as a 2nd cursor that you can move around whenever you want.

[Mario Carneiro]

when tactics are very expensive, this approach scales better

[Mario Carneiro]

because you aren't rechecking the whole file all the time

[Simon Cruanes]

Another possibility is to use hashing to avoid recomputing things that haven't changed.

[Mario Carneiro]

but it is definitely less ergonomic than the lean / isabelle "dynamic document" style, which puts more strain on the system to keep things in sync but has an easy mental model

[Sebastien Gouezel]

In Lean4, the state at the end of each line in a tactic block will be stored, right, so that you get the best of both worlds (no need to recompile the beginning of a proof if you just change the last line)?

[Simon Cruanes]

In Lean4, the state at the end of each line in a tactic block will be stored, right, so that you get the best of both worlds (no need to recompile the beginning of a proof if you just change the last line)?

that's fine if you detect that nothing was changed, yes!

[Gabriel Ebner]

it's not clear to me how to improve LSP to support our use case better though

You can easily add custom commands to LSP. I would expect that an LSP server for Lean offers a command to get the goal state at any position in the file. Then we can roll the info view as usual. I'm not sure if our (comparatively) niche use case is worth standardizing. It might even be desirable to roll it ourselves to facilitate experimentation.

[Mario Carneiro]

It might be nice to standardize the LSP extension across theorem provers though, so that the LSP client can stay relatively generic; otherwise it's not buying much over the original situation

[Simon Cruanes]

just dub the extensions "LLSP", for "logic language server protocol" :wink:

[Edward Ayers]

"Proof Generaler"

[Patrick Massot]

In Coq the proof state doesn't reflect the state of where your cursor is, but the point up to some "checkpoint".

The absence of Coq's iron curtain going up and down in your file is one of the first things I noticed when I used Lean for the first time. Maybe it was even before I noticed unicode. It really feels like absolute freedom to use a proof assistant that way, even after using Coq only for a couple of weeks.