Skip to content

Commit 8e495d8

Browse files
github-actions[bot]NicolasRouquette
github-actions[bot]
authored and
NicolasRouquette
committed
Update docs and test reports: 31b34d8 
1 parent 3f79879 commit 8e495d8

139 files changed

Lines changed: 4176 additions & 4176 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎docs/L4YAML.pdf‎

8 Bytes
Binary file not shown.

‎docs/api/L4YAML.html‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎docs/api/L4YAML/Config/Config.html‎

Lines changed: 21 additions & 21 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/Config/Limits.html‎

Lines changed: 124 additions & 124 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/FFI/FFI.html‎

Lines changed: 35 additions & 35 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/Output/Dump.html‎

Lines changed: 75 additions & 75 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/Output/Emitter.html‎

Lines changed: 14 additions & 14 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/Parser/Composition.html‎

Lines changed: 10 additions & 10 deletions
Large diffs are not rendered by default.

‎docs/api/L4YAML/Parser/Fuel.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="../.././style.css"></link><link rel="icon" href="../.././favicon.svg"></link><link rel="mask-icon" href="../.././favicon.svg" color="#000000"></link><link rel="prefetch" href="../.././/declarations/declaration-data.bmp" as="image"></link><title>L4YAML.Parser.Fuel</title><script defer="true" src="../.././mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="../.././";</script><script>const MODULE_NAME="L4YAML.Parser.Fuel";</script><script type="module" src="../.././jump-src.js"></script><script type="module" src="../.././search.js"></script><script type="module" src="../.././expand-nav.js"></script><script type="module" src="../.././how-about.js"></script><script type="module" src="../.././instances.js"></script><script type="module" src="../.././importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">L4YAML</span>.<span class="name">Parser</span>.<span class="name">Fuel</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='../.././search.html';">Search</button></form></header><nav class="internal_nav"><p><a href="#top">return to top</a></p><p class="gh_nav_link"><a href="https://github.jpl.nasa.gov/pass/lean4-yaml-verified/blob/4515042df494ce6b0e661f08c0f1cefc3c7c5cc3/L4YAML/Parser/Fuel.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../.././Init.html">Init</a></li><li><a href="../.././L4YAML/Token/Token.html">L4YAML.Token.Token</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-L4YAML.Parser.Fuel" class="imported-by-list"></ul></details></div><div class="nav_link"><a class="break_within" href="#L4YAML.TokenParser.initialFuel"><span class="name">L4YAML</span>.<span class="name">TokenParser</span>.<span class="name">initialFuel</span></a></div></nav><main>
1+
<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="../.././style.css"></link><link rel="icon" href="../.././favicon.svg"></link><link rel="mask-icon" href="../.././favicon.svg" color="#000000"></link><link rel="prefetch" href="../.././/declarations/declaration-data.bmp" as="image"></link><title>L4YAML.Parser.Fuel</title><script defer="true" src="../.././mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="../.././";</script><script>const MODULE_NAME="L4YAML.Parser.Fuel";</script><script type="module" src="../.././jump-src.js"></script><script type="module" src="../.././search.js"></script><script type="module" src="../.././expand-nav.js"></script><script type="module" src="../.././how-about.js"></script><script type="module" src="../.././instances.js"></script><script type="module" src="../.././importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">L4YAML</span>.<span class="name">Parser</span>.<span class="name">Fuel</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='../.././search.html';">Search</button></form></header><nav class="internal_nav"><p><a href="#top">return to top</a></p><p class="gh_nav_link"><a href="https://github.jpl.nasa.gov/pass/lean4-yaml-verified/blob/31b34d86acbcedca3d8c7d765c6bf5cdeb9df180/L4YAML/Parser/Fuel.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../.././Init.html">Init</a></li><li><a href="../.././L4YAML/Token/Token.html">L4YAML.Token.Token</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-L4YAML.Parser.Fuel" class="imported-by-list"></ul></details></div><div class="nav_link"><a class="break_within" href="#L4YAML.TokenParser.initialFuel"><span class="name">L4YAML</span>.<span class="name">TokenParser</span>.<span class="name">initialFuel</span></a></div></nav><main>
22
<div class="mod_doc"><h1 id="Parser-Fuel" class="markdown-heading">Parser Fuel <a class="hover-link" href="#Parser-Fuel">#</a></h1><p>Initial fuel computation for the recursive-descent parser.</p><p>Split from <code><a href="../.././Parser/TokenParser.html">Parser/TokenParser.lean</a></code> during Blueprint Initiative 1
33
Phase 3. See <code>Blueprint/03-code-organization.md</code>.</p><h2 id="Fuel-based-termination-P10-8a-b" class="markdown-heading">Fuel-based termination (P10.8a–b) <a class="hover-link" href="#Fuel-based-termination-P10-8a-b">#</a></h2><p>All 14 functions in the mutual block in <code>TokenParser.lean</code> take a
44
<code>fuel : <a href="../.././Init/Prelude.html#Nat">Nat</a></code> parameter that decreases by 1 at each function entry
@@ -10,7 +10,7 @@
1010
dispatch wrapper for the very first token (tag/anchor/scalar dispatch
1111
chain).</li></ul><p>This file holds only the fuel calculation; the formula appears once in
1212
production code (in <code>parseDocument</code>) and once in proofs (capstone fuel
13-
budget reasoning), so factoring it out keeps both call sites in sync.</p></div><div class="decl" id="L4YAML.TokenParser.initialFuel"><div class="def"><div class="gh_link"><a href="https://github.jpl.nasa.gov/pass/lean4-yaml-verified/blob/4515042df494ce6b0e661f08c0f1cefc3c7c5cc3/L4YAML/Parser/Fuel.lean">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
13+
budget reasoning), so factoring it out keeps both call sites in sync.</p></div><div class="decl" id="L4YAML.TokenParser.initialFuel"><div class="def"><div class="gh_link"><a href="https://github.jpl.nasa.gov/pass/lean4-yaml-verified/blob/31b34d86acbcedca3d8c7d765c6bf5cdeb9df180/L4YAML/Parser/Fuel.lean">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
1414
<span class="decl_name"><a class="break_within" href="../.././L4YAML/Parser/Fuel.html#L4YAML.TokenParser.initialFuel"><span class="name">L4YAML</span>.<span class="name">TokenParser</span>.<span class="name">initialFuel</span></a></span><span class="decl_args">
1515
<span class="fn">(<span class="fn">tokens</span> : <span class="fn"><a href="../.././Init/Prelude.html#Array">Array</a> <span class="fn">(<a href="../.././L4YAML/Token/Token.html#L4YAML.Positioned">Positioned</a> <a href="../.././L4YAML/Token/Token.html#L4YAML.YamlToken">YamlToken</a>)</span></span>)</span></span>
1616
<span class="decl_args"> :</span><div class="decl_type"><a href="../.././Init/Prelude.html#Nat">Nat</a></div></div><p>Initial fuel for <code>parseNode</code> invoked by <code>parseDocument</code>.</p><p>Value: <code>4 * tokens.size + 4</code>.</p><p><strong>Why <code>4 * N + 4</code></strong>: each token may trigger at most one collection

‎docs/api/L4YAML/Parser/State.html‎

Lines changed: 28 additions & 28 deletions
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)