aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 2 Packages Projects Releases Wiki Activity

feat(frontend): Command-level frontend.process #229

Merged
aniva merged 3 commits from frontend/command into dev 2025-07-11 16:05:57 -07:00
Conversation 0 Commits 3 Files Changed 6 +164 -109
6 changed files with 164 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
Pantograph/Frontend/Basic.lean
View File

@ -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

6
Pantograph/Library.lean
View File

@ -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

84
README.md
View File

@ -25,91 +25,19 @@ 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.
## Developing
## Development
A Lean development shell is provided in the Nix flake.

7
Repl.lean
View File

@ -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

17
Test/Frontend.lean
View File

@ -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 := "<anonymous>"
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 := "

96
doc/repl.md
View File

@ -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": <name> }`: 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": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
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
```