this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The Rocq Prover -- Core Binaries and Tools"
3description: """
4The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
5a formal language to write mathematical definitions, executable
6algorithms and theorems together with an environment for
7semi-interactive development of machine-checked proofs.
8
9Typical applications include the certification of properties of
10programming languages (e.g. the CompCert compiler certification
11project, or the Bedrock verified low-level programming library), the
12formalization of mathematics (e.g. the full formalization of the
13Feit-Thompson theorem or homotopy type theory) and teaching.
14
15This package includes the Rocq Prover core binaries, plugins, and tools, but
16not the vernacular standard library.
17
18Note 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
20prelude, now living in the rocq-core package."""
21maintainer: ["The Rocq development team <coqdev@inria.fr>"]
22authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
23license: "LGPL-2.1-only"
24homepage: "https://rocq-prover.org"
25doc: "https://coq.github.io/doc/"
26bug-reports: "https://github.com/coq/coq/issues"
27depends: [
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]
35depopts: ["rocq-native" "memprof-limits" "memtrace"]
36conflicts: [
37 "coq" { < "8.17" }
38 "coq-core" { < "8.21" }
39]
40dev-repo: "git+https://github.com/coq/coq.git"
41build: [
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
65url {
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}