Getting started
Installation requires opam. Please refer to this page for opam installation instructions.
Once opam installed:
$ opam install archetype
current archetype version: 1.2.0
Please refer to this page to download and install VS code.
Install through VS Code extensions. Search for archetype:
Visual Studio Code Marketplace: archetype
Can also be installed with VS Code Quick Open: press Cmd/Ctrl + P, paste the following command, and press enter.
ext install edukera.archetype
The vscode extension is configured via the normal vscode settings screen.
Make sure that VS Code inherits from opam's environement variables, so that archetype command is known.
For example on MacOS, insert eval $(opam env) in the shell profile file (.bash_profile or .zshrc) and launch VS code from Terminal with open -a Visual \Studio \Code (or an alias).
Archetype generates Why3 file format (mlw) for contract verification purpose.
The current version of why3 is 1.3.3. It is installed with opam:
$ opam install why3
You also need to install the Why3 IDE (interface) (currently 1.3.3):
$ opam install why3-ide
The IDE uses GTK library that may need to be installed with the proper system-dependent package management system (apt for linux, brew for mac os, ...).
Visit the official Why3 website for more information.
Why3 itself generates contracts' proof obligations and transcodes them to several SMT solvers languages.
Each solver needs to be installed separately. Once the solvers are installed (see below), they need to be detected by Why3 with the following command:
$ why3 config --detect-provers
Alt-ergo is developed by LRI, where Why3 also comes from. The currently supported version is 2.3.1.
$ opam install alt-ergo.2.3.1
CVC4 is developed at Stanford. The currently supported version is 1.7. Download the binary at the following page:
Z3 is developped by Microsoft. The currently supported version is 4.7.1. Download the binary at the following page:
