Skip to content

Commit 8b8afda

Browse files
proux01proux01
committed
Add deprecation notice
1 parent 7677ccf commit 8b8afda

File tree

4 files changed

+164
-184
lines changed

4 files changed

+164
-184
lines changed

‎README.md‎

Lines changed: 13 additions & 128 deletions
Original file line numberDiff line numberDiff line change
@@ -1,128 +1,13 @@
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/workflows/Docker%20CI/badge.svg?branch=master
14-
[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI"
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 Coq 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 master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq
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.

‎README_old.md‎

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
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/workflows/Docker%20CI/badge.svg?branch=master
14+
[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI"
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 Coq 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 master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq
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)

‎coq-paramcoq.opam‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,23 @@ license: "MIT"
1212

1313
synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
1414
description: """
15-
A Coq plugin providing commands for generating parametricity statements.
15+
/!\ Paramcoq is no longer actually maintained and released. It is only
16+
kept as a test case for Rocq's OCaml API. The release for Rocq 9.0
17+
will be the last one and is known to suffer some universe issues
18+
(for instance iit no longer enable to compile CoqEAL). Users are
19+
invited to switch to [coq-elpi](https://github.com/LPCIC/coq-elpi)
20+
derive.param2. One can look at
21+
[CoqEAL](https://github.com/coq-community/coqeal) for an example of
22+
porting. Main current caveat: support for mutual inductives isn't
23+
implemented yet.
24+
25+
A Rocq plugin providing commands for generating parametricity statements.
1626
Typical applications of such statements are in data refinement proofs.
1727
Note that the plugin is still in an experimental state - it is not very user
1828
friendly (lack of good error messages) and still contains bugs. But it
1929
is usable enough to "translate" a large chunk of the standard library."""
2030

31+
messages: ["/!\ This is the last release of paramcoq, more details on https://github.com/coq-community/paramcoq/blob/master/README.md"]
2132
build: [make "-j%{jobs}%"]
2233
install: [
2334
[make "install"]

‎meta.yml‎

Lines changed: 11 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -65,59 +65,15 @@ tested_coq_opam_versions:
6565
- version: 'dev'
6666

6767
documentation: |-
68-
## Usage and Commands
69-
70-
To load the plugin and make its commands available:
71-
```coq
72-
From Param Require Import Param.
73-
```
74-
75-
The command scheme for named translations is:
76-
```
77-
Parametricity <ident> as <name> [arity <n>].
78-
```
79-
For example, the following command generates a translation named `my_param`
80-
of the constant or inductive `my_id` with arity 2 (the default):
81-
```coq
82-
Parametricity my_id as my_param.
83-
```
84-
85-
The command scheme for automatically named translations is:
86-
```coq
87-
Parametricity [Recursive] <ident> [arity <n>] [qualified].
88-
```
89-
Such commands generate and name translations based on the given identifier.
90-
The `Recursive` option can be used to recursively translate all the constants
91-
and inductives which are used by the constant or inductive with the given
92-
identifier. The `qualified` option allows you to use a qualified default name
93-
for the translated constants and inductives. The default name then has the form
94-
`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the
95-
`Module.Submodule` namespace.
96-
97-
Instead of using identifiers, you can provide explicit terms to translate,
98-
according to the following command scheme:
99-
```coq
100-
Parametricity Translation <term> [as <name>] [arity <n>].
101-
```
102-
This defines a new constant containing the parametricity translation of
103-
the given term.
104-
105-
To recursively translate everything in a module:
106-
```coq
107-
Parametricity Module <module_path>.
108-
```
109-
110-
When translating terms containing section variables or axioms,
111-
it may be useful to declare a term to be the translation of a constant:
112-
```coq
113-
Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
114-
```
115-
116-
Note that translating a term or module may lead to proof obligations (for some
117-
fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to
118-
declare a tactic to solve such proof obligations:
119-
```coq
120-
Parametricity Tactic := <tactic>.
121-
```
122-
(supports global/export/local attributes like Obligation Tactic)
68+
# Deprecation Notice
69+
70+
Paramcoq is no longer actually maintained and released. It is only
71+
kept as a test case for Rocq's OCaml API. The release for Rocq 9.0
72+
will be the last one and is known to suffer some universe issues
73+
(for instance iit no longer enable to compile CoqEAL). Users are
74+
invited to switch to [coq-elpi](https://github.com/LPCIC/coq-elpi)
75+
derive.param2. One can look at
76+
[CoqEAL](https://github.com/coq-community/coqeal) for an example of
77+
porting. Main current caveat: support for mutual inductives isn't
78+
implemented yet.
12379
---

0 commit comments

Comments
 (0)