# The cairn tool

> The command line for Cairn packages. It starts a package, adds dependencies, builds, checks, bundles, documents and publishes it.

> **What works today.** `cairn` starts, builds, documents and publishes a package (`new`, `add`, `build`, `doc`,
> `publish`, `login`), and checks and bundles an app (`fuzz`, `claims`, `bench`, `size`,
> `conformance`, `bundle`), with unit tests.
> Cairn has one public registry, `https://cairn.registry.nexthub.sh`: anyone can read it, and
> publishing takes a token. It holds no prebuilt Lean yet, so the first `cairn build` compiles
> Cairn. Nothing installs `cairn` yet; build it from a Cairn checkout.

## 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
```

## 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](https://cairn.iamnbutler.workers.dev/docs/api/), 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](https://github.com/iamnbutler/cairn/issues/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.

```make
# 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:

```make
# 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

```make
# 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

```make
# 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

From https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt