VS Code recognizes localhost URLs in the terminal and automatically offers to port-forward them for you. All you need to do is run mdbook serve and then click "Open in browser".

A good trick when developing Kani on a remote machine is to SSH forward to test documentation changes.

ssh -t -L 3000:127.0.0.1:3000 kani-host 'cd kani/docs/ && ./mdbook serve'

This command will connect to kani-host where it assumes Kani is checked out in kani/ and the documentation has been built once successfully. It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your local browser when you visit: http://127.0.0.1:3000/

The code in src/tutorial/ is tested with compiletest. This means each file should be buildable independently (i.e. you can run kani on each .rs file). It also means the necessary kani- flag-comments must appear in each file.

To run just these tests, return to the Kani root directory and run:

cargo run -p compiletest --quiet -- --suite kani-docs --mode cargo-kani --quiet