refactor: make RPC independent of infoview #226
Conversation
|
The test errors seem to be nondeterministic. The windows tests succeed more often than the linux tests, which often (but not always) fail at the "Bootstrap Test Suite" stage. |
|
The test failure could be related to #227 |
|
Noticed a bug: if you delete a file, then apparently the session doesn't get closed. This is most likely a bug in master as well, since it works fine if you close the file instead of deleting it. |
|
Oops, I apparently broke the interactive diagnostics. Will look into this later. |
Can't reproduce.
Apparently we update goals and diagnostics on different schedules. I accidentally changed the code so that it only picks up the interactive diagnostics once the goals are updated, and they happen to be updated just before we get the interactive diagnostics. (We start out with the plain diagnostics, and only switch to the interactive ones when/if we get them.) Fixed now. |
There was a problem hiding this comment.
But my crazy reconnection code though :( Alas, #connecting: Map<DocumentUri, Promise<RpcSession | undefined>> will live on as a fond memory. I like the changes! I don't have time to test them, so the review is just about the codebase.
I've added a React context for the current
RpcSession
Since the RpcSession now bundles positions, I am guessing you changed your mind about not using a context to store these since the linked issue?
I didn't like storing the position in the context because the position is ambiguous (does it refer to the position of the cursor, the message, etc.?). By contrast, the |
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
Implementation of leanprover/lean4#2064. Besides adding support for widget messages, this adds an `EnvPosContext` that stores the position that a component is "about" (see the docstring for more detail). This was originally proposed in #197 and eventually dismissed (see #226 for a detailed discussion), but I think it warrants a reconsideration. While Gabriel's point that there are many positions around remains true, the `EnvPosContext` stores a very specific one. This position is only used to retrieve a snapshot, and from that a `Lean.Environment`, on the server-side. Widgets currently have to pass this position around manually; this has led to [errors](leanprover-community/ProofWidgets4@ca66ebb) in user code. Furthermore, so far I have not encountered any situation where it makes sense to modify the position; thus a context seems like a preferable approach. If needed, the context can still be set by users. I also had to update some package versions to have tests building again. I hope that didn't break anything!
This PR refactors the
RpcSessionsclass.infoview-apibecause that's where we put all code shared between infoview and extension). This allows us to potentially use the RPC interface in the extension as well to make fancier hovers, etc. See Go-to-definition for types in hover lean4#1117RpcSessiontype now stores the position in the file (which is required for RPC calls). This greatly simplifies the API wrappers.RpcSessiontype also registers the RPC references automatically. This reduces the API surface ofRpcSessionand again greatly simplifies the wrappers.RpcSession. This removes a lot ofposprops in the widget components. Addresses Infoview DocumentPosition should be a context #197.RpcSessionassociated with the retrieved diagnostics/goals. That is, if you pause an info and restart the file, we no longer send the now invalid(!) references from the old session to the newly restarted file worker.WithRpcSessionscomponent. The idea had a charm, but it was broken with paused infos anyhow, because they didn't (and shouldn't!) re-request the diagnostics/goals. Addresses Close RPC sessions on server restart. #66 (comment)What now happens when a file worker crashes or restarted is the following: Calls on
RpcSessions from the old worker will fail, returning an appropriate error message (that is shown in the tooltip, and still needs to be made more user-friendly). Non-paused infos already listen on the server restarted event; they automatically update and pick up a newRpcSessionto the new worker when they do that.| undefinedin the return type. If the RPC calls fail, then it throws an exception (with an informative error message) instead of returningundefined.