diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean
index 5710f483aa..7aa9b9523b 100644
--- a/Lake/BuildTrace.lean
+++ b/Lake/BuildTrace.lean
@@ -48,3 +48,13 @@ structure LeanTrace where
   hash : Hash
   mtime : MTime
   deriving Inhabited
+
+namespace LeanTrace
+
+def fromHash (hash : Hash) : LeanTrace :=
+  LeanTrace.mk hash 0
+
+def fromMTime (mtime : MTime) : LeanTrace :=
+  LeanTrace.mk 0 mtime
+
+end LeanTrace