check | Topaz

Synopsis and input

`topaz check`

Synopsis

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

Input

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.

Options and conflicts

Option	Default	Contract	Conflicts
`--format human\|json`	human	Select human or JSON diagnostics for check. The shared format rule lists the commands that accept JSON output.	None listed
`--exports-json`	Not specified	On a clean checked unit, write its public export surface as one JSON object. Rejected on other commands.	`--profile`
`--profile available-profile`	Not specified	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.	None listed
`--language-version 5.21`	Not specified	Select the documented language mode.	None listed
`--root dir`	Not specified	Select the module/package root. For an explicit entry, the default root is its directory and the entry must be under the root.	None listed
`--locked`	Not specified	Require the package lock check in package mode.	None listed

Output channels

stdout

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

Related rule: 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

Exit status

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.

Effects

Additional contracts are Pending.

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

Operation

Link

Ruletopaz.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.

Why

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

Examples Check the first program

Source evidence

implementation source compiler/crates/topaz_cli/src/command/flags.rs at d61f9fd0efb0 · 23-112
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at d61f9fd0efb0 · 86-128

Options and conflicts

Link

Ruletopaz.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.

Why

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

Examples Reject --exports-json on run

Diagnostics --exports-json requires check

Source evidence

implementation source compiler/crates/topaz_cli/src/command/flags.rs at d61f9fd0efb0 · 114-174
implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

Ruletopaz.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.

Why

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

Examples Reject --json on check

Diagnostics --json is not the check diagnostic format

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

--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

Link

Ruletopaz.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.

Why

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

Examples Check and emit export JSON

Source evidence

implementation source compiler/crates/topaz_cli/src/compile/self_host.rs at d61f9fd0efb0 · 166-311

Ruletopaz.rule.check.channels

Diagnostic and success channels

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.

Why

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

Examples Keep the check diagnostic format An integer is not implicitly a float Small source invocation

Source evidence

implementation source compiler/crates/topaz_cli/src/compile/self_host.rs at d61f9fd0efb0 · 166-311

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

Link

Check the first program

Link

check · checking · Verification: passed

first-program.tpzCheck the first programOpen in Playground

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

Recorded outputexit 0

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

$ topaz check first-program.tpz --compiler self · recorded with topaz 5.21.3

Expected result

Checking accepts the program. Exit code 0.

Observed assertions · passed · 5.21.3

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

Exit code 0.

Observed stdout

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

No stderr.

Passed · expected 0; observed 0

Observed assertions · passed · 5.21.3

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

Exit code 0.

Observed stdout

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

No stderr.

Passed · expected 0; observed 0

Source evidence

document docs/npm/README.md at d61f9fd0efb0 · 48-79
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at d61f9fd0efb0 · 86-128
implementation source compiler/crates/topaz_resolve/src/std/521/io.tpz at d61f9fd0efb0 · 3-5

Check and emit export JSON

Link

check · checking · Verification: not-run

first-program.tpzCheck and emit export JSONOpen in Playground

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

Expected outputexit 0

$ topaz check first-program.tpz --compiler self --format json --exports-json · target product 5.21.3

Expected result

Checking accepts the program. Exit code 0.

No stderr.

Standard output is a JSON object. Its complete schema is not specified.

This exact example has not been executed.

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.

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150
implementation source compiler/crates/topaz_cli/src/compile/self_host.rs at d61f9fd0efb0 · 166-311
implementation source render_self_typed_export_surface_json at 570530e69141 · 320-638
implementation source render_semantic_type at 570530e69141 · 640-741
implementation source TypedPreviewResult::exported_value_node at 570530e69141 · 24-47
implementation source std.io exports at 570530e69141 · 3-5
implementation source standardBoundary at 570530e69141 · 1237-1247
implementation source builtinFunction at 570530e69141 · 285-294
implementation source buildTable at 570530e69141 · 315-349
test source resolver_entry_identity_strips_exactly_one_tpz_suffix at 570530e69141 · 694-724

