### Usage Example for recordCommandSnapshot - Lean

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Example demonstrating how to record a command snapshot and obtain its ID for later use.

```lean
let envId ← recordCommandSnapshot cmdSnapshot
-- Later: use envId in a Command with env: envId field
```

--------------------------------

### REPL JSON Commands Examples

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Examples of JSON commands that can be sent to the Lean REPL for processing.

```json
{ "cmd": "def f := 2" }
```

```json
{"env": 0}
```

```json
{ "cmd": "example : f = 2 := rfl", "env": 0 }
```

```json
{"env": 1, "sorries": [{"goal": "⊢ f = 2", "proofState": 0, ...}], "messages": [...]}
```

--------------------------------

### main

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

The main executable entry point for the REPL. It initializes the Lean search path and starts the interactive read-eval-print loop.

```APIDOC
## main

### Description
The main executable entry point. Initializes the Lean search path and starts the read-eval-print loop.

### Signature
```lean
unsafe def main (_ : List String) : IO Unit
```

### Parameters
- `_` (List String) - Command-line arguments (unused)

### Behavior
1. Initializes Lean search path via `Lean.findSysroot`
2. Calls `repl` to begin the interactive loop

### Usage
```shell
lake exe repl < commands.json
```
```

--------------------------------

### Initialize a Lean Session

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Starts a new Lean session and imports the Mathlib library. This is the initial step for any new proof development.

```json
{ "cmd": "import Mathlib" }
```

--------------------------------

### Usage Example for runCommand - Lean

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Demonstrates how to execute a command using `runCommand` and handle the result, whether it's a successful response or an error.

```lean
let cmd : Command := { cmd := "def f := 2", env := none, ... }
let result ← runCommand cmd
match result with
| .inl response => IO.println response.env  -- new env ID
| .inr error => IO.println error.message
```

--------------------------------

### Usage Example for processFile - JSON

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Example of the JSON structure expected for the `File` parameter in `processFile`, specifying the file path and an optional environment ID.

```json
{ "path": "test/file.lean", "env": 3 }
```

--------------------------------

### Minimal REPL Command: Define a Term

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Define a simple term in the Lean REPL. This is a basic example to start the REPL.

```json
{ "cmd": "def f := 2" }
```

--------------------------------

### Lean 4 REPL Environment ID Examples

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/10-architecture.md

Illustrates how Environment IDs are used to reference CommandSnapshot structures, enabling branching, backtracking, and composability.

```lean
ID 0: def f := 2
ID 1: example : f = 2 := rfl  (builds on ID 0)
ID 2: theorem t : True := trivial  (builds on ID 0, skips ID 1)
```

--------------------------------

### Lean REPL Entry Point

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

The main executable entry point for the Lean REPL. It initializes the Lean search path and starts the interactive read-eval-print loop.

```lean
unsafe def main (_ : List String) : IO Unit
```

--------------------------------

### Continue Multi-Step Proof

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Continue a multi-step proof from a given proof state. This example shows completing the proof with 'exact 0'.

```json
{
  "proofState": 1,
  "tactic": "exact 0"
}
```

--------------------------------

### Define a function to pickle an environment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

This example demonstrates how to use the `pickle` function to save the Lean environment's imports and constants to a file. Ensure the `pickle` function is available in the scope.

```lean
def saveEnv (path : FilePath) (env : Environment) : IO Unit :=
  pickle path (env.header.imports, env.constants.map₂) 
```

--------------------------------

### Load Session from Checkpoint

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Loads a previously saved Lean environment state from a file. This is used to resume work or start a new branch from a saved point.

```json
{ "unpickleEnvFrom": "/data/milestone_1.olean" }
```

--------------------------------

### Lean REPL File Mode Output

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Example output from the Lean REPL when processing a file. It details the tactics executed, their proof states, and the resulting environment.

```json
{"tactics":
 [{"tactic": "exact rfl",
   "proofState": 0,
   "pos": {"line": 5, "column": 29},
   "goals": "⊢ f + g = 39",
   "endPos": {"line": 5, "column": 38}}],
 "env": 0}
```

--------------------------------

### Lean File Content

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Example Lean code defining functions and a theorem, used for file processing.

```lean
def f : Nat := 37

def g := 2

theorem h : f + g = 39 := by rfl

```

--------------------------------

### Lean REPL Command Mode Output

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Example output from the Lean REPL when processing a command. It includes sorries with their goal states, any generated messages, and the new environment ID.

```json
{"sorries":
 [{"pos": {"line": 1, "column": 18},
   "endPos": {"line": 1, "column": 23},
   "goal": "⊢ Nat",
   "proofState": 0}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 23},
   "endPos": {"line": 1, "column": 26},
   "data":
   "type mismatch\n  rfl\nhas type\n  f = f : Prop\nbut is expected to have type\n  f = 2 : Prop"}],
 "env": 6}
```

--------------------------------

### Full Info Tree Request

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Use this JSON request to get the complete info tree for a Lean command, including all command, term, and tactic information with syntax details.

```json
{
  "cmd": "def x : Nat := 5",
  "infotree": "full"
}

```

