Your first app · Cairn docs

The pieces

A Cairn app has two halves.

Lean holds everything that has meaning: the app's state, the moves a person can make, the view, the claims and their proofs. All of it is pure functions: no IO, no floating point in anything a theorem talks about.
Swift is the host. It owns the window, turns mouse and keyboard input into events, runs the effects Lean asks for (write a file, play a sound), mirrors the frame to accessibility, and paints with Metal. It has no application logic.

Between them, two byte buffers cross on every step: a batch of events going in, and a frame coming out. The host protocol describes them.

To see one before installing anything, try Counter in the browser: every frame there is one its Lean code drew, and every control shows its claim.

What you need

A Mac on macOS 27 with Xcode, for Swift 6 and the Metal toolchain.
Lean 4 through elan. The repository pins the version in lean/lean-toolchain.
bun, for the tools that build these docs.
The Cairn repository: git clone https://github.com/iamnbutler/cairn.
The cairn tool, built from the checkout:

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

docs/cli.md, lines 12–13

Running one

The repository's own app is test/fixture, which Cairn's checks run on. It is laid out the way an app in its own repository is, and built with the cairn tool; the only difference is that it requires the checkout it is in, by path. make fixture-build builds Cairn's Lean, the cairn tool, and then the fixture with cairn build:

# 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

Then cd test/fixture && swift run Fixture opens it in a window. The first build in a fresh checkout takes a while; later ones are incremental.

The fixture, from the top

The fixture's state is a list of items, the id the next item gets, the New item field, and whether the Flash note shows. Its controls are named by control refs: the claim id of the move they perform, and a key (0 for a control there is one of; an item's checkbox uses the item's id).

/-- The list's rows at first, numbered from 1 (keyed controls never use key 0), then key 0 for
the end line. -/
def rowCount : Nat := 10000
def initKeys : Array Nat := (Array.range rowCount).map (· + 1) |>.push 0

structure Item where
  id : Nat
  text : String
  done : Bool := false
deriving Repr, BEq, DecidableEq, Inhabited

structure State where
  items : List Item := []
  /-- The id the next item gets. -/
  nextId : Nat := 1
  field : Text.Field := Text.Field.empty placeholder
  /-- Whether the Flash note shows: from a press of Flash until its timer fires. -/
  flash : Bool := false
  /-- The Passcode field: a secure field (docs/text.md, "Secure fields"). -/
  passcode : Text.SecureField := Text.SecureField.empty passPlaceholder
  /-- The id the next request gets. -/
  nextReq : Nat := 0
  /-- The scroll box's row last pressed. -/
  selected : Option Nat := none
  /-- How many times the end of the rows has come into view (^16). -/
  ends : Nat := 0
  /-- The list's rows, top to bottom, by key: `1` to `rowCount` at first, then the end line's
  key, `0`. The view reads the array as it is (`VList.node`), so it is kept here, not rebuilt. -/
  keys : Array Nat := initKeys
  /-- The key the next added row gets. -/
  nextKey : Nat := rowCount + 1
  /-- Posts 1 to 4's likes and counts, on an optimistic table (Fixture/Like.lean). -/
  likes : Like.Likes := {}
  /-- Whether the list is hidden (^44): the runtime keeps its offset meanwhile. -/
  hidden : Bool := false
  /-- The count on the Dock badge (^45, ^46); no badge at 0. -/
  badged : Nat := 0
  /-- How many announcements have been posted (^47). -/
  said : Nat := 0
deriving Repr, BEq, Inhabited

