Editor Plugins
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 page for details.
VSCode
Installation
The extension is available on the VSCode Marketplace. 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:
{
"prooffrog.pythonPath": "/path/to/ProofFrog/.venv/bin/python"
}
See Installation for instructions on setting up ProofFrog itself.
Features
Syntax highlighting. Provides highlighting for all four FrogLang file extensions (.primitive, .scheme, .game, and .proof), covering keywords, types, literals, comments, and import paths.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(Future) Emacs
ProofFrog does not yet ship a dedicated Emacs plugin. The LSP server (proof_frog lsp) can be used directly with eglot or lsp-mode for syntax highlighting, diagnostics, and the basic LSP feature set. You would configure the server command as python3 -m proof_frog lsp (or the equivalent path for your environment) and associate it with the .primitive, .scheme, .game, and .proof extensions. See the Engine Internals page for LSP protocol details.
JetBrains
There’s a plugin available for JetBrains IDE-s which provides syntax validation and highlighting, custom color settings, import statement file path references, context-menu actions and other features for the ProofFrog language. You can obtain the plugin from the JetBrains Marketplace inside the IDE. The project is hosted in this GitHub repository.
Adding a new editor
Any editor that supports the Language Server Protocol can be connected to ProofFrog’s LSP server. The server is started with proof_frog lsp (or python3 -m proof_frog lsp) and communicates over stdio using the standard JSON-RPC wire protocol. It uses full document synchronisation (TextDocumentSyncKind.Full). The language ID for all four file types is prooffrog. The server expects the working directory to match the directory from which the proof files are being edited, so that import paths resolve correctly. See the Engine Internals page for a full description of the protocol surface, the supported LSP methods, and the custom notifications (prooffrog/verificationDone, prooffrog/proofSteps) used by the proof hops tree view.