The plugin executes .pvl by converting them into valid .pv files (simply appending process 0.)

However, when the .pvl file uses a diff, this does not work. The process would need to include a diff, too.

The ProVerif invocation is not escaped; leading to errors if the involved files have a space in their path.

Ensure the project can run independent from a single maintainer (me). This includes:

• Document main architecture
• Ensure multiple people have direct release access (wait for #11 to finish)
• Automate processes as much as possible (#13)

OCaml supports doccomments, which could be added here too.

For example:

(** Generation of fresh Diffie-Hellman keys. Returns a pair (kpriv,kpub) *)
letfun DHKeygen() =
new s:scalar;
(s,dh(s,G))
.

Expectation of what vscode then should display:

Automate publishing to ease publishing an update for contributors.

Resources:

• https://code.visualstudio.com/api/working-with-extensions/bundling-extension
• https://github.com/xdebug/vscode-php-debug

Webpack can be added to minify the bundle, promising a speed up: https://code.visualstudio.com/api/working-with-extensions/bundling-extension

Ensure ProVerif warnings (e.g. variable overriden) shown as warnings in the IDE (and not errors)

Some invocations launch ProVerif which runs for a long time in the background. While invocations should be terminated automatically after at most one second, this seems to be not always the case.