JSON and the command line

For a consumer outside .NET, Extract.run writes the project as JSON. Reading the result needs neither Rocq nor this library. JSON schema documents every field.

From F#

let extractTwice (outDir: string) =
    let options =
        {
            Project = "example/_CoqProject"
            OutDir = outDir
            RocqDep = None
            RocqVersion = Some "9.1.0"
            AllowStale = false
            Strict = true
            Force = false
        }

    let first = run options
    let second = run options
    printfn "first run:  %d extracted, %d reused, exit %d" first.Extracted.Length first.Reused.Length first.ExitCode
    printfn "second run: %d extracted, %d reused, exit %d" second.Extracted.Length second.Reused.Length second.ExitCode

A run rewrites only the layers of files whose .v or .glob changed:

first run:  3 extracted, 0 reused, exit 0
second run: 0 extracted, 3 reused, exit 0

The output for the example project:

files/Tally.Core.outline.json                5815 bytes
files/Tally.Core.refs.json                   1556 bytes
files/Tally.Core.tokens.json                 4689 bytes
files/Tally.Laws.outline.json               11188 bytes
files/Tally.Laws.refs.json                   2696 bytes
files/Tally.Laws.tokens.json                 8451 bytes
files/Tally.Prose.outline.json               9840 bytes
files/Tally.Prose.refs.json                  1318 bytes
files/Tally.Prose.tokens.json                5155 bytes
index.json                                   4750 bytes
xref.json                                    1650 bytes

Read only what you need. A table of contents needs index.json, and a rendered page needs the three layers of its file.

The shape of the index

let printIndexShape (outDir: string) =
    use document =
        JsonDocument.Parse (File.ReadAllBytes (Path.Combine (outDir, "index.json")))

    for property in document.RootElement.EnumerateObject () do
        match property.Value.ValueKind with
        | JsonValueKind.Array -> printfn "%-16s array of %d" property.Name (property.Value.GetArrayLength ())
        | JsonValueKind.Object ->
            let keys =
                property.Value.EnumerateObject ()
                |> Seq.map _.Name
                |> Seq.truncate 6

            printfn "%-16s { %s }" property.Name (String.concat ", " keys)
        | _ -> printfn "%-16s %s" property.Name (property.Value.GetRawText ())

schema           { major, minor }
layer            "index"
generator        { name, version }
rocqVersion      "9.1.0"
files            array of 3
declarations     { id, name, keyword, category, file, local }
symbols          { qualified, kind, file, local, decl }
fileGraph        { requires, externalRequires, references, externalReferences, rocqDep }
unknownKinds     {  }
unresolved       array of 0

From the command line

FSharp.Data.Rocq.Cli calls the same function. Both of these ran during this build:

$ FSharp.Data.Rocq.Cli extract --project example/_CoqProject --out .work/cli --force
extracted 3, reused 0; extract 172 ms, index 7 ms, total 182 ms
exit code 0

$ FSharp.Data.Rocq.Cli extract --project example/_CoqProject --out .work/cli
extracted 0, reused 3; extract 129 ms, index 11 ms, total 156 ms
exit code 0

A stale file stops the run with exit code 2, unless you allow it:

$ FSharp.Data.Rocq.Cli extract --project .work/stale/_CoqProject --out .work/cli-stale
extracted 0, reused 0; extract 0 ms, index 0 ms, total 109 ms
refused: theories/Core.v: stale .glob: it records digest 9ebb8b3ee52a6dfc8589a5e887011937, and the source has 09894747aa4d13e80757c112cfa9bd08. Recompile, or pass --allow-stale for lexical data only
exit code 2

$ FSharp.Data.Rocq.Cli extract --project .work/stale/_CoqProject --out .work/cli-stale --allow-stale
extracted 3, reused 0; extract 159 ms, index 7 ms, total 175 ms
exit code 0

Option	Effect
`--rocq-dep <file>`	Records the output of `rocq dep -f _CoqProject` as `index.fileGraph.rocqDep`
`--rocq-version <text>`	Records the Rocq version
`--allow-stale`	Keeps lexical data for a file with a stale `.glob`, instead of refusing
`--strict`	Exits 3 on an unknown `.glob` kind, as well as on an unparsed line
`--force`	Rewrites every file's layers

Exit codes: 0 success, 1 usage, 2 refused (stale or missing .glob), 3 .glob lines not understood.