Skip to content

Latest commit

 

History

History
164 lines (109 loc) · 5.35 KB

BUILDING.md

File metadata and controls

164 lines (109 loc) · 5.35 KB

VLSM Building Guide

This guide describes how to build (check) the code in the VLSM project using the Coq proof assistant. The guide assumes a Unix shell, and some installation commands assume a Debian-like Linux distribution, such as Ubuntu.

Notes for Windows users:

  • On Windows, we strongly recommend using WSL version 2 to install VLSM.
  • Before beginning the VLSM installation process on Windows, you need to make sure that you have WSL installed on your machine and that this is set to version 2. A link providing instructions towards this is available on Microsoft docs and also here (backup link).

Building VLSM manually

Install opam requirements (unless already installed)

A compiler and the unzip and bubblewrap tools are needed by opam.

To install on Debian-based distributions:

sudo apt-get update
sudo apt-get install -y build-essential unzip bubblewrap

To install on Fedora:

sudo dnf install @development-tools unzip bubblewrap

Install opam (unless already installed)

We recommend installing opam via the official install script, which will always install the latest released version:

bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
opam init

As an alternative, the opam package is included in the standard repositories in some Linux distributions. In Fedora, it can be installed by running:

sudo dnf install opam

Initialize opam

Run opam init.

If you encounter the error "Sandboxing is not working on your platform", then disable the sandboxing by choosing "Y".

Choose "y" in order to allow opam to modify ~/.profile.

Install a switch for opam

opam switch create coq-8.18 --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda

Update the current shell environment

eval $(opam env)

Install the project dependencies via opam

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.18.0 coq-stdpp.1.9.0 coq-itauto coq-equations

Clone the project repository

git clone https://github.com/runtimeverification/vlsm

Build the project

cd vlsm
make -j $(nproc)

Building VLSM using the Coq Platform

Download and unpack the Coq Platform scripts

The latest Coq Platform release is always available using this link.

However, for the purposes of demonstration, we will assume the archive is called 2023.11.0.zip.

wget https://github.com/coq/platform/archive/refs/tags/2023.11.0.zip
unzip 2023.11.0.zip

Run the Platform scripts

cd platform-2023.11.0
./coq_platform_make.sh

Activate the Platform switch

The Platform scripts will create a new opam switch, whose name can be viewed by running opam switch. Here, we assume the switch is called __coq-platform.2023.11.0~8.18~2023.11.

opam switch __coq-platform.2023.11.0~8.18~2023.11
eval $(opam env)

Clone the project repository

git clone https://github.com/runtimeverification/vlsm

Build the project

cd vlsm
make -j $(nproc)

Editor instructions

We recommend using the Visual Studio Code (VS Code) editor, which you can download and install from here.

If you are using WSL on Windows, you need to install the VS Code WSL extension. When this extension is installed, click the Connect to WSL button, to open a new editor window in the WSL environment and open the project folder from inside this window.

We recommend also installing the Fast Unicode Math Characters extension, to enable easier input of mathematical symbols.

To enable Coq support in VS Code, there are two main options: the VsCoq extension and the Coq LSP extension. Note that these extensions are restricted to Coq 8.18.0 and later. For earlier versions, you can use the VsCoq Legacy extension.

VsCoq extension

To install the VsCoq extension from the command line, make sure that switch creation and dependency installation are done and then run:

opam install vscoq-language-server && code --install-extension maximedenes.vscoq

Coq LSP extension

To install the Coq LSP extension from the command line, make sure that switch creation and dependency installation are done and then run:

opam install coq-lsp && code --install-extension ejgallego.coq-lsp