--------------------------------

### Unpickle data from a file

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

This example shows how to load a pickled object of a specific type from a file using `unpickle`. It includes manual memory management by freeing the `CompactedRegion` after processing the data. Ensure the type `Array Import × PHashMap Name ConstantInfo` matches the type used during pickling.

```lean
let (x, region) ← unpickle (Array Import × PHashMap Name ConstantInfo) "file.olean"
let result := process x
region.free
return result
```

--------------------------------

### Get Info Kind

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Returns the discriminator name for an Info union type variant.

```Lean
def kind : Info → String
```

--------------------------------

### Lean.FileMap.stxRange

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Extracts the file position range (start and end) of a syntax node using the provided FileMap.

```APIDOC
## Lean.FileMap.stxRange

### Description
Extracts the file position range (start and end) of a syntax node.

### Parameters
- **fileMap** (FileMap) - File map for position translation
- **stx** (Syntax) - Syntax node

### Returns
Tuple of `(startPos, endPos)` as `Position` records (line, column)
```

--------------------------------

### Initialize Lean Search Path

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/10-architecture.md

Initializes the Lean search path at startup to enable the elaborator to find the Lean standard library and user imports.

```lean
initSearchPath (← Lean.findSysroot)
```

--------------------------------

### Extract Syntax Range

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Extracts the file position range (start and end) of a syntax node using a FileMap.

```Lean
def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position
```

--------------------------------

### Execute Declaration in Fresh Environment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Send a Lean declaration to the REPL to create a new environment. The REPL responds with the ID of the newly created environment.

```JSON
{
  "cmd": "def f : Nat := 2"
}
```

```JSON
{
  "env": 0
}
```

--------------------------------

### Create Proof Step Response

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Constructs a `ProofStepResponse` from a proof snapshot. Use this to generate responses for proof steps, optionally computing deltas from a previous snapshot.

```lean
def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) :
    M m ProofStepResponse
```

```lean
let response ← createProofStepReponse newProofState (some oldProofState)
return .inl response
```

--------------------------------

### REPL Command: Interactive Proof Development

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Initiate interactive proof development by defining a term with a 'sorry' placeholder.

```json
{ "cmd": "def g : Nat := by sorry" }
```

--------------------------------

### Syntax.Range Structure

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/08-types.md

Defines the JSON structure for a source code range, indicating the start and end positions and whether the range is synthetic.

```Lean
structure Syntax.Range where
  synthetic : Bool
  start : Lean.Position
  finish : Lean.Position
deriving ToJson
```

--------------------------------

### Run Command in REPL

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/06-elaboration-frontend.md

Illustrates the typical workflow for executing a command in the Lean REPL, including error handling, info tree analysis, and command snapshot recording.

```lean
def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
  let cmdSnapshot? := s.env.flatMap fun i => (← get).cmdStates[i]?
  let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
  let (initialCmdState, cmdState, messages, trees) ← try
    IO.processInput s.cmd initialCmdState?
  catch ex =>
    return .inr ⟨ex.toString⟩
  -- Extract sorries, tactics, etc. from trees
  let sorries ← sorries trees initialCmdState.env none
  let tactics ← if s.allTactics then tactics trees initialCmdState.env else pure []
  -- Create and return response
  let cmdSnapshot := { cmdState, ... }
  let env ← recordCommandSnapshot cmdSnapshot
  return .inl { env, messages, sorries, tactics }
```

--------------------------------

### Lean Environment Replay Implementation

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Provides the implementation of `replayToElabEnv`, which iterates through new constants, skipping unsafe or partial ones, and adds the rest using `addAlreadyCheckedConstantInfo`.

```lean
def replayToElabEnv (env : Environment)
    (newConstants : Std.HashMap Name ConstantInfo) : Environment :=
  newConstants.fold (init := env) fun env _ ci =>
    if ci.isUnsafe || ci.isPartial then env else addAlreadyCheckedConstantInfo env ci
```

--------------------------------

### Run REPL with Commands

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Execute a sequence of commands in the Lean REPL by piping them from a JSON file.

```shell
lake exe repl < commands.json
```

--------------------------------

### Extract Tactic Name with Lean.Elab.TacticInfo.name?

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Use `name?` to get the outermost parser name of a tactic. This is useful for identifying the specific type of tactic being analyzed.

```Lean
def name? (t : TacticInfo) : Option Name
```

--------------------------------

### Apply Tactics in Interactive Proof

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Demonstrates applying tactics like 'cases' and 'simp' to progress through a proof. Each step refines the goals or completes a case.

```json
{ "proofState": 0, "tactic": "cases n" }
```

```json
{ "proofState": 1, "tactic": "simp" }
```

```json
{ "proofState": 2, "tactic": "simp [IH]" }
```

--------------------------------

### Create a ProofSnapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Constructs a ProofSnapshot from elaboration context and a list of goals. It can optionally take a local context, environment override, root goals, and types for new metavariables.

```lean
def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
    (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
    : IO ProofSnapshot
```

```lean
let snap ← ProofSnapshot.create ctx none none [goal] (some [goal])
```

--------------------------------

