diff --git a/Main.lean b/Main.lean index eb5240d..b866711 100644 --- a/Main.lean +++ b/Main.lean @@ -1,16 +1,15 @@ import Lean.Data.Json import Lean.Environment -import Pantograph.Version -import Pantograph.Library import Pantograph import Repl -- Main IO functions -open Pantograph +open Pantograph.Repl +open Pantograph.Protocol /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ -def parseCommand (s: String): Except String Protocol.Command := do +def parseCommand (s: String): Except String Command := do let s := s.trim match s.get? 0 with | .some '{' => -- Parse in Json mode @@ -30,7 +29,7 @@ partial def loop : MainM Unit := do if command.trim.length = 0 then return () match parseCommand command with | .error error => - let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError) + let error := Lean.toJson ({ error := "command", desc := error }: InteractionError) -- Using `Lean.Json.compress` here to prevent newline IO.println error.compress | .ok command => @@ -46,15 +45,15 @@ 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 - println! s!"{version}" + println! s!"{Pantograph.version}" return - initSearch "" + Pantograph.initSearch "" let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.toArray |> createCoreContext + |>.toArray |> Pantograph.createCoreContext let imports:= args.filter (λ s => ¬ (s.startsWith "--")) - let coreState ← createCoreState imports.toArray + let coreState ← Pantograph.createCoreState imports.toArray let context: Context := { imports } diff --git a/Pantograph.lean b/Pantograph.lean index 09327e8..292efb9 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,6 +1,6 @@ -import Pantograph.Compile import Pantograph.Condensed import Pantograph.Environment +import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol diff --git a/Pantograph/Compile.lean b/Pantograph/Compile.lean deleted file mode 100644 index 83b463f..0000000 --- a/Pantograph/Compile.lean +++ /dev/null @@ -1,25 +0,0 @@ -/- Adapted from lean-training-data by semorrison -/ -import Pantograph.Protocol -import Pantograph.Compile.Frontend -import Pantograph.Compile.Elab -import Pantograph.Compile.Parse - -open Lean - -namespace Pantograph.Compile - -def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do - let infoTrees := steps.bind (·.trees) - let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ - | info@(.ofTacticInfo _) => info.isOriginal - | _ => false - let tactics := tacticInfoTrees.bind collectTactics - tactics.mapM λ invocation => do - let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty - let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty - let tactic ← invocation.ctx.runMetaM {} do - let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ - return t.pretty - return { goalBefore, goalAfter, tactic } - -end Pantograph.Compile diff --git a/Pantograph/Compile/Parse.lean b/Pantograph/Compile/Parse.lean deleted file mode 100644 index 72eb620..0000000 --- a/Pantograph/Compile/Parse.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Lean - -open Lean - -namespace Pantograph.Compile - -def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do - return Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := s) - (fileName := "") - -end Pantograph.Compile diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index c47f882..125b69c 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -2,7 +2,6 @@ import Lean import Pantograph.Goal import Pantograph.Expr -import Pantograph.Protocol open Lean diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean new file mode 100644 index 0000000..ffeeec5 --- /dev/null +++ b/Pantograph/Frontend.lean @@ -0,0 +1,4 @@ +/- Adapted from lean-training-data by semorrison -/ +import Pantograph.Protocol +import Pantograph.Frontend.Basic +import Pantograph.Frontend.Elab diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Frontend/Basic.lean similarity index 58% rename from Pantograph/Compile/Frontend.lean rename to Pantograph/Frontend/Basic.lean index 3dbad85..933424c 100644 --- a/Pantograph/Compile/Frontend.lean +++ b/Pantograph/Frontend/Basic.lean @@ -8,6 +8,7 @@ namespace Lean.FileMap /-- Extract the range of a `Syntax` expressed as lines and columns. -/ -- Extracted from the private declaration `Lean.Elab.formatStxRange`, -- in `Lean.Elab.InfoTree.Main`. +@[export pantograph_frontend_stx_range] protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position := let pos := stx.getPos?.getD 0 let endPos := stx.getTailPos?.getD pos @@ -27,7 +28,9 @@ protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α : end Lean.PersistentArray -namespace Pantograph.Compile +namespace Pantograph.Frontend + +abbrev FrontendM := Elab.Frontend.FrontendM structure CompilationStep where fileName : String @@ -44,7 +47,8 @@ structure CompilationStep where Process one command, returning a `CompilationStep` and `done : Bool`, indicating whether this was the last command. -/ -def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do +@[export pantograph_frontend_process_one_command_m] +def processOneCommand: FrontendM (CompilationStep × Bool) := do let s := (← get).commandState let before := s.env let done ← Elab.Frontend.processCommand @@ -57,30 +61,52 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do let ⟨_, fileName, fileMap⟩ := (← read).inputCtx return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) -partial def processFile : Elab.Frontend.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 :: (← processFile) + 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" -def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do - let file ← IO.FS.readFile (← findSourcePath module) - let inputCtx := Parser.mkInputContext file module.toString +/-- +Use with +```lean +let m: FrontendM α := ... +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 := "") + (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, messages) ← Elab.processHeader header opts messages inputCtx + let (env, parserState, messages) ← match env? with + | .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 - processFile.run { inputCtx } - |>.run' { + let context: Elab.Frontend.Context := { inputCtx } + let state: Elab.Frontend.State := { commandState := { commandState with infoState.enabled := true }, parserState, cmdPos := parserState.pos } + return (context, state) - -end Pantograph.Compile +end Pantograph.Frontend diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Frontend/Elab.lean similarity index 71% rename from Pantograph/Compile/Elab.lean rename to Pantograph/Frontend/Elab.lean index 79833f3..4d6afe4 100644 --- a/Pantograph/Compile/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -1,9 +1,11 @@ - +/- Adapted from https://github.com/semorrison/lean-training-data -/ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree -import Pantograph.Compile.Frontend +import Pantograph.Protocol +import Pantograph.Frontend.Basic +import Pantograph.Goal open Lean @@ -75,7 +77,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : end Lean.Elab.InfoTree -namespace Pantograph.Compile +namespace Pantograph.Frontend -- Info tree filtering functions @@ -86,6 +88,7 @@ structure TacticInvocation where namespace TacticInvocation /-- Return the range of the tactic, as a pair of file positions. -/ +@[export pantograph_frontend_tactic_invocation_range] protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx /-- Pretty print a tactic. -/ @@ -131,7 +134,7 @@ partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pre /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ -def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := +private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := let infos := findAllInfo t none fun i => match i with | .ofTacticInfo _ => true | _ => false @@ -142,5 +145,46 @@ def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := def collectTactics (t : Elab.InfoTree) : List TacticInvocation := collectTacticNodes t |>.filter fun i => i.info.isSubstantive +@[export pantograph_frontend_collect_tactics_from_compilation_step_m] +def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do + let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ + | info@(.ofTacticInfo _) => info.isOriginal + | _ => false + let tactics := tacticInfoTrees.bind collectTactics + tactics.mapM λ invocation => do + let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty + let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty + let tactic ← invocation.ctx.runMetaM {} do + let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + return t.pretty + return { goalBefore, goalAfter, tactic } -end Pantograph.Compile +private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo := + let infos := findAllInfo t none fun i => match i with + | .ofTermInfo { expectedType?, expr, stx, .. } => + expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry + | _ => false + infos.filterMap fun p => match p with + | (.ofTermInfo i, _, _) => .some i + | _ => none + +@[export pantograph_frontend_collect_sorrys_m] +def collectSorrys (step: CompilationStep) : List Elab.TermInfo := + step.trees.bind collectSorrysInTree + +@[export pantograph_frontend_sorrys_to_goal_state] +def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do + assert! !sorrys.isEmpty + let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do + let type := termInfo.expectedType?.get! + let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type + return mvar.mvarId! + let root := match goals with + | [] => panic! "This function cannot be called on an empty list" + | [g] => g + | _ => { name := .anonymous } + GoalState.createFromMVars goals root + + + +end Pantograph.Frontend diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index f248923..79e3004 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -3,9 +3,7 @@ Functions for handling metavariables All the functions starting with `try` resume their inner monadic state. -/ -import Pantograph.Protocol import Pantograph.Tactic -import Pantograph.Compile.Parse import Lean @@ -48,6 +46,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do savedState, parentMVar? := .none, } +@[export pantograph_goal_state_create_from_mvars_m] +protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do + let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState + let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {} + return { + root, + savedState, + parentMVar? := .none, + } @[export pantograph_goal_state_is_conv] protected def GoalState.isConv (state: GoalState): Bool := state.convMVar?.isSome @@ -145,6 +152,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except @[export pantograph_goal_state_root_expr] protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do + if goalState.root.name == .anonymous then + .none let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasExprMVar then @@ -385,20 +394,4 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) catch exception => return .failure #[← exception.toMessageData.toString] - -protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let recursor ← match (← Compile.parseTermM recursor) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) -protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let eq ← match (← Compile.parseTermM eq) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) - end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 2f31042..23a2046 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -159,7 +159,7 @@ def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticRes runTermElabM <| state.tryAssign goal expr @[export pantograph_goal_have_m] protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do - let type ← match (← Compile.parseTermM type) with + let type ← match (← parseTermM type) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do @@ -167,12 +167,28 @@ protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: S state.tryTacticM goal $ Tactic.evalHave binderName.toName type @[export pantograph_goal_try_define_m] protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do - let expr ← match (← Compile.parseTermM expr) with + let expr ← match (← parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM state.tryTacticM goal (Tactic.evalDefine binderName.toName expr) +@[export pantograph_goal_try_motivated_apply_m] +protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let recursor ← match (← parseTermM recursor) with + | .ok syn => pure syn + | .error error => return .parseError error + state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) +@[export pantograph_goal_try_no_confuse_m] +protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let eq ← match (← parseTermM eq) with + | .ok syn => pure syn + | .error error => return .parseError error + state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goal binderName type diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index e88efa3..abfeede 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -284,21 +284,25 @@ structure GoalDiag where /-- Executes the Lean compiler on a single file -/ -structure CompileUnit where - module: String - -- If set to true, query the string boundaries of compilation units - compilationUnits: Bool := false +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, 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 - units?: Option $ List (Nat × Nat) - invocations?: Option $ List InvokedTactic +structure FrontendProcessResult where + -- String boundaries of compilation units + units: List (Nat × Nat) + invocations?: Option (List InvokedTactic) := .none + goalStates?: Option (List (Nat × Array Goal)) := .none deriving Lean.ToJson abbrev CR α := Except InteractionError α diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 93dfb95..3a9efa4 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -26,6 +26,13 @@ def parseTerm (env: Environment) (s: String): Except String Syntax := (input := s) (fileName := "") +def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do + return Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := "") + /-- Parse a syntax object. May generate additional metavariables! -/ def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do try diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index ed33cbb..2decbc1 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.18" +def version := "0.2.19" end Pantograph diff --git a/README.md b/README.md index 06ae690..04213ae 100644 --- a/README.md +++ b/README.md @@ -9,30 +9,17 @@ examine the symbol list of a Lean project for machine learning. ## Installation -For Nix based workflow, see below. +For Nix users, run +``` sh +nix build .#{sharedLib,executable} +``` +to build either the shared library or executable. Install `elan` and `lake`, and run ``` sh lake build ``` -This builds the executable in `.lake/build/bin/pantograph`. - -To use Pantograph in a project environment, setup the `LEAN_PATH` environment -variable so it contains the library path of lean libraries. The libraries must -be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, -the environment might be setup like this: - -``` sh -LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/lake-packages" -export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" - -LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ -``` -The `$LEAN_PATH` executable of any project can be extracted by -``` sh -lake env printenv LEAN_PATH -``` +This builds the executable in `.lake/build/bin/pantograph-repl`. ## Executable Usage @@ -114,6 +101,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state +* `frontend.process { ["fileName": ",] ["file": ], invocations: + , sorrys: }`: Executes the Lean frontend on a file, collecting + either the tactic invocations (`"invocations": true`) or the sorrys into goal + states (`"sorrys": true`) ### Errors @@ -130,6 +121,25 @@ Common error forms: input of another is broken. For example, attempting to query a symbol not existing in the library or indexing into a non-existent proof state. +### Project Environment + +To use Pantograph in a project environment, setup the `LEAN_PATH` environment +variable so it contains the library path of lean libraries. The libraries must +be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, +the environment might be setup like this: + +``` sh +LIB="../lib" +LIB_MATHLIB="$LIB/mathlib4/lake-packages" +export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" + +LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ +``` +The `$LEAN_PATH` executable of any project can be extracted by +``` sh +lake env printenv LEAN_PATH +``` + ### Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: @@ -143,8 +153,11 @@ ulimit -s unlimited with `Pantograph` which mirrors the REPL commands above. It is recommended to call Pantograph via this FFI since it provides a tremendous speed up. -Note that there isn't a 1-1 correspondence between executable (REPL) commands -and library functions. +The executable can be used as-is, but linking against the shared library +requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence +between executable (REPL) commands and library functions. + +Inject any project path via the `pantograph_init_search` function. ## Developing @@ -152,7 +165,11 @@ A Lean development shell is provided in the Nix flake. ### Testing -The tests are based on `LSpec`. To run tests, +The tests are based on `LSpec`. To run tests, use either +``` sh +nix flake check +``` +or ``` sh lake test ``` @@ -161,14 +178,3 @@ You can run an individual test by specifying a prefix ``` sh lake test -- "Tactic/No Confuse" ``` - -## Nix based workflow - -The included Nix flake provides build targets for `sharedLib` and `executable`. -The executable can be used as-is, but linking against the shared library -requires the presence of `lean-all`. - -To run tests: -``` sh -nix flake check -``` diff --git a/Repl.lean b/Repl.lean index ef77d56..1277e73 100644 --- a/Repl.lean +++ b/Repl.lean @@ -1,7 +1,7 @@ import Lean.Data.HashMap import Pantograph -namespace Pantograph +namespace Pantograph.Repl structure Context where imports: List String @@ -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}" @@ -54,6 +54,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do where errorCommand := errorI "command" errorIndex := errorI "index" + newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -95,7 +103,6 @@ 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 state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) @@ -108,11 +115,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok goalState => - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } + let stateId ← newGoalState goalState return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get @@ -151,11 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" pure result | false, _ => pure nextGoalState - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } + let nextStateId ← newGoalState nextGoalState let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' return .ok { nextStateId? := .some nextStateId, @@ -201,20 +200,52 @@ 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 - let module := args.module.toName + frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do + let options := (← get).options try - let steps ← Compile.processSource module - let units? := if args.compilationUnits then - .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) + 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 ("", 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 [] + let sorrys := if args.sorrys then + Frontend.collectSorrys step + else + [] + return (unitBoundary, tacticInvocations, sorrys) + let li ← m.run context |>.run' state + let units := li.map λ (unit, _, _) => unit + let invocations? := if args.invocations then + .some $ li.bind λ (_, invocations, _) => invocations else .none - let invocations? ← if args.invocations then - pure $ .some (← Compile.collectTacticsFromCompilation steps) + let goalStates? ← if args.sorrys then do + let stateIds ← li.filterMapM λ (_, _, sorrys) => do + if sorrys.isEmpty then + return .none + let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys + let stateId ← newGoalState goalState + let goals ← goalSerialize goalState options + return .some (stateId, goals) + pure $ .some stateIds else pure .none - return .ok { units?, invocations? } + return .ok { units, invocations?, goalStates? } catch e => - return .error $ errorI "compile" (← e.toMessageData.toString) + return .error $ errorI "frontend" (← e.toMessageData.toString) -end Pantograph +end Pantograph.Repl diff --git a/Test/Integration.lean b/Test/Integration.lean index b82962b..4a8e418 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -6,13 +6,13 @@ import Repl import Test.Common namespace Pantograph.Test.Integration -open Pantograph +open Pantograph.Repl def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json)) (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do let payload := Lean.Json.mkObj payload let name := name?.getD s!"{cmd} {payload.compress}" - let result ← execute { cmd, payload } + let result ← Repl.execute { cmd, payload } return LSpec.test name (toString result = toString (Lean.toJson expected)) abbrev Test := List (MainM LSpec.TestSeq) @@ -161,6 +161,68 @@ 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), + ] + +example : 1 + 2 = 3 := rfl +example (p: Prop): p → p := by simp + +def test_frontend_process_sorry : Test := + let solved := "example : 1 + 2 = 3 := rfl\n" + let withSorry := "example (p: Prop): p → p := sorry" + [ + let file := s!"{solved}{withSorry}" + let goal1: Protocol.Goal := { + name := "_uniq.1", + target := { pp? := .some "p → p" }, + vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}], + } + step "frontend.process" + [ + ("file", .str file), + ("invocations", .bool false), + ("sorrys", .bool true), + ] + ({ + units := [ + (0, solved.utf8ByteSize), + (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), + ], + goalStates? := [ + (0, #[goal1]), + ] + }: Protocol.FrontendProcessResult), + ] + + def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do -- Setup the environment for execution let context: Context := { @@ -182,6 +244,8 @@ 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 invocation", test_frontend_process), + ("frontend.process sorry", test_frontend_process_sorry), ] tests.map (fun (name, test) => (name, runTest env test))