From 3a9cfabe5818692ce2b42214f0e9113263d00743 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 8 Oct 2023 11:30:11 +0200 Subject: [PATCH] fix: trace lake jobs properly --- lakefile.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 0a3027f..8f33e46 100644 --- 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 {