From 6a3d299378bc2c14aeae69733a8d0b061b2d9f94 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 16 Sep 2021 18:33:38 -0400 Subject: [PATCH] fix: log trace computation errors at `FileTarget` resolves leanprover/lake#7 --- Lake/BuildTarget.lean | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index 0f622d6a3b..b239c6fc15 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -27,7 +27,22 @@ abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace /-- A `BuildTarget` that produces a file. -/ abbrev FileTarget := BuildTarget FilePath -instance : Coe FilePath FileTarget := ⟨Target.computeAsync⟩ + +namespace FileTarget + +variable [ComputeTrace FilePath m BuildTrace] [MonadLiftT m BuildM] + +def computeSync (path : FilePath) : FileTarget := + Target.mk path do pure <$> try liftM <| computeTrace path catch e => + BuildM.logError (toString e); throw e + +def computeAsync (path : FilePath) : FileTarget := + Target.mk path do async <| try liftM <| computeTrace path catch e => + BuildM.logError (toString e); throw e + +instance : Coe FilePath FileTarget := ⟨computeAsync⟩ + +end FileTarget -- ## Active