From 0cfd73e44e57556068b5962e3ec59d847058594e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 9 Mar 2025 23:29:33 -0700 Subject: [PATCH 1/4] test(frontend): Add scope `open` test --- Pantograph/Frontend/Basic.lean | 3 ++- Test/Frontend.lean | 19 ++++++++++++++++++- 2 files changed, 20 insertions(+), 2 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 4e15ad8..035c34b 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -40,6 +40,7 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos := abbrev FrontendM := Elab.Frontend.FrontendM structure CompilationStep where + scope : Elab.Command.Scope fileName : String fileMap : FileMap src : Substring @@ -74,7 +75,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do let msgs := s'.messages.toList.drop s.messages.toList.length let trees := s'.infoState.trees.drop s.infoState.trees.size let ⟨_, fileName, fileMap⟩ := (← read).inputCtx - return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) + return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done) partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do let (cmd, done) ← processOneCommand diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 571aa9f..bb160b0 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -1,11 +1,27 @@ -import LSpec import Pantograph import Repl import Test.Common +import LSpec + open Lean Pantograph namespace Pantograph.Test.Frontend +def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do + let filename := "" + let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} + let m := Frontend.mapCompilationSteps f + m.run context |>.run' state + +def test_open : TestT MetaM Unit := do + let sketch := " +open Nat +example : ∀ (n m: Nat), n + m = m + n := by + apply add_comm + " + let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString) + checkEq "errors" errors [[]] + def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {}) : MetaM (List GoalState) := do let filename := "" @@ -233,6 +249,7 @@ theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests := [ + ("open", test_open), ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof), ("sorry_in_middle", test_sorry_in_middle), ("sorry_in_induction", test_sorry_in_induction), From 8797bbe245a9bb7ef7f90b41fb46d80c3ded5488 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 14 Mar 2025 16:35:12 -0700 Subject: [PATCH 2/4] test(frontend): Fix the open test --- Test/Frontend.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Test/Frontend.lean b/Test/Frontend.lean index bb160b0..4062fb7 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -16,11 +16,12 @@ def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) def test_open : TestT MetaM Unit := do let sketch := " open Nat -example : ∀ (n m: Nat), n + m = m + n := by - apply add_comm +example : ∀ (n : Nat), n + 1 = Nat.succ n := by + intro + apply add_one " let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString) - checkEq "errors" errors [[]] + checkEq "errors" errors [[], []] def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {}) : MetaM (List GoalState) := do From 79e4dc697e49dcf19a96c4e9e4f6320e24eaf48c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 14 Mar 2025 16:46:28 -0700 Subject: [PATCH 3/4] feat(frontend): Add option to inherit environment --- Pantograph/Protocol.lean | 5 +++++ Repl.lean | 11 ++++++----- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 6d2c66b..164b72a 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -346,6 +346,11 @@ structure FrontendProcess where -- One of these two must be supplied: Either supply the file name or the content. fileName?: Option String := .none file?: Option String := .none + -- If set to true, read the header (otherwise discards the header) + readHeader : Bool := false + -- If set to true, Pantograph's environment will be altered to whatever is + -- after the compilation units. + inheritEnv : Bool := false -- collect tactic invocations invocations: Bool := false -- collect `sorry`s diff --git a/Repl.lean b/Repl.lean index c8f4028..e571397 100644 --- a/Repl.lean +++ b/Repl.lean @@ -53,11 +53,10 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol. | .none, .some file => pure ("", file) | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied" - let env?: Option Environment ← if args.fileName?.isSome then + let env?: Option Environment ← if args.readHeader then pure .none else do - let env ← getEnv - pure <| .some env + .some <$> getEnv let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {} let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) := Frontend.mapCompilationSteps λ step => do @@ -83,7 +82,9 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol. messages, newConstants } - let li ← frontendM.run context |>.run' state + let (li, state') ← frontendM.run context |>.run state + if args.inheritEnv then + setEnv state'.commandState.env let units ← li.mapM λ step => withEnv step.env do let newConstants? := if args.newConstants then .some $ step.newConstants.toArray.map λ name => name.toString @@ -141,7 +142,7 @@ def execute (command: Protocol.Command): MainM Json := do | "goal.print" => run goal_print | "goal.save" => run goal_save | "goal.load" => run goal_load - | "frontend.process" => run frontend_process + | "frontend.process" => run frontend_process | cmd => let error: Protocol.InteractionError := errorCommand s!"Unknown command {cmd}" From ef165b70457080faa92b9668d1c0abc955e42e1f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 14 Mar 2025 16:47:46 -0700 Subject: [PATCH 4/4] fix(frontend): Test update --- Test/Integration.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Test/Integration.lean b/Test/Integration.lean index 9815954..fc2f80b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -173,6 +173,8 @@ def test_frontend_process : Test := [ ("file", .str file), ("invocations", .bool true), + ("readHeader", .bool false), + ("inheritEnv", .bool false), ("sorrys", .bool false), ("typeErrorsAsGoals", .bool false), ("newConstants", .bool false), @@ -214,6 +216,8 @@ def test_frontend_process_sorry : Test := step "frontend.process" [ ("file", .str file), + ("readHeader", .bool false), + ("inheritEnv", .bool false), ("invocations", .bool false), ("sorrys", .bool true), ("typeErrorsAsGoals", .bool false),