Pantograph/Frontend/Basic.lean

@@ -60,24 +60,45 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
   return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
-partial def collectCompilationSteps : FrontendM (List CompilationStep) := do
+partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand
   if done then
-    return [cmd]
+    if cmd.src.isEmpty then
+      return []
+    else
+      return [← f cmd]
   else
-    return cmd :: (← collectCompilationSteps)
+    return (← f cmd) :: (← mapCompilationSteps f)
 
+
+@[export pantograph_frontend_find_source_path_m]
 def findSourcePath (module : Name) : IO System.FilePath := do
   return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
 
-@[export pantograph_create_frontend_context_state_from_file_m]
+/--
-unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := {})
+Use with
-  : IO (Elab.Frontend.Context × Elab.Frontend.State) := do
+```lean
-  let file ← IO.FS.readFile (← findSourcePath module)
+let m: FrontendM α := ...
-  let inputCtx := Parser.mkInputContext file module.toString
+let (context, state) ← createContextStateFromFile ...
+m.run context |>.run' state
+```
+-/
+@[export pantograph_frontend_create_context_state_from_file_m]
+def createContextStateFromFile
+    (file : String) -- Content of the file
+    (fileName : String := "<anonymous>")
+    (env? : Option Lean.Environment := .none) -- If set to true, assume there's no header.
+    (opts : Options := {})
+    : IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do
+  --let file ← IO.FS.readFile (← findSourcePath module)
+  let inputCtx := Parser.mkInputContext file fileName
 
-  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, parserState, messages) ← match env? with
-  let (env, messages) ← Elab.processHeader header opts messages inputCtx
+    | .some env => pure (env, {}, .empty)
+    | .none =>
+      let (header, parserState, messages) ← Parser.parseHeader inputCtx
+      let (env, messages) ← Elab.processHeader header opts messages inputCtx
+      pure (env, parserState, messages)
   let commandState := Elab.Command.mkState env messages opts
   let context: Elab.Frontend.Context := { inputCtx }
   let state: Elab.Frontend.State := {
@@ -87,18 +108,4 @@ unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options :=
   }
   return (context, state)
 
-partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
-  let (cmd, done) ← processOneCommand
-  let result ← f cmd
-  if done then
-    return [result]
-  else
-    return result :: (← mapCompilationSteps f)
-
-def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do
-  let (context, state) ← createFrontendContextStateFromFile module opts
-  m.run context |>.run' state
-
-
-
 end Pantograph.Frontend

Pantograph/Protocol.lean

@@ -284,20 +284,24 @@ structure GoalDiag where
 
 
 /-- Executes the Lean compiler on a single file -/
-structure CompileUnit where
+structure FrontendProcess where
-  module: String
+  -- 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, collect tactic invocations
   invocations: Bool := false
+  -- If set to true, collect `sorry`s
+  sorrys: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
   goalAfter: String
   tactic: String
   deriving Lean.ToJson
-structure CompileUnitResult where
+structure FrontendProcessResult where
   -- String boundaries of compilation units
   units: List (Nat × Nat)
-  invocations?: Option $ List InvokedTactic
+  invocations?: Option (List InvokedTactic) := .none
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α

Repl.lean

@@ -46,7 +46,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   | "goal.continue" => run goal_continue
   | "goal.delete"   => run goal_delete
   | "goal.print"    => run goal_print
-  | "compile.unit"  => run compile_unit
+  | "frontend.process"  => run frontend_process
   | cmd =>
     let error: Protocol.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
@@ -201,16 +201,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
     let result ← runMetaInMainM <| goalPrint goalState state.options
     return .ok result
-  compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
+  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-    let module := args.module.toName
     try
-      let li ← Frontend.runFrontendMInFile module {} <| Frontend.mapCompilationSteps λ step => do
+      let (fileName, file) ← match args.fileName?, args.file? with
+        | .some fileName, .none => do
+          let file ← IO.FS.readFile fileName
+          pure (fileName, file)
+        | .none, .some file =>
+          pure ("<anonymous>", file)
+        | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+      let env?: Option Lean.Environment ← if args.fileName?.isSome then
+          pure .none
+        else do
+          let env ← Lean.MonadEnv.getEnv
+          pure <| .some env
+      let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+      let m := Frontend.mapCompilationSteps λ step => do
         let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
         let tacticInvocations ← if args.invocations then
             Frontend.collectTacticsFromCompilationStep step
           else
             pure []
         return (unitBoundary, tacticInvocations)
+      let li ← m.run context |>.run' state
       let units := li.map λ (unit, _) => unit
       let invocations? := if args.invocations then
           .some $ li.bind λ (_, invocations) => invocations
@@ -218,6 +231,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           .none
       return .ok { units, invocations? }
     catch e =>
-      return .error $ errorI "compile" (← e.toMessageData.toString)
+      return .error $ errorI "frontend" (← e.toMessageData.toString)
 
 end Pantograph.Repl

Test/Integration.lean

@@ -161,6 +161,38 @@ def test_env_add_inspect : Test :=
       Protocol.EnvInspectResult)
   ]
 
+example : ∀ (p: Prop), p → p := by
+  intro p h
+  exact h
+
+def test_frontend_process : Test :=
+  [
+    let file := "example : ∀ (p: Prop), p → p := by\n  intro p h\n  exact h"
+    let goal1 := "p : Prop\nh : p\n⊢ p"
+    step "frontend.process"
+      [
+        ("file", .str file),
+        ("invocations", .bool true),
+        ("sorrys", .bool false),
+      ]
+     ({
+       units := [(0, file.utf8ByteSize)],
+       invocations? := .some [
+         {
+           goalBefore := "⊢ ∀ (p : Prop), p → p",
+           goalAfter := goal1,
+           tactic := "intro p h",
+         },
+         {
+           goalBefore := goal1 ,
+           goalAfter := "",
+           tactic := "exact h",
+         },
+       ]
+    }: Protocol.FrontendProcessResult),
+  ]
+
+
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let context: Context := {
@@ -182,6 +214,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
     ("env.add env.inspect", test_env_add_inspect),
+    ("frontend.process", test_frontend_process),
   ]
   tests.map (fun (name, test) => (name, runTest env test))