V

Generated by scripts/gen-format-pages.py from docs/data/format-metadata/, FILE_FORMATS.csv and docs/formats-master.csv. Do not edit by hand: change the source, then run the script.

Coq Preview.

At a glance

How much Poka reads

B4 Summary. The container and metadata are read and summarised (counts, properties, structure), but the main content is not rendered.

Confidence: medium (the reviewer read the code). Basis: Reviewed 2026-10-26: read parsers/poka-coq/src/main.rs (358 lines) and plugin.json in full. The crate has no unit tests and no tests/samples.rs, and the corpus has no .v sample, so the tier rests on reading the code. Covers .v. The output is a metadata card of counts found by matching text line by line: theorems, lemmas and corollaries, definitions, inductive types, fixpoints, records and structures, classes and instances, notations, hints, Tactic Notation and Ltac, sections and modules, Require statements, proof openings and Qed, Defined, Admitted and Abort, and line counts. Judgement: B4, because the structure is summarised but the source itself is never shown.

What Poka does not read

• The source text is not shown: the card carries only counts and a few sample names, with no code view or highlighting
• Constructs are found by matching text line by line, not by parsing, so multi-line declarations, nested or indented definitions and keywords inside strings or comments can be miscounted
• Counts of named items stop where their name list is capped (requires at 32), so a larger file under-reports them
• Files over 64 MiB are cut to the first 64 MiB (the card says so)
• Text that is not UTF-8 is decoded with replacement characters; no other encoding is tried
• Whether a proof is complete is not checked beyond counting Admitted and Abort

Libraries

Libraries Poka uses or has assessed for this format, with the status, licence and language the registry records.

• coq-lsp (candidate; LGPL-2.1; OCaml; https://github.com/ejgallego/coq-lsp) — Language server and checking engine for Rocq/Coq documents (successor to SerAPI); a document checker rather than a standalone parser library
• tree-sitter-rocq (candidate; licence unconfirmed; C; https://github.com/aruzdh/tree-sitter-rocq) — Experimental Rocq/Coq tree-sitter grammar aimed at syntax highlighting; no licence shown on the fetched page; grammar defined in JavaScript
• sv-parser (candidate; MIT OR Apache-2.0; Rust; https://github.com/dalance/sv-parser) — Only relevant if the .v files are Verilog: IEEE 1800-2017 SystemVerilog parser; accepted extensions not stated on the page
• tree-sitter-verilog (candidate; MIT; C; https://github.com/tree-sitter/tree-sitter-verilog) — Only relevant if the .v files are Verilog: SystemVerilog tree-sitter grammar; plain Verilog coverage not stated on the page

Sources

• parsers/poka-coq/src/main.rs
• parsers/poka-coq/plugin.json