Skip to content

Commit 34de123

Browse files
mattam82mattam82
committed
MetaRocq 1.4 for Rocq 9.0 release
1 parent cd4b494 commit 34de123

File tree

12 files changed

+542
-0
lines changed
  • released/packages
    • rocq-metarocq/rocq-metarocq.1.4+9.0
    • rocq-metarocq-common/rocq-metarocq-common.1.4+9.0
    • rocq-metarocq-erasure/rocq-metarocq-erasure.1.4+9.0
    • rocq-metarocq-erasure-plugin/rocq-metarocq-erasure-plugin.1.4+9.0
    • rocq-metarocq-pcuic/rocq-metarocq-pcuic.1.4+9.0
    • rocq-metarocq-quotation/rocq-metarocq-quotation.1.4+9.0
    • rocq-metarocq-safechecker/rocq-metarocq-safechecker.1.4+9.0
    • rocq-metarocq-safechecker-plugin/rocq-metarocq-safechecker-plugin.1.4+9.0
    • rocq-metarocq-template/rocq-metarocq-template.1.4+9.0
    • rocq-metarocq-template-pcuic/rocq-metarocq-template-pcuic.1.4+9.0
    • rocq-metarocq-translations/rocq-metarocq-translations.1.4+9.0
    • rocq-metarocq-utils/rocq-metarocq-utils.1.4+9.0

12 files changed

+542
-0
lines changed

