Skip to content

API Reference

The API reference is rendered from Python source with mkdocstrings.

Package

se_theory_reference_kit package.

Base

base/init.py - Shared base utilities for theory-reference tooling.

ArtifactLoadError

Bases: ReferenceKitError

Raised when a reference artifact cannot be loaded.

CheckResult dataclass

One validation finding emitted by one check.

Attributes:

Name Type Description
check_id str

Stable id of the check that emitted the finding.
status CheckStatus

Check status.
severity CheckSeverity

Finding severity.
message str

Human-readable finding message.
artifact_id str | None

Optional artifact id associated with the finding.
path Path | None

Optional path associated with the finding.
detail JsonDetail

Optional structured detail for reports or downstream tooling.

CheckSeverity

Bases: StrEnum

Severity vocabulary for one validation finding.

CheckStatus

Bases: StrEnum

Status vocabulary for one validation finding.

ConfigurationError

Bases: ReferenceKitError

Raised when repo-provided reference configuration is invalid.

ReferenceKitError

Bases: Exception

Base exception for theory-reference-kit failures.

RepositoryRootError

Bases: ReferenceKitError

Raised when a repository root cannot be resolved.

cannot_verify(check_id, message, *, artifact_id=None, path=None, detail=None)

Create a cannot-verify result.

failure(check_id, message, *, artifact_id=None, path=None, detail=None)

Create an error failure result.

find_repository_root(start=None)

Find the nearest repository root from a starting path.

Parameters:

Name Type Description Default
start Path | None

Starting path. Defaults to the current working directory.

 None

Returns:

Type Description
Path

Resolved repository root path.

Raises:

Type Description
RepositoryRootError

If no repository root marker is found.

lean_module_to_path(module, *, root=None, lean_public_root)

Resolve a Lean module name to its repository source path.

Parameters:

Name Type Description Default
module str

Lean module name.

 required
root Path | None

Repository root.

 None
lean_public_root str

Expected public Lean root for the owning repository.

 required

Returns:

Type Description
Path

Repository-contained Lean source path.

Raises:

Type Description
PathResolutionError

If the module name is empty, path-like, malformed, or outside the declared public Lean root.

ok(check_id, message, *, artifact_id=None, path=None, detail=None)

Create an ok result.

partial(check_id, message, *, artifact_id=None, path=None, detail=None)

Create a partial result.

reference_artifact_path(path, *, root=None, reference_dir_name='reference')

Resolve a declared reference artifact path.

The declared path must be repository-relative and under the reference directory.

Parameters:

Name Type Description Default
path str | Path

Declared repository-relative artifact path.

 required
root Path | None

Repository root.

 None
reference_dir_name str

Name of the reference artifact directory.

 'reference'

Returns:

Type Description
Path

Resolved reference artifact path.

Raises:

Type Description
PathResolutionError

If the path is outside the reference directory.

reference_dir(*, root=None, reference_dir_name='reference')

Return the repository reference directory.

reference_index_path(*, root=None, reference_dir_name='reference', reference_index_name='index.toml')

Return the repository reference index path.

resolve_repo_path(path, *, root=None)

Resolve a path as repository-relative and contained within the repository.

Parameters:

Name Type Description Default
path str | Path

Repository-relative path.

 required
root Path | None

Repository root. Defaults to nearest detected repository root.

 None

Returns:

Type Description
Path

Resolved absolute path.

Raises:

Type Description
PathResolutionError

If the path escapes the repository root.

warning(check_id, message, *, artifact_id=None, path=None, detail=None)

Create a warning failure result.

worst_status(results)

Return the worst status across validation results.

Declarations

declarations/init.py - Typed declarations consumed by the generic engine.

ExportSpec dataclass

A generated JSON artifact export specification.

The kit owns this model shape. Each theory repository owns the tuple of export specifications.

SurfaceSymbols dataclass

Kinded public Lean surface symbols for one theory repository.

all_symbols property

Return all declared public surface symbols.

from_optional_kinds(*, types=EMPTY_STRING_SET, predicates=EMPTY_STRING_SET, axioms=EMPTY_STRING_SET, theorems=EMPTY_STRING_SET, requirements=EMPTY_STRING_SET, vocabulary=EMPTY_STRING_SET, witnesses=EMPTY_STRING_SET) classmethod

Build a surface declaration from common optional surface kinds.

symbols_for_kind(kind)

Return public symbols for one surface kind.

TheoryReferenceConfig dataclass

Repository-specific configuration consumed by the generic engine.

Lean

lean/init.py - Generic Lean source inspection helpers.

LeanDecl dataclass

Lean declaration with name, kind, and reference section.

expected_symbols_for_kind(surface, kind)

