Deploying to gh-pages from @ 15fe149 🚀

blog/01-introducing-flux.html

@@ -230,7 +230,7 @@ <h3 id="pre-conditions"><a class="header" href="#pre-conditions">Pre-Conditions<
 </span><span class="boring">fn main() {
 </span>#[flux::sig(fn (b:bool[true]))]
 pub fn assert(b:bool) {
-  if !b { panic!(&quot;assertion failed&quot;) }
+  if !b { panic!("assertion failed") }
 }
 <span class="boring">}</span></code></pre></pre>
 <p>Here, the refined specification for <code>assert</code> says that you can <em>only</em> call

blog/02-ownership.html

@@ -405,9 +405,13 @@ <h2 id="summary"><a class="header" href="#summary">Summary</a></h2>
 <p>Next, we'll see how refinements and ownership yield a simple refined API
 for <em>vectors</em> that lets Flux check bounds safety at compile time...</p>
 <div class="footnote-definition" id="1"><sup class="footnote-definition-label">1</sup>
-<p>For those familiar with the term, these types are <em>loop invariants</em>
-<sup class="footnote-reference"><a href="#2">2</a></sup>: Setting aside the issue of overflows for now
-<sup class="footnote-reference"><a href="#3">3</a></sup>: Thereby allowing so-called <em>strong updates</em> in the type specifications</p>
+<p>For those familiar with the term, these types are <em>loop invariants</em></p>
+</div>
+<div class="footnote-definition" id="2"><sup class="footnote-definition-label">2</sup>
+<p>Setting aside the issue of overflows for now</p>
+</div>
+<div class="footnote-definition" id="3"><sup class="footnote-definition-label">3</sup>
+<p>Thereby allowing so-called <em>strong updates</em> in the type specifications</p>
 </div>
 
                     </main>

blog/03-vectors.html

@@ -219,7 +219,7 @@ <h3 id="creating-vectors"><a class="header" href="#creating-vectors">Creating Ve
 <span class="boring">}</span></code></pre></pre>
 <p>The above implements <code>RVec::new</code> as a wrapper around <code>Vec::new</code>.
 The <code>#[flux::trusted]</code> attribute tells Flux there is nothing to
-&quot;check&quot; here, as we are <em>defining</em> the API itself and trusting
+"check" here, as we are <em>defining</em> the API itself and trusting
 that the implementation (using <code>vec</code> is correct).
 However, the signature says that <em>callers</em> of the <code>RVec::new</code> get
 back a vector indexed with <code>0</code> i.e. an empty vector.</p>
@@ -293,7 +293,7 @@ <h3 id="querying-the-size"><a class="header" href="#querying-the-size">Querying
     self.inner.len()
 }
 <span class="boring">}</span></code></pre></pre>
-<p>Now, flux &quot;knows&quot; that after two <code>push</code>es, the size of the vector is <code>2</code> and after
+<p>Now, flux "knows" that after two <code>push</code>es, the size of the vector is <code>2</code> and after
 the two <code>pop</code>s, the size is <code>0</code> again</p>
 <img src="../img/push_pop_len.gif" width="100%">
 <h3 id="random-access"><a class="header" href="#random-access">Random Access</a></h3>
@@ -343,7 +343,7 @@ <h3 id="random-access"><a class="header" href="#random-access">Random Access</a>
 <p>And now the above <code>vec_sum</code> example looks a little nicer</p>
 <img src="../img/vec_sum_index.gif" width="100%">
 <h2 id="memoization"><a class="header" href="#memoization">Memoization</a></h2>
-<p>Lets put the whole API to work in this &quot;memoized&quot; version of the fibonacci
+<p>Lets put the whole API to work in this "memoized" version of the fibonacci
 function which uses a vector to store the results of previous calls</p>
 <pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
 </span><span class="boring">fn main() {
@@ -377,7 +377,7 @@ <h2 id="memoization"><a class="header" href="#memoization">Memoization</a></h2>
 <span class="boring">}</span></code></pre></pre>
 <p>Flux complains that the vector may be <em>empty</em> and so the <code>pop</code> call may
 fail ... but why? Can you spot the problem?</p>
-<p>Indeed, we missed a &quot;corner&quot; case -- when <code>n</code> is <code>0</code> we skip the loop and
+<p>Indeed, we missed a "corner" case -- when <code>n</code> is <code>0</code> we skip the loop and
 so the vector is empty! Once we add a test for that, flux is happy.</p>
 <img src="../img/fib.gif" width="100%">
 <h2 id="binary-search"><a class="header" href="#binary-search">Binary Search</a></h2>

dev/architecture.html

@@ -184,7 +184,7 @@ <h2 id="crates"><a class="header" href="#crates">Crates</a></h2>
 <li><code>crates/flux-desugar</code>: Implementation of name resolution and desugaring from Flux surface syntax into Flux high-level intermediate representation (<code>fhir</code>). This includes name resolution.</li>
 <li><code>crates/flux-driver</code>: Main entry point to Flux. It contains the <code>flux-driver</code> binary and the implementation of the <a href="https://doc.rust-lang.org/nightly/nightly-rustc/rustc_driver/trait.Callbacks.html"><code>Callbacks</code></a> trait.</li>
 <li><code>crates/flux-errors</code>: Utility definitions for user facing error reporting.</li>
