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.

(cherry picked from commit 131b458)

Author: tydeu

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

@@ -44,4 +44,3 @@ globs = [
 [[lean_lib]]
 name = "Lake"
 srcDir = "lake"
-moreLeanArgs = ["--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]

src/stdlib.make.in

@@ -101,7 +101,7 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR
 
 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
 
 ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/temp/libLake.a.export
 	@echo "[    ] Building $@"