removing anonymized artifact setup + getting started at the root

GETTING_STARTED.md

@@ -0,0 +1,95 @@
+# Getting started
+
+## What is Trocq?
+
+Trocq is a prototype of a modular parametricity plugin for Coq, aiming
+to perform proof transfer by translating the goal into an associated
+goal featuring the target data structures as well as a rich
+parametricity witness from which a function justifying the goal
+substitution can be extracted.
+
+The plugin features a hierarchy of parametricity witness types,
+ranging from structure-less relations to a new formulation of type
+equivalence, gathering several pre-existing parametricity
+translations, including
+[univalent parametricity](https://doi.org/10.1145/3429979) and
+[CoqEAL](https://github.com/coq-community/coqeal), in the same framework.
+
+This modular translation performs a fine-grained analysis and
+generates witnesses that are rich enough to preprocess the goal yet
+are not always a full-blown type equivalence, allowing to perform
+proof transfer with the power of univalent parametricity, but trying
+not to pull in the univalence axiom in cases where it is not required.
+
+The translation is implemented in Coq-Elpi and features transparent
+and readable code with respect to a sequent-style theoretical presentation.
+
+## 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 VSCode and Docker (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. You also
+need to ensure you have more than 6GB of disk space available.
+
+Here are the instructions:
+- Make sure your VSCode has the [Dev
+  Containers](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-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](https://github.com/coq-community/trocq), 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`) 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.
+
+### Via Opam (ocaml/coq/opam users only) or Nix (nix/nixos users only)
+
+Please refer to the main README.md
+
+## Exploring the examples
+
+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. Please note that on the
+first time a line is clicked in a file, the proof state can take a few seconds
+to update.
+
+### 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).
+
+### Examples from the Trocq paper
+
+## Exploring the code
+
+###