From 9dcd2ad2a33d41d2f3f8d42c1de5f1d864c80253 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 1 Oct 2024 22:22:40 -0400
Subject: [PATCH] fix:  `--no-cache` on server `DependencyBuildMode.never`
 (#5583)

Have the server disable Lake build cache fetches (via `--no-cache`) on
time-sensitive file opens (i.e.,, `DependencyBuildMode.never`).
---
 src/Lean/Server/FileWorker/SetupFile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean
index 4c972c5711..15c5e165ff 100644
--- a/src/Lean/Server/FileWorker/SetupFile.lean
+++ b/src/Lean/Server/FileWorker/SetupFile.lean
@@ -28,7 +28,7 @@ partial def runLakeSetupFile
     : IO LakeSetupFileOutput := do
   let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module)
   if m.dependencyBuildMode matches .never then
-    args := args.push "--no-build"
+    args := args.push "--no-build" |>.push "--no-cache"
   let spawnArgs : Process.SpawnArgs := {
     stdin  := Process.Stdio.null
     stdout := Process.Stdio.piped