CLI Reference¶

Prove has two CLIs:

• proof — the compiled binary (built from .prv source). Handles build, check, format, test, new, and lsp.
• prove (Python) — development and tooling commands: compiler, export, generate, index, intent, setup, view.

Requirements: Python 3.11+, gcc or clang

Build Commands (proof)¶

These commands are handled by the compiled proof binary. Build it once with python -m prove build proof/, then use ./proof/dist/proof (or install it to your PATH).

proof build [path]¶

Compile a Prove project to a native binary.

proof build
proof build path/to/project
proof build --no-mutate
proof build --debug

Runs the full pipeline: lex, parse, check, prove, emit C, compile with gcc/clang. Mutation testing runs by default.

The project directory must contain a prove.toml. The output binary and intermediate build artifacts (generated C, runtime files, PGO data) are placed in build/.

proof check [path]¶

Type-check, lint, and verify a Prove project.

proof check
proof check src/main.prv
proof check docs/tutorial.md --md
proof check --no-intent          # skip intent coverage
proof check --no-challenges      # skip refutation challenges

By default, check runs all available analyses — coherence, refutation challenges, completeness status, and intent coverage. Each analysis auto-skips silently when its data is absent (no project.intent, no narrative, no ensures contracts, no todo stubs). Use --no-* flags to opt out explicitly.

When path is a .prv file, checks that single file. When path is a directory, finds prove.toml and checks all files in src/. When path is a .md file (with --md), checks all fenced Prove blocks.

Reports type errors, warnings, and formatting issues in a unified summary. Formatting mismatches show a diff-style context excerpt.

proof test [path]¶

Run contract-based tests generated from ensures, believe, and near_miss annotations.

proof test
proof test --property-rounds 5000

The compiler parses and checks the source, generates a C test harness from the contracts, compiles it, and executes the tests.

proof format [path]¶

Format Prove source files.

proof format
proof format src/main.prv
proof format --status
proof format --stdin < src/main.prv
proof format docs/ --md

Reformats all .prv files recursively under the given path. Files with parse errors are skipped.

proof new <name>¶

Create a new Prove project with scaffolding.

proof new hello

Creates a directory with prove.toml, src/main.prv, and a .gitignore. Automatically builds the stdlib index and ML completion cache.

proof lsp¶

Start the Prove language server (LSP protocol).

proof lsp

Used by editor integrations (VS Code, Neovim, etc.) for diagnostics, completions, and hover information. Communicates over stdio.

Development Commands (prove)¶

These commands are part of the Python CLI (python -m prove or prove). They handle tooling, code generation, and data export.

prove setup¶

Re-download ML stores to ~/.prove/.

prove setup

ML stores are downloaded automatically to ~/.prove/ on first use — you do not need to run this command. Use it if your stores are corrupted or you want a clean reinstall.

For developers building stores from scratch (requires NLP deps): pip install 'prove[nlp]' then python scripts/build_stores.py.

prove generate <file>¶

Generate function stubs from narrative or intent. Auto-detects the file type:

• .prv — generate stubs from the module's narrative: block
• .intent — generate .prv files from a project intent file

prove generate src/auth.prv              # generate stubs from narrative
prove generate src/auth.prv --update     # re-generate @generated functions with todos
prove generate project.intent            # generate .prv files from intent
prove generate project.intent --dry-run  # preview without writing

For .prv files, the generator extracts verbs and nouns from the module's narrative: block, matches them against the stdlib knowledge base, and produces:

• Full bodies when a stdlib function matches with high confidence (includes explain, chosen, why_not prose annotations)
• Todo stubs when no stdlib match is found (the programmer fills these in)

Functions already present in the file are skipped.

prove intent [file.intent]¶

Work with .intent project declaration files.

prove intent                             # show status of all declarations
prove intent --drift                     # show only mismatches
prove intent --generate                  # generate .prv files from intent
prove intent --generate --dry-run        # preview without writing

The .intent file is a human-readable project declaration that describes modules, vocabulary, data flow, and constraints. The toolchain generates .prv source files from it and verifies the code stays aligned.

Intent coverage is checked automatically by proof check (skip with --no-intent).

prove view <file>¶

Display the AST of a .prv file for debugging.

prove view src/main.prv

Prints a human-readable, indented representation of the parsed AST.

prove compiler <file>¶

Convert between .prv lookup types and PDAT binary format.

prove compiler --load src/data.prv
prove compiler --dump Data.dat
prove compiler --dump Data.dat -o data.prv

When neither --load nor --dump is given, the mode is auto-detected from the file extension (.prv → load, .dat/.bin → dump).

The PDAT binary format matches the C runtime (prove_store.c) exactly — files produced by this command are interchangeable with the Store runtime at execution time.

prove index [path]¶

Rebuild the .prove_cache ML completion index.

prove index

prove export¶

Export syntax highlighting data to companion lexer projects (tree-sitter, Pygments, Chroma).

prove export
prove export -f treesitter --build

Exit Codes¶