-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #2 from coq-community/update
update meta data
- Loading branch information
Showing
3 changed files
with
289 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,104 @@ | ||
<!--- | ||
This file was generated from `meta.yml`, please do not edit manually. | ||
Follow the instructions on https://github.com/coq-community/templates to regenerate. | ||
---> | ||
# Trocq | ||
|
||
This repository contains Trocq, a modular parametricity plugin for proof transfer in Coq. | ||
[![Contributing][contributing-shield]][contributing-link] | ||
[![Code of Conduct][conduct-shield]][conduct-link] | ||
[![Zulip][zulip-shield]][zulip-link] | ||
|
||
NB: it relies on a [custom version of Coq-Elpi](https://github.com/ecranceMERCE/coq-elpi/tree/strat), mainly changing its behaviour regarding the translation of universe variables between Elpi and Coq. | ||
|
||
[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg | ||
[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md | ||
|
||
[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg | ||
[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md | ||
|
||
[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg | ||
[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users | ||
|
||
|
||
|
||
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. | ||
|
||
## Meta | ||
|
||
- Author(s): | ||
- Cyril Cohen (initial) | ||
- Enzo Crance (initial) | ||
- Assia Mahboubi (initial) | ||
- Coq-community maintainer(s): | ||
- Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril)) | ||
- Enzo Crance ([**@ecranceMERCE**](https://github.com/ecranceMERCE)) | ||
- Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi)) | ||
- License: [GNU Lesser General Public License v3.0](LICENSE) | ||
- Compatible Coq versions: 8.17 | ||
- Additional dependencies: | ||
- [Coq-Elpi custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) | ||
- [Coq-HoTT 8.17](https://github.com/HoTT/Coq-HoTT) | ||
- Coq namespace: `Trocq` | ||
- Related publication(s): | ||
- [Trocq: Proof Transfer for Free, With or Without Univalence](https://hal.science/hal-04177913/document) | ||
|
||
## Building and installation instructions | ||
|
||
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. | ||
|
||
## Documentation | ||
|
||
To appear. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,39 +1,60 @@ | ||
# This file was generated from `meta.yml`, please do not edit manually. | ||
# Follow the instructions on https://github.com/coq-community/templates to regenerate. | ||
|
||
opam-version: "2.0" | ||
name: "coq-trocq" | ||
version: "dev" | ||
maintainer: "Enzo Crance <enzo.crance@inria.fr>" | ||
authors: [ "Cyril Cohen", "Enzo Crance", "Assia Mahboubi" ] | ||
homepage: "https://github.com/ecranceMERCE/trocq" | ||
bug-reports: "https://github.com/ecranceMERCE/trocq/issues" | ||
dev-repo: "https://github.com/ecranceMERCE/trocq.git" | ||
# doc: "https://ecranceMERCE.github.io/trocq" | ||
build: [ make "-j%{jobs}%" ] | ||
install: [ make "install" ] | ||
version: "dev" | ||
|
||
homepage: "https://github.com/coq-community/trocq" | ||
dev-repo: "git+https://github.com/coq-community/trocq.git" | ||
bug-reports: "https://github.com/coq-community/trocq/issues" | ||
license: "LGPL-3.0-or-later" | ||
|
||
synopsis: "A modular parametricity plugin for proof transfer in Coq" | ||
description: """ | ||
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.""" | ||
|
||
build: [make "-j%{jobs}%"] | ||
install: [make "install"] | ||
depends: [ | ||
"coq" {>= "8.17.0" & < "8.18~" } | ||
"coq" {>= "8.17" & < "8.18"} | ||
"coq-elpi" {= "dev"} | ||
"coq-hott" {>= "8.17" & < "8.18~"} | ||
] | ||
tags: [ | ||
|
||
tags: [ | ||
"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" | ||
"category:Miscellaneous/Coq Extensions" | ||
"keyword:automation" | ||
"keyword:elpi" | ||
"date:2023-11-10" | ||
"keyword:proof transfer" | ||
"keyword:isomorphism" | ||
"keyword:univalence" | ||
"keyword:parametricity" | ||
"logpath:Trocq" | ||
] | ||
synopsis: "A modular parametricity plugin for proof transfer in Coq" | ||
description: """ | ||
Trocq is a prototype of 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, among which univalent parametricity (*), under 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. | ||
|
||
(*) The marriage of univalence and parametricity, Tabareau et al. (2021) | ||
""" | ||
url { | ||
src: "git+https://github.com/ecranceMERCE/trocq.git" | ||
} | ||
authors: [ | ||
"Cyril Cohen" | ||
"Enzo Crance" | ||
"Assia Mahboubi" | ||
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
--- | ||
fullname: Trocq | ||
shortname: trocq | ||
organization: coq-community | ||
community: true | ||
action: false | ||
coqdoc: false | ||
|
||
synopsis: >- | ||
A modular parametricity plugin for proof transfer in Coq | ||
description: |- | ||
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. | ||
publications: | ||
- pub_url: https://hal.science/hal-04177913/document | ||
pub_title: 'Trocq: Proof Transfer for Free, With or Without Univalence' | ||
|
||
authors: | ||
- name: Cyril Cohen | ||
initial: true | ||
- name: Enzo Crance | ||
initial: true | ||
- name: Assia Mahboubi | ||
initial: true | ||
|
||
maintainers: | ||
- name: Cyril Cohen | ||
nickname: CohenCyril | ||
- name: Enzo Crance | ||
nickname: ecranceMERCE | ||
- name: Assia Mahboubi | ||
nickname: amahboubi | ||
|
||
opam-file-maintainer: Enzo Crance <enzo.crance@inria.fr> | ||
|
||
opam-file-version: dev | ||
|
||
license: | ||
fullname: GNU Lesser General Public License v3.0 | ||
identifier: LGPL-3.0-or-later | ||
file: LICENSE | ||
|
||
supported_coq_versions: | ||
text: 8.17 | ||
opam: '{>= "8.17" & < "8.18"}' | ||
|
||
tested_coq_opam_versions: | ||
- version: '8.17' | ||
|
||
dependencies: | ||
- opam: | ||
name: coq-elpi | ||
version: '{= "dev"}' | ||
description: |- | ||
[Coq-Elpi custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) | ||
- opam: | ||
name: coq-hott | ||
version: '{>= "8.17" & < "8.18~"}' | ||
description: |- | ||
[Coq-HoTT 8.17](https://github.com/HoTT/Coq-HoTT) | ||
namespace: Trocq | ||
|
||
keywords: | ||
- name: automation | ||
- name: elpi | ||
- name: proof transfer | ||
- name: isomorphism | ||
- name: univalence | ||
- name: parametricity | ||
|
||
categories: | ||
- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures | ||
- name: Miscellaneous/Coq Extensions | ||
|
||
build: |- | ||
## Building and installation instructions | ||
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. | ||
documentation: |- | ||
## Documentation | ||
To appear. | ||
--- |