- Rust 84.3%
- Typst 9.2%
- TypeScript 4.8%
- TeX 0.8%
- Coq 0.5%
- Other 0.4%
| Filename | Latest commit message | Latest commit date |
|---|---|---|
| .vscode | ||
| debug-workspace | ||
| examples | ||
| extension | ||
| language-server | ||
| parser | ||
| project-report | ||
| .gitignore | ||
| architecture.excalidraw | ||
| README.md | ||
Imp2Rocq
A Visual Studio Code extension that allows developers to write and verify Imp programs with Rocq without leaving the editor.
Read the report!
Requirements
The extension has been tested with vsrocq-language-server version 2.3.4 with Rocq 9.1.0.
For the language server to run properly vsrocqtop must be installed on the host machine. This is also a requirement for VsRocq to work so you should just follow their requirements.
Imp2Rocq must also know the location of the Software Foundations Volume 2 book on your machine (it must be compiled with make): https://softwarefoundations.cis.upenn.edu/plf-current/index.html.
On startup, Imp2Rocq will prompt you to supply the path to the book on your machine as a VS Code setting.
Also rust/cargo needs to be installed for debugging.
To run
- In VS Code, press
F5to open a new window with the extension enabled. - In the new window, create a file with the
.impextension and write Imp code with contracts. See /debug-workspace for example programs.
If your pre- or postconditions starts having suboptimal squiggly lines, this might be because the vsrocqtop process is tired and you can reload the editor with the command palette command "Developer: Reload Window".
Known issues
- contracts correctly registers multiple keywords on one line, but not on multiple lines
- typing non-ascii characters (æøå) in imp files breaks the extension silently