Why3 Installation and Editor Support

There are several options for installing Why3 on your system. Instructions for each are detailed below.

It is strongly recommended that you try the Docker alternative first. The Docker option is the most easily compatible with the largest variety of systems and configurations, and is the most likely to work for you. If you have the Docker alternative working, and want to explore the other options, then you can do so. However, if you encounter issues with the other options and you have a working Docker setup, then we will not be able to provide support for the other options.

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 mattfredrikson/why3:s25
  3. Give the image a shorter tag: 
    
docker tag mattfredrikson/why3:s25 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. You can also run Why3 commands from the command line. For example, to run the prover foo.mlw, you can run: 
    
docker run --rm --volume /home/student:/data --workdir /data why3 prove foo.mlw
  7. Strongly recommended: Make a shell script to simplify this invocation 
    
#!/bin/bash
docker run --rm -p 8080:8080 --env WHY3IDE=web --volume /home/student:/data --workdir /data why3 "$@"
    Save this script as why3.sh, and make it executable with chmod +x why3.sh. Then you can run ./why3.sh ide foo.mlw to start the Why3 IDE, or ./why3.sh prove foo.mlw to run the prover.
  8. Notes:
    • When using the IDE, in order to stop 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.
    • If you are using a Mac, you might get a warning about the image's platform not matching the detected host platform. You can safely ignore this warning.


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 libgnomecanvas autoconf
  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 why3 why3-ide alt-ergo.2.6.0
  5. Install Z3: 
    
brew tap stonebuddha/formulae; brew install z3@4.10.2
  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.6.0, Z3 4.10.2, 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.6.0
  5. Install Z3: 
    
wget https://github.com/Z3Prover/z3/releases/download/z3-4.10.2/z3-4.10.2-x64-glibc-2.31.zip
unzip z3-4.10.2-x64-glibc-2.31.zip
sudo cp z3-4.10.2-x64-glibc-2.31/bin/z3 /usr/local/bin
sudo chmod +x /usr/local/bin/z3
  6. Install CVC4: 
    
wget https://github.com/CVC4/CVC4-archived/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.6.0, Z3 4.10.2, 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: