EasyCrypt VS Code Extension

EasyCrypt language support for Visual Studio Code: syntax highlighting, diagnostics via the easycrypt CLI, and interactive proof development with proof-state navigation.

Features

• Syntax highlighting for EasyCrypt (.ec, .eca).
• Diagnostics / squiggles by running EasyCrypt and parsing its output.
  • Manual check via command.
  • Optional live checks on change/save.
• Interactive proof navigation backed by a selectable communication channel:
  • emacs channel (default): EasyCrypt cli -emacs process.
  • lsp channel: EasyCrypt LSP server with custom proof/query requests.
  • auto channel: compatibility-based selection.
  • Step forward/backward through statements.
  • Jump to cursor.
  • Reset proof state.
• Proof State view (Explorer panel) that shows goals/messages/output and includes navigation buttons.
• Status bar indicator for quick “check file” access.
• Verbose logging to the “EasyCrypt” Output channel (optional).

Requirements

• EasyCrypt installed locally.
• The easycrypt executable must be available on your PATH, or configured explicitly via easycrypt.executablePath.

Getting Started

1. Install EasyCrypt.
2. Open an EasyCrypt file (.ec/.eca) in VS Code.
3. Run “EasyCrypt: Check File” from the Command Palette.
4. (Optional) Open the Proof State view in the Explorer to step through proofs.

Commands

From the Command Palette:

• EasyCrypt: Check File (easycrypt.checkFile)
• EasyCrypt: Start/Restart Process (easycrypt.startProcess) - starts/restarts current runtime (process or LSP client)
• EasyCrypt: Stop Process (easycrypt.stopProcess) - stops current runtime (process or LSP client)
• EasyCrypt: Clear All Diagnostics (easycrypt.clearAllDiagnostics)
• EasyCrypt: Clear File Diagnostics (easycrypt.clearFileDiagnostics)
• EasyCrypt: Show Diagnostic Count (easycrypt.showDiagnosticCount)
• EasyCrypt: Step Forward (easycrypt.stepForward)
• EasyCrypt: Step Backward (easycrypt.stepBackward)
• EasyCrypt: Go to Cursor (easycrypt.goToCursor)
• EasyCrypt: Reset Proof State (easycrypt.resetProof)
• EasyCrypt: Force Recovery (Fix Desync) (easycrypt.forceRecovery)
• EasyCrypt: Toggle Verbose Logging (easycrypt.toggleVerboseLogging)

Keybindings

The extension provides navigation keybindings when editing EasyCrypt files, controlled by easycrypt.keybindings.profile:

• default
  • Step Forward: Alt+Down
  • Step Backward: Alt+Up
  • Go to Cursor: Alt+Right
  • Reset Proof State: Alt+Left
• proof-general
  • Step Forward: Ctrl+Alt+Down (macOS: Ctrl+Down)
  • Step Backward: Ctrl+Alt+Up (macOS: Ctrl+Up)
  • Go to Cursor: Ctrl+Alt+Right (macOS: Ctrl+Right)
  • Reset Proof State: Ctrl+Alt+Left (macOS: Ctrl+Left)
• none
  • No keybindings are contributed by the extension.

Additionally:

• Check File: Ctrl+Shift+C (macOS: Cmd+Shift+C)

Configuration

Settings (see VS Code Settings UI under “EasyCrypt”):

• easycrypt.keybindings.profile: default | proof-general | none
• easycrypt.executablePath: path to the EasyCrypt binary (default: easycrypt)
• easycrypt.arguments: additional CLI args passed to EasyCrypt on startup
• easycrypt.proverArgs: args for backend provers (passed through EasyCrypt)

Communication channels:

• easycrypt.communication.channel: emacs | lsp | auto (default: emacs)

LSP options:

• easycrypt.lsp.serverArgs: additional args for easycrypt lsp
• easycrypt.lsp.trace.server: off | messages | verbose
• easycrypt.lsp.requestTimeoutMs: timeout for proof/query requests
• easycrypt.lsp.logToFile: sets EASYCRYPT_LSP_LOG=1 for server logging

Diagnostics:

• easycrypt.diagnostics.enabled: enable/disable diagnostics
• easycrypt.diagnostics.liveChecks: enable/disable live checks
• easycrypt.diagnostics.delay: debounce delay (ms) for live checks
• easycrypt.diagnostics.onChange: run checks when text changes
• easycrypt.diagnostics.onSave: run checks on save

Logging / debug:

• easycrypt.verboseLogging: enable verbose logging to the “EasyCrypt” Output channel
• easycrypt.proofStateView.debug.showEmacsPromptMarker: show the EasyCrypt -emacs prompt marker in the Proof State view

Channel Notes

• emacs remains the baseline/default for maximum context parity.
• lsp is supported for interactive proof commands and queries through custom RPC methods.
• auto prefers LSP only when context is compatible; otherwise it selects emacs.
• For context-sensitive setups (custom include/prover args), emacs is usually the safest choice.

Troubleshooting

• “EasyCrypt executable not found”
  • Set easycrypt.executablePath to the full path of your easycrypt binary.
  • Or ensure easycrypt is on your PATH and restart VS Code.
• Desynchronized proof state
  • Run “EasyCrypt: Force Recovery (Fix Desync)”.
  • If needed, run “EasyCrypt: Reset Proof State”.
• Where are logs?
  • Open View → Output and select EasyCrypt.
  • Enable verbose logs with “EasyCrypt: Toggle Verbose Logging”.

Development

Prereqs: Node.js 24 + npm.

If you use nvm:

• nvm install

• nvm use

• Install dependencies: npm install

• Compile: npm run compile

• Watch: npm run watch

• Lint: npm run lint

Running the extension locally

• Open this repo in VS Code.
• Press F5 to launch an Extension Development Host.
• Open a .ec file in the dev host to activate the extension.

Tests

• Unit tests: npm test
• E2E tests: npm run test:e2e

License

GPL-3.0. See LICENSE.