def fieldRef : ControlRef := ⟨2, 0⟩
def addRef : ControlRef := ⟨3, 0⟩
def toggleRef (k : Nat) : ControlRef := ⟨4, k⟩
def deleteRef (k : Nat) : ControlRef := ⟨5, k⟩
def flashRef : ControlRef := ⟨6, 0⟩
def passRef : ControlRef := ⟨9, 0⟩
def rowRef (k : Nat) : ControlRef := ⟨10, k⟩
/-- The scroll box's ref, keyed by its place: the runtime keeps its offset under it. -/
def rowsRef : ControlRef := ⟨14, 0⟩
def endRef : ControlRef := ⟨16, 0⟩
def addTopRef : ControlRef := ⟨17, 0⟩
def addEndRef : ControlRef := ⟨18, 0⟩
def likeRef (k : Nat) : ControlRef := ⟨21, k⟩
def refreshRef : ControlRef := ⟨23, 0⟩
def topRef : ControlRef := ⟨41, 0⟩
def endButtonRef : ControlRef := ⟨42, 0⟩
def goRowRef : ControlRef := ⟨43, 0⟩
def hideRef : ControlRef := ⟨44, 0⟩
def badgeRef : ControlRef := ⟨45, 0⟩
def clearBadgeRef : ControlRef := ⟨46, 0⟩
def announceRef : ControlRef := ⟨47, 0⟩
def moreRef (k : Nat) : ControlRef := ⟨25, k⟩
def menuToggleRef (k : Nat) : ControlRef := ⟨26, k⟩
def menuDeleteRef (k : Nat) : ControlRef := ⟨27, k⟩
def clearDoneRef : ControlRef := ⟨29, 0⟩
def firstRowRef : ControlRef := ⟨31, 0⟩
def noRowRef : ControlRef := ⟨32, 0⟩

test/fixture/lean/Fixture.lean, lines 76–143

The window is a place, a claim of its own, so moves can say where they appear:

place ^1 window "Fixture window" where
  does "The window: a heading, a paragraph, the New item field and Add, the Passcode field, Flash, the items and the count left."

test/fixture/lean/Fixture.lean, lines 225–226

Then the moves. Each says in plain words what the person does (does) and sees (sees), and in Lean what pressing it does (apply) and must achieve (post), with a proof (sound). Add:

move ^3 addItem (s : State) "Add" in ^1 where
  does "Press Add."
  sees "The field's text, trimmed, is added at the end of the list and the field is cleared. Blank text changes nothing."
  on press
    apply := add s
    post s' := s' = add s
    sound := by intro s; rfl

test/fixture/lean/Fixture.lean, lines 245–251

add is an ordinary function on the state:

/-- The field's text without leading and trailing whitespace. -/
def trimmed (t : List Char) : List Char :=
  ((t.dropWhile Char.isWhitespace).reverse.dropWhile Char.isWhitespace).reverse

/-- Add the field's trimmed text as a new item and clear the field; nothing when it's blank. -/
def add (s : State) : State :=
  if trimmed s.field.text = [] then s
  else
    { s with items := s.items ++ [{ id := s.nextId, text := String.ofList (trimmed s.field.text) }],
             nextId := s.nextId + 1, field := Text.Field.empty placeholder }

test/fixture/lean/Fixture.lean, lines 164–173

The app's behaviour is built from its moves and nothing else. moves% collects every move declared in the namespace, and receive hears the timer Flash sets (chapter 5):

def machine : Machine State := { init := {}, moves := moves%, receive }

test/fixture/lean/Fixture.lean, line 516

The view is a function from the state (and the UI state: hover, focus, window size) to a tree of boxes and text. Each item's row is in the tree only while the item is in the list, and its checkbox and delete button with it:

