Skip to content

Commit

Permalink
Documentation of branch “master” at 63dac43b
Browse files Browse the repository at this point in the history
  • Loading branch information
coqbot committed Feb 17, 2025
1 parent 6c5b09d commit cbc2d9a
Show file tree
Hide file tree
Showing 70 changed files with 146 additions and 146 deletions.
2 changes: 1 addition & 1 deletion master/api/rocq-runtime/Envars/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Envars (rocq-runtime.Envars)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../index.html">rocq-runtime</a> &#x00BB; Envars</nav><header class="odoc-preamble"><h1>Module <code><span>Envars</span></code></h1><p>This file provides a high-level interface to the environment variables needed by Rocq to run (such as coqlib). The values of these variables may come from different sources (shell environment variables, command line options, options set at the time Rocq was build).</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-getenv_rocq" class="anchored"><a href="#val-getenv_rocq" class="anchor"></a><code><span><span class="keyword">val</span> getenv_rocq : <span>string <span class="arrow">&#45;&gt;</span></span> <span>string option</span></span></code></div><div class="spec-doc"><p><code>getenv_rocq name</code> returns the value of &quot;ROCQ$name&quot; if it exists, otherwise the value of &quot;COQ$name&quot; if it exists and warns that it is deprecated, otherwise <code>None</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-expand_path_macros" class="anchored"><a href="#val-expand_path_macros" class="anchor"></a><code><span><span class="keyword">val</span> expand_path_macros : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>expand_path_macros warn s</code> substitutes environment variables in a string by their values. This function also takes care of substituting path of the form '~X' by an absolute path. Use <code>warn</code> as a message displayer.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-home" class="anchored"><a href="#val-home" class="anchor"></a><code><span><span class="keyword">val</span> home : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>home warn</code> returns the root of the user directory, depending on the OS. This information is usually stored in the $HOME environment variable on POSIX shells. If no such variable exists, then other common names are tried (HOMEDRIVE, HOMEPATH, USERPROFILE). If all of them fail, <code>warn</code> is called.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-datadir" class="anchored"><a href="#val-datadir" class="anchor"></a><code><span><span class="keyword">val</span> datadir : <span>unit <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>datadir</code> is the path to the installed data directory.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-configdir" class="anchored"><a href="#val-configdir" class="anchor"></a><code><span><span class="keyword">val</span> configdir : <span>unit <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>configdir</code> is the path to the installed config directory.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqbin" class="anchored"><a href="#val-coqbin" class="anchor"></a><code><span><span class="keyword">val</span> coqbin : string</span></code></div><div class="spec-doc"><p><code>coqbin</code> is the name of the current executable.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqroot" class="anchored"><a href="#val-coqroot" class="anchor"></a><code><span><span class="keyword">val</span> coqroot : string</span></code></div><div class="spec-doc"><p><code>coqroot</code> is the path to <code>coqbin</code>. The following value only makes sense when executables are running from source tree (e.g. during build or in local mode).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqpath" class="anchored"><a href="#val-coqpath" class="anchor"></a><code><span><span class="keyword">val</span> coqpath : <span>string list</span></span></code></div><div class="spec-doc"><p><code>coqpath</code> is the standard path to coq. Notice that coqpath is stored in reverse order, since that is the order it gets added to the search path.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_config_home" class="anchored"><a href="#val-xdg_config_home" class="anchor"></a><code><span><span class="keyword">val</span> xdg_config_home : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p>Rocq tries to honor the XDG Base Directory Specification to access the user's configuration files.</p><p>see <code>http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_data_home" class="anchored"><a href="#val-xdg_data_home" class="anchor"></a><code><span><span class="keyword">val</span> xdg_data_home : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_data_dirs" class="anchored"><a href="#val-xdg_data_dirs" class="anchor"></a><code><span><span class="keyword">val</span> xdg_data_dirs : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string list</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_dirs" class="anchored"><a href="#val-xdg_dirs" class="anchor"></a><code><span><span class="keyword">val</span> xdg_dirs : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string list</span></span></code></div></div></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Envars (rocq-runtime.Envars)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../index.html">rocq-runtime</a> &#x00BB; Envars</nav><header class="odoc-preamble"><h1>Module <code><span>Envars</span></code></h1><p>This file provides a high-level interface to the environment variables needed by Rocq to run (such as coqlib). The values of these variables may come from different sources (shell environment variables, command line options, options set at the time Rocq was build).</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-getenv_rocq" class="anchored"><a href="#val-getenv_rocq" class="anchor"></a><code><span><span class="keyword">val</span> getenv_rocq : <span>string <span class="arrow">&#45;&gt;</span></span> <span>string option</span></span></code></div><div class="spec-doc"><p><code>getenv_rocq name</code> returns the value of &quot;ROCQ$name&quot; if it exists, otherwise the value of &quot;COQ$name&quot; if it exists and warns that it is deprecated, otherwise <code>None</code>.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-expand_path_macros" class="anchored"><a href="#val-expand_path_macros" class="anchor"></a><code><span><span class="keyword">val</span> expand_path_macros : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>expand_path_macros warn s</code> substitutes environment variables in a string by their values. This function also takes care of substituting path of the form '~X' by an absolute path. Use <code>warn</code> as a message displayer.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-home" class="anchored"><a href="#val-home" class="anchor"></a><code><span><span class="keyword">val</span> home : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>home warn</code> returns the root of the user directory, depending on the OS. This information is usually stored in the $HOME environment variable on POSIX shells. If no such variable exists, then other common names are tried (HOMEDRIVE, HOMEPATH, USERPROFILE). If all of them fail, <code>warn</code> is called.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-datadir" class="anchored"><a href="#val-datadir" class="anchor"></a><code><span><span class="keyword">val</span> datadir : <span>unit <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>datadir</code> is the path to the installed data directory.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-configdir" class="anchored"><a href="#val-configdir" class="anchor"></a><code><span><span class="keyword">val</span> configdir : <span>unit <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p><code>configdir</code> is the path to the installed config directory.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqbin" class="anchored"><a href="#val-coqbin" class="anchor"></a><code><span><span class="keyword">val</span> coqbin : string</span></code></div><div class="spec-doc"><p><code>coqbin</code> is the name of the current executable.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqroot" class="anchored"><a href="#val-coqroot" class="anchor"></a><code><span><span class="keyword">val</span> coqroot : string</span></code></div><div class="spec-doc"><p><code>coqroot</code> is the path to <code>coqbin</code>. The following value only makes sense when executables are running from source tree (e.g. during build or in local mode).</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqpath" class="anchored"><a href="#val-coqpath" class="anchor"></a><code><span><span class="keyword">val</span> coqpath : <span>unit <span class="arrow">&#45;&gt;</span></span> <span>string list</span></span></code></div><div class="spec-doc"><p><code>coqpath</code> is the standard path to coq. Notice that coqpath is stored in reverse order, since that is the order it gets added to the search path.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_config_home" class="anchored"><a href="#val-xdg_config_home" class="anchor"></a><code><span><span class="keyword">val</span> xdg_config_home : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p>Rocq tries to honor the XDG Base Directory Specification to access the user's configuration files.</p><p>see <code>http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_data_home" class="anchored"><a href="#val-xdg_data_home" class="anchor"></a><code><span><span class="keyword">val</span> xdg_data_home : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> string</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_data_dirs" class="anchored"><a href="#val-xdg_data_dirs" class="anchor"></a><code><span><span class="keyword">val</span> xdg_data_dirs : <span><span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string list</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-xdg_dirs" class="anchored"><a href="#val-xdg_dirs" class="anchor"></a><code><span><span class="keyword">val</span> xdg_dirs : <span>warn:<span>(<span>string <span class="arrow">&#45;&gt;</span></span> unit)</span> <span class="arrow">&#45;&gt;</span></span> <span>string list</span></span></code></div></div></div></body></html>
34 changes: 17 additions & 17 deletions master/corelib/Corelib.BinNums.IntDef.html
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab5"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>
<a id="lab21"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>

