max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: Lean shared lib path before the workspace's (#7796)

Browse source 
This PR moves Lean's shared library path before the workspace's in
Lake's augmented environment (e.g., `lake env`).

Lean's comes first because Lean needs to load its own shared libraries
from this path. Giving the workspace greater precedence can break this
(e.g., when bootstrapping), This change does not effect shared library
path on Windows (i.e., `PATH`) because such shared libraries are already
prioritized by being located next to the executable.
This commit is contained in:
Mac Malone 2025-04-02 21:24:11 -04:00 • committed by GitHub
parent 12ec466aa6
commit 01f3bbb2de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/lake/Lake/Config/Workspace.lean
View file

@ -206,9 +206,13 @@ def augmentedLeanSrcPath (self : Workspace) : SearchPath :=
/-
The detected `sharedLibPathEnv` value of the environment augmented with
the workspace's `libPath` and Lean installation's shared library directories.
The order is Lean's, the workspace's, and then the enviroment's.
Lean's comes first because Lean needs to load its own shared libraries from this path.
Giving the workspace greater precedence can break this (e.g., when bootstrapping),
-/
def augmentedSharedLibPath (self : Workspace) : SearchPath :=
self.sharedLibPath ++ self.lakeEnv.sharedLibPath
self.lakeEnv.lean.sharedLibPath ++ self.sharedLibPath ++ self.lakeEnv.initSharedLibPath
/--
The detected environment augmented with Lake's and the workspace's paths.