Additions and fixes to the LSP server (work-in-progress)#12731
Closed
wvhulle wants to merge 41 commits intoleanprover:masterfrom
Closed
Additions and fixes to the LSP server (work-in-progress)#12731wvhulle wants to merge 41 commits intoleanprover:masterfrom
wvhulle wants to merge 41 commits intoleanprover:masterfrom
Conversation
This PR adds a `lake install` command that builds and installs package executables to ~/.elan/bin/. The command requires Elan to be installed. Without arguments, it installs all executables defined in the package. Specific targets can be specified to install only those executables. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds git options to `lake install` that allow installing executables directly from a Git repository: - `--git <url>` clones the repository to a temporary directory - `--branch <branch>` checks out a specific branch - `--rev <rev>` checks out a specific commit or tag Examples: lake install --git https://github.com/user/repo lake install --git https://github.com/user/repo --branch dev lake install --git https://github.com/user/repo --rev v1.0.0
Fix mimalloc setup to work in Nix sandbox by using postUnpack. Add elan-compatible package structure with proper rpath configuration. refactor: simplify flake architecture Remove override mechanism and mkLeanPackages abstraction. Use inputs.self.rev directly instead of passing git hash as parameter. Much cleaner architecture without circular dependencies.
- Build stage0 as a separate derivation with isolated source (only stage0/ subtree) so it caches independently of src/ changes - Stage1 (lean-all) depends on stage0 output as PREV_STAGE - Add lake package output as a thin wrapper around lean-all - Remove broken old-glibc dev shells (nixos-18.03/19.03 inputs) - Simplify flake structure: single nixpkgs input, less nesting Build: add build-time version assertion Build: add more binary targets
…r by target fix: remove verbose trace message and group by failed target in lake build summary
… it does not crash
… occurs when linters run without context backup
…gnostics picker when dep failed to build
… on fixed dependency build failures
…related information
… not advertise it in lsp capabilities
wvhulle
changed the title
Author
|
Will be split up |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hey, this is a long PR with additions, fixes related to the Lean LSP server. Apologies for the extend of the changes. However, this branch is based on a fairly recent commit (a few weeks ago, v4.28) but I am willing to rebase or split up later.
I found a couple of issues that were kind of related:
lake install#3423Formatter:
Diagnostics:
Diagnostic levels:
Links in popups:
For more screenshots, see https://github.com/wvhulle/lean4
Fixed:
ifAdded:
lake serveThis PR is a list of changes to get another project working and fixes some other annoyances: Heron.