Skip to content

Commit

Permalink
fix: highlighting facet dependencies
Browse files Browse the repository at this point in the history
Rebuild example JSON at the right times. We previously depended on the
dependencies of our modules, rather than the modules themselves.
  • Loading branch information
david-christiansen committed Mar 19, 2024
1 parent ec2ba38 commit 0e0810c
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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}'"
Expand All @@ -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)

0 comments on commit 0e0810c

Please sign in to comment.