Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Getting started

Executed by the tutorial harness. Every tagged command on this page runs on every pull request.

Executed. Every fenced command on this page is run by CI — the docs-tutorial step of the docs workflow (docs-lint L5) — in document order, in one shell session, on the host. A command that stops working turns the build red, so this page cannot describe a CLI that does not exist. Three kinds of block are not ordinary steps and say so in their fence: exec:expect-fail (the honest answer today is an error), exec:hardware (needs a real device; the harness reports it as skipped and never runs it in a pull request) and untagged fences, which are prose.

In about five minutes you build the one command surface of the platform, read a contract out of the contract store, read the target contract, produce a deployment plan without touching a device, and hear the two stages that are not wired yet say so. Nothing here cross-compiles and nothing here talks to hardware.

Before you start

A clone of this repository, git, and the Rust toolchain it pins. The pin is an exact compiler version, never stable, and it lives in a rust-toolchain.toml at the root of the clone; rustup reads that file, so rustup toolchain install in the clone gets you the exact compiler CI uses. Python 3.11+ if you also want to run the lints. No cross-compiler, no device, no credentials.

1. Build the CLI

CI sets REPO_ROOT to the checkout; on your machine it is your clone (export REPO_ROOT="$(pwd)" from the repository root). Everything below uses the binary this step builds.

cd "$REPO_ROOT"
cargo build -p labinetix
export PATH="$PWD/target/debug:$PATH"

labinetix is one crate in a workspace of many. Building the whole workspace needs two ordered pre-steps first (the C++ static archives, then libLxPlant.so) and the pinned zig; that is what just check and the ci workflow do, and this page deliberately does not.

2. The six stages

labinetix --help

Define, analyze, build, ship, run and observe models on embedded control hardware

Usage: labinetix <COMMAND>

Commands:
  define   Author, verify and release contracts in the CADB (`crates/studio/define-cli`)
  analyze  Predict on the host what `run` will do — goldens, simulation, the compliance check
  build    Turn the target contract into the inputs a cross build needs (`crates/studio/build-toolchains`)
  ship     Stage, activate and roll back artifacts on a target (`crates/studio/ship-deploy`)
  run      Execute a model on the target engine
  observe  Record what real hardware did — on-target runs, evidence with provenance (`crates/studio/observe-cli`)

Options:
  -h, --help     Print help
  -V, --version  Print version

The root is exactly the six stages of the spine, in spine order, and nothing else. Later work adds leaves under a stage; the six roots do not move. Four of them — define, build, ship and observe — call the studio crate that owns the stage as an ordinary in-process library call. Two of them, analyze and run, have their place in the tree and no library behind them yet; §5 and §7 show exactly what they do about that today.

3. define — the contract store

The contract store (the CADB) is the capabilities/ directory: one directory per capability, each with its authoring file, its generated views and a lockfile that pins every one of them by content hash. Every define leaf takes --repo-root, which defaults to the working directory, so from the repository root you point it at the store.

labinetix define list --repo-root capabilities

One tab-separated row per entity: type, id, contract version, ipo_id (- where the type has none), content hash, lockfile path. Tab-separated because the output is for a script as much as for you.

One entity in full:

labinetix define show interface/tutorial_adder --repo-root capabilities

The authoring file and every generated view — the C header, the Rust view, the validator — each pinned by its own hash. Nothing under a generated/ directory is ever hand-edited; the emitter writes it and the lockfile pins it.

That claim is checkable, and checking it is a leaf:

labinetix define verify --all --repo-root capabilities

verify recomputes every hash and compares it against the lockfiles. It writes nothing, prints nothing and exits zero: silence is the pass. A view edited by hand fails here, which is the whole point of the stage.

4. build — the target contract

