# Your first app

> What a Cairn app is made of, how to run one, and how to start your own.

## 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](https://cairn.iamnbutler.workers.dev/docs/internals/host-protocol.md) describes them.

To see one before installing anything, [try Counter in the browser](https://cairn.iamnbutler.workers.dev/try/counter/): 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](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md), built from the checkout:

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

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

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

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).

```lean
/-- 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:

```lean
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:

```lean
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:

```lean
/-- 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](https://cairn.iamnbutler.workers.dev/docs/guide/effects.md)):

```lean
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:

```lean
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.

```lean
def claimInfos : List ClaimInfo := claims%
```

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

```lean
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:

```lean
/-- 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`:

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

```swift
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](https://cairn.iamnbutler.workers.dev/docs/guide/shipping.md)). 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:

```lean
/-- 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/`:

```swift
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](https://cairn.iamnbutler.workers.dev/docs/examples.md) do. One tag pins both halves: the Lean package and the Swift
libraries. Start one with [the cairn tool](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md).

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

```lean
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]
```

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

```swift
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"])]),
```

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

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](https://cairn.iamnbutler.workers.dev/docs/guide/shipping.md)).

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

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