Marc Huisinga
Marc Huisinga
Following the instructions in the "Adding Aesop to Your Project" section of the README in a fresh project with the `leanprover/lean4:nightly-2022-10-03` nightly, importing aesop yields an `invalid environment extension, 'coe'...
Fixes #1170. This PR adds the module name to `RefIdent` in order to distinguish conflicting names from different files. This also fixes related issues in find-references or the call hierarchy...
This PR fixes an issue where the file worker would not provide the client with semantic tokens until the file had been elaborated completely. The file worker now also tells...
This PR adds support for requests from the server to the client in the language server. It is based on #3014 and was developed during an experiment for #3247 that...
Sends a diagnostic informing the user to run Restart File when a file dependency is saved. Based on #3014 because this feature was easier to implement with the new architecture....
When I have time to work on this again (in ~2 months), I'd like to adjust the API so that no extra conversion step is necessary at the end and...
### Description Typically, when opening a file with a stale dependency, there is a diagnostic under 'Messages' that informs us that 'Restart File' needs to be called. However, right after...
This occured [on the Lean Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Trouble.20installing.20lean4). There's a good chance that this is not an extension error. It's worth investigating whether we can somehow trigger this error on Windows.
Consider the following input: ``` foo bar \n foo bar ``` where the `\n` is typed in as `\\n`. When using undo to return the document to an empty state...
### Description Use the following MWE and trigger Go to Definition at ``: ``` #eval 1 ``` This yields an error: ``` [Error - 11:37:43 AM] Request textDocument/definition failed. Message:...