-<li><code>crates/flux-fhir-analysis</code>: Implements the &quot;analyses&quot; performed in the <code>fhir</code>, most notably well-formedness checking and conversion from <code>fhir</code> into <code>rty</code>.</li>
+<li><code>crates/flux-fhir-analysis</code>: Implements the "analyses" performed in the <code>fhir</code>, most notably well-formedness checking and conversion from <code>fhir</code> into <code>rty</code>.</li>
 <li><code>crates/flux-fixpoint</code>: Code to interact with the Liquid Fixpoint binary.</li>
 <li><code>crates/flux-macros</code>: Procedural macros used internally to implement Flux.</li>
 <li><code>crates/flux-metadata</code>: Logic for saving Flux crate metadata that can be used to import refined signatures from external crates.</li>
@@ -193,7 +193,7 @@ <h2 id="crates"><a class="header" href="#crates">Crates</a></h2>
 <li><code>crates/flux-syntax</code>: Definition of the surface syntax AST and parser.</li>
 <li><code>crates/flux-tests</code>: Flux regression tests.</li>
 <li><code>lib/flux-attrs</code>: Implementation of user facing procedural macros for annotating programs with Flux specs.</li>
-<li><code>lib/flux-rs</code>: This is just a re-export of the macros implemented in <code>flux-attrs</code>. The intention is to eventually put Flux &quot;standard library&quot; here, i.e., a set of definitions that are useful when working with Flux.</li>
+<li><code>lib/flux-rs</code>: This is just a re-export of the macros implemented in <code>flux-attrs</code>. The intention is to eventually put Flux "standard library" here, i.e., a set of definitions that are useful when working with Flux.</li>
 </ul>
 <h2 id="intermediate-representations"><a class="header" href="#intermediate-representations">Intermediate Representations</a></h2>
 <p>Flux has several intermediate representations (IR) for types. They represent a refined version of an equivalent type in some <code>rustc</code> IR. We have picked a distinct <em>verb</em> to refer to the process of going between these different representations to make it easier to refer to them. The following image summarizes all the IRs and the process for going between them.</p>

doc/cargo_flux/fn.run.html

