my-better-isabelle-prover

A patch manager for Isabelle installations.

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

It carries the patches that the surrounding Isabelle/ML research stack needs: the SIMD FFI of Semantic_Embedding, and — for development — Isa-REPL and Isa-Mini, notably an ML loader function that Isabelle2025-2 removed. This tool keeps those edits as version-keyed unified diffs and applies, reverses, and checks them idempotently, then rebuilds the affected Scala when needed.

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

The Python version constraint is declared in pyproject.toml. See 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.

Categories

Each feature is either user or dev, and my-better-isabelle patch applies only the user ones by default.

• user — needed by the user-facing systems. On Isabelle2025-2 that is now only the SIMD FFI of Semantic_Embedding (expose_foreign); the two Isabelle-MCP features are retired there and survive for Isabelle2024 alone.
• dev — needed only by developer/experiment infrastructure: Isa-REPL, and Isa-Mini's translator and AoA agent injector.

status always lists every feature regardless of category; its exit code reflects only the selected category (user by default). Categories live in patches/categories.toml.

pide_control — PIDE LSP control extensions (Isabelle2024 only; retired on 2025-2)

Edits five ML/Scala files to add these LSP requests (full request/response protocol in 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.

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; still applied there. register_thy ships natively, so no patch is needed.
• Isabelle2025-2 — pide_control and perspective_eof_clamp were applied, compiled and runtime-tested here, and have now been reversed and retired (see the note above). The reversal was verified byte-for-byte against the pristine sources and isabelle scala_build -f was re-run, so this distribution's Scala is stock again. register_thy applies and reverse-detects cleanly.
• show_types_nv — recorded for Isabelle2024 (reverse-recorded from the existing hand edit) and ported to Isabelle2025-2. On 2025-2 it is applied, the Pure heap has been rebuilt, and it is runtime-verified (free-variable type annotation suppressed). The end-to-end consumer path (Isa-Mini/.../print_formats.ML, show_markup=false, HOL terms) is pending the HOL/Isa-Mini rebuild.

Documentation

• reference.md — CLI reference: subcommands, flags, examples, exit codes, and runtime prerequisites.
• develop.md — how the manager works, the patch-repository layout, and how to add a new patch.
• RELEASE.md — how a version is cut and published to PyPI.
• Feature docs (full protocol / rationale): pide_control.md, expose_foreign.md, register_thy.md, show_types_nv.md, expose_map_syn.md.