When this was first developed, Verus was in an earlier stage, and most Verus codes were self-contained on a single file. Since we are directly using the command from the user's input, the current user interface is wrong for non-trivial projects with more than one file.
Now, when hitting the save button, this custom rust-analyzer uses --verify-module for non-root files, and --verify-root for root files.
For example, to run Verus on ironsht/src/environment_t.rs, we now run path_to/rust-verify.sh ironsht/src/main.rs --verify-module environment_t.
When this was first developed, Verus was in an earlier stage, and most Verus codes were self-contained on a single file. Since we are directly using the command from the user's input, the current user interface is wrong for non-trivial projects with more than one file.
Now, when hitting the save button, this custom rust-analyzer uses
--verify-modulefor non-root files, and--verify-rootfor root files.For example, to run Verus on
ironsht/src/environment_t.rs, we now runpath_to/rust-verify.sh ironsht/src/main.rs --verify-module environment_t.