Metadata-Version: 2.4
Name: my-better-isabelle-prover
Version: 0.1.0
Summary: Patch manager for Isabelle installations
Author-email: Qiyuan Xu <xu@qiyuan.me>
License-Expression: MIT
Project-URL: Homepage, https://github.com/xqyww123/my_better_isabelle_prover
Project-URL: Repository, https://github.com/xqyww123/my_better_isabelle_prover
Project-URL: Issues, https://github.com/xqyww123/my_better_isabelle_prover/issues
Keywords: isabelle,patch,pide,lsp,theorem-proving
Classifier: Development Status :: 3 - Alpha
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: Operating System :: POSIX
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Software Development :: Build Tools
Requires-Python: >=3.12
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

# my-better-isabelle-prover

A patch manager for Isabelle installations.

GitHub: <https://github.com/xqyww123/my_better_isabelle_prover>

It exists primarily to support
[**Isabelle-MCP**](https://github.com/xqyww123/Isabelle-MCP) (Isa-LSP), an MCP
server that drives Isabelle over its LSP interface for AI agents. That server
needs PIDE/LSP requests the stock `vscode_server` does not expose, and the
[`Isa-REPL`](https://github.com/xqyww123/Isa-REPL) it builds on needs an ML
loader function that Isabelle2025-2 removed.
Neither can be added without editing *vendored* Isabelle source — the Pure ML
loader and the `vscode_server` Scala. This tool keeps those edits as
version-keyed unified diffs and applies, reverses, and checks them idempotently,
then rebuilds the affected Scala when needed.

> [!IMPORTANT]
> Before using this tool, make sure the `isabelle` command is available — on
> your `PATH`, or passed explicitly via `--isabelle-bin PATH`. Every command
> needs it (to detect the version and locate `ISABELLE_HOME`) and aborts with an
> error if it cannot be found. The system `patch` command must likewise be
> installed.

```bash
pip install -e .
my-better-isabelle patch          # apply all patches for the detected version
my-better-isabelle status         # show what is applied
my-better-isabelle unpatch        # reverse them
```

The Python version constraint is declared in `pyproject.toml`. See
**[reference.md](reference.md)** for the full list of prerequisites and CLI
options.

## Features

A *feature* is one self-consistent bundle of patches, stored per Isabelle
version. Run `my-better-isabelle status` to see which are applied.

| Feature | Isabelle2024 | Isabelle2025-2 | What it adds |
|---------|:---:|:---:|--------------|
| [`pide_control`](my_better_isabelle_prover/patches/pide_control.md) | ✓ | ✓ | PIDE LSP control requests the stock `vscode_server` does not expose |
| [`register_thy`](my_better_isabelle_prover/patches/Isabelle2025-2/register_thy.md) | native | ✓ | Restores `Thy_Info.register_thy`, removed in 2025-2 |

### `pide_control` — PIDE LSP control extensions

Edits five ML/Scala files to add these LSP requests (full request/response
protocol in **[pide_control.md](my_better_isabelle_prover/patches/pide_control.md)**):

- **`PIDE/theory_status`** — per-theory processing status for *all* loaded
  theories, including auto-loaded dependencies.
- **`PIDE/cancel_execution`** — immediately cancel all running processing,
  globally.
- **`PIDE/command_at_position`** — source text and range of the Isar command
  enclosing a position, with no caret move.
- **`PIDE/output_at_position`** — source, range, *and* rendered prover output of
  the command enclosing a position, in one request, with no caret move.
- **`PIDE/symbols`** — dump the `etc/symbols` translation table(s) so a client
  can decode/encode Isabelle symbol notation (`\<forall>` ↔ ∀).

### `register_thy` — restore removed theory registration (Isabelle2025-2)

`Thy_Info.register_thy` existed in 2024 but was removed by the 2025-2
theory-loader refactoring. `Isa-REPL` needs it to inject an already-built,
in-memory `theory` value into Isabelle's global loader database. The patch
re-adds it, restored from the 2024 source with one node-type adaptation. Pure ML
change — no `scala_build`. Details in
**[register_thy.md](my_better_isabelle_prover/patches/Isabelle2025-2/register_thy.md)**.

## Supported versions & verification status

Patch targets are keyed by the exact output of `isabelle version`
(e.g. `Isabelle2024`, `Isabelle2025-2`).

- **Isabelle2024** — `pide_control` authored, compiled (`scala_build` clean), and
  runtime-tested. `register_thy` ships natively, so no patch is needed.
- **Isabelle2025-2** — `pide_control` authored and round-trip-verified against
  pristine source, but **not yet compiled**. `register_thy` applies and
  reverse-detects cleanly, but the Pure/HOL heap has **not** yet been rebuilt
  with it. Verify before relying on either; see each feature doc for the exact
  scope tested.

## Documentation

- **[reference.md](reference.md)** — CLI reference: subcommands, flags, examples,
  exit codes, and runtime prerequisites.
- **[develop.md](develop.md)** — how the manager works, the patch-repository
  layout, and how to add a new patch.
- Feature docs (full protocol / rationale):
  [`pide_control.md`](my_better_isabelle_prover/patches/pide_control.md),
  [`register_thy.md`](my_better_isabelle_prover/patches/Isabelle2025-2/register_thy.md).