Return expected public Lean symbols for a surface kind.

Missing kinds return an empty set. The owning theory repository supplies the surface symbols; the kit only reads the generic shape.

Parameters:

Name Type Description Default
surface SurfaceSymbols

Repo-owned public surface declaration.

 required
kind str

Surface kind.

 required

Returns:

Type Description
frozenset[str]

Expected symbols for that kind.

extract_decls(lean_file)

Extract top-level Lean declarations from a Lean file.

Parameters:

Name Type Description Default
lean_file Path

Lean source file.

 required

Returns:

Type Description
list[LeanDecl]

Extracted declarations. Missing files return an empty list.

extract_for_section(lean_file, target_section)

Extract Lean declarations matching a reference section.

Parameters:

Name Type Description Default
lean_file Path

Lean source file.

 required
target_section str

Reference section name.

 required

Returns:

Type Description
list[LeanDecl]

Declarations whose Lean kind belongs to the requested section.

extract_spec_ids(spec_file)

Extract stable citation ids from a Lean Spec file.

Parameters:

Name Type Description Default
spec_file Path

Lean Spec source file.

 required

Returns:

Type Description
set[str]

Citation id string values. Missing files return an empty set.

infer_core_modules(surface_module, lean_root)

Infer Core modules under a public Surface module namespace.

Parameters:

Name Type Description Default
surface_module str

Public surface module, typically ending in ".Surface".

 required
lean_root Path

Lean source root.

 required

Returns:

Type Description
list[str]

Inferred Core module names. Returns an empty list when the surface module
list[str]

does not follow the expected Surface naming pattern or no Core files are
list[str]

found.

infer_spec_module(surface_module)

Infer the Spec module from the public surface module.

Parameters:

Name Type Description Default
surface_module str

Public surface module.

 required

Returns:

Type Description
str

Inferred Spec module name.

lean_module_to_relative_path(module)

Convert a Lean module name to a relative Lean source path.

Parameters:

Name Type Description Default
module str

Lean module name.

 required

Returns:

Type Description
Path

Relative Lean source path.

Raises:

Type Description
PathResolutionError

If the module name is empty, malformed, or path-like.

missing_expected_surface_symbols(*, surface, registered)

Return expected public-surface symbols missing from reference registries.

Parameters:

Name Type Description Default
surface SurfaceSymbols

Repo-owned public surface declaration.

 required
registered set[str]

Lean symbols already registered in reference artifacts.

 required

Returns:

Type Description
set[str]

Expected symbols not present in registered symbols.

path_to_module(path, lean_root)

Convert a Lean file path to a Lean module name.

Parameters:

Name Type Description Default
path Path

Lean source file.

 required
lean_root Path

Root directory used for module-relative path conversion.

 required

Returns:

Type Description
str

Dotted Lean module name.

Reference

reference/init.py - Generic reference artifact tooling.

LoadedReferenceArtifact dataclass

Loaded reference artifact.

Attributes:

Name Type Description
artifact_id str

Stable artifact id from the reference index.
path Path

Resolved artifact path.
kind str

Artifact kind declared by the owning repository.
data ReferenceDocument

Parsed TOML data.

ReferenceRegistry dataclass

Loaded reference artifact registry.

Attributes:

Name Type Description
artifacts tuple[LoadedReferenceArtifact, ...]

Loaded reference artifacts in index order.

by_id()

Return loaded artifacts keyed by artifact id.

build_reference_registry(artifact_declarations, *, root, reference_dir_name='reference')

Build a registry from artifact declarations.

Parameters:

Name Type Description Default
artifact_declarations list[ArtifactDeclaration]

Artifact declarations from reference/index.toml.

 required
root Path

Repository root.

 required
reference_dir_name str

Reference directory name.

 'reference'

Returns:

Type Description
ReferenceRegistry

Loaded reference registry.

discover_reference_artifacts(*, root=None, reference_dir_name='reference')

Discover TOML reference artifacts under the reference directory.

Parameters:

Name Type Description Default
root Path | None

Repository root.

 None
reference_dir_name str

Reference directory name.

 'reference'

Returns:

Type Description
tuple[Path, ...]

Sorted reference TOML paths.

load_reference_artifact(artifact, *, root, reference_dir_name='reference')

Load one reference artifact declared in the reference index.

Parameters:

Name Type Description Default
artifact ArtifactDeclaration

Artifact declaration from reference/index.toml.

 required
root Path

Repository root.

 required
reference_dir_name str

Reference directory name.

 'reference'

Returns:

Type Description
LoadedReferenceArtifact

Loaded reference artifact.

Raises:

Type Description
ValueError

If the declaration lacks a valid path.

make_stub(declaration, source_module)

