v0.1.0-alpha.6

Installing this build

Per-platform .vsix (recommended — Java is bundled)

Download the asset whose suffix matches the host where the VS Code extension runs. For SSH-Remote, WSL, or dev-container setups, that's the remote / target host's OS + CPU, not your laptop's.

Asset suffix	Host platform
-win32-x64.vsix	Windows x64
-win32-arm64.vsix	Windows on ARM
-linux-x64.vsix	Linux x64 (glibc)
-linux-arm64.vsix	Linux ARM64 (glibc)
-alpine-x64.vsix	Alpine / musl x64
-alpine-arm64.vsix	Alpine / musl ARM64
-darwin-arm64.vsix	macOS Apple silicon

• macOS Intel users: install the universal .vsix instead (no platform suffix). Requires Java 21+ on PATH. The dedicated macOS Intel build was dropped in v0.1.0-alpha.3 due to chronic macos-13 runner pool unavailability — see AGENTS.md §17.

Install via either:

• VS Code GUI — Extensions view → … menu → Install from VSIX… → pick the downloaded file; or
• Command line — code --install-extension <downloaded>.vsix.

Universal .vsix (isabelle-pide-vscode-0.1.0-alpha.6.vsix)

For platforms not listed above (NixOS, *BSD, exotic CPU archs, macOS Intel) or bring-your-own-Java setups. Requires Java 21+ on PATH.

Runtime prerequisites

• Java 21+ on PATH — only required by the universal .vsix. Per-platform builds bundle Eclipse Temurin 21 under extension/jre/.
• Isabelle 2019 or newer with isabelle on PATH (or set isabelle.executablePath) for build / language-server / sledgehammer features. The extension still activates without it; basic syntax features work, and a Setup Walkthrough surfaces any missing piece.

See the README and THIRD_PARTY_NOTICES.md for full installation guidance and the bundled-JRE license summary.

What's Changed

• docs(release): harden alpha.5 release gate by @Arthur742Ramos in #98
• ci(tier2): automate real Isabelle smoke checks by @Arthur742Ramos in #99
• fix(setup): harden current mode diagnostics by @Arthur742Ramos in #100
• docs: clarify alpha to beta readiness by @Arthur742Ramos in #101
• chore(release): v0.1.0-alpha.6 by @Arthur742Ramos in #102
• docs: align alpha.6 release references by @Arthur742Ramos in #103
• chore(release): harden release readiness by @Arthur742Ramos in #104
• Surface PIDE proof-state and Sledgehammer trust indicators by @Arthur742Ramos in #105
• ci: harden Tier-2 smoke automation by @Arthur742Ramos in #106
• feat(ux): improve Isabelle command discoverability by @Arthur742Ramos in #108
• fix(setup): clarify Windows Isabelle launcher failures by @Arthur742Ramos in #110
• feat(setup): add actionable current-mode next steps by @Arthur742Ramos in #107
• feat(lsp): add one-click auto-start retry by @Arthur742Ramos in #109
• chore(release): v0.1.0-alpha.6 by @Arthur742Ramos in #111

Full Changelog: v0.1.0-alpha.5...v0.1.0-alpha.6

v0.1.0-alpha.5

Installing this build

Per-platform .vsix (recommended — Java is bundled)

Download the asset whose suffix matches the host where the VS Code extension runs. For SSH-Remote, WSL, or dev-container setups, that's the remote / target host's OS + CPU, not your laptop's.

Asset suffix	Host platform
-win32-x64.vsix	Windows x64
-win32-arm64.vsix	Windows on ARM
-linux-x64.vsix	Linux x64 (glibc)
-linux-arm64.vsix	Linux ARM64 (glibc)
-alpine-x64.vsix	Alpine / musl x64
-alpine-arm64.vsix	Alpine / musl ARM64
-darwin-arm64.vsix	macOS Apple silicon

