Prover Studio

This Visual Studio Code extension provides support for using PiSPEC, LCF, HLL and sHLL languages, but also the RJSON format. It is developed by Prover.

Features

• Syntax highlighting of PiSPEC, LCF, HLL and sHLL files
• Syntax highlighting RJSON files. RJSON, for Relaxed JSON, is a format intended as a generic data specification format. RJSON is both a super-set of the JavaScript Object Notation (JSON), and a subset of the “YAML Ain’t Markup Language” (YAML) format.
• Reports syntax errors

• Reports semantic errors (such as references to unknown functions)

• Provides "Go to definition", "Find references", and document outlines.

• Helps with creating Prover iLock package bundles (.pipkgs files) out of the packages in the workspace and their dependencies, by providing a 'Make package bundle' command. Access it via the command palette (Ctrl+Shift+P). This command is only availble on Windows.

• Manages Prover Studio projects for HLL and sHLL: creation of projects, adding and removing files, selecting the active project, etc. Access projected related commands via the command palette or with the file explorer context menu.

Requirements

To use the Windows version of this extension, you need .NET framework 4.7.2 or later installed on your machine.

Setting up your workspace

The following doesn't apply if you are using HLL and/or sHLL only.

Prover Studio will look through your workspace for any package directories (directories containing a "package.xml" file) and project directories (directories containing ".isy" files). Make sure to add these folders to your workspace to make Prover Studio recognize them.

For project directories, only files in the "config" directory will be considered by the extension. Files outside the "config" directory are not picked up (unless explicitly opened in VS code).

Multi-file projects for HLL and sHLL

Use a Prover Studio project file to create multi-file models (for HLL and sHLL):

• Open in VS Code a folder containing all the files needed in your project.
• Create a Prover Studio project using the "New Prover Studio project" command accessible from the command palette (Ctrl+Shift+P). You will need to choose a name for the project and some files belonging to the project.
• You can add or remove files to the project using the commands "Add file to Prover Studio project" and "Remove file from Prover Studio project" accessible from the command palette or with a right click on the file of your choice in the VS code file explorer. It is also possible to select multiple files in the explorer and add all of them with one command (accessible with a right click on any of the selected files). All the files from a subdirectory can also be added or removed with "Add/Remove contained HLL/sHLL files to Prover Studio project".
• All the files of the project must be in the opened folder or a subdirectory. The "Go to definition" and "Go to declaration" commands will search in all the project files, and the semantic checks will be performed on the project as a whole.
• The project specifications are stored in a file named <project_name>.psprj that is automatically edited by Prover Studio.

Several Prover Studio projects in the same folder, and active project:

• You may create several projects in the same folder. For that you have to follow the same steps as mentioned in the previous paragraph.
• If a file belongs to several projects, it will be considered as part of the "active project" which can be changed with the "Change active Prover Studio project" command, which is also accessible with a right click on the project file in the file explorer.
• In the file explorer, the files of the active project are green, and the files that belong to no project are in light grey.

If an error is found in the project, the project file will be red in the explorer. Open it to see the details and fix the problem.

Semantic checks for HLL

Semantic checks for HLL rely on Prover Expander 1 which is distributed with Prover Certifier. Make sure you have it installed with a valid license. Then go to the extensions settings and:

• Specify the path to Prover Expander 1 binary in "Hll Semantic Checks: Prover Expander1 Path"
• Specify the path to the license in "Hll Semantic Checks: Prover License Path"
• For Windows, specify the path to cygwin bash.exe in "Hll Semantic Checks: Cygwin Bash Path"
• Enable "Hll Semantics Checks"

Once everything is set up properly, semantic errors will appear in the editor, including for properly configured multi-file projects (see above). In the current version, sHLL is not covered.

Reachability Obligations

Prover Studio has rudimentary support for Reachability Obligations for now. This means that the syntax checks are performed, but for the semantic checks it requires Prover Expander 1 version 3.3 or later. For earlier versions of Prover Expander 1, it is recommended to isolate all Reachability Obligations into a separate file, as Prover Expander 1 will stop at the first syntax error.

Extension Settings

You can configure regular expressions to use for filtering warnings produced by Prover Studio. If used, we recommend configuring these filters on the workspace level. Go to "Settings" in Visual Studio code, select the "Workspace" tab, and search for "Prover Studio" to list all available settings.

Known Issues

No known issues, but see Release notes.

References

Prover Studio demo (HLL features)