Create a generic reference entry stub for a Lean declaration.

Parameters:

Name Type Description Default
declaration LeanDecl

Lean declaration.

 required
source_module str

Source module for the declaration.

 required

Returns:

Type Description
ReferenceEntry

Reference entry stub.

merge_entry(existing, generated, *, overwrite)

Merge an existing hand-authored entry with generated fields.

Parameters:

Name Type Description Default
existing ReferenceEntry

Existing entry.

 required
generated ReferenceEntry

Generated stub fields.

 required
overwrite bool

If true, generated values replace existing values.

 required

Returns:

Type Description
ReferenceEntry

Merged entry.

ordered_table_values(document, table_name)

Return nested table values sorted by order, then id/key.

Parameters:

Name Type Description Default
document ReferenceDocument

Parsed reference artifact.

 required
table_name str

Top-level table name.

 required

Returns:

Type Description
list[dict[str, object]]

Ordered table entries. Each entry receives an id if missing.

Raises:

Type Description
ValueError

If the table is not a table of tables.

reference_artifact_meta(document)

Return normalized metadata from a reference artifact.

Parameters:

Name Type Description Default
document ReferenceDocument

Parsed reference artifact.

 required

Returns:

Type Description
dict[str, object]

Copy of the [meta] table, or an empty dictionary when absent.

Raises:

Type Description
ValueError

If [meta] is present but not a table.

reference_stub_key(declaration)

Return the default reference stub key for a Lean declaration.

Parameters:

Name Type Description Default
declaration LeanDecl

Lean declaration.

 required

Returns:

Type Description
str

Stub key.

registered_lean_symbols(registry, *, sections=None)

Return Lean symbols registered in reference artifacts.

Parameters:

Name Type Description Default
registry ReferenceRegistry

Loaded reference registry.

 required
sections frozenset[str] | None

Optional section filter.

 None

Returns:

Type Description
set[str]

Registered Lean symbol names.

section_entries(data, section)

Return table entries for a reference section.

Parameters:

Name Type Description Default
data ReferenceDocument

Parsed reference artifact.

 required
section str

Section name.

 required

Returns:

Type Description
SectionEntries

Section entries keyed by entry id.

source_modules_in_registry(data)

Return source modules declared inside a reference artifact.

Parameters:

Name Type Description Default
data ReferenceDocument

Parsed reference artifact.

 required

Returns:

Type Description
list[str]

Source module names in first-seen order.

validate_reference_artifact_shape(*, check_id, artifact)

Validate generic reference artifact shape.

Parameters:

Name Type Description Default
check_id str

Validation check id.

 required
artifact LoadedReferenceArtifact

Loaded reference artifact.

 required

Returns:

Type Description
tuple[CheckResult, ...]

Validation findings.

validate_required_fields(*, check_id, artifact, section, required_fields=REQUIRED_ENTRY_FIELDS)

Validate required fields for all entries in one reference section.

Parameters:

Name Type Description Default
check_id str

Validation check id.

 required
artifact LoadedReferenceArtifact

Loaded reference artifact.

 required
section str

Section name.

 required
required_fields Iterable[str]

Required field names.

 REQUIRED_ENTRY_FIELDS

Returns:

Type Description
tuple[CheckResult, ...]

Validation findings.

Export

export/init.py - Generic generated export helpers.

CatalogEntry dataclass

Generic catalog entry for one loaded reference artifact.

ExportResult dataclass

Result of one generated export operation.

Attributes:

Name Type Description
output_path Path

Generated output path.
current bool

True when output is current or was written.
wrote bool

True when output was written.
checked bool

True when the operation ran in check mode.

build_reference_catalog(*, registry, schema, source, namespace, artifact)

Build a generic reference catalog from loaded reference artifacts.

This function builds the common catalog envelope and reference path list. Repo-specific catalog payload sections remain owned by the theory repo.

Parameters:

Name Type Description Default
registry ReferenceRegistry

Loaded reference registry.

 required
schema str

Catalog schema id.

 required
source str

Owning repository slug.

 required
namespace str

Reference namespace.

 required
artifact str

Catalog artifact name.

 required

Returns:

Type Description
JsonObject

JSON-compatible catalog payload.

build_registry_payload(*, spec, document, source_path, repo_slug, reference_namespace)

Build one generated registry payload from one reference artifact.

Parameters:

Name Type Description Default
spec ExportSpec

Repo-owned export specification.

 required
document ReferenceDocument

Parsed reference artifact.

 required
source_path Path

Source reference artifact path.

 required
repo_slug str

Owning repository slug.

 required
reference_namespace str

Reference namespace for generated payloads.

 required

Returns:

Type Description
JsonObject

JSON-compatible generated registry payload.

