From fb3aae75097f030b29e1dfabe7de77bb968e1988 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 27 Jan 2026 10:02:20 +0100 Subject: [PATCH] refactor: remove redundant calls to `DocumentMeta.mod` (#12085) --- src/Lean/Server/FileWorker.lean | 43 +++++++++++---------- src/Lean/Server/FileWorker/SetupFile.lean | 47 +++++------------------ 2 files changed, 33 insertions(+), 57 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 6e113b2477..9f3b37fe39 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -410,29 +410,32 @@ def setupImports message := stderrLine } chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic] - let isSetupError := fileSetupResult.kind matches .importsOutOfDate - || fileSetupResult.kind matches .error .. + let isSetupError := fileSetupResult matches .importsOutOfDate + || fileSetupResult matches .error .. chanOut.sync.send <| .ofMsg <| mkIleanHeaderSetupInfoNotification doc isSetupError -- clear progress notifications in the end chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[] - match fileSetupResult.kind with - | .importsOutOfDate => - return .error { - diagnostics := (← Language.diagnosticsOfHeaderError - "Imports are out of date and must be rebuilt; \ - use the \"Restart File\" command in your editor.") - result? := none - metaSnap := default - } - | .error msg => - return .error { - diagnostics := (← diagnosticsOfHeaderError msg) - result? := none - metaSnap := default - } - | _ => pure () - - let setup := fileSetupResult.setup + let setup ← do + match fileSetupResult with + | .importsOutOfDate => + return .error { + diagnostics := (← Language.diagnosticsOfHeaderError + "Imports are out of date and must be rebuilt; \ + use the \"Restart File\" command in your editor.") + result? := none + metaSnap := default + : Language.Lean.HeaderProcessedSnapshot + } + | .error msg => + return .error { + diagnostics := (← diagnosticsOfHeaderError msg) + result? := none + metaSnap := default + } + | .noLakefile => + pure { name := doc.mod, isModule := header.isModule } + | .success setup => + pure setup -- override cmdline options with file options let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) setup.options.toOptions diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean index 630fcc37b1..35a756819a 100644 --- a/src/Lean/Server/FileWorker/SetupFile.lean +++ b/src/Lean/Server/FileWorker/SetupFile.lean @@ -56,10 +56,10 @@ partial def runLakeSetupFile let exitCode ← lakeProc.wait return ⟨spawnArgs, exitCode, stdout, stderr⟩ -/-- Categorizes possible outcomes of running `lake setup-file`. -/ -inductive FileSetupResultKind where +/-- Result of running `lake setup-file`. -/ +inductive FileSetupResult where /-- File configuration loaded and dependencies updated successfully. -/ - | success + | success (setup : ModuleSetup) /-- No Lake project found, no setup was done. -/ | noLakefile /-- Imports must be rebuilt but `--no-build` was specified. -/ @@ -67,43 +67,16 @@ inductive FileSetupResultKind where /-- Other error during Lake invocation. -/ | error (msg : String) -/-- Result of running `lake setup-file`. -/ -structure FileSetupResult where - /-- Kind of outcome. -/ - kind : FileSetupResultKind - /-- Configuration from a successful setup, or else the default. -/ - setup : ModuleSetup - -def FileSetupResult.ofSuccess (setup : ModuleSetup) : IO FileSetupResult := do return { - kind := FileSetupResultKind.success - setup -} - -def FileSetupResult.ofNoLakefile (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return { - kind := FileSetupResultKind.noLakefile - setup := {name := m.mod, isModule := header.isModule} -} - -def FileSetupResult.ofImportsOutOfDate (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return { - kind := FileSetupResultKind.importsOutOfDate - setup := {name := m.mod, isModule := header.isModule} -} - -def FileSetupResult.ofError (m : DocumentMeta) (header : ModuleHeader) (msg : String) : IO FileSetupResult := do return { - kind := FileSetupResultKind.error msg - setup := {name := m.mod, isModule := header.isModule} -} - /-- Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`. Compilation progress is reported to `handleStderr`. Returns the search path for source files and the options for the file. -/ partial def setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr : String → IO Unit) : IO FileSetupResult := do let some filePath := System.Uri.fileUriToPath? m.uri - | return ← FileSetupResult.ofNoLakefile m header -- untitled files have no lakefile + | return FileSetupResult.noLakefile -- untitled files have no lakefile let lakePath ← determineLakePath if !(← System.FilePath.pathExists lakePath) then - return ← FileSetupResult.ofNoLakefile m header + return FileSetupResult.noLakefile let result ← runLakeSetupFile m lakePath filePath header handleStderr @@ -112,12 +85,12 @@ partial def setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr : match result.exitCode with | 0 => let Except.ok (setup : ModuleSetup) := Json.parse result.stdout >>= fromJson? - | return ← FileSetupResult.ofError m header s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}" + | return FileSetupResult.error s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}" setup.dynlibs.forM loadDynlib - FileSetupResult.ofSuccess setup + return FileSetupResult.success setup | 2 => -- exit code for lake reporting that there is no lakefile - FileSetupResult.ofNoLakefile m header + return FileSetupResult.noLakefile | 3 => -- exit code for `--no-build` - FileSetupResult.ofImportsOutOfDate m header + return FileSetupResult.importsOutOfDate | _ => - FileSetupResult.ofError m header s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}" + return FileSetupResult.error s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"