From e68c6a38fb7ae749eee1dcb516f156ee577b5f9d Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 29 May 2025 22:02:35 -0400
Subject: [PATCH] feat: lake: relative paths for Lean build messages (#8539)

This PR changes Lake to use relative path for the Lean messages produced
by a module build. This makes the message portable across different
machines, which is useful for Mathlib's cache.
---
 src/lake/Lake/Build/Actions.lean | 4 +++-
 src/lake/Lake/Build/Module.lean  | 2 +-
 src/lake/Lake/Config/Module.lean | 6 ++++++
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index a36c46efda..0a47f65c91 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -7,6 +7,7 @@ prelude
 import Lake.Config.Dynlib
 import Lake.Util.Proc
 import Lake.Util.NativeLib
+import Lake.Util.FilePath
 import Lake.Util.IO
 
 /-! # Common Build Actions
@@ -19,7 +20,7 @@ open Lean hiding SearchPath
 namespace Lake
 
 def compileLeanModule
-  (leanFile : FilePath)
+  (leanFile relLeanFile : FilePath)
   (oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
   (leanPath : SearchPath := []) (rootDir : FilePath := ".")
   (dynlibs plugins : Array Dynlib := #[])
@@ -57,6 +58,7 @@ def compileLeanModule
       if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
         unless txt.isEmpty do
           logInfo s!"stdout:\n{txt}"
+        let msg := {msg with fileName := mkRelPathString relLeanFile}
         logSerialMessage msg
         return txt
       else if txt.isEmpty && ln.isEmpty then
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index c49fc5ce7f..9aa61060ae 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -280,7 +280,7 @@ def Module.recBuildLean (mod : Module) : FetchM (Job Unit) := do
     addTrace srcTrace
     setTraceCaption s!"{mod.name.toString}:leanArts"
     let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace.mtime) mod (← getTrace) mod.traceFile do
-      compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile mod.bcFile?
+      compileLeanModule mod.leanFile mod.relLeanFile mod.oleanFile mod.ileanFile mod.cFile mod.bcFile?
         (← getLeanPath) mod.rootDir dynlibs plugins
         (mod.weakLeanArgs ++ mod.leanArgs) (← getLean)
       mod.clearOutputHashes
diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean
index 799ef8ce94..d668017646 100644
--- a/src/lake/Lake/Config/Module.lean
+++ b/src/lake/Lake/Config/Module.lean
@@ -82,6 +82,12 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def leanFile (self : Module) : FilePath :=
   self.srcPath "lean"
 
+@[inline] def relLeanFile (self : Module) : FilePath :=
+  if let some relPath := self.leanFile.toString.dropPrefix? self.pkg.dir.toString then
+    FilePath.mk (relPath.drop 1).toString -- remove leading `/`
+  else
+    self.leanFile
+
 @[inline] def leanLibPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.leanLibDir ext