max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: run setup-file on lakefiles (#7153)

Browse source 
This PR changes the server to run `lake setup-file` on Lake
configuration files (e.g., `lakefile.lean`).

This is needed to support Lake passing the server its own Lake plugin to
load when elaborating the configuration file.
This commit is contained in:
Mac Malone 2025-02-20 23:04:10 -05:00 • committed by GitHub
parent 36c798964e
commit aea58113cb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Server/FileWorker/SetupFile.lean
View file

@ -110,11 +110,6 @@ partial def setupFile (m : DocumentMeta) (imports : Array Import) (handleStderr
let some filePath := System.Uri.fileUriToPath? m.uri
| return ← FileSetupResult.ofNoLakefile -- untitled files have no lakefile
-- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps
-- NOTE: lake does not exist in stage 0 (yet?)
if filePath.fileName == "lakefile.lean" then
return ← FileSetupResult.ofNoLakefile -- the lakefile itself has no lakefile
let lakePath ← determineLakePath
if !(← System.FilePath.pathExists lakePath) then
return ← FileSetupResult.ofNoLakefile