From 131b458236cdd1d2315b499ee67c801faa660953 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 20 Mar 2025 20:59:43 -0400
Subject: [PATCH] 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     | 6 ------
 src/lake/tests/setupFile/test.sh | 6 +++---
 src/lakefile.toml.in             | 1 -
 src/stdlib.make.in               | 2 +-
 4 files changed, 4 insertions(+), 11 deletions(-)

diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
index ddbcfdcadb..fc36f47316 100644
--- a/src/lake/Lake/CLI/Serve.lean
+++ b/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
diff --git a/src/lake/tests/setupFile/test.sh b/src/lake/tests/setupFile/test.sh
index b42dfe18fd..58c944e701 100755
--- a/src/lake/tests/setupFile/test.sh
+++ b/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
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index 8aed37f200..e856088eed 100644
--- a/src/lakefile.toml.in
+++ b/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"
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 92fb020125..659f08c2ff 100644
--- a/src/stdlib.make.in
+++ b/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