From 01f3bbb2deab89b4849a8440346a7930ff156787 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 2 Apr 2025 21:24:11 -0400 Subject: [PATCH] fix: lake: Lean shared lib path before the workspace's (#7796) 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. --- src/lake/Lake/Config/Workspace.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index 153cdfaa87..7e8b8a75b3 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -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.