vscode-motoko
vscode-motoko copied to clipboard
Draft: Fix minor issues to enable Serokell to use the IDE for local testing
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:
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.:
cp /nix/store/x7amwi31gzavs8r7q89ljwwaksg5kqzw-moc.js ../vscode-motoko/generated/moc.js
- Open the workspace in VS Code (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.: