diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean
index eedfa57f3b..1889755d9c 100644
--- a/Lake/BuildModule.lean
+++ b/Lake/BuildModule.lean
@@ -87,8 +87,7 @@ def OleanAndCTarget.run' (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget
   let oleanTask ← t.mapAsync fun info depTrace => do
     return mixTrace (← computeTrace info.oleanFile) depTrace
   let cTask ← t.mapAsync fun info _ => do
-    let leanTrace ← BuildTrace.compute (← getLean)
-    return mixTrace (← computeTrace info.cFile) leanTrace
+    return mixTrace (← computeTrace info.cFile) (← getLeanTrace)
   return t.withInfo {
     oleanTarget := ActiveTarget.mk self.oleanFile oleanTask
     cTarget := ActiveTarget.mk self.cFile cTask
@@ -100,9 +99,8 @@ def moduleTarget [CheckExists i] [GetMTime i] [ComputeHash i] (info : i)
 (leanFile traceFile : FilePath) (contents : String) (depTarget : BuildTarget x)
 (build : BuildM PUnit) : BuildTarget i :=
   Target.mk info <| depTarget.mapOpaqueAsync fun depTrace => do
-    let leanTrace ← BuildTrace.compute (← getLean)
     let srcTrace : BuildTrace := ⟨Hash.ofString contents, ← getMTime leanFile⟩
-    let fullTrace := leanTrace.mix <| srcTrace.mix depTrace
+    let fullTrace := (← getLeanTrace).mix <| srcTrace.mix depTrace
     let (upToDate, trace) ← fullTrace.check info traceFile
     unless upToDate do
       build
diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean
index 31ab96da3f..0a0e917c62 100644
--- a/Lake/BuildMonad.lean
+++ b/Lake/BuildMonad.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Task
+import Lake.Trace
 import Lake.InstallPath
 
 open System
@@ -20,6 +21,7 @@ constant BuildMethodsRefPointed : PointedType.{0}
 def BuildMethodsRef : Type := BuildMethodsRefPointed.type
 
 structure BuildContext where
+  leanTrace : BuildTrace
   leanInstall : LeanInstall
   lakeInstall : LakeInstall
   methodsRef : BuildMethodsRef
@@ -82,10 +84,13 @@ def getLeanIncludeDir : BuildM FilePath :=
   LeanInstall.includeDir <$> getLeanInstall
 
 def getLeanc : BuildM FilePath :=
-  LeanInstall.leanc  <$> getLeanInstall
+  LeanInstall.leanc <$> getLeanInstall
 
 def getLean : BuildM FilePath :=
-  LeanInstall.lean  <$> getLeanInstall
+  LeanInstall.lean <$> getLeanInstall
+
+def getLeanTrace : BuildM BuildTrace := do
+  BuildContext.leanTrace <$> read
 
 def getLakeInstall : BuildM LakeInstall :=
   BuildContext.lakeInstall <$> read
@@ -107,7 +112,7 @@ def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
 
 end BuildM
 
-export BuildM (getLeanInstall getLeanIncludeDir getLean getLeanc getLakeInstall)
+export BuildM (getLeanInstall getLeanIncludeDir getLean getLeanTrace getLeanc getLakeInstall)
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
 | Except.ok a => a
diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 07ec31e114..7fdd9c4cf4 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -143,8 +143,9 @@ def getInstall : CliM (LeanInstall × LakeInstall) := do
 /-- Perform the given build action using information from CLI. -/
 def runBuildM (x : BuildM α) : CliM α := do
   let (leanInstall, lakeInstall) ← getInstall
+  let leanTrace ← runIO <| computeTrace leanInstall.lean
   runIO <| x.runIn {
-    leanInstall, lakeInstall
+    leanTrace, leanInstall, lakeInstall,
     methodsRef := BuildMethodsRef.mk {
       logInfo  := fun msg => IO.println msg
       logError := fun msg => IO.eprintln msg
@@ -257,8 +258,9 @@ def printPaths (imports : List String := []) : CliM PUnit := do
   if (← runIO' configFile.pathExists noConfigFileCode) then
     let pkg ← loadPkg (← getSubArgs)
     runIO do
+      let leanTrace ← computeTrace leanInstall.lean
       let pkgs ← pkg.buildImportsAndDeps imports |>.runIn {
-        leanInstall, lakeInstall
+        leanTrace, leanInstall, lakeInstall
         methodsRef := BuildMethodsRef.mk {
           logInfo  := fun msg => IO.eprintln msg
           logError := fun msg => IO.eprintln msg