fix: trace lake jobs properly

leanprover · Oct 8, 2023 · 3a9cfab · 3a9cfab
1 parent fa8c9d7
commit 3a9cfab
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -31,11 +31,12 @@ module_facet docs (mod) : FilePath := do
   let buildDir := (← getWorkspace).root.buildDir
   -- Build all documentation imported modules
   let imports ← mod.imports.fetch
-  imports.forM fun mod => discard <| fetch <| mod.facet `docs
+  let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
   let docFile := mod.filePath (buildDir / "doc") "html"
+  depDocJobs.bindAsync fun _ depDocTrace => do
   exeJob.bindAsync fun exeFile exeTrace => do
   modJob.bindSync fun _ modTrace => do
-    let depTrace := exeTrace.mix modTrace
+    let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
     let trace ← buildFileUnlessUpToDate docFile depTrace do
       logStep s!"Documenting module: {mod.name}"
       proc {