Status: the Rust compiler (
rust/,cargo build --release -p sky) is the primary Sky compiler; the Haskell compiler is preserved underlegacy-haskell-compiler/. Verified by the example sweep + compiler test suite (cargo test+ xtask gates). See../history/compiler/versions.mdfor the changelog.
Every sky subcommand. Run sky --help for the authoritative list.
Compile a Sky source file to a Go binary under sky-out/.
sky build src/Main.skyPipeline:
- Parse
sky.tomlfor[go.dependencies]and[dependencies]. - Auto-regenerate any missing FFI bindings in
.skycache/. - Resolve modules, type-check, lower to Go under
sky-out/. - Invoke
go build→sky-out/app(or thebinname set insky.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/metricssame-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.
--target |
Produces | Notes |
|---|---|---|
web / tablet |
dist/ ready to serve |
serve statically, or same-origin via Server.static "/" "../dist"; tablet == responsive web |
desktop |
sky-out/desktop/<app> (native binary) |
generates a Std.Webview.url shell + builds it (cgo — WKWebView / WebView2 / webkit2gtk) |
ios |
sky-out/ios/build/<App>.app |
generates a SwiftUI + WKWebView shell + builds it for the Simulator (swiftc). Requires full Xcode + the iOS Simulator runtime; missing → warns + exits |
android |
sky-out/android/build/<app>.apk (signed) |
generates a WebView shell + builds a signed APK (aapt2 → javac → d8 → zipalign → apksigner, no Gradle). Requires the Android SDK (ANDROID_HOME / adb) + a JDK; missing → warns + exits |
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
--embedbuild staged is removed. - Where the bundle comes from. The pin is
[database] postgresVersion.sky build --embeduses$SKY_HOME/postgres-bundles/, else re-packs an existingsky db provision --embedcache (no network), else fetches and checksum-verifies the release. A priorsky db provisionis not required. - Cross-compiling.
GOOS/GOARCHselect the target's bundle, soGOOS=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. --embedplus 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.skyWhat 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.
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.
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/androidalso 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 backendThe 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.
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 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:
| File | What |
|---|---|
REPORT.md |
Human-readable summary: stop reason (exit / panic / signal / hang), wall time, goroutine count + a state breakdown, and a |
cpu.pprof |
CPU profile for the whole run — go tool pprof -http=: cpu.pprof for a flame graph. |
heap.pprof |
Heap profile at stop — go tool pprof -http=: heap.pprof. |
goroutines.txt |
Full goroutine stack dump; the top frame of each blocked goroutine is where it's stuck. |
Options:
--profile-dir <dir>— where to write (defaultprofile/, 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 hangsThe 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.
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:
- fmt — every
.skyfile under the source root +tests/is alreadysky fmt-clean. - check — type-checks +
go builds and emits the production binary (sky check≡sky buildminus the artefact, so this one build covers both). - test — every
tests/*.skysuite passes.
sky verify # gate the current project
sky verify path/to/appA 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.
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.
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.
kind |
Fields |
|---|---|
diagnostic |
file: the path relative to the project root (root on the summary), /-separated, or null. range: start / end, each {line, character}, 0-based, character in UTF-16 code units (the LSP Range), or null. severity: error, warning or info. code: the Sky error code (E2001) or null. message. source: sky or go. relatedInformation (only when present): a list of {file, range, message}. suggestion (only when present): the fix hint the text mode prints as Try: …; a v0.27.0 hint ends with its see docs/migration/v0.27.md#… link. half (a Sky.Spa sky build only): frontend or backend, the split project the diagnostic came from. |
test |
sky test only, one per case: suite (the enclosing Test.suite labels joined with >, or the test module's name for a top-level case), name (the case's own name), fullName (as the human output prints it), status (pass or fail), message (on a failure), durationMs (null: Sky.Test runs every case in one pure pass, with no clock between cases). |
summary |
Always exactly one, always the last line: command, ok (the exit code was 0), errors and warnings (the counts of the diagnostic lines above), durationMs, root (the absolute project directory). sky test adds total, passed, failed, skipped (always 0; Sky.Test has no skip) and exitCode. |
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.tomlwarnings (an unknown key, a[database] driverthat 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 buildfailure with nofile.go:line:colline (a toolchain error); sky fmt --check(one error per unformatted file:fileis set,rangeisnull).
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.
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).
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 -> intorString -> Intboth findString.length,String.toIntetc.). - 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.
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.
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:
| Check id | Severity | What it covers |
|---|---|---|
entry-missing |
error | the entry file (default src/Main.sky) exists. A library ([lib] in sky.toml) with no entry has no entry file and is not asked for one |
library-no-modules |
error | a library has at least one .sky module under its source root |
go-toolchain |
error | Go ≥ 1.22 on PATH |
ffi-cache-orphan |
warn | .skycache/ffi/*.skyi with no .skydeps/ source |
missing-lockfile |
info | .skydeps/ populated but no sky.lock |
auth-secret-short / auth-secret-missing |
error / warn | SKY_AUTH_TOKEN_SECRET ≥ 32 bytes when [live] / [auth] set |
ci-parity |
info | .github/workflows/ci.yml invokes sky build / cargo test / verify-*.sh |
stdlib-version-drift |
warn (fixable) | .skycache generated by a different Sky compiler version |
toml-unknown-section |
info | sky.toml top-level keys outside the known set |
subapp-bin-missing |
warn | [subapp] bin = "..." paths are executable |
check-smoke |
info | reminder to run sky check when build is current |
govulncheck-* |
info | flags govulncheck availability for Go-runtime CVE scanning |
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)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 upgraderuns 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_GBto 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
skyversions (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
GOCACHEand 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.
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 verifydoes no scenario-driven HTTP assertion, and this section used to say it did. The removed text described hitting/plus "any routes declared inexamples/<n>/verify.json", checking status codes and body substrings, skipping GUI examples viaSKY_SKIP_GUI=1, printingruntime 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 scriptsreturns nothing from the verify path.Two consequences worth knowing:
- Four committed
verify.jsonfiles are dead inputs.examples/{15-http-server,30-sse-server-demo,32-sse-relay,33-websocket-echo}/verify.jsonare read by nothing.- GUI skipping is not env-gated. It is a hard-coded
skip-guirow inscripts/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.shreadsexamples/<n>/e2e.jsonand honoursexpectStatus(example-e2e.sh:113,:185). That is the behavioural tier indocs/rust-rewrite/11-testing-and-verification.md§1. To get scripted HTTP assertions on an example, write ane2e.json— not averify.json.
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.
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.
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)migraterewritessky.tomland the entry module, then tells you to review withgit diffand runsky check.--dry-runshows the moved / removed / changed key summary and the diff without writing any files.--checkis the CI gate: exit0when no legacy runtime keys remain, non-zero (listing them) when they do.--checkand--dry-runare 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.
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 exitBoth 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 statusexits non-zero on drift (an applied migration whose SQL was edited) — use it as a CI schema-drift gate.sky db migrateexits 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;migratealways applies every pending one.
See Sky.Db — Schema migrations.
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 # create missing tables + add new columns to match your typesThe 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 # 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 resetEMPTIES the data and resets autoincrement counters, but KEEPS the schema and the_sky_migrationsledger. On Postgres it runs oneTRUNCATE … RESTART IDENTITY CASCADE; on SQLite itDELETEs each table and clearssqlite_sequence(foreign-key enforcement is toggled off for the operation). The fast "wipe my dev data, keep the tables" loop.sky db dropremoves 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. UsesDROP 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/-yskips the prompt (scripts, CI, container entrypoints).- On a non-TTY without
--yes, the command refuses rather than guess. - In production (
ENV/SKY_ENVin{production, prod, staging}) it refuses unless--yesis 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.
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 bysky init).rm -rf .skydataresets 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>/), becausesockaddr_uncaps a socket path at ~107 bytes and a deeply nested project overflows it. - Tuned small —
shared_buffers = 32MBagainst 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.jsonis what letssky db ps --allsee 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).
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
SHA256SUMSis 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.tomlas[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 aSHA256SUMSbeside the archive).sky doctor --fixpre-warms the cache for a project with[database] embedded = true.SKY_POSTGRES_BUNDLE_URLpoints 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.
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
CONNECTon its own database andPUBLIC'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 withscram-sha-256on loopback; without it nothing is exposed to the network. - An OS service unit with
--service, generated into<state>/servicewith thesudolines to install it: a systemd unit on Linux, a launchd job plus a shutdown wrapper on macOS. Both stop PostgreSQL withSIGINT(fast shutdown); aSIGTERMmeans smart shutdown, which waits for every client for ever. - A backup timer with
--backup:pg_dump --format=customper 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, asinitdbrefuses. - Re-running
--appis 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-passwordissues 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 initandsky db statusbelong to the migration engine documented above and are unchanged. The cluster verbs arestart/stop/ps/provision.
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, serveWhen 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 bootRun 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); newMaybecolumn → nullable. - dropped column / table / type change → quarantined in a
destructivearray 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 onerenameColumn, 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).
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.
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):
- An undotted import head (
net/http,io) is stdlib → Go, no probe. - 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 itssky.toml→ Sky (the cloned tree is kept, no re-fetch). If it has no[lib](a Sky app, or asrc/-less Go repo) the tree is discarded and it falls through to Go. If the clone fails (a Go package subpath likegithub.com/stripe/stripe-go/v84/customer, or a vanity path likegolang.org/x/sync/errgroup, is not a clonable URL) it falls through to Go. - 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. - 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 addrecords the exact resolved version — reproducible builds out of the box. Write@latest(or editsky.tomlto"latest") to opt into floating. - Re-adding upserts:
sky add pkg@v2whenpkgis already declared updates the recorded version (the most recentsky addwins), sosky.tomlnever disagrees with the regenerated surface. - The spec is passed straight to
go get pkg@<spec>—latest, an exactvX.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 isErr. 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, offupdate, wrap it yourself:Task.lazy (\_ -> Pkg.call args) |> Task.andThen Task.fromResult. The generatedsky-ffi/<pkg>.skyilists each binding with itsResulttype. 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]forFfi.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 returnsResult Error a, as in your code.sky installdoes 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.modmakes it a Go module, recorded under its module path; the build addsrequire <module> v0.0.0andreplace <module> => <absolute dir>to the generatedgo.modon every build (the build rewritesgo.modeach time, so the wiring is re-applied fromsky.toml, never lost), then runsgo get <module>@v0.0.0so the module's owngoline and requirements reach the generatedgo.modandgo.sum.sky addinspects it for its FFI surface like any Go dependency, and records it insky.tomlonly when that succeeds: a module Go cannot load leavessky.tomlunchanged and the error names Go's own message. Its functions returnResult Error a. Asky.tomlor.skysources make it a Sky package, recorded under itsname(else the directory name); every build loads its modules from its source root. A directory that is both is a Sky package;--go/--skyforce the kind. - A Sky path dependency is checked as your code. Its modules are
parse-checked and type-checked by
sky check,sky buildandsky 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 watchrebuilds when a path dependency's.sky,.goorgo.modfiles change. When a Go path dependency's exported API changes (a function added, removed or given a new signature), the nextsky build/sky check/sky testre-inspects the module and rewrites itssky-ffi/surface before it compiles, and says so (… changed its exported API → sky-ffi/<name>.* refreshed): a path dependency is your own code, so nosky installis 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.modnow declares a different module path is a build warning.sky doctorwarns 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 removetakes the recorded name or the path.sky installre-inspects a Go path dependency (it changes without a version bump).sky updateleaves a path dependency alone and says so.
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.
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.
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>.
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 buildNotes 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 dev builds, and for lsp / fmt / --version. Set
SKY_NO_UPDATE_CHECK=1 to disable it completely.
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.bakso an accidental run on a project that customised the file is recoverable. - Prints a one-line summary including the byte-count delta and the
skyversion 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.bakRuns 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 terminalThe 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(orSKY_ENV=…outside{dev, development, local}) — production-mode gate; suppresses console + banner entirely and gates/_sky/metricsbehind auth.
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).
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.
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/