What happened?
The Lean autocomplete is still a bit finicky
How can we reproduce this issue?
Example:
- Click an input area that is not the first one in the proof.
- Start a sentence with "E" and notice that examples and exercises are shown as suggestions.
What should happen?
These suggestions should not show up as is. If we are getting suggestions from the language server, the useful ones would be local variable/hypothesis names, or exercise names that could be referred to explicitly.
These suggestions are particularly annoying if you mistype something and accidentally accept them.
Possible resolutions:
- Turn off autocompletions from the Lean LSP all together.
- Filter these suggestions
- Something else?
Note that the code that handles this is common to Rocq and Lean, so take care not to degrade the Rocq experience when working on this.
What happened?
The Lean autocomplete is still a bit finicky
How can we reproduce this issue?
Example:
What should happen?
These suggestions should not show up as is. If we are getting suggestions from the language server, the useful ones would be local variable/hypothesis names, or exercise names that could be referred to explicitly.
These suggestions are particularly annoying if you mistype something and accidentally accept them.
Possible resolutions:
Note that the code that handles this is common to Rocq and Lean, so take care not to degrade the Rocq experience when working on this.