CLI reference

Status: the Rust compiler (rust/, cargo build --release -p sky) is the primary Sky compiler; the Haskell compiler is preserved under legacy-haskell-compiler/. Verified by the example sweep + compiler test suite (cargo test + xtask gates). See ../history/compiler/versions.md for the changelog.

Every sky subcommand. Run sky --help for the authoritative list.

Build & run

sky build [path]

Compile a Sky source file to a Go binary under sky-out/.

sky build src/Main.sky

Pipeline:

1. Parse sky.toml for [go.dependencies] and [dependencies].
2. Auto-regenerate any missing FFI bindings in .skycache/.
3. Resolve modules, type-check, lower to Go under sky-out/.
4. Invoke go build → sky-out/app (or the bin name set in sky.toml).

Client entries AUTO-SPLIT. When the entry resolves to a client app — a Std.App (App.app / App.run) built for a client target (--target web:app / mobile:* / tablet:*, from which the build synthesises the split), or a low-level Spa.app — sky build src/Main.sky derives a wasm frontend + native backend + shared codec under .split/ (override with --out) and builds both — the split you would otherwise run sky spa-split … --build for by hand. sky run src/Main.sky does the same and then runs the backend (it serves the frontend

• /_rpc + /_sky/console + /_sky/metrics same-origin, one binary).

--target and --embed compose with the split: --target <t> picks the frontend delivery shell, --embed bundles PostgreSQL into the backend, and they combine (sky build --embed --target ios src/Main.sky). Three things skip the split: sky check (type-checks the shared source directly), an explicit --wasm (a raw client build, below), and a project already generated by a prior split (its sky.toml carries a [spa] generated = true marker, so building the generated frontend — itself a client entry — never re-splits). For the explicit form that keeps the artefacts at a chosen path, see sky spa-split.

--wasm compiles a Sky.Spa client for the browser (GOOS=js GOARCH=wasm) instead of a native binary, writing sky-out/main.wasm + sky-out/wasm_exec.js (the matching loader). Standard-Go wasm has full reflect, so it runs in any browser / WKWebView / Android WebView.

sky build --wasm src/Main.sky        # -> sky-out/main.wasm + wasm_exec.js

--target <t> builds the wasm client (implies --wasm), always stages the servable dist/ bundle (index.html + main.wasm + wasm_exec.js), and then — for a native surface — generates a shell and builds it into a real artifact. Each shell is a thin native window over the SAME wasm client, loading it from your backend; client and server stay separate, only the shell is native.

sky build --target web src/Main.sky      # -> dist/ (serve it)
sky build --target desktop src/Main.sky  # -> sky-out/desktop/<app>  (run after starting your backend)
sky build --target ios src/Main.sky      # -> sky-out/ios/build/<App>.app  (xcrun simctl install booted …)
sky build --target android src/Main.sky  # -> sky-out/android/build/<app>.apk  (adb install -r …)

The generated shells point at http://127.0.0.1:8951/ (desktop, via PORT), http://localhost:8951/ (iOS Simulator — shares the host network), and http://10.0.2.2:8951/ (Android emulator's host alias) — start your backend first. For a real device / production, host the dist/ bundle from your backend over https and point the shell there. For ios / android the platform toolchain is checked before the (slower) build, so a missing SDK fails fast with an install hint rather than half-building. The hand-written reference shells live in examples/60-spa-todos/{mobile-ios,mobile-android,desktop} if you want to eject and customize (icons, permissions, package id).

--embed bundles a PostgreSQL distribution into the binary, so ./sky-out/app --embed is a self-contained app and database on a bare host — one file, no system PostgreSQL, no DATABASE_URL.

sky build --embed src/Main.sky
./sky-out/app --embed                       # starts its own cluster
./sky-out/app --embed --data-dir /var/lib/myapp

• What it costs. The binary grows by the compressed bundle — about 25–30 MB — and becomes platform-specific. A build without the flag pays nothing: no bundle is linked, and any archive an earlier --embed build staged is removed.
• Where the bundle comes from. The pin is [database] postgresVersion. sky build --embed uses $SKY_HOME/postgres-bundles/, else re-packs an existing sky db provision --embed cache (no network), else fetches and checksum-verifies the release. A prior sky db provision is not required.
• Cross-compiling. GOOS / GOARCH select the target's bundle, so GOOS=linux GOARCH=arm64 sky build --embed … embeds Linux/arm64 PostgreSQL. A target Sky publishes no bundle for is refused before the build starts — the host's binaries are never embedded into another platform's binary.
• --embed plus an explicit DSN is an error, at app startup, naming the source. There is no precedence that does not either ignore the operator's database or make the flag inert.

--embed belongs on sky build, not on sky run — see below.

--timings (or SKY_TIMINGS=1 in the environment) prints a table of the build's phases, each with its wall-clock and the process's peak resident memory when the phase ended, to stderr when the build ends: loading the sources, parse, canonicalise + typecheck, lower + emit Go, writing sky-out/, go build, and for a client build the split, both legs, the dist/ bundle and its precompression. A split build runs its backend and frontend legs as child sky builds; each leg prints its own table under its own == … == header, and the parent's table gives the wall-clock of each leg. sky check --timings works the same way. Use it to see where a slow build spends its time before you report it.

sky build --timings --target web:app src/Main.sky

What a rebuild reuses. Go's build cache keys on content, and Sky's emitted Go is deterministic, so an unchanged module is never recompiled. A client build keeps each leg's sky-out/ between builds, so a rebuild whose Go did not change does not re-link the backend or the wasm client either. The .gz / .br variants in dist/ are cached by the SHA-256 of the file they compress (in ~/.cache/sky/precompress, or under $XDG_CACHE_HOME), so brotli-11 runs only when the wasm bytes change. sky run does not write them at all: its backend serves the bundle itself and compresses on the fly.

Serial or parallel legs. A leg needs its own sky process (which stays in memory while its go build runs) plus its largest Go compile. The backend and frontend legs of a client build run in parallel only when the machine's available memory holds both legs' sky and Go peaks plus a 1 GB reserve; otherwise they run one after the other. Available memory is free + inactive + speculative pages on macOS (vm_stat) and MemAvailable on Linux, capped by the cgroup's remaining limit in a container. The plan estimates each leg from the size of its generated sources, and raises each figure to the peak the leg measured on a previous build when that was more (each leg keeps the largest it has seen in its own sky-out/, .sky-front-peak-bytes and .sky-go-peak-bytes; a record from a compiler before v0.25.18 is ignored). When memory cannot be read, the legs run serially. SKY_BUILD_SERIAL=1 forces serial and SKY_BUILD_PARALLEL=1 forces parallel. The build prints its decision in the == building … == line and in the --timings report.

Go compile parallelism. go build compiles up to one package per CPU at the same time, and the compile of a large app's generated main package is the largest process in a build (about 2.2 GB for a 22k-line app). So sky build passes go build -p <n> when the available memory does not hold one such compile per CPU plus the 1 GB reserve, with n the number of compiles it does hold (at least 1). The per-compile peak is an estimate from the size of the generated main.go, raised to the largest Go process measured on the project's previous builds (sky-out/.sky-go-peak-bytes) when that was more. Unknown memory builds one package at a time. When a client build runs its legs in parallel, it sets each leg's -p from the memory both legs share. SKY_GO_BUILD_JOBS=<n> sets -p <n> yourself (auto decides as above), and a -p already in GOFLAGS is kept. The decision is printed under the --timings table as go build: -p ….

