v0.9.0

.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

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:

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

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`.

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
 

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,32 +6,32 @@ 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
 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:

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"
         )
     ]
 )

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)))
+```

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,50 +6,50 @@ 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
 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
 config = LeanREPLConfig(project=TempRequireProject(lean_version="v4.19.0", require="mathlib"))
 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 
   (x : ℝ) (y : ℚ) : Irrational x → Irrational (x + y) := by
   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