-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Documentation of branch “master” at 097d5313
- Loading branch information
Showing
292 changed files
with
1,240 additions
and
1,240 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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>Env (rocq-runtime.Boot.Env)</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="../../../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> » <a href="../index.html">Boot</a> » Env</nav><header class="odoc-preamble"><h1>Module <code><span>Boot.Env</span></code></h1><p>Coq runtime enviroment API.</p><p>This module provides functions for manipulation of Coq's runtime enviroment, including the standard directories and support files.</p><p>This API is similar in spirit to findlib's or dune-sites API, see their documentation for more information:</p><ul><li>http://projects.camlcity.org/projects/dl/findlib-1.9.1/doc/ref-html/lib/index.html</li><li>https://dune.readthedocs.io/en/stable/sites.html#sites</li></ul><p>It is important that this library has a minimal dependency set.</p><p>The Coq runtime enviroment needs to be properly initialized before use; we detail the rules below. It is recommended that applications requiring multiple accesses to the environment, do initialize it once and keep a ref to it. We don't forbid yet double initialization, (second time is a noop) but we may do so in the future. Rules for "coqlib" are:</p><ul><li>the <code>ROCQLIB</code> env variable will be used if set</li><li>if not, the existence of <code>theories/Init/Prelude.vo</code> will be checked, in the following order:</li></ul><ol><li><code>coqlibsuffix</code> given in configure</li><li><code>coqlib</code> given in configure</li></ol><ul><li>if none of the above succeeds, the initialization will fail</li></ul><ul><li>The <code>ROCQRUNTIMELIB</code> env variable is also used if set, if not, the location of the rocq-runtime files will be assumed to be <code>ROCQLIB/../rocq-runtime</code>, except if <code>ROCQLIB/plugins</code> exists <code>as in some developers layouts</code>, in which case we will set <code>ROCQRUNTIMELIB:=ROCQLIB</code>.</li></ul><p>Note that <code>set_coqlib</code> is used by some commands to process the <code>-coqlib</code> option, as of now this sets both <code>coqlib</code> and <code>coqcorelib</code>; this part of the initialization will be eventually moved here.</p><p>The error handling policy of this module is simple for now: failing to initialize Coq's env will produce a fatal error, and the application will exit with code 1. No error handling is thus required on the client yet.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module" id="module-Path" class="anchored"><a href="#module-Path" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Path/index.html">Path</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This API is loosely inspired by <code>Stdune.Path</code>, for now we keep it minimal, but at some point we may extend it.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-t" class="anchored"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Coq runtime enviroment, including location of Coq's stdlib</p></div></div><div class="odoc-spec"><div class="spec value" id="val-init" class="anchored"><a href="#val-init" class="anchor"></a><code><span><span class="keyword">val</span> init : <span>unit <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p><code>init ()</code> will initialize the Coq environment.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-stdlib" class="anchored"><a href="#val-stdlib" class="anchor"></a><code><span><span class="keyword">val</span> stdlib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>stdlib directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-plugins" class="anchored"><a href="#val-plugins" class="anchor"></a><code><span><span class="keyword">val</span> plugins : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>plugins directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-user_contrib" class="anchored"><a href="#val-user_contrib" class="anchor"></a><code><span><span class="keyword">val</span> user_contrib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>user contrib directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-tool" class="anchored"><a href="#val-tool" class="anchor"></a><code><span><span class="keyword">val</span> tool : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>tool-specific directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-native_cmi" class="anchored"><a href="#val-native_cmi" class="anchor"></a><code><span><span class="keyword">val</span> native_cmi : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>.cmi files needed for native compilation</p></div></div><div class="odoc-spec"><div class="spec value" id="val-revision" class="anchored"><a href="#val-revision" class="anchor"></a><code><span><span class="keyword">val</span> revision : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>The location of the revision file</p></div></div><div class="odoc-spec"><div class="spec value" id="val-corelib" class="anchored"><a href="#val-corelib" class="anchor"></a><code><span><span class="keyword">val</span> corelib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>rocq-runtime/lib directory, not sure if to keep this</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqlib" class="anchored"><a href="#val-coqlib" class="anchor"></a><code><span><span class="keyword">val</span> coqlib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>coq/lib directory, not sure if to keep this</p></div></div><div class="odoc-spec"><div class="spec value" id="val-set_coqlib" class="anchored"><a href="#val-set_coqlib" class="anchor"></a><code><span><span class="keyword">val</span> set_coqlib : <span>string <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Internal, should be set automatically by passing cmdline args to init; note that this will set both <code>coqlib</code> and <code>corelib</code> for now.</p></div></div></div></body></html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Env (rocq-runtime.Boot.Env)</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="../../../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> » <a href="../index.html">Boot</a> » Env</nav><header class="odoc-preamble"><h1>Module <code><span>Boot.Env</span></code></h1><p>Rocq runtime enviroment API.</p><p>This module provides functions for manipulation of Rocq's runtime enviroment, including the standard directories and support files.</p><p>This API is similar in spirit to findlib's or dune-sites API, see their documentation for more information:</p><ul><li>http://projects.camlcity.org/projects/dl/findlib-1.9.1/doc/ref-html/lib/index.html</li><li>https://dune.readthedocs.io/en/stable/sites.html#sites</li></ul><p>It is important that this library has a minimal dependency set.</p><p>The Rocq runtime enviroment needs to be properly initialized before use; we detail the rules below. It is recommended that applications requiring multiple accesses to the environment, do initialize it once and keep a ref to it. We don't forbid yet double initialization, (second time is a noop) but we may do so in the future. Rules for "coqlib" are:</p><ul><li>the <code>ROCQLIB</code> env variable will be used if set</li><li>if not, the existence of <code>theories/Init/Prelude.vo</code> will be checked, in the following order:</li></ul><ol><li><code>coqlibsuffix</code> given in configure</li><li><code>coqlib</code> given in configure</li></ol><ul><li>if none of the above succeeds, the initialization will fail</li></ul><ul><li>The <code>ROCQRUNTIMELIB</code> env variable is also used if set, if not, the location of the rocq-runtime files will be assumed to be <code>ROCQLIB/../rocq-runtime</code>, except if <code>ROCQLIB/plugins</code> exists <code>as in some developers layouts</code>, in which case we will set <code>ROCQRUNTIMELIB:=ROCQLIB</code>.</li></ul><p>Note that <code>set_coqlib</code> is used by some commands to process the <code>-coqlib</code> option, as of now this sets both <code>coqlib</code> and <code>coqcorelib</code>; this part of the initialization will be eventually moved here.</p><p>The error handling policy of this module is simple for now: failing to initialize Rocq's env will produce a fatal error, and the application will exit with code 1. No error handling is thus required on the client yet.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module" id="module-Path" class="anchored"><a href="#module-Path" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Path/index.html">Path</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This API is loosely inspired by <code>Stdune.Path</code>, for now we keep it minimal, but at some point we may extend it.</p></div></div><div class="odoc-spec"><div class="spec type" id="type-t" class="anchored"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Rocq runtime enviroment, including location of Rocq's stdlib</p></div></div><div class="odoc-spec"><div class="spec value" id="val-init" class="anchored"><a href="#val-init" class="anchor"></a><code><span><span class="keyword">val</span> init : <span>unit <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p><code>init ()</code> will initialize the Rocq environment.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-stdlib" class="anchored"><a href="#val-stdlib" class="anchor"></a><code><span><span class="keyword">val</span> stdlib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>stdlib directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-plugins" class="anchored"><a href="#val-plugins" class="anchor"></a><code><span><span class="keyword">val</span> plugins : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>plugins directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-user_contrib" class="anchored"><a href="#val-user_contrib" class="anchor"></a><code><span><span class="keyword">val</span> user_contrib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>user contrib directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-tool" class="anchored"><a href="#val-tool" class="anchor"></a><code><span><span class="keyword">val</span> tool : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p><code>tool-specific directory</code></p></div></div><div class="odoc-spec"><div class="spec value" id="val-native_cmi" class="anchored"><a href="#val-native_cmi" class="anchor"></a><code><span><span class="keyword">val</span> native_cmi : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>.cmi files needed for native compilation</p></div></div><div class="odoc-spec"><div class="spec value" id="val-revision" class="anchored"><a href="#val-revision" class="anchor"></a><code><span><span class="keyword">val</span> revision : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>The location of the revision file</p></div></div><div class="odoc-spec"><div class="spec value" id="val-corelib" class="anchored"><a href="#val-corelib" class="anchor"></a><code><span><span class="keyword">val</span> corelib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>rocq-runtime/lib directory, not sure if to keep this</p></div></div><div class="odoc-spec"><div class="spec value" id="val-coqlib" class="anchored"><a href="#val-coqlib" class="anchor"></a><code><span><span class="keyword">val</span> coqlib : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="Path/index.html#type-t">Path.t</a></span></code></div><div class="spec-doc"><p>coq/lib directory, not sure if to keep this</p></div></div><div class="odoc-spec"><div class="spec value" id="val-set_coqlib" class="anchored"><a href="#val-set_coqlib" class="anchor"></a><code><span><span class="keyword">val</span> set_coqlib : <span>string <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Internal, should be set automatically by passing cmdline args to init; note that this will set both <code>coqlib</code> and <code>corelib</code> for now.</p></div></div></div></body></html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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>Boot (rocq-runtime.Boot)</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> » Boot</nav><header class="odoc-preamble"><h1>Module <code><span>Boot</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module" id="module-Env" class="anchored"><a href="#module-Env" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Env/index.html">Env</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Coq runtime enviroment API.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Path" class="anchored"><a href="#module-Path" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Path/index.html">Path</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Usage" class="anchored"><a href="#module-Usage" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Usage/index.html">Usage</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Util" class="anchored"><a href="#module-Util" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Util/index.html">Util</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Boot (rocq-runtime.Boot)</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> » Boot</nav><header class="odoc-preamble"><h1>Module <code><span>Boot</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module" id="module-Env" class="anchored"><a href="#module-Env" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Env/index.html">Env</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Rocq runtime enviroment API.</p></div></div><div class="odoc-spec"><div class="spec module" id="module-Path" class="anchored"><a href="#module-Path" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Path/index.html">Path</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Usage" class="anchored"><a href="#module-Usage" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Usage/index.html">Usage</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module" id="module-Util" class="anchored"><a href="#module-Util" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="Util/index.html">Util</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html> |
Oops, something went wrong.