<div class="paragraph"> </div>

Expand All @@ -291,7 +291,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab6"></a><h2 class="section">Doubling and variants</h2>
<a id="lab22"></a><h2 class="section">Doubling and variants</h2>

</div>
<div class="code">
Expand Down Expand Up @@ -324,7 +324,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab7"></a><h2 class="section">Subtraction of positive into Z</h2>
<a id="lab23"></a><h2 class="section">Subtraction of positive into Z</h2>

</div>
<div class="code">
Expand All @@ -347,7 +347,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab8"></a><h2 class="section">Addition</h2>
<a id="lab24"></a><h2 class="section">Addition</h2>

</div>
<div class="code">
Expand All @@ -370,7 +370,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab9"></a><h2 class="section">Opposite</h2>
<a id="lab25"></a><h2 class="section">Opposite</h2>

</div>
<div class="code">
Expand All @@ -390,7 +390,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab10"></a><h2 class="section">Subtraction</h2>
<a id="lab26"></a><h2 class="section">Subtraction</h2>

</div>
<div class="code">
Expand All @@ -405,7 +405,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab11"></a><h2 class="section">Multiplication</h2>
<a id="lab27"></a><h2 class="section">Multiplication</h2>

</div>
<div class="code">
Expand All @@ -428,7 +428,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab12"></a><h2 class="section">Power function</h2>
<a id="lab28"></a><h2 class="section">Power function</h2>