build turns hardware/targets/*.toml into the inputs a cross build needs. It compiles nothing itself.

labinetix build target

validated 3 target(s): cepe, cpxe, host-linux

Called with no name it validates the whole contract and lists it. Called with one name it prints that entry — here the host, which is the only one this page uses:

labinetix build target host-linux

The CI level and the rest come from hardware/targets/host-linux.toml and from nowhere else: a build fact that is not in the contract does not exist. The triple is the one thing that file does not write down — host-linux names the machine in front of you, so its triple is resolved from the toolchain that is running, and the line above will say x86_64 or aarch64 depending on where you ran it. The two embedded entries in that list, cepe and cpxe, need the pinned zig and a CMake toolchain file, which is labinetix build cmake-toolchain and is out of scope here.

5. analyze — not wired yet

analyze is the host-side prediction stage: goldens, simulation, the compliance check. The subcommand exists and the crate that will back it exists, but that crate has no library target to call, so the stage refuses instead of pretending:

labinetix analyze

It exits non-zero and prints one line naming what will back it. That is deliberate: a stage with a place in the tree and nothing behind it is recorded, not stubbed.

6. ship — a deployment plan without a device

ship plan resolves a deployment offline. It opens no socket, so you can run it here:

labinetix ship plan \
  --manifest crates/studio/ship-deploy/tests/fixtures/manifests/valid-pair.json \
  --artifact-dir crates/studio/ship-deploy/tests/fixtures/artifacts \
  --site-profile crates/studio/ship-deploy/tests/fixtures/profiles/sites/example.site.toml \
  --platform-profile crates/studio/ship-deploy/profiles/platforms/cpxe.toml

The manifest, the artifacts and the site profile are the synthetic fixtures the ship tests use, so the plan is real and the plant is not. Read the output for two things: the compatible set — libExternalIPO.so and libLxPlant.so, the pair that is the product’s artifact, each with its hash and its deploy path — and the redaction. The address and the username come back as <redacted-addr:…> and <redacted-user:…>, which is why a plan is safe to paste into an issue.

Staging and activating that plan is the same command surface against a real target, and it is never run by a pull request:

labinetix ship stage --transport cpxe \
  --manifest "$MANIFEST" --artifact-dir "$ARTIFACTS" \
  --site-profile "$SITE_PROFILE" --platform-profile "$PLATFORM_PROFILE"
labinetix ship activate --transport cpxe --confirm-reboot \
  --manifest "$MANIFEST" --artifact-dir "$ARTIFACTS" \
  --site-profile "$SITE_PROFILE" --platform-profile "$PLATFORM_PROFILE"

Activation reboots the target, which is why it demands --confirm-reboot; labinetix ship rollback restores the pair that was there before. The address and the username live in the site profile, never on the command line, and the password never anywhere either — ship reads it from the environment or from a credential agent.

7. run — not wired yet

run is the device stage: the engine executing a model on the target. Like analyze, it has its root and no library behind it today:

labinetix run

8. observe — what the hardware actually did

observe records. It is the only stage whose output carries authority about a real target, and it needs the lab:

labinetix observe --help

One leaf, run: scenario → deploy → remote → compare → evidence. Against a real CPX-E it is a long command because every input is pinned explicitly — the scenario and the lockfile from the store, both manifests, both artifact directories, the exact SHA-256 of the test executable, and where the evidence goes:

labinetix observe run \
  --scenario-json "$SCENARIO_JSON" \
  --lock-json "$LOCK_JSON" \
  --lx-core-root "$LX_CORE_ROOT" \
  --plant-manifest "$PLANT_MANIFEST" \
  --plant-artifact-dir "$PLANT_ARTIFACTS" \
  --executable-manifest "$EXECUTABLE_MANIFEST" \
  --executable-artifact-dir "$EXECUTABLE_ARTIFACTS" \
  --executable-sha256 "$EXECUTABLE_SHA256" \
  --site-profile "$SITE_PROFILE" \
  --output-dir "$OUTPUT_DIR" \
  --transport cpxe --confirm-real-remote --confirm-plant --confirm-place

CI reports that block as skipped and moves on. That asymmetry is the design: analyze predicts on the host on every pull request, observe records on real hardware and produces the evidence a release is not a release without.

Where to go next

  • The CLI reference on this site lists every command, subcommand and option of the surface this page walked through. It is walked off the command tree by the CLI itself and byte-compared against that tree on every pull request, so it cannot describe a flag that does not exist.
  • just check runs, in workflow order, exactly what the two CI workflows run, and just build the three ordered build steps alone. Each check is its own recipe under the name CI reports it by — boundary-lint, cargo-fmt, cargo-clippy, cargo-build, cargo-test, kernels-no-std, generated-check, docs-tutorial and the rest — so a check that went red is a recipe you can run by that name.
  • The layers, the six stages, the machine checks that hold them and the working rules a change has to satisfy are documented with the source, in the clone you started from, rather than on this site.