Merge pull request 'fix: Use in-context environment in sorry collection' (#166) from bug/collect-sorry-generated-constants into dev

Reviewed-on: #166

Pantograph/Frontend/Elab.lean

@@ -148,34 +148,39 @@ structure AnnotatedGoalState where
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
+
+WARNING: Behaviour is unstable when there are multiple `sorry`s. Consider using
+the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
-  let goalsM := sorrys.mapM λ i => do
-    match i.info with
-    | .ofTermInfo termInfo  => do
-      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      if (← mvarId.getType).hasSorry then
-        throwError s!"Coupling is not allowed in drafting"
-      return [(mvarId, stxByteRange termInfo.stx)]
-    | .ofTacticInfo tacticInfo => do
-      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-      for mvarId in mvarIds do
+  withEnv env do
+    let goalsM := sorrys.mapM λ i => do
+      match i.info with
+      | .ofTermInfo termInfo  => do
+        let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
         if (← mvarId.getType).hasSorry then
           throwError s!"Coupling is not allowed in drafting"
-      let range := stxByteRange tacticInfo.stx
-      return mvarIds.map (·, range)
-    | _ => panic! "Invalid info"
-  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-  let goals := annotatedGoals.map Prod.fst
-  let srcBoundaries := annotatedGoals.map Prod.snd
-  let root := match goals with
-    | [] => panic! "No MVars generated"
-    | [g] => g
-    | _ => { name := .anonymous }
-  let state ← GoalState.createFromMVars goals root
-  return { state, srcBoundaries }
+        return [(mvarId, stxByteRange termInfo.stx)]
+      | .ofTacticInfo tacticInfo => do
+        let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+        for mvarId in mvarIds do
+          if (← mvarId.getType).hasSorry then
+            throwError s!"Coupling is not allowed in drafting"
+        let range := stxByteRange tacticInfo.stx
+        return mvarIds.map (·, range)
+      | _ => panic! "Invalid info"
+    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+    let goals := annotatedGoals.map Prod.fst
+    let srcBoundaries := annotatedGoals.map Prod.snd
+    let root := match goals with
+      | [] => panic! "No MVars generated"
+      | [g] => g
+      | _ => { name := .anonymous }
+    let state ← GoalState.createFromMVars goals root
+    return { state, srcBoundaries }
 
 
 @[export pantograph_frontend_collect_new_defined_constants_m]

Repl.lean

@@ -3,6 +3,8 @@ import Pantograph
 
 namespace Pantograph.Repl
 
+open Lean
+
 structure Context where
 
 /-- Stores state of the REPL -/
@@ -12,7 +14,7 @@ structure State where
   goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context $ StateRefT State Lean.CoreM
+abbrev MainM := ReaderT Context $ StateRefT State CoreM
 /-- Fallible subroutine return type -/
 abbrev CR α := Except Protocol.InteractionError α
 
@@ -26,20 +28,98 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   return stateId
 
 
-def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
+def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
   metaM.run'
-def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
+def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
   termElabM.run' (ctx := defaultElabContext) |>.run'
 
+section Frontend
+
+structure CompilationUnit where
+  -- Should be the penultimate environment, but this is ok
+  env : Environment
+  boundary : Nat × Nat
+  invocations : List Protocol.InvokedTactic
+  sorrys : List Frontend.InfoWithContext
+  messages : Array String
+  newConstants : List Name
+
+def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+  let options := (← get).options
+  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 Environment ← if args.fileName?.isSome then
+      pure .none
+    else do
+      let env ← getEnv
+      pure <| .some env
+  let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
+    Frontend.mapCompilationSteps λ step => do
+    let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations then
+        Frontend.collectTacticsFromCompilationStep step
+      else
+        pure []
+    let sorrys ← if args.sorrys then
+        Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
+      else
+        pure []
+    let messages ← step.messageStrings
+    let newConstants ← if args.newConstants then
+        Frontend.collectNewDefinedConstants step
+      else
+        pure []
+    return {
+      env := step.before,
+      boundary,
+      invocations,
+      sorrys,
+      messages,
+      newConstants
+    }
+  let li ← frontendM.run context |>.run' state
+  let units ← li.mapM λ step => withEnv step.env do
+    let newConstants? := if args.newConstants then
+        .some $ step.newConstants.toArray.map λ name => name.toString
+      else
+        .none
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
+        pure (.none, .none, .none)
+      else do
+        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
+        let stateId ← newGoalState state
+        let goals ← goalSerialize state options
+        let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+        pure (.some stateId, .some goals, .some srcBoundaries)
+    let invocations? := if args.invocations then .some step.invocations else .none
+    return {
+      boundary := step.boundary,
+      messages := step.messages,
+      invocations?,
+      goalStateId?,
+      goals?,
+      goalSrcBoundaries?,
+      newConstants?,
+    }
+  return .ok { units }
+
+end Frontend
+
 /-- Main loop command of the REPL -/
-def execute (command: Protocol.Command): MainM Lean.Json := do
-  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
-    match Lean.fromJson? command.payload with
+def execute (command: Protocol.Command): MainM Json := do
+  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → MainM (CR β)): MainM Json :=
+    match fromJson? command.payload with
     | .ok args => do
       match (← comm args) with
