From 0e0810c0229ce7738addbe232b8d5102d53b89ec Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 19 Mar 2024 21:46:15 +0100 Subject: [PATCH] fix: highlighting facet dependencies Rebuild example JSON at the right times. We previously depended on the dependencies of our modules, rather than the modules themselves. --- lakefile.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index e42d4a8..cd6a59d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -28,13 +28,13 @@ module_facet examples mod : FilePath := do | error "The subverso-extract executable was not found" let exeJob ← extract.exe.fetch - let modJob ← mod.leanArts.fetch + let modJob ← mod.olean.fetch let buildDir := ws.root.buildDir let hlFile := mod.filePath (buildDir / "examples") "json" exeJob.bindAsync fun exeFile exeTrace => - modJob.bindSync fun () modTrace => do + modJob.bindSync fun _oleanPath modTrace => do let depTrace := mixTrace exeTrace modTrace let trace ← buildFileUnlessUpToDate hlFile depTrace do logStep s!"Exporting highlighted example JSON for '{mod.name}'" @@ -61,5 +61,5 @@ package_facet examples pkg : FilePath := do let buildDir := ws.root.buildDir let hlDir := buildDir / "examples" libJobs.bindSync fun () trace => do - logStep s!"Highlighted code written to '{hlDir}'" + logInfo s!"Highlighted code written to '{hlDir}'" pure (hlDir, trace)