def view (s : State) (ui : UI) : Node :=
  .box { width := .fill, height := .fill, padding := ⟨20, 20, 20, 20⟩, gap := 12,
         background := some bg, clip := true } none
    [ .text { font := { size := 22, weight := 700 }, color := ink } "Fixture",
      .para { font := { size := 13 }, color := muted } {}
        "Cairn's test app. Type an item and press Enter or Add, check it off or delete it, and \
         press Flash to set a timer. Lean breaks this paragraph to the window's width.",
      inputRow s ui,
      passcodeRow s ui,
      .box { width := .fill, gap := 4 } none
        [ .box { axis := .row, width := .fill, gap := 8, align := .center } none
            ([button ui flashRef "Flash", button ui addTopRef "Add above",
              button ui addEndRef "Add below"] ++
             (if s.flash then [.text { font := body, color := accent } "Flashing"] else [])),
          .box { axis := .row, width := .fill, gap := 8, align := .center } none
            ((if s.hidden then [] else
              [button ui topRef "Top", button ui endButtonRef "End",
               button ui goRowRef "Go to row"]) ++
             [button ui hideRef (if s.hidden then "Show rows" else "Hide rows")]),
          .box { axis := .row, width := .fill, gap := 8, align := .center } none
            [button ui badgeRef "Badge", button ui clearBadgeRef "Clear badge",
             button ui announceRef "Announce"] ],
      .box { width := .fill, gap := 4 } none (s.items.map (itemRow ui)),
      .text { font := { size := 13 }, color := muted } (leftLabel (left s)),
      likesRow s ui,
      if s.hidden then .text { font := { size := 13 }, color := muted } "Rows hidden"
      else rowsBox s ui ]

test/fixture/lean/Fixture.lean, lines 740–768

Finally the app: the machine, one window showing the view, and every claim the app makes.

def claimInfos : List ClaimInfo := claims%

test/fixture/lean/Fixture.lean, line 610

def app : App State :=
  { machine.toApp [.window 1 "Fixture" view, .menuBar 28 menuBar] claimInfos with
    keepScroll := fun _ => [rowsRef] }

test/fixture/lean/Fixture.lean, lines 783–786

The host side

The Lean app is compiled to a static library that exports three C functions: start, step and frame. A small module holds them:

/-- Core Text metrics in the running app. -/
def cfg : Runtime.Config := { metrics := TextMetrics.host }

@[export cairn_app_init]
def appInit (w h scalePercent : UInt32) : Runtime.State State :=
  Runtime.initState app cfg w h scalePercent

@[export cairn_app_step]
def appStep (s : Runtime.State State) (events : ByteArray) : Runtime.State State :=
  Runtime.stepBytes app cfg Frame.boundary s events

@[export cairn_app_frame]
def appFrame (s : Runtime.State State) : ByteArray := Runtime.frameBytes Frame.boundary s

test/fixture/lean/Fixture/Abi.lean, lines 14–26

The Swift executable names those functions, and hands them to the generic host. The module initializer, runtime_initialize_fixture_Fixture_Abi, is declared in a small C target of the app's own, CFixture:

let fixture = LeanApp(
    module: runtime_initialize_fixture_Fixture_Abi,
    initialize: { w, h, scale in cairn_app_init(w, h, scale) },
    step: { cairn_app_step($0, $1) },
    frame: { cairn_app_frame($0) },
    codec: FrameV1Codec())

test/fixture/Sources/Fixture/main.swift, lines 24–29

MainActor.assumeIsolated {
    CairnApp.main(CairnApp.Config(title: "Fixture", size: size) { LeanCore(fixture) })
}

test/fixture/Sources/Fixture/main.swift, lines 567–569

That is the whole of the app's Swift that isn't a test; the rest of its main.swift is --selftest, --bench and --close-test (chapter 6). Everything else (threads, input, text input, accessibility, painting) is the shared host, CairnHost.

