check | Topaz

Synopsis and input

`topaz check`

Форма вызова

topaz check [entry] [--format human|json] [--exports-json]

Ввод

With entry, check the selected source unit. Without an entry, use package mode and load topaz.toml from the selected package root. In package mode, --locked requires the lock root manifest hash to match the current manifest before compilation.

Параметры и конфликты

Параметр	Значение по умолчанию	Контракт	Конфликты
`--format human\|json`	human	Select human or JSON diagnostics for check. The shared format rule lists the commands that accept JSON output.	Не перечислены
`--exports-json`	Не указано	On a clean checked unit, write its public export surface as one JSON object. Rejected on other commands.	`--profile`
`--profile available-profile`	Не указано	Select a recognized check profile. The installed distribution must include its required assets and execution support.	`--exports-json`
`--compiler self\|rust`	self	Select the compiler. SELF is the default. The rust value selects the reference compiler.	Не перечислены
`--language-version 5.21`	Не указано	Select the documented language mode.	Не перечислены
`--root dir`	Не указано	Select the module/package root. For an explicit entry, the default root is its directory and the entry must be under the root.	Не перечислены
`--locked`	Не указано	Require the package lock check in package mode.	Не перечислены

Каналы вывода

stdout

For a clean checked unit, --exports-json writes one checked public export-surface JSON object to standard output and returns success.

Связанное правило · Checked export output →

Resolver and checker diagnostics use standard error and make the unprofiled SELF check fail. Human success status uses standard output. A clean check in JSON diagnostic mode emits no human success banner. Diagnostic JSON, checked exports, and profile summaries are separate outputs.

Связанное правило · Diagnostic and success channels →

stderr

Resolver and checker diagnostics use standard error and make the unprofiled SELF check fail. Human success status uses standard output. A clean check in JSON diagnostic mode emits no human success banner. Diagnostic JSON, checked exports, and profile summaries are separate outputs.

Связанное правило · Diagnostic and success channels →

Статус завершения

0

The selected compilation unit checks successfully.

nonzero

Options are invalid, the compilation product is invalid, or resolver/checker diagnostics are reported. Failures can use plain-text messages even in JSON diagnostic mode.

Эффекты

Дополнительные контракты не определены.

Checking does not execute the program. The check command defines package loading, root and lock handling, and filesystem effects.

Operation

Ссылка

Правилоtopaz.rule.check.compilation-unit

Checking a compilation unit

check parses, resolves, and type checks the selected Topaz compilation unit. It does not run the checked program.

Package selection, root and lock handling, and profiles follow the check command.

Причина

Checking resolves and types the compilation unit before execution. Keeping execution separate lets callers validate code without running its effects.

Примеры Check the first program →

Options and conflicts

Ссылка

Правилоtopaz.rule.check.exports-option

Scope of --exports-json

--exports-json applies to check. Using it with run is rejected during command validation before the program executes.

Причина

--exports-json describes the checked export surface. Rejecting it for other commands prevents an accepted flag from silently doing nothing.

Примеры Reject --exports-json on run →

Диагностика --exports-json requires check →

Правилоtopaz.rule.check.json-option

Diagnostic JSON option

Use --format json for check diagnostics. check --json is rejected; it is not an alias for --format json.

The shared format rule defines the commands that accept JSON output.

Причина

--format json names the diagnostic format explicitly. Rejecting --json on check avoids a second spelling for the same request.

Примеры Reject --json on check →

Диагностика --json is not the check diagnostic format →

--format json and --exports-json are not mutually exclusive in the reviewed validator. --profile cannot be combined with --exports-json. A concrete profile example requires verified membership in the selected default distribution.

Results and output channels

Ссылка

Правилоtopaz.rule.check.exports

Checked export output

For a clean checked unit, --exports-json writes one checked public export-surface JSON object to standard output and returns success.

The complete export schema follows the check command.

Причина

Tools need the checked public names and types without executing their module. A JSON object makes that interface available as structured data.

Примеры Check and emit export JSON →

Правилоtopaz.rule.check.channels

Diagnostic and success channels

Resolver and checker diagnostics use standard error and make the unprofiled SELF check fail. Human success status uses standard output. A clean check in JSON diagnostic mode emits no human success banner. Diagnostic JSON, checked exports, and profile summaries are separate outputs.

Diagnostic and profile-summary fields follow the check command.

The clean JSON example asserts empty output streams. The primitive mismatch example checks a diagnostic on standard error and empty standard output. The safe command recipe checks successful exit without asserting human output bytes.

Причина

Separate channels let callers pipe successful output without mixing it with diagnostics. Suppressing the success banner keeps JSON output parseable.

Примеры Keep the check diagnostic format →An integer is not implicitly a float →Small source invocation →

A profile check has additional output behavior and must carry its profile identity. The reviewed SELF path emits a profile summary on standard output in JSON mode. That object is separate from the checked export surface.

Examples

Ссылка

Check the first program

Ссылка

check · checking · Проверка · Пройдено

first-program.tpzCheck the first programОткрыть песочницу →

import std.io
function greet(name: string) -> string {
return "Hello, {name}!"
}
io.writeLine(greet("Topaz"))

Зафиксированный выводКод завершения 0

first-program.tpz: types-ok (2 modules)
first-program.tpz: resolve-ok (2 modules)

$ topaz check first-program.tpz --compiler self · Зафиксировано с Топазом 5.21.3

Ожидаемый результат

Проверка принимает программу. Код завершения 0.

Наблюдаемые утверждения · Пройдено · 5.21.3

2026-11-06T04:37:26.2102809Z · checking · sha256:b6c3f574b78c558b526196fa04f5d835c9fe1df59d07397dbf4e5d279a3e1665

Код завершения 0.

Наблюдаемый стандартный вывод

first-program.tpz: types-ok (2 modules)
first-program.tpz: resolve-ok (2 modules)

Нет вывода ошибок.

Пройдено · expected 0; observed 0

Наблюдаемые утверждения · Пройдено · 5.21.3

2026-11-06T13:40:27.7737018Z · checking · sha256:b6c3f574b78c558b526196fa04f5d835c9fe1df59d07397dbf4e5d279a3e1665

Код завершения 0.

Наблюдаемый стандартный вывод

first-program.tpz: types-ok (2 modules)
first-program.tpz: resolve-ok (2 modules)

Нет вывода ошибок.

Пройдено · expected 0; observed 0

Check and emit export JSON

Ссылка

check · checking · Проверка · Не выполнялось

first-program.tpzCheck and emit export JSONОткрыть песочницу →

import std.io
function greet(name: string) -> string {
return "Hello, {name}!"
}
io.writeLine(greet("Topaz"))

Ожидаемый выводКод завершения 0

$ topaz check first-program.tpz --compiler self --format json --exports-json · Целевой продукт 5.21.3

Ожидаемый результат

Проверка принимает программу. Код завершения 0.

Нет вывода ошибок.

Стандартный вывод содержит объект JSON. Полная схема не определена.

Этот пример ещё не выполнялся.

This example checks one JSON object on standard output. The check command defines its complete export schema and distinguishes unknown metadata from an empty export list.

Reject --exports-json on run

Ссылка

reject · command-validation · Проверка · Пройдено

first-program.tpzReject --exports-json on runОткрыть песочницу →

import std.io
function greet(name: string) -> string {
return "Hello, {name}!"
}
io.writeLine(greet("Topaz"))

Фрагмент зафиксированного выводаКод завершения 1

Нет стандартного вывода.

topaz: `--compiler self` accepts `--exports-json` only on `check`

topaz — Topaz toolchain developer driver (run `topaz --version`)

USAGE:
    topaz <COMMAND> [ARGS]

