From a261a4099a92fec943eb253e64058d15f474e489 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 14:55:40 -0700 Subject: [PATCH 1/3] feat(frontend): Cancel token in frontend --- Pantograph/Frontend/Basic.lean | 63 +++++++++++++++++++++++++++------- Pantograph/Library.lean | 6 +++- Repl.lean | 7 ++-- Test/Frontend.lean | 17 +++++---- 4 files changed, 72 insertions(+), 21 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 3fbc99d..ba013bb 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -6,8 +6,6 @@ open Lean 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 @@ -19,9 +17,10 @@ namespace Lean.PersistentArray /-- Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`. + +We can't remove the `[Inhabited α]` hypotheses here until +`PersistentArray`'s `GetElem` instance also does. -/ --- We can't remove the `[Inhabited α]` hypotheses here until --- `PersistentArray`'s `GetElem` instance also does. protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α := List.range (t.size - n) |>.map fun i => t.get! (n + i) @@ -36,8 +35,11 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos := let endPos := stx.getTailPos?.getD 0 (pos, endPos) +structure Context where + cancelTk? : Option IO.CancelToken := .none -abbrev FrontendM := Elab.Frontend.FrontendM +/-- This `FrontendM` comes with more options. -/ +abbrev FrontendM := ReaderT Context Elab.Frontend.FrontendM structure CompilationStep where scope : Elab.Command.Scope @@ -50,10 +52,44 @@ structure CompilationStep where msgs : List Message trees : List Elab.InfoTree -namespace CompilationStep +/-- Like `Elab.Frontend.runCommandElabM`, but taking `cancelTk?` into account. -/ +@[inline] def runCommandElabM (x : Elab.Command.CommandElabM α) : FrontendM α := do + let config ← read + let ctx ← readThe Elab.Frontend.Context + let s ← get + let cmdCtx : Elab.Command.Context := { + cmdPos := s.cmdPos + fileName := ctx.inputCtx.fileName + fileMap := ctx.inputCtx.fileMap + snap? := none + cancelTk? := config.cancelTk? + } + match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with + | Except.error e => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}" + | Except.ok (a, sNew) => Elab.Frontend.setCommandState sNew; return a -end CompilationStep +def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do + runCommandElabM do + let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} }) + Elab.Command.elabCommandTopLevel stx + let mut msgs := (← get).messages + modify ({ · with messages := initMsgs ++ msgs }) +open Elab.Frontend in +def processCommand : FrontendM Bool := do + updateCmdPos + let cmdState ← getCommandState + let ictx ← getInputContext + let pstate ← getParserState + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with + | (cmd, ps, messages) => + modify fun s => { s with commands := s.commands.push cmd } + setParserState ps + setMessages messages + elabCommandAtFrontend cmd + pure (Parser.isTerminalCommand cmd) /-- Process one command, returning a `CompilationStep` and @@ -63,17 +99,19 @@ Process one command, returning a `CompilationStep` and def processOneCommand: FrontendM (CompilationStep × Bool) := do let s := (← get).commandState let before := s.env - let done ← Elab.Frontend.processCommand + let done ← processCommand let stx := (← get).commands.back! - let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos + let src := (← readThe Elab.Frontend.Context).inputCtx.input.toSubstring.extract + (← get).cmdPos + (← get).parserState.pos let s' := (← get).commandState let after := s'.env let msgs := s'.messages.toList.drop s.messages.toList.length let trees := s'.infoState.trees.drop s.infoState.trees.size - let ⟨_, fileName, fileMap⟩ := (← read).inputCtx + let ⟨_, fileName, fileMap⟩ := (← readThe Elab.Frontend.Context).inputCtx return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done) -partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do +partial def mapCompilationSteps { α } (f: CompilationStep → FrontendM α) : FrontendM (List α) := do let (cmd, done) ← processOneCommand if done then if cmd.src.isEmpty then @@ -106,10 +144,11 @@ def createContextStateFromFile --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 | .some env => pure (env, {}, .empty) | .none => - let (header, parserState, messages) ← Parser.parseHeader inputCtx + -- Only process the header if we don't have an environment. let (env, messages) ← Elab.processHeader header opts messages inputCtx pure (env, parserState, messages) let commandState := Elab.Command.mkState env messages opts diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index f361046..a2095c3 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -2,7 +2,6 @@ import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol import Pantograph.Delate -import Pantograph.Version import Lean @@ -188,4 +187,9 @@ def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : UInt32) cancelToken.set return () +def spawnCancelToken (timeout : UInt32) : IO IO.CancelToken := do + let token ← IO.CancelToken.new + runCancelTokenWithTimeout token timeout + return token + end Pantograph diff --git a/Repl.lean b/Repl.lean index ef91a5e..ae116f1 100644 --- a/Repl.lean +++ b/Repl.lean @@ -200,7 +200,7 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP else do .some <$> getEnv let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {} - let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) := + let frontendM: 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?.isSome then @@ -224,7 +224,10 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP messages, newConstants } - let (li, state') ← frontendM.run context |>.run state + let cancelTk? ← match (← get).options.timeout with + | 0 => pure .none + | timeout => .some <$> spawnCancelToken (timeout := .ofBitVec timeout) + let (li, state') ← frontendM.run { cancelTk? } |>.run context |>.run state if args.inheritEnv then setEnv state'.commandState.env if let .some scope := state'.commandState.scopes.head? then diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 4062fb7..fec2e01 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -7,11 +7,16 @@ import LSpec open Lean Pantograph namespace Pantograph.Test.Frontend -def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do +open Frontend + +def runFrontend { α } (source: String) (f : CompilationStep → FrontendM α) (timeout : UInt32 := 0): MetaM (List α) := do let filename := "" - let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} - let m := Frontend.mapCompilationSteps f - m.run context |>.run' state + let (context, state) ← do createContextStateFromFile source filename (← getEnv) {} + let m := mapCompilationSteps f + let cancelTk? ← match timeout with + | 0 => pure .none + | timeout => .some <$> spawnCancelToken timeout + m.run { cancelTk? } |>.run context |>.run' state def test_open : TestT MetaM Unit := do let sketch := " @@ -29,7 +34,7 @@ def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionO let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} let m := Frontend.mapCompilationSteps λ step => do return (step.before, ← Frontend.collectSorrys step options) - let li ← m.run context |>.run' state + let li ← m.run {} |>.run context |>.run' state let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do if sorrys.isEmpty then return .none @@ -227,7 +232,7 @@ def collectNewConstants (source: String) : MetaM (List (List Name)) := do let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} let m := Frontend.mapCompilationSteps λ step => do Frontend.collectNewDefinedConstants step - m.run context |>.run' state + m.run {} |>.run context |>.run' state def test_collect_one_constant : TestT MetaM Unit := do let input := " -- 2.44.1 From 18edccd4d0aa702a8a4083303608f8032c578d05 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 15:00:23 -0700 Subject: [PATCH 2/3] doc: Move repl documentation to `doc/repl.md` --- README.md | 82 +++------------------------------------------ doc/repl.md | 96 +++++++++++++++++++++++++++++++++++++++++++++++------ 2 files changed, 91 insertions(+), 87 deletions(-) diff --git a/README.md b/README.md index 4280f60..168efa5 100644 --- a/README.md +++ b/README.md @@ -25,87 +25,15 @@ lake build ``` This builds the executable in `.lake/build/bin/pantograph-repl`. -## Executable Usage +### Executable Usage -``` sh -pantograph-repl MODULES|LEAN_OPTIONS -``` +See [Executable Usage](./doc/repl.md) -The `pantograph-repl` executable must be run with a list of modules to import. -It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. - -The REPL loop accepts commands as single-line JSON inputs and outputs either an -`Error:` (indicating malformed command) or a JSON return value indicating the -result of a command execution. The command can be passed in one of two formats -``` -command { ... } -{ "cmd": command, "payload": ... } -``` -The list of available commands can be found in `Pantograph/Protocol.lean` and below. An -empty command aborts the REPL. - - -Example: (~5k symbols) -``` -$ pantograph Init -env.catalog -env.inspect {"name": "Nat.le_add_left"} -``` -Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) -``` -$ pantograph Mathlib.Analysis.Seminorm -env.catalog -``` -Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof -``` -$ pantograph Init -goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} -goal.tactic {"stateId": 0, "tactic": "intro n m"} -goal.tactic {"stateId": 1, "tactic": "assumption"} -goal.delete {"stateIds": [0]} -stat {} -goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"} -stat -``` -where the application of `assumption` should lead to a failure. - -For a list of commands, see [REPL Documentation](doc/repl.md). - -### 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" -export LEAN_PATH="$LIB_MATHLIB:$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: -```sh -ulimit -s unlimited -``` - -## Library Usage +### Library Usage `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call -with `Pantograph` which mirrors the REPL commands above. It is recommended to -call Pantograph via this FFI since it provides a tremendous speed up. - -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. +with `Pantograph` which mirrors the REPL commands above. 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. diff --git a/doc/repl.md b/doc/repl.md index 02d1735..7ee9750 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -1,5 +1,71 @@ # REPL +This documentation is about interacting with the REPL. + +## Examples + +``` sh +pantograph-repl MODULES|LEAN_OPTIONS +``` + +The `pantograph-repl` executable must be run with a list of modules to import. +It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. + +The REPL loop accepts commands as single-line JSON inputs and outputs either an +`Error:` (indicating malformed command) or a JSON return value indicating the +result of a command execution. The command can be passed in one of two formats +``` +command { ... } +{ "cmd": command, "payload": ... } +``` +The list of available commands can be found in `Pantograph/Protocol.lean` and below. An +empty command aborts the REPL. + +Example: (~5k symbols) +``` +$ pantograph Init +env.catalog +env.inspect {"name": "Nat.le_add_left"} +``` +Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) +``` +$ pantograph Mathlib.Analysis.Seminorm +env.catalog +``` +Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof +``` +$ pantograph Init +goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} +goal.tactic {"stateId": 0, "tactic": "intro n m"} +goal.tactic {"stateId": 1, "tactic": "assumption"} +goal.delete {"stateIds": [0]} +stat {} +goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"} +stat +``` +where the application of `assumption` should lead to a failure. + +For a list of commands, see [REPL Documentation](doc/repl.md). + +### 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" +export LEAN_PATH="$LIB_MATHLIB:$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 +``` + ## Commands See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. @@ -15,16 +81,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va current environment to/from a file * `env.module_read { "module": }`: Reads a list of symbols from a module * `env.describe {}`: Describes the imports and modules in the current environment -* `options.set { key: value, ... }`: Set one or more options (not Lean options; those - have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - - One particular option for interest for machine learning researchers is the - automatic mode (flag: `"automaticMode"`). By default it is turned on, with - all goals automatically resuming. This makes Pantograph act like a gym, - with no resumption necessary to manage your goals. - - Set `timeout` to a non-zero number to specify timeout (milliseconds) for all `CoreM` - operations. +* `options.set { key: value, ... }`: Set one or more options. These are not Lean + `CoreM` options; those have to be set via command line arguments.), for + options see below. * `options.print`: Display the current set of options * `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol @@ -63,6 +122,16 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft tactic if possible. +## Options + +The full list of options can be found in `Pantograph/Protocol.lean`. Particularly: +- `automaticMode` (default on): Goals will not become dormant when this is + turned on. By default it is turned on, with all goals automatically resuming. + This makes Pantograph act like a gym, with no resumption necessary to manage + your goals. +- `timeout` (default 0): Set `timeout` to a non-zero number to specify timeout + (milliseconds) for all `CoreM` and frontend operations. + ## Errors When an error pertaining to the execution of a command happens, the returning JSON structure is @@ -77,3 +146,10 @@ Common error forms: * `index`: Indicates an invariant maintained by the output of one command and 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. + +## Troubleshooting + +If lean encounters stack overflow problems when printing catalog, execute this before running lean: +```sh +ulimit -s unlimited +``` -- 2.44.1 From 58b52359e1e40289a7ab2a4ea1d096e6d38ba9ea Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 15:01:00 -0700 Subject: [PATCH 3/3] doc: Wording --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 168efa5..963ef97 100644 --- a/README.md +++ b/README.md @@ -37,7 +37,7 @@ with `Pantograph` which mirrors the REPL commands above. Note that there isn't a Inject any project path via the `pantograph_init_search` function. -## Developing +## Development A Lean development shell is provided in the Nix flake. -- 2.44.1