Skip to content

Commit e6e0f42

Browse files
palmskogpalmskog
committed
add coq-core.8.17.0, coq-stdlib.8.17.0, coq-server.8.17.0, coq.8.17.0
1 parent e395020 commit e6e0f42

File tree

4 files changed

+201
-0
lines changed
  • packages
    • coq-core/coq-core.8.17.0
    • coq-stdlib/coq-stdlib.8.17.0
    • coqide-server/coqide-server.8.17.0
    • coq/coq.8.17.0

4 files changed

+201
-0
lines changed

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

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
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 <[email protected]>"]
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" {>= "2.9"}
29+
"ocaml" {>= "4.09.0"}
30+
"ocamlfind" {>= "1.8.1"}
31+
"zarith" {>= "1.11"}
32+
"ounit2" {with-test}
33+
]
34+
conflicts: [
35+
"coq" { < "8.17" }
36+
"ocaml-option-bytecode-only"
37+
]
38+
build: [
39+
[ "./configure"
40+
"-prefix" prefix
41+
"-mandir" man
42+
"-libdir" "%{lib}%/coq"
43+
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
44+
]
45+
[
46+
"dune"
47+
"build"
48+
"-p"
49+
name
50+
"-j"
51+
jobs
52+
"@install"
53+
"@runtest" {with-test}
54+
"@doc" {with-doc}
55+
]
56+
]
57+
dev-repo: "git+https://github.com/coq/coq.git"
58+
depopts: ["coq-native"]
59+
60+
url {
61+
src: "https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz"
62+
checksum: "sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250"
63+
}

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

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
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 <[email protected]>"]
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" {>= "2.9"}
25+
"coq-core" {= version}
26+
]
27+
build: [
28+
[ "./configure"
29+
"-prefix" prefix
30+
"-mandir" man
31+
"-libdir" "%{lib}%/coq"
32+
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
33+
]
34+
[ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
35+
[
36+
"dune"
37+
"build"
38+
"-p"
39+
name
40+
"-j"
41+
jobs
42+
"@install"
43+
"@runtest" {with-test}
44+
"@doc" {with-doc}
45+
]
46+
]
47+
dev-repo: "git+https://github.com/coq/coq.git"
48+
depopts: ["coq-native"]
49+
50+
url {
51+
src: "https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz"
52+
checksum: "sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250"
53+
}

‎packages/coq/coq.8.17.0/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 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 <[email protected]>"]
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" {>= "2.9"}
22+
"coq-core" {= version}
23+
"coq-stdlib" {= version}
24+
"coqide-server" {= version}
25+
]
26+
build: [
27+
["dune" "subst"] {dev}
28+
[
29+
"dune"
30+
"build"
31+
"-p"
32+
name
33+
"-j"
34+
jobs
35+
"@install"
36+
"@runtest" {with-test}
37+
"@doc" {with-doc}
38+
]
39+
]
40+
dev-repo: "git+https://github.com/coq/coq.git"
41+
42+
url {
43+
src: "https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz"
44+
checksum: "sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250"
45+
}

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

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
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 <[email protected]>"]
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" {>= "2.9"}
21+
"coq-core" {= version}
22+
]
23+
build: [
24+
[
25+
"dune"
26+
"build"
27+
"-p"
28+
name
29+
"-j"
30+
jobs
31+
"@install"
32+
"@doc" {with-doc}
33+
]
34+
]
35+
dev-repo: "git+https://github.com/coq/coq.git"
36+
37+
url {
38+
src: "https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz"
39+
checksum: "sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250"
40+
}

0 commit comments

Comments
 (0)