this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "Compatibility binaries for Coq after the Rocq renaming"
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 compatibility binaries to call Rocq
16through previous Coq commands like coqc coqtop,..."""
17maintainer: ["The Rocq development team <coqdev@inria.fr>"]
18authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
19license: "LGPL-2.1-only"
20homepage: "https://rocq-prover.org/"
21doc: "https://coq.github.io/doc/"
22bug-reports: "https://github.com/coq/coq/issues"
23depends: [
24 "dune" {>= "3.8"}
25 "rocq-runtime" {= version}
26 "odoc" {with-doc}
27]
28dev-repo: "git+https://github.com/coq/coq.git"
29build: [
30 ["dune" "subst"] {dev}
31 [
32 "dune"
33 "build"
34 "-p"
35 name
36 "-j"
37 jobs
38 "@install"
39 "@runtest" {with-test}
40 "@doc" {with-doc}
41 ]
42]
43
44url {
45 src:
46 "https://github.com/coq/coq/releases/download/V9.0.0/rocq-9.0.0.tar.gz"
47 checksum: [
48 "md5=8d522602d23e7a665631826dab9aa92b"
49 "sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be"
50 ]
51}
52
53post-messages: [
54 "Coq has been renamed to The Rocq Prover, see https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details.
55 This package provides compatibility binaries to ease the transition to the new rocq binary."]