opt-bug-336b68e-final

feat: 'unknown identifier' code actions (#7665)

This PR adds support for code actions that resolve 'unknown identifier'
errors by either importing the missing declaration or by changing the
identifier to one from the environment.

<details>
<summary>Demo (Click to open)</summary>


![Demo](https://github.com/user-attachments/assets/ba575860-b76d-4213-8cd7-a5525cd60287)
</details>

Specifically, the following kinds of code actions are added by this PR,
all of which are triggered on 'unknown identifier' errors:
- A code action to import the module containing the identifier at the
text cursor position.
- A code action to change the identifier at the text cursor position to
one from the environment.
- A source action to import the modules for all unambiguous identifiers
in the file.

### Details
When clicking on an identifier with an 'unknown identifier' diagnostic,
after a debounce delay of 1000ms, the language server looks up the
(potentially partial) identifier at the position of the cursor in the
global reference data structure by fuzzy-matching against all
identifiers and collects the 10 closest matching entries. This search
accounts for open namespaces at the position of the cursor, including
the namespace of the type / expected type when using dot notation. The
10 closest matching entries are then offered to the user as code
actions:
- If the suggested identifier is not contained in the environment, a
code action that imports the module that the identifier is contained in
and changes the identifier to the suggested one is offered. The
suggestion is inserted in a "minimal" manner, i.e. by accounting for
open namespaces.
- If the suggested identifier is contained in the environment, a code
action that only changes the identifier to the suggested one is offered.
- If the suggested identifier is not contained in the environment and
the suggested identifier is a perfectly unambiguous match, a source
action to import all unambiguous in the file is offered.

The source action to import all unambiguous identifiers can also always
be triggered by right-clicking in the document and selecting the 'Source
Action...' entry.

At the moment, for large projects, the search for closely matching
identifiers in the global reference data structure is still a bit slow.
I hope to optimize it next quarter.

### Implementation notes
- Since the global reference data structure is in the watchdog process,
whereas the elaboration information is in the file worker process, this
PR implements support for file worker -> watchdog requests, including a
new `$/lean/queryModule` request that can be used by the file worker to
request global identifier information.
- To identify 'unknown identifier' errors, several 'unknown identifier'
errors in the elaborator are tagged with a new tag.
- The debounce delay of 1000ms is necessary because VS Code will
re-request code actions while editing an unknown identifier and also
while hovering over the identifier.
- We also implement cancellation for these 'unknown identifier' code
actions. Once the file worker responds to the request as having been
cancelled, the watchdog cancels its computation of all corresponding
file worker -> watchdog requests, too.
- Aliases (i.e. `export`) are currently not accounted for. I've found
that we currently don't handle them correctly in auto-completion, too,
so we will likely add support for this later when fixing the
corresponding auto-completion issue.
- The new code actions added by this request support incrementality.