Draft: Fix minor issues to enable Serokell to use the IDE for local testing #281
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
How to use this fix:
Make sure you have the "Viper v4.3.1" extension installed in VS Code, and that it has installed its dependencies (this happen via a prompt when you open e.g., an empty Viper file in VS Code with this extension installed). Verifying Viper files should work automatically upon saving .vpr files.
Setup the VS Code extension repo as follows:
This should print something like
/nix/store/x7amwi31gzavs8r7q89ljwwaksg5kqzw-moc.js
(which is a directory). Copy the internal JS file into a place that would be seen by the VS Code extension, e.g.:code .
) and enter a debug session (e.g., hit F5 or click play in the Run and Debug panel of VS Code):In the new window, open a folder (a.k.a. workspace) containing some Motoko-san source files. For example, open "motoko/test/viper/".
Choose one Motoko-san source file, e.g., "reverse.mo", from your workspace.
Ensure that you have
// @verify
on the very first line of the file (this tells the motoko-san extension that it needs to try to verify this file).Upon assertion violation, you should see some interactive feedback from the tool upon saving the file, e.g.: