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.

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.

종료 상태

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. 종료 코드가 0이 아닙니다.

--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. 종료 코드가 0이 아닙니다.

--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. 종료 코드가 0이 아닙니다.

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`