From 418d630255b2f78b0fcdf5257c244279d478f809 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:06:07 -0800 Subject: [PATCH 1/5] fix: Remove unused variable --- Test/Environment.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/Environment.lean b/Test/Environment.lean index c49cbae..e954bc3 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -110,7 +110,7 @@ def test_symbol_location : TestT IO Unit := do checkTrue "file" result.sourceUri?.isNone checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0 checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88 - let .ok { imports, constNames, extraConstNames } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed" + let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed" checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"] checkTrue "constNames" $ constNames.contains "Nat.succ_add" From 976646fb67f3c86365b06ac1e5332047444ea3aa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:11:05 -0800 Subject: [PATCH 2/5] chore: Use repeat-break structure --- Main.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Main.lean b/Main.lean index be01ff6..b20724d 100644 --- a/Main.lean +++ b/Main.lean @@ -23,10 +23,10 @@ def parseCommand (s: String): Except String Command := do return { cmd := s.take offset, payload := payload } | .none => throw "Command is empty" -partial def loop : MainM Unit := do +partial def loop : MainM Unit := do repeat do let state ← get let command ← (← IO.getStdin).getLine - if command.trim.length = 0 then return () + if command.trim.length = 0 then break match parseCommand command with | .error error => let error := Lean.toJson ({ error := "command", desc := error }: InteractionError) @@ -43,7 +43,6 @@ partial def loop : MainM Unit := do let message ← e.toMessageData.toString let error := Lean.toJson ({ error := "main", desc := message }: InteractionError) IO.println error.compress - loop unsafe def main (args: List String): IO Unit := do From 787c9e606d30ef78ee2b0786db3d87e8576df242 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:22:58 -0800 Subject: [PATCH 3/5] chore: Cleanup REPL loop --- Main.lean | 24 ++++++++++++------------ Repl.lean | 1 - Test/Integration.lean | 4 +--- 3 files changed, 13 insertions(+), 16 deletions(-) diff --git a/Main.lean b/Main.lean index b20724d..c4d30c6 100644 --- a/Main.lean +++ b/Main.lean @@ -10,22 +10,25 @@ open Pantograph.Protocol /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ def parseCommand (s: String): Except String Command := do - let s := s.trim - match s.get? 0 with - | .some '{' => -- Parse in Json mode + match s.trim.get? 0 with + | .some '{' => + -- Parse in Json mode Lean.fromJson? (← Lean.Json.parse s) - | .some _ => -- Parse in line mode + | .some _ => + -- Parse in line mode let offset := s.posOf ' ' |> s.offsetOfPos if offset = s.length then return { cmd := s.take offset, payload := Lean.Json.null } else let payload ← s.drop offset |> Lean.Json.parse return { cmd := s.take offset, payload := payload } - | .none => throw "Command is empty" + | .none => + throw "Command is empty" partial def loop : MainM Unit := do repeat do let state ← get let command ← (← IO.getStdin).getLine + -- Halt the program if empty line is given if command.trim.length = 0 then break match parseCommand command with | .error error => @@ -47,20 +50,17 @@ partial def loop : MainM Unit := do repeat do unsafe def main (args: List String): IO Unit := do -- NOTE: A more sophisticated scheme of command line argument handling is needed. - -- Separate imports and options if args == ["--version"] then do IO.println s!"{Pantograph.version}" return Pantograph.initSearch "" - let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.toArray |> Pantograph.createCoreContext - let imports:= args.filter (λ s => ¬ (s.startsWith "--")) + -- Separate imports and options + let (options, imports) := args.partition (·.startsWith "--") + let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext let coreState ← Pantograph.createCoreState imports.toArray - let context: Context := { - imports - } + let context: Context := {} try let coreM := loop.run context |>.run' {} IO.println "ready." diff --git a/Repl.lean b/Repl.lean index 083edd1..ddf3201 100644 --- a/Repl.lean +++ b/Repl.lean @@ -4,7 +4,6 @@ import Pantograph namespace Pantograph.Repl structure Context where - imports: List String /-- Stores state of the REPL -/ structure State where diff --git a/Test/Integration.lean b/Test/Integration.lean index 7864515..9815954 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -235,9 +235,7 @@ def test_frontend_process_sorry : Test := def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do -- Setup the environment for execution - let context: Context := { - imports := ["Init"] - } + let context: Context := {} let commands: MainM LSpec.TestSeq := steps.foldlM (λ suite step => do let result ← step From 6a7830cb717a23c7a5ea5d43a59dbb2886b35991 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:24:54 -0800 Subject: [PATCH 4/5] fix: Remove spurious print --- Test/Proofs.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index e13e528..bf43bf6 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -750,8 +750,6 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do addTest $ assertUnreachable $ other.toString return () - let iex : InternalExceptionId := { idx := 4 } - IO.println s!"{← iex.getName}" let tactic := "simpa [h] using And.imp_left h _" --let state2 ← match ← state1.tacticOn 0 tactic with -- | .success state => pure state From 970c16a0a4d808c4be86cc313ff1f4acb3ff0aca Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 20:19:07 -0800 Subject: [PATCH 5/5] chore: Use `StateRefT` in `Repl.lean` --- Repl.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Repl.lean b/Repl.lean index ddf3201..4c7adc3 100644 --- a/Repl.lean +++ b/Repl.lean @@ -12,7 +12,9 @@ structure State where goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty /-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.CoreM) +abbrev MainM := ReaderT Context $ StateRefT State Lean.CoreM +/-- Fallible subroutine return type -/ +abbrev CR α := Except Protocol.InteractionError α def newGoalState (goalState: GoalState) : MainM Nat := do let state ← get @@ -24,10 +26,6 @@ def newGoalState (goalState: GoalState) : MainM Nat := do return stateId --- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables --- certain monadic features in `MainM` -abbrev CR α := Except Protocol.InteractionError α - def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := metaM.run' def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=