### Install Pre-commit Hooks

Source: https://github.com/leanprover/pantograph/blob/dev/doc/contributing.md

Install pre-commit hooks for ensuring code quality and commit message compliance. Use either 'prek' or 'pre-commit' for installation.

```sh
prek install
```

```sh
pre-commit install --install-hooks
```

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

### REPL Basic Usage Example

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Example of running the REPL with the `Init` module and inspecting a symbol.

```sh
$ repl Init
env.catalog {}
env.inspect {"name": "Nat.le_add_left"}
```

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

### REPL Theorem Proving Example

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Demonstrates proving a theorem using REPL commands. Use `goal.start` to prime the proof.

```sh
$ repl 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
```

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

### REPL Mathlib4 Usage Example

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Example of running the REPL with the `Mathlib.Analysis.Seminorm` module. This may cause stack overflows on large libraries.

```sh
$ repl Mathlib.Analysis.Seminorm
env.catalog {}
```

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

### Build Pantograph without Nix

Source: https://github.com/leanprover/pantograph/blob/dev/README.md

For non-Nix users, install 'lake' and 'lean' and use this command to build the executable.

```sh
lake build
```

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

### Lean Pattern Matching Formatting

Source: https://github.com/leanprover/pantograph/blob/dev/doc/contributing.md

Demonstrates the required formatting for pattern matching in 'let' bindings within Lean code. The '|' should be on the next line for clarity.

```lean
let .some result := function
  | fail "incorrect"
```

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

### Run All Tests with Nix

Source: https://github.com/leanprover/pantograph/blob/dev/doc/contributing.md

Execute all project tests using the Nix flake. This is the recommended way to ensure all checks pass.

```sh
nix flake check
```

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

### REPL Executable Usage

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

The `repl` executable accepts modules to import and Lean options. Use `lake exe repl` to run it.

```sh
repl MODULES|LEAN_OPTIONS
```

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

### Run All Tests with Lake

Source: https://github.com/leanprover/pantograph/blob/dev/doc/contributing.md

Execute all project tests using the Lake build tool. This provides an alternative to Nix for running tests.

```sh
lake test
```

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

### Goal Management Commands

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Commands for managing and interacting with proof goals.

```APIDOC
## GOAL.START

### Description
Start a new proof from a given expression or symbol.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.start

### Parameters
#### Request Body
- **name** (string) - Optional - The name of the proof.
- **expr** (string) - Optional - The expression to prove.
- **levels** (array) - Optional - An array of levels.
- **copyFrom** (string) - Optional - Symbol to copy the proof from.

### Request Example
```json
{
  "expr": "∀ (n : Nat), n = n",
  "name": "reflexivity"
}
```

## GOAL.TACTIC

### Description
Execute a tactic string on a given goal site. The tactic is supplied as additional key-value pairs.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.tactic

### Parameters
#### Request Body
- **stateId** (string) - Required - The ID of the current state.
- **goalId** (string) - Optional - The ID of the specific goal to apply the tactic to.
- **autoResume** (boolean) - Optional - Whether to automatically resume after tactic execution.
- **tactic** (string) - Optional - The tactic to execute.
- **mode** (string) - Optional - The tactic mode (e.g., `tactic`, `conv`, `calc`).
- **expr** (string) - Optional - An expression to assign to the current goal.
- **have** (string) - Optional - An expression to use with the `have` tactic.
- **binderName** (string) - Optional - The name for a binder created by `have` or `let`.
- **let** (string) - Optional - An expression to use with the `let` tactic.
- **draft** (string) - Optional - An expression to draft with `sorry`s.

### Request Example
```json
{
  "stateId": "123",
  "tactic": "intro h",
  "goalId": "456"
}
```

## GOAL.CONTINUE

### Description
Execute continuation/resumption of a goal state.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.continue

### Parameters
#### Request Body
- **stateId** (string) - Required - The ID of the state to continue from.
- **branch** (string) - Optional - The ID of the branch to continue on.
- **goals** (array) - Optional - An array of goal names to resume.

### Request Example
```json
{
  "stateId": "123",
  "goals": ["goal1", "goal2"]
}
```

## GOAL.SUBSUME

### Description
Determine if any goal in `candidates` subsumes the specified `goal`. Returns the subsumptor and a new state ID if successful.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.subsume

### Parameters
#### Request Body
- **stateId** (string) - Required - The ID of the state containing the goal.
- **goal** (string) - Required - The goal to check for subsumption.
- **candidates** (array) - Required - An array of candidate goal IDs.
- **srcStateId** (string) - Optional - The ID of the source state for candidates.

### Request Example
```json
{
  "stateId": "123",
  "goal": "goalA",
  "candidates": ["goalB", "goalC"]
}
```

## GOAL.REMOVE

### Description
Drop the goal states specified in the list.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.remove

### Parameters
#### Request Body
- **stateIds** (array) - Required - An array of state IDs to remove.

### Request Example
```json
{
  "stateIds": ["123", "456"]
}
```

## GOAL.PRINT

### Description
Print a goal state.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.print

### Parameters
#### Request Body
- **stateId** (string) - Required - The ID of the state to print.

## GOAL.SAVE

### Description
Save a goal state to a file.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.save

### Parameters
#### Request Body
- **id** (string) - Required - The ID of the goal state to save.
- **path** (string) - Required - The file path to save the state to.

## GOAL.LOAD

### Description
Load a goal state from a file. The environment is not carried with the state.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/goal.load

### Parameters
#### Request Body
- **path** (string) - Required - The file path to load the state from.

### Note
The user is responsible to ensure the sender/receiver instances share the same environment.
```

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

