| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Problem:
The name `server_configurations` is extremely verbose and irritatingly
formal and dogmatic. This overlong name is a constant nuisance when
reading, writing, and coding.
It's also not even correct: these configurations are just as much
"client" configurations as they are "server" configurations.
Solution:
- Rename to a shorter name.
- Leave placeholder files for any old URLs that link to the old
location.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This is partially a bugfix, as such packages would appear to function
correctly because we fell back to `lean --server` -- but that is a lie,
as it means `lake` doesn't control the LSP environment (and specifically
it means that shared objects aren't correctly found for a package which
prebuilds them with prebuildModules).
While we're here, remove said ancient Lean 4 logic for versions no one
has used for years, simplifying the startup (and saving a subprocess).
It'd have been better to fail loudly here rather than falling back to
confusing errors.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Enables workspace symbols for the Lean 4 LSP.
Older versions of Lake (and Lean 4) lack a serve command,
so on those we fallback to the old behavior by directly starting
the LSP.
Closes: Julian/lean.nvim#229
Refs: leanprover/lake#46
|
| |
|
|
|
|
|
|
|
| |
The argument is ignored by the server, but it is useful because it is
shown by `htop`, `ps ax`, etc., so you can figure out which Lean servers
are running.
The lean3ls doesn't require a corresponding change: we use the
`lean-language-server` wrapper, which appends the root directory itself
to the wrapped `lean --server` command.
|
| | |
|
| | |
|
| |
|
