tape check

Usage

bash
tape check <file.tape>

Purpose

Runs the frontend pipeline through type checking without generating code. Useful for fast feedback in editors and CI.

bash
tape check app.tape
# OK

tape check broken.tape
# broken.tape:12:5: error: 'n' is i64, given string |     let n: i64 = "five";

What it does

  1. Split source into regions
  2. Parse #code (with the rt0 preamble if there are no imports, as tape build does) and #view, merging components
  3. Parse the #test region, if there is one, and merge its tests, helper functions, constants and fixtures into the module, as tape test does
  4. Without imports: execute @tape blocks (compile-time metaprogramming), then type check and lower
  5. With imports: resolve and check every imported module the way tape build does, so imported names and qualified types resolve identically

Prints OK on success. Errors go to stderr.

The module and its tests are compiled together, once: an error in test code is reported by tape check, not only when tape test runs, and an error in the module is reported once. The tests are compiled, not run.

Options

FlagDescription
--humanHuman-readable errors with color and source context
--max-errors <N>Stop after N errors
-I <path>Add module search path (then ./stdlib, then stdlib/ next to the tape binary)
--tape-fuel <n>The compile-time budget of each @tape block, as for tape build
--set NAME=VALUECheck with a build setting’s value, as for tape build; without it each setting is its default
--purityDon’t check: print whether the module is pure (it reaches nothing outside the memory it is given: it imports only pure modules and calls only the runtime’s memory functions) or capability: <why>, naming the import, runtime call or extern fn that gives it access to the outside world. Exit code 0 either way

Diagnostics

A syntax error is reported once, where it is: a missing ; at the end of the statement that lacks it, an unterminated string at its opening quote, an unknown escape at its backslash. Nothing after the first syntax error is reported, since the parser does not resynchronize and every later complaint would follow from the first. Type errors are independent of each other and are all reported.

A message says what is wrong and what to write instead, and nothing else: 'print' is not defined, 'io.println' takes 1 argument, given 2, module 'io' has no 'prinln', '{' is never closed: expected '}' before the end of the file (at the {), 'name' is a let: it can't change, 'count' is i64, given string. A string missing its closing quote runs on to the next line, and the error lands there; --human names the string it came from. A suggestion that goes beyond that, such as the nearest name that exists, is a hint: --human prints it under the source line (= did you mean 'println'?), and editors show it with the message. The default output, made for tools, prints the message alone.

Exit codes

CodeMeaning
0No errors
1Parse errors, comptime errors, or type errors found

Speed

tape check lowers the code (the lowering reports errors too, as in tape run and tape build) and throws the result away. It skips:

  • Link checking
  • Native codegen
  • Binary emission

It’s the recommended command for editor integrations and pre-commit hooks.

Last modified: