ad5ec0e196
This PR adds the ability to specify a name for the initialization
function of a Lean plugin on load.
* The `Lean.loadPlugin` API has gained a `initFn?` argument that
defaults to `none`. When `none`, the initialization function name will
be inferred from the shared library's name (as before).
* The CLI `--plugin` option can now have a initialization function
specified via `--plugin=path:initFn`.
* The `--setup` JSON configuration now also accepts`{"path": ...,
"initFn": ...}` for plugins.
|
||
|---|---|---|
| .. | ||
| clean.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||
| run_test.sh | ||
| test.lean | ||
| testEnv.lean | ||
| testEnvUse.lean | ||
| UserEnvPlugin.lean | ||
| UserPlugin.lean | ||