export_registries(*, specs, registry, reference_root, output_root, repo_slug, reference_namespace, check)

Export generated registry JSON artifacts.

Parameters:

Name Type Description Default
specs tuple[ExportSpec, ...]

Repo-owned export specifications.

 required
registry ReferenceRegistry

Loaded reference registry.

 required
reference_root Path

Reference artifact root.

 required
output_root Path

Generated output root.

 required
repo_slug str

Owning repository slug.

 required
reference_namespace str

Reference namespace.

 required
check bool

If true, check freshness without writing.

 required

Returns:

Type Description
tuple[ExportResult, ...]

Export results.

export_registry(*, spec, registry, reference_root, output_root, repo_slug, reference_namespace, check)

Export one registry JSON artifact.

Parameters:

Name Type Description Default
spec ExportSpec

Repo-owned export specification.

 required
registry ReferenceRegistry

Loaded reference registry.

 required
reference_root Path

Reference artifact root.

 required
output_root Path

Generated output root.

 required
repo_slug str

Owning repository slug.

 required
reference_namespace str

Reference namespace.

 required
check bool

If true, check freshness without writing.

 required

Returns:

Type Description
ExportResult

Export result.

Raises:

Type Description
FileNotFoundError

If the source artifact is not loaded in the registry.

Validation

validation/init.py - Checks, registry, runner, and default check set.

Public surface
  • Check, CheckRegistry the check contract and its catalogue
  • CheckResult, CheckStatus, ... the result vocabulary
  • RunReport, run_checks execution with crash isolation
  • default_registry, DEFAULT_CHECKS the kit's fixed generic check set

Check dataclass

A registered check: a function plus its catalogue metadata.

Attributes:

Name Type Description
check_id str

Stable, unique id.
title str

Short human-readable description for logs and reports.
run CheckFunc

The check function.
strict_only bool

When true, the check runs only in strict mode.

CheckRegistry dataclass

An immutable, ordered collection of checks.

Order is preserved so runs are deterministic and the default generic checks always precede consumer-appended checks. Ids must be unique across the registry.

__post_init__()

Reject duplicate check ids at construction time.

extend(*checks)

Return a new registry with the given checks appended.

The kit's defaults are never mutated; a consumer extends them. The returned registry preserves order and re-validates id uniqueness, so a consumer cannot shadow a default id.

extended_with(checks)

Return a new registry appending an iterable of checks.

ids()

Return the check ids in order.

select(*, strict)

Return the checks that should run for the given mode.

In non-strict mode, strict-only checks are skipped. In strict mode, all checks run.

CheckResult dataclass

One validation finding emitted by one check.

Attributes:

Name Type Description
check_id str

Stable id of the check that emitted the finding.
status CheckStatus

Check status.
severity CheckSeverity

Finding severity.
message str

Human-readable finding message.
artifact_id str | None

Optional artifact id associated with the finding.
path Path | None

Optional path associated with the finding.
detail JsonDetail

Optional structured detail for reports or downstream tooling.

CheckSeverity

Bases: StrEnum

Severity vocabulary for one validation finding.

CheckStatus

Bases: StrEnum

Status vocabulary for one validation finding.

ReferenceRunContext dataclass

Resolved read-only context for theory-reference validation.

Attributes:

Name Type Description
repo_root Path

Repository root.
config TheoryReferenceConfig

Repo-provided reference configuration.
surface SurfaceSymbols

Repo-provided public Lean surface declaration.
export_specs tuple[ExportSpec, ...]

Repo-provided generated export specifications.
reference_index ReferenceIndex | None

Parsed reference index, when already loaded.

generated_root property

Return the generated data directory.

reference_index_path property

Return the reference index path.

reference_root property

Return the reference artifact directory.

RunReport dataclass

The outcome of running a registry against a context.

Attributes:

Name Type Description
results tuple[CheckResult, ...]

Every finding from every check, in check order.
strict bool

Whether the run was executed in strict mode.
overall_status CheckStatus

Worst status across all results.

exit_code property

Return the process exit code: 0 when passed, 1 otherwise.

failures property

Return results that count as failures for this run's mode.

Error-severity findings always count. Warning-severity findings count only under strict mode. Cannot-verify always counts.

passed property

Return true when no findings count as failures for this mode.

default_registry()

Return the kit's default registry of generic checks.

Returns a fresh CheckRegistry each call. Consumers extend it to add repo-specific checks; the kit's defaults are never mutated.

run_checks(*, registry, context, strict=False)

Run selected checks against the context with crash isolation.

Each check is executed independently. If a check raises ReferenceKitError, it is recorded as a cannot-verify result and the run continues. One broken check never hides the results of the others.

Commands

Command implementations for cli.