Release of VS Code extension

Author: dstebila

index.md

@@ -38,6 +38,7 @@ See the [installation instructions]({% link manual/installation.md %}) for detai
 
 ## Recent updates
 
+- Apr. 11, 2025: Release of [ProofFrog VS Code Extension version 0.1.0](https://marketplace.visualstudio.com/items?itemName=ProofFrog.prooffrog) on VS Code Extension Marketplace
 - Mar. 6, 2026: [ProofFrog discussions and demos at HACS 2026](http://prooffrog.github.io/researchers/publications/hacs-2026/)
 - **Mar. 5, 2026: Release of [ProofFrog version 0.3.1](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.3.1)** featuring a web interface and engine updates
 

manual/editor-plugins.md

@@ -8,7 +8,7 @@ nav_order: 80
 # Editor Plugins
 {: .no_toc }
 
-ProofFrog ships a plugin for Visual Studio Code that provides rich editing support for FrogLang files. The plugin connects to an LSP server bundled with ProofFrog (`proof_frog lsp`); any other editor that supports the Language Server Protocol can be wired up to the same server without a dedicated plugin. Additional first-party plugins may be added in the future. See the [Engine Internals]({% link researchers/engine-internals.md %}) page for details on the LSP protocol, the language IDs, and the workspace configuration the server expects.
+ProofFrog ships a plugin for Visual Studio Code that provides rich editing support for FrogLang files. A plugin is also available for JetBrains IDEs. Any editor that supports the Language Server Protocol can be connected to ProofFrog's bundled LSP server; see the [Engine Internals]({% link researchers/engine-internals.md %}) page for details.
 
 - TOC
 {:toc}
@@ -19,21 +19,7 @@ ProofFrog ships a plugin for Visual Studio Code that provides rich editing suppo
 
 ### Installation
 
-The extension is not currently published on the VSCode Marketplace. It ships as a `.vsix` package that you install manually.
-
-**From a pre-built package.** If you have a `.vsix` file (distributed separately or built by a colleague), install it from within VSCode: open the Extensions view, click the `...` menu in its header, and choose "Install from VSIX...". Select the `.vsix` file and reload the window when prompted.
-
-**Building from source.** From the repository root, run:
-
-```bash
-# Compile the extension
-make vscode-extension
-
-# Package as .vsix
-make vscode-vsix
-```
-
-Then install the resulting `.vsix` via the Extensions view as described above.
+The extension is available on the [VSCode Marketplace](https://marketplace.visualstudio.com/items?itemName=ProofFrog.prooffrog). To install it, open the Extensions view in VSCode, search for "ProofFrog", and click Install.
 
 **Requirements.** The extension requires VSCode 1.85 or later and Python 3.11 or later with ProofFrog installed in the Python environment it uses. By default the extension looks for `python3` on your PATH. If you use a virtual environment, set the `prooffrog.pythonPath` setting to the full path of that environment's interpreter:
 
@@ -49,29 +35,25 @@ See [Installation]({% link manual/installation.md %}) for instructions on settin
 
 ### Features
 
-The features described below are implemented in the LSP server (`proof_frog/lsp/`) and surfaced through the VSCode extension client.
-
-**Syntax highlighting.** The extension registers a single language ID (`prooffrog`, also aliased as `ProofFrog` and `FrogLang`) for all four FrogLang file extensions: `.primitive`, `.scheme`, `.game`, and `.proof`. A TextMate grammar provides token-based highlighting for keywords, types, literals, comments, and import paths.
-
-**Diagnostics.** Parse errors are reported as squiggle underlines on every keystroke, without waiting for a save. On save, the server runs semantic analysis (type checking) and reports any type errors inline. For `.proof` files, saving also triggers full proof verification: each game hop is checked, and failed hops appear as error diagnostics on the relevant line in the `games:` list. All diagnostics come from `proof_frog/lsp/diagnostics.py` and `proof_frog/lsp/proof_features.py`.
+**Syntax highlighting.** Provides highlighting for all four FrogLang file extensions (`.primitive`, `.scheme`, `.game`, and `.proof`), covering keywords, types, literals, comments, and import paths.
 
-**Go-to-definition.** Pressing F12 (or Cmd/Ctrl+click) on an import path navigates to the imported file. On a dotted name such as `E.KeyGen`, the extension jumps to the declaration of that field or method within the imported file. Implemented in `proof_frog/lsp/navigation.py`.
+**Diagnostics.** Parse errors are reported as squiggle underlines on every keystroke. On save, the extension runs type checking and reports any type errors inline. For `.proof` files, saving also triggers full proof verification: each game hop is checked, and failed hops appear as error diagnostics on the relevant line in the `games:` list.
 
-**Hover information.** Hovering over an import name or a dotted member reference shows a Markdown popup with the interface description for that primitive, scheme, or game, or the signature of the specific method. Implemented in `proof_frog/lsp/navigation.py`.
+**Go-to-definition.** Pressing F12 (or Cmd/Ctrl+click) on an import path navigates to the imported file. On a dotted name such as `E.KeyGen`, the extension jumps to the declaration of that field or method within the imported file.
 
-**Outline panel and document symbols.** The Explorer Outline panel is populated with the structural elements of the active file: the primitive or scheme name with its fields and methods, game or reduction definitions with their oracle methods, the `theorem:` declaration in a proof file, and the `games:` list with each step as a child entry. This uses `proof_frog/lsp/symbols.py`.
+**Hover information.** Hovering over an import name or a dotted member reference shows a popup with the interface description for that primitive, scheme, or game, or the signature of the specific method.
 
-**Code folding.** Method bodies, game and reduction bodies, and the `games:` list in a proof file can be collapsed with the standard fold controls. Blocks of three or more consecutive comment lines are also foldable as a comment region. Implemented in `proof_frog/lsp/folding.py`.
+**Outline panel.** The Explorer Outline panel shows the structural elements of the active file: primitive or scheme names with their fields and methods, game or reduction definitions with their oracle methods, the `theorem:` declaration in a proof file, and the `games:` list with each step as a child entry.
 
-**Rename (F2).** Pressing F2 on an identifier renames all whole-word occurrences of that identifier throughout the current file, skipping occurrences inside comments and string literals. Language keywords and built-in type names (`Initialize`, `Finalize`, `BitString`, etc.) cannot be renamed. Implemented in `proof_frog/lsp/rename.py`.
+**Code folding.** Method bodies, game and reduction bodies, and the `games:` list in a proof file can be collapsed. Blocks of three or more consecutive comment lines are also foldable.
 
-**Completion and signature help.** The extension provides two forms of IntelliSense. Keyword completion offers context-sensitive keywords for each file type (different sets for `.primitive`, `.scheme`, `.game`, and `.proof` files). Member completion triggers after a dot (`.`) and lists the fields and methods of the named import or `let:` binding. Signature help appears when you open a parenthesis on a method call and highlights the active parameter as you type commas. Completion also resolves `let:` bindings in proof files so that aliases like `E2.KeyGen` are completed correctly. Implemented in `proof_frog/lsp/completion.py`.
+**Rename (F2).** Renames all whole-word occurrences of an identifier throughout the current file, skipping occurrences inside comments and string literals. Language keywords and built-in type names cannot be renamed.
 
-**Code lens for proof hops.** In `.proof` files, after a save triggers proof verification, each line in the `games:` list receives an inline annotation showing whether that hop passed (`interchangeability`), failed (`interchangeability -- FAILED`), or was an assumption hop (`assumption`). Failed hops are also reported as error diagnostics. Implemented in `proof_frog/lsp/proof_features.py`.
+**Completion and signature help.** Context-sensitive keyword completion offers different keyword sets for each file type. Member completion triggers after a dot (`.`) and lists the fields and methods of the named import or `let:` binding. Signature help appears when you open a parenthesis on a method call and highlights the active parameter as you type commas.
 
-**Proof hops tree view.** When a `.proof` file is active, a "ProofFrog: Proof Hops" panel appears in the Explorer sidebar. It lists every game hop with its pass/fail status and the descriptions of the two games being compared. Clicking an entry navigates to the corresponding line in the proof file. This view is updated automatically each time proof verification completes. Implemented in `proof_frog/lsp/proof_features.py` (server side) and `vscode-extension/src/proof_tree.ts` (client side).
+**Code lens for proof hops.** In `.proof` files, after a save triggers proof verification, each line in the `games:` list receives an inline annotation showing whether that hop passed, failed, or was an assumption hop. Failed hops are also reported as error diagnostics.
 
-<!-- TODO screenshot: VSCode showing a proof file with hop status code lens -->
+**Proof hops tree view.** When a `.proof` file is active, a "ProofFrog: Proof Hops" panel appears in the Explorer sidebar. It lists every game hop with its pass/fail status and the descriptions of the two games being compared. Clicking an entry navigates to the corresponding line in the proof file.
 
 ---