### REPL Command Formats

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

After the `ready.` signal, REPL accepts commands in JSON format. Use either `command { ... }` or `{ "cmd": command, "payload": ... }`.

```json
command { ... }
```

```json
{ "cmd": command, "payload": ... }
```

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

### Build Pantograph with Nix

Source: https://github.com/leanprover/pantograph/blob/dev/README.md

Use this command for Nix users to build either the shared library or executable of Pantograph.

```sh
nix build .#{sharedLib,executable}
```

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

### Expression and Environment Commands

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Commands for inspecting and manipulating Lean expressions and environments.

```APIDOC
## EXPR.ECHO

### Description
Determine the type of an expression and format it.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/expr.echo

### Parameters
#### Request Body
- **expr** (string) - Required - The expression to evaluate.
- **type** (string) - Optional - The expected type of the expression.
- **levels** (array) - Optional - An array of levels.

### Request Example
```json
{
  "expr": "Nat.add",
  "type": "Nat -> Nat -> Nat",
  "levels": ["zero"]
}
```

## ENV.CATALOG

### Description
Display a list of all safe Lean symbols in the current environment.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.catalog

## ENV.INSPECT

### Description
Show the type and package of a given symbol. If the `value` flag is set, the value is printed or hidden.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.inspect

### Parameters
#### Request Body
- **name** (string) - Required - The name of the symbol.
- **value** (boolean) - Optional - If true, print the value; otherwise, hide it. Defaults to false.

### Request Example
```json
{
  "name": "Nat.add",
  "value": true
}
```

## ENV.SAVE

### Description
Save the current environment to a file.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.save

### Parameters
#### Request Body
- **path** (string) - Required - The file path to save the environment to.

## ENV.LOAD

### Description
Load an environment from a file.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.load

### Parameters
#### Request Body
- **path** (string) - Required - The file path to load the environment from.

## ENV.MODULE_READ

### Description
Reads a list of symbols from a module.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.module_read

### Parameters
#### Request Body
- **module** (string) - Required - The name of the module.

## ENV.DESCRIBE

### Description
Describes the imports and modules in the current environment.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.describe

## ENV.PARSE

### Description
Parse a bit of syntax and returns the parser's terminal position.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/env.parse

### Parameters
#### Request Body
- **input** (string) - Required - The input string to parse.
- **category** (string) - Required - The parser category.

### Request Example
```json
{
  "input": "variable x : Nat",
  "category": "term"
}
```
```

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

### Frontend Processing Commands

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Commands for processing Lean files with the frontend.

