Proven, then run
A proof says a function keeps its contract; it does not say the contract is the encoding the parts meant. So sysl is checked twice: every obligation proven by sysp, then the library built to C and run on the host, each answer compared with Racket's own encoding of the same bytes.
The targets
| Target | What it does |
|---|---|
make | proves every obligation of lib/, host/ and tests/callers.sysp, with proofs from the store every checkout shares (../tools/store proofs); then checks every file is in sysp's canonical format |
make test | the proofs, then the tests: the library on the host, and the docs current; a test file whose inputs are as they were when it last passed is not run again (../tools/tested.rkt, sysx 101) |
make docs-check | the docs test alone: what tools/wt land runs instead of make test when only docs/, specs/ or .md files changed since the code last passed (sysx 029) |
make docs | whether every page is current; after rereading a page, racket tools/docs.rkt review PAGE.html |
make clean | the build and compiled Racket, gone |
The Makefile says USES := sysp: the only part sysl's build and tests read besides itself, so tools/wt land runs them again only when sysl or sysp changed.
On the host
sysp's host harness (../sysp/tools/host.rkt, sysp 051), which sysc, sysf and sysn use too, builds host/host.sysp and the library to C with sysp, every obligation proven, and compiles it with a shim of a few lines that only moves records between standard input and output and host-step. tools/host.rkt says only what is sysl's: its sources, the library and the host, with sysp's tools/harness.sysp, which says a record's header once for every part (sysp 073). The shim's sizes, a record of at most 4,101 bytes in and an answer of 300 out, are host/host.sysp's rec-max and out-size, which the harness reads from there (sysl 004, 015). A record is a kind byte, a 32-bit little-endian length, then that many bytes; host/host.sysp reads one and answers one.
| Record | Asks | The test compares with |
|---|---|---|
r at, buffer | every read at at: le32, le64, be16, be32, be48 | integer-bytes->integer, each byte order and width |
w at, value | every write of the value at at, each into a buffer of zeros | the value's bytes placed at at, zeros around them: a write touches only its own bytes |
z at, n, buffer | whether [at, at + n) is all zero | every byte of the range looked at |
c at, m, bytes | the bytes copied at at into m bytes of 0xee | the copy made in Racket |
e from, to, buffer | the buffer with [from, to) zeroed | the zeroing done in Racket |
b y u h s k, m, then what to write | one function of sysl/text writing from k into m bytes of 0xee (sysl 003); the answer is where the next byte goes, then the m bytes | number->string, hex and escaping done in Racket, the whole text cut where the buffer ends, a number whole or not at all, hex in whole bytes; 0xee left wherever nothing was to be written |
n at, e, max, then t | scan-dec of t[at, e) under max (sysl 012); the answer is the value plus one, 0 for none, as 8 bytes | Racket's own reading of the digits: -1 for an empty range, a byte not a digit, or more than max |
tests/scan-test.rkt reads every range of 4,000 short buffers, mostly digits, under maxima from 0 to 1017, with the edges written out (an empty range, a lone 0, leading zeros, a number at max and one past it), and 2,000 numbers as Racket writes them, read back under their own value and one below it.
tests/text-test.rkt writes from every offset into buffers of every size up to 40, with the edges written out: an empty buffer, an offset at its end, a number one digit too long, room for one hex byte and a half.
tests/bytes-test.rkt asks each at every offset from 0 to 8, with the edges written out (all zeros, all ones, counting bytes, a top bit set) and random bytes and values beside them, from a fixed seed so a failure comes back. The C is borrowed until sysi runs all of sysp (docs/borrowed.md); the shim, sysp's, is the only C written for it, and it knows only records.
The docs
Each page names the files it explains in its covers: this one the build, the host and the tests; Said once the library and its callers' contracts. tools/docs.rkt is the suite's bookkeeping (../tools/docs.rkt, sysx 020) given sysl's sources. status fails if a source is explained by no page, or if a definition, a test or a target a page covers changed since the page was last reviewed; tests/docs-test.rkt runs it, so make test fails on a stale page. info.rkt names the collection and its version.