WaterproofThe Waterproof vscode extension helps students learn how to write mathematical proofs. Quick install instructions for Windows and MacInstall this extension and follow the installation instructions that pop up. More extensive installation instructionsInstallation on WindowsStep 1: Dependencies installerDownload and execute the bundled installer Step 2: Install the vscode extensionInstall this Waterproof vscode extension Step 3: Update the settings for WaterproofWithin vscode, go to the Extensions tab (Ctrl+Shift+X) and search for the installed Waterproof extension. Once the extension is found, click on the gear icon and enter the 'Extension Settings'. Within the setting 'Waterproof: Path' enter the following line:
Note: This will only work if you have not changed the default installation for the dependencies. In the case that a different file location was used for the installation, find the location of '.opam\wp\bin\coq-lsp' within this folder. Paste instead the absolute file address of this coq-lsp file into the 'Waterproof: Path' setting. Installation on Windows with WSLIf the above method did not work for Windows, it is possible to instead install the dependencies and run the Waterproof vscode extension using WSL Step 0: Install WSLFor the Waterproof extension to work on Windows, one needs to use WSL. If WSL is not yet set up on your Windows computer, open a Powershell window and run it as administrator (for instance by clicking on the magnifying glass, typing "Powershell", right clicking the Powershell app and pressing "Run as administrator"). In the Powershell window that appears, execute
This will specifically install the Ubuntu distribution If necessary, you can find more information about WSL and how to install it here. If this is your first time installing WSL and the Ubuntu Distribution you need to set up a username and password to use later. After setting this up, you will need to update the package lists on the system. To do this execute the following line:
(Press enter to accept all requests) Step 1: Install the coq-lsp and coq-waterproof pluginsWithin a WSL distribution, execute the following lines:
The last two lines may take a while to install (Press enter to accept all requests or 'y' to accept them one-by-one) Step 2: Install the WSL vscode extensionStep 3: Connect to WSL from vscodePress Alternatively, one navigate to a folder in WSL itself, and type Step 4: Install this Waterproof vscode extensionFrom this page in vscode, you can just click on the "Install" button. Installation on LinuxStep 1: Install this Waterproof vscode extensionStep 2: Install the coq-lsp and coq-waterproof pluginsIn a terminal, execute the following lines
Installation on MacStep 1: Dependencies installerDownload and execute the bundled installer Open the Step 2: Install the vscode extensionInstall this Waterproof vscode extension Step 3: Update the path settings for WaterproofWithin vscode, go to the Extensions tab (Shift+Command+X) and search for the installed Waterproof extension. Once the extension is found, click on the gear icon and enter the
Step 4: Update the args settings for WaterproofStill in the 'Extension Settings' within the setting
You may have to restart vscode before these settings are implemented. WarningUpon opening a .mv file for the first time, a pop-up about verifying the developer may appear. To fix this issue, click 'Show in Finder', Control click on the Coq-Platform application and press open. Click 'open' again if a pop-up appears. You may close the application once it has opened. This will ensure that the application is now trusted when using the Waterproof extension in the future. Manual Installation on MacIf the above method did not work for Mac, it is possible to instead install the dependencies manually using opam. Step 1: Install this Waterproof vscode extensionStep 2: Install the coq-lsp and coq-waterproof pluginsIf you use homebrew, first install opam by executing the following lines in a terminal
If you prefer MacPorts, instead run
Then execute
|