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:
git clone https://github.com/dfinity/vscode-motoko -b arshavir/serokell-ide-quick-fix
cd vscode-motoko
npm install
cd ..
Compile your custom version of the Motoko compiler into JS:
git clone https://github.com/serokell/motoko
cd motoko
nix-build -A js
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.:
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
// @verifyon 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.: