chore: lake: revert use of Lake plugin (#7608)

This PR removes the use of the Lake plugin in the Lake build and in
configuration files.

With #7399, the plugin is no longer necessary and may be the source of
some persistent intermittent Lake test failures.

src/lake/Lake/CLI/Serve.lean

@@ -45,8 +45,6 @@ def setupFile
       paths := {
         oleanPath := loadConfig.lakeEnv.leanPath
         srcPath := loadConfig.lakeEnv.leanSrcPath
-        loadDynlibPaths := #[]
-        pluginPaths := #[loadConfig.lakeEnv.lake.sharedLib]
       }
       setupOptions := ⟨∅⟩
       : FileSetupInfo
@@ -59,15 +57,11 @@ 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
     let {dynlibs, plugins} ←
       MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
         ws.runBuild (buildImportsAndDeps path imports) buildConfig
-    let plugins :=
-      if usesLake then plugins.push ws.lakeEnv.lake.sharedLib else plugins
     let paths : LeanPaths := {
       oleanPath := ws.leanPath
       srcPath := ws.leanSrcPath

src/lake/tests/setupFile/test.sh

@@ -6,11 +6,11 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Test `setup-file` functionality
 #---
 
-# Test that, by default. no plugins are used.
+# Test that, by default, no plugins are used.
 $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, by default, no dynlibs are used.
+$LAKE setup-file bogus Foo | grep -F --color '"loadDynlibPaths":[]'
 
 # Test that `setup-file` on an invalid Lean configuration file succeeds.
 $LAKE -f invalid.lean setup-file invalid.lean Lake

src/lakefile.toml.in

@@ -63,7 +63,6 @@ globs = [
 ]
 libName = "${LAKE_LIB_PREFIX}Lake"
 defaultFacets = ["static", "static.export"]
-moreLeanArgs = ["--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"

src/stdlib.make.in

@@ -62,7 +62,7 @@ Lean: Std
 
 Lake:
 # lake is in its own subdirectory, so must adjust relative paths...
-	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" LEAN_OPTS+="--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}" EXTRA_SRC_ROOTS=LakeMain.lean
+	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
 
 endif