From aea58113cbcf97b68285441b08d210aa729caeb7 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 20 Feb 2025 23:04:10 -0500 Subject: [PATCH] feat: run `setup-file` on lakefiles (#7153) 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. --- src/Lean/Server/FileWorker/SetupFile.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean index bb06e313ed..5ae2dcdd4c 100644 --- a/src/Lean/Server/FileWorker/SetupFile.lean +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -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