diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 9f3b72982af6..d68b87110310 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/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 diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index 3c9fdc1f3e5e..679980771e44 100644 --- a/src/Lean/Elab/Import.lean +++ b/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 diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e5688de3f1e9..64c736691830 100644 --- a/src/Lean/Environment.lean +++ b/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] @@ -1406,11 +1407,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 diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 33a0807bee97..5db07a2de79c 100644 --- a/src/Lean/Language/Lean.lean +++ b/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 diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 2ee0c9e1ba59..9000bcff68bb 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -331,6 +331,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch return .ok { mainModuleName opts + plugins := fileSetupResult.plugins } /- Worker initialization sequence. -/ diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean index 15c5e165ff0f..281ecd077c0a 100644 --- a/src/Lean/Server/FileWorker/SetupFile.lean +++ b/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` diff --git a/src/Lean/Util/Paths.lean b/src/Lean/Util/Paths.lean index 70420a10b61e..9a0e77adc74e 100644 --- a/src/Lean/Util/Paths.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 4598b7206e94..ab9056beafd7 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/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 diff --git a/src/util/shell.cpp b/src/util/shell.cpp index ff1542ada9f0..1283d8cf76ba 100644 --- a/src/util/shell.cpp +++ b/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 run_new_frontend( @@ -360,6 +361,7 @@ pair_ref run_new_frontend( oilean_file_name, json_output, error_kinds.to_obj_arg(), + mk_empty_array(), io_mk_world() )); }