</div>
<div class="code">
Expand All @@ -451,7 +451,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab13"></a><h2 class="section">Comparison</h2>
<a id="lab29"></a><h2 class="section">Comparison</h2>

</div>
<div class="code">
Expand Down Expand Up @@ -520,7 +520,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab14"></a><h2 class="section">Minimum and maximum</h2>
<a id="lab30"></a><h2 class="section">Minimum and maximum</h2>

</div>
<div class="code">
Expand All @@ -543,7 +543,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab15"></a><h2 class="section">Conversions</h2>
<a id="lab31"></a><h2 class="section">Conversions</h2>

<div class="paragraph"> </div>

Expand Down Expand Up @@ -607,11 +607,11 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab16"></a><h2 class="section">Euclidean divisions for binary integers</h2>
<a id="lab32"></a><h2 class="section">Euclidean divisions for binary integers</h2>

<div class="paragraph"> </div>

<a id="lab17"></a><h2 class="section">Floor division</h2>
<a id="lab33"></a><h2 class="section">Floor division</h2>

<div class="paragraph"> </div>

Expand Down Expand Up @@ -702,7 +702,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab18"></a><h2 class="section">Trunc Division</h2>
<a id="lab34"></a><h2 class="section">Trunc Division</h2>

<div class="paragraph"> </div>

Expand Down Expand Up @@ -763,7 +763,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
No infix notation for rem, otherwise it becomes a keyword
<div class="paragraph"> </div>

<a id="lab19"></a><h2 class="section">Parity functions</h2>
<a id="lab35"></a><h2 class="section">Parity functions</h2>

</div>
<div class="code">
Expand All @@ -781,7 +781,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab20"></a><h2 class="section">Division by two</h2>
<a id="lab36"></a><h2 class="section">Division by two</h2>

<div class="paragraph"> </div>

Expand All @@ -804,7 +804,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
</div>

<div class="doc">
<a id="lab21"></a><h2 class="section">Square root</h2>
<a id="lab37"></a><h2 class="section">Square root</h2>

</div>
<div class="code">
Expand Down
8 changes: 4 additions & 4 deletions master/corelib/Corelib.BinNums.NatDef.html
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
</div>

<div class="doc">
<a id="lab1"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>
<a id="lab38"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>

</div>
<div class="code">
Expand All @@ -282,7 +282,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
</div>

<div class="doc">
<a id="lab2"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>
<a id="lab39"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>

</div>
<div class="code">
Expand All @@ -298,7 +298,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
</div>

<div class="doc">
<a id="lab3"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>
<a id="lab40"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>

</div>
<div class="code">
Expand All @@ -314,7 +314,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
</div>

<div class="doc">
<a id="lab4"></a><h2 class="section">The successor of a <span class="inlinecode"><span class="id" title="var">N</span></span> can be seen as a <span class="inlinecode"><span class="id" title="var">positive</span></span></h2>
<a id="lab41"></a><h2 class="section">The successor of a <span class="inlinecode"><span class="id" title="var">N</span></span> can be seen as a <span class="inlinecode"><span class="id" title="var">positive</span></span></h2>

</div>
<div class="code">
Expand Down
Loading

0 comments on commit cbc2d9a

Please sign in to comment.