Reject --exports-json on run

Link

reject · command-validation · Verification: passed

first-program.tpzReject --exports-json on runOpen in Playground

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

Recorded output excerptexit 1

No stdout.

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 · recorded with topaz 5.21.3

Expected result

Rejection during command. Nonzero exit.

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

No stdout.

Observed assertions · passed · 5.21.3

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

Exit code 1.

No stdout.

Observed stderr (excerpt)

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

Passed · expected nonzero; observed 1
Passed · stdout matches the authored expectation
Passed · command validation; cause exports-json-requires-check; no source location applies

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

Reject --json on check

Link

reject · command-validation · Verification: passed

first-program.tpzReject --json on checkOpen in Playground

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

Recorded output excerptexit 1

No stdout.

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 · recorded with topaz 5.21.3

Expected result

Rejection during command. Nonzero exit.

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

No stdout.

Observed assertions · passed · 5.21.3

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

Exit code 1.

No stdout.

Observed stderr (excerpt)

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

Passed · expected nonzero; observed 1
Passed · stdout matches the authored expectation
Passed · command validation; cause json-is-not-check-format; no source location applies

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

Keep the check diagnostic format

Link

check · command-validation · Verification: not-run

main.tpzKeep the check diagnostic formatOpen in Playground

let value = 1

Expected outputexit 0

No stdout.

$ topaz check main.tpz --language-version 5.21 --format json · target product 5.21.3

Expected result

Checking accepts the program. Exit code 0.

No stderr.

No stdout.

This exact example has not been executed.

Source evidence

implementation source compiler/crates/topaz_cli/src/command/flags.rs at 9b1bbdeceba9 · 650-718
implementation source compiler/crates/topaz_cli/src/command/validation.rs at 9b1bbdeceba9 · 112-148
implementation source compiler/crates/topaz_cli/src/compiler_support.rs at 9b1bbdeceba9 · 3-26
implementation source compiler/crates/topaz_cli/src/compiler_support.rs at 9b1bbdeceba9 · 392-453
implementation source compiler/crates/topaz_diag/src/explain.rs at 9b1bbdeceba9 · 69-102
implementation source compiler/crates/topaz_diag/src/explain.rs at 9b1bbdeceba9 · 518-525
implementation source compiler/crates/topaz_cli/src/commands/bench.rs at 9b1bbdeceba9 · 30-50
implementation source compiler/crates/topaz_cli/src/commands/bench.rs at 9b1bbdeceba9 · 98-120
implementation source compiler/crates/topaz_cli/src/lispex_embed.rs at 9b1bbdeceba9 · 33-77
implementation source compiler/crates/topaz_lispex_embed/src/report.rs at 9b1bbdeceba9 · 6-66
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at 9b1bbdeceba9 · 439-441
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at 9b1bbdeceba9 · 676-690

An integer is not implicitly a float

Link

reject · checking · Verification: passed

example.tpzAn integer is not implicitly a floatOpen in Playground

let value: float = 1

Recorded outputexit 1

No stdout.

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 · recorded with topaz 5.21.3

Expected result

Rejection during check. Nonzero exit.

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

No stdout.

Observed assertions · passed · 5.21.3

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

Exit code 1.

No stdout.

Observed stderr

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

Passed · expected nonzero; observed 1
Passed · stdout matches the authored expectation
Passed · checking TPZ5001; cause types-int-not-float; primary location asserted; additional diagnostics allow
Passed · checking TPZ5001; cause types-int-not-float; primary location asserted; additional diagnostics allow

Source evidence

