Skip to content

FSharp.Data.Rocq

Typed access to a compiled Rocq project from F#, and a static reader for its proofs.

Get started Open the example site Comment syntax
FSharp.Data.Rocq

Sentences, declarations, proofs, comments, resolved references and file dependencies, as F# values or JSON. It reads .v and .glob files, and it does not need Rocq installed.

 Nacara.Plugin.Rocq

A Nacara plugin that publishes a project as a site: a page per module, a Guarantees page, hover cards, search and two looks.

Install

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

dotnet add package FSharp.Data.Rocq --prerelease

The Nacara plugin 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

Everything here is real

A small Rocq project, Tally, is compiled and committed beside the site. Each build runs the code you see against it and places the output under the code. This is the example site, built by the plugin as part of this site: