Skip to content

Getting started

Install

Both packages target .NET 10 and are in preview, so --prerelease is required.

For the library:

dotnet add package FSharp.Data.Rocq --prerelease

For the Nacara plugin, which brings in the library, first add the feed that holds its Xantham.* dependency:

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

dotnet add package Nacara.Plugin.Rocq --prerelease

Compile the project

Both packages read what Rocq leaves behind, so compile first. Each .v needs a .glob beside it.

rocq compile -Q theories Tally theories/Core.v

Load it

load takes the path of a _CoqProject. This is the program, and what it printed when this page was built:

let loadProject () =
    match load "example/_CoqProject" with
    | Ok project ->
        for file in project.Files do
            printfn
                "%-12s %-20s %s %2d declarations %3d sentences %2d comments"
                file.Module
                file.Path
                (file.Digest.Substring (0, 8))
                file.Model.Declarations.Length
                file.Model.Sentences.Length
                file.Model.Comments.Length
    | Error failures ->
        for failure in failures do
            eprintfn "%s" (describeFailure failure)

Tally.Core   theories/Core.v      9ebb8b3e  5 declarations   8 sentences  5 comments
Tally.Laws   theories/Laws.v      4274b000  8 declarations  42 sentences 12 comments
Tally.Prose  theories/Prose.v     b168bd75  7 declarations  11 sentences 14 comments

load refuses a project with a stale or missing .glob, and returns every reason. See Library.

Publish it

To turn the same project into a site, add the plugin to a Nacara site. Navigator has the details.

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

Where to go next

You want Read
Declarations, proofs and source text in F# Library
What uses what References and dependencies
The data in another language JSON and the command line
A reader for your proofs Navigator
To write documentation in your .v files Prose syntax
Every type and function API reference