Facts

type Facts =
    {
        RocqVersion: string
        Digests: Map<string,string>
        Symbols: Map<string,SymbolFact>
    }


Assembly	`Nacara.Plugin.Rocq`

The contents of facts.json.

Fields

RocqVersion: string

Digests: Map<string,string>

Source digest at capture, by project-relative file path.

Symbols: Map<string,SymbolFact>

Facts by full Rocq name: see Facts.symbolKey.

Functions and values

capture (rocq: string array) (projectDir: string) (project: RocqProject) (config: Config) (jobs: int) : Result<Facts,string>

Runs Rocq over the compiled project and collects its facts.

Parameter
`rocq`	The command that starts `rocq`, followed by any arguments it needs first.
`projectDir`	The directory holding `_CoqProject` and the `.vo` files.
`project`	The project loaded from that directory.
`config`	Supplies the modules imported before capture.
`jobs`	The most `rocq repl` processes to run at once, each with the whole project loaded.

Returns. Error when Rocq fails to start or exits abnormally, or when a module fails to load.

captureScript (project: RocqProject) (config: Config) : string

The script for rocq repl: a Fail Check __nav_N. separator precedes command N.

captureScripts (project: RocqProject) (config: Config) (jobs: int) : string array

captureScript split into at most jobs scripts that together run each of its commands once, under the same number. Command N goes to script N mod the script count, which spreads the theorems evenly.

parseBinders (checkText: string) : Map<string,string>

The binders of the forall or ∀ opening checkText: name to type, empty when it has none.

parseTranscript (project: RocqProject) (transcript: string) : Map<string,SymbolFact>

Reads the output of captureScript for the same project. Every captured symbol has an entry.

read (path: string) : Result<Facts,string>

Reads facts.json. Returns Error naming the path when it is missing or malformed.

reconcile (dropStale: bool) (project: RocqProject) (facts: Facts) : Result<Facts,string array>

Matches facts to the project. Facts for symbols outside the project are dropped. A file whose digest differs from the recorded one is an error, or with dropStale loses its facts.

symbolKey (project: RocqProject) (symbol: ProjectSymbol) : string

The full Rocq name of a symbol, which keys Facts.Symbols.

write (path: string) (facts: Facts) : unit

Writes facts.json, with keys in sorted order.