• macOS Intel users: install the universal .vsix instead (no platform suffix). Requires Java 21+ on PATH. The dedicated macOS Intel build was dropped in v0.1.0-alpha.3 due to chronic macos-13 runner pool unavailability — see AGENTS.md §17.

Install via either:

• VS Code GUI — Extensions view → … menu → Install from VSIX… → pick the downloaded file; or
• Command line — code --install-extension <downloaded>.vsix.

Universal .vsix (isabelle-pide-vscode-0.1.0-alpha.5.vsix)

For platforms not listed above (NixOS, *BSD, exotic CPU archs, macOS Intel) or bring-your-own-Java setups. Requires Java 21+ on PATH.

Runtime prerequisites

• Java 21+ on PATH — only required by the universal .vsix. Per-platform builds bundle Eclipse Temurin 21 under extension/jre/.
• Isabelle 2019 or newer with isabelle on PATH (or set isabelle.executablePath) for build / language-server / sledgehammer features. The extension still activates without it; basic syntax features work, and a Setup Walkthrough surfaces any missing piece.

See the README and THIRD_PARTY_NOTICES.md for full installation guidance and the bundled-JRE license summary.

What's Changed

• docs: alpha polish pass — smoke session, doc drift, beta criteria, screenshot spec by @Arthur742Ramos in #91
• feat(pide): Phase 3c — range-filtered snapshot.messages for per-cursor proof state by @Arthur742Ramos in #94
• chore(release): v0.1.0-alpha.5 by @Arthur742Ramos in #95

Full Changelog: v0.1.0-alpha.4...v0.1.0-alpha.5

v0.1.0-alpha.4

Installing this build

Per-platform .vsix (recommended — Java is bundled)

Download the asset whose suffix matches the host where the VS Code extension runs. For SSH-Remote, WSL, or dev-container setups, that's the remote / target host's OS + CPU, not your laptop's.

Asset suffix	Host platform
-win32-x64.vsix	Windows x64
-win32-arm64.vsix	Windows on ARM
-linux-x64.vsix	Linux x64 (glibc)
-linux-arm64.vsix	Linux ARM64 (glibc)
-alpine-x64.vsix	Alpine / musl x64
-alpine-arm64.vsix	Alpine / musl ARM64
-darwin-arm64.vsix	macOS Apple silicon

• macOS Intel users: install the universal .vsix instead (no platform suffix). Requires Java 21+ on PATH. The dedicated macOS Intel build was dropped in v0.1.0-alpha.3 due to chronic macos-13 runner pool unavailability — see AGENTS.md §17.

Install via either:

• VS Code GUI — Extensions view → … menu → Install from VSIX… → pick the downloaded file; or
• Command line — code --install-extension <downloaded>.vsix.

Universal .vsix (isabelle-pide-vscode-0.1.0-alpha.4.vsix)

For platforms not listed above (NixOS, *BSD, exotic CPU archs, macOS Intel) or bring-your-own-Java setups. Requires Java 21+ on PATH.

Runtime prerequisites

• Java 21+ on PATH — only required by the universal .vsix. Per-platform builds bundle Eclipse Temurin 21 under extension/jre/.
• Isabelle 2019 or newer with isabelle on PATH (or set isabelle.executablePath) for build / language-server / sledgehammer features. The extension still activates without it; basic syntax features work, and a Setup Walkthrough surfaces any missing piece.

See the README and THIRD_PARTY_NOTICES.md for full installation guidance and the bundled-JRE license summary.

What's Changed

• feat(setup): auto-detect isabelle on PATH + run session cascade for every PIDE command by @Arthur742Ramos in #87
• chore(release): v0.1.0-alpha.4 by @Arthur742Ramos in #88

Full Changelog: v0.1.0-alpha.3...v0.1.0-alpha.4

v0.1.0-alpha.3

Installing this build

Per-platform .vsix (recommended — Java is bundled)

