ac1197ff59
This PR adds `Lean.loadPlugin` which exposes functionality similar to the `lean` executable's `--plugin` option to Lean code. This will allow custom Lean frontends (e.g., Lake, the Lean language server) to also load plugins. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
8 lines
206 B
Text
8 lines
206 B
Text
import Lean.LoadDynlib
|
|
|
|
def main (args : List String) : IO UInt32 := do
|
|
let plugin :: [] := args
|
|
| IO.println "Usage: lean --run test.lean <plugin>"
|
|
return 1
|
|
Lean.loadPlugin plugin
|
|
return 0
|