Commit graph

5 commits

Author SHA1 Message Date
Mac Malone
a41fb49e25
feat: smarter plugin loading (#7090)
This PR strips `lib` prefixes and `_shared` suffixes from plugin names.
It also moves most of the dynlib processing code to Lean to make such
preprocessing more standard.
2025-02-18 23:03:52 +00:00
Mac Malone
ac1197ff59
feat: Lean.loadPlugin (#6130)
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>
2024-11-27 09:56:31 +00:00
Henrik Böving
23e49eb519 perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Leonardo de Moura
02c4e548df feat: replace constant with opaque 2022-06-14 17:02:59 -07:00
tydeu
a3250dc44b feat: expose --load-dynlib functionality to Lean code 2021-12-15 08:26:48 +00:00