```APIDOC
## FRONTEND.PROCESS

### Description
Executes the Lean frontend on a file, collecting tactic invocations or new constants.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/frontend.process

### Parameters
#### Request Body
- **fileName** (string) - Optional - The name of the file to process.
- **file** (string) - Optional - The content of the file to process.
- **readHeader** (boolean) - Required - Whether to read the header.
- **inheritEnv** (boolean) - Required - Whether to inherit the environment.
- **invocations** (string) - Required - Path to collect tactic invocations.
- **newConstants** (boolean) - Required - Whether to collect new constants.

### Request Example
```json
{
  "file": "def foo : Nat := 0",
  "readHeader": true,
  "inheritEnv": false,
  "invocations": "./invocations.txt",
  "newConstants": true
}
```

## FRONTEND.DISTIL

### Description
Extract condensed search targets from a file. Coupled search targets will be condensed into one.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/frontend.distil

### Parameters
#### Request Body
- **file** (string) - Required - The content of the file.
- **binderName** (string) - Optional - Override the binder name (e.g., `f`).
- **ignoreValues** (boolean) - Required - If false, incorporate existing solutions.

### Request Example
```json
{
  "file": "theorem ex : True := by sorry",
  "binderName": "h",
  "ignoreValues": false
}
```

## FRONTEND.TRACK

### Description
Check if one file conforms to another. Declarations in `src` can have `sorry`s that declarations in `dst` would fill.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/frontend.track

### Parameters
#### Request Body
- **src** (string) - Required - The source file content.
- **dst** (string) - Required - The destination file content.

### Request Example
```json
{
  "src": "theorem ex : True := by sorry",
  "dst": "theorem ex : True := rfl"
}
```

## FRONTEND.REFACTOR (Experimental)

### Description
Group dependent `sorry`s into one single `sorry`. Currently only flat dependencies are supported.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/frontend.refactor

### Parameters
#### Request Body
- **file** (string) - Required - The file content.
- **coreOptions** (array) - Required - Core options in the format `["<key>=<val>"]`.

### Request Example
```json
{
  "file": "def f : Nat := sorry",
  "coreOptions": [["someKey=someValue"]]
}
```
```

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

### Setting LEAN_PATH for Project Environment

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Configures the `LEAN_PATH` environment variable to include library paths for using Pantograph in a project. Libraries must be built beforehand.

```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 repl $@
```

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

### Troubleshooting Lean Stack Overflow

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Execute this command in your shell to remove stack size limitations when Lean encounters stack overflow problems while printing the catalog.

```sh
ulimit -s unlimited
```

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

### Run Individual Test with Lake

Source: https://github.com/leanprover/pantograph/blob/dev/doc/contributing.md

Run a specific test by providing a prefix. This is useful for debugging or focusing on a particular test case.

```sh
lake test -- Frontend/Collect
```

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

### Extracting LEAN_PATH

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Command to extract the `LEAN_PATH` environment variable for any project.

```sh
lake env printenv LEAN_PATH
```

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

### Cache and Statistics Commands

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Commands for managing cached data and displaying system statistics.

```APIDOC
## RESET

### Description
Delete all cached expressions and proof trees.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/reset

## STAT

### Description
Display resource usage statistics.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/stat
```

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

### Options Management Commands

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

Commands for setting and viewing Pantograph options.

```APIDOC
## OPTIONS.SET

### Description
Set one or more options. These are not Lean `CoreM` options.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/options.set

### Parameters
#### Request Body
- **key** (string) - Required - The option key.
- **value** (any) - Required - The value to set for the option.

### Request Example
```json
{
  "key": "someOption",
  "value": "someValue"
}
```

## OPTIONS.PRINT

### Description
Display the current set of options.

### Method
POST

### Endpoint
/leanprover/pantograph/commands/options.print
```

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

### Pantograph Error JSON Structure

Source: https://github.com/leanprover/pantograph/blob/dev/doc/repl.md

This JSON structure is returned when an error occurs during command execution in Pantograph. It includes the error type and a description.

```json
{
  "error": "type",
  "desc": "description"
}
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.