adding meta.yml

coq-community · Nov 11, 2023 · 2a864bd · 2a864bd
1 parent 9ebb988
commit 2a864bd
Show file tree

Hide file tree

Showing 3 changed files with 221 additions and 28 deletions.
diff --git a/README.md b/README.md
@@ -1,5 +1,79 @@
+<!---
+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.
+[![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.
+[docker-action-shield]: https://github.com/ecranceMERCE/trocq/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/ecranceMERCE/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):
+  - [<nil>](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/ecranceMERCE/trocq.git
+cd trocq
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Documentation
+
+Coming
diff --git a/coq-trocq.opam b/coq-trocq.opam
@@ -1,39 +1,64 @@
+# 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 <[email protected]>"
-authors: [ "Cyril Cohen", "Enzo Crance", "Assia Mahboubi" ]
+version: "dev"
+
 homepage: "https://github.com/ecranceMERCE/trocq"
+dev-repo: "git+https://github.com/ecranceMERCE/trocq.git"
 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" ]
+license: "GPL-3.0-only"
+
+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
@@ -0,0 +1,94 @@
+fullname: Trocq
+shortname: trocq
+organization: ecranceMERCE
+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 <[email protected]>
+
+opam-file-version: dev
+
+license:
+  fullname: GNU Lesser General Public License v3.0
+  identifier: GPL-3.0-only
+  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