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-checker, proof state controls) by @Arthur742Ramos in #58
• Make the extension installable end-to-end by @Arthur742Ramos in #59
• feat(setup): walkthrough, prerequisite checker, auto-detect, install matrix by @Arthur742Ramos in #60
• fix(setup): address PR #60 review comments by @Arthur742Ramos in #61
• ci: add Release workflow that publishes .vsix on v* tags by @Arthur742Ramos in #62
• docs: add agent instructions, contributor guide, templates, and cloud-agent setup by @Arthur742Ramos in #63
• docs(skills): add cross-agent skills + Copilot CLI helper extension by @Arthur742Ramos in #64
• feat(setup): smart-default LSP auto-start when Isabelle is detected by @Arthur742Ramos in #65
• feat(release): bundle per-platform Eclipse Temurin 21 JRE in .vsix by @Arthur742Ramos in #66
• fix(lsp): resolve bare isabelle on Windows PATH via .ps1 lookup by @Arthur742Ramos in #67
• Review-driven hardening: smoke theory, docs reconciliation, Explain Current Mode command by @Arthur742Ramos in #68
• chore(release): v0.1.0-alpha.1 by @Arthur742Ramos in #69
• fix(lsp): omit ServerOptions transport so isabelle vscode_server accepts launch by @Arthur742Ramos in #70
• feat(menus): add curated right-click menu for Isabelle .thy files by @Arthur742Ramos in #71
• chore(backend): migrate Scala backend to 3.3.4 for PIDE compat by @Arthur742Ramos in #72
• feat(backend): wire runtime classpath bridge to Isabelle/PIDE by @Arthur742Ramos in #74
• feat(test): add minimal VS Code-hosted activation + command-registration tests by @Arthur742Ramos in #73
• feat(backend): wire PIDE document submission via Headless.Session.use_theories (Phase 2a) by @Arthur742Ramos in #75
• feat(backend): cancel in-flight use_theories via Session teardown (Phase 2b) by @Arthur742Ramos in #76
• feat(backend): wire PIDE cache diagnostics + prewarm-on-activation (Phase 2c) by @Arthur742Ramos in #77
• refactor(backend): async PIDE cancel teardown + status-bar copy + AGENTS §13 (Phase 2b polish) by @Arthur742Ramos in #78
• feat(backend): Phase 3a — PIDE snapshot extraction + per-(uri,version,session) cache by @Arthur742Ramos in #79
• feat(backend): Phase 3b — real PIDE proof state via snapshot.messages by @Arthur742Ramos in #80
• feat(backend): Phase 4 — PIDE-backed Sledgehammer via source-injection by @Arthur742Ramos in #81
• feat: Phase 5 — Sledgehammer minimization (M7 upstream-blocked unlock) by @Arthur742Ramos in #82
• docs(roadmap): PIDE backend integration track is complete by @Arthur742Ramos in #83
• chore(release): v0.1.0-alpha.2 by @Arthur742Ramos in #84
• ci(release): drop darwin-x64 from per-platform matrix due to macos-13 runner unavailability by @Arthur742Ramos in #85
• chore(release): v0.1.0-alpha.3 by @Arthur742Ramos in #86

Full Changelog: https://github.com/Arthur742Ramos/Isabelle-VSCode/commits/v0.1.0-alpha.3