this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The Rocq Prover with its prelude"
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 prelude, that is loaded automatically
16by Rocq in every .v file, as well as other modules bound to the
17Corelib.* and Ltac2.* namespaces."""
18maintainer: ["The Rocq development team <coqdev@inria.fr>"]
19authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
20license: "LGPL-2.1-only"
21homepage: "https://rocq-prover.org"
22doc: "https://coq.github.io/doc/"
23bug-reports: "https://github.com/coq/coq/issues"
24depends: [
25 "dune" {>= "3.8"}
26 "rocq-runtime" {= version}
27 "odoc" {with-doc}
28]
29dev-repo: "git+https://github.com/coq/coq.git"
30build: [
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
49url {
50 src:
51 "https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
52 checksum: [
53 "md5=8d522602d23e7a665631826dab9aa92b"
54 "sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
55 ]
56}