The cairn tool · Cairn docs

Building it

cairn is its own Swift package in Cairn's tools/cairn, with no dependencies:

cd tools/cairn && swift build -c release   # .build/release/cairn
cd tools/cairn && swift test

docs/cli.md, lines 12–13

Commands

Command	What it does
`cairn new <name> [--lib\|--bin]`	starts a package in a new directory: `cairn.toml` with its `kind`, an empty `claims.lock`, and `lean/` with a lakefile that sets the claim scope to `<name>` and requires Cairn. Its Lean module does `public import Cairn`. An app (`--bin`) is a working one: a window with a count and a Count button (place `^1`, move `^2`), its exports in `lean/<Module>/Abi.lean`, `Package.swift`, a C target declaring its initializer, and a host with `--selftest`; a library (`--lib`) gets none of the Swift. With neither flag it asks which.
`cairn add [<owner>/]<name>[@<range>]`	adds a dependency from the registry to `cairn.toml` and the lakefile, replacing a `require … from git` of it. It prints the `Package.swift` line rather than editing Swift. With no range it uses `^` and the latest release, and with no owner it looks up the name's owner. It needs no login.
`cairn build [--release]`	`lake cache get` (prebuilt Lean from the registry, when it has it), `lake build`, Cairn's `cairn-link` to merge the Lean into one static library in `.cairn/lib/`, then `swift build`.
`cairn doc [--private] [--open]`	the package's API docs, in `build/doc/<name>/`, the same pages as Cairn's own, with every claim on its module's page.
`cairn publish [--owner <login>] [--dry-run]`	publishes the commit at the tag `v<version>`, which must be HEAD with a clean tree: its source, its `claims.lock` and its prebuilt Lean. It publishes under the login your token belongs to, or under an Org you can write to with `--owner`; a name's first publish makes that account its owner. The registry refuses a version that drops, renumbers or redefines a claim id. It takes no docs from a publisher; they will be built from the source (issue #94).
`cairn login`	checks a nexthub token with `package:write`, read from standard input, and saves it. Only `cairn publish` needs it: anyone reads the registry, and Lake, git and SwiftPM fetch from it with no credential.

cairn uses the public registry, https://cairn.registry.nexthub.sh. CAIRN_REGISTRY points it at another, such as a local nextpm, and CAIRN_TOKEN gives a token without cairn login, as CI needs.

cairn.toml names the package, its version and the Lean libraries to link. Its name has to match the lakefile's package name and the claim scope, and cairn build and cairn publish check that all three agree.

Checks

Cairn's per-app tools run on any app package, from anywhere in it; Cairn's own make check runs them on its test app, test/fixture. Each writes under the package's build/.

Command	What it does
`cairn fuzz [<target>…] [--iterations N] [--seed S] [--steps K]`	claim-driven fuzzing into `build/fuzz/`. The package declares a `lean_exe fuzz` whose `main` runs `Cairn.Fuzz.main fuzz_targets%`
`cairn claims [<module>…] [--out FILE]`	every claim of the package as JSON
`cairn bench [--product P]`	a release build, then the app's own `--bench`
`cairn size [--product P]… [--limit BYTES]`	the stripped release binary, attributed, and a guard at 5 MB
`cairn conformance [--module M] [--n N]`	the Lean model replayed against the running app through its debug socket. The package has a generator module, `<App>.Conformance`
`cairn bundle [--sign ID] [--name N]`	a release build wrapped in `build/apps/<N>.app`, with the package's `bundle/Info.plist` and `bundle/entitlements.plist` when it has them; signed with `--sign`, else ad hoc

A package of several apps picks one with --app <App> for build, bench, size, conformance and bundle. Running an app is still SwiftPM's: swift run <Product> after cairn build.

Cairn's own checks

cairn run, cairn check and cairn doctor are planned. Until cairn check lands, the lint, axiom audit and kernel replay run from the Cairn repository's Makefile, and so do Cairn's own checks. Run them from the root of the repository; each is shown as it is in the Makefile.

# Everything a PR must pass. The per-app checks run on test/fixture, Cairn's own app; the
# example apps are in their own repository, iamnbutler/cairn_examples.
check: lint audit ledger kernel doctest test selftest fuzz-quick fuzz-scope size fuzz-trusted-quick fixture-ledger site-build registry-check new-check cairn-tool-test

Makefile, lines 68–70

The per-app checks run on test/fixture with the commands above:

# test/fixture: Cairn's own app (test/fixture/README.md), a package of its own that requires this
# checkout by path. The framework's per-app checks (selftest, fuzz-quick, size, bench) run on it
# through the `cairn` CLI, as an app in its own repository runs them (docs/cli.md, "Checks").
FIXTURE = test/fixture
CAIRN = $(CURDIR)/tools/cairn/.build/release/cairn

cairn-tool:
	cd tools/cairn && swift build -c release -q

# The CLI's unit tests, and #196's stale checkout on a localhost dumb-HTTP server (needs python3).
cairn-tool-test:
	cd tools/cairn && swift test -q

fixture-build: lean cairn-tool
	cd $(FIXTURE) && $(CAIRN) build

Makefile, lines 74–88

# Drives the fixture headlessly through the host's real threads, timers and accessibility
# mirror. Then --close-test: the real app's window
# (shown without focus) closed with work in flight; it must quit cleanly.
selftest: fixture-build
	cd $(FIXTURE) && $$(swift build --show-bin-path)/Fixture --selftest
	cd $(FIXTURE) && $$(swift build --show-bin-path)/Fixture --close-test

Makefile, lines 118–123

# Binary size (bench/size.md): the fixture's executable built for release with a link map,
# stripped, attributed (Lean runtime, Cairn, the app, Swift host, shaders), and checked against
# SIZE_LIMIT bytes, with `cairn size` (test/fixture/build/size/). No app links `Lean` (the
# compiler, about 100 MB), so it is a few MB; crossing the limit almost always means something
# imported `Lean`.
SIZE_LIMIT = 5000000

Makefile, lines 269–274