Commands, build, tests

Commands

bin/sysi runs racket -y sysi/main.rkt with its arguments: -y compiles any module whose sources or dependencies changed, judged by hash, so a .zo another racket wrote is never run stale (specs/047). 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, each flag that takes a value with its value. Those flags are a list beside the declarations, and tests/cli-test.rkt reads the declarations and checks that each flag with a value is in it (specs/035: --clear-cases and --ext were not, so after a file --clear-cases took the next flag, sysk's -o, for its file).

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/, eight side by side, through the suite's tools/tested.rkt (sysx 101; specs/034), which skips a file whose reads all hash as when it last passed: 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 benchmark tasks written from a stub, 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. The Makefile's USES names what these tests read besides sysi, as paths (sysx 059): sysp's checker and benchmark, sysr's checker, ISS and ISA, sysk's libraries, and sysn's and sysf's programs with what they take from sysc and sysl. A landing reuses a pass while none of them changed, and only a change to one of them waits for sysi's gate (sysx's tools/wt; specs/019); within the gate, only the files that read what changed run again. tests/bench-test.rkt builds its programs in build/test/bench, so they count by their content; tests/parts-test.rkt and tests/secret-test.rkt ask make -n for sysn's, sysf's and sysc's sources, whose reads are not seen, and so run every time. The two mutant sweeps, in tests/refine-test.rkt and tests/validate-test.rkt, take nearly all of the time. Each runs its mutants in places side by side, each place taking every n-th, and a sweep that passed is kept in the suite's store (tools/store sysi-sweeps) by a hash of what it reads: the modules its test loads, followed through Racket's module graph (sysi's checks, backend and lowering; specs/031: not all of sysi, so a change to a tool or another test does not sweep again), of sysp only what its front end reads, as for refine's own results (specs/045, 048: the sweeps lower without sysp's verifier, which changes most often in sysp), what it loads or reads as it runs (sysr's checker, ISS and ISA, tests/programs), the tools' versions and MUTATE (tests/sweep.rkt). As a sweep runs, each place adds a line to build/refine-sweep.log or build/validate-sweep.log for every twentieth mutant it tries and when it is done, since the gate shows a test's output only when the test ends (specs/048). A gate that runs because sysk's libraries or sysn's code moved prints the kept result and sweeps nothing. 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.

Since specs/014 the bookkeeping (status, review, writing the two files) is the suite's, the root's tools/docs.rkt, which every part's calls; sysi's says which files are its sources, how each is read into items (a Racket module's definitions with their comments, a test file's cases, a make target, a section of the reference), and what data and run hold. Each page names its files in <meta name="covers">, and the suite's kit draws the "In the source" box at its end from them.

make docs runs data, run and status (a failing status does not fail the target); make docs-check 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; and when a branch changed only docs/, specs/ or Markdown since the tests last passed, tools/wt land runs make docs-check instead of make test. 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.