### Apply Tactic in Multi-Step Proof

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Execute the first step of a multi-step proof by applying a tactic. The response indicates the new proof state and remaining goals.

```json
{
  "proofState": 0,
  "tactic": "intro x"
}
```

--------------------------------

### Pickle Environment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Serialize a Lean environment to an .olean file.

```json
{ "env": 7, "pickleTo": "path/to/file.olean" }
```

--------------------------------

### Get Proof Status

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Determines the completion status of a proof by evaluating its goals, type checking, and checking for sorries or metavariables. Use this to understand if a proof is fully resolved or has issues.

```lean
def getProofStatus (proofState : ProofSnapshot) : M m String
```

--------------------------------

### Run Lean REPL with Project Environment

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Execute the Lean REPL using 'lake env' to ensure it has access to the local project's dependencies and environment.

```shell
lake env ../path/to/repl/.lake/build/bin/repl < commands.in
```

--------------------------------

### Execute a Proof Step

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Executes a single tactic in a given proof state. It handles parsing the tactic, running it, and returning the new proof state or an error. Use this to advance proofs interactively.

```Lean
def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error)

```

```JSON
{
  "proofState": 0,
  "tactic": "apply Int.natAbs"
}

```

--------------------------------

### Safely unpickle data with automatic cleanup

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

This example uses `withUnpickle` to load a pickled object and execute a continuation function with it. Memory is automatically managed and freed after the continuation completes, even if errors occur. The type annotation `(x : Array Import × PHashMap Name ConstantInfo)` should match the pickled object's type.

```lean
let result ← withUnpickle "file.olean" fun (x : Array Import × PHashMap Name ConstantInfo) => do
  return process x
-- Memory freed automatically, even if process throws
```

--------------------------------

### Main API Functions

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/MANIFEST.txt

Entry points and core command handlers for interacting with the Lean REPL.

```APIDOC
## Entry Points

### `main`

Description: The primary entry point for the REPL application.

### `repl`

Description: Initializes and runs the interactive REPL session.

## Command Handlers

### `runCommand`

Description: Executes a single command within the REPL.

### `runProofStep`

Description: Executes a proof step.

### `processFile`

Description: Processes a Lean file, executing its commands.
```

--------------------------------

### ProofSnapshot.create

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Constructs a ProofSnapshot from elaboration context and goals. It captures the monadic state and context necessary for tactic execution.

```APIDOC
## ProofSnapshot.create

### Description
Constructs a `ProofSnapshot` from elaboration context and a list of goals. It captures the monadic state and context necessary for tactic execution.

### Method
`def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId) := none) (types : List Expr := []) : IO ProofSnapshot`

### Parameters
- `ctx : ContextInfo` - Elaboration context (contains command state, file map, etc.)
- `lctx? : Option LocalContext` - Optional local context (defaults to empty if `none`)
- `env? : Option Environment` - Optional environment override
- `goals : List MVarId` - Goals to include in the snapshot
- `rootGoals? : Option (List MVarId)` - Original goals (for proof status tracking; defaults to `goals`)
- `types : List Expr` - Optional list of types to create as fresh metavariables and add to goals

### Returns
`IO ProofSnapshot` - A `ProofSnapshot` ready for tactic execution.

### Behavior
1. Runs in the `MetaM` monad within the context.
2. Creates fresh metavariables for any provided types.
3. Captures all elaboration state (core, meta, term, tactic).
4. Records root goals.
5. Returns assembled snapshot.

### Usage
```lean
let snap ← ProofSnapshot.create ctx none none [goal] (some [goal])
```
```

--------------------------------

### Run Test Suite

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Execute the test suite which wraps `test.sh` to check the REPL against expected outputs. This is suitable for CI and scripting.

```sh
lake exe test
```

--------------------------------

### Run Syntax as Tactic in ProofSnapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Parses and executes a Syntax object as a tactic within the ProofSnapshot context. Returns the updated snapshot.

```lean
def runSyntax (p : ProofSnapshot) (t : Syntax) : IO ProofSnapshot
```

--------------------------------

### Process Lean File with REPL

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Use the REPL to process an entire Lean file. The 'allTactics' option ensures all tactics within the file are executed.

```shell
echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl
```

--------------------------------

### Load Development Progress (Resume)

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Loads a previously saved environment state from 'checkpoint.olean'. This restores all definitions and theorems available at the time of saving.

```json
{ "unpickleEnvFrom": "checkpoint.olean" }
```

--------------------------------

### Unpickle Proof State from File

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Load a previously pickled proof state from a file. The command returns the identifier for the newly loaded proof state.

```json
{"unpickleProofStateFrom": "path/to/file.olean"}
```

--------------------------------

### Environment IDs in Lean REPL

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Demonstrates how environment IDs are used to reference specific states in the Lean REPL, enabling branching and backtracking.

```lean
env 0 → def f := 2
env 1 → example : f = 2 := rfl
env 2 → theorem t : True := trivial  # alternative path from env 0
```

--------------------------------

### Run a Single Tactic

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Use this to execute a single tactic on a given proof state. Ensure the prerequisite proof state matches.

