Skip to content

Latest commit

 

History

History
111 lines (91 loc) · 5.52 KB

INSTALL.md

File metadata and controls

111 lines (91 loc) · 5.52 KB
Raw

Getting started

Getting the right setup

This artifact contains an implementation of the Trocq parametricity framework as a plugin for the Coq proof assistant. As such, we offer several possibilities for the reader, according to their level of familiarity with the ecosystem and interest in our work for their own use. All methods were tested on Linux and macOS, we therefore recommend that the reader use one of these operating systems.

Via codespaces (recommended browser setup)

Open codespaces and click "Create codespace".

Via VSCode and Docker (recommended machine setup)

In this set-up, the reader considers this code mainly as the artifact for our paper, and thus wants to check it is working properly. To that end, we propose to interact in an easy way with a Docker container containing our code. The main requirement for the reader is to have Docker and VSCode installed on their machine. The VSCode current user must have permission to run Docker. You also need to ensure you have more than 6GB of disk space available.

The container with all the dependencies is accessible on Dockerhub as cohencyril/trocq-deps and the corresponding Dockerfile is in .devcontainer/Dockerfile in this repo. You could run it manually using docker run -it cohencyril/trocq-deps but you would not be able to run VSCode in the docker terminal, hence the setup described below.

Here are the instructions:

  • Make sure your VSCode has the Dev Containers extension by running code --install-extension ms-vscode-remote.remote-containers or from the menus.
  • Clone or download the repository of the Trocq plugin, e.g. curl -L -O https://github.com/coq-community/trocq/archive/master.zip && unzip master.zip
  • Run VSCode in it (e.g. code trocq-master, or code trocq-ESOP2024 if you are browsing the companion artifact to the paper) and immediately after opening it will suggest to "Reopen in Container", click this (otherwise type F1 and "Reopen in Container").
  • Wait for VSCode to download a 1.28 GB archive that extracts to about 6 GB, on our system this takes about 2 min.
  • Wait for VSCode to compile the code of the plugin, this takes about 30s. The last line of the terminal output should be 
    make[1]: Leaving directory '/workspaces/trocq'
    before you can actually skip to the next section.

Via Nix (recommended only for nix/nixos users)

  1. First install nix https://nixos.org/download
  2. Add the cachix repository coq-community
nix-env -iA cachix -f https://cachix.org/api/v1/install
cachix use coq-community
  1. Clone the current repository and type nix-shell
git clone https://github.com/coq-community/trocq.git
nix-shell
  1. You may also use nix-build to build it and reuse it as a nix package.

Via Opam (recommended only for ocaml/coq/opam users)

  1. Install opam and configure the coq opam repository
  2. Install the custom version of coq-elpi
opam pin add coq-elpi https://github.com/ecranceMERCE/coq-elpi/archive/refs/heads/strat.tar.gz
  1. Build Trocq
git clone https://github.com/coq-community/trocq.git
cd trocq
opam install . --deps-only # to install dependencies
make   # or make -j <number-of-cores-on-your-machine>
  1. You can also run make install to install Trocq on your system.

Exploring the examples with VSCode

After completing the Getting the right setup phase above, the examples folder can be unfolded and the files can be inspected by clicking on them.

When a file is clicked, it is displayed and a Goals tab opens. It shows the state of step-by-step execution of the file by Coq. The main actions related to the Trocq plugin are the Trocq Use commands feeding the database of the plugin, and the trocq tactic actually performing the expected proof transfer step.

One can check that this tactic is working as expected by clicking right before it in the Coq file, waiting for Coq to execute the file until the pointer and update the proof state in the Goals panel, then clicking right after the dot after trocq and waiting for the proof state to be updated with the associated goal generated by Trocq to replace the initial one. The process should be almost instantaneous on all the examples. Please note that on the first time a line is clicked in a file, the proof state can take a few seconds to update.

If you have unexpected errors press "Ctrl-Shift-P" to get the command palette and type Coq LSP: Restart the Coq Language Server and enter to reload the Coq $\leftrightarrow$ VSCode communication.

Example from the artifact paper

In file artifact_paper_example.v, this amounts to putting the pointer on line 38 column 7 (counter visible on the bottom right-hand side of the editor), then on line 38 column 14 and checking the updated goal is the expected one (in this particular case, featuring nat in the associated goal instead of N in the initial goal).