Skip to content

Site output

This page shows what the plugin produces. The program from Navigator ran as its own process while this site was being built:

let buildSite (baseUrl: string) (arguments: string[]) =
    let options =
        Rocq.defaults
        |> Rocq.project "example/_CoqProject"
        |> Rocq.facts (Some "example/facts.json")
        |> Rocq.config (Some "example/navigator.json")

    Site.create "Tally"
    |> Site.baseUrl baseUrl
    |> Site.output ".work/minimal"
    |> Site.noStaticFiles
    |> Rocq.register options
    |> Site.collection (
        Rocq.collection "proofs" options
        |> Collection.layout (Rocq.reader options)
    )
    |> fun site -> Nacara.run site arguments

The build

» Loaded the content, 501 ms
✓ Built 4 pages, 19 written, 623 ms
exit code 0

The files

Tally.Core.html                             24374 bytes
Tally.Laws.html                             26718 bytes
Tally.Prose.html                            22214 bytes
assets/fonts/Inter-wght.woff2               48256 bytes
assets/fonts/JetBrainsMono-Regular.woff2    69440 bytes
assets/fonts/JetBrainsMono-SemiBold.woff2    70820 bytes
assets/fonts/OFL-Inter.txt                   4477 bytes
assets/fonts/OFL-JetBrainsMono.txt           4524 bytes
assets/fonts/OFL-SourceSerif4.txt            4407 bytes
assets/fonts/SourceSerif4-wght-italic.woff2    51576 bytes
assets/fonts/SourceSerif4-wght.woff2        50936 bytes
assets/navigator.css                        26900 bytes
assets/navigator.js                        406015 bytes
data/Tally.Core.symbols.json                10160 bytes
data/Tally.Laws.symbols.json                 6600 bytes
data/Tally.Prose.symbols.json                6602 bytes
data/index.symbols.json                       252 bytes
data/search.json                             6024 bytes
index.html                                  12639 bytes

A page per module, the index, the shared stylesheet and client, fonts, and the data the client fetches. Every file is static, so any file host will serve it.

The HTML

This is the declaration size from Tally.Core.html, with a line break added before each block for reading. The source text is in the markup, the reference links work without a script, and the proof and reference lists fold with details.

Fixpoint size (t : tally) : nat :=
  match t with
  | empty => 0
  | _ :: rest => S (size rest)
  end.

<section class="decl documented" id="size">
<div class="doc">
<p>How many counts a tally holds.</p>
</div>
<div class="args">
<p class="args-label">Arguments</p>
<div class="args-rows">
<div class="args-row" data-binders="b4.3">
<div class="args-sig"><span class="args-name">t</span><span class="args-type"> : <a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s0">tally</a></span></div>
<div class="args-text">the tally measured.</div></div></div></div>
<div class="panel">
<details class="body" open>
<summary data-lines="5 lines">
<pre class="statement"><code><span class="l"><span class="kw">Fixpoint</span> size (<span data-ref="b4.3">t</span> : <a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s0">tally</a>) : <span data-ref="x3">nat</span> :=
</span></code></pre></summary>
<pre class="statement"><code><span class="l" style="--i:2">  <span class="kw">match</span> <span data-ref="b4.3">t</span> <span class="kw">with</span>
</span><span class="l" style="--i:2">  | <a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s1">empty</a> =&gt; 0
</span><span class="l" style="--i:2">  | _<a href="/FSharp.Data.Rocq/example/Tally.Core.html#d1" data-ref="s7"> :: </a>rest =&gt; <span data-ref="x0">S</span> (<a href="/FSharp.Data.Rocq/example/Tally.Core.html#size" data-ref="s10">size</a> rest)
</span><span class="l" style="--i:2">  <span class="kw">end</span>.</span></code></pre></details><button type="button" class="refs-chip" aria-haspopup="dialog">uses 5 · used by 3</button>
<div class="args">
<p class="args-label">Arguments</p>
<div class="args-rows">
<div class="args-row" data-binders="b4.3">
<div class="args-sig"><span class="args-name">t</span><span class="args-type"> : <a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s0">tally</a></span></div>
<div class="args-text">the tally measured.</div></div></div></div></div>
<details class="refs">
<summary>References</summary>
<div class="ref-list" data-list="uses">
<p>Uses</p>
<ul>
<li><a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s0">tally</a></li>
<li><a href="/FSharp.Data.Rocq/example/Tally.Core.html#tally" data-ref="s1">empty</a></li>
<li><a href="/FSharp.Data.Rocq/example/Tally.Core.html#d1" data-ref="s7">::</a></li>
<li><span data-ref="x0">S</span></li>
<li><span data-ref="x3">nat</span></li></ul></div>
<div class="ref-list" data-list="used-by">
<p>Used by</p>
<ul>
<li><a href="/FSharp.Data.Rocq/example/Tally.Laws.html#counts_are_small" data-ref="s14">counts_are_small</a></li>
<li><a href="/FSharp.Data.Rocq/example/Tally.Laws.html#size_stable" data-ref="s15">size_stable</a></li>
<li><a href="/FSharp.Data.Rocq/example/Tally.Laws.html#size_append" data-ref="s16">size_append</a></li></ul></div></details></section>

In the browser