diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index e7d3a70..786c10f 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -5,20 +5,20 @@ on: branches: - main paths: - - 'docs/**' - - 'mkdocs.yml' - - 'src/lean_interact/**' - - '.github/workflows/docs.yml' + - "docs/**" + - "mkdocs.yml" + - "src/lean_interact/**" + - ".github/workflows/docs.yml" tags: - - 'v*' # Deploy on version tags + - "v*" # Deploy on version tags workflow_dispatch: inputs: version: - description: 'Version to deploy (e.g., v0.7.0, latest, dev)' + description: "Version to deploy (e.g., v0.7.0, latest, dev)" required: false - default: 'dev' + default: "dev" alias: - description: 'Alias for this version (e.g., stable, latest)' + description: "Alias for this version (e.g., stable, latest)" required: false # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages @@ -29,7 +29,7 @@ permissions: # Allow only one concurrent deployment concurrency: - group: 'pages' + group: "pages" cancel-in-progress: false jobs: @@ -44,7 +44,7 @@ jobs: - name: Setup Python uses: actions/setup-python@v5 with: - python-version: '3.10' + python-version: "3.10" - name: Install uv uses: astral-sh/setup-uv@v4 @@ -72,6 +72,8 @@ jobs: - name: Generate changelog run: | + # First wait a bit to ensure changelogs from the last release are available + sleep 120 uv run python docs/generate_changelog.py - name: Determine version and alias diff --git a/README.md b/README.md index dc36196..ff8a8c1 100644 --- a/README.md +++ b/README.md @@ -15,10 +15,12 @@ Check the [documentation](https://augustepoiroux.github.io/LeanInteract/) for de - **πŸ”— Interactivity**: Execute Lean code and files directly from Python. - **πŸš€ Ease of Use**: LeanInteract abstracts the complexities of Lean setup and interaction. - **πŸ’» Cross-platform**: Works on Windows, macOS, and Linux operating systems. -- **πŸ”§ Compatibility**: Supports all Lean versions between `v4.7.0-rc1` and `v4.24.0-rc1`. +- **πŸ”§ Compatibility**: Supports all Lean versions between `v4.8.0-rc1` and `v4.24.0-rc1`. - We backport the latest features of Lean REPL to older versions of Lean (see [fork](https://github.com/augustepoiroux/repl)). - **πŸ“¦ Temporary Projects**: Easily instantiate temporary Lean environments. - Useful for experimenting with benchmarks depending on [Mathlib](https://github.com/leanprover-community/mathlib4) like [ProofNet#](https://huggingface.co/datasets/PAug/ProofNetSharp) and [MiniF2F](https://github.com/yangky11/miniF2F-lean4). +- **🧾 Data extraction (new in v0.9.0)**: Extract declarations and info trees for analysis and dataset building. +- **⚑ Incremental + Parallel elaboration (new in v0.9.0)**: Automatically reuse partial computations from previous commands, and enable `Elab.async` for faster processing. ## Table of Contents @@ -221,7 +223,7 @@ ProofStepResponse(proof_state=3, goals=[], proof_status='Completed') #### Specific Lean version ```python -config = LeanREPLConfig(lean_version="v4.7.0") +config = LeanREPLConfig(lean_version="v4.8.0") ``` #### Existing Lean projects @@ -374,6 +376,14 @@ response = server.run(FileCommand(path="myfile.lean")) response = server.run(FileCommand(path="myfile.lean", root_goals=True)) ``` +Extract Lean declarations while processing a file: + +```python +response = server.run(FileCommand(path="myfile.lean", declarations=True)) +for d in response.declarations: + print(d.full_name, d.signature.pp) +``` + ### ProofStep Work with proofs step by step using tactics: diff --git a/docs/api/interface.md b/docs/api/interface.md index 2dbca9c..c1d1356 100644 --- a/docs/api/interface.md +++ b/docs/api/interface.md @@ -4,6 +4,7 @@ heading: "Interface" show_symbol_type_heading: false members: + - CommandOptions - Command - FileCommand - ProofStep @@ -24,3 +25,13 @@ - CommandNode - TermNode - Syntax + - DocString + - DeclModifiers + - DeclSignature + - BinderView + - DeclBinders + - DeclType + - DeclValue + - OpenDecl + - ScopeInfo + - DeclarationInfo diff --git a/docs/api/server.md b/docs/api/server.md index 9bf9073..5f5894e 100644 --- a/docs/api/server.md +++ b/docs/api/server.md @@ -6,3 +6,15 @@ members: - LeanServer - AutoLeanServer + +--- + +## Notes on performance features + +LeanInteract automatically augments `Command` and `FileCommand` requests to speed up elaboration and processing of files: + +- Incremental elaboration is enabled by default +- Parallel elaboration is enabled via `set_option Elab.async true` by default when supported (Lean >= v4.19.0) + +You can disable these behaviors in `LeanREPLConfig` by setting +`enable_incremental_optimization=False` and/or `enable_parallel_elaboration=False`. diff --git a/docs/index.md b/docs/index.md index 4e7089f..66f9642 100644 --- a/docs/index.md +++ b/docs/index.md @@ -17,10 +17,12 @@ hide: - **πŸ”— Interactivity**: Execute Lean code and files directly from Python - **πŸš€ Ease of Use**: LeanInteract abstracts the complexities of Lean setup and interaction - **πŸ’» Cross-platform**: Works on Windows, macOS, and Linux operating systems -- **πŸ”§ Compatibility**: Supports all Lean versions between `v4.7.0-rc1` and `v4.24.0-rc1` +- **πŸ”§ Compatibility**: Supports all Lean versions between `v4.8.0-rc1` and `v4.24.0-rc1` - We backport the latest features of Lean REPL to older versions of Lean (see [fork](https://github.com/augustepoiroux/repl)). - **πŸ“¦ Temporary Projects**: Easily instantiate temporary Lean environments - Useful for experimenting with benchmarks depending on [Mathlib](https://github.com/leanprover-community/mathlib4) like [ProofNet#](https://huggingface.co/datasets/PAug/ProofNetSharp) and [MiniF2F](https://github.com/yangky11/miniF2F-lean4) +- **🧾 Data extraction**: Extract declarations and info trees for analysis and dataset building. +- **⚑ Incremental + Parallel elaboration**: Automatically reuse partial computations from previous commands, and enable `Elab.async` for faster processing. ## Quick Start diff --git a/docs/user-guide/basic-usage.md b/docs/user-guide/basic-usage.md index 87c09d6..b9cfb29 100644 --- a/docs/user-guide/basic-usage.md +++ b/docs/user-guide/basic-usage.md @@ -1,7 +1,3 @@ ---- -execute: true ---- - # Basic Usage This guide covers the fundamental operations and command types in LeanInteract. @@ -10,7 +6,7 @@ This guide covers the fundamental operations and command types in LeanInteract. The most common operation in LeanInteract is executing Lean code directly using the `Command` class: -```python tags=["execute"] +```python exec="on" source="above" session="base" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command # Setup @@ -18,24 +14,24 @@ config = LeanREPLConfig() server = LeanServer(config) # Run a simple theorem -server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := id")) +print(server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := id"))) ``` The response contains: -- An environment state (`env`) that can be used for subsequent commands - Messages returned by Lean if any (errors, information, etc.) +- An environment state (`env`) that can be used for subsequent commands. ### Working with Environment States Each command execution creates a new environment state. You can use this state in subsequent commands: -```python tags=["execute"] +```python exec="on" source="above" session="base" result="python" # First command creates environment state response1 = server.run(Command(cmd="def x := 5")) # Use environment state 0 for the next command -server.run(Command(cmd="#check x", env=response1.env)) +print(server.run(Command(cmd="#check x", env=response1.env))) ``` ## Processing Lean Files @@ -57,13 +53,16 @@ response = server.run(FileCommand(path="myfile.lean", root_goals=True)) Both `Command` and `FileCommand` support several options: - `all_tactics`: Get information about tactics used +- `declarations`: Extract fine-grained information about declarations in the code - `root_goals`: Get information about goals in theorems and definitions -- `infotree`: Get Lean infotree containing various informations about declarations and tactics +- `infotree`: Get Lean infotree containing various informations from the Lean syntax tree +- `incrementality`: Enable or disable incremental elaboration for this specific command. +- `set_options`: Set Lean options for this command (see [Set Options](set-options.md)) - `env`: The environment from a previous command to be used as context. If `env = None`, starts from scratch. Example with options: -```python tags=["execute"] +```python exec="on" source="above" session="base" result="python" response = server.run(Command( cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := by simp", all_tactics=True @@ -75,7 +74,7 @@ print(response.tactics) # Shows tactics used When Lean code contains `sorry` (incomplete proofs), LeanInteract returns information about these `sorry`: -```python tags=["execute"] +```python exec="on" source="above" session="base" result="python" response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := sorry")) print(response.sorries[0]) ``` @@ -88,7 +87,7 @@ This response will include a list of `Sorry` objects, each containing: ## Error Handling -```python tags=["execute"] +```python exec="on" source="above" session="base" result="python" from lean_interact.interface import LeanError try: diff --git a/docs/user-guide/custom-lean-configuration.md b/docs/user-guide/custom-lean-configuration.md index d9e4741..b9a5b90 100644 --- a/docs/user-guide/custom-lean-configuration.md +++ b/docs/user-guide/custom-lean-configuration.md @@ -10,7 +10,7 @@ You can specify which version of Lean 4 you want to use when no project is speci from lean_interact import LeanREPLConfig, LeanServer # Use a specific Lean version -config = LeanREPLConfig(lean_version="v4.7.0") +config = LeanREPLConfig(lean_version="v4.8.0") server = LeanServer(config) ``` @@ -81,12 +81,12 @@ from lean_interact import LeanREPLConfig, TempRequireProject, LeanRequire # Create a temporary project with Mathlib as a dependency project = TempRequireProject( - lean_version="v4.7.0", + lean_version="v4.8.0", require=[ LeanRequire( name="mathlib", git="https://github.com/leanprover-community/mathlib4.git", - rev="v4.7.0" + rev="v4.8.0" ) ] ) diff --git a/docs/user-guide/data-extraction.md b/docs/user-guide/data-extraction.md new file mode 100644 index 0000000..c3686ef --- /dev/null +++ b/docs/user-guide/data-extraction.md @@ -0,0 +1,71 @@ +# Data Extraction: Declarations, Tactics, and InfoTrees + +LeanInteract makes it easy to extract rich data from elaboration, including declarations, tactics, and detailed InfoTrees. + +## Declarations + +Set `declarations=True` to retrieve a list of `DeclarationInfo` for each declaration introduced in your Lean code. +Full details about the fields in `DeclarationInfo` can be found in the [API reference](../api/interface.md#lean_interact.interface.DeclarationInfo). + +```python exec="on" source="above" session="extraction" result="python" +from lean_interact import LeanServer, LeanREPLConfig, Command +from lean_interact.interface import CommandResponse + +code = """ +theorem ex (n : Nat) : n = 5 β†’ n = 5 := by + intro h; exact h +""" + +server = LeanServer(LeanREPLConfig()) +res = server.run(Command(cmd=code, declarations=True)) +assert isinstance(res, CommandResponse) +for d in res.declarations: + print(f"Full name: `{d.full_name}`") + print(f"Kind: `{d.kind}`") + print(f"Signature: `{d.signature}`") + print(f"Value: `{d.value}`") + print(f"Binders: `{d.binders}`") +``` + +For files: + +```python +from lean_interact import FileCommand +res = server.run(FileCommand(path="myfile.lean", declarations=True)) +``` + +Tip: See [`examples/extract_mathlib_decls.py`](https://github.com/augustepoiroux/LeanInteract/blob/main/examples/extract_mathlib_decls.py) for a scalable, per-file parallel extractor over Mathlib. + +## Tactics + +Use `all_tactics=True` to collect tactic applications with their goals and used constants. + +```python exec="on" source="above" session="extraction" result="python" +resp = server.run(Command(cmd=code, all_tactics=True)) +for t in resp.tactics: + print(t.tactic, "::: used:", t.used_constants) +``` + +## InfoTrees + +Request `infotree` to obtain structured elaboration information. Accepted values include `"full"`, `"tactics"`, `"original"`, and `"substantive"`. + +```python exec="on" source="above" session="extraction" result="python" +from lean_interact.interface import InfoTree + +res = server.run(Command(cmd=code, infotree="full")) +trees: list[InfoTree] = res.infotree or [] + +# Example: iterate over all command-level nodes and print their kind +for tree in trees: + for cmd_node in tree.commands(): + print(cmd_node.kind, cmd_node.node.stx) +``` + +## Root goals and messages + +You can also ask for `root_goals=True` to retrieve initial goals for declarations (even if already proved). + +```python exec="on" source="above" session="extraction" result="python" +print(server.run(Command(cmd=code, root_goals=True))) +``` diff --git a/docs/user-guide/examples.md b/docs/user-guide/examples.md index 53335d2..e22a38a 100644 --- a/docs/user-guide/examples.md +++ b/docs/user-guide/examples.md @@ -1,7 +1,3 @@ ---- -execute: true ---- - # Examples This page provides practical examples of using LeanInteract in different scenarios. You can find a few full example scripts in the [`examples`](https://github.com/augustepoiroux/LeanInteract/tree/main/examples) directory of the repository. @@ -10,7 +6,7 @@ This page provides practical examples of using LeanInteract in different scenari This example demonstrates how to define a simple theorem with a partial proof in Lean using LeanInteract: -```python tags=["execute"] +```python exec="on" source="above" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command # Initialize configuration and server @@ -18,19 +14,19 @@ config = LeanREPLConfig() server = LeanServer(config) # Define a simple theorem -server.run(Command(cmd=""" +print(server.run(Command(cmd=""" theorem add_comm (a b : Nat) : a + b = b + a := by induction a with | zero => simp | succ a ih => sorry -""")) +"""))) ``` ## Working with Mathlib This example shows how to use Mathlib to work with more advanced mathematical concepts: -```python +```python exec="on" source="above" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command, TempRequireProject # Create configuration with Mathlib @@ -38,7 +34,7 @@ config = LeanREPLConfig(project=TempRequireProject(lean_version="v4.19.0", requi server = LeanServer(config) # Define a theorem using Mathlib's real numbers -server.run(Command(cmd=""" +print(server.run(Command(cmd=""" import Mathlib theorem irrational_plus_rational @@ -46,14 +42,14 @@ theorem irrational_plus_rational intro h simp assumption -""")) +"""))) ``` ## Using Custom REPL Versions This example demonstrates how to use a specific REPL version from a custom repository: -```python +```python exec="on" source="above" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command # Use a specific REPL version from the official Lean repository diff --git a/docs/user-guide/getting-started.md b/docs/user-guide/getting-started.md index e7ca587..04be669 100644 --- a/docs/user-guide/getting-started.md +++ b/docs/user-guide/getting-started.md @@ -1,7 +1,3 @@ ---- -execute: true ---- - # Getting Started with LeanInteract ## Overview @@ -14,7 +10,7 @@ LeanInteract provides a Python interface to the Lean 4 theorem prover via the Le ## Quick Example -```python tags=["execute"] +```python exec="on" source="above" session="getting-started" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command # Create a Lean REPL configuration diff --git a/docs/user-guide/installation.md b/docs/user-guide/installation.md index 95a3d7c..4b61849 100644 --- a/docs/user-guide/installation.md +++ b/docs/user-guide/installation.md @@ -1,7 +1,3 @@ ---- -execute: true ---- - # Installation ## Prerequisites @@ -20,7 +16,7 @@ We recommend using Linux or macOS for the best experience, but LeanInteract also You can install LeanInteract directly from PyPI: -``` +```bash pip install lean-interact ``` @@ -28,7 +24,7 @@ pip install lean-interact LeanInteract provides a convenient command to install Lean 4 along with its official [Elan](https://github.com/leanprover/elan) version manager: -``` +```bash install-lean ``` @@ -41,7 +37,7 @@ This command will install Elan, which manages Lean versions. You can verify that LeanInteract is properly installed by running a simple Python script: -```python tags=["execute"] +```python exec="on" source="above" session="install" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command # Create a configuration @@ -66,7 +62,7 @@ If everything is set up correctly, the script should output a successful respons On Windows, you might encounter path length limitations. If you get an error related to path length, you can enable long paths in Windows 10 and later versions by running the following command in an administrator PowerShell: -``` +```powershell New-ItemProperty -Path "HKLM:\SYSTEM\CurrentControlSet\Control\FileSystem" -Name LongPathsEnabled -Value 1 -PropertyType DWord -Force git config --system core.longpaths true ``` @@ -81,12 +77,12 @@ If you're using LeanInteract in a Docker container, make sure to include Git in If you need to clear the LeanInteract cache (for troubleshooting or disk space reasons), you can use: -``` +```bash clear-lean-cache ``` To completely uninstall: -``` +```bash pip uninstall lean-interact ``` diff --git a/docs/user-guide/multi-processing.md b/docs/user-guide/multi-processing.md deleted file mode 100644 index b65e346..0000000 --- a/docs/user-guide/multi-processing.md +++ /dev/null @@ -1,164 +0,0 @@ ---- -execute: false ---- - -# Multi-processing Guide - -LeanInteract is designed with multi-processing in mind, allowing you to leverage multiple CPU cores for parallel theorem proving and verification tasks. This guide covers the best practices, patterns, and potential pitfalls when using LeanInteract in multi-process environments. - -We recommend using `AutoLeanServer`. -It is specifically designed for multi-process environments with -automated restart on fatal Lean errors, timeouts, and when memory limits are reached. -On automated restarts, only commands run with `add_to_session_cache=True` (attribute of the `AutoLeanServer.run` method) will be preserved. - -`AutoLeanServer` is still experimental, any feedback or issues encountered while using it are welcome. - -## Best Practices Summary - -1. **Always pre-instantiate** `LeanREPLConfig` before multiprocessing -2. **One lean server per process** -3. **Use `AutoLeanServer`** -4. **Configure memory limits** to prevent system overload -5. **Set appropriate timeouts** for long-running operations -6. **Use session caching** to keep context between requests -7. **Consider using `maxtasksperchild`** to limit memory accumulation - -## Quick Start - -Here is a minimal example of using LeanInteract with multiple processes: - -```python -import multiprocessing as mp -from lean_interact import LeanREPLConfig, AutoLeanServer, Command - -def worker(config: LeanREPLConfig, task_id): - """Worker function that runs in each process""" - server = AutoLeanServer(config) - result = server.run(Command(cmd=f"#eval {task_id} * {task_id}")) - return f"Task {task_id}: {result.messages[0].data if hasattr(result, 'messages') else 'Error'}" - -if __name__ == "__main__": - # Pre-instantiate config before multiprocessing - # LeanREPLConfig downloads and initializes resources - config = LeanREPLConfig(verbose=True) - - # Create processes - ctx = mp.get_context("spawn") - with ctx.Pool(processes=4) as pool: - tasks = range(5) - results = pool.starmap(worker, [(config, task_id) for task_id in tasks]) - - for result in results: - print(result) -``` - -For more examples, check the [examples directory](https://github.com/augustepoiroux/LeanInteract/tree/main/examples). - -## Core Principles - -### 1. Pre-instantiate Configuration - -Always create your `LeanREPLConfig` instance **before** starting multiprocessing: - -```python -from lean_interact import LeanREPLConfig, AutoLeanServer -import multiprocessing as mp - -# βœ… CORRECT: Config created in main process -def correct_approach(): - config = LeanREPLConfig() # Pre-setup in main process - - def worker(cfg): - server = AutoLeanServer(cfg) # Use pre-configured config - # ... your work here - pass - - ctx = mp.get_context("spawn") - with ctx.Pool() as pool: - pool.map(worker, [config] * 4) - -# ❌ INCORRECT: Config created in each process -def incorrect_approach(): - def worker(): - config = LeanREPLConfig() - server = AutoLeanServer(config) - # ... your work here - pass - - ctx = mp.get_context("spawn") - with ctx.Pool() as pool: - pool.map(worker, range(4)) -``` - -### 2. One Server Per Process - -Each process should have its own `LeanServer` or `AutoLeanServer` instance. - -```python -def worker(config, task_data): - # Each process gets its own server - server = AutoLeanServer(config) - - # Process your tasks - for task in task_data: - result = server.run(task) - # Handle result - - return results -``` - -## Thread Safety - -### Within a Single Process - -`LeanServer` and `AutoLeanServer` are thread-safe within a single process thanks to internal locking mechanisms. -All concurrent requests will be processed sequentially. - -### Across Processes - -Servers are **NOT** safe to share across processes. Each process must have its own server instance: - -```python -import multiprocessing as mp -from lean_interact import AutoLeanServer, LeanREPLConfig - -# βœ… CORRECT: Each process creates its own server -def correct_multiprocess_worker(config: LeanREPLConfig, worker_id: int): - server = AutoLeanServer(config) # New server per process - # ... work with server - -# ❌ INCORRECT: Don't share servers across processes -def incorrect_multiprocess_pattern(): - config = LeanREPLConfig() - server = AutoLeanServer(config) - - def worker(worker_id): - # This will cause issues - server can't be pickled/shared - result = server.run(Command(cmd="...")) - - with mp.Pool() as pool: - pool.map(worker, range(4)) # Will fail! -``` - -## Memory Management - -```python -from lean_interact import AutoLeanServer, LeanREPLConfig - -# Configure memory limits for multi-process safety -config = LeanREPLConfig(memory_hard_limit_mb=8192) # 8GB per server, works on Linux only - -server = AutoLeanServer( - config, - max_total_memory=0.8, # Restart when system uses >80% memory - max_process_memory=0.8, # Restart when process uses >80% of limit - max_restart_attempts=5 # Allow up to 5 restart attempts per command -) -``` - -### Memory Configuration Options - -- `max_total_memory`: System-wide memory threshold (0.0-1.0) -- `max_process_memory`: Per-process memory threshold (0.0-1.0) -- `memory_hard_limit_mb`: Hard memory limit in MB (Linux only) -- `max_restart_attempts`: Maximum consecutive restart attempts diff --git a/docs/user-guide/performance.md b/docs/user-guide/performance.md new file mode 100644 index 0000000..8f1471b --- /dev/null +++ b/docs/user-guide/performance.md @@ -0,0 +1,199 @@ +# Performance & Multi-processing + +LeanInteract implements two complementary mechanisms for faster feedback by default: + +- Incremental elaboration: reuse partial computations across commands/files +- Parallel elaboration: enable `Elab.async` to elaborate independent parts in parallel + +## Incremental elaboration + +Incremental elaboration reduces latency and memory by automatically reusing elaboration results from prior commands executed on the same `LeanServer`. +You can disable it if needed by setting `enable_incremental_optimization=False` in `LeanREPLConfig`. + +### Example + +Below is a small script that measures the elapsed time of a first "heavier" command and a second dependent command that benefits from incremental reuse: + +```python exec="on" source="above" session="perf" result="python" +import time +from lean_interact import LeanREPLConfig, LeanServer, Command + +server = LeanServer(LeanREPLConfig()) + +t1 = time.perf_counter() +print(server.run(Command(cmd=""" +def fib : Nat β†’ Nat + | 0 => 0 + | 1 => 1 + | n + 2 => fib (n + 1) + fib n +#eval fib 35 + +theorem foo : n = n := by rfl +#check foo +"""))) +print(f"First run: {time.perf_counter() - t1:.3f}s") + +t2 = time.perf_counter() +print(server.run(Command(cmd=""" +def fib : Nat β†’ Nat + | 0 => 0 + | 1 => 1 + | n + 2 => fib (n + 1) + fib n +#eval fib 35 + +theorem foo2 : n = n+0 := by rfl +#check foo2 +"""))) +print(f"Second run: {time.perf_counter() - t2:.3f}s") +``` + +!!! warning Imports are cached + Imports are cached in incremental mode, meaning that if the content of one of your imported file has changed, it will not be taken into account unless you restart the server. + +## Parallel elaboration (Elab.async) + +When supported (Lean >= v4.19.0), Lean can elaborate different parts of a command/file in parallel. LeanInteract auto-enables this by adding `set_option Elab.async true` to each request. +You can disable it if needed by setting `enable_parallel_elaboration=False` in `LeanREPLConfig`. + +!!! note + Only available for Lean >= v4.19.0 + +--- + +## Multi-processing Guide + +LeanInteract is designed with multi-processing in mind, allowing you to leverage multiple CPU cores for parallel theorem proving and verification tasks. + +We recommend using `AutoLeanServer`. It is specifically designed for multi-process environments with automated restart on fatal Lean errors, timeouts, and when memory limits are reached. On automated restarts, only commands run with `add_to_session_cache=True` (attribute of the `AutoLeanServer.run` method) will be preserved. + +`AutoLeanServer` is still experimental; feedback and issues are welcome. + +### Best Practices Summary + +1. **Always pre-instantiate** `LeanREPLConfig` before multiprocessing +2. **One lean server per process** +3. **Use `AutoLeanServer`** +4. **Configure memory limits** to prevent system overload +5. **Set appropriate timeouts** for long-running operations +6. **Use session caching** to keep context between requests +7. **Consider using `maxtasksperchild`** to limit memory accumulation + +### Quick Start + +```python +from multiprocessing import Pool +from lean_interact import AutoLeanServer, Command, LeanREPLConfig +from lean_interact.interface import LeanError + +def worker(config: LeanREPLConfig, task_id: int): + """Worker function that runs in each process""" + server = AutoLeanServer(config) + result = server.run(Command(cmd=f"#eval {task_id} * {task_id}")) + return f"Task {task_id}: {result.messages[0].data if not isinstance(result, LeanError) else 'Error'}" + +# Pre-instantiate config before multiprocessing (downloads/initializes resources) +config = LeanREPLConfig(verbose=True) +with Pool() as p: + print(p.starmap(worker, [(config, i) for i in range(5)])) +``` + +For more examples, check the [examples directory](https://github.com/augustepoiroux/LeanInteract/tree/main/examples). + +### Core Principles + +#### 1. Pre-instantiate Configuration + +Always create your `LeanREPLConfig` instance **before** starting multiprocessing: + +```python +from lean_interact import LeanREPLConfig, AutoLeanServer +import multiprocessing as mp + +# βœ… CORRECT: Config created in main process +config = LeanREPLConfig() # Pre-setup in main process + +def worker(cfg): + server = AutoLeanServer(cfg) # Use pre-configured config + # ... your work here + pass + +ctx = mp.get_context("spawn") +with ctx.Pool() as pool: + pool.map(worker, [config] * 4) + +# ❌ INCORRECT: Config created in each process +def worker(): + config = LeanREPLConfig() + server = AutoLeanServer(config) + # ... your work here + pass + +ctx = mp.get_context("spawn") +with ctx.Pool() as pool: + pool.map(worker, range(4)) +``` + +#### 2. One Server Per Process + +Each process should have its own `LeanServer` or `AutoLeanServer` instance. + +```python +def worker(config, task_data): + # Each process gets its own server + server = AutoLeanServer(config) + + for task in task_data: + result = server.run(task) + # Handle result + + return results +``` + +### Thread Safety + +Within a single process, `LeanServer` and `AutoLeanServer` are thread-safe thanks to internal locking. All concurrent requests are processed sequentially. Across processes, servers are not shareable: each process must create its own instance. + +```python +import multiprocessing as mp +from lean_interact import AutoLeanServer, LeanREPLConfig + +# βœ… CORRECT: Each process creates its own server +def correct_multiprocess_worker(config: LeanREPLConfig, worker_id: int): + server = AutoLeanServer(config) # New server per process + # ... work with server + +# ❌ INCORRECT: Don't share servers across processes +def incorrect_multiprocess_pattern(): + config = LeanREPLConfig() + server = AutoLeanServer(config) + + def worker(worker_id): + # This will cause issues - server can't be pickled/shared + result = server.run(Command(cmd="...")) + + with mp.Pool() as pool: + pool.map(worker, range(4)) # Will fail! +``` + +### Memory Management + +```python +from lean_interact import AutoLeanServer, LeanREPLConfig + +# Configure memory limits for multi-process safety +config = LeanREPLConfig(memory_hard_limit_mb=8192) # 8GB per server, works on Linux only + +server = AutoLeanServer( + config, + max_total_memory=0.8, # Restart when system uses >80% memory + max_process_memory=0.8, # Restart when process uses >80% of memory limit + max_restart_attempts=5 # Allow up to 5 restart attempts per command +) +``` + +#### Memory Configuration Options + +- `max_total_memory`: System-wide memory threshold (0.0-1.0) +- `max_process_memory`: Per-process memory threshold (0.0-1.0) +- `memory_hard_limit_mb`: Hard memory limit in MB (Linux only) +- `max_restart_attempts`: Maximum consecutive restart attempts diff --git a/docs/user-guide/set-options.md b/docs/user-guide/set-options.md new file mode 100644 index 0000000..4647788 --- /dev/null +++ b/docs/user-guide/set-options.md @@ -0,0 +1,26 @@ +# Set Lean Options from Python (`set_option`) + +You can pass Lean options per request using the `setOptions` field on `Command` and `FileCommand`. This mirrors Lean’s `set_option` commands and lets you customize elaboration or pretty-printing on a per-request basis. + +## Shape + +- `setOptions` is a list of pairs `(Name, DataValue)` +- `Name` is a list of components, e.g. `["pp", "unicode"]` +- `DataValue` can be `bool | int | str | Name` + +Example: + +```python exec="on" source="above" session="options" result="python" +from lean_interact import Command, LeanServer, LeanREPLConfig + +server = LeanServer(LeanREPLConfig()) +print(server.run(Command( + cmd="variable (n : Nat)\n#check n+0=n", + setOptions=[(["pp", "raw"], True)], +))) +``` + +LeanInteract will also merge your `setOptions` with its own defaults when enabled (e.g., it may add `(["Elab","async"], True)` to enable parallel elaboration). Your explicitly provided options are appended and forwarded with the request. + +!!! note + Options apply only to the single request you send; pass them again for subsequent calls diff --git a/docs/user-guide/tactic-mode.md b/docs/user-guide/tactic-mode.md index 3cc7881..28c116f 100644 --- a/docs/user-guide/tactic-mode.md +++ b/docs/user-guide/tactic-mode.md @@ -1,7 +1,3 @@ ---- -execute: true ---- - # Tactic Mode Tactic mode in LeanInteract allows you to work with Lean's proof tactics step-by-step, providing an interactive way to develop and explore proofs. @@ -20,12 +16,10 @@ Using tactics in LeanInteract involves two main steps: First, let's create a proof state by defining a theorem with `sorry`: -```python tags=["execute"] +```python exec="on" source="above" session="tactic" result="python" from lean_interact import LeanREPLConfig, LeanServer, Command -# Setup -config = LeanREPLConfig() -server = LeanServer(config) +server = LeanServer(LeanREPLConfig()) # Define a theorem with sorry response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := by sorry")) @@ -41,19 +35,15 @@ This response contains a `Sorry` object that includes: Once you have a proof state, you can apply tactics using the `ProofStep` class: -```python tags=["execute"] -from lean_interact import LeanREPLConfig, LeanServer, Command, ProofStep - -# Setup -config = LeanREPLConfig() -server = LeanServer(config) +```python exec="on" source="above" session="tactic" result="python" +from lean_interact import ProofStep # Define a theorem with sorry theorem_response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := sorry")) proof_state_id = theorem_response.sorries[0].proof_state # Apply a single tactic (intro) to the proof state -server.run(ProofStep(tactic="intro h", proof_state=proof_state_id)) +print(server.run(ProofStep(tactic="intro h", proof_state=proof_state_id))) ``` The response contains: @@ -66,12 +56,8 @@ The response contains: You can chain multiple tactics by using the proof state from each response: -```python tags=["execute"] -from lean_interact import LeanREPLConfig, LeanServer, Command, ProofStep - -# Setup -config = LeanREPLConfig() -server = LeanServer(config) +```python exec="on" source="above" session="tactic" result="python" +from lean_interact import ProofStep # Define a theorem with sorry theorem_response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := sorry")) @@ -81,24 +67,14 @@ proof_state_id = theorem_response.sorries[0].proof_state intro_response = server.run(ProofStep(tactic="intro h", proof_state=proof_state_id)) # Apply 'exact' tactic to the resulting proof state -server.run(ProofStep(tactic="exact h", proof_state=intro_response.proof_state)) +print(server.run(ProofStep(tactic="exact h", proof_state=intro_response.proof_state))) ``` ### Applying Multiple Tactics at Once You can also apply multiple tactics at once by wrapping them in parentheses: -```python tags=["execute"] -from lean_interact import LeanREPLConfig, LeanServer, Command, ProofStep - -# Setup -config = LeanREPLConfig() -server = LeanServer(config) - -# Define a theorem with sorry -theorem_response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 β†’ n = 5 := sorry")) -proof_state_id = theorem_response.sorries[0].proof_state - +```python exec="on" source="above" session="tactic" result="python" # Apply multiple tactics at once multi_response = server.run(ProofStep(tactic="""( intro h @@ -112,13 +88,7 @@ print(multi_response) The `ProofStepResponse` contains a `proof_status` field that indicates whether the proof is complete. Here's a complete example of working with tactics: -```python tags=["execute"] -from lean_interact import LeanREPLConfig, LeanServer, Command, ProofStep - -# Setup -config = LeanREPLConfig() -server = LeanServer(config) - +```python exec="on" source="above" session="tactic" result="python" # Create a theorem with sorry theorem_response = server.run(Command(cmd="theorem my_theorem (x : Nat) : x = x := sorry")) print("Initial goal:", theorem_response.sorries[0].goal) diff --git a/examples/extract_mathlib_decls.py b/examples/extract_mathlib_decls.py new file mode 100644 index 0000000..0cd9e17 --- /dev/null +++ b/examples/extract_mathlib_decls.py @@ -0,0 +1,92 @@ +"""Clone mathlib4 and extract all Lean declarations in parallel (per-file tasks). + +Output: mathlib_declarations.jsonl (JSONL, one declaration per line). + Can be parsed back using `DeclarationInfo.model_validate_json()` from `lean_interact.interface`. +""" + +import json +import multiprocessing as mp +import os +from concurrent.futures import ProcessPoolExecutor, as_completed +from pathlib import Path + +from tqdm import tqdm + +from lean_interact import LeanREPLConfig +from lean_interact.project import GitProject + +MATHLIB_GIT = "https://github.com/leanprover-community/mathlib4.git" +MATHLIB_REV = "v4.24.0-rc1" # or use a commit hash, branch name, etc. +NUM_PROCS = max((os.cpu_count() or 2) - 1, 1) # Override with env var NUM_PROCS if desired + + +def find_lean_files(root: Path) -> list[Path]: + excluded = {".git", ".lake", "build", "lake-packages"} + return [p for p in root.rglob("*.lean") if p.name != "lakefile.lean" and not (set(p.parts) & excluded)] + + +def process_file(rel_path: str, config: LeanREPLConfig) -> list[dict]: + """Extract declarations from a single .lean file (relative to project).""" + from lean_interact.interface import CommandResponse, FileCommand, LeanError + from lean_interact.server import LeanServer + + server = LeanServer(config) + out: list[dict] = [] + try: + res = server.run(FileCommand(path=rel_path, declarations=True)) + if isinstance(res, LeanError): + return out + assert isinstance(res, CommandResponse) + for d in res.declarations: + out.append({"file": rel_path, "decl": d.model_dump_json()}) + except Exception: + # Skip files that fail to elaborate for any reason + return out + return out + + +def main() -> None: + # Create the GitProject for mathlib (auto-builds) + project = GitProject(url=MATHLIB_GIT, rev=MATHLIB_REV) + config = LeanREPLConfig(project=project, verbose=True) + project_dir = Path(project.get_directory()) + mathlib_root = project_dir / "Mathlib" + search_root = mathlib_root if mathlib_root.exists() else project_dir + + print(f"Scanning Lean files under: {search_root}") + files = find_lean_files(search_root) + rel_paths = [str(p.relative_to(project_dir)) for p in files] + print(f"Discovered {len(rel_paths)} .lean files") + + if not rel_paths: + print("No .lean files found; exiting.") + return + + num_jobs = max(1, int(os.environ.get("NUM_PROCS", NUM_PROCS))) + print(f"Starting {num_jobs} workers over {len(rel_paths)} files…") + + # Simple tqdm progress that updates as each file finishes + results: list[list[dict]] = [] + with tqdm(total=len(rel_paths), desc="Processing files", unit="file") as pbar: + with ProcessPoolExecutor(max_workers=num_jobs, mp_context=mp.get_context("spawn")) as executor: + futures = [executor.submit(process_file, rp, config) for rp in rel_paths] + for fut in as_completed(futures): + try: + results.append(fut.result()) + finally: + pbar.update(1) + + # Write output + out_path = Path.cwd() / "mathlib_declarations.jsonl" + total = 0 + with out_path.open("w", encoding="utf-8") as f: + for lst in results: + total += len(lst) + for rec in lst: + f.write(json.dumps(rec, ensure_ascii=False) + "\n") + + print(f"Wrote {total} declarations to {out_path}") + + +if __name__ == "__main__": + main() diff --git a/mkdocs.yml b/mkdocs.yml index 64a5779..92cc76c 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -83,6 +83,7 @@ plugins: version_selector: true css_dir: css javascript_dir: js + - markdown-exec - mkdocstrings: handlers: python: @@ -104,16 +105,6 @@ plugins: show_overloads: false unwrap_annotated: true signature_crossrefs: true - - execute: - execute_without_tag: [] # Don't execute any files by default - include: - - "*.md" - exclude: [] - tags: - execute: "execute" - hide_cell: "hide-cell" - hide_input: "hide-input" - hide_output: "hide-output" markdown_extensions: - pymdownx.highlight: @@ -143,7 +134,9 @@ nav: - Getting Started: user-guide/getting-started.md - Basic Usage: user-guide/basic-usage.md - Tactic Mode: user-guide/tactic-mode.md - - Multi-processing: user-guide/multi-processing.md + - Performance & Multi-processing: user-guide/performance.md + - Data Extraction: user-guide/data-extraction.md + - Set Lean Options: user-guide/set-options.md - Examples: user-guide/examples.md - Custom Lean Configuration: user-guide/custom-lean-configuration.md - Troubleshooting: user-guide/troubleshooting.md diff --git a/pyproject.toml b/pyproject.toml index 9912f15..e12df11 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "lean-interact" -version = "0.8.3" +version = "0.9.0" description = "LeanInteract is a Python package that allows you to interact with the Lean theorem prover." keywords = ["Lean", "theorem proving", "autoformalization", "REPL"] license = { file = "LICENSE" } @@ -30,7 +30,7 @@ dev = [ "mkdocstrings-python>=1.16.10", "pymdown-extensions>=10.15", "ruff>=0.11.10", - "mkdocs-execute-plugin>=0.0.8", + "markdown-exec[ansi]>=1.9.3", "mike>=2.1.3", "mdformat>=0.7.22", "mdformat-mkdocs>=4.3.0" @@ -39,3 +39,9 @@ dev = [ [project.scripts] install-lean = "lean_interact.utils:install_lean" clear-lean-cache = "lean_interact.utils:clear_cache" + +[tool.hatch.build.targets.wheel] +packages = ["src/lean_interact"] + +[tool.hatch.build.targets.wheel.force-include] +"src/lean_interact/py.typed" = "lean_interact/py.typed" diff --git a/src/lean_interact/config.py b/src/lean_interact/config.py index bea1156..d2b74a5 100644 --- a/src/lean_interact/config.py +++ b/src/lean_interact/config.py @@ -40,6 +40,8 @@ def __init__( build_repl: bool = True, lake_path: str | PathLike = "lake", memory_hard_limit_mb: int | None = None, + enable_incremental_optimization: bool = True, + enable_parallel_elaboration: bool = True, verbose: bool = False, ): """ @@ -82,6 +84,13 @@ def __init__( The maximum memory usage in MB for the Lean server. Setting this value too low may lead to more command processing failures. Only available on Linux platforms. Default is `None`, which means no limit. + enable_incremental_optimization: + Whether to enable incremental optimization for all commands in the Lean REPL. This can significantly speed up processing + and decrease memory usage of commands by automatically reusing partial computations from previous commands. + Only available for Lean >= v4.8.0-rc1. Default is `True`. + enable_parallel_elaboration: + Whether to enable parallel elaboration in the Lean REPL. This can significantly speed up processing + of commands, especially in large files. Only available for Lean >= v4.19.0. Default is `True`. verbose: Whether to print additional information during the setup process. @@ -128,6 +137,8 @@ def __init__( self.local_repl_path = Path(local_repl_path) if local_repl_path else None self.build_repl = build_repl self.memory_hard_limit_mb = memory_hard_limit_mb + self.enable_incremental_optimization = enable_incremental_optimization + self.enable_parallel_elaboration = enable_parallel_elaboration self.lake_path = Path(lake_path) self.verbose = verbose self._timeout_lock = 300 diff --git a/src/lean_interact/interface.py b/src/lean_interact/interface.py index 6265e30..337ae37 100644 --- a/src/lean_interact/interface.py +++ b/src/lean_interact/interface.py @@ -35,18 +35,34 @@ class BaseREPLQuery(REPLBaseModel): """Base class for all Lean requests.""" +Name = list[str] + +DataValue = bool | int | str | Name + +Options = list[tuple[Name, DataValue]] + + class CommandOptions(REPLBaseModel): """Common options for `Command` and `FileCommand`.""" all_tactics: Annotated[bool | None, Field(alias="allTactics")] = None """If true, return all tactics used in the command with their associated information.""" + declarations: bool | None = None + """If true, return detailed information about declarations in the command.""" + root_goals: Annotated[bool | None, Field(alias="rootGoals")] = None """If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof.""" infotree: str | None = None """Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.""" + incrementality: bool | None = None + """If true, enable incremental optimization for the command.""" + + set_options: Annotated[Options | None, Field(alias="setOptions")] = None + """Options to be set before executing the command (i.e. `set_option` commands in Lean).""" + class Command(BaseREPLQuery, CommandOptions): """Command to be executed in the REPL.""" @@ -442,6 +458,80 @@ def theorem_for_sorry(self, sorry: Sorry) -> Self | None: return found +class DocString(REPLBaseModel): + content: str + range: Range + + +class DeclModifiers(REPLBaseModel): + doc_string: Annotated[DocString | None, Field(default=None, alias="docString")] + visibility: Literal["regular", "private", "protected", "public"] = "regular" + compute_kind: Annotated[Literal["regular", "meta", "noncomputable"], Field(default="regular", alias="computeKind")] + rec_kind: Annotated[Literal["default", "partial", "nonrec"], Field(default="default", alias="recKind")] + is_protected: Annotated[bool, Field(default=False, alias="isProtected")] + is_unsafe: Annotated[bool, Field(default=False, alias="isUnsafe")] + attributes: list[str] = Field(default_factory=list) + + +class DeclSignature(REPLBaseModel): + pp: str + constants: list[str] + range: Range + + +class BinderView(REPLBaseModel): + id: str + type: str + binderInfo: str + + +class DeclBinders(REPLBaseModel): + pp: str + groups: list[str] + map: list[BinderView] + range: Range + + +class DeclType(REPLBaseModel): + pp: str + constants: list[str] + range: Range + + +class DeclValue(REPLBaseModel): + pp: str + constants: list[str] + range: Range + + +class OpenDecl(REPLBaseModel): + simple: dict[str, str | list[str]] | None = None + rename: dict[str, str] | None = None + + +class ScopeInfo(REPLBaseModel): + var_decls: Annotated[list[str], Field(default_factory=list, alias="varDecls")] + include_vars: Annotated[list[str], Field(default_factory=list, alias="includeVars")] + omit_vars: Annotated[list[str], Field(default_factory=list, alias="omitVars")] + level_names: Annotated[list[str], Field(default_factory=list, alias="levelNames")] + curr_namespace: Annotated[str, Field(alias="currNamespace")] + open_decl: Annotated[list[OpenDecl], Field(default_factory=list, alias="openDecl")] + + +class DeclarationInfo(REPLBaseModel): + pp: str + range: Range + scope: ScopeInfo + name: str + full_name: Annotated[str, Field(alias="fullName")] + kind: str + modifiers: DeclModifiers + signature: DeclSignature + binders: DeclBinders | None = None + type: DeclType | None = None + value: DeclValue | None = None + + # Response @@ -501,6 +591,9 @@ class CommandResponse(BaseREPLResponse): tactics: list[Tactic] = Field(default_factory=list) """List of tactics in the code. Returned only if `all_tactics` is true.""" + declarations: list[DeclarationInfo] = Field(default_factory=list) + """List of declarations in the code. Returned only if `declarations` is true.""" + infotree: list[InfoTree] | None = None """The infotree of the code. Returned only if `infotree` is true.""" diff --git a/src/lean_interact/py.typed b/src/lean_interact/py.typed new file mode 100644 index 0000000..e69de29 diff --git a/src/lean_interact/server.py b/src/lean_interact/server.py index b1aae2f..b2a33e1 100644 --- a/src/lean_interact/server.py +++ b/src/lean_interact/server.py @@ -70,6 +70,7 @@ def lean_version(self) -> str | None: def start(self) -> None: """Start the Lean REPL server process. This is called automatically in the constructor.""" + self._proc = subprocess.Popen( [ str(self.config.lake_path), @@ -294,6 +295,16 @@ def run_dict(self, request: dict, verbose: bool = False, timeout: float | None = return self._parse_repl_output(raw_output, verbose) + def _augment_request(self, request: BaseREPLQuery) -> BaseREPLQuery: + if isinstance(request, (Command, FileCommand)): + if self.config.enable_incremental_optimization: + request = request.model_copy(update={"incrementality": True}) + if self.config.enable_parallel_elaboration: + set_options = list(request.set_options) if request.set_options is not None else [] + set_options.append((["Elab", "async"], True)) + request = request.model_copy(update={"set_options": set_options}) + return request + # Type hints for IDE and static analysis @overload def run( @@ -333,6 +344,7 @@ def run( Depending on the request type, the response will be one of the following: `CommandResponse`, `ProofStepResponse`, or `LeanError` """ + request = self._augment_request(request) request_dict = request.model_dump(exclude_none=True, by_alias=True) result_dict = self.run_dict(request=request_dict, verbose=verbose, timeout=timeout, **kwargs) @@ -572,6 +584,7 @@ def run( Depending on the request type, the response will be one of the following: `CommandResponse`, `ProofStepResponse`, or `LeanError` """ + request = self._augment_request(request) request_dict = request.model_dump(exclude_none=True, by_alias=True) result_dict = self._run_dict_backoff(request=request_dict, verbose=verbose, timeout=timeout) diff --git a/src/lean_interact/utils.py b/src/lean_interact/utils.py index ae13751..cadc50c 100644 --- a/src/lean_interact/utils.py +++ b/src/lean_interact/utils.py @@ -22,7 +22,7 @@ ROOT_DIR = Path(__file__).resolve().parent DEFAULT_CACHE_DIR = ROOT_DIR / "cache" DEFAULT_REPL_GIT_URL = "https://github.com/augustepoiroux/repl" -DEFAULT_REPL_VERSION = "v1.0.16" +DEFAULT_REPL_VERSION = "v1.3.4" os.makedirs(DEFAULT_CACHE_DIR, exist_ok=True) diff --git a/tests/test_server.py b/tests/test_server.py index a00b340..a195081 100644 --- a/tests/test_server.py +++ b/tests/test_server.py @@ -15,8 +15,15 @@ from lean_interact.config import LeanREPLConfig from lean_interact.interface import ( + BinderView, Command, CommandResponse, + DeclarationInfo, + DeclBinders, + DeclModifiers, + DeclSignature, + DeclType, + DeclValue, FileCommand, LeanError, Message, @@ -25,6 +32,8 @@ Pos, ProofStep, ProofStepResponse, + Range, + ScopeInfo, Sorry, UnpickleEnvironment, UnpickleProofState, @@ -43,7 +52,7 @@ class TestLeanServer(unittest.TestCase): maxDiff = None - oldestVersion = "v4.8.0-rc1" if platform.system() == "Windows" else "v4.7.0" + oldestVersion = "v4.8.0-rc1" @classmethod def setUpClass(cls): @@ -135,10 +144,10 @@ def test_init_with_project_dir(self): def test_init_with_official_repl(self): config = LeanREPLConfig( - repl_rev="v4.21.0-rc3", repl_git="https://github.com/leanprover-community/repl", verbose=True + repl_rev="v4.24.0-rc1", repl_git="https://github.com/leanprover-community/repl", verbose=True ) server = AutoLeanServer(config=config) - self.assertEqual(server.lean_version, "v4.21.0-rc3") + self.assertEqual(server.lean_version, "v4.24.0-rc1") response = server.run(Command(cmd="#eval Lean.versionString"), verbose=True) self.assertIsInstance(response, CommandResponse) self.assertEqual( @@ -149,7 +158,7 @@ def test_init_with_official_repl(self): start_pos=Pos(line=1, column=0), end_pos=Pos(line=1, column=5), severity="info", - data='"4.21.0-rc3"', + data='"4.24.0-rc1"', ) ], env=0, @@ -396,14 +405,16 @@ def test_process_request_memory_restart(self): @unittest.mock.patch("lean_interact.server.LeanServer.run_dict") def test_process_request_with_negative_env_id(self, mock_super): - server = AutoLeanServer(config=LeanREPLConfig(verbose=True)) + server = AutoLeanServer(config=LeanREPLConfig(verbose=True, enable_parallel_elaboration=False)) # Prepare restart_persistent_session_cache assert isinstance(server._session_cache, PickleSessionCache) server._session_cache._cache[-1] = PickleSessionState(-1, 10, False, "") with unittest.mock.patch.object(server, "_get_repl_state_id", return_value=10): mock_super.return_value = {"env": 10} result = server.run(Command(cmd="test", env=-1)) - mock_super.assert_called_with(request={"cmd": "test", "env": 10}, verbose=False, timeout=DEFAULT_TIMEOUT) + mock_super.assert_called_with( + request={"cmd": "test", "env": 10, "incrementality": True}, verbose=False, timeout=DEFAULT_TIMEOUT + ) self.assertEqual(result, CommandResponse(env=10)) @unittest.mock.patch("lean_interact.server.LeanServer.run_dict") @@ -544,6 +555,120 @@ def test_run_proof_equivalence(self): step2 = server.run(ProofStep(tactic="rfl", proof_state=step1.proof_state), verbose=True) self.assertEqual(step2, ProofStepResponse(proof_state=2, goals=[], proof_status="Completed")) + def test_declaration_info(self): + server = AutoLeanServer(config=LeanREPLConfig(verbose=True)) + result = server.run(Command(cmd="def x := 42", declarations=True), verbose=True) + self.assertEqual( + result, + CommandResponse( + declarations=[ + DeclarationInfo( + pp="def x := 42", + range=Range(synthetic=False, start=Pos(line=1, column=0), finish=Pos(line=1, column=11)), + scope=ScopeInfo( + var_decls=[], + include_vars=[], + omit_vars=[], + level_names=[], + curr_namespace="[anonymous]", + open_decl=[], + ), + name="x", + full_name="x", + kind="definition", + modifiers=DeclModifiers( + doc_string=None, + visibility="regular", + compute_kind="regular", + rec_kind="default", + is_protected=False, + is_unsafe=False, + attributes=[], + ), + signature=DeclSignature( + pp="", + constants=[], + range=Range(synthetic=True, start=Pos(line=1, column=0), finish=Pos(line=1, column=0)), + ), + binders=None, + type=None, + value=DeclValue( + pp=":= 42", + constants=[], + range=Range(synthetic=False, start=Pos(line=1, column=6), finish=Pos(line=1, column=11)), + ), + ) + ], + env=0, + ), + ) + + result = server.run( + Command(cmd="variable (p : Prop)\ntheorem test (h : p) : 0 = 0 := by rfl", declarations=True), verbose=True + ) + print(result) + self.assertEqual( + result, + CommandResponse( + messages=[ + Message( + end_pos=Pos(column=15, line=2), + severity="warning", + data="unused variable `h`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", + start_pos=Pos(column=14, line=2), + ) + ], + env=1, + declarations=[ + DeclarationInfo( + pp="theorem test (h : p) : 0 = 0 := by rfl", + type=DeclType( + pp="0 = 0", + range=Range(synthetic=False, finish=Pos(column=28, line=2), start=Pos(column=23, line=2)), + constants=[], + ), + full_name="test", + binders=DeclBinders( + pp="(h : p)", + groups=["(h : p)"], + map=[BinderView(id="h", type="p", binderInfo="default")], + range=Range(synthetic=False, finish=Pos(column=20, line=2), start=Pos(column=13, line=2)), + ), + kind="theorem", + range=Range(synthetic=False, finish=Pos(column=38, line=2), start=Pos(column=0, line=2)), + modifiers=DeclModifiers( + doc_string=None, + is_unsafe=False, + is_protected=False, + rec_kind="default", + attributes=[], + visibility="regular", + compute_kind="regular", + ), + signature=DeclSignature( + pp="(h : p) : 0 = 0", + range=Range(synthetic=False, finish=Pos(column=28, line=2), start=Pos(column=13, line=2)), + constants=["h", "p"], + ), + scope=ScopeInfo( + level_names=[], + open_decl=[], + curr_namespace="[anonymous]", + omit_vars=[], + var_decls=["variable (p : Prop)"], + include_vars=[], + ), + name="test", + value=DeclValue( + pp=":= by rfl", + range=Range(synthetic=False, finish=Pos(column=38, line=2), start=Pos(column=29, line=2)), + constants=[], + ), + ) + ], + ), + ) + def test_infotree(self): """Test infotree with all possible values""" server = AutoLeanServer(config=LeanREPLConfig(verbose=True)) @@ -605,13 +730,12 @@ def test_run_multiple_commands(self): if platform.system() != "Linux": self.skipTest("This test is only relevant on Linux") - # Test this issue: https://github.com/leanprover-community/repl/issues/77 + # Check that the following issue is now solved: https://github.com/leanprover-community/repl/issues/77 server = AutoLeanServer(config=LeanREPLConfig(memory_hard_limit_mb=4096, verbose=True)) - with self.assertRaises(ConnectionAbortedError): - for i in range(1000): - cmd = Command(cmd=f"theorem womp{i} (a{i} b c : Nat) : (a{i} + b) + c = c + a{i} + b := by sorry") - server.run(cmd) + for i in range(1000): + cmd = Command(cmd=f"theorem womp{i} (a{i} b c : Nat) : (a{i} + b) + c = c + a{i} + b := by sorry") + server.run(cmd) def test_run_lots_of_commands(self): # Test this issue: https://github.com/leanprover-community/repl/issues/77 diff --git a/uv.lock b/uv.lock index 9ea890a..3a40fae 100644 --- a/uv.lock +++ b/uv.lock @@ -28,15 +28,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/25/8a/c46dcc25341b5bce5472c718902eb3d38600a903b14fa6aeecef3f21a46f/asttokens-3.0.0-py3-none-any.whl", hash = "sha256:e3078351a059199dd5138cb1c706e6430c05eff2ff136af5eb4790f9d28932e2", size = 26918 }, ] -[[package]] -name = "attrs" -version = "25.3.0" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/5a/b0/1367933a8532ee6ff8d63537de4f1177af4bff9f3e829baf7331f595bb24/attrs-25.3.0.tar.gz", hash = "sha256:75d7cefc7fb576747b2c81b4442d4d4a1ce0900973527c011d1030fd3bf4af1b", size = 812032 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/77/06/bb80f5f86020c4551da315d78b3ab75e8228f89f0162f2c3a819e407941a/attrs-25.3.0-py3-none-any.whl", hash = "sha256:427318ce031701fea540783410126f03899a97ffc6f61596ad581ac2e40e3bc3", size = 63815 }, -] - [[package]] name = "babel" version = "2.17.0" @@ -59,36 +50,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/0c/37/fb6973edeb700f6e3d6ff222400602ab1830446c25c7b4676d8de93e65b8/backrefs-5.8-py39-none-any.whl", hash = "sha256:a66851e4533fb5b371aa0628e1fee1af05135616b86140c9d787a2ffdf4b8fdc", size = 380336 }, ] -[[package]] -name = "beautifulsoup4" -version = "4.13.4" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "soupsieve" }, - { name = "typing-extensions" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/d8/e4/0c4c39e18fd76d6a628d4dd8da40543d136ce2d1752bd6eeeab0791f4d6b/beautifulsoup4-4.13.4.tar.gz", hash = "sha256:dbb3c4e1ceae6aefebdaf2423247260cd062430a410e38c66f2baa50a8437195", size = 621067 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/50/cd/30110dc0ffcf3b131156077b90e9f60ed75711223f306da4db08eff8403b/beautifulsoup4-4.13.4-py3-none-any.whl", hash = "sha256:9bbbb14bfde9d79f38b8cd5f8c7c85f4b8f2523190ebed90e950a8dea4cb1c4b", size = 187285 }, -] - -[[package]] -name = "bleach" -version = "6.2.0" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "webencodings" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/76/9a/0e33f5054c54d349ea62c277191c020c2d6ef1d65ab2cb1993f91ec846d1/bleach-6.2.0.tar.gz", hash = "sha256:123e894118b8a599fd80d3ec1a6d4cc7ce4e5882b1317a7e1ba69b56e95f991f", size = 203083 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/fc/55/96142937f66150805c25c4d0f31ee4132fd33497753400734f9dfdcbdc66/bleach-6.2.0-py3-none-any.whl", hash = "sha256:117d9c6097a7c3d22fd578fcd8d35ff1e125df6736f554da4e432fdd63f31e5e", size = 163406 }, -] - -[package.optional-dependencies] -css = [ - { name = "tinycss2" }, -] - [[package]] name = "certifi" version = "2025.1.31" @@ -283,15 +244,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/d5/50/83c593b07763e1161326b3b8c6686f0f4b0f24d5526546bee538c89837d6/decorator-5.1.1-py3-none-any.whl", hash = "sha256:b8c3f85900b9dc423225913c5aace94729fe1fa9763b38939a95226f02d37186", size = 9073 }, ] -[[package]] -name = "defusedxml" -version = "0.7.1" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/0f/d5/c66da9b79e5bdb124974bfe172b4daf3c984ebd9c2a06e2b8a4dc7331c72/defusedxml-0.7.1.tar.gz", hash = "sha256:1bb3032db185915b62d7c6209c5a8792be6a32ab2fedacc84e01b52c51aa3e69", size = 75520 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/07/6c/aa3f2f849e01cb6a001cd8554a88d4c77c5c1a31c95bdf1cf9301e6d9ef4/defusedxml-0.7.1-py2.py3-none-any.whl", hash = "sha256:a352e7e428770286cc899e2542b6cdaedb2b4953ff269a210103ec58f6198a61", size = 25604 }, -] - [[package]] name = "exceptiongroup" version = "1.2.2" @@ -310,15 +262,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/7b/8f/c4d9bafc34ad7ad5d8dc16dd1347ee0e507a52c3adb6bfa8887e1c6a26ba/executing-2.2.0-py2.py3-none-any.whl", hash = "sha256:11387150cad388d62750327a53d3339fad4888b39a6fe233c3afbb54ecffd3aa", size = 26702 }, ] -[[package]] -name = "fastjsonschema" -version = "2.21.1" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/8b/50/4b769ce1ac4071a1ef6d86b1a3fb56cdc3a37615e8c5519e1af96cdac366/fastjsonschema-2.21.1.tar.gz", hash = "sha256:794d4f0a58f848961ba16af7b9c85a3e88cd360df008c59aac6fc5ae9323b5d4", size = 373939 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/90/2b/0817a2b257fe88725c25589d89aec060581aabf668707a8d03b2e9e0cb2a/fastjsonschema-2.21.1-py3-none-any.whl", hash = "sha256:c9e5b7e908310918cf494a434eeb31384dd84a98b57a30bcb1f535015b554667", size = 23924 }, -] - [[package]] name = "filelock" version = "3.18.0" @@ -476,33 +419,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/62/a1/3d680cbfd5f4b8f15abc1d571870c5fc3e594bb582bc3b64ea099db13e56/jinja2-3.1.6-py3-none-any.whl", hash = "sha256:85ece4451f492d0c13c5dd7c13a64681a86afae63a5f347908daf103ce6d2f67", size = 134899 }, ] -[[package]] -name = "jsonschema" -version = "4.23.0" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "attrs" }, - { name = "jsonschema-specifications" }, - { name = "referencing" }, - { name = "rpds-py" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/38/2e/03362ee4034a4c917f697890ccd4aec0800ccf9ded7f511971c75451deec/jsonschema-4.23.0.tar.gz", hash = "sha256:d71497fef26351a33265337fa77ffeb82423f3ea21283cd9467bb03999266bc4", size = 325778 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/69/4a/4f9dbeb84e8850557c02365a0eee0649abe5eb1d84af92a25731c6c0f922/jsonschema-4.23.0-py3-none-any.whl", hash = "sha256:fbadb6f8b144a8f8cf9f0b89ba94501d143e50411a1278633f56a7acf7fd5566", size = 88462 }, -] - -[[package]] -name = "jsonschema-specifications" -version = "2025.4.1" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "referencing" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/bf/ce/46fbd9c8119cfc3581ee5643ea49464d168028cfb5caff5fc0596d0cf914/jsonschema_specifications-2025.4.1.tar.gz", hash = "sha256:630159c9f4dbea161a6a2205c3011cc4f18ff381b189fff48bb39b9bf26ae608", size = 15513 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/01/0e/b27cdbaccf30b890c40ed1da9fd4a3593a5cf94dae54fb34f8a4b74fcd3f/jsonschema_specifications-2025.4.1-py3-none-any.whl", hash = "sha256:4653bffbd6584f7de83a67e0d620ef16900b390ddc7939d56684d6c81e33f1af", size = 18437 }, -] - [[package]] name = "jupyter-client" version = "8.6.3" @@ -533,35 +449,9 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/c9/fb/108ecd1fe961941959ad0ee4e12ee7b8b1477247f30b1fdfd83ceaf017f0/jupyter_core-5.7.2-py3-none-any.whl", hash = "sha256:4f7315d2f6b4bcf2e3e7cb6e46772eba760ae459cd1f59d29eb57b0a01bd7409", size = 28965 }, ] -[[package]] -name = "jupyterlab-pygments" -version = "0.3.0" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/90/51/9187be60d989df97f5f0aba133fa54e7300f17616e065d1ada7d7646b6d6/jupyterlab_pygments-0.3.0.tar.gz", hash = "sha256:721aca4d9029252b11cfa9d185e5b5af4d54772bb8072f9b7036f4170054d35d", size = 512900 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/b1/dd/ead9d8ea85bf202d90cc513b533f9c363121c7792674f78e0d8a854b63b4/jupyterlab_pygments-0.3.0-py3-none-any.whl", hash = "sha256:841a89020971da1d8693f1a99997aefc5dc424bb1b251fd6322462a1b8842780", size = 15884 }, -] - -[[package]] -name = "jupytext" -version = "1.17.1" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "markdown-it-py" }, - { name = "mdit-py-plugins" }, - { name = "nbformat" }, - { name = "packaging" }, - { name = "pyyaml" }, - { name = "tomli", marker = "python_full_version < '3.11'" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/6e/d9/b7acd3bed66c194cec1915c5bbec30994dbb50693ec209e5b115c28ddf63/jupytext-1.17.1.tar.gz", hash = "sha256:c02fda8af76ffd6e064a04cf2d3cc8aae242b2f0e38c42b4cd80baf89c3325d3", size = 3746897 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/12/b7/e7e3d34c8095c19228874b1babedfb5d901374e40d51ae66f2a90203be53/jupytext-1.17.1-py3-none-any.whl", hash = "sha256:99145b1e1fa96520c21ba157de7d354ffa4904724dcebdcd70b8413688a312de", size = 164286 }, -] - [[package]] name = "lean-interact" -version = "0.8.3" +version = "0.9.0" source = { editable = "." } dependencies = [ { name = "filelock" }, @@ -576,11 +466,11 @@ dependencies = [ [package.dev-dependencies] dev = [ { name = "ipykernel" }, + { name = "markdown-exec", extra = ["ansi"] }, { name = "mdformat" }, { name = "mdformat-mkdocs" }, { name = "mike" }, { name = "mkdocs" }, - { name = "mkdocs-execute-plugin" }, { name = "mkdocs-material" }, { name = "mkdocstrings" }, { name = "mkdocstrings-python" }, @@ -602,11 +492,11 @@ requires-dist = [ [package.metadata.requires-dev] dev = [ { name = "ipykernel", specifier = ">=6.29.5" }, + { name = "markdown-exec", extras = ["ansi"], specifier = ">=1.9.3" }, { name = "mdformat", specifier = ">=0.7.22" }, { name = "mdformat-mkdocs", specifier = ">=4.3.0" }, { name = "mike", specifier = ">=2.1.3" }, { name = "mkdocs", specifier = ">=1.6.1" }, - { name = "mkdocs-execute-plugin", specifier = ">=0.0.8" }, { name = "mkdocs-material", specifier = ">=9.6.14" }, { name = "mkdocstrings", specifier = ">=0.29.1" }, { name = "mkdocstrings-python", specifier = ">=1.16.10" }, @@ -623,6 +513,23 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/51/3f/afe76f8e2246ffbc867440cbcf90525264df0e658f8a5ca1f872b3f6192a/markdown-3.8-py3-none-any.whl", hash = "sha256:794a929b79c5af141ef5ab0f2f642d0f7b1872981250230e72682346f7cc90dc", size = 106210 }, ] +[[package]] +name = "markdown-exec" +version = "1.11.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "pymdown-extensions" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/e8/e4/ddd5ca350f2b072e51a22359cb51e94b5fdbe85810351e7484ccfd923324/markdown_exec-1.11.0.tar.gz", hash = "sha256:e0313a0dff715869a311d24853b3a7ecbbaa12e74eb0f3cf7d91401a7d8f0082", size = 81826 } +wheels = [ + { url = "https://files.pythonhosted.org/packages/22/41/5551f05c0e6430e3d2dcbd40965840a4cf280c045a529552690f04b7c0a0/markdown_exec-1.11.0-py3-none-any.whl", hash = "sha256:0526957984980f55c02b425d32e8ac8bb21090c109c7012ff905d3ddcc468ceb", size = 34747 }, +] + +[package.optional-dependencies] +ansi = [ + { name = "pygments-ansi-color" }, +] + [[package]] name = "markdown-it-py" version = "3.0.0" @@ -810,18 +717,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/fd/1a/31b7cd6e4e7a02df4e076162e9783620777592bea9e4bb036389389af99d/mike-2.1.3-py3-none-any.whl", hash = "sha256:d90c64077e84f06272437b464735130d380703a76a5738b152932884c60c062a", size = 33754 }, ] -[[package]] -name = "mistune" -version = "3.1.3" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "typing-extensions", marker = "python_full_version < '3.11'" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/c4/79/bda47f7dd7c3c55770478d6d02c9960c430b0cf1773b72366ff89126ea31/mistune-3.1.3.tar.gz", hash = "sha256:a7035c21782b2becb6be62f8f25d3df81ccb4d6fa477a6525b15af06539f02a0", size = 94347 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/01/4d/23c4e4f09da849e127e9f123241946c23c1e30f45a88366879e064211815/mistune-3.1.3-py3-none-any.whl", hash = "sha256:1a32314113cff28aa6432e99e522677c8587fd83e3d51c29b82a52409c842bd9", size = 53410 }, -] - [[package]] name = "mkdocs" version = "1.6.1" @@ -860,23 +755,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/87/dc/fc063b78f4b769d1956319351704e23ebeba1e9e1d6a41b4b602325fd7e4/mkdocs_autorefs-1.4.2-py3-none-any.whl", hash = "sha256:83d6d777b66ec3c372a1aad4ae0cf77c243ba5bcda5bf0c6b8a2c5e7a3d89f13", size = 24969 }, ] -[[package]] -name = "mkdocs-execute-plugin" -version = "0.0.8" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "ipykernel" }, - { name = "jupytext" }, - { name = "markdown" }, - { name = "mkdocs" }, - { name = "nbconvert" }, - { name = "traitlets" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/ef/fa/d3ff75edbb541ec1e7220e7f08bc22cda71c4c741f6142275cd0d305f27d/mkdocs_execute_plugin-0.0.8.tar.gz", hash = "sha256:892972c8295cddac8187fbe153b570a297cceb0c56145d6441a3457b600f055e", size = 6628 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/cc/4f/2b386e2efb0c65b9c7b2b52fc2b05c4312ab0705fba56ddb9f10a45657fb/mkdocs_execute_plugin-0.0.8-py3-none-any.whl", hash = "sha256:b401842d4057c8dc9464f16bc3d7ce8c94410fc9e25151fcc2381f2ac39f4d81", size = 9862 }, -] - [[package]] name = "mkdocs-get-deps" version = "0.2.0" @@ -963,61 +841,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/2b/9f/7ba6f94fc1e9ac3d2b853fdff3035fb2fa5afbed898c4a72b8a020610594/more_itertools-10.7.0-py3-none-any.whl", hash = "sha256:d43980384673cb07d2f7d2d918c616b30c659c089ee23953f601d6609c67510e", size = 65278 }, ] -[[package]] -name = "nbclient" -version = "0.10.2" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "jupyter-client" }, - { name = "jupyter-core" }, - { name = "nbformat" }, - { name = "traitlets" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/87/66/7ffd18d58eae90d5721f9f39212327695b749e23ad44b3881744eaf4d9e8/nbclient-0.10.2.tar.gz", hash = "sha256:90b7fc6b810630db87a6d0c2250b1f0ab4cf4d3c27a299b0cde78a4ed3fd9193", size = 62424 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/34/6d/e7fa07f03a4a7b221d94b4d586edb754a9b0dc3c9e2c93353e9fa4e0d117/nbclient-0.10.2-py3-none-any.whl", hash = "sha256:4ffee11e788b4a27fabeb7955547e4318a5298f34342a4bfd01f2e1faaeadc3d", size = 25434 }, -] - -[[package]] -name = "nbconvert" -version = "7.16.6" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "beautifulsoup4" }, - { name = "bleach", extra = ["css"] }, - { name = "defusedxml" }, - { name = "jinja2" }, - { name = "jupyter-core" }, - { name = "jupyterlab-pygments" }, - { name = "markupsafe" }, - { name = "mistune" }, - { name = "nbclient" }, - { name = "nbformat" }, - { name = "packaging" }, - { name = "pandocfilters" }, - { name = "pygments" }, - { name = "traitlets" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/a3/59/f28e15fc47ffb73af68a8d9b47367a8630d76e97ae85ad18271b9db96fdf/nbconvert-7.16.6.tar.gz", hash = "sha256:576a7e37c6480da7b8465eefa66c17844243816ce1ccc372633c6b71c3c0f582", size = 857715 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/cc/9a/cd673b2f773a12c992f41309ef81b99da1690426bd2f96957a7ade0d3ed7/nbconvert-7.16.6-py3-none-any.whl", hash = "sha256:1375a7b67e0c2883678c48e506dc320febb57685e5ee67faa51b18a90f3a712b", size = 258525 }, -] - -[[package]] -name = "nbformat" -version = "5.10.4" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "fastjsonschema" }, - { name = "jsonschema" }, - { name = "jupyter-core" }, - { name = "traitlets" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/6d/fd/91545e604bc3dad7dca9ed03284086039b294c6b3d75c0d2fa45f9e9caf3/nbformat-5.10.4.tar.gz", hash = "sha256:322168b14f937a5d11362988ecac2a4952d3d8e3a2cbeb2319584631226d5b3a", size = 142749 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/a9/82/0340caa499416c78e5d8f5f05947ae4bc3cba53c9f038ab6e9ed964e22f1/nbformat-5.10.4-py3-none-any.whl", hash = "sha256:3b48d6c8fbca4b299bf3982ea7db1af21580e4fec269ad087b9e81588891200b", size = 78454 }, -] - [[package]] name = "nest-asyncio" version = "1.6.0" @@ -1045,15 +868,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/90/96/04b8e52da071d28f5e21a805b19cb9390aa17a47462ac87f5e2696b9566d/paginate-0.5.7-py2.py3-none-any.whl", hash = "sha256:b885e2af73abcf01d9559fd5216b57ef722f8c42affbb63942377668e35c7591", size = 13746 }, ] -[[package]] -name = "pandocfilters" -version = "1.5.1" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/70/6f/3dd4940bbe001c06a65f88e36bad298bc7a0de5036115639926b0c5c0458/pandocfilters-1.5.1.tar.gz", hash = "sha256:002b4a555ee4ebc03f8b66307e287fa492e4a77b4ea14d3f934328297bb4939e", size = 8454 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/ef/af/4fbc8cab944db5d21b7e2a5b8e9211a03a79852b1157e2c102fcc61ac440/pandocfilters-1.5.1-py2.py3-none-any.whl", hash = "sha256:93be382804a9cdb0a7267585f157e5d1731bbe5545a85b268d6f5fe6232de2bc", size = 8663 }, -] - [[package]] name = "parso" version = "0.8.4" @@ -1258,6 +1072,18 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/8a/0b/9fcc47d19c48b59121088dd6da2488a49d5f72dacf8262e2790a1d2c7d15/pygments-2.19.1-py3-none-any.whl", hash = "sha256:9ea1544ad55cecf4b8242fab6dd35a93bbce657034b0611ee383099054ab6d8c", size = 1225293 }, ] +[[package]] +name = "pygments-ansi-color" +version = "0.3.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "pygments" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/50/f9/7f417aaee98a74b4f757f2b72971245181fcf25d824d2e7a190345669eaf/pygments-ansi-color-0.3.0.tar.gz", hash = "sha256:7018954cf5b11d1e734383a1bafab5af613213f246109417fee3f76da26d5431", size = 7317 } +wheels = [ + { url = "https://files.pythonhosted.org/packages/e6/17/8306a0bcd8c88d7761c2e73e831b0be026cd6873ce1f12beb3b4c9a03ffa/pygments_ansi_color-0.3.0-py3-none-any.whl", hash = "sha256:7eb063feaecadad9d4d1fd3474cbfeadf3486b64f760a8f2a00fc25392180aba", size = 10242 }, +] + [[package]] name = "pymdown-extensions" version = "10.15" @@ -1440,20 +1266,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/e3/fe/72e7e166bda3885810bee7b23049133e142f7c80c295bae02c562caeea16/pyzmq-26.2.1-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:bd8fdee945b877aa3bffc6a5a8816deb048dab0544f9df3731ecd0e54d8c84c9", size = 556563 }, ] -[[package]] -name = "referencing" -version = "0.36.2" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "attrs" }, - { name = "rpds-py" }, - { name = "typing-extensions", marker = "python_full_version < '3.13'" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/2f/db/98b5c277be99dd18bfd91dd04e1b759cad18d1a338188c936e92f921c7e2/referencing-0.36.2.tar.gz", hash = "sha256:df2e89862cd09deabbdba16944cc3f10feb6b3e6f18e902f7cc25609a34775aa", size = 74744 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/c1/b1/3baf80dc6d2b7bc27a95a67752d0208e410351e3feb4eb78de5f77454d8d/referencing-0.36.2-py3-none-any.whl", hash = "sha256:e8699adbbf8b5c7de96d8ffa0eb5c158b3beafce084968e2ea8bb08c6794dcd0", size = 26775 }, -] - [[package]] name = "requests" version = "2.32.3" @@ -1483,105 +1295,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/19/71/39c7c0d87f8d4e6c020a393182060eaefeeae6c01dab6a84ec346f2567df/rich-13.9.4-py3-none-any.whl", hash = "sha256:6049d5e6ec054bf2779ab3358186963bac2ea89175919d699e378b99738c2a90", size = 242424 }, ] -[[package]] -name = "rpds-py" -version = "0.25.1" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/8c/a6/60184b7fc00dd3ca80ac635dd5b8577d444c57e8e8742cecabfacb829921/rpds_py-0.25.1.tar.gz", hash = "sha256:8960b6dac09b62dac26e75d7e2c4a22efb835d827a7278c34f72b2b84fa160e3", size = 27304 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/cb/09/e1158988e50905b7f8306487a576b52d32aa9a87f79f7ab24ee8db8b6c05/rpds_py-0.25.1-cp310-cp310-macosx_10_12_x86_64.whl", hash = "sha256:f4ad628b5174d5315761b67f212774a32f5bad5e61396d38108bd801c0a8f5d9", size = 373140 }, - { url = "https://files.pythonhosted.org/packages/e0/4b/a284321fb3c45c02fc74187171504702b2934bfe16abab89713eedfe672e/rpds_py-0.25.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:8c742af695f7525e559c16f1562cf2323db0e3f0fbdcabdf6865b095256b2d40", size = 358860 }, - { url = "https://files.pythonhosted.org/packages/4e/46/8ac9811150c75edeae9fc6fa0e70376c19bc80f8e1f7716981433905912b/rpds_py-0.25.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:605ffe7769e24b1800b4d024d24034405d9404f0bc2f55b6db3362cd34145a6f", size = 386179 }, - { url = "https://files.pythonhosted.org/packages/f3/ec/87eb42d83e859bce91dcf763eb9f2ab117142a49c9c3d17285440edb5b69/rpds_py-0.25.1-cp310-cp310-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:ccc6f3ddef93243538be76f8e47045b4aad7a66a212cd3a0f23e34469473d36b", size = 400282 }, - { url = "https://files.pythonhosted.org/packages/68/c8/2a38e0707d7919c8c78e1d582ab15cf1255b380bcb086ca265b73ed6db23/rpds_py-0.25.1-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:f70316f760174ca04492b5ab01be631a8ae30cadab1d1081035136ba12738cfa", size = 521824 }, - { url = "https://files.pythonhosted.org/packages/5e/2c/6a92790243569784dde84d144bfd12bd45102f4a1c897d76375076d730ab/rpds_py-0.25.1-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:e1dafef8df605fdb46edcc0bf1573dea0d6d7b01ba87f85cd04dc855b2b4479e", size = 411644 }, - { url = "https://files.pythonhosted.org/packages/eb/76/66b523ffc84cf47db56efe13ae7cf368dee2bacdec9d89b9baca5e2e6301/rpds_py-0.25.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0701942049095741a8aeb298a31b203e735d1c61f4423511d2b1a41dcd8a16da", size = 386955 }, - { url = "https://files.pythonhosted.org/packages/b6/b9/a362d7522feaa24dc2b79847c6175daa1c642817f4a19dcd5c91d3e2c316/rpds_py-0.25.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:e87798852ae0b37c88babb7f7bbbb3e3fecc562a1c340195b44c7e24d403e380", size = 421039 }, - { url = "https://files.pythonhosted.org/packages/0f/c4/b5b6f70b4d719b6584716889fd3413102acf9729540ee76708d56a76fa97/rpds_py-0.25.1-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:3bcce0edc1488906c2d4c75c94c70a0417e83920dd4c88fec1078c94843a6ce9", size = 563290 }, - { url = "https://files.pythonhosted.org/packages/87/a3/2e6e816615c12a8f8662c9d8583a12eb54c52557521ef218cbe3095a8afa/rpds_py-0.25.1-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:e2f6a2347d3440ae789505693a02836383426249d5293541cd712e07e7aecf54", size = 592089 }, - { url = "https://files.pythonhosted.org/packages/c0/08/9b8e1050e36ce266135994e2c7ec06e1841f1c64da739daeb8afe9cb77a4/rpds_py-0.25.1-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:4fd52d3455a0aa997734f3835cbc4c9f32571345143960e7d7ebfe7b5fbfa3b2", size = 558400 }, - { url = "https://files.pythonhosted.org/packages/f2/df/b40b8215560b8584baccd839ff5c1056f3c57120d79ac41bd26df196da7e/rpds_py-0.25.1-cp310-cp310-win32.whl", hash = "sha256:3f0b1798cae2bbbc9b9db44ee068c556d4737911ad53a4e5093d09d04b3bbc24", size = 219741 }, - { url = "https://files.pythonhosted.org/packages/10/99/e4c58be18cf5d8b40b8acb4122bc895486230b08f978831b16a3916bd24d/rpds_py-0.25.1-cp310-cp310-win_amd64.whl", hash = "sha256:3ebd879ab996537fc510a2be58c59915b5dd63bccb06d1ef514fee787e05984a", size = 231553 }, - { url = "https://files.pythonhosted.org/packages/95/e1/df13fe3ddbbea43567e07437f097863b20c99318ae1f58a0fe389f763738/rpds_py-0.25.1-cp311-cp311-macosx_10_12_x86_64.whl", hash = "sha256:5f048bbf18b1f9120685c6d6bb70cc1a52c8cc11bdd04e643d28d3be0baf666d", size = 373341 }, - { url = "https://files.pythonhosted.org/packages/7a/58/deef4d30fcbcbfef3b6d82d17c64490d5c94585a2310544ce8e2d3024f83/rpds_py-0.25.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4fbb0dbba559959fcb5d0735a0f87cdbca9e95dac87982e9b95c0f8f7ad10255", size = 359111 }, - { url = "https://files.pythonhosted.org/packages/bb/7e/39f1f4431b03e96ebaf159e29a0f82a77259d8f38b2dd474721eb3a8ac9b/rpds_py-0.25.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d4ca54b9cf9d80b4016a67a0193ebe0bcf29f6b0a96f09db942087e294d3d4c2", size = 386112 }, - { url = "https://files.pythonhosted.org/packages/db/e7/847068a48d63aec2ae695a1646089620b3b03f8ccf9f02c122ebaf778f3c/rpds_py-0.25.1-cp311-cp311-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:1ee3e26eb83d39b886d2cb6e06ea701bba82ef30a0de044d34626ede51ec98b0", size = 400362 }, - { url = "https://files.pythonhosted.org/packages/3b/3d/9441d5db4343d0cee759a7ab4d67420a476cebb032081763de934719727b/rpds_py-0.25.1-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:89706d0683c73a26f76a5315d893c051324d771196ae8b13e6ffa1ffaf5e574f", size = 522214 }, - { url = "https://files.pythonhosted.org/packages/a2/ec/2cc5b30d95f9f1a432c79c7a2f65d85e52812a8f6cbf8768724571710786/rpds_py-0.25.1-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:c2013ee878c76269c7b557a9a9c042335d732e89d482606990b70a839635feb7", size = 411491 }, - { url = "https://files.pythonhosted.org/packages/dc/6c/44695c1f035077a017dd472b6a3253553780837af2fac9b6ac25f6a5cb4d/rpds_py-0.25.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:45e484db65e5380804afbec784522de84fa95e6bb92ef1bd3325d33d13efaebd", size = 386978 }, - { url = "https://files.pythonhosted.org/packages/b1/74/b4357090bb1096db5392157b4e7ed8bb2417dc7799200fcbaee633a032c9/rpds_py-0.25.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:48d64155d02127c249695abb87d39f0faf410733428d499867606be138161d65", size = 420662 }, - { url = "https://files.pythonhosted.org/packages/26/dd/8cadbebf47b96e59dfe8b35868e5c38a42272699324e95ed522da09d3a40/rpds_py-0.25.1-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:048893e902132fd6548a2e661fb38bf4896a89eea95ac5816cf443524a85556f", size = 563385 }, - { url = "https://files.pythonhosted.org/packages/c3/ea/92960bb7f0e7a57a5ab233662f12152085c7dc0d5468534c65991a3d48c9/rpds_py-0.25.1-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:0317177b1e8691ab5879f4f33f4b6dc55ad3b344399e23df2e499de7b10a548d", size = 592047 }, - { url = "https://files.pythonhosted.org/packages/61/ad/71aabc93df0d05dabcb4b0c749277881f8e74548582d96aa1bf24379493a/rpds_py-0.25.1-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:bffcf57826d77a4151962bf1701374e0fc87f536e56ec46f1abdd6a903354042", size = 557863 }, - { url = "https://files.pythonhosted.org/packages/93/0f/89df0067c41f122b90b76f3660028a466eb287cbe38efec3ea70e637ca78/rpds_py-0.25.1-cp311-cp311-win32.whl", hash = "sha256:cda776f1967cb304816173b30994faaf2fd5bcb37e73118a47964a02c348e1bc", size = 219627 }, - { url = "https://files.pythonhosted.org/packages/7c/8d/93b1a4c1baa903d0229374d9e7aa3466d751f1d65e268c52e6039c6e338e/rpds_py-0.25.1-cp311-cp311-win_amd64.whl", hash = "sha256:dc3c1ff0abc91444cd20ec643d0f805df9a3661fcacf9c95000329f3ddf268a4", size = 231603 }, - { url = "https://files.pythonhosted.org/packages/cb/11/392605e5247bead2f23e6888e77229fbd714ac241ebbebb39a1e822c8815/rpds_py-0.25.1-cp311-cp311-win_arm64.whl", hash = "sha256:5a3ddb74b0985c4387719fc536faced33cadf2172769540c62e2a94b7b9be1c4", size = 223967 }, - { url = "https://files.pythonhosted.org/packages/7f/81/28ab0408391b1dc57393653b6a0cf2014cc282cc2909e4615e63e58262be/rpds_py-0.25.1-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:b5ffe453cde61f73fea9430223c81d29e2fbf412a6073951102146c84e19e34c", size = 364647 }, - { url = "https://files.pythonhosted.org/packages/2c/9a/7797f04cad0d5e56310e1238434f71fc6939d0bc517192a18bb99a72a95f/rpds_py-0.25.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:115874ae5e2fdcfc16b2aedc95b5eef4aebe91b28e7e21951eda8a5dc0d3461b", size = 350454 }, - { url = "https://files.pythonhosted.org/packages/69/3c/93d2ef941b04898011e5d6eaa56a1acf46a3b4c9f4b3ad1bbcbafa0bee1f/rpds_py-0.25.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a714bf6e5e81b0e570d01f56e0c89c6375101b8463999ead3a93a5d2a4af91fa", size = 389665 }, - { url = "https://files.pythonhosted.org/packages/c1/57/ad0e31e928751dde8903a11102559628d24173428a0f85e25e187defb2c1/rpds_py-0.25.1-cp312-cp312-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:35634369325906bcd01577da4c19e3b9541a15e99f31e91a02d010816b49bfda", size = 403873 }, - { url = "https://files.pythonhosted.org/packages/16/ad/c0c652fa9bba778b4f54980a02962748479dc09632e1fd34e5282cf2556c/rpds_py-0.25.1-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:d4cb2b3ddc16710548801c6fcc0cfcdeeff9dafbc983f77265877793f2660309", size = 525866 }, - { url = "https://files.pythonhosted.org/packages/2a/39/3e1839bc527e6fcf48d5fec4770070f872cdee6c6fbc9b259932f4e88a38/rpds_py-0.25.1-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:9ceca1cf097ed77e1a51f1dbc8d174d10cb5931c188a4505ff9f3e119dfe519b", size = 416886 }, - { url = "https://files.pythonhosted.org/packages/7a/95/dd6b91cd4560da41df9d7030a038298a67d24f8ca38e150562644c829c48/rpds_py-0.25.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2c2cd1a4b0c2b8c5e31ffff50d09f39906fe351389ba143c195566056c13a7ea", size = 390666 }, - { url = "https://files.pythonhosted.org/packages/64/48/1be88a820e7494ce0a15c2d390ccb7c52212370badabf128e6a7bb4cb802/rpds_py-0.25.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:1de336a4b164c9188cb23f3703adb74a7623ab32d20090d0e9bf499a2203ad65", size = 425109 }, - { url = "https://files.pythonhosted.org/packages/cf/07/3e2a17927ef6d7720b9949ec1b37d1e963b829ad0387f7af18d923d5cfa5/rpds_py-0.25.1-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:9fca84a15333e925dd59ce01da0ffe2ffe0d6e5d29a9eeba2148916d1824948c", size = 567244 }, - { url = "https://files.pythonhosted.org/packages/d2/e5/76cf010998deccc4f95305d827847e2eae9c568099c06b405cf96384762b/rpds_py-0.25.1-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:88ec04afe0c59fa64e2f6ea0dd9657e04fc83e38de90f6de201954b4d4eb59bd", size = 596023 }, - { url = "https://files.pythonhosted.org/packages/52/9a/df55efd84403736ba37a5a6377b70aad0fd1cb469a9109ee8a1e21299a1c/rpds_py-0.25.1-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:a8bd2f19e312ce3e1d2c635618e8a8d8132892bb746a7cf74780a489f0f6cdcb", size = 561634 }, - { url = "https://files.pythonhosted.org/packages/ab/aa/dc3620dd8db84454aaf9374bd318f1aa02578bba5e567f5bf6b79492aca4/rpds_py-0.25.1-cp312-cp312-win32.whl", hash = "sha256:e5e2f7280d8d0d3ef06f3ec1b4fd598d386cc6f0721e54f09109a8132182fbfe", size = 222713 }, - { url = "https://files.pythonhosted.org/packages/a3/7f/7cef485269a50ed5b4e9bae145f512d2a111ca638ae70cc101f661b4defd/rpds_py-0.25.1-cp312-cp312-win_amd64.whl", hash = "sha256:db58483f71c5db67d643857404da360dce3573031586034b7d59f245144cc192", size = 235280 }, - { url = "https://files.pythonhosted.org/packages/99/f2/c2d64f6564f32af913bf5f3f7ae41c7c263c5ae4c4e8f1a17af8af66cd46/rpds_py-0.25.1-cp312-cp312-win_arm64.whl", hash = "sha256:6d50841c425d16faf3206ddbba44c21aa3310a0cebc3c1cdfc3e3f4f9f6f5728", size = 225399 }, - { url = "https://files.pythonhosted.org/packages/2b/da/323848a2b62abe6a0fec16ebe199dc6889c5d0a332458da8985b2980dffe/rpds_py-0.25.1-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:659d87430a8c8c704d52d094f5ba6fa72ef13b4d385b7e542a08fc240cb4a559", size = 364498 }, - { url = "https://files.pythonhosted.org/packages/1f/b4/4d3820f731c80fd0cd823b3e95b9963fec681ae45ba35b5281a42382c67d/rpds_py-0.25.1-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:68f6f060f0bbdfb0245267da014d3a6da9be127fe3e8cc4a68c6f833f8a23bb1", size = 350083 }, - { url = "https://files.pythonhosted.org/packages/d5/b1/3a8ee1c9d480e8493619a437dec685d005f706b69253286f50f498cbdbcf/rpds_py-0.25.1-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:083a9513a33e0b92cf6e7a6366036c6bb43ea595332c1ab5c8ae329e4bcc0a9c", size = 389023 }, - { url = "https://files.pythonhosted.org/packages/3b/31/17293edcfc934dc62c3bf74a0cb449ecd549531f956b72287203e6880b87/rpds_py-0.25.1-cp313-cp313-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:816568614ecb22b18a010c7a12559c19f6fe993526af88e95a76d5a60b8b75fb", size = 403283 }, - { url = "https://files.pythonhosted.org/packages/d1/ca/e0f0bc1a75a8925024f343258c8ecbd8828f8997ea2ac71e02f67b6f5299/rpds_py-0.25.1-cp313-cp313-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:3c6564c0947a7f52e4792983f8e6cf9bac140438ebf81f527a21d944f2fd0a40", size = 524634 }, - { url = "https://files.pythonhosted.org/packages/3e/03/5d0be919037178fff33a6672ffc0afa04ea1cfcb61afd4119d1b5280ff0f/rpds_py-0.25.1-cp313-cp313-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:5c4a128527fe415d73cf1f70a9a688d06130d5810be69f3b553bf7b45e8acf79", size = 416233 }, - { url = "https://files.pythonhosted.org/packages/05/7c/8abb70f9017a231c6c961a8941403ed6557664c0913e1bf413cbdc039e75/rpds_py-0.25.1-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a49e1d7a4978ed554f095430b89ecc23f42014a50ac385eb0c4d163ce213c325", size = 390375 }, - { url = "https://files.pythonhosted.org/packages/7a/ac/a87f339f0e066b9535074a9f403b9313fd3892d4a164d5d5f5875ac9f29f/rpds_py-0.25.1-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:d74ec9bc0e2feb81d3f16946b005748119c0f52a153f6db6a29e8cd68636f295", size = 424537 }, - { url = "https://files.pythonhosted.org/packages/1f/8f/8d5c1567eaf8c8afe98a838dd24de5013ce6e8f53a01bd47fe8bb06b5533/rpds_py-0.25.1-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:3af5b4cc10fa41e5bc64e5c198a1b2d2864337f8fcbb9a67e747e34002ce812b", size = 566425 }, - { url = "https://files.pythonhosted.org/packages/95/33/03016a6be5663b389c8ab0bbbcca68d9e96af14faeff0a04affcb587e776/rpds_py-0.25.1-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:79dc317a5f1c51fd9c6a0c4f48209c6b8526d0524a6904fc1076476e79b00f98", size = 595197 }, - { url = "https://files.pythonhosted.org/packages/33/8d/da9f4d3e208c82fda311bff0cf0a19579afceb77cf456e46c559a1c075ba/rpds_py-0.25.1-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:1521031351865e0181bc585147624d66b3b00a84109b57fcb7a779c3ec3772cd", size = 561244 }, - { url = "https://files.pythonhosted.org/packages/e2/b3/39d5dcf7c5f742ecd6dbc88f6f84ae54184b92f5f387a4053be2107b17f1/rpds_py-0.25.1-cp313-cp313-win32.whl", hash = "sha256:5d473be2b13600b93a5675d78f59e63b51b1ba2d0476893415dfbb5477e65b31", size = 222254 }, - { url = "https://files.pythonhosted.org/packages/5f/19/2d6772c8eeb8302c5f834e6d0dfd83935a884e7c5ce16340c7eaf89ce925/rpds_py-0.25.1-cp313-cp313-win_amd64.whl", hash = "sha256:a7b74e92a3b212390bdce1d93da9f6488c3878c1d434c5e751cbc202c5e09500", size = 234741 }, - { url = "https://files.pythonhosted.org/packages/5b/5a/145ada26cfaf86018d0eb304fe55eafdd4f0b6b84530246bb4a7c4fb5c4b/rpds_py-0.25.1-cp313-cp313-win_arm64.whl", hash = "sha256:dd326a81afe332ede08eb39ab75b301d5676802cdffd3a8f287a5f0b694dc3f5", size = 224830 }, - { url = "https://files.pythonhosted.org/packages/4b/ca/d435844829c384fd2c22754ff65889c5c556a675d2ed9eb0e148435c6690/rpds_py-0.25.1-cp313-cp313t-macosx_10_12_x86_64.whl", hash = "sha256:a58d1ed49a94d4183483a3ce0af22f20318d4a1434acee255d683ad90bf78129", size = 359668 }, - { url = "https://files.pythonhosted.org/packages/1f/01/b056f21db3a09f89410d493d2f6614d87bb162499f98b649d1dbd2a81988/rpds_py-0.25.1-cp313-cp313t-macosx_11_0_arm64.whl", hash = "sha256:f251bf23deb8332823aef1da169d5d89fa84c89f67bdfb566c49dea1fccfd50d", size = 345649 }, - { url = "https://files.pythonhosted.org/packages/e0/0f/e0d00dc991e3d40e03ca36383b44995126c36b3eafa0ccbbd19664709c88/rpds_py-0.25.1-cp313-cp313t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8dbd586bfa270c1103ece2109314dd423df1fa3d9719928b5d09e4840cec0d72", size = 384776 }, - { url = "https://files.pythonhosted.org/packages/9f/a2/59374837f105f2ca79bde3c3cd1065b2f8c01678900924949f6392eab66d/rpds_py-0.25.1-cp313-cp313t-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:6d273f136e912aa101a9274c3145dcbddbe4bac560e77e6d5b3c9f6e0ed06d34", size = 395131 }, - { url = "https://files.pythonhosted.org/packages/9c/dc/48e8d84887627a0fe0bac53f0b4631e90976fd5d35fff8be66b8e4f3916b/rpds_py-0.25.1-cp313-cp313t-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:666fa7b1bd0a3810a7f18f6d3a25ccd8866291fbbc3c9b912b917a6715874bb9", size = 520942 }, - { url = "https://files.pythonhosted.org/packages/7c/f5/ee056966aeae401913d37befeeab57a4a43a4f00099e0a20297f17b8f00c/rpds_py-0.25.1-cp313-cp313t-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:921954d7fbf3fccc7de8f717799304b14b6d9a45bbeec5a8d7408ccbf531faf5", size = 411330 }, - { url = "https://files.pythonhosted.org/packages/ab/74/b2cffb46a097cefe5d17f94ede7a174184b9d158a0aeb195f39f2c0361e8/rpds_py-0.25.1-cp313-cp313t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f3d86373ff19ca0441ebeb696ef64cb58b8b5cbacffcda5a0ec2f3911732a194", size = 387339 }, - { url = "https://files.pythonhosted.org/packages/7f/9a/0ff0b375dcb5161c2b7054e7d0b7575f1680127505945f5cabaac890bc07/rpds_py-0.25.1-cp313-cp313t-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:c8980cde3bb8575e7c956a530f2c217c1d6aac453474bf3ea0f9c89868b531b6", size = 418077 }, - { url = "https://files.pythonhosted.org/packages/0d/a1/fda629bf20d6b698ae84c7c840cfb0e9e4200f664fc96e1f456f00e4ad6e/rpds_py-0.25.1-cp313-cp313t-musllinux_1_2_aarch64.whl", hash = "sha256:8eb8c84ecea987a2523e057c0d950bcb3f789696c0499290b8d7b3107a719d78", size = 562441 }, - { url = "https://files.pythonhosted.org/packages/20/15/ce4b5257f654132f326f4acd87268e1006cc071e2c59794c5bdf4bebbb51/rpds_py-0.25.1-cp313-cp313t-musllinux_1_2_i686.whl", hash = "sha256:e43a005671a9ed5a650f3bc39e4dbccd6d4326b24fb5ea8be5f3a43a6f576c72", size = 590750 }, - { url = "https://files.pythonhosted.org/packages/fb/ab/e04bf58a8d375aeedb5268edcc835c6a660ebf79d4384d8e0889439448b0/rpds_py-0.25.1-cp313-cp313t-musllinux_1_2_x86_64.whl", hash = "sha256:58f77c60956501a4a627749a6dcb78dac522f249dd96b5c9f1c6af29bfacfb66", size = 558891 }, - { url = "https://files.pythonhosted.org/packages/90/82/cb8c6028a6ef6cd2b7991e2e4ced01c854b6236ecf51e81b64b569c43d73/rpds_py-0.25.1-cp313-cp313t-win32.whl", hash = "sha256:2cb9e5b5e26fc02c8a4345048cd9998c2aca7c2712bd1b36da0c72ee969a3523", size = 218718 }, - { url = "https://files.pythonhosted.org/packages/b6/97/5a4b59697111c89477d20ba8a44df9ca16b41e737fa569d5ae8bff99e650/rpds_py-0.25.1-cp313-cp313t-win_amd64.whl", hash = "sha256:401ca1c4a20cc0510d3435d89c069fe0a9ae2ee6495135ac46bdd49ec0495763", size = 232218 }, - { url = "https://files.pythonhosted.org/packages/78/ff/566ce53529b12b4f10c0a348d316bd766970b7060b4fd50f888be3b3b281/rpds_py-0.25.1-pp310-pypy310_pp73-macosx_10_12_x86_64.whl", hash = "sha256:b24bf3cd93d5b6ecfbedec73b15f143596c88ee249fa98cefa9a9dc9d92c6f28", size = 373931 }, - { url = "https://files.pythonhosted.org/packages/83/5d/deba18503f7c7878e26aa696e97f051175788e19d5336b3b0e76d3ef9256/rpds_py-0.25.1-pp310-pypy310_pp73-macosx_11_0_arm64.whl", hash = "sha256:0eb90e94f43e5085623932b68840b6f379f26db7b5c2e6bcef3179bd83c9330f", size = 359074 }, - { url = "https://files.pythonhosted.org/packages/0d/74/313415c5627644eb114df49c56a27edba4d40cfd7c92bd90212b3604ca84/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d50e4864498a9ab639d6d8854b25e80642bd362ff104312d9770b05d66e5fb13", size = 387255 }, - { url = "https://files.pythonhosted.org/packages/8c/c8/c723298ed6338963d94e05c0f12793acc9b91d04ed7c4ba7508e534b7385/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:7c9409b47ba0650544b0bb3c188243b83654dfe55dcc173a86832314e1a6a35d", size = 400714 }, - { url = "https://files.pythonhosted.org/packages/33/8a/51f1f6aa653c2e110ed482ef2ae94140d56c910378752a1b483af11019ee/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:796ad874c89127c91970652a4ee8b00d56368b7e00d3477f4415fe78164c8000", size = 523105 }, - { url = "https://files.pythonhosted.org/packages/c7/a4/7873d15c088ad3bff36910b29ceb0f178e4b3232c2adbe9198de68a41e63/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:85608eb70a659bf4c1142b2781083d4b7c0c4e2c90eff11856a9754e965b2540", size = 411499 }, - { url = "https://files.pythonhosted.org/packages/90/f3/0ce1437befe1410766d11d08239333ac1b2d940f8a64234ce48a7714669c/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c4feb9211d15d9160bc85fa72fed46432cdc143eb9cf6d5ca377335a921ac37b", size = 387918 }, - { url = "https://files.pythonhosted.org/packages/94/d4/5551247988b2a3566afb8a9dba3f1d4a3eea47793fd83000276c1a6c726e/rpds_py-0.25.1-pp310-pypy310_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:ccfa689b9246c48947d31dd9d8b16d89a0ecc8e0e26ea5253068efb6c542b76e", size = 421705 }, - { url = "https://files.pythonhosted.org/packages/b0/25/5960f28f847bf736cc7ee3c545a7e1d2f3b5edaf82c96fb616c2f5ed52d0/rpds_py-0.25.1-pp310-pypy310_pp73-musllinux_1_2_aarch64.whl", hash = "sha256:3c5b317ecbd8226887994852e85de562f7177add602514d4ac40f87de3ae45a8", size = 564489 }, - { url = "https://files.pythonhosted.org/packages/02/66/1c99884a0d44e8c2904d3c4ec302f995292d5dde892c3bf7685ac1930146/rpds_py-0.25.1-pp310-pypy310_pp73-musllinux_1_2_i686.whl", hash = "sha256:454601988aab2c6e8fd49e7634c65476b2b919647626208e376afcd22019eeb8", size = 592557 }, - { url = "https://files.pythonhosted.org/packages/55/ae/4aeac84ebeffeac14abb05b3bb1d2f728d00adb55d3fb7b51c9fa772e760/rpds_py-0.25.1-pp310-pypy310_pp73-musllinux_1_2_x86_64.whl", hash = "sha256:1c0c434a53714358532d13539272db75a5ed9df75a4a090a753ac7173ec14e11", size = 558691 }, - { url = "https://files.pythonhosted.org/packages/41/b3/728a08ff6f5e06fe3bb9af2e770e9d5fd20141af45cff8dfc62da4b2d0b3/rpds_py-0.25.1-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:f73ce1512e04fbe2bc97836e89830d6b4314c171587a99688082d090f934d20a", size = 231651 }, - { url = "https://files.pythonhosted.org/packages/49/74/48f3df0715a585cbf5d34919c9c757a4c92c1a9eba059f2d334e72471f70/rpds_py-0.25.1-pp311-pypy311_pp73-macosx_10_12_x86_64.whl", hash = "sha256:ee86d81551ec68a5c25373c5643d343150cc54672b5e9a0cafc93c1870a53954", size = 374208 }, - { url = "https://files.pythonhosted.org/packages/55/b0/9b01bb11ce01ec03d05e627249cc2c06039d6aa24ea5a22a39c312167c10/rpds_py-0.25.1-pp311-pypy311_pp73-macosx_11_0_arm64.whl", hash = "sha256:89c24300cd4a8e4a51e55c31a8ff3918e6651b241ee8876a42cc2b2a078533ba", size = 359262 }, - { url = "https://files.pythonhosted.org/packages/a9/eb/5395621618f723ebd5116c53282052943a726dba111b49cd2071f785b665/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:771c16060ff4e79584dc48902a91ba79fd93eade3aa3a12d6d2a4aadaf7d542b", size = 387366 }, - { url = "https://files.pythonhosted.org/packages/68/73/3d51442bdb246db619d75039a50ea1cf8b5b4ee250c3e5cd5c3af5981cd4/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:785ffacd0ee61c3e60bdfde93baa6d7c10d86f15655bd706c89da08068dc5038", size = 400759 }, - { url = "https://files.pythonhosted.org/packages/b7/4c/3a32d5955d7e6cb117314597bc0f2224efc798428318b13073efe306512a/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:2a40046a529cc15cef88ac5ab589f83f739e2d332cb4d7399072242400ed68c9", size = 523128 }, - { url = "https://files.pythonhosted.org/packages/be/95/1ffccd3b0bb901ae60b1dd4b1be2ab98bb4eb834cd9b15199888f5702f7b/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:85fc223d9c76cabe5d0bff82214459189720dc135db45f9f66aa7cffbf9ff6c1", size = 411597 }, - { url = "https://files.pythonhosted.org/packages/ef/6d/6e6cd310180689db8b0d2de7f7d1eabf3fb013f239e156ae0d5a1a85c27f/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b0be9965f93c222fb9b4cc254235b3b2b215796c03ef5ee64f995b1b69af0762", size = 388053 }, - { url = "https://files.pythonhosted.org/packages/4a/87/ec4186b1fe6365ced6fa470960e68fc7804bafbe7c0cf5a36237aa240efa/rpds_py-0.25.1-pp311-pypy311_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:8378fa4a940f3fb509c081e06cb7f7f2adae8cf46ef258b0e0ed7519facd573e", size = 421821 }, - { url = "https://files.pythonhosted.org/packages/7a/60/84f821f6bf4e0e710acc5039d91f8f594fae0d93fc368704920d8971680d/rpds_py-0.25.1-pp311-pypy311_pp73-musllinux_1_2_aarch64.whl", hash = "sha256:33358883a4490287e67a2c391dfaea4d9359860281db3292b6886bf0be3d8692", size = 564534 }, - { url = "https://files.pythonhosted.org/packages/41/3a/bc654eb15d3b38f9330fe0f545016ba154d89cdabc6177b0295910cd0ebe/rpds_py-0.25.1-pp311-pypy311_pp73-musllinux_1_2_i686.whl", hash = "sha256:1d1fadd539298e70cac2f2cb36f5b8a65f742b9b9f1014dd4ea1f7785e2470bf", size = 592674 }, - { url = "https://files.pythonhosted.org/packages/2e/ba/31239736f29e4dfc7a58a45955c5db852864c306131fd6320aea214d5437/rpds_py-0.25.1-pp311-pypy311_pp73-musllinux_1_2_x86_64.whl", hash = "sha256:9a46c2fb2545e21181445515960006e85d22025bd2fe6db23e76daec6eb689fe", size = 558781 }, -] - [[package]] name = "ruff" version = "0.11.10" @@ -1625,15 +1338,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/04/be/d09147ad1ec7934636ad912901c5fd7667e1c858e19d355237db0d0cd5e4/smmap-5.0.2-py3-none-any.whl", hash = "sha256:b30115f0def7d7531d22a0fb6502488d879e75b260a9db4d0819cfb25403af5e", size = 24303 }, ] -[[package]] -name = "soupsieve" -version = "2.7" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/3f/f4/4a80cd6ef364b2e8b65b15816a843c0980f7a5a2b4dc701fc574952aa19f/soupsieve-2.7.tar.gz", hash = "sha256:ad282f9b6926286d2ead4750552c8a6142bc4c783fd66b0293547c8fe6ae126a", size = 103418 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/e7/9c/0e6afc12c269578be5c0c1c9f4b49a8d32770a080260c333ac04cc1c832d/soupsieve-2.7-py3-none-any.whl", hash = "sha256:6e60cc5c1ffaf1cebcc12e8188320b72071e922c2e897f737cadce79ad5d30c4", size = 36677 }, -] - [[package]] name = "stack-data" version = "0.6.3" @@ -1648,18 +1352,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/f1/7b/ce1eafaf1a76852e2ec9b22edecf1daa58175c090266e9f6c64afcd81d91/stack_data-0.6.3-py3-none-any.whl", hash = "sha256:d5558e0c25a4cb0853cddad3d77da9891a08cb85dd9f9f91b9f8cd66e511e695", size = 24521 }, ] -[[package]] -name = "tinycss2" -version = "1.4.0" -source = { registry = "https://pypi.org/simple" } -dependencies = [ - { name = "webencodings" }, -] -sdist = { url = "https://files.pythonhosted.org/packages/7a/fd/7a5ee21fd08ff70d3d33a5781c255cbe779659bd03278feb98b19ee550f4/tinycss2-1.4.0.tar.gz", hash = "sha256:10c0972f6fc0fbee87c3edb76549357415e94548c1ae10ebccdea16fb404a9b7", size = 87085 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/e6/34/ebdc18bae6aa14fbee1a08b63c015c72b64868ff7dae68808ab500c492e2/tinycss2-1.4.0-py3-none-any.whl", hash = "sha256:3a49cf47b7675da0b15d0c6e1df8df4ebd96e9394bb905a5775adb0d884c5289", size = 26610 }, -] - [[package]] name = "tomli" version = "2.2.1" @@ -1806,15 +1498,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/fd/84/fd2ba7aafacbad3c4201d395674fc6348826569da3c0937e75505ead3528/wcwidth-0.2.13-py2.py3-none-any.whl", hash = "sha256:3da69048e4540d84af32131829ff948f1e022c1c6bdb8d6102117aac784f6859", size = 34166 }, ] -[[package]] -name = "webencodings" -version = "0.5.1" -source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/0b/02/ae6ceac1baeda530866a85075641cec12989bd8d31af6d5ab4a3e8c92f47/webencodings-0.5.1.tar.gz", hash = "sha256:b36a1c245f2d304965eb4e0a82848379241dc04b865afcc4aab16748587e1923", size = 9721 } -wheels = [ - { url = "https://files.pythonhosted.org/packages/f4/24/2a3e3df732393fed8b3ebf2ec078f05546de641fe1b667ee316ec1dcf3b7/webencodings-0.5.1-py2.py3-none-any.whl", hash = "sha256:a0af1213f3c2226497a97e2b3aa01a7e4bee4f403f95be16fc9acd2947514a78", size = 11774 }, -] - [[package]] name = "zipp" version = "3.23.0"