Skip to content

lean-rs v0.1.13

Choose a tag to compare

@jcreinhold jcreinhold released this 26 May 12:06

Lake-manifest transitive search paths in shims-only sessions

lean-rs-host session imports now add .olean search paths for packages listed in the project's
lake-manifest.json. Shims-only sessions opened with LeanHost::load_shims_only() can import modules from
mathlib, batteries, aesop, and other transitive Lake dependencies without requiring a user :shared dylib.