diff --git a/.nix/config.nix b/.nix/config.nix index b664596..d50780c 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -84,14 +84,13 @@ ## Below we list some standard ones cachix.coq = {}; cachix.math-comp = {}; - cachix.coq-community = {}; ## If you have write access to one of these caches you can ## provide the auth token or signing key through a secret ## variable on GitHub. Then, you should give the variable ## name here. For instance, coq-community projects can use ## the following line instead of the one above: - # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; + cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; ## Or if you have a signing key for a given Cachix cache: # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" diff --git a/README.md b/README.md index 0b7e0b9..9a94ba1 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,76 @@ + # Trocq -This repository contains Trocq, a modular parametricity plugin for proof transfer in Coq. +[![Docker CI][docker-action-shield]][docker-action-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. \ No newline at end of file +[docker-action-shield]: https://github.com/coq-community/trocq/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/trocq/actions?query=workflow:"Docker%20CI" + + + + +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 [1] and +CoqEAL [2], 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. + +[1] The marriage of univalence and parametricity, Tabareau et al. (2021) +[2] https://github.com/coq-community/coqeal + +## Meta + +- Author(s): + - Cyril Cohen (initial) + - Enzo Crance (initial) + - Assia Mahboubi (initial) +- License: [GNU Lesser General Public License v3.0](LICENSE) +- Compatible Coq versions: Coq 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): + - [](https://hal.science/hal-04177913/document) + +## Building and installation instructions + +The easiest way to install the latest released version of Trocq +is via [OPAM](https://opam.ocaml.org/doc/Install.html): + +```shell +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-trocq +``` + +To instead build and install manually, do: + +``` shell +git clone https://github.com/coq-community/trocq.git +cd trocq +make # or make -j +make install +``` + + +## Documentation + +Coming diff --git a/coq-trocq.opam b/coq-trocq.opam index c1a5c48..6d02370 100644 --- a/coq-trocq.opam +++ b/coq-trocq.opam @@ -1,39 +1,61 @@ +# 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 " -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 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 [1] and +CoqEAL [2], 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. + +[1] The marriage of univalence and parametricity, Tabareau et al. (2021) +[2] https://github.com/coq-community/coqeal""" + +build: [make "-j%{jobs}%"] +install: [make "install"] depends: [ - "coq" {>= "8.17.0" & < "8.18~" } - "coq-elpi" {= "dev"} + "coq" { (= "8.17") } + "coq-epli" { = "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" "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" +] diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..e118180 --- /dev/null +++ b/meta.yml @@ -0,0 +1,91 @@ +fullname: Trocq +shortname: trocq +organization: coq-community +opam_name: coq-trocq +community: false +action: true +coqdoc: false + +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 [1] and + CoqEAL [2], 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. + + [1] The marriage of univalence and parametricity, Tabareau et al. (2021) + [2] https://github.com/coq-community/coqeal + +authors: +- name: Cyril Cohen + initial: true +- name: Enzo Crance + initial: true +- name: Assia Mahboubi + initial: true + +opam-file-maintainer: Enzo Crance + +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: Coq 8.17 + opam: '{ (= "8.17") }' + +tested_coq_opam_versions: +- version: 'coq-8.17' + repo: 'coq/coq' + +dependencies: +- opam: + name: coq-epli + 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 + +categories: +- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures +- name: Miscellaneous/Coq Extensions + +publications: +- pub_url: https://hal.science/hal-04177913/document + pub_title: +documentation: |- + ## Documentation + + Coming