```json
{
  "proofState": 0,
  "tactic": "exact 2"
}
```

--------------------------------

### REPL Command: Apply Tactic in Interactive Proof

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Apply a specific tactic, 'exact 2', to a given proof state during interactive proof development.

```json
{ "proofState": 0, "tactic": "exact 2" }
```

--------------------------------

### ProofSnapshot.pickle

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Serializes a `ProofSnapshot` to a `.olean` file at the specified path. This process is efficient as it only stores delta information from imports.

```APIDOC
## ProofSnapshot.pickle

### Description
Serializes a `ProofSnapshot` to a `.olean` file. It extracts environment and new constants, compacts monadic states, and serializes essential components.

### Method
Lean Function

### Parameters
- `p` (ProofSnapshot) - The snapshot to serialize.
- `path` (FilePath) - The output file path for the serialized snapshot.

### Returns
- `IO Unit` - An IO action that completes upon successful serialization.
```

--------------------------------

### Enter Tactic Mode in Lean REPL

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Initiate tactic mode by sending a command containing 'sorry'. The 'proofState' index from the response is used to target specific goals.

```json
{"cmd" : "def f (x : Unit) : Nat := by sorry"}
```

--------------------------------

### Lean.Environment.pickle

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Serializes an entire Lean Environment to a .olean file. It efficiently stores only the new constants not present in the environment's imports.

```APIDOC
## Lean.Environment.pickle

### Description
Serializes an entire `Environment` to a `.olean` file. This process extracts imports and only the new constants (delta from imports), pickling them as a tuple. It's efficient as it only stores the delta, resulting in small, shareable files.

### Method
`pickle`

### Signature
```lean
def pickle (env : Environment) (path : FilePath) : IO Unit
```

### Parameters
#### Path Parameters
- **env** (Environment) - Required - The environment to serialize.
- **path** (FilePath) - Required - The output file path for the serialized environment.

### Behavior
1. Extracts the list of imports from the environment header.
2. Extracts only the new constants (delta from imports) via `env.constants.map₂`.
3. Pickles both as a tuple using `_root_.pickle`.

### Portability
The pickled environment is portable to any machine with the same imports available.
```

--------------------------------

### Send Command to Lean REPL

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Send a complete Lean command to the REPL for execution. Use the 'env' field to specify an existing environment for the command.

```json
{"cmd" : "def f := 2"}
```

```json
{"cmd" : "example : f = 2 := rfl", "env" : 1}
```

--------------------------------

### Request All Tactics in a Proof

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Use the `allTactics: true` option to retrieve all substantive tactics applied within a proof definition. The response includes tactic positions and goals.

```json
{
  "cmd": "theorem f : 1 + 1 = 2 := by rfl",
  "allTactics": true
}
```

--------------------------------

### ProofSnapshot.ppGoals

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Pretty-prints the current goals in a given proof snapshot. It formats each goal in the snapshot's tactic state for display.

```APIDOC
## ProofSnapshot.ppGoals

### Description
Pretty-prints the current goals in the snapshot. Uses `Meta.ppGoal` to format each goal in the snapshot's tactic state.

### Method
Lean Function

### Parameters
- `p` (ProofSnapshot) - The snapshot to pretty-print goals from.

### Returns
- `List Format` - A list of formatted goal strings.
```

--------------------------------

### Unpickle Environment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Deserialize a Lean environment from an .olean file.

```json
{ "unpickleEnvFrom": "path/to/file.olean" }
```

--------------------------------

### Process Lean File

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Execute commands from a specified Lean file. Can include all tactics in the response.

```json
{ "path": "test/file.lean", "allTactics": true }
```

--------------------------------

### Explore Proof with Infotrees

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Defines a trivial proof and requests its 'infotree' representation. This enables advanced IDE features like navigation and type inspection.

```json
{ "cmd": "def complex_proof : ∀ n : Nat, n = n := fun n => rfl", "infotree": "substantive" }
```

--------------------------------

### createProofStepReponse

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Constructs a `ProofStepResponse` from a proof snapshot, computing messages, goals, and sorries. It can optionally compute deltas from a previous proof snapshot.

```APIDOC
## createProofStepReponse

### Description
Constructs a `ProofStepResponse` from a proof snapshot, computing messages, goals, and sorries.

### Signature
def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : M m ProofStepResponse

### Parameters
#### Path Parameters
- **proofState** (ProofSnapshot) - The proof snapshot.
- **old?** (Option ProofSnapshot) - Optional. Previous proof snapshot (to compute deltas).

### Returns
- **ProofStepResponse** - The constructed proof step response structure.

### Behavior
1. Computes new messages (delta from `old?` if provided)
2. Computes new info trees (delta from `old?`)
3. Extracts sorries and goals from the state
4. Records the proof snapshot and returns its ID
5. Evaluates overall proof status
6. Assembles response with all fields

### Example
```lean
let response ← createProofStepReponse newProofState (some oldProofState)
return .inl response
```
```

--------------------------------

### runProofStep

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Executes a single tactic in a given proof state. It takes a ProofStep object containing the proof state ID and the tactic to run, and returns either a ProofStepResponse with the updated proof state or an Error.