Download the asset whose suffix matches the host where the VS Code extension runs. For SSH-Remote, WSL, or dev-container setups, that's the remote / target host's OS + CPU, not your laptop's.

Asset suffix	Host platform
-win32-x64.vsix	Windows x64
-win32-arm64.vsix	Windows on ARM
-linux-x64.vsix	Linux x64 (glibc)
-linux-arm64.vsix	Linux ARM64 (glibc)
-alpine-x64.vsix	Alpine / musl x64
-alpine-arm64.vsix	Alpine / musl ARM64
-darwin-arm64.vsix	macOS Apple silicon

• macOS Intel users: install the universal .vsix instead (no platform suffix). Requires Java 21+ on PATH. The dedicated macOS Intel build was dropped in v0.1.0-alpha.3 due to chronic macos-13 runner pool unavailability — see AGENTS.md §17.

Install via either:

• VS Code GUI — Extensions view → … menu → Install from VSIX… → pick the downloaded file; or
• Command line — code --install-extension <downloaded>.vsix.

Universal .vsix (isabelle-pide-vscode-0.1.0-alpha.3.vsix)

For platforms not listed above (NixOS, *BSD, exotic CPU archs, macOS Intel) or bring-your-own-Java setups. Requires Java 21+ on PATH.

Runtime prerequisites

• Java 21+ on PATH — only required by the universal .vsix. Per-platform builds bundle Eclipse Temurin 21 under extension/jre/.
• Isabelle 2019 or newer with isabelle on PATH (or set isabelle.executablePath) for build / language-server / sledgehammer features. The extension still activates without it; basic syntax features work, and a Setup Walkthrough surfaces any missing piece.

See the README and THIRD_PARTY_NOTICES.md for full installation guidance and the bundled-JRE license summary.

What's Changed

