feat: frontend & server support for plugins (#6893)

This PR adds support for plugins to the frontend and server.

Implementation-wise, this adds a `plugins` argument to `runFrontend`,
`processHeader`, amd `importModules`, a `plugins` field to
`SetupImportsResult` and `FileSetupResult`. and a `pluginsPath` field to
`LeanPaths`, and then threads the value through these.

src/Lean/Elab/Frontend.lean

@@ -143,13 +143,14 @@ def runFrontend
     (ileanFileName? : Option String := none)
     (jsonOutput : Bool := false)
     (errorOnKinds : Array Name := #[])
+    (plugins : Array System.FilePath := #[])
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
   let opts := Language.Lean.internal.cmdlineSnapshots.setIfNotSet opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
-  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
+  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel, plugins }) none ctx
   let snaps := Language.toSnapshotTree snap
   let severityOverrides := errorOnKinds.foldl (·.insert · .error) {}
   let hasErrors ← snaps.runAndReport opts jsonOutput severityOverrides

src/Lean/Elab/Import.lean

@@ -18,10 +18,11 @@ def headerToImports (header : Syntax) : Array Import :=
     { module := id, runtimeOnly := runtime }
 
 def processHeader (header : Syntax) (opts : Options) (messages : MessageLog)
-    (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (leakEnv := false)
+    (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0)
+    (plugins : Array System.FilePath := #[]) (leakEnv := false)
     : IO (Environment × MessageLog) := do
   try
-    let env ← importModules (leakEnv := leakEnv) (headerToImports header) opts trustLevel
+    let env ← importModules (leakEnv := leakEnv) (headerToImports header) opts trustLevel plugins
     pure (env, messages)
   catch e =>
     let env ← mkEmptyEnvironment

src/Lean/Environment.lean

@@ -19,6 +19,7 @@ import Lean.Util.FindExpr
 import Lean.Util.Profile
 import Lean.Util.InstantiateLevelParams
 import Lean.PrivateName
+import Lean.LoadDynlib
 
 /-!
 # Note [Environment Branches]
@@ -1510,11 +1511,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
 
 @[export lean_import_modules]
 def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0)
-    (leakEnv := false) : IO Environment := profileitIO "import" opts do
+    (plugins : Array System.FilePath := #[]) (leakEnv := false)
+    : IO Environment := profileitIO "import" opts do
   for imp in imports do
     if imp.module matches .anonymous then
       throw <| IO.userError "import failed, trying to import module with anonymous name"
   withImporting do
+    plugins.forM Lean.loadPlugin
     let (_, s) ← importModulesCore imports |>.run
     finalizeImport (leakEnv := leakEnv) s imports opts trustLevel
 

src/Lean/Language/Lean.lean

@@ -243,6 +243,8 @@ structure SetupImportsResult where
   opts : Options
   /-- Kernel trust level. -/
   trustLevel : UInt32 := 0
+  /-- Lean plugins to load as part of the environment setup. -/
+  plugins : Array System.FilePath := #[]
 
 /-- Performance option used by cmdline driver. -/
 register_builtin_option internal.cmdlineSnapshots : Bool := {
@@ -414,7 +416,7 @@ where
       let startTime := (← IO.monoNanosNow).toFloat / 1000000000
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
       let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) stx setup.opts .empty
-        ctx.toInputContext setup.trustLevel
+        ctx.toInputContext setup.trustLevel setup.plugins
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then

src/Lean/Server/FileWorker.lean

@@ -354,6 +354,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch
   return .ok {
     mainModuleName
     opts
+    plugins := fileSetupResult.plugins
   }
 
 /- Worker initialization sequence. -/

src/Lean/Server/FileWorker/SetupFile.lean

@@ -71,30 +71,35 @@ structure FileSetupResult where
   srcSearchPath : SearchPath
   /-- Additional options from successful setup, or else empty. -/
   fileOptions   : Options
+  /-- Lean plugins from successful setup, or else empty. -/
+  plugins       : Array System.FilePath
 
 def FileSetupResult.ofSuccess (pkgSearchPath : SearchPath) (fileOptions : Options)
-    : IO FileSetupResult := do return {
+    (plugins : Array System.FilePath) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.success
   srcSearchPath := ← initSrcSearchPath pkgSearchPath,
-  fileOptions
+  fileOptions, plugins
 }
 
 def FileSetupResult.ofNoLakefile : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.noLakefile
   srcSearchPath := ← initSrcSearchPath
   fileOptions   := Options.empty
+  plugins       := #[]
 }
 
 def FileSetupResult.ofImportsOutOfDate : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.importsOutOfDate
   srcSearchPath := ← initSrcSearchPath
   fileOptions   := Options.empty
+  plugins       := #[]
 }
 
 def FileSetupResult.ofError (msg : String) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.error msg
   srcSearchPath := ← initSrcSearchPath
   fileOptions   := Options.empty
+  plugins       := #[]
 }
 
 /-- Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`.
@@ -124,7 +129,8 @@ partial def setupFile (m : DocumentMeta) (imports : Array Import) (handleStderr
     initSearchPath (← getBuildDir) info.paths.oleanPath
     info.paths.loadDynlibPaths.forM loadDynlib
     let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized
-    FileSetupResult.ofSuccess pkgSearchPath info.setupOptions.toOptions
+    let pluginPaths ← info.paths.pluginPaths.mapM realPathNormalized
+    FileSetupResult.ofSuccess pkgSearchPath info.setupOptions.toOptions pluginPaths
   | 2 => -- exit code for lake reporting that there is no lakefile
     FileSetupResult.ofNoLakefile
   | 3 => -- exit code for `--no-build`

src/Lean/Util/Paths.lean

@@ -18,6 +18,7 @@ structure LeanPaths where
   oleanPath       : SearchPath
   srcPath         : SearchPath
   loadDynlibPaths : Array FilePath := #[]
+  pluginPaths     : Array FilePath := #[]
   deriving ToJson, FromJson
 
 def initSrcSearchPath (pkgSearchPath : SearchPath := ∅) : IO SearchPath := do

src/lake/Lake/CLI/Serve.lean

@@ -49,6 +49,7 @@ def setupFile
       oleanPath := ws.leanPath
       srcPath := ws.leanSrcPath
       loadDynlibPaths := dynlibs
+      pluginPaths := #[]
       : LeanPaths
     }
     let setupOptions : LeanOptions ← do

src/util/shell.cpp

@@ -336,6 +336,7 @@ extern "C" object * lean_run_frontend(
     object * ilean_filename,
     uint8_t  json_output,
     object * error_kinds,
+    object * plugins,
     object * w
 );
 pair_ref<elab_environment, object_ref> run_new_frontend(
@@ -360,6 +361,7 @@ pair_ref<elab_environment, object_ref> run_new_frontend(
         oilean_file_name,
         json_output,
         error_kinds.to_obj_arg(),
+        mk_empty_array(),
         io_mk_world()
     ));
 }