Commands, build, tests

Commands

bin/sysi runs racket sysi/main.rkt with its arguments. The commands, as sysi/main.rkt lists them in its first lines:

Every command that takes .sysp files runs sysp's checker on them first, with verification, and stops if the program does not check (lower-files). check is the exception: it reads .sysi text and runs only the well-formedness check; and difftest lowers without verifying (it checks every assumption the program's proof would justify as it runs, so run sysp check first if a false one could be the program's). refine, validate, check and difftest print each problem, then a summary line that starts with ok when there is none; they exit 0 only then. Flags may come before or after the files, as with sysp: flags-first moves them to the front.

Options

Read from parse-options in sysi/main.rkt, with the help text each carries. The help text names one command for some options; the last column says which commands the code actually reads each one in.

Try a command line

Pick a command, then options: those the command does not read are greyed out.

The Makefile

Each target with the comment above it in the Makefile. SYSK (default ../sysk) chooses the sysk checkout the sysk targets use, RACO the raco to run.

The sysk targets are explained on Every build checked.

Test suites

make test compiles and runs every file in tests/ (raco test tests): 11 test cases written out by name, and in tests/validate-test.rkt two more for each of the two programs it builds (features, and bench: the 15 benchmark tasks with bench-driver.sysp): "NAME: accepted" and "NAME: the stack build is not the register build", made in a loop and so not in the lists below. Each file's header, and its named test cases:

Requirements

The docs suite

These pages are written by hand, but what can be read off the code is generated by tools/docs.rkt. Its usage, from the file:

• data writes data.js: each source file's header, its definitions with their comments, its text, the instruction set, the commands, the test cases, line counts and the reference. data --check exits 1 if data.js is stale.
• run writes run.js: real runs of sysi on docs/site/examples/sum.sysp (sysp's check, the lowering, the assembly, the C, refine, and validate on an executable linked with tests/programs/rt.S), one lowering mutant of sum and what refine says of it, the example's run on sysp's meaning region by region and sysi difftest on it with the driver it wrote (for the checker, tested), and the last line of each check from build/sysk-gate/ if a gate has run here.
• status fails if a source file is explained by no page, or if something a page's files define (a definition's first line and comment, a script's header, a make target, a test case) changed since the page was last reviewed.
• review PAGE.html ... records what each page was read against in docs/site/reviewed.rktd.

make docs runs data, run and status (a failing status does not fail the target); make docs-status runs data --check and status. tests/docs-test.rkt runs the same two, so make test fails when data.js is stale or a page needs rereading. run needs clang and ld.lld (or CLANG and LLD) for the validate run, and prints "(no clang/ld.lld: not run)" in its place without them.

Environment variables

What the code reads with getenv, and what each does there. The SYSI_ variables are for working on the checks; none changes a verdict except SYSI_INCR, which changes how queries are put to z3.