```APIDOC
## runProofStep

### Description
Executes a single tactic in a proof state.

### Method
Not applicable (function call)

### Signature
def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error)

### Parameters
- **s** (ProofStep) - The `ProofStep` object containing the `proofState` ID and the `tactic` string.

### Returns
- `.inl` — `ProofStepResponse` with new proof state ID and resulting goals.
- `.inr` — `Error` with message.

### Behavior
1. Looks up proof state by ID; fails if not found.
2. Parses the tactic string and runs it via `proofState.runString`.
3. Creates a `ProofStepResponse` with the new goals, messages, and status.
4. Records the new proof state if not failed.

### Failures
- Unknown proof state ID → error "Unknown proof state."
- Parse error → error "Lean error:\n" + parser error
- Tactic failure → error "Lean error:\n" + tactic error

### Usage Example
```json
{ "proofState": 0, "tactic": "apply Int.natAbs" }
```
```

--------------------------------

### ProofSnapshot.runSyntax

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Parses and executes a `Syntax` object as a tactic within the context of a `ProofSnapshot`, returning the updated snapshot.

```APIDOC
## ProofSnapshot.runSyntax

### Description
Parses and executes a `Syntax` object as a tactic within the context of a `ProofSnapshot`, returning the updated snapshot.

### Method
`def runSyntax (p : ProofSnapshot) (t : Syntax) : IO ProofSnapshot`

### Parameters
- `p : ProofSnapshot` - The snapshot to run the tactic in.
- `t : Syntax` - The pre-parsed `Syntax` object representing the tactic.

### Returns
`IO ProofSnapshot` - The updated `ProofSnapshot` after executing the tactic.

### Behavior
Calls `evalTactic` on the syntax within the snapshot's tactic monad.
```

--------------------------------

### Pickle Command Snapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Picks an environment after running a command, saving its state. It handles unknown environments and uses the `Lean.Environment.pickle` utility. Returns either the updated environment or an error message.

```Lean
-- Pickle an environment after running a command
def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do
  match (← get).cmdStates[n.env]? with
  | none => return .inr ⟨"Unknown environment."⟩
  | some env ->
    discard <| env.pickle n.pickleTo  -- Uses Lean.Environment.pickle
    return .inl { env := n.env }
```

--------------------------------

### Serialize Lean Environment to .olean File

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Serializes an entire Lean `Environment` to a specified file path. It extracts imports and new constants, storing only the delta for efficiency and portability.

```lean
def pickle (env : Environment) (path : FilePath) : IO Unit
```

--------------------------------

### Run Command - Lean

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Executes a Lean command, returning either a CommandResponse or an Error. It handles environment lookup, command elaboration, and snapshot recording.

```lean
def runCommand (s : Command) : M IO (CommandResponse ⊕ Error)
```

--------------------------------

### Pickle Environment to File

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Save the current REPL environment to a specified file path. This allows for later restoration of the environment.

```json
{"pickleTo": "path/to/file.olean", "env": 7}
```

--------------------------------

### Lean.Elab.TacticInfo.goalStateAfter

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Pretty-prints the state of the goals after the tactic was executed.

```APIDOC
## Lean.Elab.TacticInfo.goalStateAfter

### Description
Retrieves and pretty-prints the state of the goals as they were after the tactic was applied.

### Parameters
- `info` (TacticInfo) - Tactic info containing the goal state after execution.
- `ctx` (ContextInfo) - The Lean context.

### Returns
`IO (List Format)` - A list of formatted strings, each representing a goal.
```

--------------------------------

### Pickle Proof State to File

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Save a specific proof state to a file. This is useful for preserving intermediate proof states for later use.

```json
{"pickleTo": "path/to/file.olean", "proofState": 17}
```

--------------------------------

### Import a Mathlib Module

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Imports a module from the Mathlib library. This is typically the first step in a development phase to access predefined definitions and theorems.

```json
{ "cmd": "import Mathlib.Data.List.Basic" }
```

--------------------------------

### Process File - Lean

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Reads a file and processes its content as a single Lean command. It wraps `runCommand` and handles potential I/O errors during file reading.

```lean
def processFile (s : File) : M IO (CommandResponse ⊕ Error)
```

--------------------------------

### Proof State IDs in Lean REPL

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/README.md

Illustrates the use of proof state IDs to track the progress of a proof, showing the evolution of goals during tactic-based development.

```lean
proofState 0 → goal: x : Unit ⊢ Nat
proofState 1 → goal: ⊢ Nat  (after intro x)
proofState 2 → goal: (none)  (after exact 0)
```

--------------------------------

### runCommand

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Executes a Lean command, returning either a CommandResponse or an Error. It handles command parsing, elaboration, and snapshot recording.