• Build Isabelle VS Code milestone scaffold by @Arthur742Ramos in #1
• Continue Isabelle VS Code roadmap through proof-state panel by @Arthur742Ramos in #2
• Add Sledgehammer workflow surface by @Arthur742Ramos in #6
• Add checked repair loop foundation by @Arthur742Ramos in #5
• Milestone 11: production readiness polish by @Arthur742Ramos in #7
• Add theory dependency graph foundation by @Arthur742Ramos in #4
• Add repository validation CI by @Arthur742Ramos in #3
• Add proof engineering tools by @Arthur742Ramos in #8
• Advance Isabelle roadmap foundations by @Arthur742Ramos in #9
• Add document status/status-surface roadmap increment by @Arthur742Ramos in #10
• Cross-file definition navigation roadmap increment by @Arthur742Ramos in #12
• Checked repair verification roadmap increment by @Arthur742Ramos in #11
• Introduce PIDE bridge scaffold in Scala backend (Milestone 4/5 architecture) by @Arthur742Ramos in #13
• Add Sledgehammer run history (Milestone 7 increment) by @Arthur742Ramos in #15
• Add theory entity outline (Milestone 5 increment) by @Arthur742Ramos in #16
• Add command-span status decorations (Milestone 4 increment) by @Arthur742Ramos in #14
• Add reverse-dependency navigation to the theory graph (Milestone 8 increment) by @Arthur742Ramos in #17
• Debounce command-span decoration refresh (Milestone 4 follow-up) by @Arthur742Ramos in #18
• Add docs/PIDE_INTEGRATION.md describing the Isabelle LSP-relay approach by @Arthur742Ramos in #21
• Add ScalaTest test framework wiring (redux of #24) by @Arthur742Ramos in #25
• Add Isabelle LSP client scaffold via isabelle vscode_server (Milestone 4/5/7 PIDE) by @Arthur742Ramos in #26
• Auto-wrap Isabelle .ps1 launcher on Windows for the LSP client by @Arthur742Ramos in #27
• Refresh PIDE_INTEGRATION.md for shipped LSP scaffold + Windows fix by @Arthur742Ramos in #28
• Verify LSP PublishDiagnostics merge with CLI-build diagnostics (Milestone 4) by @Arthur742Ramos in #29
• Research: capture isabelle vscode_server LSP surface for Sledgehammer (Milestone 7 research) by @Arthur742Ramos in #30
• Add LSP notification I/O seam on IsabelleLanguageClient (Milestone 7 plumbing) by @Arthur742Ramos in #31
• Add Isabelle XML parser for PIDE/sledgehammer_output (Milestone 7 plumbing, recommendation #4) by @Arthur742Ramos in #32
• Add isabelle.sledgehammer.{provers,isar,try0} settings + reader (Milestone 7 plumbing, recommendation #6) by @Arthur742Ramos in #33
• Add PideSledgehammerProversCache subscribing to PIDE/sledgehammer_provers_response (Milestone 7 plumbing, recommendation #6) by @Arthur742Ramos in #34
• Suppress local command-span decorations while the LSP is running (Milestone 4) by @Arthur742Ramos in #35
• Add LspSledgehammerSession orchestrating PIDE/sledgehammer_* runs (Milestone 7, rec #2 groundwork + #3) by @Arthur742Ramos in #36
• Route SledgehammerPanel through LSP when language server is running (Milestone 7) by @Arthur742Ramos in #37
• Wire two-step LSP sendback insert flow into SledgehammerPanel (Milestone 7, rec #5) by @Arthur742Ramos in #38
• Add quiescence gate before LSP-mode Sledgehammer dispatch (Milestone 7, rec #7) by @Arthur742Ramos in #39
• Verify Milestone 4 + 5 LSP/local feature coexistence structurally by @Arthur742Ramos in #40
• Add Isabelle: Pick Sledgehammer Suggestion command (Milestone 7 polish) by @Arthur742Ramos in #41
• Research: PIDE state-panel + sledgehammer-minimization LSP surfaces (M6 unblock, M7-min blocked) by @Arthur742Ramos in #42
• Implement LSP-backed proof state via PIDE/state_* surface (Milestone 6) by @Arthur742Ramos in #43
• Add optional AI repair seam: clipboard export + opt-in provider registry (Milestone 9) by @Arthur742Ramos in #44
• Add PIDE/dynamic_output subsurface to the proof state panel (Milestone 6 2/2) by @Arthur742Ramos in #45
• Add IsabellePideExtensionApi for 3rd-party AI repair provider registration (M9 follow-up) by @Arthur742Ramos in #46
• Add SecretStorage-backed credential helper for AI repair providers (M9 follow-up) by @Arthur742Ramos in #47
• Add built-in manual-paste-back AI repair provider (M9 — safe-by-default, no network) by @Arthur742Ramos in #48
• docs(ai-repair): refresh TL;DR to reflect the bundled manual-paste-back provider by @Arthur742Ramos in #49
• docs: add ROADMAP_STATUS.md consolidating the full session outcome by @Arthur742Ramos in #50
• Add PIDE/decoration editor overlay (Milestone 5 advance) by @Arthur742Ramos in #51
• Add PIDE abbreviations cache + completion provider (Milestone 5 advance) by @Arthur742Ramos in #52
• Add Isabelle: Browse Isabelle Documentation command (Milestone 5 advance) by @Arthur742Ramos in #53
• docs(roadmap-status): consolidate PRs 51-53 + map remaining upstream LSP surfaces by @Arthur742Ramos in #54
• Add Isabelle: Preview Theory live HTML preview commands (Milestone 5 advance) by @Arthur742Ramos in #55
• Add Isabelle spell-checker dictionary commands (Milestone 5 advance) by @Arthur742Ramos in #56
• Add proof state auto-update + margin + relocate controls (Milestone 6 advance) by @Arthur742Ramos in #57
• docs(roadmap-status): consolidate PRs 55-57 (preview, spell-c...