-      | .ok result =>  return Lean.toJson result
-      | .error ierror => return Lean.toJson ierror
-    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
+      | .ok result =>  return toJson result
+      | .error ierror => return toJson ierror
+    | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
   try
     match command.cmd with
     | "reset"         => run reset
@@ -65,10 +145,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | cmd =>
       let error: Protocol.InteractionError :=
         errorCommand s!"Unknown command {cmd}"
-      return Lean.toJson error
+      return toJson error
   catch ex => do
     let error ← ex.toMessageData.toString
-    return Lean.toJson $ errorIO error
+    return toJson $ errorIO error
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
@@ -78,7 +158,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    Lean.Core.resetMessageLog
+    Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -98,12 +178,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
     Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let env ← Lean.MonadEnv.getEnv
+    let env ← MonadEnv.getEnv
     environmentPickle env args.path
     return .ok {}
   env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let (env, _) ← environmentUnpickle args.path
-    Lean.setEnv env
+    setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
@@ -128,7 +208,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
     return .ok (← get).options
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let env ← Lean.MonadEnv.getEnv
+    let env ← MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
       | .none, .some copyFrom =>
@@ -245,66 +325,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     goalStatePickle goalState args.path
     return .ok {}
   goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
-    let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
     return .ok { id }
   frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-    let options := (← get).options
     try
-      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 frontendM := Frontend.mapCompilationSteps λ step => do
-        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
-            let invocations ← Frontend.collectTacticsFromCompilationStep step
-            pure $ .some invocations
-          else
-            pure .none
-        let sorrys ← if args.sorrys then
-            Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
-          else
-            pure []
-        let messages ← step.messageStrings
-        let newConstants ← if args.newConstants then
-            Frontend.collectNewDefinedConstants step
-          else
-            pure []
-        return (step.before, boundary, invocations?, sorrys, messages, newConstants)
-      let li ← frontendM.run context |>.run' state
-      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
-        let newConstants? := if args.newConstants then
-            .some $ newConstants.toArray.map λ name => name.toString
-          else
-            .none
-        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
-            pure (.none, .none, .none)
-          else do
-            let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
-            let stateId ← newGoalState state
-            let goals ← goalSerialize state options
-            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
-            pure (.some stateId, .some goals, .some srcBoundaries)
-        return {
-          boundary,
-          messages,
-          invocations?,
-          goalStateId?,
-          goals?,
-          goalSrcBoundaries?,
-          newConstants?,
-        }
-      return .ok { units }
+      frontend_process_inner args
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 

doc/repl.md

@@ -52,7 +52,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   (`"invocations": true`), the sorrys and type errors into goal states
   (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
   `sorrys`, this command additionally outputs the position of each captured
-  `sorry`.
+  `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
+  draft tactic if possible.
 
 ## Errors