feat: basic full file mode

README.md

@@ -57,6 +57,34 @@ Example output:
 
 showing any messages generated, and sorries with their goal states.
 
+## File mode
+
+There is a simple wrapper around command mode that allows reading in an entire file.
+
+If `file.lean` contains
+```lean
+def f : Nat := 37
+
+def g := 2
+
+theorem h : f + g = 39 := by exact rfl
+```
+
+then sending
+```json
+{"path": "test/file.lean", "allTactics": true}
+```
+to the REPL results in output
+```json
+{"tactics":
+ [{"tactic": "exact rfl",
+   "proofState": 0,
+   "pos": {"line": 5, "column": 29},
+   "goals": "⊢ f + g = 39",
+   "endPos": {"line": 5, "column": 38}}],
+ "env": 0}
+ ```
+
 ## Tactic mode (experimental)
 
 To enter tactic mode issue a command containing a `sorry`,

REPL/JSON.lean

@@ -11,21 +11,28 @@ open Lean Elab InfoTree
 
 namespace REPL
 
-/-- Run Lean commands.
-If `env = none`, starts a new session (in which you can use `import`).
-If `env = some n`, builds on the existing environment `n`.
--/
-structure Command where
-  env : Option Nat
-  cmd : String
+structure CommandOptions where
   allTactics : Option Bool := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
   -/
   infotree : Option String
+
+/-- Run Lean commands.
+If `env = none`, starts a new session (in which you can use `import`).
+If `env = some n`, builds on the existing environment `n`.
+-/
+structure Command extends CommandOptions where
+  env : Option Nat
+  cmd : String
 deriving ToJson, FromJson
 
+/-- Process a Lean file in a fresh environment. -/
+structure File extends CommandOptions where
+  path : System.FilePath
+deriving FromJson
+
 /--
 Run a tactic in a proof state.
 -/

REPL/Main.lean

@@ -227,6 +227,13 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
       tactics
       infotree }
 
+def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
+  try
+    let cmd ← IO.FS.readFile s.path
+    runCommand { s with env := none, cmd }
+  catch e =>
+    pure <| .inr ⟨e.toString⟩
+
 /--
 Run a single tactic, returning the id of the new proof statement, and the new goals.
 -/
@@ -261,6 +268,7 @@ instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
 /-- Commands accepted by the REPL. -/
 inductive Input
 | command : REPL.Command → Input
+| file : REPL.File → Input
 | proofStep : REPL.ProofStep → Input
 | pickleEnvironment : REPL.PickleEnvironment → Input
 | unpickleEnvironment : REPL.UnpickleEnvironment → Input
@@ -285,6 +293,8 @@ def parse (query : String) : IO Input := do
     | .ok (r : REPL.UnpickleProofState) => return .unpickleProofSnapshot r
     | .error _ => match fromJson? j with
     | .ok (r : REPL.Command) => return .command r
+    | .error _ => match fromJson? j with
+    | .ok (r : REPL.File) => return .file r
     | .error e => throw <| IO.userError <| toString <| toJson <|
         (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error)
 
@@ -298,6 +308,7 @@ where loop : M IO Unit := do
   if query.startsWith "#" || query.startsWith "--" then loop else
   IO.println <| toString <| ← match ← parse query with
   | .command r => return toJson (← runCommand r)
+  | .file r => return toJson (← processFile r)
   | .proofStep r => return toJson (← runProofStep r)
   | .pickleEnvironment r => return toJson (← pickleCommandSnapshot r)
   | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r)

test/file.expected.out

@@ -0,0 +1,8 @@
+{"tactics":
+ [{"tactic": "exact rfl",
+   "proofState": 0,
+   "pos": {"line": 5, "column": 29},
+   "goals": "⊢ f + g = 39",
+   "endPos": {"line": 5, "column": 38}}],
+ "env": 0}
+

test/file.in

@@ -0,0 +1 @@
+{"path": "test/file.lean", "allTactics": true}

test/file.lean

@@ -0,0 +1,5 @@
+def f : Nat := 37
+
+def g := 2
+
+theorem h : f + g = 39 := by exact rfl