COMMANDS:
    parse <file>      parse a Topaz source file and report diagnostics
    dump-ast <file>   parse a Topaz source file and print the AST
    check [entry]     parse + resolve + type a selected compilation unit
                      (no entry = package mode from topaz.toml)
    run [entry]       execute a checked program (no entry = package mode)
    test [entry]      run a checked selected unit on the deterministic TestHost
                      (--root <package> keeps its manifest, lock, and dependencies
                      for a selected entry; no entry uses the manifest entry)
    fmt [entry]       parse-gated deterministic whitespace formatting
                      (`--check` reports drift without writing;
                      no entry = package mode; skips vendor/target)
    lsp               run the deterministic stdio language server; package
                      diagnostics use initialize.rootUri (or --root) with a
                      valid locked package and open-document overlays
    emit [entry]      expose generated Rust source for inspection/integration
                      (`--target rust`); print the primary source to stdout,
                      or write the complete source set with --out-dir <dir>
                      (--root <dir>; no entry = package mode)
    build [entry]     lower + scaffold (--out-dir <dir>, required) + drive
                      cargo to build a native binary at
                      <dir>/target/<profile>/program (final binary only), or with
                      --target web a wasm package at <dir>/topaz-web.wasm
                      (--target web-worker also emits worker glue)
                      (--release for an optimized build; --run to execute
                      native builds after building; no entry = package mode)
    init              scaffold a deterministic current-profile native package
                      at --root (default `.`); refuses to overwrite existing
                      files
    add <dep>         add a dependency to topaz.toml (`name@version`, or
                      `name --path <relative-path>` with content hash)
    lock              write deterministic topaz.lock for the package at
                      --root (default `.`); local/path dependency hashes must
                      already match topaz.toml
    fetch             fetch registry dependencies from --from <local-registry>
                      into vendor/<name>/<version>, verify content, write lock
    vendor            copy registry dependencies from --from <local-registry>
                      into vendor/<name>/<version>, verify content, write lock
    doc               generate deterministic package docs into --out-dir
    bench [entry]     time the resolve + type-check pipeline without running
                      user code (no entry = package mode)
    compiler observe [entry]
                      write canonical observations through generated Rust source
                      to --out-dir (no entry = package mode)
    compiler preview [entry]
                      run the linked self compiler and
                      write a typed-terminal observation to --out-dir;
                      add --producer stage1|stage2 --terminal rust-source for
                      an explicit compiler producer; Stage 2 also accepts
                      --self-source to compile the embedded compiler source set
    compiler validate <dir>
                      validate an observation bundle without recompiling
    compiler compare <left> <right>
                      compare two validated observations (semantic by default);
                      use --layer generated-source|provenance, or compare two
                      binary files with --layer native-binary
    compiler status   report the installed Topaz compiler and reference compiler
                      support (`--json` emits topaz.compiler-supp

$ topaz run first-program.tpz --compiler self --exports-json · Зафиксировано с Топазом 5.21.3

Ожидаемый результат

Этап отклонения command. Ненулевой код завершения.

--exports-json requires check →
exports-json-requires-check

Нет стандартного вывода.

Наблюдаемые утверждения · Пройдено · 5.21.3

2026-11-06T04:37:26.3388970Z · command-validation · sha256:b6c3f574b78c558b526196fa04f5d835c9fe1df59d07397dbf4e5d279a3e1665

Код завершения 1.

Нет стандартного вывода.

Фрагмент наблюдаемого вывода ошибок

topaz: `--compiler self` accepts `--exports-json` only on `check`
topaz — Topaz toolchain developer driver (run `topaz --version`)
USAGE:
topaz <COMMAND> [ARGS]
COMMANDS:
parse <file> parse a Topaz source file and report diagnostics
dump-ast <file> parse a Topaz source file and print the AST
check [entry] parse + resolve + type a selected compilation unit
(no entry = package mode from topaz.toml)
run [entry] execute a checked program (no entry = package mode)
test [entry] run a checked selected unit on the deterministic TestHost
(--root <package> keeps its manifest, lock, and dependencies
for a selected entry; no entry uses the manifest entry)
fmt [entry] parse-gated deterministic whitespace formatting
(`--check` reports drift without writing;
no entry = package mode; skips vendor/target)
lsp run the deterministic stdio language server; package
diagnostics use initialize.rootUri (or --root) with a
valid locked package and open-document overlays
emit [entry] expose generated Rust source for inspection/integration
(`--target rust`); print the primary source to stdout,
or write the complete source set with --out-dir <dir>
(--root <dir>; no entry = package mode)
build [entry] lower + scaffold (--out-dir <dir>, required) + drive
cargo to build a native binary at
<dir>/target/<profile>/program (final binary only), or with
--target web a wasm package at <dir>/topaz-web.wasm
(--target web-worker also emits worker glue)
(--release for an optimized build; --run to execute
native builds after building; no entry = package mode)
init scaffold a deterministic current-profile native package
at --root (default `.`); refuses to overwrite existing
files
add <dep> add a dependency to topaz.toml (`name@version`, or
`name --path <relative-path>` with content hash)
lock write deterministic topaz.lock for the package at
--root (default `.`); local/path dependency hashes must
already match topaz.toml
fetch fetch registry dependencies from --from <local-registry>
into vendor/<name>/<version>, verify content, write lock
vendor copy registry dependencies from --from <local-registry>
into vendor/<name>/<version>, verify content, write lock
doc generate deterministic package docs into --out-dir
bench [entry] time the resolve + type-check pipeline without running
user code (no entry = package mode)
compiler observe [entry]
write canonical observations through generated Rust source
to --out-dir (no entry = package mode)
compiler preview [entry]
run the linked self compiler and
write a typed-terminal observation to --out-dir;
add --producer stage1|stage2 --terminal rust-source for
an explicit compiler producer; Stage 2 also accepts
--self-source to compile the embedded compiler source set
compiler validate <dir>
validate an observation bundle without recompiling
compiler compare <left> <right>
compare two validated observations (semantic by default);
use --layer generated-source|provenance, or compare two
binary files with --layer native-binary
compiler status report the installed Topaz compiler and reference compiler
support (`--json` emits topaz.compiler-supp

Пройдено · expected nonzero; observed 1
Пройдено · stdout matches the authored expectation
Пройдено · command validation; cause exports-json-requires-check; no source location applies

Reject --json on check

Ссылка

reject · command-validation · Проверка · Пройдено

first-program.tpzReject --json on checkОткрыть песочницу →

import std.io
function greet(name: string) -> string {
return "Hello, {name}!"
}
io.writeLine(greet("Topaz"))

Фрагмент зафиксированного выводаКод завершения 1

Нет стандартного вывода.

topaz: `--json` applies to `compiler status`, `explain`, and `bench` only; use `topaz lispex embed info --json` for the embedded evaluator

topaz — Topaz toolchain developer driver (run `topaz --version`)

USAGE:
    topaz <COMMAND> [ARGS]

COMMANDS:
    parse <file>      parse a Topaz source file and report diagnostics
    dump-ast <file>   parse a Topaz source file and print the AST
    check [entry]     parse + resolve + type a selected compilation unit
                      (no entry = package mode from topaz.toml)
    run [entry]       execute a checked program (no entry = package mode)
    test [entry]      run a checked selected unit on the deterministic TestHost
                      (--root <package> keeps its manifest, lock, and dependencies
                      for a selected entry; no entry uses the manifest entry)
    fmt [entry]       parse-gated deterministic whitespace formatting
                      (`--check` reports drift without writing;
                      no entry = package mode; skips vendor/target)
    lsp               run the deterministic stdio language server; package
                      diagnostics use initialize.rootUri (or --root) with a
                      valid locked package and open-document overlays
    emit [entry]      expose generated Rust source for inspection/integration
                      (`--target rust`); print the primary source to stdout,
                      or write the complete source set with --out-dir <dir>
                      (--root <dir>; no entry = package mode)
    build [entry]     lower + scaffold (--out-dir <dir>, required) + drive
                      cargo to build a native binary at
                      <dir>/target/<profile>/program (final binary only), or with
                      --target web a wasm package at <dir>/topaz-web.wasm
                      (--target web-worker also emits worker glue)
                      (--release for an optimized build; --run to execute
                      native builds after building; no entry = package mode)
    init              scaffold a deterministic current-profile native package
                      at --root (default `.`); refuses to overwrite existing
                      files
    add <dep>         add a dependency to topaz.toml (`name@version`, or
                      `name --path <relative-path>` with content hash)
    lock              write deterministic topaz.lock for the package at
                      --root (default `.`); local/path dependency hashes must
                      already match topaz.toml
    fetch             fetch registry dependencies from --from <local-registry>
                      into vendor/<name>/<version>, verify content, write lock
    vendor            copy registry dependencies from --from <local-registry>
                      into vendor/<name>/<version>, verify content, write lock
    doc               generate deterministic package docs into --out-dir
    bench [entry]     time the resolve + type-check pipeline without running
                      user code (no entry = package mode)
    compiler observe [entry]
                      write canonical observations through generated Rust source
                      to --out-dir (no entry = package mode)
    compiler preview [entry]
                      run the linked self compiler and
                      write a typed-terminal observation to --out-dir;
                      add --producer stage1|stage2 --terminal rust-source for
                      an explicit compiler producer; Stage 2 also accepts
                      --self-source to compile the embedded compiler source set
    compiler validate <dir>
                      validate an observation bundle without recompiling
    compiler compare <left> <right>
                      compare two validated observations (semantic by default);
                      use --layer generated-source|provenance, or compare two
                      binary files with --layer native-binary
    compiler status   report the installed Topaz compiler and reference c

$ topaz check first-program.tpz --compiler self --json · Зафиксировано с Топазом 5.21.3

Ожидаемый результат

Этап отклонения command. Ненулевой код завершения.

--json is not the check diagnostic format →
json-is-not-check-format

Нет стандартного вывода.

Наблюдаемые утверждения · Пройдено · 5.21.3

2026-11-06T04:37:26.3470127Z · command-validation · sha256:b6c3f574b78c558b526196fa04f5d835c9fe1df59d07397dbf4e5d279a3e1665

Код завершения 1.

Нет стандартного вывода.

Фрагмент наблюдаемого вывода ошибок

topaz: `--json` applies to `compiler status`, `explain`, and `bench` only; use `topaz lispex embed info --json` for the embedded evaluator
topaz — Topaz toolchain developer driver (run `topaz --version`)
USAGE:
topaz <COMMAND> [ARGS]
COMMANDS:
parse <file> parse a Topaz source file and report diagnostics
dump-ast <file> parse a Topaz source file and print the AST
check [entry] parse + resolve + type a selected compilation unit
(no entry = package mode from topaz.toml)
run [entry] execute a checked program (no entry = package mode)
test [entry] run a checked selected unit on the deterministic TestHost
(--root <package> keeps its manifest, lock, and dependencies
for a selected entry; no entry uses the manifest entry)
fmt [entry] parse-gated deterministic whitespace formatting
(`--check` reports drift without writing;
no entry = package mode; skips vendor/target)
lsp run the deterministic stdio language server; package
diagnostics use initialize.rootUri (or --root) with a
valid locked package and open-document overlays
emit [entry] expose generated Rust source for inspection/integration
(`--target rust`); print the primary source to stdout,
or write the complete source set with --out-dir <dir>
(--root <dir>; no entry = package mode)
build [entry] lower + scaffold (--out-dir <dir>, required) + drive
cargo to build a native binary at
<dir>/target/<profile>/program (final binary only), or with
--target web a wasm package at <dir>/topaz-web.wasm
(--target web-worker also emits worker glue)
(--release for an optimized build; --run to execute
native builds after building; no entry = package mode)
init scaffold a deterministic current-profile native package
at --root (default `.`); refuses to overwrite existing
files
add <dep> add a dependency to topaz.toml (`name@version`, or
`name --path <relative-path>` with content hash)
lock write deterministic topaz.lock for the package at
--root (default `.`); local/path dependency hashes must
already match topaz.toml
fetch fetch registry dependencies from --from <local-registry>
into vendor/<name>/<version>, verify content, write lock
vendor copy registry dependencies from --from <local-registry>
into vendor/<name>/<version>, verify content, write lock
doc generate deterministic package docs into --out-dir
bench [entry] time the resolve + type-check pipeline without running
user code (no entry = package mode)
compiler observe [entry]
write canonical observations through generated Rust source
to --out-dir (no entry = package mode)
compiler preview [entry]
run the linked self compiler and
write a typed-terminal observation to --out-dir;
add --producer stage1|stage2 --terminal rust-source for
an explicit compiler producer; Stage 2 also accepts
--self-source to compile the embedded compiler source set
compiler validate <dir>
validate an observation bundle without recompiling
compiler compare <left> <right>
compare two validated observations (semantic by default);
use --layer generated-source|provenance, or compare two
binary files with --layer native-binary
compiler status report the installed Topaz compiler and reference c

Пройдено · expected nonzero; observed 1
Пройдено · stdout matches the authored expectation
Пройдено · command validation; cause json-is-not-check-format; no source location applies

Keep the check diagnostic format

Ссылка

check · command-validation · Проверка · Не выполнялось

main.tpzKeep the check diagnostic formatОткрыть песочницу →

let value = 1

Ожидаемый выводКод завершения 0

Нет стандартного вывода.

$ topaz check main.tpz --language-version 5.21 --format json · Целевой продукт 5.21.3

Ожидаемый результат

Проверка принимает программу. Код завершения 0.

Нет вывода ошибок.

Нет стандартного вывода.

Этот пример ещё не выполнялся.

An integer is not implicitly a float

Ссылка

reject · checking · Проверка · Пройдено

example.tpzAn integer is not implicitly a floatОткрыть песочницу →

let value: float = 1

Зафиксированный выводКод завершения 1

Нет стандартного вывода.

error[TPZ5001]: expected `float`, found `int`
 --> example.tpz:1:20
  |
1 | let value: float = 1
  |                    ^

example.tpz: 1 type diagnostic

$ topaz check example.tpz --compiler self · Зафиксировано с Топазом 5.21.3

Ожидаемый результат

Этап отклонения check. Ненулевой код завершения.

TPZ5001 →
types-int-not-float at example.tpz:1:20

Нет стандартного вывода.

Наблюдаемые утверждения · Пройдено · 5.21.3

2026-11-06T13:59:21.1995114Z · checking · sha256:b6c3f574b78c558b526196fa04f5d835c9fe1df59d07397dbf4e5d279a3e1665

Код завершения 1.

Нет стандартного вывода.

Наблюдаемый вывод ошибок

error[TPZ5001]: expected `float`, found `int`
--> example.tpz:1:20
|
1 | let value: float = 1
| ^
example.tpz: 1 type diagnostic

Пройдено · expected nonzero; observed 1
Пройдено · stdout matches the authored expectation
Пройдено · checking TPZ5001; cause types-int-not-float; primary location asserted; additional diagnostics allow
Пройдено · checking TPZ5001; cause types-int-not-float; primary location asserted; additional diagnostics allow

Small source invocation

Ссылка

check · checking · Проверка · Не выполнялось

main.tpzSmall source invocationОткрыть песочницу →

function identity<T>(value: T) -> T {
value
}

Ожидаемый выводКод завершения 0

$ topaz check main.tpz --language-version 5.21 · Целевой продукт 5.21.3

Ожидаемый результат

Проверка принимает программу. Код завершения 0.

Этот пример ещё не выполнялся.

Reuse the complete generic declaration accepted by the pilot. A successful fixture does not settle generic-call or inference contracts.

Verification

Ссылка

--exports-json requires check

Семейство: topaz-cli
Этап: command
Операция: option-validation
Категория: exports-json-requires-check

Причина и условия

--exports-json applies to check. Using it with run is rejected during command validation before the program executes.

Связанное правило · Scope of --exports-json →

Действия

Use topaz check with --exports-json.

--json is not the check diagnostic format

Семейство: topaz-cli
Этап: command
Операция: option-validation
Категория: json-is-not-check-format

Причина и условия

Use --format json for check diagnostics. check --json is rejected; it is not an alias for --format json.

Связанное правило · Diagnostic JSON option →

Действия

Use --format json for check diagnostics and --exports-json for checked exports.

Functions and generics →

TPZ5523: Duplicate protocol bound →

std.io.writeLine →

Synopsis and input

topaz check

Ввод

Параметры и конфликты

Каналы вывода

Статус завершения

Эффекты

Operation

Checking a compilation unit

Причина

Options and conflicts

Scope of --exports-json

Причина

Diagnostic JSON option

Причина

Results and output channels

Checked export output

Причина

Diagnostic and success channels

Причина

Examples

Check the first program

Ожидаемый результат

Check and emit export JSON

Ожидаемый результат

Reject --exports-json on run

Ожидаемый результат

Reject --json on check

Ожидаемый результат

Keep the check diagnostic format

Ожидаемый результат

An integer is not implicitly a float

Ожидаемый результат

Small source invocation

Ожидаемый результат

Verification

Related entries

--exports-json requires check

Причина и условия

Действия

--json is not the check diagnostic format

Причина и условия

Действия

`topaz check`