Editor support

The DSRV language has editor support for Visual Studio Code, provided by two separate components:

• the robosapiens-trustworthiness-checker-vscode extension, which supplies syntax highlighting, the .dsrv file association, and commands for running a model;
• the dsrv-lsp language server, which supplies completion and diagnostics over the Language Server Protocol.

The language server links the Trustworthiness Checker (TC) as a library and reuses its parser and type checker, so editor diagnostics come from the same language definition the TC evaluates, though not necessarily from the same revision of it. See When diagnostics and runs disagree.

Both executables ship inside the extension. Installing it is the whole setup; nothing has to be built first.

What the extension provides

Install the extension

Search for RoboSAPIENS Trustworthiness Checker in the Extensions view (Ctrl+Shift+X) and install it.

The extension contains the binaries for every supported platform and uses the ones matching your machine.

To install it from a file instead, take robosapiens-trustworthiness-checker-vscode.vsix from the releases and run:

code --install-extension robosapiens-trustworthiness-checker-vscode.vsix

Bundled binaries

The extension contains a dsrv-lsp and a trustworthiness_checker for each of these platforms, and uses the pair matching the machine it runs on.

Completion, diagnostics and running a model all work on a fresh install on those platforms.

Each release pins the exact version of each executable it ships, rather than tracking the latest; bundled-binaries.json in the extension's repository records which ones a given version contains.

Using your own build

Set either path setting and the extension uses your executable instead of the bundled one.

Each accepts the executable itself, a directory containing it, or a bare command name to resolve from PATH. Given a Cargo checkout it also looks in target/release and target/debug, so pointing the setting at the repository root is enough.

The extension looks at the setting first, then at the bundled binary, then at PATH. An empty setting, the default, means the bundled binary is used.

To build the executables yourself, see Getting started for the checker, and build in release mode from the repository root:

cargo build --release --package trustworthiness_checker

The executable is written to target/release/trustworthiness_checker. Build the language server the same way from a dsrv-lsp checkout, which writes target/release/dsrv-lsp.

Run a model from the editor

Open a .dsrv file and press the run button in the editor bar.

The command invoked is:

<trustworthiness_checker> <model.dsrv> --input-file <input> \
    --language dsrv [--semantics <semantics>] [--runtime <runtime>] \
    --output-stdout

The run appears in its own terminal as a VS Code task, which echoes that command line at the top.

Choosing semantics and a runtime

While a .dsrv file is open, the status bar shows which semantics a run will use. Click it to change the setting.

Both are empty by default, which means running from the editor is the same command as running from a shell. The status bar shows DSRV: checker default in that case, because the default belongs to the checker and the extension does not restate it.

Semantics

The checker accepts further semantics that target MLTL and STL; the extension does not offer them, because it supports DSRV only. See the CLI reference for the full set.

Runtimes

causal only runs on the semi-synchronous runtime, so selecting it makes the extension pass --runtime semi-sync whatever DSRV.runtime says. The status bar shows this as DSRV: causal · semi-sync, and the echoed command line shows the flag.

Troubleshooting

No completion or diagnostics. The language server did not start. Check the DSRV output channel (View -> Output, then select DSRV). A message of the form Failed to start dsrv-lsp: spawn dsrv-lsp ENOENT means the executable was not found, which on a default installation should not happen. Check whether DSRV.lspPath is set and points somewhere that no longer exists. Clearing it falls back to the bundled server.

Setting dsrv-lsp.trace.server to verbose logs the traffic between the editor and the server in the same output channel.

A run reports that the checker could not be found. The same applies to DSRV.binaryPath: clear it to go back to the bundled checker. The error message offers to locate the executable for you, which writes the path into the setting.

A run exits immediately with a usage error. Read the echoed command line in the terminal. A --semantics or --runtime value edited by hand in settings.json may not be one your checker accepts; the extension's dropdowns only offer values that work with the bundled one.

Diagnostics disagree with what a run accepts. The two bundled executables contain copies of the DSRV front end built from different revisions of the checker, so in edge cases around typing they can disagree: the editor may not flag something a run rejects, or the other way round. When they disagree, the run is the authority.

If you build both yourself, rebuild dsrv-lsp against the checker revision you are running and the two agree. With the bundled binaries there is nothing to adjust; closing this gap is the next piece of work on the language server.