```APIDOC
## runCommand

### Description
Executes a Lean command, returning either a `CommandResponse` or an `Error`. It handles command parsing, elaboration, and snapshot recording.

### Method Signature
```lean
def runCommand (s : Command) : M IO (CommandResponse ⊕ Error)
```

### Parameters
* `s` (Command) - The `Command` to execute (contains `cmd`, optional `env`, and options)

### Returns
* `.inl` (`CommandResponse`) - Contains environment ID, messages, sorries, tactics
* `.inr` (`Error`) - Contains message string

### Behavior
1. Looks up prior environment by ID (if `env` field specified); fails if not found
2. Parses and elaborates the command text via `IO.processInput`
3. Collects sorries, messages, and tactics (if requested)
4. Creates a new `CommandSnapshot` and records it
5. Optionally extracts and serializes the info tree based on the `infotree` option

### Failures
* Unknown prior environment ID → error "Unknown environment."
* Lean elaboration error → error with elaborator exception message

### Usage Example
```lean
let cmd : Command := { cmd := "def f := 2", env := none, ... }
let result ← runCommand cmd
match result with
| .inl response => IO.println response.env  -- new env ID
| .inr error => IO.println error.message
```
```

--------------------------------

### PickleEnvironment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/08-types.md

Represents a request to serialize a command environment.

```APIDOC
## PickleEnvironment

### Description
Represents a request to serialize a command environment.

### Structure
```lean
structure PickleEnvironment where
  env : Nat
  pickleTo : System.FilePath
deriving ToJson, FromJson
```

### Fields
- `env` (Nat) - The environment to serialize.
- `pickleTo` (System.FilePath) - The file path to save the serialized environment.
```

--------------------------------

### Execute Lean Command

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Send a Lean command to be executed. Can specify an environment ID to build upon.

```json
{ "cmd": "def f := 2" }
```

```json
{ "cmd": "example : f = 2 := rfl", "env": 1 }
```

--------------------------------

### Run String as Tactic in ProofSnapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Parses a string as a tactic and executes it within the ProofSnapshot context. It handles parsing errors and returns the updated snapshot.

```lean
def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot
```

```lean
let newSnap ← proofSnap.runString "apply Int.natAbs"
```

--------------------------------

### ProofSnapshot.runCoreM

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Executes a `CoreM` computation within the context of a `ProofSnapshot`, returning the result and the updated snapshot.

```APIDOC
## ProofSnapshot.runCoreM

### Description
Executes a `CoreM` computation within the context of a `ProofSnapshot`, returning the result and the updated snapshot.

### Method
`def runCoreM (p : ProofSnapshot) (t : CoreM α) : IO (α × ProofSnapshot)`

### Parameters
- `p : ProofSnapshot` - The snapshot to run the computation in.
- `t : CoreM α` - The `CoreM` computation to execute.

### Returns
`IO (α × ProofSnapshot)` - A tuple containing the result of the computation and the potentially updated `ProofSnapshot`.
```

--------------------------------

### Deserialize Lean Environment from .olean File

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Deserializes a Lean `Environment` from a `.olean` file. It reconstructs the environment by replaying new constants after initializing with the stored imports. Requires initializers to be executed.

```lean
def unpickle (path : FilePath) : IO (Environment × CompactedRegion)
```

--------------------------------

### pickleCommandSnapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Serializes a command environment to a .olean file. It looks up the environment by ID, serializes it relative to imports, and returns the environment ID.

```APIDOC
## pickleCommandSnapshot

### Description
Serializes a command environment to a `.olean` file. It looks up the environment by ID, serializes it relative to imports, and returns the environment ID.

### Method
```lean
def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error)
```

### Parameters
- `n` — `PickleEnvironment` with environment ID and output path

### Returns
`CommandResponse` with the environment ID, or error
```

--------------------------------

### Record Proof Snapshot - Lean

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Records a ProofSnapshot and returns its numeric ID. This is analogous to recording command snapshots but for proof states.

```lean
def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat
```

--------------------------------

### Serialization Utilities

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/MANIFEST.txt

Functions for serializing and deserializing command and proof states.

```APIDOC
## Serialization

### `pickleCommandSnapshot`

Description: Serializes a command snapshot.

### `unpickleCommandSnapshot`

Description: Deserializes a command snapshot.

### `pickleProofSnapshot`

Description: Serializes a proof snapshot.

### `unpickleProofSnapshot`

Description: Deserializes a proof snapshot.
```

--------------------------------

### Unpickle Environment from File

Source: https://github.com/leanprover-community/repl/blob/master/README.md

Load a previously pickled environment from a file. The command returns the identifier for the newly loaded environment.

```json
{"unpickleEnvFrom": "path/to/file.olean"}
```

--------------------------------

### Save Development Progress (Checkpoint)

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Saves the current environment state to a file named 'checkpoint.olean'. This allows for resuming development later from this exact point.

```json
{ "env": 2, "pickleTo": "checkpoint.olean" }
```

--------------------------------

### ProofSnapshot.runString

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Parses a string as a tactic and executes it within the context of a `ProofSnapshot`, returning the updated snapshot. Handles parsing errors.

