check

Arguments and rejection

Accept zero or one entry operand. Without an entry, load the package selected by --root or the current directory. With an entry, resolve that compilation unit under the selected source root.

Accept the listed compiler, lock, export, verbosity, root, profile, format, language, and resource options. --types and --json are rejected. A profile cannot be combined with --exports-json, and it must match the selected canonical language profile.

Reject unreadable inputs, invalid package metadata, missing dependencies, lock mismatches, parse errors, name resolution errors, type errors, and profile violations before any program execution.

Output

Unprofiled SELF output follows the check channel rule. A successful standalone check writes the entry label with types-ok and resolve-ok summaries. Profile checks include the profile name.

JSON diagnostics are newline-delimited objects on standard error. Each object carries string code, severity, and message fields, one primary label, a secondary label array, and a string notes array. Each label has string file and message fields, integer line, col, endLine, endCol, lo, and hi fields. Label coordinates follow the source position rule.

A profile diagnostic uses a topaz.profile-diagnostic/v1 object with string profile, nullable string rule, the nested diagnostic object, and nullable fix. A fix has string applicability equal to machine-applicable, string description, and an edit object. The edit carries file, line, col, endLine, endCol, lo, hi, and string replacement with the same coordinate meanings as a label.

A profile check with JSON output writes one topaz.profile-check/v1 summary on standard output with profile, language, status, diagnosticCount, and errorCount. Status is pass or fail. Counts are nonnegative integers.

Successful export inspection follows the checked export rule. The export object's modules array identifies each module by identity, signatureHash, and ambient, with values, aliases, records, enums, newtypes, and conformances arrays. Value rows carry name, type, vars, bounds, required, namesKnown, names, and defaulted. Export data is omitted on failure. Diagnostic JSON and export JSON may be selected together because they serve different purposes.

Each alias row has string name, nonnegative integer params, and string type. params counts declared type parameters. type contains the declaration's target type text.

Each record row has string name, nonnegative integer params, and a fields array. Each field has string name, string type, and boolean hasDefault. Fields retain declaration order. hasDefault records whether a default initializer exists and does not serialize its value.

Each enum row has string name, nonnegative integer params, and a variants array. Each variant has string name and a payloads array of type strings. Variants and payloads retain declaration order. A variant with no payload has an empty payloads array.

Each newtype row has string name, nonnegative integer params, and string base. base contains the declaration's underlying type text. Alias, field, payload, and base type text retains declaration spelling and need not use the checked value type renderer.

The conformances field is an empty array in this report. It leaves the module's protocol membership unspecified. Consumers must not infer that a module implements no protocols from that field.

A value row's vars counts declared function type parameters when its function declaration metadata is available. bounds has one string array per type parameter. names and defaulted align in parameter declaration order. required counts declared parameters without a default initializer.

When namesKnown is false, declaration parameter metadata is unavailable. The accompanying zero vars and required values and empty bounds, names, and defaulted arrays are placeholders. They do not establish zero arity or the absence of generic parameters.

A value type equal to unknown records the absence of an exported checked type node. The checked type renderer uses ? for an unknown semantic type and ?inference for an inference variable. These strings remain explicit metadata states and must not be treated as established concrete types.

The modules array includes resolved module identities even when a module has no exported rows. Module identities are sorted, and declaration rows within each category are sorted by exported name. Field, variant, payload, parameter, and bound order follows the declaration.

signatureHash is sha256 followed by a colon and 64 lowercase hexadecimal digits. It fingerprints the serialized module report body before the hash field is inserted. That body includes identity, ambient, and the six declaration arrays. Function bodies and default initializer values are not serialized into that body. Package integrity is established through the lock and package content identities.

Argument, loader, and compiler-startup errors remain textual errors on standard error. Selecting JSON diagnostics does not turn a command-validation failure into a source diagnostic.

Exit status

Exit 0 means the unit passed all selected checks and its requested report was produced. Exit 1 covers argument errors, package or lock errors, source diagnostics, profile rejection, report failure, worker failure, and resource exhaustion.

Filesystem effects

Read the source graph, manifest, lock, installed standard library, and existing vendor tree. Do not modify project inputs or materialize dependencies. Compiler-owned temporary files may be used.

Network access

Checking performs no network access. A missing dependency is an error and never starts a registry download.

Reproducibility

Fixed source and dependency bytes, lock identity, root and entry paths, language and profile, compiler identity, and presentation settings produce the same diagnostics and public export ordering. Host resource failures are external inputs.

Packages and locks

Package dependencies use table declarations. Registry dependencies require a valid matching lock and existing verified vendor content. --locked verifies the existing lock before checking and never rewrites it. A standalone entry cannot use --locked to create package context.

Registry dependencies or Lispex configuration require explicit --locked, even when a matching lock exists. Without that option, a local-only package can load declared path dependencies by their expected hashes. Locked loading rejects missing or stale state and never repairs it.

Standalone entry mode rejects --locked. Selected-entry test is the exception when an explicit root contains the package manifest and the entry belongs to that package.

The invocation topaz check main.tpz --language-version 5.21 is expected to exit with 0.