The lakefile names the package, which is also the claim scope (the fixture's ids are fixture^N), and the library cairn build links:

/-- Cairn's fixture app (../README.md). The package name is the claim scope: its claims are
`fixture^N`, in ../claims.lock, never in Cairn's. -/
package fixture where
  leanOptions := #[⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩,
    ⟨`weak.cairn.claims.scope, "fixture"⟩]

-- This checkout's Cairn, not a release: the fixture tests the tree it is in.
require cairn from "../../../lean"

/-- The app and its exports (`Fixture.Abi`), which `cairn build` links (bin/cairn-link). -/
@[default_target]
lean_lib Fixture where
  roots := #[`Fixture.Abi, `Fixture]
  defaultFacets := #[LeanLib.staticFacet]

test/fixture/lean/lakefile.lean, lines 5–18

Package.swift builds the host and links that library from .cairn/lib/:

let package = Package(
    name: "fixture",
    platforms: [.macOS("27.0")],
    dependencies: [.package(path: cairnDir.path)],
    targets: [
        // The Lean export Cairn's CLean doesn't declare: the app's initializer.
        .target(name: "CFixture", dependencies: [.product(name: "CLean", package: cairn)]),
        .executableTarget(
            name: "Fixture",
            dependencies: ["CFixture",
                           .product(name: "CLean", package: cairn),
                           .product(name: "CairnFrame", package: cairn),
                           .product(name: "CairnRender", package: cairn),
                           .product(name: "CairnHost", package: cairn)],
            linkerSettings: [.unsafeFlags(["-L" + lib, "-lfixture"])]),
    ]
)

test/fixture/Package.swift, lines 14–30

An app in its own repository

An app lives in a repository of its own and depends on a tagged release of Cairn, the way the example apps do. One tag pins both halves: the Lean package and the Swift libraries. Start one with the cairn tool.

cairn new hello --bin makes hello/ with a cairn.toml, an empty claims.lock, and a lean/ whose lakefile sets the claim scope to hello, so the app's ids are hello^1, hello^2, and so on. The app is a working one, laid out like the fixture: a window with a count and a Count button (a place, hello^1, and a move, hello^2), its exports in lean/Hello/Abi.lean, a Package.swift and a host whose --selftest runs it headlessly. Its Lean files start with public import Cairn, which brings in everything an app links, the claim commands included. cairn new hello --lib makes a library instead, with no host.

cairn add cairn points the lakefile and cairn.toml at Cairn's latest release in the registry and prints the line for Package.swift. An app can also require Cairn from git at a tag:

package yap where
  leanOptions := #[⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩,
    ⟨`weak.cairn.claims.scope, "yap"⟩]

require cairn from git "https://github.com/iamnbutler/cairn" @ "v0.5.2" / "lean"

@[default_target]
lean_lib Yap where
  roots := #[`Yap.Abi, `Yap]
  defaultFacets := #[LeanLib.staticFacet]

docs/package.md, lines 43–52

Then depend on the same tag in Package.swift, and link the library that the build makes:

let lib = Context.packageDirectory + "/.cairn/lib"
// dependencies:
.package(url: "https://github.com/iamnbutler/cairn", exact: "0.5.2"),
// the app's executable:
.executableTarget(name: "CairnYap",
    dependencies: ["CYap", .product(name: "CairnHost", package: "cairn"), /* … */],
    linkerSettings: [.unsafeFlags(["-L" + lib, "-lyap"])]),

docs/package.md, lines 64–70

cairn build builds the Lean, links it with Cairn's runtime into one static library in .cairn/lib/, and builds the host. By hand, that is:

cd lean && lake build
cd lean && .lake/packages/cairn/bin/cairn-link --lib Yap --out ../.cairn/lib/libyap.a
swift build

docs/package.md, lines 94–96

The app's main.swift hands its three exports to the host, as the fixture's does above, and swift run Hello opens it. cairn fuzz, cairn bench, cairn size, cairn conformance and cairn bundle check and ship it from anywhere in the package (chapter 6).

Claim ids

Ids are scoped per package, so an app numbers from ^1. The fixture's are fixture^1 to fixture^9, in test/fixture/claims.lock; the template's are hello^1 and hello^2. Cairn's own are cairn^N: the trusted base's assumptions, ^7, ^214, ^900 and up. Claims that move to another package take their numbers with them: one that was cairn^2 becomes <scope>^2.

Give a new claim an id the package hasn't used (look in claims.lock), then record it from the package's lean/ directory, and commit claims.lock with the claim. For the fixture: lake exe ledger update --scope fixture --root Checks --lock ../claims.lock.