fix: lake: setup-file on an invalid Lean config (#7182)

This PR makes `lake setup-file` succeed on an invalid Lean configuration
file.

The server will disable interactivity if `setup-file` fails. When
editing the workspace configuration file, this behavior has the prior
effect of making the configuration file noninteractive if saved with an
invalid configuration.

src/lake/Lake/CLI/Serve.lean

@@ -9,10 +9,11 @@ import Lake.Build
 import Lake.Util.MainM
 import Lean.Util.FileSetupInfo
 
-namespace Lake
 open Lean
 open System (FilePath)
 
+namespace Lake
+
 /-- Exit code to return if `setup-file` cannot find the config file. -/
 def noConfigFileCode : ExitCode := 2
 
@@ -33,7 +34,24 @@ def setupFile
   (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
   (buildConfig : BuildConfig := {})
 : MainM PUnit := do
-  if (← configFileExists loadConfig.configFile) then
+  let configFile ← realConfigFile loadConfig.configFile
+  let isConfig := EIO.catchExceptions (h := fun _ => pure false) do
+    let path ← IO.FS.realPath path
+    return configFile.normalize == path.normalize
+  if configFile.toString.isEmpty then
+    exit noConfigFileCode
+  else if (← isConfig) then
+    IO.println <| Json.compress <| toJson {
+      paths := {
+        oleanPath := loadConfig.lakeEnv.leanPath
+        srcPath := loadConfig.lakeEnv.leanSrcPath
+        loadDynlibPaths := #[]
+        pluginPaths := #[loadConfig.lakeEnv.lake.sharedLib]
+      }
+      setupOptions := ⟨∅⟩
+      : FileSetupInfo
+    }
+  else
     if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
       IO.eprint errLog
       IO.eprintln s!"Failed to configure the Lake workspace. Please restart the server after fixing the error above."
@@ -41,6 +59,7 @@ def setupFile
     let outLv := buildConfig.verbosity.minLogLv
     let ws ← MainM.runLoggerIO (minLv := outLv) (ansiMode := .noAnsi) do
       loadWorkspace loadConfig
+    -- Imperfect heuristic for determine when the Lake plugin is needed.
     let usesLake := imports.any (·.startsWith "Lake")
     let imports := imports.foldl (init := #[]) fun imps imp =>
       if let some mod := ws.findModule? imp.toName then imps.push mod else imps
@@ -67,8 +86,6 @@ def setupFile
       setupOptions
       : FileSetupInfo
     }
-  else
-    exit noConfigFileCode
 
 /--
 Start the Lean LSP for the `Workspace` loaded from `config`

src/lake/Lake/Load/Package.lean

@@ -30,6 +30,25 @@ def configFileExists (cfgFile : FilePath) : BaseIO Bool :=
     let tomlFile := cfgFile.addExtension "toml"
     leanFile.pathExists <||> tomlFile.pathExists
 
+/--
+Returns the absolute path of the configuration file (if it exists).
+Otherwise, returns an empty string.
+-/
+def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
+  if cfgFile.extension.isSome then
+    realPath cfgFile
+  else
+    let realLeanFile ← realPath (cfgFile.addExtension "lean")
+    if realLeanFile.toString.isEmpty then
+      realPath (cfgFile.addExtension "toml")
+    else
+      return realLeanFile
+where
+  @[inline] realPath file := do
+    match (← (IO.FS.realPath file).toBaseIO) with
+    | .ok path => return if (← path.pathExists) then path else ""
+    | _ => return ""
+
 /--
 Loads a Lake package configuration (either Lean or TOML).
 The resulting package does not yet include any dependencies.

src/lake/tests/setupFile/clean.sh

@@ -0,0 +1 @@
+rm -f lake-manifest.json

src/lake/tests/setupFile/invalid.lean

@@ -0,0 +1 @@
+foo

src/lake/tests/setupFile/test.sh

@@ -11,3 +11,6 @@ $LAKE setup-file bogus Foo | grep -F --color '"pluginPaths":[]'
 
 # Test that a Lake import uses the Lake plugin.
 $LAKE setup-file bogus Lake | (grep -F --color '"pluginPaths":[]' && exit 1 || true)
+
+# Test that `setup-file` on an invalid Lean configuration file succeeds.
+$LAKE -f invalid.lean setup-file invalid.lean Lake