-
Notifications
You must be signed in to change notification settings - Fork 16
Expand file tree
/
Copy pathCHANGELOG
More file actions
18 lines (17 loc) · 2.14 KB
/
Copy pathCHANGELOG
File metadata and controls
18 lines (17 loc) · 2.14 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
## ChangeLog
### 1.0.66 (2025.05.23)
First public release of vscode-pvs-8 for PVS version 8.
- Syntax highlighting: PVS keywords and library functions are automatically highlighted.
- Autocompletion and code snippets: Tooltips suggesting function names and language keywords are automatically presented in the editor when placing the mouse over a symbol name. Code snippets are provided for frequent modeling blocks, e.g., if-then-else.
- Hover information for symbol definitions: Hover boxes providing information about identifiers are automatically displayed when the user places the cursor over an identifier.
- Go-to definition: Click on the name of the identifier while holding down the Ctrl key to jump to the location where the identifier is declared.
- Peek definitions: Symbol definitions can be shown in mini editors embedded in the current view.
- Live diagnostics: Parsing is automatically performed in the background, and errors are reported in-line in the editor. Problematic expressions are underlined with red wavy lines. Tooltips presenting the error details are shown when the user places the cursor over the wavy lines.
- Outline View: Interactive tree view showing the outline of the pvs file open in the editor. Point-and-click actions can be used to jump to definitions.
- Workspace Explorer: Interactive tree view showing all theories in the current workspace, name and status of theorems and typecheck conditions.
- Proof Explorer: Interactive tree view for viewing and editing the current proof.
- Prover Console: An integrated terminal for interacting with the theorem prover. Auto-completion is provided (using the TAB key) for prover commands, as well as access to the commands history.
- Evaluator Console: An integrated terminal for evaluating PVS expressions in PVSio.
- Proof Mate: Helper tool, provides functionalities for suggesting proof commands, sketching proof attempts, and repairing broken proofs during interactive proof sessions.
- Prototype Builder: Rapid prototyping toolkit, for building interactive visual simulations based on PVS specifications.
- NASALib search: Search engine for navigating/searching the NASALib and the PVS Prelude Library