Skip to content

Commit 54096cb

Browse files
committed
chore: adapt to Lake API changes
1 parent 9fb8fc2 commit 54096cb

File tree

1 file changed

+6
-7
lines changed

1 file changed

+6
-7
lines changed

Cache/IO.lean

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -138,13 +138,14 @@ def _root_.Lean.SearchPath.relativize (sp : SearchPath) : IO SearchPath := do
138138

139139
/--
140140
Detects the directory Lake uses to cache artifacts.
141-
This is very sensitive to changes in `Lake.Env.compute`.
141+
This is very sensitive to changes in `Lake.Env.computeCache`.
142142
-/
143143
def getLakeArtifactDir? : IO (Option FilePath) := do
144144
let elan? ← Lake.findElanInstall?
145-
let toolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD Lean.toolchain
146-
let .ok cache ← Lake.Env.compute.getCache? elan? toolchain |>.toBaseIO
147-
| return none
145+
let toolchain ← Lake.Env.computeToolchain
146+
let cache ← Lake.Env.computeCache elan? toolchain
147+
if cache.isDisabled then
148+
return none
148149
let artifactDir := cache.artifactDir
149150
if (← artifactDir.pathExists) then
150151
return artifactDir
@@ -320,9 +321,7 @@ This is sensitive to changes in `Lake.readTraceFile`.
320321
def readTraceOutputs (path : FilePath) : BaseIO (Option Lake.ModuleOutputHashes) := do
321322
let .ok contents ← IO.FS.readFile path |>.toBaseIO
322323
| return none
323-
if Lake.Hash.ofString? contents.trim |>.isSome then
324-
return none
325-
let .ok (data : Lake.BuildMetadata) := Json.parse contents >>= fromJson?
324+
let .ok data := Lake.BuildMetadata.parse contents
326325
| return none
327326
let some outs := data.outputs?
328327
| return none

0 commit comments

Comments
 (0)