1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
(lang dune 3.8)
(name rocq-stdlib)
; We use directory targets in documentation
(using directory-targets 0.1)
(using coq 0.8)
(formatting
(enabled_for ocaml))
(generate_opam_files true)
(license LGPL-2.1-only)
(maintainers "The Rocq standard library development team")
(authors "The Rocq development team, INRIA, CNRS, and contributors")
; This generates bug-reports and dev-repo
(source (github coq/stdlib))
(homepage https://coq.inria.fr/)
(documentation "https://coq.github.io/doc/")
(version dev)
(package
(name rocq-stdlib)
(depends
rocq-runtime
(rocq-core (= :version)))
(synopsis "The Rocq Proof Assistant -- Standard Library")
(description "Rocq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching.
This package includes the Rocq Standard Library, that is to say, the
set of modules usually bound to the Stdlib.* namespace."))
(package
(name coq-stdlib)
(allow_empty)
(depends
coq-core
(rocq-stdlib (= :version)))
(synopsis "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"))
(package
(name rocq-stdlib-doc)
(license "OPUBL-1.0")
(depends
(conf-python-3 :build)
(rocq (and :build (= :version))))
(synopsis "The Rocq Proof Assistant Standard Library --- Reference Manual")
(description "Rocq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
This package provides the Reference Manual for the Standard Library."))
|
