From 752d13182d9cb285d989cd1532ff5b30ec5f8eb5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 16:24:30 -0700 Subject: [PATCH] fix(frontend): Tomograph fix --- Tomograph.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Tomograph.lean b/Tomograph.lean index 9847d49..469ee53 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -14,14 +14,14 @@ def dissect (args : List String) : IO UInt32 := do let fileName :: _args := args | fail s!"Must supply a file name" let file ← IO.FS.readFile fileName let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {} - let frontendM: Elab.Frontend.FrontendM _ := + let frontendM: Frontend.FrontendM _ := Frontend.mapCompilationSteps λ step => do IO.println s!"🐈 {step.stx.getKind.toString}" for (tree, i) in step.trees.zipIdx do IO.println s!"🌲[{i}] {← tree.toString}" for (msg, i) in step.msgs.zipIdx do IO.println s!"🔈[{i}] {← msg.toString}" - let (_, _) ← frontendM.run context |>.run state + let (_, _) ← frontendM.run {} |>.run context |>.run state return 0 end Pantograph