Merge pull request #59 from Zimmi48/leave-travis

Use templates to generate standard files and switch from Travis to GitHub Actions.

.github/workflows/coq-action.yml

@@ -0,0 +1,54 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-paramcoq.opam'
+          custom_image: ${{ matrix.image }}
+          custom_script: |
+            startGroup Print opam config
+              opam config list; opam repo list; opam list
+            endGroup
+            startGroup Build dependencies
+              opam pin add -n -y -k path $PACKAGE $WORKDIR
+              opam update -y
+              opam install -y -j 2 $PACKAGE --deps-only
+            endGroup
+            startGroup Build
+              opam install -y -v -j 2 $PACKAGE
+              opam list
+            endGroup
+            startGroup Workaround permission issue
+              sudo chown -R coq:coq .
+            endGroup
+            startGroup Run tests
+              make -C test-suite examples
+            endGroup
+            startGroup Uninstallation test
+              opam remove $PACKAGE
+            endGroup
+      - name: Revert permissions
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -0,0 +1,101 @@
+# Paramcoq
+
+[![CI][action-shield]][action-link]
+[![Contributing][contributing-shield]][contributing-link]
+[![Code of Conduct][conduct-shield]][conduct-link]
+[![Zulip][zulip-shield]][zulip-link]
+[![DOI][doi-shield]][doi-link]
+
+[action-shield]: https://github.com/coq-community/paramcoq/workflows/CI/badge.svg?branch=master
+[action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow%3ACI
+
+[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
+
+
+[doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.399.svg
+[doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.399
+
+The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.
+
+
+## Meta
+
+- Author(s):
+  - Chantal Keller (initial)
+  - Marc Lasson (initial)
+  - Abhishek Anand
+  - Pierre Roux
+  - Emilio Jesús Gallego Arias
+  - Cyril Cohen
+  - Matthieu Sozeau
+- Coq-community maintainer(s):
+  - Pierre Roux ([**@proux01**](https://github.com/proux01))
+- License: [MIT](LICENSE)
+- Compatible Coq versions: The master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq.
+
+- Additional dependencies: none
+- Coq namespace: `Param`
+- Related publication(s):
+  - [Parametricity in an Impredicative Sort](https://hal.archives-ouvertes.fr/hal-00730913/) doi:[10.4230/LIPIcs.CSL.2012.399](https://doi.org/10.4230/LIPIcs.CSL.2012.399)
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of Paramcoq
+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-paramcoq
+```
+
+To instead build and install manually, do:
+
+``` shell
+git clone https://github.com/coq-community/paramcoq.git
+cd paramcoq
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+Available commands
+------------------
+
+The default arity is 2.
+
+- Parametricity *ident* as *name* [arity *n*].
+
+Declare the translation named *name* from the translation of the constant or inductive *ident*.
+
+- Parametricity [Recursive] *ident* [arity *n*] [qualified].
+
+The default name for the translation of the constant or inductive *ident* is automatically generated (from its unqualified name).
+You can use the `Recursive` option to recursively translate all the constants and inductives which are used by *ident*.
+You can use the `qualified` option to use a qualified default name for the translated constants and inductives. The default name then has the form `Module_o_Submodule_o_ident` if *ident* lies in the `Module.Submodule` namespace.
+
+- Parametricity Translation *term* [as *name*] [arity *n*].
+
+Define a new constant named *name* obtained by computing the parametricity translation of *term*.
+
+- Parametricity Module *modulepath*.
+
+Recursively translate everything in a module.
+
+- Realizer *constant or variable* [as *name*] [arity *n*] := *term*.
+
+Declare *term* to be the translation of a constant.
+Useful to translate terms containing section variables, or axioms.
+
+Note that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import `ProofIrrelevence`).
+
+- [Global | Local] Parametricity Tactic := t.
+
+Use the tactic t to solve proof obligations generated by the `Parametricity` command.
+

coq-paramcoq.opam

@@ -1,40 +1,36 @@
 opam-version: "2.0"
-version: "dev"
 maintainer: "Pierre Roux <[email protected]>"
+version: "dev"
 
 homepage: "https://github.com/coq-community/paramcoq"
 dev-repo: "git+https://github.com/coq-community/paramcoq.git"
 bug-reports: "https://github.com/coq-community/paramcoq/issues"
 license: "MIT"
 
-build: [make "-j%{jobs}%"]
+synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
+description: """
+The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.
+"""
+
+build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.10" & < "8.10~"}
+  "coq" {= dev }
 ]
 
 tags: [
+  "category:Miscellaneous/Coq Extensions"
   "keyword:paramcoq"
   "keyword:parametricity"
   "keyword:ocaml module"
-  "category:Miscellaneous/Coq Extensions"
   "logpath:Param"
 ]
 authors: [
-  "Chantal Keller (Inria, École polytechnique)"
-  "Marc Lasson (ÉNS de Lyon)"
+  "Chantal Keller"
+  "Marc Lasson"
   "Abhishek Anand"
   "Pierre Roux"
   "Emilio Jesús Gallego Arias"
   "Cyril Cohen"
   "Matthieu Sozeau"
 ]
-synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
-description: """
-The plugin is still in an experimental state. It is not very user
-friendly (lack of good error messages) and still contains bugs. But is
-useable enough to "translate" a large chunk of standard library."""
-url {
-  src: "https://github.com/coq-community/paramcoq/archive/v1.1.2+coq8.7.tar.gz"
-  checksum: "sha256=48fcb716c00d52802a9596ee396eab9af7f368da6afebdbb9cf67738ae133b97"
-}