diff --git a/GETTING_STARTED.md b/GETTING_STARTED.md index 9977a6f..bed1880 100644 --- a/GETTING_STARTED.md +++ b/GETTING_STARTED.md @@ -1,29 +1,5 @@ # 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 @@ -57,7 +33,35 @@ Here are the instructions: 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) +### Via Nix (recommended only for nix/nixos users) + + 1. First install nix https://nixos.org/download + 2. Add the [cachix](https://docs.cachix.org/installation) repository `coq-community` + ```shell + nix-env -iA cachix -f https://cachix.org/api/v1/install + cachix use coq-community + ``` + 3. Clone the current repository and type `nix-shell` + ```shell + git clone https://github.com/coq-community/trocq.git + nix-shell + ``` + 4. 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](https://opam.ocaml.org/doc/Install.html) + 2. Install the custom version of `coq-elpi` + ```shell + opam pin add coq-elpi https://github.com/ecranceMERCE/coq-elpi/archive/refs/heads/strat.tar.gz + ``` + 3. Build Trocq + ```shell + git clone https://github.com/coq-community/trocq.git + cd trocq + make # or make -j + ``` + 4. You can also run `make install` to install Trocq on your system. Please refer to the main README.md @@ -92,4 +96,4 @@ initial goal). ## Exploring the code -### \ No newline at end of file +### diff --git a/README.md b/README.md index 6ddd573..3fc6ee8 100644 --- a/README.md +++ b/README.md @@ -67,37 +67,8 @@ As Trocq is a prototype, it is currently unreleased, and depends on a [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of Coq-Elpi. There is not yet a dedicated way to install it. -There are however two ways to develop it and experiment with it: - -### Through nix - -1. First install nix https://nixos.org/download -2. Add the [cachix](https://docs.cachix.org/installation) repository `coq-community` -```shell -nix-env -iA cachix -f https://cachix.org/api/v1/install -cachix use coq-community -``` -3. Clone the current repository and type `nix-shell` -```shell -git clone https://github.com/coq-community/trocq.git -nix-shell -``` -4. You may also use `nix-build` to build it and reuse it as a nix package. - -### Through opam - -1. Install [opam](https://opam.ocaml.org/doc/Install.html) -2. Install the custom version of `coq-elpi` -```shell -opam pin add coq-elpi https://github.com/ecranceMERCE/coq-elpi/archive/refs/heads/strat.tar.gz -``` -3. Build Trocq -```shell -git clone https://github.com/coq-community/trocq.git -cd trocq -make # or make -j -``` -4. You can also run `make install` to install Trocq on your system. +There are however three ways to develop it and experiment with it, +they are documented in the [GETTING_STARTED.md file](GETTING_STARTED.md). ## Documentation diff --git a/meta.yml b/meta.yml index b8599a9..f8dd256 100644 --- a/meta.yml +++ b/meta.yml @@ -101,37 +101,9 @@ build: |- [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of Coq-Elpi. There is not yet a dedicated way to install it. - There are however two ways to develop it and experiment with it: - - ### Through nix - - 1. First install nix https://nixos.org/download - 2. Add the [cachix](https://docs.cachix.org/installation) repository `coq-community` - ```shell - nix-env -iA cachix -f https://cachix.org/api/v1/install - cachix use coq-community - ``` - 3. Clone the current repository and type `nix-shell` - ```shell - git clone https://github.com/coq-community/trocq.git - nix-shell - ``` - 4. You may also use `nix-build` to build it and reuse it as a nix package. - - ### Through opam - - 1. Install [opam](https://opam.ocaml.org/doc/Install.html) - 2. Install the custom version of `coq-elpi` - ```shell - opam pin add coq-elpi https://github.com/ecranceMERCE/coq-elpi/archive/refs/heads/strat.tar.gz - ``` - 3. Build Trocq - ```shell - git clone https://github.com/coq-community/trocq.git - cd trocq - make # or make -j - ``` - 4. You can also run `make install` to install Trocq on your system. + There are however three ways to develop it and experiment with it, + they are documented in the [GETTING_STARTED.md file](GETTING_STARTED.md). + documentation: |- ## Documentation