← Command reference · lean-pkg formalization · CLI overview

lean-pkg formalization render

render formalization.yaml (v0.4, what Palomar reads) from the registry and the repo at HEAD; stdout unless –write/–out (formalization NAME is the same).

Also spelled: lean-pkg formalization NAME (all aliases).

Usage

lean-pkg formalization render [--write] [--no-registry] [--out PATH] [--force]
                              [--reason REASON] [--author NAME] [--headline-config PATH]
                              [--repo DIR] [--agent AGENT] [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag	Description
NAME	the package
--write	write <repo>/<formalization_yaml or formalization.yaml> and set the registry pointer (event updated); refuses a differing file without –force
--no-registry	with –write: write the file only; the registry is not updated (no pointer, no event), so this is not a registry write (no lock, no –commit)
--out PATH	write the render here instead; the registry is untouched
--force	with –write: overwrite a file that differs from the render; with –reason also override a live lease held by another agent
--reason REASON	with –write –force: why another agent’s lease is overridden (recorded in the updated event)
--author NAME	project.authors entry (repeatable); otherwise kept from the file, else consent[] owners/authors, else a placeholder
--headline-config PATH	the headline comparator configuration (the paper’s main results) for this render; –write also records it (registry headline_config). Default: the registry field, else comparator.headline.json when tracked. status.main_results then lists its theorems only, each covered by the gate-bound comparator receipt (else refused)
--repo DIR	read the checkout DIR instead of the registered local_path, for this call only (never saved): claims, comparator configurations, the kept keys and the receipts at DIR’s committed HEAD; the gate receipt’s facts only when bound to that HEAD. DIR must be a git work tree, and when it has remotes one must be the package’s repo; not with –write
--agent AGENT	lease holder, if one is live (for the registry update)

Details

Form	What it does	Key flags
formalization render NAME (or formalization NAME)	render formalization.yaml (mathlib-initiative v0.4, what Palomar reads) from the registry and the repo at HEAD; stdout by default; --write writes <repo>/<formalization_yaml or formalization.yaml>, is a no-op when equal, refuses a differing file without --force, then sets the registry pointer (event updated), so --write is a registry write; --write --no-registry writes the file only and leaves the registry untouched (no pointer, no event, no lock, --commit ignored; "registry_skipped": true); the lease (another agent’s live lease refuses unless --force --reason) and a dry run of the registry update are checked before the file is written; validated against the vendored schema; --headline-config PATH (else the registry’s headline_config, else comparator.headline.json when tracked) makes status.main_results list that headline configuration’s theorems only, refused unless the gate-bound comparator receipt covers every name and signs every hole, not applied (warning) when no receipt validates at HEAD; --write records it; --json headline {config, source, applied, reason, receipt, theorems} or null; see formalization.yaml	[--write [--no-registry]] [--out PATH] [--force [--reason TEXT]] [--author NAME]… [--headline-config PATH] [--agent A]