max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: IO.runMeta: print traces (by default)

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-15 14:38:44 +02:00
parent e10507e661
commit 3caf6e83f8
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Lean/Meta/Basic.lean
View file

@ -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))