This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.
This PR fixes several causes of test flakiness and re-enables the tests
that were disabled in #10665, #10669 and #10673.
Specifically, it fixes:
- A race condition in the file worker that caused it to report an
incomplete snapshot prefix in the inlay hint request (confirmed to be
the cause of #10665)
- A bug in the test runner where it didn't correctly account for
non-deterministic message ordering inducing different RPC pointer
numbering (confirmed to be the cause of #10673)
- A race condition in the watchdog that would sometimes cause the module
hierarchy to be empty (likely the cause of #10669, but not confirmed as
this issue only reproduced again once in tens of thousands of test runs
on various machines, including CI)
- An unrelated bug in the module hierarchy implementation that would
cause it to report an empty module hierarchy when the file was changed
It also replaces some calls to `Task.get` in the language server with
`IO.wait` to protect the code against unfortunate compiler re-ordering.
This PR fixes deadlocking `exit` calls in the language server.
We have previously observed deadlocking calls to `exit` inside of the
language server and deemed them irrelevant. However, child processes of
these deadlocking exiting processes can continue to consume a large
amount of CPU as they try to compile a library etc. Hence, this PR
switches to the MT safe `_Exit` inside of the language server,
in order to ensure the server finishes when it is told to.
This PR speeds up auto-completion by a factor of ~3.5x through various
performance improvements in the language server. On one machine, with
`import Mathlib`, completing `i` used to take 3200ms and now instead
yields a result in 920ms.
Specifically, the following improvements are made:
- The watchdog process no longer de-serializes and re-serializes most
messages from the file worker before passing them on to the user - a
fast partial de-serialization procedure is now used to determine whether
the message needs to be de-serialized in full or not.
- `escapePart` is optimized to perform better on ASCII strings that do
not need escaping.
- `Json.compress` is optimized to allocate fewer objects.
- A faster JSON compression specifically for completion responses is
implemented that skips allocating `Json` altogether.
- The JSON compression has been moved to the task where we convert a
request response to `Json` so that converting to a string won't block
the output task of the FileWorker and so the `Json` value is not marked
as multi-threaded when we compress is, which drastically increases the
cost of reference-counting.
- The JSON representation of the `data?` field of each completion item
is optimized.
- Both the completion kind and the set of completion tags for each
imported completion item is now cached.
- The filtering of duplicate completion items is optimized.
Other adjustments:
- `LT UInt8` and `LE UInt8` are moved to Prelude so that they can be
used in `Init.Meta` for the name part escaping fast path.
- `Array.usize` is exposed since it was marked as `@[simp]`.
This PR ports more of the post-initialization C++ shell code to Lean.
All that remains is the initialization of the profiler and task manager.
As initialization tasks rather than main shell code, they were left in
C++ (where the rest of the initialization code currently is).
The `max_memory` and `timeout` Lean options used by the the `--memory`
and `--timeout` command-line options are now properly registered. The
server defaults for max memory and max heartbeats (timeout) were removed
as they were not actually used (because the `server` option that was
checked was neither set nor exists).
This PR also makes better use of the module system in `Shell.lean` and
fixes a minor bug in a previous port where the file name check was
dependent on building the `.ilean` rather than the `.c` file (as was
originally the case).
Fixes#9879.
This PR fixes a bug that caused the Lean server process tree to survive
the closing of VS Code.
The cause of this issue was that the file worker main task was blocked
on waiting for the result of `lake setup-file` because the blocking call
was lifted outside of the dedicated server task that was supposed to
contain it by the compiler.
This PR changes `lake setup-file` to use the server-provided header for
workspace modules.
This also reverts #9163 as the underlying issue is now fixed.
This PR removes uses of `Lean.RBMap` in Lean itself.
Furthermore some massaging of the import graph is done in order to avoid
having `Std.Data.TreeMap.AdditionalOperations` (which is quite
expensive) be the critical path for a large chunk of Lean. In particular
we can build `Lean.Meta.Simp` and `Lean.Meta.Grind` without it thanks to
these changes.
We did previously not conduct this change as `Std.TreeMap` was not
outperforming `Lean.RBMap` yet, however this has changed with the new
code generator.
This PR disables the use of the header produced by `lake setup-file` in
the server for now. It will be re-enabled once Lake takes into account
the header given by the server when processing workspace modules.
Without that, `setup-file` header can produce odd behavior when the file
on disk and in an editor disagree on whether the file participates in
the module system.
This PR adds support to the server for the new module setup process by
changing how `lake setup-file` is used.
In the new server setup, `lake setup-file` is invoked with the file name
of the edited module passed as a CLI argument and with the parsed header
passed to standard input in JSON form. Standard input is used to avoid
potentially exceeding the CLI length limits on Windows. Lake will build
the module's imports along with any other dependencies and then return
the module's workspace configuration via JSON (now in the form of
`ModuleSetup`). The server then post-processes this configuration a bit
and returns it back to the Lean language processor.
The server's header is currently only fully respected by Lake for
external modules (files that are not part of any workspace library). For
workspace modules, the saved module header is currently used to build
imports (as has been done since #7909). A follow-up Lake PR will align
both cases to follow the server's header.
Lean search paths (e.g., `LEAN_PATH`, `LEAN_SRC_PATH`) are no longer
negotiated between the server and Lake. These environment variables are
already configured during sever setup by `lake serve` and do not change
on a per-file basis. Lake can also pre-resolve the `.olean` files of
imports via the `importArts` field of `ModuleSetup`, limiting the
potential utility of communicating `LEAN_PATH`.
This PR fixes a bug where the unknown identifier code actions wouldn't
work correctly for some unknown identifier error spans and adjusts
several unknown identifier spans to actually end on the identifier in
question.
The following additional adjustments are made:
- The fallback mechanism of the unknown identifier code actions is
removed, since it could produce severely incorrect suggestions for
unknown identifier errors on fields.
- A performance bug when using the code action to import all unknown
identifiers is fixed.
- A bug that occurs when the elaborator produces multiple overlapping
completion infos is fixed.
- A bug in the snapshot selection that could cause it to wait for
snapshots in snapshots with non-canonical syntax is fixed.
- Some invariants of the snapshot tree are documented.
- The snapshot tree formatting is adjusted to display the final info
tree again.
This PR adjusts the experimental module system to not export the bodies
of `def`s unless opted out by the new attribute `@[expose]` on the `def`
or on a surrounding `section`.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR adds the `--setup` option to the `lean` CLI. It takes a path to
a JSON file containing information about a module's imports and
configuration, superseding that in the module's own file header. This
will be used by Lake to specify paths to module artifacts (e.g., oleans
and ileans) separate from the `LEAN_PATH` schema.
To facilitate JSON serialization of the header data structure, `NameMap`
JSON instances have been added to core, and `LeanOptions` now makes use
of them.
This PR reverts #8056 because the implementation there has a bug that is
best fixed with a different approach, and which we should preferably
only merge next release cycle.
This PR fixes a bug where the trace nodes in the InfoView would close
while the file was still being elaborated.
Closes#8053.
The cause of this bug was that we didn't memorize interactive
diagnostics correctly, so the server would generate new RPC pointers in
every single `getInteractiveDiagnostics` RPC request, which lead to the
client resetting the UI.
This PR extends `Std.Channel` to provide a full sync and async API, as
well as unbounded, zero sized and bounded channels.
A few notes on the implementation:
- the bounded channel is inspired by [Go channels on
steroids](https://docs.google.com/document/d/1yIAYmbvL3JxOKOjuCyon7JhW4cSv1wy5hC0ApeGMV9s/pub)
though currently doesn't do any of the lock-free optimizations
- @mhuisi convinced me that having a non-closable channel may be a good
idea as this alleviates the need for error handling which is very
annoying when working with `Task`. This does complicate the API a little
bit and I'm not quite sure whether this is a choice we want users to
give. An alternative to this would be to just write `send!` that panics
on sending to a closed channel (receiving from a closed channel is not
an error), this is for example the behavior that golang goes with.
This PR fixes a number of bugs related to the handling of the source
search path in the language server, where deleting files could cause
several features to stop functioning and both untitled files and files
that don't exist on disc could have conflicting module names.
In detail, it makes the following adjustments:
- The URI <-> module name conversion was adjusted to produce no name
collisions.
- File URIs in the search path yield a module name relative to the
search path, as before.
- File URIs not in the search path, non-file URIs and non-`.lean` files
yield a `«external:<full uri>»` module name.
- To avoid the issue of the URI -> module name conversion failing when a
file is deleted from disc, we now cache the result of this conversion in
the watchdog and the file worker when the file is first opened.
- All of the URI <-> module name conversions now consistently go through
`Server.documentUriFromModule?` and `moduleFromDocumentUri` to ensure
that we don't have minor deviations for this conversion all over the
place.
- The threading of the source search path through the file worker (from
`lake setup-file`) is removed. It turns out that `lake serve` already
sets the correct source search path in the environment, so we can just
always use the search path from the environment.
- Since we can now answer more requests that need the .ileans in
untitled files, a lot of the tests that test 'Go to definition' needed
to be adjusted so that they use the information from the watchdog, not
the file worker. As we load references asynchronously, this PR adds an
internal `$/lean/waitForILeans` request that tests can use to wait for
all .ilean files to be loaded and for the ilean references from the file
worker for the current document version to be finalized.
- As part of this PR, we noticed that the .ileans aren't available in
the NixOS setup, so @Kha adjusted the Nix CI to fix this.
### Breaking changes
- `Server.documentUriFromModule` has been renamed to
`Server.documentUriFromModule?` and doesn't take a `SearchPath` argument
anymore, as the `SearchPath` is now computed from the `LEAN_SRC_PATH`
environment variable. It has also been moved from `Lean.Server.GoTo` to
`Lean.Server.Utils`.
- `Server.moduleFromDocumentUri` does not take a `SearchPath` argument
anymore and won't return an `Option` anymore. It has also been moved
from `Lean.Server.GoTo` to `Lean.Server.Utils`.
- The `System.SearchPath.searchModuleNameOfUri` function has been
removed. It is recommended to use `Server.moduleFromDocumentUri`
instead.
- The `initSrcSearchPath` function has been renamed to
`getSrcSearchPath` and has been moved from `Lean.Util.Paths` to
`Lean.Util.Path`. It also doesn't need to take a `pkgSearchPath`
argument anymore.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
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>
</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.
This PR enables the elaboration of theorem bodies, i.e. proofs, to
happen in parallel to each other as well as to other elaboration tasks.
Specifically, to be eligible for parallel proof elaboration,
* the theorem must not be in a `mutual` block
* `deprecated.oldSectionVars` must not be set
* `Elab.async` must be set (currently defaults to `true` in the language
server, `false` on the cmdline)
To be activated for downstream projects (i.e. in stage 1) pending
further Mathlib validation.
This PR adds server-side support for dedicated 'unsolved goals' and
'goals accomplished' diagnostics that will have special support in the
Lean 4 VS Code extension. The special 'unsolved goals' diagnostic is
adapted from the 'unsolved goals' error diagnostic, while the 'goals
accomplished' diagnostic is issued when a `theorem` or `Prop`-typed
`example` has no errors or `sorry`s. The Lean 4 VS Code extension
companion PR is at leanprover/vscode-lean4#585.
Specifically, this PR extends the diagnostics served by the language
server with the following fields:
- `leanTags`: Custom tags that denote the kind of diagnostic that is
being served. As opposed to the `code`, `leanTags` should never be
displayed in the UI. Examples introduced by this PR are a tag to
distinguish 'unsolved goals' errors from other diagnostics, as well as a
tag to distinguish the new 'goals accomplished' diagnostic from other
diagnostics.
- `isSilent`: Whether a diagnostic should not be displayed as a regular
diagnostic in the editor. In VS Code, this means that the diagnostic is
displayed in the InfoView under 'Messages', but that it will not be
displayed under 'All Messages' and that it will also not be displayed
with a squiggly line.
The `isSilent` field is also implemented for `Message` so that silent
diagnostics can be logged in the elaborator. All code paths except for
the language server that display diagnostics to users are adjusted to
filter `Message`s with `isSilent := true`.
This PR fixes several inlay hint race conditions that could result in a
violation of the monotonic progress assumption, introduced in #7149.
Specifically:
- In rare circumstances, it could happen that stateful LSP requests were
executed out-of-order with their `didChange` handlers, as both requests
and the `didChange` handlers waited on `lake setup-file` to complete,
with the latter running those handlers in a dedicated task afterwards.
This meant that a request could be added to the stateful LSP handler
request queue before the corresponding `didChange` call that actually
came before it. This PR resolves this issue by folding the task that
waits for `lake setup-file` into the `RequestContext`, which ensures
that we only need to wait for it when actually executing the request
handler.
- While #7164 fixed the monotonic progress assertion violation that was
caused by `$/cancelRequest`, it did not account for our internal notion
of silent request cancellation in stateful LSP requests, which we use to
cancel the inlay hint edit delay when VS Code fails to emit a
`$/cancelRequest` notification. This issue is resolved by always
producing the full finished prefix of the command snapshot queue, even
on cancellation. Additionally, this also fixes an issue where in the
same circumstances, the language server could produce an empty inlay
hint response when a request was cancelled by our internal notion of
silent request cancellation.
- For clients that use `fullChange` `didChange` notifications (e.g. not
VS Code), we would get several aspects of stateful LSP request
`didChange` state handling wrong, which is also addressed by this PR.
This PR ensures that all tasks in the language server either use
dedicated tasks or reuse an existing thread from the thread pool. This
ensures that elaboration tasks cannot prevent language server tasks from
being scheduled. This is especially important with parallelism right
around the corner and elaboration becoming more likely to starve the
language server of computation, which could drive up language server
latencies significantly on machines with few cores.
Specifically, all language server tasks are refactored to use a new thin
`ServerTask` API wrapper with a single "costly" vs "cheap" dimension,
where costly tasks are always scheduled as dedicated tasks, and cheap
tasks are always made to either run on the calling thread or to reuse
the thread of the task being mapped on by using the `sync` flag.
ProofWidgets4 adaption PR:
https://github.com/leanprover-community/ProofWidgets4/pull/106
### Other changes
- This PR makes several tasks dedicated that weren't dedicated before,
and uses `sync := true` for some others. The rules for this are
described in the module docstring of `ServerTask.lean`.
- Most notably, the reporting task in the file worker was *not* a
dedicated task before this PR, which could easily lead to thread pool
starvation on successive changes. It also did not support cancellation.
This PR ensures that it does.
### Breaking changes
- `RequestTask` and the request-oriented snapshot API are refactored to
use `ServerTask` instead of `Task`. All functions in `Task` have close
analogues in `ServerTask`, and functions on `RequestTask` now need to
distinguish between whether a `map` or a `bind` is cheap or costly. This
affects all downstream users of `RequestM`, e.g. tools that extend the
language server with their own requests, or some users of the RPC
mechanism.
- The following unused functions of the `AsyncList` API have been
deleted: `append`, `unfoldAsync`, `getAll`, `waitHead?`, `cancel`
This PR adds language server support for request cancellation to the
following expensive requests: Code actions, auto-completion, document
symbols, folding ranges and semantic highlighting. This means that when
the client informs the language server that a request is stale (e.g.
because it belongs to a previous state of the document), the language
server will now prematurely cancel the computation of the response in
order to reduce the CPU load for requests that will be discarded by the
client anyways.
This PR fixes a bug where the goal state selection would sometimes
select incomplete incremental snapshots on whitespace, leading to an
incorrect "no goals" response. Fixes#6594, a regression that was
originally introduced in 4.11.0 by #4727.
The fundamental cause of #6594 was that the snapshot selection would
always select the first snapshot with a range that contains the cursor
position. For tactics, whitespace had to be included in this range.
However, in the test case of #6594, this meant that the snapshot
selection would also sometimes pick a snapshot before the cursor that
still contains the cursor in its whitespace, but which also does not
necessarily contain all the information needed to produce a correct goal
state. Specifically, at the `InfoTree`-level, when the cursor is in
whitespace, we distinguish competing goal states by their level of
indentation. The snapshot selection did not have access to this
information, so it necessarily had to do the wrong thing in some cases.
This PR fixes the issue by adjusting the snapshot selection for goals to
explicitly account for whitespace and indentation, and refactoring the
language processor architecture to thread enough information through to
the snapshot selection so that it can decide which snapshots to use
without having to force too many tasks, which would destroy
incrementality in goal state requests.
Specifically, this PR makes the following adjustments:
- Refactor `SnapshotTask` to contain both a `Syntax` and a `Range`.
Before, `SnapshotTask`s had a single range that was used both for
displaying file progress information and for selecting snapshots in
server requests. For most snapshots, this range did not include
whitespace, though for tactics it did. Now, the `reportingRange` field
of `SnapshotTask` is intended exclusively for reporting file progress
information, and the `Syntax` is used for selecting snapshots in server
requests. Importantly, the `Syntax` contains the full range information
of the snapshot, i.e. its regular range and its range including
whitespace.
- Adjust all call-sites of `SnapshotTask` to produce a reasonable
`Syntax`.
- Adjust the goal snapshot selection to account for whitespace and
indentation, as the `InfoTree` goal selection does.
- Fix a bug in the snapshot tree tracing that would cause it to render
the `Info` of a snapshot at the wrong location when `trace.Elab.info`
was also set.
This PR is based on #6329.
This PR enables the language server to present multiple disjoint line
ranges as being worked on. Even before parallelism lands, we make use of
this feature to show post-elaboration tasks such as kernel checking on
the first line of a declaration to distinguish them from the final
tactic step.
This PR implements a number of refinements for the auto-implicit inlay
hints implemented in #6768.
Specifically:
- In #6768, there was a bug where the inlay hint edit delay could
accumulate on successive edits, which meant that it could sometimes take
much longer for inlay hints to show up. This PR implements the basic
infrastructure for request cancellation and implements request
cancellation for semantic tokens and inlay hints to resolve the issue.
With this edit delay bug fixed, it made more sense to increase the edit
delay slightly from 2000ms to 3000ms.
- In #6768, we applied the edit delay to every single inlay hint request
in order to reduce the amount of inlay hint flickering. This meant that
the edit delay also had a significant effect on how far inlay hints
would lag behind the file progress bar. This PR adjusts the edit delay
logic so that it only affects requests sent directly after a
corresponding `didChange` notification. Once the edit delay is used up,
all further semantic token requests are responded to without delay, so
that the only latency that affects how far the inlay hints lag behind
the progress bar is how often we emit refresh requests and how long VS
Code takes to respond to them.
- For inlay hints, refresh requests are now emitted 500ms after a
response to an inlay hint request, not 2000ms, which means that after
the edit delay, inlay hints should only lag behind the progress bar by
about up to 500ms. This is justifiable for inlay hints because the
response should be much smaller than e.g. is the case for semantic
tokens.
- In #6768, 'Restart File' did not prompt a refresh, but it does now.
- VS Code does not immediately remove old inlay hints from the document
when they are applied. In #6768, this meant that inlay hints would
linger around for a bit once applied. To mitigate this issue, this PR
adjusts the inlay hint edit delay logic to identify edits sent from the
client as being inlay hint applications, and sets the edit delay to 0ms
for the inlay hint requests following it. This means that inlay hints
are now applied immediately.
- In #6768, hovering over single-letter auto-implicit inlay hints was a
bit finicky because VS Code uses the regular cursor icon on inlay hints,
not the thin text cursor icon, which means that it is easy to put the
cursor in the wrong spot. We now add the separation character (` ` or
`{`) preceding an auto-implicit to the hover range as well, which makes
hovering over inlay hints much smoother.
This PR adds support for plugins to the frontend and server.
Implementation-wise, this adds a `plugins` argument to `runFrontend`,
`processHeader`, amd `importModules`, a `plugins` field to
`SetupImportsResult` and `FileSetupResult`. and a `pluginsPath` field to
`LeanPaths`, and then threads the value through these.
This PR adds preliminary support for inlay hints, as well as support for
inlay hints that denote the auto-implicits of a function. Hovering over
an auto-implicit displays its type and double-clicking the auto-implicit
inserts it into the text document.
This PR is an extension of #3910.
### Known issues
- In VS Code, when inserting an inlay hint, the inlay hint may linger
for a couple of seconds before it disappears. This is a defect of the VS
Code implementation of inlay hints and cannot adequately be resolved by
us.
- When making a change to the document, it may take a couple of seconds
until the inlay hints respond to the change. This is deliberate and
intended to reduce the amount of inlay hint flickering while typing. VS
Code has a mechanism of its own for this, but in my experience it is
still far too sensitive without additional latency.
- Inserting an auto-implicit inlay hint that depends on an auto-implicit
meta-variable causes a "failed to infer binder type" error. We can't
display these meta-variables in the inlay hint because they don't have a
user-displayable name, so it is not clear how to resolve this problem.
- Inlay hints are currently always resolved eagerly, i.e. we do not
support the `textDocument/inlayHint/resolve` request yet. Implementing
support for this request is future work.
### Other changes
- Axioms did not support auto-implicits due to an oversight in the
implementation. This PR ensures they do.
- In order to reduce the amount of inlay hint flickering when making a
change to the document, the language server serves old inlay hints for
parts of the file that have not been processed yet. This requires LSP
request handler state (that sometimes must be invalidated on
`textDocument/didChange`), so this PR introduces the notion of a
stateful LSP request handler.
- The partial response mechanism that we use for semantic tokens, where
we simulate incremental LSP responses by periodically emitting refresh
requests to the client, is generalized to accommodate both inlay hints
and semantic tokens. Additionally, it is made more robust to ensure that
we never emit refresh requests while a corresponding request is in
flight, which causes VS Code to discard the respond of the request, as
well as to ensure that we keep prompting VS Code to send another request
if it spuriously decides not to respond to one of our refresh requests.
- The synthetic identifier of an `example` had the full declaration as
its (non-canonical synthetic) range. Since we need a reasonable position
for the identifier to insert an inlay hint for the auto-implicits of an
`example`, we change the (canonical synthetic) range of the synthetic
identifier to that of the `example` keyword.
- The semantic highlighting request handling is moved to a separate
file.
### Breaking changes
- The semantic highlighting request handler is not a pure request
handler anymore, but a stateful one. Notably, this means that clients
that extend the semantic highlighting of the Lean language server with
the `chainLspRequestHandler` function must now use the
`chainStatefulLspRequestHandler` function instead.
Avoids build time overhead until the option is proven to speed up
average projects. Adds Init.Prelude (many tiny declarations, "worst
case") and Init.List.Sublist (many nontrivial theorems, "best case")
under -DElab.async=true as new benchmarks for tracking.
This PR moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and
renames them to `Std.Channel` and `Std.Mutex`.
Note that the original files are retained and the deprecation is written
manually as we cannot import `Std` from `Init` so this is the only way
to deprecate without a hard breaking change. In particular we do not yet
move `Std.Queue` from `Init` to `Std` both because it needs to be
retained for this deprecation to work but also because it is already
within the `Std` namespace and as such we cannot maintain two copies of
the file at once. After the deprecation period is finished `Std.Queue`
will find a new home in `Std.Data.Queue`.
