Auto-compilation & -setup of dependencies on file worker startup #263
Conversation
This file contains 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
Kha
commented
Jan 14, 2021
src/Leanpkg.lean
Outdated
| @@ -18,6 +18,24 @@ def readManifest : IO Manifest := do | |||
| def writeManifest (manifest : Lean.Syntax) (fn : String) : IO Unit := do | |||
| IO.FS.writeFile fn manifest.reprint.get! | |||
|
|
|||
| def lockFileName := "build/.lock" | |||
|
|
|||
| partial def withLockFile (x : IO α) : IO α := | |||
Kha
commented
Jan 18, 2021
| let stderr ← IO.ofExcept stderr.get | ||
| if (← leanpkgProc.wait) == 0 then | ||
| match stdout.split (· == '\n') with | ||
| | [leanPath, leanSrcPath] => searchPathRef.set (← parseSearchPath leanPath (← getBuiltinSearchPath)) |
There was a problem hiding this comment.
@leodemoura @Vtec234 now with LEAN_SRC_PATH (unused so far)
will otherwise be constantly retriggered by documentSymbol in Emacs
…RC_PATH (unused as of yet)
|
Nix support is working, so this should be ready to go: |
ChrisHughes24
pushed a commit
to ChrisHughes24/lean4
that referenced
this pull request
Dec 2, 2022
- split Mathlib/Lean/Expr into multiple files. - implement a version of replaceRecM that correctly instantiates free vars. - some additonal Expr functions These are prereqs of leanprover#234 and leanprover#229 Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR extends the file worker to call
leanpkg print-path <imports>on startup (if there is aleanpkg.tomlin the workspace root), which will configure the current package (compiling all dependencies), compile the specified (local) modules, and print the correspondingLEAN_PATHto stdout, where it is picked up by the file worker. While running, the latest stderr line of leanpkg is reported as an "information" message.Note that this won't work when editing Lean's own
src/because there is noleanpkgbinary in stage 0.There are two more minor server changes included:
didOpen(i.e. when we know the path of the current file) is reported as a diagnostic, which is great for displaying the result of a failed leanpkg invocationdidChangerequests restart a crashed file worker now; without this change, thedocumentSymbolrequest threw my Emacs into a restart loopFeel free to give this a try, perhaps even on Windows if someone feels courageous!
How to test:
tests/leanpkg/b/as a workspace folderB.leanin there should automatically compile & findB/Foo.leanas well as the dependency../aB/Foo.lean, e.g. introducing the commented delay or an error; restarting the worker forB.leanshould make the change visible thereTODO:
flake.nixin the root instead