Skip to content

Commit e64810d

Browse files
proux01proux01
authored
Merge pull request #112 from mattam82/stdlib-rocq-manual
Stdlib rocq manual
2 parents 4546804 + 3d1cb1c commit e64810d

File tree

6 files changed

+129
-9
lines changed

6 files changed

+129
-9
lines changed

‎.gitignore‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,6 @@ config/coq_config.py
5959
config/dune.c_flags
6060
ide/coqide/config.ml
6161
dev/ocamldebug-coq
62-
coqdoc.sty
63-
coqdoc.css
6462
time-of-build*.log
6563
time-of-build*.log2
6664
time-of-build*.log3
@@ -166,3 +164,5 @@ user-contrib/Ltac2/dune
166164

167165
.wrappers
168166
rocq-stdlib-doc.opam
167+
doc/stdlib/Library.fdb_latexmk
168+
doc/stdlib/Library.fls

‎doc/common/macros.tex‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@
9191
%%%%%%%%%%%%%%%%%%%%%%%%
9292

9393
\newcommand{\Coq}{\textsc{Coq}}
94+
\newcommand{\Rocq}{\textsc{Rocq}}
9495
\newcommand{\gallina}{\textsc{Gallina}}
9596
\newcommand{\Gallina}{\textsc{Gallina}}
9697
\newcommand{\CoqIDE}{\textsc{CoqIDE}}

‎doc/sphinx/_static/coqdoc.css‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/************************************************************************/
2+
/* * The Rocq Prover / The Rocq Development Team */
3+
/* v * Copyright INRIA, CNRS and contributors */
4+
/* <O___,, * (see version control and CREDITS file for authors & dates) */
5+
/* \VV/ **************************************************************/
6+
/* // * This file is distributed under the terms of the */
7+
/* * GNU Lesser General Public License Version 2.1 */
8+
/* * (see LICENSE file for the text of the license) */
9+
/************************************************************************/
10+
/* Taken from CoqDoc's default stylesheet */
11+
12+
.coqdoc-constructor {
13+
color: rgb(60%,0%,0%);
14+
}
15+
16+
.coqdoc-var {
17+
color: rgb(40%,0%,40%);
18+
}
19+
20+
.coqdoc-variable {
21+
color: rgb(40%,0%,40%);
22+
}
23+
24+
.coqdoc-definition {
25+
color: rgb(0%,40%,0%);
26+
}
27+
28+
.coqdoc-abbreviation {
29+
color: rgb(0%,40%,0%);
30+
}
31+
32+
.coqdoc-lemma {
33+
color: rgb(0%,40%,0%);
34+
}
35+
36+
.coqdoc-instance {
37+
color: rgb(0%,40%,0%);
38+
}
39+
40+
.coqdoc-projection {
41+
color: rgb(0%,40%,0%);
42+
}
43+
44+
.coqdoc-method {
45+
color: rgb(0%,40%,0%);
46+
}
47+
48+
.coqdoc-inductive {
49+
color: rgb(0%,0%,80%);
50+
}
51+
52+
.coqdoc-record {
53+
color: rgb(0%,0%,80%);
54+
}
55+
56+
.coqdoc-class {
57+
color: rgb(0%,0%,80%);
58+
}
59+
60+
.coqdoc-keyword {
61+
color : #cf1d1d;
62+
}
63+
64+
/* Custom additions */
65+
66+
.coqdoc-tactic {
67+
font-weight: bold;
68+
}
69+
70+
.smallcaps {
71+
font-variant: small-caps;
72+
}
73+
74+
75+
:root {
76+
--refman-custom-primary-blue: #260086;
77+
--refman-custom-primary-blue-2: #040b92;
78+
--refman-custom-secondary-orange: #ff540a;
79+
--refman-custom-secondary-orange-2: #ffe9df;
80+
}
81+
82+
.btn-info:hover, a:hover, a.wy-text-info:hover {
83+
color: var(--refman-custom-primary-blue-2) !important
84+
}
85+
86+
.wy-menu-vertical header, .wy-menu-vertical p.caption, .rst-content .wy-alert-neutral.admonition-todo a, .rst-content .wy-alert-neutral.admonition a, .rst-content .wy-alert-neutral.attention a, .rst-content .wy-alert-neutral.caution a, .rst-content .wy-alert-neutral.danger a, .rst-content .wy-alert-neutral.error a, .rst-content .wy-alert-neutral.hint a, .rst-content .wy-alert-neutral.important a, .rst-content .wy-alert-neutral.note a, .rst-content .wy-alert-neutral.seealso a, .rst-content .wy-alert-neutral.tip a, .rst-content .wy-alert-neutral.warning a, .wy-alert.wy-alert-neutral a, a, .wy-text-info, .btn-link, .wy-inline-validate.wy-inline-validate-info .wy-input-context, .wy-nav .wy-menu-vertical header, .rst-versions a, .rst-content a code, .rst-content a tt, html.writer-html4 .rst-content dl:not(.docutils)>dt, html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt, html.writer-html4 .rst-content dl:not(.docutils)>dt:before, html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt:before {
87+
color: var(--refman-custom-primary-blue) !important
88+
}
89+
90+
.rst-content .note .admonition-title,.rst-content .note .wy-alert-title,.rst-content .seealso .admonition-title,.rst-content .seealso .wy-alert-title,.rst-content .wy-alert-info.admonition-todo .admonition-title,.rst-content .wy-alert-info.admonition-todo .wy-alert-title,.rst-content .wy-alert-info.admonition .admonition-title,.rst-content .wy-alert-info.admonition .wy-alert-title,.rst-content .wy-alert-info.attention .admonition-title,.rst-content .wy-alert-info.attention .wy-alert-title,.rst-content .wy-alert-info.caution .admonition-title,.rst-content .wy-alert-info.caution .wy-alert-title,.rst-content .wy-alert-info.danger .admonition-title,.rst-content .wy-alert-info.danger .wy-alert-title,.rst-content .wy-alert-info.error .admonition-title,.rst-content .wy-alert-info.error .wy-alert-title,.rst-content .wy-alert-info.hint .admonition-title,.rst-content .wy-alert-info.hint .wy-alert-title,.rst-content .wy-alert-info.important .admonition-title,.rst-content .wy-alert-info.important .wy-alert-title,.rst-content .wy-alert-info.tip .admonition-title,.rst-content .wy-alert-info.tip .wy-alert-title,.rst-content .wy-alert-info.warning .admonition-title,.rst-content .wy-alert-info.warning .wy-alert-title,.rst-content .wy-alert.wy-alert-info .admonition-title,.wy-alert.wy-alert-info .rst-content .admonition-title,.wy-alert.wy-alert-info .wy-alert-title {
91+
background: var(--refman-custom-primary-blue) !important
92+
}
93+
94+
html.writer-html4 .rst-content dl:not(.docutils)>dt,html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt {
95+
background: var(--refman-custom-secondary-orange-2) !important;
96+
color: var(--refman-custom-primary-blue) !important;
97+
border-top: 3px solid var(--refman-custom-secondary-orange) !important;
98+
}
99+
100+
.wy-tray-container li.wy-tray-item-info, .btn-info, .wy-menu-vertical a:active, .wy-side-nav-search, .wy-dropdown-menu>dd>a:hover, .wy-dropdown.wy-dropdown-bubble .wy-dropdown-menu a:hover, .wy-side-nav-search img, .wy-nav .wy-menu-vertical a:hover, .wy-nav-top, .wy-nav-top img {
101+
background-color: var(--refman-custom-secondary-orange) !important
102+
}
103+
104+
.wy-side-nav-search input[type=text] {
105+
border-color: var(--refman-custom-primary-blue-2) !important
106+
}
107+
108+
.rst-versions, .wy-nav-side {
109+
background: #dedede !important;
110+
}
111+
112+
.wy-side-nav-search>div.version {
113+
color: #dedede !important;
114+
}
115+
116+
.wy-menu-vertical a:hover {
117+
background-color: #494949 !important;
118+
color: #dedede !important;
119+
}