‎released/packages/rocq-metarocq-common/rocq-metarocq-common.1.4+9.0/opam

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "common"]
25+
]
26+
install: [
27+
[make "-C" "common" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-utils" {= version}
31+
]
32+
synopsis: "The common library of Template Rocq and PCUIC"
33+
description: """
34+
MetaRocq is a meta-programming framework for Rocq.
35+
"""
36+
url {
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
38+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
39+
}

‎released/packages/rocq-metarocq-erasure-plugin/rocq-metarocq-erasure-plugin.1.4+9.0/opam

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "erasure-plugin"]
25+
]
26+
install: [
27+
[make "-C" "erasure-plugin" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-template-pcuic" {= version}
31+
"rocq-metarocq-erasure" {= version}
32+
]
33+
synopsis: "Implementation and verification of an erasure procedure for Rocq"
34+
description: """
35+
MetaRocq is a meta-programming framework for Rocq.
36+
37+
The Erasure module provides a complete specification of Rocq's so-called
38+
\"extraction\" procedure, starting from the PCUIC calculus and targeting
39+
untyped call-by-value lambda-calculus.
40+
41+
The `erasure` function translates types and proofs in well-typed terms
42+
into a dummy `tBox` constructor, following closely P. Letouzey's PhD
43+
thesis.
44+
"""
45+
url {
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
47+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
48+
}

‎released/packages/rocq-metarocq-erasure/rocq-metarocq-erasure.1.4+9.0/opam

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "erasure"]
25+
]
26+
install: [
27+
[make "-C" "erasure" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-safechecker" {= version}
31+
"rocq-metarocq-template-pcuic" {= version}
32+
]
33+
synopsis: "Implementation and verification of an erasure procedure for Rocq"
34+
description: """
35+
MetaRocq is a meta-programming framework for Rocq.
36+
37+
The Erasure module provides a complete specification of Rocq's so-called
38+
\"extraction\" procedure, starting from the PCUIC calculus and targeting
39+
untyped call-by-value lambda-calculus.
40+
41+
The `erasure` function translates types and proofs in well-typed terms
42+
into a dummy `tBox` constructor, following closely P. Letouzey's PhD
43+
thesis.
44+
"""
45+
url {
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
47+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
48+
}

‎released/packages/rocq-metarocq-pcuic/rocq-metarocq-pcuic.1.4+9.0/opam

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "pcuic"]
25+
]
26+
install: [
27+
[make "-C" "pcuic" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-common" {= version}
31+
]
32+
synopsis: "A type system equivalent to Rocq's and its metatheory"
33+
description: """
34+
MetaRocq is a meta-programming framework for Rocq.
35+
36+
The PCUIC module provides a cleaned-up specification of Rocq's typing algorithm along
37+
with a certified typechecker for it. This module includes the standard metatheory of
38+
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
39+
"""
40+
url {
41+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
42+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
43+
}

‎released/packages/rocq-metarocq-quotation/rocq-metarocq-quotation.1.4+9.0/opam

+53
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "quotation"]
25+
]
26+
install: [
27+
[make "-C" "quotation" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-template" {= version}
31+
"rocq-metarocq-pcuic" {= version}
32+
"rocq-metarocq-template-pcuic" {= version}
33+
]
34+
synopsis: "Gallina quotation functions for Template Rocq"
35+
description: """
36+
MetaRocq is a meta-programming framework for Rocq.
37+
38+
The Quotation module is geared at providing functions `□T → □□T` for
39+
`□T := Ast.term` (currently implemented) and for `□T := { t : Ast.term
40+
& Σ ;;; [] |- t : T }` (still in the works). Currently `Ast.term →
41+
Ast.term` and `(Σ ;;; [] |- t : T) → Ast.term` functions are provided
42+
for Template and PCUIC terms, in `MetaRocq.Quotation.ToTemplate.All`
43+
and `MetaRocq.Quotation.ToPCUIC.All`. Proving well-typedness is still
44+
a work in progress.
45+
46+
Ultimately the goal of this development is to prove that `□` is a lax monoidal
47+
semicomonad (a functor with `cojoin : □T → □□T` that codistributes over `unit`
48+
and `×`), which is sufficient for proving Löb's theorem.
49+
"""
50+
url {
51+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
52+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
53+
}

‎released/packages/rocq-metarocq-safechecker-plugin/rocq-metarocq-safechecker-plugin.1.4+9.0/opam

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "safechecker-plugin"]
25+
]
26+
install: [
27+
[make "-C" "safechecker-plugin" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-template-pcuic" {= version}
31+
"rocq-metarocq-safechecker" {= version}
32+
]
33+
synopsis: "Implementation and verification of an erasure procedure for Rocq"
34+
description: """
35+
MetaRocq is a meta-programming framework for Rocq.
36+
37+
The Erasure module provides a complete specification of Rocq's so-called
38+
\"extraction\" procedure, starting from the PCUIC calculus and targeting
39+
untyped call-by-value lambda-calculus.
40+
41+
The `erasure` function translates types and proofs in well-typed terms
42+
into a dummy `tBox` constructor, following closely P. Letouzey's PhD
43+
thesis.
44+
"""
45+
url {
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
47+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
48+
}

‎released/packages/rocq-metarocq-safechecker/rocq-metarocq-safechecker.1.4+9.0/opam

+42
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "safechecker"]
25+
]
26+
install: [
27+
[make "-C" "safechecker" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-pcuic" {= version}
31+
]
32+
synopsis: "Implementation and verification of safe conversion and typechecking algorithms for Rocq"
33+
description: """
34+
MetaRocq is a meta-programming framework for Rocq.
35+
36+
The SafeChecker modules provides a correct implementation of
37+
weak-head reduction, conversion and typechecking of Rocq definitions and global environments.
38+
"""
39+
url {
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
41+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
42+
}

‎released/packages/rocq-metarocq-template-pcuic/rocq-metarocq-template-pcuic.1.4+9.0/opam

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://metarocq.github.io/metarocq"
4+
dev-repo: "git+https://github.com/MetaRocq/metarocq.git#main"
5+
bug-reports: "https://github.com/MetaRocq/metarocq/issues"
6+
authors: ["Abhishek Anand <[email protected]>"
7+
"Danil Annenkov <[email protected]>"
8+
"Simon Boulier <[email protected]>"
9+
"Cyril Cohen <[email protected]>"
10+
"Yannick Forster <[email protected]>"
11+
"Jason Gross <[email protected]>"
12+
"Fabian Kunze <[email protected]>"
13+
"Meven Lennon-Bertrand <[email protected]>"
14+
"Kenji Maillard <[email protected]>"
15+
"Gregory Malecha <[email protected]>"
16+
"Jakob Botsch Nielsen <[email protected]>"
17+
"Matthieu Sozeau <[email protected]>"
18+
"Nicolas Tabareau <[email protected]>"
19+
"Théo Winterhalter <[email protected]>"
20+
]
21+
license: "MIT"
22+
build: [
23+
["bash" "./configure.sh"]
24+
[make "-j" "%{jobs}%" "-C" "template-pcuic"]
25+
]
26+
install: [
27+
[make "-C" "template-pcuic" "install"]
28+
]
29+
depends: [
30+
"rocq-metarocq-template" {= version}
31+
"rocq-metarocq-pcuic" {= version}
32+
]
33+
synopsis: "Translations between Template Rocq and PCUIC and proofs of correctness"
34+
description: """
35+
"""
36+
url {
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.4-9.0/v1.4-9.0.tar.gz"
38+
checksum: "sha512=47adfad51b4abaa91bc7875848516e2870b6258ff0c4376ce7afb9d7e3ba209b6501c2506c952f369ec5061d786a474990abb26033a98305b4e3264329f3a1e9"
39+
}

0 commit comments

Comments
 (0)