Skip to content

Commit 6ed188d

Browse files
mserimseri
authored
Merge pull request #27278 from proux01/coq_8_20_1
Add Coq 8.20.1
2 parents 1c403b8 + 516d043 commit 6ed188d

File tree

4 files changed

+220
-0
lines changed
  • packages
    • coq/coq.8.20.1
    • coq-core/coq-core.8.20.1
    • coq-stdlib/coq-stdlib.8.20.1
    • coqide-server/coqide-server.8.20.1

4 files changed

+220
-0
lines changed

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

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
opam-version: "2.0"
2+
synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
3+
description: """
4+
Coq 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 Coq core binaries, plugins, and tools, but
16+
not the vernacular standard library.
17+
18+
Note that in this setup, Coq needs to be started with the -boot and
19+
-noinit options, as will otherwise fail to find the regular Coq
20+
prelude, now living in the coq-stdlib package."""
21+
maintainer: ["The Coq development team <coqdev@inria.fr>"]
22+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
23+
license: "LGPL-2.1-only"
24+
homepage: "https://coq.inria.fr/"
25+
doc: "https://coq.github.io/doc/"
26+
bug-reports: "https://github.com/coq/coq/issues"
27+
depends: [
28+
"dune" {>= "3.6.1"}
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+
conflicts: [
36+
"coq" { < "8.17" }
37+
]
38+
depopts: ["coq-native" "memprof-limits" "memtrace"]
39+
dev-repo: "git+https://github.com/coq/coq.git"
40+
build: [
41+
["dune" "subst"] {dev}
42+
[ "./configure"
43+
"-prefix" prefix
44+
"-mandir" man
45+
"-libdir" "%{lib}%/coq"
46+
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
47+
]
48+
[
49+
"dune"
50+
"build"
51+
"-p"
52+
name
53+
"-j"
54+
jobs
55+
"--promote-install-files=false"
56+
"@install"
57+
"@runtest" {with-test}
58+
"@doc" {with-doc}
59+
]
60+
["dune" "install" "-p" name "--create-install-files" name]
61+
]
62+
63+
url {
64+
src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
65+
checksum: [
66+
"md5=0cfaa70f569be9494d24c829e6555d46"
67+
"sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
68+
]
69+
}

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

+55
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
opam-version: "2.0"
2+
synopsis: "The Coq Proof Assistant -- Standard Library"
3+
description: """
4+
Coq 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 Coq Standard Library, that is to say, the
16+
set of modules usually bound to the Coq.* namespace."""
17+
maintainer: ["The Coq development team <coqdev@inria.fr>"]
18+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
19+
license: "LGPL-2.1-only"
20+
homepage: "https://coq.inria.fr/"
21+
doc: "https://coq.github.io/doc/"
22+
bug-reports: "https://github.com/coq/coq/issues"
23+
depends: [
24+
"dune" {>= "3.6"}
25+
"coq-core" {= version}
26+
"odoc" {with-doc}
27+
]
28+
depopts: ["coq-native"]
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 coq-core
33+
[ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
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: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
51+
checksum: [
52+
"md5=0cfaa70f569be9494d24c829e6555d46"
53+
"sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
54+
]
55+
}

‎packages/coq/coq.8.20.1/opam

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
opam-version: "2.0"
2+
synopsis: "The Coq Proof Assistant"
3+
description: """
4+
Coq 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+
maintainer: ["The Coq development team <coqdev@inria.fr>"]
15+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
16+
license: "LGPL-2.1-only"
17+
homepage: "https://coq.inria.fr/"
18+
doc: "https://coq.github.io/doc/"
19+
bug-reports: "https://github.com/coq/coq/issues"
20+
depends: [
21+
"dune" {>= "3.6"}
22+
"coq-core" {= version}
23+
"coq-stdlib" {= version}
24+
"coqide-server" {= version}
25+
"odoc" {with-doc}
26+
]
27+
dev-repo: "git+https://github.com/coq/coq.git"
28+
build: [
29+
["dune" "subst"] {dev}
30+
[
31+
"dune"
32+
"build"
33+
"-p"
34+
name
35+
"-j"
36+
jobs
37+
"--promote-install-files=false"
38+
"@install"
39+
"@doc" {with-doc}
40+
]
41+
["dune" "install" "-p" name "--create-install-files" name]
42+
]
43+
44+
url {
45+
src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
46+
checksum: [
47+
"md5=0cfaa70f569be9494d24c829e6555d46"
48+
"sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
49+
]
50+
}

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

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
opam-version: "2.0"
2+
synopsis: "The Coq Proof Assistant, XML protocol server"
3+
description: """
4+
Coq 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+
This package provides the `coqidetop` language server, an
10+
implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
11+
which allows clients, such as CoqIDE, to interact with Coq in a
12+
structured way."""
13+
maintainer: ["The Coq development team <coqdev@inria.fr>"]
14+
authors: ["The Coq 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.6"}
21+
"coq-core" {= 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: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
42+
checksum: [
43+
"md5=0cfaa70f569be9494d24c829e6555d46"
44+
"sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
45+
]
46+
}

0 commit comments

Comments
 (0)