diff --git a/README.md b/README.md index 0b7e0b9..6ddd573 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,104 @@ + # 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. \ No newline at end of file + +[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 +``` +4. You can also run `make install` to install Trocq on your system. + +## Documentation + +To appear. diff --git a/coq-trocq.opam b/coq-trocq.opam index c1a5c48..f1f95e0 100644 --- a/coq-trocq.opam +++ b/coq-trocq.opam @@ -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 " -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" +] diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..b8599a9 --- /dev/null +++ b/meta.yml @@ -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 + +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 + ``` + 4. You can also run `make install` to install Trocq on your system. + +documentation: |- + ## Documentation + + To appear. +---