Why3 Installation and Editor Support

Why3 installation guide

There are several options for installing Why3 on your system. Instructions for each are detailed below. If you encounter difficulties when attempting to install locally or use the Docker image, we recommend that you just use the virtual appliance.

Docker

If you already have Docker installed on your machine, or are familiar with how to use it, then this is likely the most straightforward way to get Why3 up and running.

  1. If you do not already have Docker installed, then follow the instructions on the Docker site for your platform.

  2. Pull the Why3 Docker image:
    
docker pull mfredrik/15414:why3-s22
  3. Give the image a shorter tag: 
    
docker tag mfredrik/15414:why3-s22 why3
  4. You can now run Why3 inside the docker image, and connect to its graphical interface through your web browser.
    Assuming your home directory is in /home/student, and there is a source file foo.mlw in that directory that you would like to work on, then you will run the command: 
    
docker run --rm -p 8080:8080 --env WHY3IDE=web --volume /home/student:/data --workdir /data why3 ide foo.mlw
  5. Open a new browser window, and connect to http://localhost:8080.
  6. Note that in order to stop this docker container, the best way is to use the File/Quit menu within the Why3 IDE. Once you have responded to the save prompt, this will cause the container to stop running on your system.
  7. Note that if you are using a ARM-based Mac, you might get a warning about the image's platform not matching the detected host platform. You can safely ignore this warning.


Virtual Machine

For those who are not familiar with Docker, it may be simpler to use the virtual appliance created by the course staff.

  1. Install the latest version of Oracle VirtualBox.
  2. Download the Why3 virtual appliance.
  3. Launch VirtualBox, navigate to Files/Import Appliance, and select the virtual appliance that you downloaded.
  4. Start the virtual machine. You may want to create a shared folder with the home directory on your host machine, so that you can easily access your work. You can do so by navigating to Settings/Shared Folders in the VirtualBox UI.
The password for the default account on the virtual appliance is a single space character.


macOS

If any of these instructions fail because your operating system is unable to support the recommended versions, we suggest that you follow the VM or Docker setup instructions above instead.

  1. Install the Homebrew package manager.

  2. Install opam and libraries for Why3: 
    
brew install hg darcs opam gtk+ gmp gtksourceview3 autoconf
    Note: we used to install libgnomecanvas but this is no longer supported.

  3. Initialize opam, and answer yes if queried: 
    
opam init; eval $(opam config env)
  4. Install Why3 and Alt-Ergo: 
    
opam install zarith lablgtk3 lablgtk3-sourceview3 frama-c why3 why3-ide alt-ergo.2.4.0
    Note: Even though installing frama-c is overkill, it will make the IDE work for Why3 since libgnomecanvas is no longer supported.

  5. Install Z3: 
    
brew tap stonebuddha/formulae; brew install z3@4.8.6
  6. Install CVC4: 
    
brew tap cvc4/cvc4; brew install cvc4/cvc4/cvc4
  7. For ARM-based Macs, if you get an error saying "The x86_64 architecture is required for this software":
    1. Click “Get Info” for the iTerm application and select “Open using Rosetta”. (If you use Terminal, you should be able to find something similar)
    2. If you try installing cvc4, now it might say "Cannot install under Rosetta 2 in ARM default prefix (/opt/homebrew)!" If so, install Homebrew into /usr/local. In my case I just had to add export PATH=/usr/local/Homebrew/bin:$PATH to my .zshrc file.
    3. Now installing cvc4 should work.
  8. Set up Why3 to detect all of the installed provers: 
    
why3 config detect
  9. Make sure that the output of the previous step reflects that Why3 detected Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8.


Ubuntu

These instructions are written assuming a recent version of Ubuntu (at least 18.04), or similar distribution. If you use something else, or these instructions do not work for you, then we recommend that you use either the Docker image or virtual appliance.

  1. Install opam and libraries for Why3: 
    
sudo add-apt-repository ppa:avsm/ppa
sudo apt update
sudo apt-get install build-essential autoconf m4 make opam
  2. Initialize opam, and answer yes if queried: 
    
opam init; eval $(opam config env)
  3. Install required dependencies: 
    
sudo apt-get install libgmp-dev libgtksourceview2.0-dev
  4. Install Why3 and Alt-Ergo: 
    
opam install why3 why3-ide alt-ergo.2.4.0
  5. Install Z3: 
    
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-ubuntu-16.04.zip
unzip z3-4.8.6-x64-ubuntu-16.04.zip
sudo cp z3-4.8.6-x64-ubuntu-16.04/bin/z3 /usr/local/bin
sudo chmod +x /usr/local/bin/z3
  6. Install CVC4: 
    
wget https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
sudo cp cvc4-1.8-x86_64-linux-opt /usr/local/bin/cvc4
sudo chmod +x /usr/local/bin/cvc4
  7. Set up Why3 to detect all of the installed provers: 
    
why3 config detect
  8. Make sure that the output of the previous step reflects that Why3 detected Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8.


WSL2 on Windows 11

If you are using Windows 11 and do not want to use Docker, you may install Why3 on the Windows Subsystem for Linux.

  1. Install WSL2 Microsoft Support Page
  2. Install Ubuntu on WSL2 Ubuntu WSL Page
  3. Enable GUI applications to run on your Ubuntu installation Microsoft Support Page
    Note: If you are not running Windows 11 Build 22000 or higher, the above method may not work for you. An alternative is to run an X11 (X11 Wikipedia) server on windows, and connect your Ubuntu installation to this server. Instructions for this can be found here: Stackoverflow Post You will want to install the VcXsrv Windows X Server: Download
  4. Once you have GUI applications working on your WSL2 Ubuntu installation, you can follow the steps above for Ubuntu.


Text editors with support for WhyML

The following text editors provide WhyML extensions, including syntax highlighting: