📝 Getting started guide

artifact-clean/GETTING_STARTED.md

@@ -0,0 +1,36 @@
+# Getting started
+
+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.
+
+## Testing the code (recommended)
+
+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](https://www.docker.com) and [VSCode](https://code.visualstudio.com) installed on their machine.
+
+Here are the instructions:
+- Pull the Docker image containing our code.
+  ```shell
+  docker pull cohencyril/trocq
+  ```
+- Run a Docker container from this image and leave this terminal on the side.
+  ```shell
+  docker run --rm -it -v bash cohencyril/trocq
+  ```
+- Start VSCode on the host and install the [Dev Containers](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers) extension.
+- Click on the `><` button at the bottom left-hand corner of the window.
+  A menu opens in the middle.
+- Choose `Attach to Running Container...` and select the container that is based on the `cohencyril/trocq` image.
+  A new window opens and connects to this container.
+- Wait for the actions displayed on the bottom bar to end.
+  That is, the navigator on the top left-hand side shows `Connected to remote.` and the bottom bar does no longer load anything and just displays `Container cohencyril/trocq [...]`.
+- Click `Open Folder` in the navigator on the top left-hand side, then navigate to `/home/coq/trocq` and click `OK`.
+- Now, 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. Please note that on the first time a line is clicked in a file, the proof state can take a few seconds to update.
+
+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).
+
+## Installing the plugin
+
+In this set-up, the reader is a regular Coq user and might want to install the plugin for further use in their proofs. In this case, the recommended way to proceed is to clone the [Trocq repository](https://github.com/coq-community/trocq/) and follow instructions in the `README`. In particular, two options are available to install Trocq, according to personal preference, one through the `opam` package manager and the other through Nix.