Navigator

Nacara.Plugin.Rocq publishes a compiled project as a static site. Pages read, fold and link with JavaScript off, and the client adds hover cards, search and settings.

Install

The package targets .NET 10 and is in preview. Add the feed that holds its Xantham.* dependency, then the package:

dotnet nuget add source https://nuget.cloudsmith.io/shayanhabibi/xantham/v3/index.json --name xantham-cloudsmith

dotnet add package Nacara.Plugin.Rocq --prerelease

Add it to a site

This is the complete program that built the site on the Site output page:

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 plugin also works beside other content. This documentation site is one Nacara site: the guide uses Partas.Nacara.Theme, and the example is a collection with Rocq.root "example", so its pages live under /example/:

let rocqOptions =
    Rocq.defaults
    |> Rocq.project "example/_CoqProject"
    |> Rocq.facts (Some "example/facts.json")
    |> Rocq.config (Some "example/navigator.json")
    |> Rocq.root "example"
    |> Rocq.home (Some ("Documentation", baseUrl))

Options

navigator.json

The file is optional, and so is every key. The example project uses this one:

{
  "falsifiedSuffix": "_falsified",
  "checkMarker": "@checked",
  "captureImports": ["Tally.Core"],
  "collapseCodeOver": 8
}

The first line of every multi-line code body is a fold for the rest, so readers can open or close any of them. Bodies start open unless collapseCodeOver closes them.

Types and assumption badges

A build never runs Rocq. Types and assumptions come from facts.json, which a separate command writes. It needs Rocq and the .vo files. A site builds without it, and shows no badges.

dotnet run -- rocq-capture --rocq "rocq" --out facts.json

The value of --rocq is split into words, so a wrapper works too. The example's facts were captured with Rocq 9.1.0 running in WSL, through wsl.exe and opam exec.

Print Assumptions takes most of the time, since Rocq walks a theorem's whole dependency tree on each call. The command splits its queries across --jobs Rocq processes running at once: by default the processor count, at most 8. Each process loads the whole project, so a project built on Iris needs about 1 GB per job.

Rocq code blocks

The plugin colours Markdown fences marked rocq or coq on any page of the site, with the lexer and keywords the library uses to read a source file:

(* Comments nest, and a string can hold a closing mark: "*)". *)
Theorem add_zero : forall n : nat, n + 0 = n.
Proof.
  induction n; simpl.
  - reflexivity.
  - rewrite IHn. reflexivity.
Qed.

Building the client

The plugin embeds its client bundle. A build from this repository needs the bundle first, and the script compiles it with Fickl:

bash navigator/build-client.sh

Minifying HTML

The default Nuglify.minifyHtml removes the comments that mark hydration roots. Cards, search, the settings and the right pane's lists would stop working, so the build fails with rocq/hydration-markers-stripped. Keep the comments:

|> Nuglify.minifyHtmlWith (Nuglify.htmlRemoveComments false)

Diagnostics