```APIDOC
## ProofSnapshot.runString

### Description
Parses a string as a tactic and executes it within the context of a `ProofSnapshot`, returning the updated snapshot. Handles parsing errors.

### Method
`def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot`

### Parameters
- `p : ProofSnapshot` - The snapshot to run the tactic in.
- `t : String` - The tactic source code as a string.

### Returns
`IO ProofSnapshot` - The updated `ProofSnapshot` after executing the tactic.

### Behavior
1. Parses string using `Parser.runParserCategory` with `tactic` category.
2. If parse error, throws `IO.userError`.
3. Otherwise, calls `runSyntax`.

### Example
```lean
let newSnap ← proofSnap.runString "apply Int.natAbs"
```
```

--------------------------------

### Lean Environment Replay Function Signature

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Defines the signature for `replayToElabEnv`, which takes an environment and a map of new constants to return an updated environment.

```lean
def replayToElabEnv (env : Environment)
    (newConstants : Std.HashMap Name ConstantInfo) : Environment
```

--------------------------------

### Exception Handling in REPL

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/10-architecture.md

Wraps command processing in a try-catch block to handle Lean exceptions gracefully. Converts exceptions to error responses, preventing REPL crashes.

```lean
let (initialCmdState, cmdState, messages, trees) ← try
  IO.processInput s.cmd initialCmdState?
catch ex =>
  return .inr ⟨ex.toString⟩
```

--------------------------------

### ProofSnapshot.unpickle

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Deserializes a `ProofSnapshot` from a `.olean` file. It reconstructs the environment and restores elaboration state, optionally using a command snapshot.

```APIDOC
## ProofSnapshot.unpickle

### Description
Deserializes a `ProofSnapshot` from a `.olean` file. Reconstructs the environment, restores elaboration state, and reactivates open scoped declarations.

### Method
Lean Function

### Parameters
- `path` (FilePath) - The input file path for the serialized snapshot.
- `cmd?` (Option CommandSnapshot) - An optional command snapshot used to restore environment context. If `none`, imports are loaded fresh.

### Returns
- `IO (ProofSnapshot × CompactedRegion)` - An IO action returning a tuple of the deserialized `ProofSnapshot` and its `CompactedRegion`.
```

--------------------------------

### Pickle Proof State Request

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Serializes a specified proof state to an .olean file.

```APIDOC
## Pickle Proof State Request

### Description
Serializes a specified proof state to an .olean file.

### Method
Not applicable (JSON RPC)

### Endpoint
Not applicable (JSON RPC)

### Parameters
#### Request Body
- **proofState** (Nat) - Required - Proof state ID to serialize
- **pickleTo** (System.FilePath) - Required - Output .olean file path

### Request Example
```json
{ "proofState": 17, "pickleTo": "path/to/file.olean" }
```

### Response
#### Success Response
Indicates successful serialization of the proof state.
```

--------------------------------

### Chain Commands in Existing Environment

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Execute a command in an existing environment by specifying its ID. This allows for sequential development and building upon previous definitions.

```JSON
{
  "cmd": "example : f = 2 := rfl",
  "env": 0
}
```

```JSON
{
  "env": 1
}
```

--------------------------------

### Lean.Environment.unpickle

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/07-utilities-api.md

Deserializes a Lean Environment from a .olean file. It reconstructs the environment by replaying imports and new constants.

```APIDOC
## Lean.Environment.unpickle

### Description
Deserializes a Lean `Environment` from a `.olean` file. This function reconstructs the environment by reading pickled imports and new constants, initializing a fresh environment with the imports, and then adding the new constants.

### Method
`unpickle`

### Signature
```lean
def unpickle (path : FilePath) : IO (Environment × CompactedRegion)
```

### Parameters
#### Path Parameters
- **path** (FilePath) - Required - The input file path from which to deserialize the environment.

### Returns
A tuple containing the restored `Environment` and its associated `CompactedRegion`.

### Behavior
1. Reads the pickled tuple (imports, new constants) from the specified file path.
2. Initializes a fresh `Environment` with the listed imports.
3. Adds the new constants via `replayToElabEnv`.
4. Returns the reconstructed environment and memory region.

### Initialization
Calls `enableInitializersExecution` to run initializers during import, which is necessary for correct environment setup.
```

--------------------------------

### Lean.Elab.IO.processInput

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/06-elaboration-frontend.md

High-level entry point for processing Lean code, with or without an existing command state. It handles parsing, imports, and command elaboration.

```APIDOC
## Lean.Elab.IO.processInput

### Description
High-level entry point for processing Lean code, with or without an existing command state. It parses headers, processes imports, and elaborates commands.

### Method
IO

### Endpoint
N/A (Function Call)

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **input** (String) - Required - Lean source code to process
- **cmdState?** (Option Command.State) - Optional - Prior command state. `none` processes as a fresh module, `some state` adds to the existing environment.
- **opts** (Options) - Optional - Parser/elaborator options (defaults to empty)
- **fileName** (Option String) - Optional - File name for error messages (defaults to `"<input>"`)

### Request Example
```lean
let (headerState, cmdState, msgs, trees) ← processInput "def f := 2" none
```

### Response
#### Success Response
Tuple of:
1. **Command.State** - State after processing headers (imports, etc.) only
2. **Command.State** - State after processing entire input
3. **List Message** - All messages from both phases
4. **List InfoTree** - Info trees from the command phase

#### Response Example
```json
{
  "headerState": { ... },
  "cmdState": { ... },
  "msgs": [ ... ],
  "trees": [ ... ]
}
```
```

