this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The Rocq Proof Assistant -- Standard Library"
3description: """
4Rocq is a formal proof management system. 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 Standard Library, that is to say, the
16set of modules usually bound to the Stdlib.* namespace."""
17maintainer: ["The Rocq standard library development team"]
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/stdlib/issues"
23depends: [
24 "rocq-runtime"
25 "rocq-core" {>= "9.0" & < "9.1~"}
26]
27dev-repo: "git+https://github.com/coq/stdlib.git"
28build: [
29 [make "-j" jobs]
30]
31install: [
32 [make "install"]
33]
34
35url {
36 src:
37 "https://github.com/coq/stdlib/releases/download/V9.0.0/stdlib-9.0.0.tar.gz"
38 checksum: "sha512=97faa80d63a398c2c6872e043d65b1b907bb01ec3ea42f35cf757b3457b8fa2b64475d1577000ce2dea2c3f93e59e36cc5af9864adacf47f92db96ecbe307a45"
39}