Skip to content

Commit eb68ba7

Browse files
mattam82mattam82
authored
Merge pull request #27613 from mattam82/rocq-9.0-release
Rocq 9.0 release + Coq 9.0 compatibility packages
1 parent 6ccbe63 commit eb68ba7

File tree

8 files changed

+329
-0
lines changed
  • packages
    • coq-core/coq-core.9.0.0
    • coq-stdlib/coq-stdlib.9.0.0
    • coqide-server/coqide-server.9.0.0
    • coq/coq.9.0.0
    • rocq-core/rocq-core.9.0.0
    • rocq-prover/rocq-prover.9.0.0
    • rocq-runtime/rocq-runtime.9.0.0
    • rocq-stdlib/rocq-stdlib.9.0.0

8 files changed

+329
-0
lines changed

‎packages/coq-core/coq-core.9.0.0/opam

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
opam-version: "2.0"
2+
synopsis: "Compatibility binaries for Coq after the Rocq renaming"
3+
description: """
4+
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
Typical applications include the certification of properties of
10+
programming languages (e.g. the CompCert compiler certification
11+
project, or the Bedrock verified low-level programming library), the
12+
formalization of mathematics (e.g. the full formalization of the
13+
Feit-Thompson theorem or homotopy type theory) and teaching.
14+
15+
This package includes compatibility binaries to call Rocq
16+
through previous Coq commands like coqc coqtop,..."""
17+
maintainer: ["The Rocq development team <[email protected]>"]
18+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
19+
license: "LGPL-2.1-only"
20+
homepage: "https://rocq-prover.org/"
21+
doc: "https://coq.github.io/doc/"
22+
bug-reports: "https://github.com/coq/coq/issues"
23+
depends: [
24+
"dune" {>= "3.8"}
25+
"rocq-runtime" {= version}
26+
"odoc" {with-doc}
27+
]
28+
dev-repo: "git+https://github.com/coq/coq.git"
29+
build: [
30+
["dune" "subst"] {dev}
31+
[
32+
"dune"
33+
"build"
34+
"-p"
35+
name
36+
"-j"
37+
jobs
38+
"@install"
39+
"@runtest" {with-test}
40+
"@doc" {with-doc}
41+
]
42+
]
43+
44+
url {
45+
src:
46+
"https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
47+
checksum: [
48+
"md5=8d522602d23e7a665631826dab9aa92b"
49+
"sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
50+
]
51+
}
52+
53+
post-messages: [
54+
"Coq has been renamed to The Rocq Prover, see https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details.
55+
This package provides compatibility binaries to ease the transition to the new rocq binary."]

‎packages/coq-stdlib/coq-stdlib.9.0.0/opam

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
opam-version: "2.0"
2+
synopsis: "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"
3+
maintainer: ["The Rocq standard library development team"]
4+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
5+
license: "LGPL-2.1-only"
6+
homepage: "https://coq.inria.fr/"
7+
doc: "https://coq.github.io/doc/"
8+
bug-reports: "https://github.com/coq/stdlib/issues"
9+
depends: [
10+
"coq-core"
11+
"rocq-stdlib" {= version}
12+
]
13+
dev-repo: "git+https://github.com/coq/stdlib.git"

‎packages/coq/coq.9.0.0/opam

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
opam-version: "2.0"
2+
synopsis: "Compatibility metapackage for Coq after the Rocq renaming"
3+
maintainer: ["The Rocq development team <[email protected]>"]
4+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
5+
license: "LGPL-2.1-only"
6+
homepage: "https://coq.inria.fr/"
7+
doc: "https://coq.github.io/doc/"
8+
bug-reports: "https://github.com/coq/coq/issues"
9+
depends: [
10+
"dune" {>= "3.8"}
11+
"rocq-prover" {= version}
12+
"coq-core" {= version}
13+
"coq-stdlib" {= "9.0.0"}
14+
"coqide-server" {= version}
15+
"odoc" {with-doc}
16+
]

‎packages/coqide-server/coqide-server.9.0.0/opam

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Prover, XML protocol server"
3+
description: """
4+
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
This package provides the `coqidetop` language server, an
10+
implementation of Rocq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
11+
which allows clients, such as RocqIDE, to interact with the Rocq Prover in a
12+
structured way."""
13+
maintainer: ["The Rocq development team <[email protected]>"]
14+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
15+
license: "LGPL-2.1-only"
16+
homepage: "https://coq.inria.fr/"
17+
doc: "https://coq.github.io/doc/"
18+
bug-reports: "https://github.com/coq/coq/issues"
19+
depends: [
20+
"dune" {>= "3.8"}
21+
"rocq-runtime" {= version}
22+
"odoc" {with-doc}
23+
]
24+
build: [
25+
["dune" "subst"] {dev}
26+
[
27+
"dune"
28+
"build"
29+
"-p"
30+
name
31+
"-j"
32+
jobs
33+
"@install"
34+
"@runtest" {with-test}
35+
"@doc" {with-doc}
36+
]
37+
]
38+
dev-repo: "git+https://github.com/coq/coq.git"
39+
40+
url {
41+
src:
42+
"https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
43+
checksum: [
44+
"md5=8d522602d23e7a665631826dab9aa92b"
45+
"sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
46+
]
47+
}

‎packages/rocq-core/rocq-core.9.0.0/opam

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Prover with its prelude"
3+
description: """
4+
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
Typical applications include the certification of properties of
10+
programming languages (e.g. the CompCert compiler certification
11+
project, or the Bedrock verified low-level programming library), the
12+
formalization of mathematics (e.g. the full formalization of the
13+
Feit-Thompson theorem or homotopy type theory) and teaching.
14+
15+
This package includes the Rocq prelude, that is loaded automatically
16+
by Rocq in every .v file, as well as other modules bound to the
17+
Corelib.* and Ltac2.* namespaces."""
18+
maintainer: ["The Rocq development team <[email protected]>"]
19+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
20+
license: "LGPL-2.1-only"
21+
homepage: "https://rocq-prover.org"
22+
doc: "https://coq.github.io/doc/"
23+
bug-reports: "https://github.com/coq/coq/issues"
24+
depends: [
25+
"dune" {>= "3.8"}
26+
"rocq-runtime" {= version}
27+
"odoc" {with-doc}
28+
]
29+
dev-repo: "git+https://github.com/coq/coq.git"
30+
build: [
31+
["dune" "subst"] {dev}
32+
# We tell dunestrap to use coq-config from rocq-runtime
33+
[ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"]
34+
[
35+
"dune"
36+
"build"
37+
"-p"
38+
name
39+
"-j"
40+
jobs
41+
"--promote-install-files=false"
42+
"@install"
43+
"@runtest" {with-test}
44+
"@doc" {with-doc}
45+
]
46+
["dune" "install" "-p" name "--create-install-files" name]
47+
]
48+
49+
url {
50+
src:
51+
"https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
52+
checksum: [
53+
"md5=8d522602d23e7a665631826dab9aa92b"
54+
"sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
55+
]
56+
}

‎packages/rocq-prover/rocq-prover.9.0.0/opam

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Prover with Stdlib"
3+
description: """
4+
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
Typical applications include the certification of properties of
10+
programming languages (e.g. the CompCert compiler certification
11+
project, or the Bedrock verified low-level programming library), the
12+
formalization of mathematics (e.g. the full formalization of the
13+
Feit-Thompson theorem or homotopy type theory) and teaching.
14+
15+
This package is a virtual package gathering the rocq-core and rocq-stdlib packages."""
16+
maintainer: ["The Rocq development team <[email protected]>"]
17+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
18+
license: "LGPL-2.1-only"
19+
homepage: "https://rocq-prover.org"
20+
doc: "https://coq.github.io/doc/"
21+
bug-reports: "https://github.com/coq/coq/issues"
22+
depends: [
23+
"dune" {>= "3.8"}
24+
"rocq-core" {= version}
25+
"rocq-stdlib"
26+
"ounit2" {with-test}
27+
"conf-python-3" {with-test}
28+
"conf-time" {with-test}
29+
"odoc" {with-doc}
30+
]
31+
dev-repo: "git+https://github.com/coq/coq.git"

‎packages/rocq-runtime/rocq-runtime.9.0.0/opam

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Prover -- Core Binaries and Tools"
3+
description: """
4+
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
Typical applications include the certification of properties of
10+
programming languages (e.g. the CompCert compiler certification
11+
project, or the Bedrock verified low-level programming library), the
12+
formalization of mathematics (e.g. the full formalization of the
13+
Feit-Thompson theorem or homotopy type theory) and teaching.
14+
15+
This package includes the Rocq Prover core binaries, plugins, and tools, but
16+
not the vernacular standard library.
17+
18+
Note that in this setup, Rocq needs to be started with the -boot and
19+
-noinit options, as will otherwise fail to find the regular Rocq
20+
prelude, now living in the rocq-core package."""
21+
maintainer: ["The Rocq development team <[email protected]>"]
22+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
23+
license: "LGPL-2.1-only"
24+
homepage: "https://rocq-prover.org"
25+
doc: "https://coq.github.io/doc/"
26+
bug-reports: "https://github.com/coq/coq/issues"
27+
depends: [
28+
"dune" {>= "3.8"}
29+
"ocaml" {>= "4.09.0"}
30+
"ocamlfind" {>= "1.8.1"}
31+
"zarith" {>= "1.11"}
32+
"conf-linux-libc-dev" {os = "linux"}
33+
"odoc" {with-doc}
34+
]
35+
depopts: ["rocq-native" "memprof-limits" "memtrace"]
36+
conflicts: [
37+
"coq" { < "8.17" }
38+
"coq-core" { < "8.21" }
39+
]
40+
dev-repo: "git+https://github.com/coq/coq.git"
41+
build: [
42+
["dune" "subst"] {dev}
43+
[ "./configure"
44+
"-release" # -release must be the first command line argument
45+
"-prefix" prefix
46+
"-mandir" man
47+
"-libdir" "%{lib}%/coq"
48+
"-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
49+
]
50+
[
51+
"dune"
52+
"build"
53+
"-p"
54+
name
55+
"-j"
56+
jobs
57+
"--promote-install-files=false"
58+
"@install"
59+
"@runtest" {with-test}
60+
"@doc" {with-doc}
61+
]
62+
["dune" "install" "-p" name "--create-install-files" name]
63+
]
64+
65+
url {
66+
src:
67+
"https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
68+
checksum: [
69+
"md5=8d522602d23e7a665631826dab9aa92b"
70+
"sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
71+
]
72+
}

‎packages/rocq-stdlib/rocq-stdlib.9.0.0/opam

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Proof Assistant -- Standard Library"
3+
description: """
4+
Rocq is a formal proof management system. It provides
5+
a formal language to write mathematical definitions, executable
6+
algorithms and theorems together with an environment for
7+
semi-interactive development of machine-checked proofs.
8+
9+
Typical applications include the certification of properties of
10+
programming languages (e.g. the CompCert compiler certification
11+
project, or the Bedrock verified low-level programming library), the
12+
formalization of mathematics (e.g. the full formalization of the
13+
Feit-Thompson theorem or homotopy type theory) and teaching.
14+
15+
This package includes the Rocq Standard Library, that is to say, the
16+
set of modules usually bound to the Stdlib.* namespace."""
17+
maintainer: ["The Rocq standard library development team"]
18+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
19+
license: "LGPL-2.1-only"
20+
homepage: "https://rocq-prover.org"
21+
doc: "https://coq.github.io/doc/"
22+
bug-reports: "https://github.com/coq/stdlib/issues"
23+
depends: [
24+
"rocq-runtime"
25+
"rocq-core" {>= "9.0" & < "9.1~"}
26+
]
27+
dev-repo: "git+https://github.com/coq/stdlib.git"
28+
build: [
29+
[make "-j" jobs]
30+
]
31+
install: [
32+
[make "install"]
33+
]
34+
35+
url {
36+
src:
37+
"https://github.com/coq/stdlib/releases/download/V9.0.0/stdlib-9.0.0.tar.gz"
38+
checksum: "sha512=97faa80d63a398c2c6872e043d65b1b907bb01ec3ea42f35cf757b3457b8fa2b64475d1577000ce2dea2c3f93e59e36cc5af9864adacf47f92db96ecbe307a45"
39+
}

0 commit comments

Comments
 (0)