|
1 | | -<!--- |
2 | | -This file was generated from `meta.yml`, please do not edit manually. |
3 | | -Follow the instructions on https://github.com/coq-community/templates to regenerate. |
4 | | ----> |
5 | | -# Paramcoq |
6 | | - |
7 | | -[![Docker CI][docker-action-shield]][docker-action-link] |
8 | | -[![Contributing][contributing-shield]][contributing-link] |
9 | | -[![Code of Conduct][conduct-shield]][conduct-link] |
10 | | -[![Zulip][zulip-shield]][zulip-link] |
11 | | -[![DOI][doi-shield]][doi-link] |
12 | | - |
13 | | -[docker-action-shield]: https://github.com/coq-community/paramcoq/actions/workflows/docker-action.yml/badge.svg?branch=v9.0 |
14 | | -[docker-action-link]: https://github.com/coq-community/paramcoq/actions/workflows/docker-action.yml |
15 | | - |
16 | | -[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg |
17 | | -[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md |
18 | | - |
19 | | -[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg |
20 | | -[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md |
21 | | - |
22 | | -[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg |
23 | | -[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users |
24 | | - |
25 | | - |
26 | | -[doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.381.svg |
27 | | -[doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.381 |
28 | | - |
29 | | -A Rocq plugin providing commands for generating parametricity statements. |
30 | | -Typical applications of such statements are in data refinement proofs. |
31 | | -Note that the plugin is still in an experimental state - it is not very user |
32 | | -friendly (lack of good error messages) and still contains bugs. But it |
33 | | -is usable enough to "translate" a large chunk of the standard library. |
34 | | - |
35 | | -## Meta |
36 | | - |
37 | | -- Author(s): |
38 | | - - Chantal Keller (initial) |
39 | | - - Marc Lasson (initial) |
40 | | - - Abhishek Anand |
41 | | - - Pierre Roux |
42 | | - - Emilio Jesús Gallego Arias |
43 | | - - Cyril Cohen |
44 | | - - Matthieu Sozeau |
45 | | -- Coq-community maintainer(s): |
46 | | - - Pierre Roux ([**@proux01**](https://github.com/proux01)) |
47 | | -- License: [MIT License](LICENSE) |
48 | | -- Compatible Coq versions: The v9.0 branch supports version 9.0 of Rocq, see releases for compatibility with released versions of Rocq |
49 | | -- Additional dependencies: none |
50 | | -- Coq namespace: `Param` |
51 | | -- Related publication(s): |
52 | | - - [Parametricity in an Impredicative Sort](https://hal.archives-ouvertes.fr/hal-00730913/) doi:[10.4230/LIPIcs.CSL.2012.381](https://doi.org/10.4230/LIPIcs.CSL.2012.381) |
53 | | - |
54 | | -## Building and installation instructions |
55 | | - |
56 | | -The easiest way to install the latest released version of Paramcoq |
57 | | -is via [OPAM](https://opam.ocaml.org/doc/Install.html): |
58 | | - |
59 | | -```shell |
60 | | -opam repo add coq-released https://coq.inria.fr/opam/released |
61 | | -opam install coq-paramcoq |
62 | | -``` |
63 | | - |
64 | | -To instead build and install manually, do: |
65 | | - |
66 | | -``` shell |
67 | | -git clone https://github.com/coq-community/paramcoq.git |
68 | | -cd paramcoq |
69 | | -make # or make -j <number-of-cores-on-your-machine> |
70 | | -make install |
71 | | -``` |
72 | | - |
73 | | - |
74 | | -## Usage and Commands |
75 | | - |
76 | | -To load the plugin and make its commands available: |
77 | | -```coq |
78 | | -From Param Require Import Param. |
79 | | -``` |
80 | | - |
81 | | -The command scheme for named translations is: |
82 | | -``` |
83 | | -Parametricity <ident> as <name> [arity <n>]. |
84 | | -``` |
85 | | -For example, the following command generates a translation named `my_param` |
86 | | -of the constant or inductive `my_id` with arity 2 (the default): |
87 | | -```coq |
88 | | -Parametricity my_id as my_param. |
89 | | -``` |
90 | | - |
91 | | -The command scheme for automatically named translations is: |
92 | | -```coq |
93 | | -Parametricity [Recursive] <ident> [arity <n>] [qualified]. |
94 | | -``` |
95 | | -Such commands generate and name translations based on the given identifier. |
96 | | -The `Recursive` option can be used to recursively translate all the constants |
97 | | -and inductives which are used by the constant or inductive with the given |
98 | | -identifier. The `qualified` option allows you to use a qualified default name |
99 | | -for the translated constants and inductives. The default name then has the form |
100 | | -`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the |
101 | | -`Module.Submodule` namespace. |
102 | | - |
103 | | -Instead of using identifiers, you can provide explicit terms to translate, |
104 | | -according to the following command scheme: |
105 | | -```coq |
106 | | -Parametricity Translation <term> [as <name>] [arity <n>]. |
107 | | -``` |
108 | | -This defines a new constant containing the parametricity translation of |
109 | | -the given term. |
110 | | - |
111 | | -To recursively translate everything in a module: |
112 | | -```coq |
113 | | -Parametricity Module <module_path>. |
114 | | -``` |
115 | | - |
116 | | -When translating terms containing section variables or axioms, |
117 | | -it may be useful to declare a term to be the translation of a constant: |
118 | | -```coq |
119 | | -Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>. |
120 | | -``` |
121 | | - |
122 | | -Note that translating a term or module may lead to proof obligations (for some |
123 | | -fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to |
124 | | -declare a tactic to solve such proof obligations: |
125 | | -```coq |
126 | | -Parametricity Tactic := <tactic>. |
127 | | -``` |
128 | | -(supports global/export/local attributes like Obligation Tactic) |
| 1 | +# Deprecation Notice |
| 2 | + |
| 3 | +Paramcoq is no longer actually maintained and released. It is only |
| 4 | +kept as a test case for Rocq's OCaml API. The release for Rocq 9.0 |
| 5 | +will be the last one and is known to suffer some universe issues |
| 6 | +(for instance iit no longer enable to compile CoqEAL). Users are |
| 7 | +invited to switch to [coq-elpi](https://github.com/LPCIC/coq-elpi) |
| 8 | +derive.param2. One can look at |
| 9 | +[CoqEAL](https://github.com/coq-community/coqeal) for an example of |
| 10 | +porting. Main current caveat: support for mutual inductives isn't |
| 11 | +implemented yet. |
| 12 | + |
| 13 | +See [old README](README_old.md) for previous documentation. |
0 commit comments