--------------------------------

### Lean.Elab.TacticInfo.runMetaMGoalsBefore

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/05-infotree-api.md

Runs a computation on the list of metavariable goals present before a tactic application.

```APIDOC
## Lean.Elab.TacticInfo.runMetaMGoalsBefore

### Description
Executes a given computation using the metavariable goals that existed immediately before the tactic was applied.

### Parameters
- `info` (TacticInfo) - Tactic info containing the metavariable context before the tactic.
- `ctx` (ContextInfo) - The Lean context.
- `x` (List MVarId → MetaM α) - The computation to run, which takes a list of metavariable IDs.

### Returns
`IO α` - The result of the executed computation.
```

--------------------------------

### Process Commands with Info Trees

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/06-elaboration-frontend.md

Processes commands from a parser state and returns elaboration state, messages, and info trees. Enables `infoState` to capture elaboration details.

```lean
def processCommandsWithInfoTrees
    (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
    (commandState : Command.State) : IO (Command.State × List Message × List InfoTree)
```

--------------------------------

### CommandSnapshot.pickle

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Serializes a CommandSnapshot to a .olean file for later resumption. It extracts the environment and its imports, then serializes a compacted version of the command state, omitting the environment and non-essential caches.

```APIDOC
## CommandSnapshot.pickle

### Description
Serializes a `CommandSnapshot` to a `.olean` file for later resumption.

### Method
`IO Unit` (Implicitly called via `CommandSnapshot.pickle` function)

### Endpoint
N/A (Function call)

### Parameters
- **p** (`CommandSnapshot`) - The snapshot to serialize
- **path** (`FilePath`) - Output file path

### Request Example
```lean
let snapshot : CommandSnapshot := ...
CommandSnapshot.pickle snapshot "session.olean"
```

### Response
#### Success Response (200)
`IO Unit` - Indicates successful serialization.

#### Response Example
N/A (void return type)
```

--------------------------------

### Define a Theorem in the Second Milestone

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/09-examples.md

Defines a theorem 'thm_2' in a new environment (env 2), potentially after loading a checkpoint. This continues the proof development.

```json
{ "cmd": "def thm_2 : 1 = 1 := rfl", "env": 2 }
```

--------------------------------

### CompactableCommandSnapshot Structure

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/04-snapshots-api.md

Represents a trimmed version of Command.State used during pickling. It omits the environment and caches, focusing on essential components like scopes and name generators.

```lean
structure CompactableCommandSnapshot where
  scopes         : List Scope := [{ header := "" }]
  nextMacroScope : Nat     := firstFrontendMacroScope + 1
  maxRecDepth    : Nat
  nextInstIdx    : Nat := 1
  ngen           : NameGenerator  := {}
```

--------------------------------

### pickleProofSnapshot

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Serializes a proof state to a .olean file. It looks up the proof state by ID, serializes it, and returns a response with the proof state ID.

```APIDOC
## pickleProofSnapshot

### Description
Serializes a proof state to a `.olean` file. It looks up the proof state by ID, serializes it, and returns a response with the proof state ID.

### Method
```lean
def pickleProofSnapshot (n : PickleProofState) : M m (ProofStepResponse ⊕ Error)
```

### Parameters
- `n` — `PickleProofState` with proof state ID and output path

### Returns
`ProofStepResponse`, or error
```

--------------------------------

### Pickle Environment Request

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/02-json-protocol.md

Serializes a specified environment to an .olean file.

```APIDOC
## Pickle Environment Request

### Description
Serializes a specified environment to an .olean file.

### Method
Not applicable (JSON RPC)

### Endpoint
Not applicable (JSON RPC)

### Parameters
#### Request Body
- **env** (Nat) - Required - Environment ID to serialize
- **pickleTo** (System.FilePath) - Required - Output .olean file path

### Request Example
```json
{ "env": 7, "pickleTo": "path/to/file.olean" }
```

### Response
#### Success Response
Indicates successful serialization of the environment.
```

--------------------------------

### CommandOptions

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/08-types.md

Options for command and file processing, inherited by Command and File.

```APIDOC
## CommandOptions

### Description
Options for command and file processing. Inherited by `Command` and `File`.

### Structure
```lean
structure CommandOptions where
  allTactics : Option Bool := none
  rootGoals : Option Bool := none
  infotree : Option String
```

### Fields
- `allTactics` (Option Bool) - Include all substantive tactic applications in response.
- `rootGoals` (Option Bool) - Include root goals as sorries in response.
- `infotree` (Option String) - Info tree detail level: "full", "tactics", "original", or "substantive", or `none`.
```

--------------------------------

### Collect Root Goals as Sorries

Source: https://github.com/leanprover-community/repl/blob/master/_autodocs/03-main-api.md

Treats all root goals in a tactic proof as 'sorries' by creating a proof snapshot for each. This function is used when the `rootGoals: true` option is set to analyze initial goals as if they were explicit `sorry` placeholders.

```lean
def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry)
```