Interactive goals & diagnostics #596
Conversation
There was a problem hiding this comment.
We add a new taggedMsg field to the Diagnostic type which clients can ignore [...]
Is this true? Don't you get a memory leak if you don't release the RPC references? (Also, diagnostics are updated really often. This will cause a lot of release requests.)
(There's also the question of who owns these references in the vscode extension, i.e., who is responsible for releasing them. If it is the infoview, what happens if it is closed?)
This is correct. We can have a |
What happens if the infoview is closed? |
|
There's also quite a bit of discussion on the corresponding vscode-lean4 PR: leanprover/vscode-lean4#32 |
|
This should now be in a reviewable state. There are some TODOs for which I will make issues, but the backend seems to be working. |
| let ckvs := kvs.fold (fun acc k j => s!"{renderString k}:{compress j}" :: acc) [] | ||
| let ckvs := ",".intercalate ckvs | ||
| s!"\{{ckvs}}" | ||
| protected inductive CompressWorkItem |
There was a problem hiding this comment.
It doesn't seem possible to open a private inductive to get its constructors (unknown namespace 'CompressWorkItem').
There was a problem hiding this comment.
Interesting, I think that could be considered a bug
| def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot MessageLog) := do | ||
| let inputCtx := Parser.mkInputContext contents "<input>" | ||
| def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do | ||
| let inputCtx := Parser.mkInputContext text.source "<input>" | ||
| let cmdState := snap.cmdState | ||
| let scope := cmdState.scopes.head! | ||
| let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } | ||
| let (cmdStx, cmdParserState, msgLog) := | ||
| Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog |
There was a problem hiding this comment.
I think we can also just pass a fresh message log here so that the result contains the new messages only. A command shouldn't care about messages before it.
There was a problem hiding this comment.
Yeah, that would get rid of computing the MessageLog diff. But we do want Snapshot.interactiveDiags to contain every diagnostic up to a point so that we can send them easily without folding over all snapshots. So we'd have a MessageLog with messages just for this snapshot but an interactive diagnostics log for everything, which is perhaps a bit weird. What do you think?
There was a problem hiding this comment.
I think that's fine, we can call it allInteractiveDiags or something similar. Not sure folding would even be a performance issue, concatenating mostly-empty arrays should be quite fast even with hundreds of snapshots.
There was a problem hiding this comment.
I tried this out now, but it is still clunky. The reason is that the MessageLog is part of Command.State which is designed for a "rolling" usage. So we'd have to leave most of the command state as-is but clear out just the message log. I would leave it as is, but added a comment clarifying it.
src/Lean/Widget/TaggedText.lean
Outdated
| partial def map (f : α → β) : TaggedText α → TaggedText β := | ||
| go | ||
| where go : TaggedText α → TaggedText β |
There was a problem hiding this comment.
| partial def map (f : α → β) : TaggedText α → TaggedText β := | |
| go | |
| where go : TaggedText α → TaggedText β | |
| variable (f : α → β) in | |
| partial def map : TaggedText α → TaggedText β |
etc
There was a problem hiding this comment.
Changed, but I must note that this is one of few things where the Lean 3 syntax actually seems more natural/sensible to me. The old fixed-before-colon/recursive-after-colon makes sense once one gets used to it. It's kind of weird that variable (a : T) in def foo has a different behaviour than directly writing def foo (a : T) and indeed I forgot about it here.
|
I've tried implementing the RPC protocol in the neovim plugin (Julian/lean.nvim#118). Some thoughts: There is another problem with The keep-alive mechanism is not particularly helpful for the neovim plugin. It doesn't do anything that can't be done by sending a I'd like to reiterate at this point that I think it is worth to get the basic design right from the beginning. It is trivial to add new functions and fields to existing structures; and this is unlikely to break anything. However the current approach really hardcodes the assumption that every editor has at most one infoview which uses at most one session, and doesn't use the RPC for anything else. I would at least like to see a plan on how to support two infoviews. There are all kinds of cool things on the horizon (e.g. there could be a vscode API to embed a webview in the editor), and I would hate it if we couldn't make use of them due to basic design constraints. The The The I don't completely understand the |
|
Something else that would be super cool and might be hard to retrofit (because the InfoWithCtx is a reference, and we can't just add a field there) is semantic highlighting. That is, information about which parts of a CodeWithInfos are keywords, literals, operators, etc. |
|
@gebner I am thinking more about backwards compatibility. We should preserve the interface when possible, but ultimately I do want to at least be able to make breaking changes. I am assuming that we do not have to worry about a new server<->old client situation because at least VSCode will auto-update extensions, and in Vim or Emacs we can expect users to update as well. This leaves new client<->old server in cases when one is working on a project that e.g. uses older mathlib. For this, I think we should start properly versioning the Lean server (currently on 0.0.1) and detect this in editor extensions when necessary, then use the API for that server version. |
Motivation: we may want to also use RPC in editor insets, or multiple webviews in general.
|
All outstanding comments should be addressed now. |
|
@Vtec234 Is it ready to be merged? |
| | k => | ||
| (do let stx ← (delabAttribute.getValues (← getEnv) k).firstM id | ||
| let stx ← annotateCurPos stx | ||
| addTermInfo (← getPos) stx (← getExpr) |
There was a problem hiding this comment.
What is the overhead of using addTermInfo here? Is the slowdown significant? Just curious.
There was a problem hiding this comment.
I didn't test in a profiler, but in terms of wall time on both a long trace (~1s to print) and a long expression (~1.3s), I observed no difference with and without the addTermInfo/addFieldInfo calls.
I think so. There are some smaller discussions left which can be addressed later. |
* `false` -> `False` (we're talking about the Prop, not the Bool). * `begin .. end` -> `by ...` * Remove obsolete comment about `push_neg` not being implemented. (It landed in leanprover#344).
Implements server-side support for interactive goals and diagnostics.
Currently the only supported mode of interaction is exploringExprs (we can check the types of subexpressions and explicit arguments). We add a newtaggedMsgfield to theDiagnostictype which clients can ignore, while the infoview uses it to visualize things.We support the following interactive objects:
Exprbut other objects such as generalSyntaxwill also work, as long as they have associatedElab.Infolet-bound valuesTODOs:
InfoTrees instead ofExprs directly (depends at least on feat: pp.analyze heuristics for concise roundtripping #575)