From 3caf6e83f81befd8dc7c3920aca9630a64da8ff2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 May 2020 14:38:44 +0200 Subject: [PATCH] feat: IO.runMeta: print traces (by default) --- src/Init/Lean/Meta/Basic.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean index 5024cf1b28..557f89fecc 100644 --- a/src/Init/Lean/Meta/Basic.lean +++ b/src/Init/Lean/Meta/Basic.lean @@ -853,7 +853,13 @@ open Lean open Lean.Meta /-- Helper function for running `MetaM` methods in attributes -/ -@[inline] def IO.runMeta {α} (x : MetaM α) (env : Environment) (cfg : Config := {}) : IO (α × Environment) := +@[inline] def IO.runMeta {α} (x : MetaM α) (env : Environment) (cfg : Config := {}) (printTraces := true) : IO (α × Environment) := match (x { config := cfg, currRecDepth := 0, maxRecDepth := defaultMaxRecDepth }).run { env := env } with -| EStateM.Result.ok a s => pure (a, s.env) -| EStateM.Result.error ex _ => throw (IO.userError (toString ex)) +| EStateM.Result.ok a s => do + when printTraces $ + s.traceState.traces.forM $ fun msg => IO.println (fmt msg); + pure (a, s.env) +| EStateM.Result.error ex s => do + when printTraces $ + s.traceState.traces.forM $ fun msg => IO.println (fmt msg); + throw (IO.userError (toString ex))