Build identity. The app's version, commit and build time are automatic: no flag, no environment variable, no CI step. sky build writes them into generated Go source (the sky-out/skybuildinfo/ package), so any go build of sky-out/ carries them, including your own cross-compile (CGO_ENABLED=0 GOOS=linux go build .). They are resolved once, at the project root, and every leg of the build embeds the same values. The commit is, first match wins: SKY_BUILD_COMMIT (optional override); git rev-parse HEAD in the project directory or any parent; the commit variable your CI sets by default (GITHUB_SHA, CI_COMMIT_SHA, BITBUCKET_COMMIT, CIRCLE_SHA1, BUILDKITE_COMMIT, GIT_COMMIT, SOURCE_VERSION, COMMIT_SHA, VERCEL_GIT_COMMIT_SHA, RENDER_GIT_COMMIT, CF_PAGES_COMMIT_SHA, DRONE_COMMIT_SHA, TRAVIS_COMMIT, SEMAPHORE_GIT_SHA, BUILD_SOURCEVERSION; a non-hex value is skipped); else src-<12 hex>, a hash of the source tree, sky.toml and sky.lock. The build time (RFC 3339 UTC) is SKY_BUILD_EPOCH=<unix seconds> (optional override), else the commit time of HEAD when git resolves, else the newest modification time of those source files (git archive | tar -x sets it to the commit time). It is never the wall clock, because a per-build value would re-link the binary on every no-change rebuild. The app reports them at /_sky/buildinfo (with source: git, ci:<VAR>, content, override or ldflags) and in the Sky Console header. Your own go build -ldflags "-X sky-app/rt.buildCommit=..." (also buildAt, skyVersion) still wins, field by field. See docs/observability.md.

sky package --release --target <t> [--upload testflight [--ipa <file>]] [path]

Builds the store / distribution artefact for a native shell into sky-out/release/: a signed .ipa for mobile:ios (unsigned -unsigned.ipa without signing configured), a release .apk signed with your upload key plus an .aab when bundletool is on PATH for mobile:android, and a .app + .dmg for desktop:mac. It runs sky build --target <t> in release mode (device build, release signing, no web inspector).

Signing comes from the environment only (SKY_IOS_SIGN_IDENTITY, SKY_IOS_PROVISIONING_PROFILE, SKY_ANDROID_KEYSTORE, SKY_ANDROID_KEYSTORE_PASSWORD, SKY_ANDROID_KEY_ALIAS, SKY_ANDROID_KEY_PASSWORD, SKY_MACOS_SIGN_IDENTITY, SKY_MACOS_PROVISIONING_PROFILE; see docs/sky-toml.md). Before any build it refuses: no --release (exit 2), a target that is not a native shell, a local or plain-http backend address, a generic permission purpose string, missing Android signing, and an iOS identity without a provisioning profile. Guide: docs/skyapp/native.md.

--upload testflight (with --target mobile:ios or tablet:ipad, on macOS with Xcode) then validates the signed .ipa and uploads it to App Store Connect with xcrun altool, which makes it a TestFlight build. The API key comes from SKY_ASC_KEY_ID, SKY_ASC_ISSUER_ID and SKY_ASC_KEY_PATH (the .p8, which never goes on a command line). --ipa <file> uploads an .ipa packaged earlier, without a build. Before any build or network call it refuses an unknown destination or a non-iOS target (exit 2), a missing Bundle.withId or Bundle.withBuild, a missing key variable or key file, and a build that is not signed for App Store distribution (exit 1). Apple's errors are printed as Apple wrote them with the fix, and the exit status is 1. Guide: docs/skyapp/native.md#upload-to-testflight--sky-package---upload-testflight.

sky spa-split <path> --out <dir> [--build | --target <t>]

The explicit Sky.Spa auto-split generator — the form of the split that sky build / sky run invoke for you (see above); reach for spa-split directly when you want the generated shared//backend//frontend/ kept at a chosen --out path. It takes ONE Sky.Spa project whose update runs effects inline, and generates a wasm frontend + native stateless backend + a shared wire contract — no hand-written API. The compiler infers the client/server split from effects (the rule is dead simple: pure → client, any effect → server; the client is 100 % pure UI), so a database/file/secret/auth value or function can never reach the browser — it is a build failure if it could (a fail-closed guard over every kernel family). Server branches become generated RPC endpoints; Cmd.publish fans out to subscribed clients over SSE (server→client push).

• bare — generates shared/, backend/, frontend/ and prints the build commands.
• --build — also builds both: backend native, frontend wasm (--target web).
• --target <web|desktop|ios|android|tablet> — builds the frontend for that delivery surface (implies --build); desktop/ios/android also produce the native shell (WKWebView / WebView2 / webkit2gtk / Android WebView / SwiftUI) over the same wasm client.
• --embed — builds the backend with an embedded PostgreSQL bundle (the backend owns the DB); combines with --build/--target.

sky spa-split src/Main.sky --out dist/split                 # generate only
sky spa-split src/Main.sky --out dist/split --build         # + build backend + web frontend
sky spa-split src/Main.sky --out dist/split --target desktop # + native desktop shell
sky spa-split src/Main.sky --out dist/split --build --embed  # + PostgreSQL bundled in the backend

The generated backend serves the frontend, the /_rpc/<Msg> endpoints, and GET /_sky/sub (SSE). Client→server is HTTP RPC, server→client is SSE — same origin, so no CORS and a trivial connect-src 'self' CSP. Each /_rpc/<Msg> is a Server.rpc route (same-origin application/json POSTs only), and /_sky/sub streams a topic only when the app's subscriptions for the verified session name it (auto-split.md §21). Inspect the derived split first with sky spa-partition — it prints each branch CLIENT/SERVER with the reason. (In-process broker = single replica; SKY_LIVE_BROKER_URL gives cross-replica push, same as Sky.Live.) Design + internals: docs/skyspa/auto-split.md.

sky spa-partition <path>

Read-only: prints the inferred client/server partition of a Sky.Spa update — each branch as CLIENT or SERVER with the taint reason, each server branch's RPC inputs/outputs, and the server-tainted top-level bindings. Answers "what runs where, and why" before you generate anything with sky spa-split. Nothing is hidden: the split is inferred but always inspectable.

sky run [path]

sky build + execute the resulting binary. On a Sky.Spa entry it auto-splits (as sky build does) and runs the backend, which serves the frontend + /_rpc same-origin; --embed and --target compose (sky run --embed src/Main.sky runs the backend with its own bundled PostgreSQL).

For a plain (non-Spa) app in development you do not need --embed (and sky run --embed on such an app is refused with a pointer): set [database] embedded = true in sky.toml and sky run starts a local cluster, injects the DSN, and stops it on exit. See sky db start.

--profile turns on runtime profiling of the app (not the compiler) — for when an app hangs, spins the CPU, or eats memory and you can't tell which. It writes a profile/ directory next to your project on stop:

Options:

• --profile-dir <dir> — where to write (default profile/, relative to the project root).
• --profile-timeout <dur> — if the app hasn't exited after <dur> (e.g. 30s, 2m), dump profiles with a hang verdict and exit. Opt-in — leave it off for a server (which "hangs" by design); it still profiles until you Ctrl-C it.

sky run src/Main.sky --profile                     # profile until exit / Ctrl-C
sky run src/Main.sky --profile --profile-timeout 30s   # + auto-dump if it hangs

The stop fires whichever comes first: normal exit / panic, a signal (SIGINT/SIGTERM/SIGQUIT), or the timeout. --profile off means zero overhead — profiling is armed purely by an env var the flag sets, and the emitted Go is byte-identical either way.

sky verify [project]

The one-command pre-release gate for a project. Run inside a project dir (or pass its path) and it runs, in order, stopping non-zero on the first failure:

1. fmt — every .sky file under the source root + tests/ is already sky fmt-clean.
2. check — type-checks + go builds and emits the production binary (sky check ≡ sky build minus the artefact, so this one build covers both).
3. test — every tests/*.sky suite passes.

sky verify           # gate the current project
sky verify path/to/app

A library package has no entry to build: its sky.toml names no entry, and it declares a [lib] table or has no Main module. For one, the check step type-checks and go builds every module under the source root (through a generated entry that imports each of them, built in a scratch directory), the tests run as usual, and only the entry binary is skipped:

  ✓ fmt      (2 file(s) clean)
  ✓ check    (library: 1 module(s) type-check and build; no entry binary)
  ✓ tests    (1 suite(s) passed)

In the compiler repo (a dir with examples/), sky verify instead builds AND runs every example — the runtime smoke sweep. sky verify --help documents both modes.

sky check [path]

Fully validate the program. sky check is a strict superset of sky build: it runs parsing, canonicalisation, HM inference, Go codegen, and invokes go build on the emitted output — without producing a runnable binary. If sky build would fail, sky check fails with the same error. This is the soundness gate — editor integrations should use it directly.

sky check <module.sky> on a module that is not a program entry (it defines no main and no Std.App app) checks that module and what it imports the way a library check does: it type-checks, lowers and go builds them, and prints Checked module <Name> …. The program entry is checked by sky check with no path, or by naming the entry file.

Machine-readable output: --format json

sky check, sky build, sky test and sky fmt --check take --format json (or --format=json; --format text is the default). Stdout then carries only NDJSON: one JSON object per line. The human text (progress, the Elm-style error blocks, a test suite's ok / FAIL lines) goes to stderr. The exit code is the same as in text mode (sky test: 0 all passed, 1 a test failed, 2 nothing ran).

sky check --format json src/Main.sky

{"kind":"diagnostic","schema":1,"file":"src/Main.sky","range":{"start":{"line":8,"character":4},"end":{"line":8,"character":10}},"severity":"error","code":"E2001","message":"[x] type mismatch: `String` vs `Int`","source":"sky"}
{"kind":"summary","schema":1,"command":"check","ok":false,"errors":1,"warnings":0,"durationMs":146,"root":"/home/me/app"}

Every line has "schema": 1 and a "kind". The schema number changes only when a field changes meaning or type; a new field does not change it.

The diagnostics are the same values the text mode prints, so the two modes report the same errors. A parse, name or type diagnostic has the location of its primary label. A lowering warning or error (the memoised-value lint, an unresolved Go-FFI call, an over-applied kernel, an internal compiler error) has the location of the expression being lowered when it was raised, else of the definition's name; the text mode prints it as src/Main.sky:11:1: …. A go build failure is reported against the Go file go named (sky-out/main.go, or a file in a local Go path dependency) with source: "go", because the generated Go carries no map back to the Sky source.

file and range are null only for a diagnostic that is about the program or the project as a whole and so has no source node:

• the lowering warning no \main` in entry moduleand the driver errorsno entry module named …, no .sky under …, lowering found no entry `main`, Sky dependency … not fetched` and the missing path-dependency error;
• sky.toml warnings (an unknown key, a [database] driver that contradicts its DSN), path-dependency drift warnings, and the legacy-config migration hint (info);
• a Sky.Spa split that refuses the app as a whole (cannot auto-split: …);
• a go build failure with no file.go:line:col line (a toolchain error);
• sky fmt --check (one error per unformatted file: file is set, range is null).

A failing run that produced no error line of its own gets one that points at stderr, so ok: false always comes with a reason.

Sky.Spa builds. sky build of a Sky.Spa entry checks the app's own source first (the same front half sky check runs), so an error in the app is reported against src/… in both output modes. It then builds the two generated projects of the auto-split. In json mode each of those builds runs with --format json and its diagnostics are relayed with an extra key, "half": "frontend" or "half": "backend" (an added key, so the schema stays 1). A diagnostic in a module the split copied unchanged is reported against the app's own file (src/Store.sky); one in a generated or rewritten file is reported against that file's real path (.split/backend/src/Main.sky). A module both halves compile can report the same warning once per half.

sky fmt --format json needs --check: it reports, it never rewrites.

sky watch [path]

File-watch-driven hot rebuild + restart. Watched scope is a strict allowlist: sky.toml + the entry-point's directory (recursive .sky walk) + tests/ at the project root if present. Generated dirs (sky-out/, .skycache/, .skydeps/, node_modules/, .git/) are excluded.

sky watch                           # entry: src/Main.sky
sky watch src/Main.sky              # explicit entry
sky watch --no-run                  # rebuild only (don't spawn)
sky watch --clear                   # clear screen between rebuilds
sky watch --interval=200            # poll interval ms (default 200)
sky watch --debounce=150            # debounce after a change (default 150)
sky watch --kill-timeout=3000       # SIGTERM grace before SIGKILL
sky watch --watch=docs/notes.md     # additional path (repeatable)

Build-error policy: on a failing rebuild, the previously-running binary stays alive. The next successful build kills + respawns. A typo halfway through a save doesn't tear down the dev session.

Caches reused: .skycache/source.hash (full short-circuit on unchanged source), .skycache/lowered/ (per-module IR), .skycache/ffi/*.skyi (HM types — never regenerated by watch). Typical warm rebuild: 1-3 s.

Signals: Ctrl-C and SIGTERM both go through the clean-teardown path. Sky.Live's SSE handshake auto-reconnects post-restart (banner shows "Reconnecting…" for ~1 s then clears).

sky doc [target] [--list] [--serve] [--tui] [--port N]

Browsable API documentation for the Sky stdlib + project + deps. Four modes:

sky doc Sky.Core.String          # terminal: list every symbol with its HM signature
sky doc List                     # shorthand for Sky.Core.List
sky doc --list                   # print every documented module
sky doc --serve                  # HTTP doc server (auto-opens browser)
sky doc --serve --port 8081      # custom port
sky doc --tui                    # interactive terminal doc browser (Sky.Tui)

--serve and --tui are mutually exclusive — --serve runs the Sky.Http.Server bundle; --tui runs the Sky.Tui bundle. Both consume the same on-disk catalogue rendered to .skycache/doc-out/ under the project root.

Which stdlib. Inside the Sky repository (a directory with sky-stdlib/ and runtime-go/ above the working directory) sky doc reads the working-tree sky-stdlib/, so it shows edits that are not released yet. Anywhere else it reads the stdlib embedded in the sky binary. The first line of the output names the source: stdlib: working tree (<repo>/sky-stdlib) or stdlib: embedded in this sky binary. A record type alias is printed with its fields (type alias Chunk = { data : String , … }).

The HTTP server (default :8080) renders:

• Per-module pages with HM signatures, Markdown-rendered doc comments, and an in-module symbol filter (counter shows X / Y).
• Fuzzy search by name, module, OR type signature (Hoogle-style, case-insensitive — string -> int or String -> Int both find String.length, String.toInt etc.).
• FFI binding browsing — every imported Go-pkg FFI dep lists its surface alongside the stdlib.
• Live reload if the underlying project changes (re-runs the index build on each request).

The server is a Sky.Live mini-app bundled into the compiler binary (sky-bundled/doc/), spawned as a child + reverse-proxied behind the sky doc --serve entry point.

--tui runs the Sky.Tui sibling (sky-bundled/doc/src/MainTui.sky) which reads the same JSON catalogue and renders an interactive terminal view: ↑/↓ navigate, Enter expands the highlighted entry, / focuses the search box, Esc clears, Ctrl-C quits.

sky doc --diagram <kind> [--format puml|md|svg] [--out <path>]

A read-only architecture diagram of the current project, drawn to an audit-grade standard — the kind an engineer uses for an architecture deep-dive and that stands up in a SOC2 / ISO review. Four kinds ship today — components, wire, telemetry, and journey. Three formats are available for every kind: puml (raw PlantUML, the default), md (a Markdown table), and svg (a self-contained SVG the compiler draws itself, with no external tool). --out <path> writes the output to a file instead of stdout. Mermaid is retired.

sky doc --diagram components               # raw PlantUML (default)
sky doc --diagram components --format svg  # a self-contained SVG
sky doc --diagram components --format md   # a module → capability table
sky doc --diagram wire --target web:app    # the Sky.Spa /_rpc contract, as PlantUML
sky doc --diagram wire --out wire.puml     # write the PlantUML to a file
sky doc --diagram telemetry --format md    # the privacy/observability inventory
sky doc --diagram journey --format svg     # the page state machine, as an SVG
sky doc --diagram journey --target web:app # client/server split per action (Sky.Spa)

The PlantUML output is a raw @startuml … @enduml document with one title line, a shared skinparam block, and a legend — so it pipes straight into a .puml file. The SVG output is a complete <svg>…</svg> document, laid out with orthogonal edges only, collapsed parallel edges, generous spacing, a legend, and a canvas sized to its content — no diagonal spaghetti and no overlapping labels. All three formats carry the same depth — the table lists, the per-branch effect families, the effectful / pure action split — as node labels + notes (puml), sections + tables (md), or drawn sections (svg); the md form additionally carries the reader notes as prose.

The three architecture kinds are target-aware: the zones, crossing labels and sections change with the app shape derived from the resolved target — Sky.Spa (a wasm client + a server over /_rpc), Sky.Live (one trusted server serving SSR + one SSE channel per session), Sky.Tui / Sky.Cli (a single terminal binary, no network boundary), and Sky.Http.Server (an HTTP API). --target overrides the sky.toml [app] target.

components is a C4 container diagram. It does not draw every module (that detail stays in the md table); it collapses the app to a handful of containers inside dashed trust-boundary zones, left → right: a User actor, a Browser · untrusted zone holding the SPA «wasm client» (Sky.Spa only), a Server · trusted zone holding the Backend «native» container with its data stores (Database, Files) and an audit-egress sink below it, and an External zone holding any External HTTP systems. The Database container lists the app's real table names — every Std.Db.Schema.table / Std.Db.Store.fromCodec name, capped at eight with a "+N more" line. For a Sky.Spa app the /_rpc crossing is labelled with the count of effectful actions that round-trip (N effectful → /_rpc), and a caption under the SPA states how many pure client actions stay in the wasm client. Auth is a control marker on the crossing; the remaining effect families (Env/Config, Jobs, Realtime, Time/Random/Uuid) fold into the Backend subtitle. A Sky.Live app drops the Browser zone and connects the actor (User (browser)) straight to the Backend over HTTPS + SSE; a terminal app draws a single Process · local zone with an in-process edge and no auth crossing; an HTTP app connects a Client over HTTPS.

wire is a data-flow diagram (DFD). The headline is the trust boundary: a client entity and a Server · trusted process either side of a dashed boundary line, with a representative request / response crossing labelled for the shape (request · /_rpc for Spa, an interaction · SSE / patch · SSE session channel for Live, HTTP for an API). For a Sky.Spa app the RPC endpoints (/_rpc) table lists every SERVER update branch that becomes a POST /_rpc/<Msg> endpoint, with its REQUEST (the Model fields it reads plus the Msg args, or "whole model"), its RESPONSE (the fields it writes), and the effect families it reaches — so a missing read is visible at a glance. Beside it, an HTTP endpoints section lists the raw App.api endpoints that sit outside /_rpc (an inbound Stripe webhook, say): each is drawn as an inbound external entity crossing the boundary to a CSRF-exempt endpoint. A Sky.Live app has no /_rpc; it shows its HTTP route table — page GET routes (App.route / App.routeParam) plus any raw App.api — and the SSE session channel as the browser↔server interaction. An HTTP app shows its whole Sky.Http.Server route map (method, path, handler, kind). A terminal app has no network boundary, so it prints one clear line.

telemetry is a data-egress inventory — what behavioural data leaves the system, and to where. Modules sit on the left; the sinks on the right are grouped into Internal (structured logs — console; OTel when OTEL_EXPORTER_OTLP_ENDPOINT is set), External egress (the analytics store), and Consent (the per-session consent state). One collapsed edge per module → sink pair carries the comma-joined events (no parallel overlapping edges); a chatty module is summarised as a few events plus "+N more" (the full list stays in the md table). Log and Analytics are effect kernels, so under a Sky.Spa split they run on the server, reached over /_rpc. An app with no such call sites prints a short note and exits 0.

journey is a TEA state machine. Each page (a Page union variant the Model's page field uses, with its URL when the app declares an App.withRoutes table) is a state, ranked left → right from the initial page (which carries the [*] entry). Parallel Msgs between the same two states are collapsed onto one edge whose label lists them, so labels never stack on top of each other; a self-navigation is one collapsed self-loop; a run-time-chosen target routes to a (dynamic page) state. Below the machine, the non-navigating actions are split into two typed sections: Effectful actions (server-classified — they reach a side effect), each chip annotated with its effect families (AddToBasket · Db), and Pure actions (client-only UI, no effect). The section labels are shape-aware: Effectful (server · /_rpc) for Spa, server-side for Live, in-process for a terminal app. A Cli app (a TEA loop with no Page union) drops the state machine and shows only the two action sections; an HTTP API prints one clear line. Per-page attribution is best-effort: a navigation target is the page an action routes TO, not attributed to a source page (the md form carries that note).

The components, wire, and journey kinds reuse the same analysis as the Sky.Spa auto-split, so the diagram cannot drift from what ships; no kind type-checks beyond the shared source load, lowers, go builds, or writes.

The remaining kind — callpath — is planned and exits non-zero with a "not yet implemented" note today.

sky doctor [--fix] [--verbose]

Project + environment health checks. v0.15.48 shipped 15 checks total — the foundational 5 (sky.toml syntax, stale .skycache/, stale sky-out/, port-in-use, missing FFI) plus 10 tooling-polish additions:

The Sky compiler repo also gets mem-guard (Info: running mem-guard.sh check) — gated to the compiler repo so user projects don't see it.

sky doctor                       # report only
sky doctor --fix                 # apply safe fixes (clean stale caches, etc.)
sky doctor --verbose             # print check-id alongside each finding
sky doctor --warm-cache          # prime the Go build cache (native + wasm)

The Sky Go build cache

sky build runs go build, which stores compiled objects in a build cache. Sky keeps its own isolated cache at ~/.sky/go-build (rather than the shared machine-global Go cache), so Sky can bound its size and refresh it on upgrade without ever touching the cache your other Go projects rely on.

• Warm the cache with sky doctor --warm-cache — it compiles the runtime for native and js/wasm so the first real build is fast instead of a cold compile. sky upgrade runs this automatically for the new version.
• Size is bounded. The cache is pruned when it grows past a cap (default 10 GB, set SKY_GO_CACHE_MAX_GB to change it), so it never fills your disk.
• Shared safely across versions. A new compiler embeds a new runtime, and its objects get new content-addressed keys, so two sky versions (an installed release and a dev build, or an upgrade while an editor still runs the old one) share the cache without cleaning it for each other. The old version's entries are reclaimed by Go's own trim (unused for five days) and by the size cap.
• Escape hatch. Set your own GOCACHE and Sky uses it as-is and manages nothing (its size and lifetime become yours to control).

Exit codes: 0 clean, 1 warnings, 2 errors. CI-friendly.

sky verify [example]

CI canonical runtime check. Iterates every directory under examples/ (or the named one), builds it, go builds the emitted Go, and runs it (cmd_verify, rust/crates/sky/src/main.rs:3842-3941).

Output lines: ok: <name>, FAIL build: …, FAIL go-build: …, FAIL run: …. Exit code is non-zero if any example fails.

sky verify does no scenario-driven HTTP assertion, and this section used to say it did. The removed text described hitting / plus "any routes declared in examples/<n>/verify.json", checking status codes and body substrings, skipping GUI examples via SKY_SKIP_GUI=1, printing runtime ok: / FAIL scenario: / [skip], and a {"requests":[… "expectStatus" … "expectBody" …]} schema. None of it exists — grep -rn 'verify.json\|expectStatus\|SKY_SKIP_GUI\|runtime ok\|FAIL scenario' rust runtime-go scripts returns nothing from the verify path.

Two consequences worth knowing:

• Four committed verify.json files are dead inputs. examples/{15-http-server,30-sse-server-demo,32-sse-relay,33-websocket-echo}/verify.json are read by nothing.
• GUI skipping is not env-gated. It is a hard-coded skip-gui row in scripts/verify-cli.sh:71.

The scenario-contract mechanism the old text described does exist — under a different name, in a different tool: scripts/example-e2e.sh reads examples/<n>/e2e.json and honours expectStatus (example-e2e.sh:113, :185). That is the behavioural tier in docs/rust-rewrite/11-testing-and-verification.md §1. To get scripted HTTP assertions on an example, write an e2e.json — not a verify.json.

sky test <file>

Run a Sky test module. Only that suite and the project modules it imports are built, so a type error in another suite under tests/ does not stop it (sky verify runs every suite). See testing.md. --format json prints one test line per case and a summary with the case counts (see Machine-readable output). A project with a .env.test file runs in test mode: outbound HTTP is mocked from tests/mocks/ fixtures (unmatched requests fail closed), a [database] project gets an ephemeral offline database, and SKY_TEST_SEED / SKY_TEST_CLOCK_MS make effects deterministic. The mock fixture shape and the multi-outcome patterns are in testing.md.

sky test --scaffold-mocks writes mock-fixture skeletons for the app's outbound HTTP boundary (method + urlContains pre-filled from the typed IR; fill each body with a captured payload). It never overwrites an existing fixture. See testing.md.

sky fuzz <file>

The unified app fuzzer for any TEA app (Spa or Live). It always runs the model no-panic net: derives a Msg generator from the app's own Msg union, folds random Msg sequences from init () through the real update, and asserts no unclassified panic. Runs offline under test mode.

sky fuzz src/Main.sky --iters 500 --seed 42          # model no-panic net
sky fuzz src/Main.sky --target web:app --iters 500   # + the differential split oracle

--target (default: the project's sky.toml [app] target) selects the app shape. When it is a Sky.Spa client target (web:app, mobile*, desktop:<os>, tablet:<os>) sky fuzz ALSO runs the differential split oracle: it runs each random (Model, Msg) directly and through the client/server split and asserts the two agree — a free oracle that catches dropped read/write-set fields and Msg-argument collisions. A non-split target (or none) runs the model net alone. This replaces the former sky spa-diff-fuzz verb. Exit 0 on PASS, non-zero on the first divergence or panic (reproducible with the same --seed). See testing.md.

Configuration

sky config migrate

Rewrite a legacy sky.toml's runtime keys into a typed config binding (the Sky.Config / Live.withX surface — see sky.toml typed config).

sky config migrate            # move legacy runtime keys → typed config, in place
sky config migrate --dry-run  # print the summary + diff, write nothing
sky config migrate --check    # exit non-zero if legacy runtime keys remain (CI gate)

• migrate rewrites sky.toml and the entry module, then tells you to review with git diff and run sky check.
• --dry-run shows the moved / removed / changed key summary and the diff without writing any files.
• --check is the CI gate: exit 0 when no legacy runtime keys remain, non-zero (listing them) when they do. --check and --dry-run are mutually exclusive.

The same legacy keys, when present, are also reported by a migration LIST printed on every sky build / sky run (moved / removed / changed), self-extinguishing once the keys are gone. Both the build-time hint and this verb derive from one migration table, so the hint names exactly what the verb rewrites.

Database

sky db status [FILE] · sky db migrate [FILE]

Inspect and apply Std.Db schema migrations. FILE defaults to src/Main.sky.

sky db status      # report applied / pending / drifted migrations, then exit
sky db migrate     # apply all pending migrations in order, then exit

Both build the project, then run it in DB-ops mode — the app's Db.migrate call does the work and exits before serving. The underlying mechanism is the SKY_DB_OP env var (status / migrate), usable directly in a deploy pipeline: SKY_DB_OP=migrate ./sky-out/app.

• sky db status exits non-zero on drift (an applied migration whose SQL was edited) — use it as a CI schema-drift gate.
• sky db migrate exits non-zero if a migration fails — run it as a pre-cutover deploy step so a bad migration blocks the rollout.
• There is no migrate <singlefile>: migrations are an ordered, checksum-tracked set; migrate always applies every pending one.

See Sky.Db — Schema migrations.

sky db migrate --gen [NAME] — file-based migrations (no live DB)

When you define your schema with Std.Db.Store + Std.Codec and expose a db : Store.Project binding, --gen derives migration files from the types — no database connection required:

sky db init                      # scaffold db/migrations/ + db/schema.json (once)
sky db migrate --gen init        # first migration: CREATE TABLE for every store
# …add a field to a record, then:
sky db migrate --gen add_stock   # → addColumn (required cols get a safe backfill DEFAULT)
sky db status                    # ✓ applied / ○ pending per committed file vs the ledger
sky db migrate                   # apply the committed db/migrations/*.json to the live DB
sky db seed                      # run the entry module's seed : Db -> Task Error ()

sky db status compares the committed files against the live _sky_migrations ledger and exits non-zero while anything is pending — a ready-made "is this DB up to date?" deploy gate. sky db seed runs the seed binding your entry module exposes (module Main exposing (main, db, seed)), against the live DB.

sky db push — no-migration-files dev sync

sky db push        # create missing tables + add new columns to match your types

The fast prototyping loop (Prisma-style db push): syncs the live DB to your current db : Store.Project with no migration files — creates each missing table and adds any new (nullable) columns. Additive + idempotent; never drops or retypes. Use sky db migrate --gen once your schema stabilises and you want reviewable, committed history for production.

sky db reset [table] · sky db drop [table] — destructive resets

sky db reset            # empty EVERY declared table (keep schema + the ledger)
sky db reset users      # empty just the `users` table
sky db drop             # drop EVERY declared table + `_sky_migrations`
sky db drop users       # drop just the `users` table (ledger untouched)

Both operate on the tables your entry module declares via db : Store.Project (each Table carries its name / cols / pk) — not on other tables that happen to share the database.

• sky db reset EMPTIES the data and resets autoincrement counters, but KEEPS the schema and the _sky_migrations ledger. On Postgres it runs one TRUNCATE … RESTART IDENTITY CASCADE; on SQLite it DELETEs each table and clears sqlite_sequence (foreign-key enforcement is toggled off for the operation). The fast "wipe my dev data, keep the tables" loop.
• sky db drop removes the tables. Dropping ALL declared tables also drops _sky_migrations, returning the database to a fresh "never ran migrate/push" state; a single-table drop (sky db drop users) leaves the ledger alone. Uses DROP TABLE IF EXISTS … CASCADE (Postgres) / DROP TABLE IF EXISTS … with FK enforcement off (SQLite).

Both are destructive, so both prompt before doing anything:

This will reset 3 table(s) in sqlite — type 'yes' to continue:

• --yes / -y skips the prompt (scripts, CI, container entrypoints).
• On a non-TTY without --yes, the command refuses rather than guess.
• In production (ENV / SKY_ENV in {production, prod, staging}) it refuses unless --yes is passed explicitly.

Scope note. reset / drop only touch the tables your Store.Project declares. For a TOTAL wipe of a shared database (every table + extensions + sequences, including ones Sky doesn't know about), use your database's own tooling — e.g. DROP SCHEMA public CASCADE; CREATE SCHEMA public; on Postgres, or delete the SQLite file.

sky db start · sky db stop · sky db ps — the local PostgreSQL cluster

Every verb above talks to a database. These three are the database: they supervise a local PostgreSQL cluster for the project you are standing in, so development runs the same engine production does instead of the SQLite that quietly diverges from it. The design is docs/skydb/embedded-postgres.md.

sky db start        # initdb on first use, then start; already running is a no-op
sky db ps           # this project's cluster
sky db ps --all     # every Sky-managed cluster on the machine
sky db stop         # stop this project's cluster (pg_ctl stop -m fast)
sky db stop --all   # stop all of them

$ sky db start
sky db start: PostgreSQL 18.6 running (pid 41277).
  data:   /Users/dev/shop/.skydata/pg
  socket: /tmp/sky-9f2c1a4b7e03d5c8
  log:    /Users/dev/shop/.skydata/postgres.log

Connect with:
  psql -h /tmp/sky-9f2c1a4b7e03d5c8 postgres
  DSN: postgresql:///postgres?host=/tmp/sky-9f2c1a4b7e03d5c8

• One cluster per project, in .skydata/pg/ (gitignored by sky init). rm -rf .skydata resets exactly one project, and two projects on different PostgreSQL majors never fight.
• A unix socket, never a TCP port — so two sky db starts cannot race over a port and nothing is exposed to the network. The socket lives in a short hashed directory outside the project ($XDG_RUNTIME_DIR/sky/<hash>/, else /tmp/sky-<hash>/), because sockaddr_un caps a socket path at ~107 bytes and a deeply nested project overflows it.
• Tuned small — shared_buffers = 32MB against PostgreSQL's 128MB default, so an idle project cluster costs tens of megabytes rather than hundreds. Only resource knobs are set; nothing that changes what a query means.
• A machine-level registry at ~/.sky/clusters.json is what lets sky db ps --all see clusters this shell did not start. It is reconciled on every read: a dead pid is erased, and a vanished data dir is dropped.
• Idempotent by design. Starting a running cluster and stopping a stopped one both succeed, so both are safe in a script or a shell trap.

The binaries are discovered, in order, from SKY_POSTGRES_BIN, then ~/.sky/postgres/<version>/bin (pinned version first, then newest), then PATH; a directory must hold initdb, pg_ctl and postgres to count. SKY_POSTGRES_BIN set but incomplete is an error rather than a fall-through — silently using a different installation is worse than the typo. Set SKY_HOME to relocate the registry (tests and CI).

sky db provision --embed — fetch PostgreSQL, no system install needed

Populates the middle entry of that discovery order with Sky's own build of PostgreSQL, so a machine with no PostgreSQL at all can still run sky db start.

sky db provision --embed                 # fetch, verify, install, pin
sky db provision --embed --force         # re-install over an existing cache
sky db provision --embed --from ./postgres-18.6-linux-amd64.tar.gz \
                        --checksum <sha256>   # offline, from a local file

$ sky db provision --embed
sky db provision: fetching https://github.com/anzellai/sky/releases/download/…
sky db provision: PostgreSQL 18.6 installed.
  /Users/dev/.sky/postgres/18.6/bin
  pinned in sky.toml ([database] postgresVersion = "18.6")

Next: sky db start

• Verified before it is trusted. The release's SHA256SUMS is fetched first, the downloaded archive is hashed on disk, and a mismatch installs nothing and says so. A corrupt or truncated download never reaches the cache.
• Installed atomically — extracted to scratch and renamed into place, so an interrupted provision leaves no half-populated bin/ for discovery to find.
• Idempotent. Already provisioned is a fast success with no request made.
• Pinned in sky.toml as [database] postgresVersion, and discovery prefers that version, so a checkout on another machine gets the PostgreSQL the project states.
• Offline-capable via --from (with --checksum, or a SHA256SUMS beside the archive). sky doctor --fix pre-warms the cache for a project with [database] embedded = true. SKY_POSTGRES_BUNDLE_URL points at a mirror.

Bundles are built from source in Sky's CI for linux-amd64, linux-arm64, darwin-amd64 and darwin-arm64; psql is deliberately excluded (GNU readline is GPL-3.0). Windows is out of scope — use a system PostgreSQL and SKY_POSTGRES_BIN.

sky db provision --shared — one cluster for every app on a host

The production counterpart to sky db start. --embed provisions the binaries; --shared provisions the cluster they run, at a stable state directory (/var/lib/sky, /usr/local/var/sky on macOS, --state-dir to move it), tuned from the host's real RAM and CPU rather than from the small development profile.

sky db provision --shared --service --backup --start   # once per host
sky db provision --shared --app orders                 # once per app, prints its DSN
sky db provision --shared --app orders --rotate-password
sky db provision --shared --dry-run                    # show the conf, hba, SQL and units

$ sky db provision --shared --app orders
sky db provision --shared: app orders is ready.
  database: orders
  role:     orders  (may connect to orders and to nothing else)

DSN — sky does not write this anywhere; put it in your secret store:
  postgresql://orders:<generated>@/orders?host=/var/lib/sky/run

• A database and a role per app, the role granted CONNECT on its own database and PUBLIC's implicit access revoked. App A's credentials are refused by PostgreSQL — not by an application check — when pointed at app B.
• Socket-only by default. --listen <addr> adds a TCP listener with scram-sha-256 on loopback; without it nothing is exposed to the network.
• An OS service unit with --service, generated into <state>/service with the sudo lines to install it: a systemd unit on Linux, a launchd job plus a shutdown wrapper on macOS. Both stop PostgreSQL with SIGINT (fast shutdown); a SIGTERM means smart shutdown, which waits for every client for ever.
• A backup timer with --backup: pg_dump --format=custom per app on a daily schedule (--backup-at HH:MM, --backup-keep <days>), reading the app list at run time so an app added later is included.
• Run it as the account the cluster will run as — sudo -u postgres sky db provision --shared. Running as root is refused, as initdb refuses.
• Re-running --app is idempotent and prints no DSN: the password is stored as a SCRAM verifier and cannot be read back, so a printed one would be invented. --rotate-password issues a new one.

SKY_PG_TUNE_MEM_MB states the RAM the cluster may use, for containers where /proc/meminfo reports the host's total rather than the cgroup limit.

sky db init and sky db status belong to the migration engine documented above and are unchanged. The cluster verbs are start / stop / ps / provision.

Running migrations as part of sky run

sky run takes --db-push, --db-migrate, and --db-seed flags that run those steps (in that order) before the app starts — the container-entrypoint "migrate-then-serve" shape. Any step failing aborts the run.

sky run --db-migrate --db-seed src/Main.sky   # apply committed migrations, seed, serve
sky run --db-push src/Main.sky                # dev: sync schema, serve

Deploying — self-migrating binaries

When a project has db/migrations/, sky build embeds the migrations into the binary. A deployed binary then self-migrates with no source tree and no sky toolchain on the host:

SKY_DB_OP=migrate ./app   # apply the embedded migrations, print a summary, exit
SKY_DB_OP=status  ./app   # report applied / pending, exit
./app                     # (unset) boot + serve — no migration on boot

Run SKY_DB_OP=migrate ./app once as a deploy step (a single owner), then start your replicas normally — booting without SKY_DB_OP never migrates, so scaling out is safe. The connection comes from the app's usual config (DATABASE_URL / <PREFIX>_DB_PATH).

How it works — gen builds a temporary DB-free entry (main = Store.dumpSchema db), captures the type-derived schema, and diffs it against the committed snapshot db/schema.json:

• new table → createTable; new required column → addColumn NOT NULL DEFAULT <zero> (backfills existing rows); new Maybe column → nullable.
• dropped column / table / type change → quarantined in a destructive array in the migration file, never auto-applied (the "never silently lossy" rule). On a TTY, gen instead asks: a drop can be resolved as a (r)ename (rewritten to one renameColumn, data preserved), a confirmed (d)rop, or (s)kip; a required new column can take a custom backfill default. Non-interactive (CI / piped) runs keep the safe quarantine defaults.

The output is committed to git (db/migrations/*.json + db/schema.json), so review + history live in the repo. sky db migrate (with db/migrations/ present) applies the files through the same checksummed _sky_migrations ledger as the code-defined path — at most once each, dialect-correct for the live connection (one file → correct on SQLite and Postgres).

Cache & cleanup

sky clean

Removes:

• sky-out/ — compiled binary + Go source
• .skycache/ — generated FFI bindings, lowered-module cache, incremental state
• .skydeps/ — Sky source dependencies (if any)
• dist/ — release archives

Rebuild from scratch with sky build after sky clean.

Dependencies

sky add [--go|--sky] <pkg>[@version]

Adds a dependency. With neither flag, sky add smart-resolves whether the target is a Go module or a Sky-source package and routes accordingly; --go / --sky force one path and skip the probe.

For a Go module it fetches the module, runs the FFI inspector, generates the FFI surface (sky-ffi/<slug>.{skyi,kernel.json} + sky-ffi/go/<slug>_bindings.go — a gitignored build artifact, regenerated by sky install), and records the dependency under ["go.dependencies"]. For a Sky package it git clones the repo into .skydeps/<slug>/ and records it under [dependencies].

Smart resolution (deterministic, content-based):

1. An undotted import head (net/http, io) is stdlib → Go, no probe.
2. Otherwise the import path is cloned (a Sky package always lives at its repo root). If the clone succeeds and the repo has a [lib] table in its sky.toml → Sky (the cloned tree is kept, no re-fetch). If it has no [lib] (a Sky app, or a src/-less Go repo) the tree is discarded and it falls through to Go. If the clone fails (a Go package subpath like github.com/stripe/stripe-go/v84/customer, or a vanity path like golang.org/x/sync/errgroup, is not a clonable URL) it falls through to Go.
3. Go: go get <path>@<spec> resolves the package (it walks a package path up to its module and handles vanity redirects + major-version subdirs). On success the Go surface is generated.
4. If neither resolves → an actionable error suggesting --go / --sky.

Tie-break: a repo that is both a Go module and a Sky [lib] package resolves to Sky (that is the case the smart default exists for — sky add github.com/org/sky-widgets); pass --go to force the Go surface. A private Sky package whose probe clone fails on auth looks like "not a repo" and falls to Go — use --sky to force it.

Version handling (Go-native):

sky add github.com/google/uuid           # pin-by-default: records the resolved
                                          # version, e.g. "v1.6.0"
sky add github.com/google/uuid@v1.5.0    # pin an exact version / branch / commit
sky add github.com/google/uuid@latest    # explicit float — pulls latest on every
                                          # install/rebuild (a broken latest API
                                          # fails the build, forcing a fix)
sky add github.com/stripe/stripe-go/v84

• Pin-by-default: with no @version, sky add records the exact resolved version — reproducible builds out of the box. Write @latest (or edit sky.toml to "latest") to opt into floating.
• Re-adding upserts: sky add pkg@v2 when pkg is already declared updates the recorded version (the most recent sky add wins), so sky.toml never disagrees with the regenerated surface.
• The spec is passed straight to go get pkg@<spec> — latest, an exact vX.Y.Z, a branch, or a commit SHA. Non-Go semver constraints (>=, ~, ^) are rejected (Go uses MVS, not constraint solving).
• Go bindings return Result Error a, not a Task. The Go call runs where the expression is evaluated, and a Go error, a nil or a recovered panic is Err. This is deliberate: handling the Result at each call site marks where the code leaves Sky's guarantees, so prefer the stdlib where it covers the job. To run a call later, off update, wrap it yourself: Task.lazy (\_ -> Pkg.call args) |> Task.andThen Task.fromResult. The generated sky-ffi/<pkg>.skyi lists each binding with its Result type. See boundary-philosophy.md.

Forcing the kind — sky add --go / sky add --sky:

sky add github.com/anzellai/sky-tailwind              # smart-resolves → Sky
sky add --sky github.com/anzellai/sky-tailwind@v1.2.0 # force Sky, pin a tag/SHA
sky add --go  github.com/some/polyglot-repo           # force Go for a repo that
                                                       # is both a Go module and
                                                       # a Sky [lib] package

--sky trusts the looser src/ marker (you asserted it is a Sky package), so it also accepts a Sky package that predates the [lib] convention. --go skips the clone probe entirely (offline-friendly for a known Go module). A Sky package is git cloned into the gitignored .skydeps/<slug>/ and recorded under [dependencies], with the same version semantics as Go deps (pin-by-default; latest/branch float; exact tag/SHA pin). sky install fetches every declared [dependencies]; sky build is read-only and errors run 'sky install' if a declared Sky dep isn't fetched; sky remove --sky <path> drops the entry and its .skydeps/ tree.

A fetched package is checked as your code. sky check, sky build and sky test parse-check and type-check every module under .skydeps/<slug>/src/ on every build, with the rules your own modules follow, and report an error under the package file (.skydeps/<slug>/src/Evil/Probe.sky:8:5). Three consequences:

• A package gets no Sky.Ffi ([E1011] for Ffi.kernel, Ffi.call, Ffi.callPure, Ffi.callTask, under any qualifier). A package is pure Sky and ships no Go kernel, so it calls the typed stdlib like an application does.
• A package's Go FFI call is typed from the project's pinned surface (sky-ffi/<pkg>.kernel.json) and returns Result Error a, as in your code. sky install does not install a package's Go dependencies; the project declares them.
• A package that does not type-check under this compiler fails the build that uses it, at the package file.

Why every build, and not once per pinned version: a pin fixes the package's text, not the result of checking it. The same text can be checked by a newer compiler, against a newer stdlib or another Go surface, and give a different answer, so a verdict cached under the package's hash would need all of those in its key to be sound. The check is the same pass that runs over your own modules, packages are small, and the go build that follows costs far more, so the build re-checks them rather than trust a cached verdict.

The FFI inspector (sky-ffi-inspect) is embedded in the sky binary and self-provisions into $XDG_CACHE_HOME/sky/tools/ on first use — no separate install required. Cold start costs one go build (~4s); subsequent calls are instant. Content-hashed cache means sky upgrade invalidates the helper automatically.

There are no overrides. This section used to list a probe order — $SKY_FFI_INSPECTOR, then bin/sky-ffi-inspect in the cwd or an ancestor, then the embedded fallback. Neither of the first two is implemented (grep -rn 'SKY_FFI_INSPECTOR\|bin/sky-ffi-inspect' rust/crates --include='*.rs' is empty); ffi::ensure_inspector (rust/crates/ffi/src/inspect.rs:329) goes directly to the source tree and the content-hashed cache. See docs/development.md for what that means for the bin/ copy scripts/build.sh still writes.

Local path dependencies — sky add ./dir:

An argument that starts with ./, ../ or / names a directory on this machine instead of an import path. Nothing is fetched or copied:

sky add ../greet        # has go.mod    → ["go.dependencies"] "example.com/greet" = { path = "../greet" }
sky add ./libs/widgets  # has sky.toml or .sky sources → [dependencies] "widgets" = { path = "./libs/widgets" }

• The directory decides the kind. A go.mod makes it a Go module, recorded under its module path; the build adds require <module> v0.0.0 and replace <module> => <absolute dir> to the generated go.mod on every build (the build rewrites go.mod each time, so the wiring is re-applied from sky.toml, never lost), then runs go get <module>@v0.0.0 so the module's own go line and requirements reach the generated go.mod and go.sum. sky add inspects it for its FFI surface like any Go dependency, and records it in sky.toml only when that succeeds: a module Go cannot load leaves sky.toml unchanged and the error names Go's own message. Its functions return Result Error a. A sky.toml or .sky sources make it a Sky package, recorded under its name (else the directory name); every build loads its modules from its source root. A directory that is both is a Sky package; --go / --sky force the kind.
• A Sky path dependency is checked as your code. Its modules are parse-checked and type-checked by sky check, sky build and sky test, and a diagnostic names the file in the dependency relative to the project (../widgets/src/Widget.sky:8:5). A fetched registry package under .skydeps/ is checked the same way, on every build (see A fetched package is checked as your code above).
• Paths are relative to the project root, not the working directory, and are resolved against it at build time. An absolute argument is stored as given.
• Edits are picked up. A changed function body is compiled by the next build, and sky watch rebuilds when a path dependency's .sky, .go or go.mod files change. When a Go path dependency's exported API changes (a function added, removed or given a new signature), the next sky build / sky check / sky test re-inspects the module and rewrites its sky-ffi/ surface before it compiles, and says so (… changed its exported API → sky-ffi/<name>.* refreshed): a path dependency is your own code, so no sky install is needed. The build compares a fingerprint of the exported declarations (sky-ffi/<name>.pathsig), so a body edit does not re-inspect. A registry dependency keeps its pinned surface.
• Drift is reported. A declared directory that no longer exists stops the build with an error naming the dependency. A Go module whose go.mod now declares a different module path is a build warning. sky doctor warns about a missing directory, and about one outside the repository, which a CI checkout or a deploy that copies only the repository will not have.
• sky remove takes the recorded name or the path. sky install re-inspects a Go path dependency (it changes without a version bump). sky update leaves a path dependency alone and says so.

sky remove [--go|--sky] <pkg>

Drops a dependency. With no flag it routes by which sky.toml section declares the package: a [dependencies] entry (Sky package) removes the [dependencies] line and its .skydeps/<slug>/ tree; a ["go.dependencies"] entry (Go module) removes the line, the generated sky-ffi/<slug>.* surface, and the go.mod require (go mod tidy). The routing is a local section lookup — no probe. --go / --sky force one path.

sky install

Regenerates the FFI surface from the declared dependencies. For each ["go.dependencies"] entry it ensures the go.mod pin, then generates any absent surface and re-inspects each present one. Because sky-ffi/ is a gitignored build artifact (not a committed reproducibility anchor), a present surface that no longer matches a fresh inspection — e.g. after a toolchain or dependency-version change — is simply refreshed in place (reported as refreshed), never a hard failure. All three files (.kernel.json, .skyi, go/*_bindings.go) are compared, and each carries a surface-format stamp: a surface written by a sky with another format (or none) is refreshed and named as such, and sky build warns about it until sky install runs. Unchanged surfaces are left untouched (verified). For each [dependencies] entry it clones any Sky package that is absent or whose pinned ref drifted. Idempotent.

sky update

Re-floats latest/branch-pinned [go.dependencies] to their newest versions and regenerates their surfaces. Exact-pinned deps (vX.Y.Z / commit SHA) are left untouched — bump a pin explicitly with sky add pkg@<newversion>.

sky upgrade

Self-upgrades the sky binary from the latest GitHub release. After a successful upgrade it prints the release notes for every version between your old and new binary, flagging any release with breaking changes or a migration section.

sky upgrade           # upgrade, then print the notes for each version jumped
sky upgrade --notes   # preview the notes for (current, latest] WITHOUT upgrading
sky upgrade --force    # install the latest release even from a dev build

Notes come from the GitHub Release body (mirrored from CHANGELOG.md); the fetch is best-effort and never fails the upgrade.

Automatic update nudge. When you run a sky command interactively and a newer release exists, sky prints a one-line "a new release is available — run sky upgrade" note to stderr. The check is cached (~/.cache/sky/update-check.json, %LOCALAPPDATA%\sky on Windows) and refreshed at most once a day in a detached background process, so it never slows a command or blocks on the network. The nudge itself prints at most once a day. It stays out of your way entirely when output isn't interactive: it's suppressed unless stderr is a TTY (so scripts / CI / pipes never see it), for builds from a source checkout (their sky --version names a commit: sky v0.27.5 (1a2b3c4)), and for lsp / fmt / --version. Set SKY_NO_UPDATE_CHECK=1 to disable it completely.

sky upgrade-claude

Refreshes the cwd's CLAUDE.md from the template embedded in the running sky binary at build time. Useful after sky upgrade — the binary's embedded template moves with new releases (new stdlib APIs, deprecation notes, current limitations) but a project's CLAUDE.md is a snapshot taken at sky init time and won't auto- update.

Behaviour:

• Always overwrites ./CLAUDE.md (the file is AI-context, not hand-edited project source).
• Backs the prior file up to ./CLAUDE.md.bak so an accidental run on a project that customised the file is recoverable.
• Prints a one-line summary including the byte-count delta and the sky version that produced the new template, so you can see at a glance whether the template actually changed.

$ sky upgrade-claude
Refreshed CLAUDE.md (118432 → 132422 bytes, from sky v0.27.0)
  previous version saved as CLAUDE.md.bak

Dev console

sky console [--port N] [--tui]

Runs the bundled Sky Console mini-app standalone. The console is also auto-mounted at /_sky/console inside every Sky.Live and Sky.Http.Server app in dev mode — the standalone form is for ad-hoc inspection when you don't have (or don't want to start) a host app.

sky console                # Sky.Live in the browser on :8025
sky console --port 8030    # different port
sky console --tui          # same UI rendered through Sky.Tui in your terminal

The source lives in sky-bundled/console/ (embedded into the sky binary via Template Haskell). First invocation builds into $XDG_CACHE_HOME/sky/console-<version>/ (~3–10 s); subsequent runs are instant. Cache keys include the version string so sky upgrade auto-invalidates.

Live and TUI variants share the same State.sky + View.sky — only the entry-point module switches between Live.app and Tui.app. Cached binaries are kept side-by-side (app-live / app-tui) so switching backends doesn't trigger a rebuild.

Env flags (full reference in CLAUDE.md):

• SKY_CONSOLE_EMBED=off — opt-out of the auto-mount inside user apps (the standalone CLI still works).
• SKY_DEV_BANNER=off — opt-out of the floating "🔍" Sky Console tab (right edge, vertically centred) without disabling the mount.
• SKY_CONSOLE_URL=https://... — override the banner's href (e.g. to point at a remote shared dashboard).
• ENV=production (or SKY_ENV=… outside {dev, development, local}) — production-mode gate; suppresses console + banner entirely and gates /_sky/metrics behind auth.

Formatting

sky fmt <file>

sky fmt --check <file…> rewrites nothing and exits 1 when a file is not formatted; add --format json for one diagnostic line per such file.

Opinionated, deterministic, no configuration (output is Elm-compatible):

• 4-space indent, no tabs.
• Leading commas for multi-line lists/records.
• Pipelines broken onto new lines.
• Refuses to overwrite if the formatter would lose more than one-third of the source lines (guards against partial-parse deletions).

Editor integration

sky lsp

Starts the Language Server over JSON-RPC / stdio. Used by the Helix and Zed integrations and any LSP-aware editor.

See lsp.md for configuration snippets.

Layout

Sky writes generated artefacts to predictable locations — everything under .skycache/ and sky-out/ is regenerable. Nothing generated lives alongside your source.

project/
    src/                  -- your Sky source
    sky.toml              -- manifest
    .skycache/
        ffi/              -- .skyi signatures + kernel.json registries
        go/               -- generated Go FFI wrappers
        lowered/          -- incremental lowered-module cache
    .skydeps/             -- Sky source deps (if any)
    sky-out/              -- compiled binary + lowered main.go + rt/