From 0cfd73e44e57556068b5962e3ec59d847058594e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
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 := "<anonymous>"
+ 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 := "<anonymous>"
@@ -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),
--
2.44.1
From 8797bbe245a9bb7ef7f90b41fb46d80c3ded5488 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
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
--
2.44.1
From 79e4dc697e49dcf19a96c4e9e4f6320e24eaf48c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
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 ("<anonymous>", 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}"
--
2.44.1
From ef165b70457080faa92b9668d1c0abc955e42e1f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
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),
--
2.44.1