Skip to content

Commit

Permalink
moving the opam and nix instructions to GETTING_STARTED
Browse files Browse the repository at this point in the history
  • Loading branch information
CohenCyril committed Jan 5, 2024
1 parent 05e4c0c commit 1079a9f
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 88 deletions.
56 changes: 30 additions & 26 deletions GETTING_STARTED.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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 <number-of-cores-on-your-machine>
```
4. You can also run `make install` to install Trocq on your system.

Please refer to the main README.md

Expand Down Expand Up @@ -92,4 +96,4 @@ initial goal).

## Exploring the code

###
###
33 changes: 2 additions & 31 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 <number-of-cores-on-your-machine>
```
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

Expand Down
34 changes: 3 additions & 31 deletions meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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 <number-of-cores-on-your-machine>
```
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
Expand Down

0 comments on commit 1079a9f

Please sign in to comment.