implementation source assignable at af88afbc1d99 · 358-376
implementation source widen at af88afbc1d99 · 543-554
implementation source typeEqual at af88afbc1d99 · 246-259
implementation source assignable at af88afbc1d99 · 358-416
implementation source formLiteralType at af88afbc1d99 · 251-272
implementation source checkExpressionExpectedResult at af88afbc1d99 · 1716-1748
implementation source reportExpectedType at af88afbc1d99 · 1660-1684
implementation source bindingAnnotationType / inferBindingValue at af88afbc1d99 · 100-193
implementation source checkBindingStatement at af88afbc1d99 · 422-475
implementation source widen at af88afbc1d99 · 543-554

Small source invocation

Link

check · checking · Verification: not-run

main.tpzSmall source invocationOpen in Playground

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

Expected outputexit 0

$ topaz check main.tpz --language-version 5.21 · target product 5.21.3

Expected result

Checking accepts the program. Exit code 0.

This exact example has not been executed.

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

Source evidence

implementation source compiler/crates/topaz_cli/src/command/flags.rs at b48527d0a174
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at b48527d0a174
implementation source compiler/crates/topaz_cli/src/command/validation.rs at b48527d0a174
implementation source compiler/crates/topaz_cli/src/compiler_support.rs at b48527d0a174
implementation source docs/content-next/en/functions-generics.json at b48527d0a174

Verification

Link

Pending · Installed check profile support

Which public distributions include the required assets and verified execution support for each recognized check profile? The diagnostic, profile summary, checked export, root, and lock contracts are specified. Current source recognizes agent-pack, test-profile, and bootstrap. Release-specific execution evidence is still needed to establish which profiles are usable in each public distribution and what required profile assets are included. Next run the installed profile matrix for each distribution and record its product identities and outcomes.

Source evidence

implementation source compiler/crates/topaz_cli/src/command/flags.rs at d61f9fd0efb0 · 23-112
implementation source compiler/crates/topaz_cli/src/command/flags.rs at d61f9fd0efb0 · 114-174
implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150
implementation source compiler/crates/topaz_cli/src/command/dispatch.rs at d61f9fd0efb0 · 86-128
implementation source compiler/crates/topaz_cli/src/compile/self_host.rs at d61f9fd0efb0 · 166-311
implementation source check package and file dispatch at 151141d7bb44 · 86-128
implementation source CheckProfile.parse at 151141d7bb44 · 11-34
implementation source check profile and export validation at 151141d7bb44 · 110-139
implementation source topaz.profile-check/v1 at 151141d7bb44 · 245-255
implementation source render_self_typed_export_surface_json at 151141d7bb44 · 320-356
implementation source topaz.profile-diagnostic/v1 at 151141d7bb44 · 106-142

Link

--exports-json requires check

Family: topaz-cli
Phase: command
Operation: option-validation
Category: exports-json-requires-check

Cause and conditions

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

Related rule: Scope of --exports-json

Response

Use topaz check with --exports-json.

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

--json is not the check diagnostic format

Family: topaz-cli
Phase: command
Operation: option-validation
Category: json-is-not-check-format

Cause and conditions

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

Related rule: Diagnostic JSON option

Response

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

Source evidence

implementation source compiler/crates/topaz_cli/src/command/validation.rs at d61f9fd0efb0 · 110-150

Functions and generics

TPZ5523: Duplicate protocol bound

std.io.writeLine

Synopsis and input

topaz check

Input

Options and conflicts

Output channels

Exit status

Effects

Operation

Checking a compilation unit

Why

Options and conflicts

Scope of --exports-json

Why

Diagnostic JSON option

Why

Results and output channels

Checked export output

Why

Diagnostic and success channels

Why

Examples

Check the first program

Expected result

Check and emit export JSON

Expected result

Reject --exports-json on run

Expected result

Reject --json on check

Expected result

Keep the check diagnostic format

Expected result

An integer is not implicitly a float

Expected result

Small source invocation

Expected result

Verification

Related entries

--exports-json requires check

Cause and conditions

Response

--json is not the check diagnostic format

Cause and conditions

Response

`topaz check`