leanprover
Move the abbreviations provider to a UI extension
Currently all of vscode-lean4 runs as a workspace extension, meaning that in remote setups it will run in the remote extension host. This makes the abbreviations UX pretty bad when the connection has a high latency, because abbreviations are resolved across the network. It would be nicer if they were resolved locally. I'm not 100% sure but this might require splitting out a small "abbreviations" extension with extensionKind: ["ui"].
Yes, this is a great idea.
- We need to make sure the transition goes very smoothly. If you have the Lean 4 extension installed and upgrade to the new version, the abbreviation extension must be installed automatically, without any user intervention.
- Also for first-time installation. Installing the Lean 4 extension must automatically and without any user intervention install the abbreviation extension as well.
- It will be hard to revert to an older version of the extension after that, so this change will be in a release by itself.
- We should also remove the abbreviations from the Lean 3 extension as well.
- Some people / installation scripts / bundles download the extension vsix manually to preload vscode. We need to make them aware of this change.
After we extract the abbrevations into their own extension we can remove the markdown trigger for the main extension. The abbreviation extension should then probably always be loaded, with a user-configurable list of file types.
Can I just put it in the InfoView package so I don't have to create a new package?
In case it's unclear what this issue is about: we're talking about the feature that turns \all into ∀ while you type.
It needs to be a separate extension, so in particular it should be a separate package. The abbreviations feature also has nothing to do with the infoview, so it makes little sense to bundle them together.
I mistakenly thought you were talking about the cheat sheet taking too long to load in the documentation view. Sounds like you are talking about the actual interaction in the vscode text editor when you type '\alpha{SPACE} ', it is taking too long to convert that to α as implemented by the AbbreviationRewriter.ts? so you want all this to run client side? On all the remote machines I've tested it is super quick. How could you have a socket taking more than 100ms? This means your response from LSP for things like "." method completion must also be really slow right? How slow, what are you seeing? Can we help debug it to make sure it is not something else causing the delay?
@gebner Hi! I find it extremely confusing that the Lean4 plugin is activated even if I open a random README.md in a repo completely irrelevant to Lean (and elan starts to download the latest nightly). And a bit of research has got me here.
In case it's unclear what this issue is about: we're talking about the feature that turns
\allinto∀while you type.It needs to be a separate extension, so in particular it should be a separate package. The abbreviations feature also has nothing to do with the infoview, so it makes little sense to bundle them together.
I'm wondering how this abbreviation feature interacts with markdown files and why the .md trigger is required in its current form. Or am I misinterpreting the context? 🤔️
