From 6b3f40f82666b1ec6b2ea2868e8948353a075143 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Wed, 19 Feb 2025 14:16:12 +0100
Subject: [PATCH] Use `buildUnlessUpToDate?` to avoid building Rust code when
 fetched

---
 lakefile.lean | 38 +++++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 17 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index f7809bf..83e9701 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,30 +32,34 @@ extern_lib ffi pkg := do
 
 extern_lib egg_for_lean pkg := do
   pkg.afterBuildCacheAsync do
-    proc {
-      cmd := "cargo",
-      args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
-      cwd := pkg.dir / "Rust" / "Egg"
-    }
-    let name := nameToStaticLib "egg_for_lean"
-    let srcPath := pkg.dir / "Rust" / "Egg" / "target" / "release" / name
-    IO.FS.createDirAll pkg.nativeLibDir
-    let tgtPath := pkg.nativeLibDir / name
-    IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
+    let name      := nameToStaticLib "egg_for_lean"
+    let srcPath   := pkg.dir / "Rust" / "Egg" / "target" / "release" / name
+    let tgtPath   := pkg.nativeLibDir / name
+    let traceFile := pkg.buildDir / "rust" / "egg.trace"
+    let _ ← buildUnlessUpToDate? traceFile (← getTrace) traceFile do
+      proc {
+        cmd := "cargo",
+        args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
+        cwd := pkg.dir / "Rust" / "Egg"
+      }
+      IO.FS.createDirAll pkg.nativeLibDir
+      IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
     return pure tgtPath
 
 extern_lib slotted_for_lean pkg := do
   pkg.afterBuildCacheAsync do
-    proc {
-      cmd := "cargo",
-      args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
-      cwd := pkg.dir / "Rust" / "Slotted"
-    }
     let name := nameToStaticLib "slotted_for_lean"
     let srcPath := pkg.dir / "Rust" / "Slotted" / "target" / "release" / name
-    IO.FS.createDirAll pkg.nativeLibDir
     let tgtPath := pkg.nativeLibDir / name
-    IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
+    let traceFile := pkg.buildDir / "rust" / "slotted.trace"
+    let _ ← buildUnlessUpToDate? traceFile (← getTrace) traceFile do
+      proc {
+        cmd := "cargo",
+        args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
+        cwd := pkg.dir / "Rust" / "Slotted"
+      }
+      IO.FS.createDirAll pkg.nativeLibDir
+      IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
     return pure tgtPath
 
 @[test_driver]