From 95ef1c88dbaf55b8f0b99861efce69c2473562c7 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Wed, 25 Aug 2021 13:03:01 +0200 Subject: [PATCH] merge changes from master that do not break 8.12 --- .github/workflows/docker-action.yml | 34 ++++++++ .gitignore | 8 +- Makefile | 22 ++--- README.md | 127 ++++++++++++++++++++++++++++ Make.cfg => _CoqProject | 2 + coq-paramcoq.opam | 30 ++++--- dune-project | 3 + meta.yml | 122 ++++++++++++++++++++++++++ src/dune | 13 ++- theories/Param.v | 1 + theories/dune | 5 ++ 11 files changed, 333 insertions(+), 34 deletions(-) create mode 100644 .github/workflows/docker-action.yml create mode 100644 README.md rename Make.cfg => _CoqProject (79%) create mode 100644 dune-project create mode 100644 meta.yml create mode 100644 theories/Param.v create mode 100644 theories/dune diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..f635f97 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,34 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - v8.12 + 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:8.12' + 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 }} + export: 'OPAMWITHTEST' + env: + OPAMWITHTEST: 'true' + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.gitignore b/.gitignore index 9c0328c..1423b63 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,6 @@ # Generated Makefile -/Makefile.coq -/Makefile.coq.conf +Makefile.coq +Makefile.coq.conf # Make dependencies *.d @@ -38,3 +38,7 @@ # coqpp generated file src/abstraction.ml + +# lia cache +.lia.cache +status diff --git a/Makefile b/Makefile index d4d7fad..ad909e5 100644 --- a/Makefile +++ b/Makefile @@ -1,14 +1,16 @@ -# -*- Makefile -*- -.PHONY: coq clean +all: Makefile.coq + @+$(MAKE) -f Makefile.coq all -coq:: Makefile.coq - $(MAKE) -f Makefile.coq +clean: Makefile.coq + @+$(MAKE) -f Makefile.coq cleanall + @rm -f Makefile.coq Makefile.coq.conf -Makefile.coq: Make.cfg - coq_makefile -f Make.cfg -o Makefile.coq +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq -distclean: - rm -f Makefile.coq Makefile.coq.conf Makefile.coq.bak .coqdeps.d +force _CoqProject Makefile: ; -install: - $(MAKE) -f Makefile.coq install +%: Makefile.coq force + @+$(MAKE) -f Makefile.coq $@ + +.PHONY: all clean force diff --git a/README.md b/README.md new file mode 100644 index 0000000..d54fcf5 --- /dev/null +++ b/README.md @@ -0,0 +1,127 @@ + +# Paramcoq + +[![Docker CI][docker-action-shield]][docker-action-link] +[![Contributing][contributing-shield]][contributing-link] +[![Code of Conduct][conduct-shield]][conduct-link] +[![Zulip][zulip-shield]][zulip-link] +[![DOI][doi-shield]][doi-link] + +[docker-action-shield]: https://github.com/coq-community/paramcoq/workflows/Docker%20CI/badge.svg?branch=v8.12 +[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI" + +[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 + +A Coq plugin providing commands for generating parametricity statements. +Typical applications of such statements are in data refinement proofs. +Note that the plugin is still in an experimental state - it is not very user +friendly (lack of good error messages) and still contains bugs. But it +is usable enough to "translate" a large chunk of the 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](LICENSE) +- Compatible Coq versions: The v8.12 branch tracks version 8.13 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 +make install +``` + + +## Usage and Commands + +To load the plugin and make its commands available: +```coq +From Param Require Import Param. +``` + +The command scheme for named translations is: +``` +Parametricity as [arity ]. +``` +For example, the following command generates a translation named `my_param` +of the constant or inductive `my_id` with arity 2 (the default): +```coq +Parametricity my_id as my_param. +``` + +The command scheme for automatically named translations is: +```coq +Parametricity [Recursive] [arity ] [qualified]. +``` +Such commands generate and name translations based on the given identifier. +The `Recursive` option can be used to recursively translate all the constants +and inductives which are used by the constant or inductive with the given +identifier. The `qualified` option allows you to use a qualified default name +for the translated constants and inductives. The default name then has the form +`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the +`Module.Submodule` namespace. + +Instead of using identifiers, you can provide explicit terms to translate, +according to the following command scheme: +```coq +Parametricity Translation [as ] [arity ]. +``` +This defines a new constant containing the parametricity translation of +the given term. + +To recursively translate everything in a module: +```coq +Parametricity Module . +``` + +When translating terms containing section variables or axioms, +it may be useful to declare a term to be the translation of a constant: +```coq +Realizer [as ] [arity ] := . +``` + +Note that translating a term or module may lead to proof obligations (for some +fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to +declare a tactic to solve such proof obligations: +```coq +[Global|Local] Parametricity Tactic := . +``` diff --git a/Make.cfg b/_CoqProject similarity index 79% rename from Make.cfg rename to _CoqProject index 7984b76..d8dfbb2 100644 --- a/Make.cfg +++ b/_CoqProject @@ -1,3 +1,4 @@ +-R theories Param -R src Param -I src src/debug.ml @@ -6,3 +7,4 @@ src/relations.ml src/declare_translation.ml src/abstraction.mlg src/paramcoq.mlpack +theories/Param.v diff --git a/coq-paramcoq.opam b/coq-paramcoq.opam index ecf2ad5..446b310 100644 --- a/coq-paramcoq.opam +++ b/coq-paramcoq.opam @@ -1,40 +1,42 @@ +# 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" -version: "1.1.2+coq8.12" maintainer: "Pierre Roux " +version: "8.12.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" +synopsis: "Plugin for generating parametricity statements to perform refinement proofs" +description: """ +A Coq plugin providing commands for generating parametricity statements. +Typical applications of such statements are in data refinement proofs. +Note that the plugin is still in an experimental state - it is not very user +friendly (lack of good error messages) and still contains bugs. But it +is usable enough to "translate" a large chunk of the standard library.""" + build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {>= "8.12" & < "8.13~"} + "coq" {>= "8.12" & < "8.13" } ] 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" -} diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..6111640 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.5) +(using coq 0.2) +(name paramcoq) diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..cf89e11 --- /dev/null +++ b/meta.yml @@ -0,0 +1,122 @@ +--- +fullname: Paramcoq +shortname: paramcoq +organization: coq-community +community: true +action: true +plugin: true +doi: 10.4230/LIPIcs.CSL.2012.399 +branch: v8.12 + +synopsis: Plugin for generating parametricity statements to perform refinement proofs + +description: |- + A Coq plugin providing commands for generating parametricity statements. + Typical applications of such statements are in data refinement proofs. + Note that the plugin is still in an experimental state - it is not very user + friendly (lack of good error messages) and still contains bugs. But it + is usable enough to "translate" a large chunk of the standard library. + +publications: +- pub_title: Parametricity in an Impredicative Sort + pub_url: https://hal.archives-ouvertes.fr/hal-00730913/ + pub_doi: 10.4230/LIPIcs.CSL.2012.399 + +authors: +- name: Chantal Keller + initial: true +- name: Marc Lasson + initial: true +- name: Abhishek Anand +- name: Pierre Roux +- name: Emilio Jesús Gallego Arias +- name: Cyril Cohen +- name: Matthieu Sozeau + +maintainers: +- name: Pierre Roux + nickname: proux01 + +license: + fullname: MIT License + identifier: MIT + +supported_coq_versions: + text: >- + The v8.12 branch tracks version 8.13 of Coq, see + releases for compatibility with released versions of Coq. + opam: '{>= "8.12" & < "8.13" }' + +categories: +- name: 'Miscellaneous/Coq Extensions' + +keywords: +- name: paramcoq +- name: parametricity +- name: ocaml module + +namespace: Param + +opam-file-maintainer: 'Pierre Roux ' + +opam-file-version: '8.12.dev' + +tested_coq_opam_versions: +- version: '8.12' + +documentation: |- + ## Usage and Commands + + To load the plugin and make its commands available: + ```coq + From Param Require Import Param. + ``` + + The command scheme for named translations is: + ``` + Parametricity as [arity ]. + ``` + For example, the following command generates a translation named `my_param` + of the constant or inductive `my_id` with arity 2 (the default): + ```coq + Parametricity my_id as my_param. + ``` + + The command scheme for automatically named translations is: + ```coq + Parametricity [Recursive] [arity ] [qualified]. + ``` + Such commands generate and name translations based on the given identifier. + The `Recursive` option can be used to recursively translate all the constants + and inductives which are used by the constant or inductive with the given + identifier. The `qualified` option allows you to use a qualified default name + for the translated constants and inductives. The default name then has the form + `Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the + `Module.Submodule` namespace. + + Instead of using identifiers, you can provide explicit terms to translate, + according to the following command scheme: + ```coq + Parametricity Translation [as ] [arity ]. + ``` + This defines a new constant containing the parametricity translation of + the given term. + + To recursively translate everything in a module: + ```coq + Parametricity Module . + ``` + + When translating terms containing section variables or axioms, + it may be useful to declare a term to be the translation of a constant: + ```coq + Realizer [as ] [arity ] := . + ``` + + Note that translating a term or module may lead to proof obligations (for some + fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to + declare a tactic to solve such proof obligations: + ```coq + [Global|Local] Parametricity Tactic := . + ``` +--- diff --git a/src/dune b/src/dune index 177bd59..3c06cd2 100644 --- a/src/dune +++ b/src/dune @@ -1,11 +1,8 @@ (library (name paramcoq) - (public_name coq.plugins.paramcoq) - (synopsis "Coq Plugin for Parametricity") - (flags :standard -warn-error -3) - (libraries coq.plugins.ltac)) + (public_name coq-paramcoq.plugin) + (synopsis "Plugin for generating parametricity statements to perform refinement proofs") + (flags :standard -rectypes -w -9-27) + (libraries coq-core.plugins.ltac)) -(rule - (targets abstraction.ml) - (deps (:pp-file abstraction.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules abstraction)) diff --git a/theories/Param.v b/theories/Param.v new file mode 100644 index 0000000..c3a74b5 --- /dev/null +++ b/theories/Param.v @@ -0,0 +1 @@ +Declare ML Module "paramcoq". diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..d65823a --- /dev/null +++ b/theories/dune @@ -0,0 +1,5 @@ +(coq.theory + (name Param) + (package coq-paramcoq) + (synopsis "Plugin for generating parametricity statements to perform refinement proofs") + (libraries coq-paramcoq.plugin))