‎doc/sphinx/introduction.rst‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
The is the reference manual of the Standard Library of Coq.
2-
It mostly presents a few tactics.
1+
This is the reference manual of the Standard Library of the Rocq Prover.
2+
It mostly presents a few notations and tactics.
33

44
.. only:: html
55

‎doc/sphinx/language/coq-library.rst‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,8 @@ These directories belong to the initial load path of the system, and
2929
the modules they provide are compiled at installation time. So they
3030
are directly accessible with the command ``Require``.
3131

32-
The different modules of the Coq standard library are documented
33-
online at https://coq.inria.fr/stdlib/.
32+
The different modules of the Rocq standard library are documented
33+
online at https://rocq-prover.org/stdlib/.
3434

3535
Peano’s arithmetic (nat)
3636
~~~~~~~~~~~~~~~~~~~~~~~~
@@ -250,7 +250,7 @@ Floats library
250250
~~~~~~~~~~~~~~
251251

252252
The standard library has a small ``Floats`` module for accessing
253-
processor floating-point operations through the Coq kernel.
253+
processor floating-point operations through the Rocq kernel.
254254
However, while this module supports computation and has a bit-level
255255
specification, it doesn't include elaborate theorems, such as a link
256256
to real arithmetic or various error bounds. To do proofs by

‎doc/stdlib/Library.tex‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,9 @@
2323
\tableofcontents
2424

2525
\newpage
26-
% \section*{The \Coq\ standard library}
26+
% \section*{The \Rocq\ standard library}
2727

28-
This document is a short description of the \Coq\ standard library.
28+
This document is a short description of the \Rocq\ standard library.
2929
This library comes with the system as a complement of the core library
3030
(the {\bf Init} library ; see the Reference Manual for a description
3131
of this library). It provides a set of modules directly available

0 commit comments

Comments
 (0)