Commit graph

6 commits

Author SHA1 Message Date
Sebastian Ullrich
5df4e48dc9
feat: importModules without loading environment extensions (#6325)
This PR ensures that environments can be loaded, repeatedly, without
executing arbitrary code
2025-04-02 08:37:11 +00:00
Mac Malone
c9c3366521
feat: lake: support plugins (#7001)
This PR adds support for plugins to Lake. Precompiled modules are now
loaded as plugins rather than via `--load-dynlib`.

Additional plugins can be added through an experimental `plugins`
configuration option. The syntax for specifying this is not yet
convenient, and will be improved in future changes. A parallel `dynlibs`
configuration option has been added for specifying additional dynamic
libraries to build and pass to `--load-dynlib`.

This PR also changes the default directory for `.olean`, `.ilean`, and
module dynamic libraries (i.e., `leanLibDir`) to `lib/lean` instead of
the previous default of `lib`. This avoids potential name clashes
between single module shared libraries and the shared libraries of a
full `lean_lib`.

On non-Windows systems, module dynamic libraries are no longer linked to
their imports or external symbols. Symbols from those libraries are left
unresolved until load time. This avoids nesting these dependencies
within the shared library and means Lake no longer needs to augment the
shared library path to allow Lean to resolve such nested dependencies on
load.
2025-02-14 04:57:31 +00:00
tydeu
4ec3d78afa chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
tydeu
926663505e chore: split up & simplify importModules 2023-08-31 15:37:33 -04:00
Sebastian Ullrich
53d313c74c chore: fix function name 2022-02-28 16:16:22 +01:00
Sebastian Ullrich
8cbd7ccf09 test: reimplement package tests using Lake 2022-02-09 12:21:11 -08:00
Renamed from tests/leanpkg/user_attr_app/UserAttr.lean (Browse further)