Skip to content

Commit 7abf260

Browse files
avsmavsm
authored
Merge pull request #24378 from gares/opam-publish-coq.8.18.0
5 packages from coq/coq at 8.18.0
2 parents 1a5f809 + 2603bb6 commit 7abf260

File tree

5 files changed

+275
-0
lines changed
  • packages
    • coq-core/coq-core.8.18.0
    • coq-stdlib/coq-stdlib.8.18.0
    • coqide-server/coqide-server.8.18.0
    • coqide/coqide.8.18.0
    • coq/coq.8.18.0

5 files changed

+275
-0
lines changed

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

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

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
# This file is generated by dune, edit dune-project instead
2+
opam-version: "2.0"
3+
synopsis: "The Coq Proof Assistant -- Standard Library"
4+
description: """
5+
Coq is a formal proof management system. It provides
6+
a formal language to write mathematical definitions, executable
7+
algorithms and theorems together with an environment for
8+
semi-interactive development of machine-checked proofs.
9+
10+
Typical applications include the certification of properties of
11+
programming languages (e.g. the CompCert compiler certification
12+
project, or the Bedrock verified low-level programming library), the
13+
formalization of mathematics (e.g. the full formalization of the
14+
Feit-Thompson theorem or homotopy type theory) and teaching.
15+
16+
This package includes the Coq Standard Library, that is to say, the
17+
set of modules usually bound to the Coq.* namespace."""
18+
maintainer: ["The Coq development team <[email protected]>"]
19+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
20+
license: "LGPL-2.1-only"
21+
homepage: "https://coq.inria.fr/"
22+
doc: "https://coq.github.io/doc/"
23+
bug-reports: "https://github.com/coq/coq/issues"
24+
depends: [
25+
"dune" {>= "2.9"}
26+
"coq-core" {= version}
27+
]
28+
build: [
29+
# Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
30+
# ["dune" "subst"] {pinned}
31+
#
32+
# XXX need to run configure as in coq-core, or else dunestrap will
33+
# use the default rule in config
34+
[ "./configure"
35+
"-prefix" prefix
36+
"-mandir" man
37+
"-libdir" "%{lib}%/coq"
38+
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
39+
]
40+
[ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
41+
[
42+
"dune"
43+
"build"
44+
"-p"
45+
name
46+
"-j"
47+
jobs
48+
"@install"
49+
"@runtest" {with-test}
50+
"@doc" {with-doc}
51+
]
52+
]
53+
dev-repo: "git+https://github.com/coq/coq.git"
54+
depopts: ["coq-native"]
55+
url {
56+
src:
57+
"https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
58+
checksum: [
59+
"md5=8d852367b54f095d9fbabd000304d450"
60+
"sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50"
61+
]
62+
}

‎packages/coq/coq.8.18.0/opam‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
# This file is generated by dune, edit dune-project instead
2+
opam-version: "2.0"
3+
synopsis: "The Coq Proof Assistant"
4+
description: """
5+
Coq is a formal proof management system. It provides
6+
a formal language to write mathematical definitions, executable
7+
algorithms and theorems together with an environment for
8+
semi-interactive development of machine-checked proofs.
9+
10+
Typical applications include the certification of properties of
11+
programming languages (e.g. the CompCert compiler certification
12+
project, or the Bedrock verified low-level programming library), the
13+
formalization of mathematics (e.g. the full formalization of the
14+
Feit-Thompson theorem or homotopy type theory) and teaching."""
15+
maintainer: ["The Coq development team <[email protected]>"]
16+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
17+
license: "LGPL-2.1-only"
18+
homepage: "https://coq.inria.fr/"
19+
doc: "https://coq.github.io/doc/"
20+
bug-reports: "https://github.com/coq/coq/issues"
21+
depends: [
22+
"dune" {>= "2.9"}
23+
"coq-core" {= version}
24+
"coq-stdlib" {= version}
25+
"coqide-server" {= version}
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/coq/coq.git"
42+
url {
43+
src:
44+
"https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
45+
checksum: [
46+
"md5=8d852367b54f095d9fbabd000304d450"
47+
"sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50"
48+
]
49+
}

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

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# This file is generated by dune, edit dune-project instead
2+
opam-version: "2.0"
3+
synopsis: "The Coq Proof Assistant, XML protocol server"
4+
description: """
5+
Coq is a formal proof management system. It provides
6+
a formal language to write mathematical definitions, executable
7+
algorithms and theorems together with an environment for
8+
semi-interactive development of machine-checked proofs.
9+
10+
This package provides the `coqidetop` language server, an
11+
implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
12+
which allows clients, such as CoqIDE, to interact with Coq in a
13+
structured way."""
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+
]
24+
build: [
25+
# Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
26+
# ["dune" "subst"] {pinned}
27+
[
28+
"dune"
29+
"build"
30+
"-p"
31+
name
32+
"-j"
33+
jobs
34+
"@install"
35+
"@doc" {with-doc}
36+
]
37+
]
38+
dev-repo: "git+https://github.com/coq/coq.git"
39+
url {
40+
src:
41+
"https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
42+
checksum: [
43+
"md5=8d852367b54f095d9fbabd000304d450"
44+
"sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50"
45+
]
46+
}

‎packages/coqide/coqide.8.18.0/opam‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# This file is generated by dune, edit dune-project instead
2+
opam-version: "2.0"
3+
synopsis: "The Coq Proof Assistant --- GTK3 IDE"
4+
description: """
5+
Coq is a formal proof management system. It provides
6+
a formal language to write mathematical definitions, executable
7+
algorithms and theorems together with an environment for
8+
semi-interactive development of machine-checked proofs.
9+
10+
This package provides the CoqIDE, a graphical user interface for the
11+
development of interactive proofs."""
12+
maintainer: ["The Coq development team <[email protected]>"]
13+
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
14+
license: "LGPL-2.1-only"
15+
homepage: "https://coq.inria.fr/"
16+
doc: "https://coq.github.io/doc/"
17+
bug-reports: "https://github.com/coq/coq/issues"
18+
depends: [
19+
"dune" {>= "2.9"}
20+
"ocamlfind" {build}
21+
"conf-findutils" {build}
22+
"conf-adwaita-icon-theme"
23+
"coqide-server" {= version}
24+
"cairo2" {>= "0.6.4"}
25+
"lablgtk3-sourceview3" {>= "3.1.2"}
26+
]
27+
build: [
28+
# Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
29+
# ["dune" "subst"] {pinned}
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/coq/coq.git"
43+
url {
44+
src:
45+
"https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
46+
checksum: [
47+
"md5=8d852367b54f095d9fbabd000304d450"
48+
"sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50"
49+
]
50+
}

0 commit comments

Comments
 (0)