@@ -1 +1 @@
-<!DOCTYPE html><html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width, initial-scale=1.0"><meta name="generator" content="rustdoc"><meta name="description" content="API documentation for the Rust `run` fn in crate `cargo_flux`."><title>run in cargo_flux - Rust</title><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceSerif4-Regular-46f98efaafac5295.ttf.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/FiraSans-Regular-018c141bf0843ffd.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/FiraSans-Medium-8f9a781e4970d388.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceCodePro-Regular-562dcc5011b6de7d.ttf.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceCodePro-Semibold-d899c5a5c4aeb14a.ttf.woff2"><link rel="stylesheet" href="../static.files/normalize-76eba96aa4d2e634.css"><link rel="stylesheet" href="../static.files/rustdoc-9ee3a5e31a2afa3e.css"><meta name="rustdoc-vars" data-root-path="../" data-static-root-path="../static.files/" data-current-crate="cargo_flux" data-themes="" data-resource-suffix="" data-rustdoc-version="1.75.0-nightly (7adc89b69 2023-11-07)" data-channel="nightly" data-search-js="search-8fbf244ebcf71464.js" data-settings-js="settings-74424d7eec62a23e.js" ><script src="../static.files/storage-fec3eaa3851e447d.js"></script><script defer src="sidebar-items.js"></script><script defer src="../static.files/main-9dd44ab47b99a0fb.js"></script><noscript><link rel="stylesheet" href="../static.files/noscript-5d8b3c7633ad77ba.css"></noscript><link rel="alternate icon" type="image/png" href="../static.files/favicon-16x16-8b506e7a72182f1c.png"><link rel="alternate icon" type="image/png" href="../static.files/favicon-32x32-422f7d1d52889060.png"><link rel="icon" type="image/svg+xml" href="../static.files/favicon-2c020d218678b618.svg"></head><body class="rustdoc fn"><!--[if lte IE 11]><div class="warning">This old browser is unsupported and will most likely display funky things.</div><![endif]--><nav class="mobile-topbar"><button class="sidebar-menu-toggle">&#9776;</button></nav><nav class="sidebar"><div class="sidebar-crate"><h2><a href="../cargo_flux/index.html">cargo_flux</a><span class="version">0.1.0</span></h2></div><div class="sidebar-elems"></div></nav><main><div class="width-limiter"><nav class="sub"><form class="search-form"><span></span><input class="search-input" name="search" aria-label="Run search in the documentation" autocomplete="off" spellcheck="false" placeholder="Click or press ‘S’ to search, ‘?’ for more options…" type="search"><div id="help-button" title="help" tabindex="-1"><a href="../help.html">?</a></div><div id="settings-menu" tabindex="-1"><a href="../settings.html" title="settings"><img width="22" height="22" alt="Change settings" src="../static.files/wheel-7b819b6101059cd0.svg"></a></div></form></nav><section id="main-content" class="content"><div class="main-heading"><h1>Function <a href="index.html">cargo_flux</a>::<wbr><a class="fn" href="#">run</a><button id="copy-path" title="Copy item path to clipboard"><img src="../static.files/clipboard-7571035ce49a181d.svg" width="19" height="18" alt="Copy item path"></button></h1><span class="out-of-band"><a class="src" href="../src/cargo_flux/cargo-flux.rs.html#24-57">source</a> · <button id="toggle-all-docs" title="collapse all docs">[<span>&#x2212;</span>]</button></span></div><pre class="rust item-decl"><code>pub(crate) fn run() -&gt; <a class="type" href="https://docs.rs/anyhow/1.0.75/anyhow/type.Result.html" title="type anyhow::Result">Result</a>&lt;<a class="primitive" href="https://doc.rust-lang.org/nightly/std/primitive.i32.html">i32</a>&gt;</code></pre></section></div></main></body></html>
+<!DOCTYPE html><html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width, initial-scale=1.0"><meta name="generator" content="rustdoc"><meta name="description" content="API documentation for the Rust `run` fn in crate `cargo_flux`."><title>run in cargo_flux - Rust</title><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceSerif4-Regular-46f98efaafac5295.ttf.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/FiraSans-Regular-018c141bf0843ffd.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/FiraSans-Medium-8f9a781e4970d388.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceCodePro-Regular-562dcc5011b6de7d.ttf.woff2"><link rel="preload" as="font" type="font/woff2" crossorigin href="../static.files/SourceCodePro-Semibold-d899c5a5c4aeb14a.ttf.woff2"><link rel="stylesheet" href="../static.files/normalize-76eba96aa4d2e634.css"><link rel="stylesheet" href="../static.files/rustdoc-9ee3a5e31a2afa3e.css"><meta name="rustdoc-vars" data-root-path="../" data-static-root-path="../static.files/" data-current-crate="cargo_flux" data-themes="" data-resource-suffix="" data-rustdoc-version="1.75.0-nightly (7adc89b69 2023-11-07)" data-channel="nightly" data-search-js="search-8fbf244ebcf71464.js" data-settings-js="settings-74424d7eec62a23e.js" ><script src="../static.files/storage-fec3eaa3851e447d.js"></script><script defer src="sidebar-items.js"></script><script defer src="../static.files/main-9dd44ab47b99a0fb.js"></script><noscript><link rel="stylesheet" href="../static.files/noscript-5d8b3c7633ad77ba.css"></noscript><link rel="alternate icon" type="image/png" href="../static.files/favicon-16x16-8b506e7a72182f1c.png"><link rel="alternate icon" type="image/png" href="../static.files/favicon-32x32-422f7d1d52889060.png"><link rel="icon" type="image/svg+xml" href="../static.files/favicon-2c020d218678b618.svg"></head><body class="rustdoc fn"><!--[if lte IE 11]><div class="warning">This old browser is unsupported and will most likely display funky things.</div><![endif]--><nav class="mobile-topbar"><button class="sidebar-menu-toggle">&#9776;</button></nav><nav class="sidebar"><div class="sidebar-crate"><h2><a href="../cargo_flux/index.html">cargo_flux</a><span class="version">0.1.0</span></h2></div><div class="sidebar-elems"></div></nav><main><div class="width-limiter"><nav class="sub"><form class="search-form"><span></span><input class="search-input" name="search" aria-label="Run search in the documentation" autocomplete="off" spellcheck="false" placeholder="Click or press ‘S’ to search, ‘?’ for more options…" type="search"><div id="help-button" title="help" tabindex="-1"><a href="../help.html">?</a></div><div id="settings-menu" tabindex="-1"><a href="../settings.html" title="settings"><img width="22" height="22" alt="Change settings" src="../static.files/wheel-7b819b6101059cd0.svg"></a></div></form></nav><section id="main-content" class="content"><div class="main-heading"><h1>Function <a href="index.html">cargo_flux</a>::<wbr><a class="fn" href="#">run</a><button id="copy-path" title="Copy item path to clipboard"><img src="../static.files/clipboard-7571035ce49a181d.svg" width="19" height="18" alt="Copy item path"></button></h1><span class="out-of-band"><a class="src" href="../src/cargo_flux/cargo-flux.rs.html#24-57">source</a> · <button id="toggle-all-docs" title="collapse all docs">[<span>&#x2212;</span>]</button></span></div><pre class="rust item-decl"><code>pub(crate) fn run() -&gt; <a class="type" href="https://docs.rs/anyhow/1.0.79/anyhow/type.Result.html" title="type anyhow::Result">Result</a>&lt;<a class="primitive" href="https://doc.rust-lang.org/nightly/std/primitive.i32.html">i32</a>&gt;</code></pre></section></div></main></body></html>