Skip to content

Commit 66e6029

Browse files
silenesilene
committed
Add Rocq 9.1+rc1
1 parent f6368c6 commit 66e6029

File tree

8 files changed

+319
-1
lines changed
  • packages
    • coq-core/coq-core.9.1+rc1
    • coq-lsp/coq-lsp.0.2.3+9.0
    • coqide-server/coqide-server.9.1+rc1
    • coq/coq.9.1+rc1
    • rocq-core/rocq-core.9.1+rc1
    • rocq-devtools/rocq-devtools.9.1+rc1
    • rocq-runtime/rocq-runtime.9.1+rc1
    • rocqide/rocqide.9.1+rc1

8 files changed

+319
-1
lines changed

‎packages/coq-core/coq-core.9.1+rc1/opam

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
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://rocq-prover.org/docs/"
22+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
23+
depends: [
24+
"dune" {>= "3.8"}
25+
"rocq-runtime" {= version}
26+
"odoc" {with-doc}
27+
]
28+
build: [
29+
["dune" "subst"] {dev}
30+
[
31+
"dune"
32+
"build"
33+
"-p"
34+
name
35+
"-j"
36+
jobs
37+
"@install"
38+
"@runtest" {with-test}
39+
"@doc" {with-doc}
40+
]
41+
]
42+
dev-repo: "git+https://github.com/rocq-prover/rocq.git"
43+
post-messages: [
44+
"Coq has been renamed to The Rocq Prover, see https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details.
45+
This package provides compatibility binaries to ease the transition to the new rocq binary."
46+
]
47+
url {
48+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
49+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
50+
}

‎packages/coq-lsp/coq-lsp.0.2.3+9.0/opam

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ depends: [
3636
# unit testing
3737
"ppx_inline_test" { >= "v0.15.0" }
3838

39-
"rocq-prover" { >= "9.0" < "9.1" }
39+
"rocq-core" { >= "9.0" < "9.1" }
40+
"rocq-stdlib"
4041

4142
# [release branch] Remove
4243
"ocamlfind" {>= "1.9.1" & (>= "1.9.8" | os != "windows") }

‎packages/coq/coq.9.1+rc1/opam

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
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://rocq-prover.org/"
7+
doc: "https://rocq-prover.org/docs/"
8+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
9+
depends: [
10+
"coq-core" {= version}
11+
"coq-stdlib" {= "9.0.0"}
12+
"coqide-server" {= version}
13+
]
14+
dev-repo: "git+https://github.com/rocq-prover/rocq.git"

‎packages/coqide-server/coqide-server.9.1+rc1/opam

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
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/rocq-prover/rocq/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://rocq-prover.org/"
17+
doc: "https://rocq-prover.org/docs/"
18+
bug-reports: "https://github.com/rocq-prover/rocq/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/rocq-prover/rocq.git"
39+
url {
40+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
41+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
42+
}

‎packages/rocq-core/rocq-core.9.1+rc1/opam

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
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://rocq-prover.org/docs/"
23+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
24+
depends: [
25+
"dune" {>= "3.8"}
26+
"rocq-runtime" {= version}
27+
"odoc" {with-doc}
28+
]
29+
dev-repo: "git+https://github.com/rocq-prover/rocq.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+
url {
49+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
50+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
51+
}

‎packages/rocq-devtools/rocq-devtools.9.1+rc1/opam

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
opam-version: "2.0"
2+
synopsis: "Development tools for Rocq"
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 tools to help when developing Rocq projects
16+
(timelog2html)."""
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://rocq-prover.org/docs/"
22+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
23+
depends: [
24+
"dune" {>= "3.8"}
25+
"rocq-runtime" {= version}
26+
"yojson" {>= "2.0"}
27+
"camlzip"
28+
"odoc" {with-doc}
29+
]
30+
build: [
31+
["dune" "subst"] {dev}
32+
[
33+
"dune"
34+
"build"
35+
"-p"
36+
name
37+
"-j"
38+
jobs
39+
"@install"
40+
"@runtest" {with-test}
41+
"@doc" {with-doc}
42+
]
43+
]
44+
dev-repo: "git+https://github.com/rocq-prover/rocq.git"
45+
url {
46+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
47+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
48+
}

‎packages/rocq-runtime/rocq-runtime.9.1+rc1/opam

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
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://rocq-prover.org/docs/"
26+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
27+
depends: [
28+
"dune" {>= "3.8"}
29+
"ocaml" {>= "4.14.0"}
30+
"ocamlfind" {>= "1.9.1" & (>= "1.9.8" | os != "windows")}
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/rocq-prover/rocq.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+
url {
65+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
66+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
67+
}

‎packages/rocqide/rocqide.9.1+rc1/opam

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
opam-version: "2.0"
2+
synopsis: "The Rocq Prover --- GTK3 IDE"
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 RocqIDE, a graphical user interface for the
10+
development of interactive proofs."""
11+
maintainer: ["The Rocq development team <[email protected]>"]
12+
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
13+
license: "LGPL-2.1-only"
14+
homepage: "https://rocq-prover.org/"
15+
doc: "https://rocq-prover.org/docs/"
16+
bug-reports: "https://github.com/rocq-prover/rocq/issues"
17+
depends: [
18+
"dune" {>= "3.8"}
19+
"ocamlfind" {build}
20+
"conf-findutils" {build}
21+
"conf-adwaita-icon-theme"
22+
"coqide-server" {= version}
23+
"cairo2" {>= "0.6.4"}
24+
"lablgtk3-sourceview3" {>= "3.1.2" & (>= "3.1.5" | os != "windows")}
25+
"odoc" {with-doc}
26+
]
27+
build: [
28+
["dune" "subst"] {dev}
29+
[
30+
"dune"
31+
"build"
32+
"-p"
33+
name
34+
"-j"
35+
jobs
36+
"@install"
37+
"@runtest" {with-test}
38+
"@doc" {with-doc}
39+
]
40+
]
41+
dev-repo: "git+https://github.com/rocq-prover/rocq.git"
42+
url {
43+
src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
44+
checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
45+
}

0 commit comments

Comments
 (0)