// 本文件提到的 docs/** 指针都指向已收口删除的设计文档（原文在 git 历史里）：要读原文用 git log --all -- <path>。doc-refs: history-only

sokonanoda — learn theorem proving in a Lean-4-style language

Zero setup. Install the extension, open a .sokonanoda file, and the language server and the sokonanoda CLI are already there — they ship inside the extension as platform-specific packages (macOS arm64/x86_64, Linux x64/arm64, Alpine x64/arm64, Windows x64/arm64), so no Rust toolchain, no checkout, and no network download. Every exercise you finish is graded by a complete Lean-4-compatible kernel: if it's green, it's a real proof.

Part of the sokonanoda-lang suite: a self-contained teaching compiler + language server + agent skills.

What you get

Proof checking that doesn't lie

• Real kernel grading — declarations are checked by a full dependent type checker (not text matching or heuristics). Solved exercises show as solved; sorry placeholders are graded as warnings, real mistakes as errors.
• Unfinished lemmas are still usable — like Lean 4's sorryAx, an open exercise enters the environment with its stated type, so later proofs can reference it and keep their goal states; the reference gets a uses-open-exercise warning instead of an unknown identifier error.
• A broken signature is never mistaken for "not done yet" — an exercise's signature is type-checked too, sorry or not: theorem t : 3 := sorry reports kernel-expected-sort on the signature, and a theorem's type must be a Prop (kernel-theorem-not-prop). A typo'd lemma name or a wrong conclusion in a 100-exercise canvas surfaces as a diagnostic instead of a silently "open" exercise.
• Types on hover, with real names — hover any expression (including inside parentheses) for expression : type; partial applications print your actual binder names, definition heads stay folded (Not a, not a -> False). Hovering a name inside a tactic shows the goal state, then that name's own type; hovering a declaration shows its signature and, for a def, the := body too; hovering a #check / #print line shows that command's output. Every piece of .sokonanoda text in a hover is a syntax-coloured fenced block (the same renderer as the goal state and the Infoview cards).
• Honest warnings — a declaration named Prop, Sort or Type still compiles, but those names are already defined by the kernel, so the name can never be used; the editor flags it with a reserved-declaration-name warning. And when the answer is already complete but a leftover sorry line follows it, the editor flags that exact line with a redundant-sorry warning — the declaration stays open, and the fix is to delete the line rather than keep proving.
• Implicit arguments bind the Lean 4 way by default (strict) — a positional argument binds only the explicit parameters of a signature; to feed an implicit position, write @f α x (the error message prints the exact @-form to copy). Since 2026-11-01 this is the default dialect in the editor and on the CLI, and it needs no environment variable. The old reading is the escape hatch: turn sokonanoda.dialect.strictImplicitArgs off (applies without a restart) or pass --dialect loose on the command line.

Guided exercises

• Exercise canvas — sorry marks an exercise. Fill it in, save, and the kernel grades you instantly.
• Goal view — an Explorer tree shows every declaration's status (open / solved / failed), the remaining goal and the hypotheses you have introduced; alt+n / alt+shift+n jump between holes.
• Goals at cursor — with the caret inside a by proof, the same tree shows the goal, the hypotheses in scope and your by progress at that position; click the goal to jump to the tactic.
• Infoview panel — a dockable, syntax-styled goal panel (Lean-Infoview style) in its own container on the right side bar, so it can sit next to your proof: multi-goal columns with each goal's hypotheses (h : A ⊆ B — name, colon, type), by k/n progress, the declaration list (an open declaration also shows its goal as a coloured ⊢ … line, one row per remaining goal), and the live server version. Only the declaration name is clickable (it jumps to the definition; it is plain bold text, not a link, and no source line number is shown); notation symbols and identifiers in goals, hypotheses and types are plain coloured text. Goal and hypothesis text is coloured from the same single source as the editor's semantic highlighting (no separate, drifting rules), and it uses your file's own notation — a goal the kernel prints as Set.subset α A B shows up as A ⊆ B, exactly as you wrote it (binder grouping, Type 0 and line breaks are preserved byte for byte), it reads the same kernel-checked data as the tree, updates only on debounced caret moves (never refetches the declaration list on cursor movement), and falls back to the Explorer tree's 「当前光标处」 group when webviews are unavailable. Open it with Sokonanoda: Infoview (目标面板) (needs VS Code 1.106+).
• Hint ladders — each exercise carries 2–3 progressive hints (-- soko:hint directives); reveal them one at a time when stuck.
• Your own notation — declare infix:50 " ∈ " => Set.mem (or infixl:, infixr:, and the nullary notation "∅" => Set.empty) and write a ∈ A instead of Set.mem α a A. Mathematical symbols are first-class tokens, declared symbols are highlighted as operators, and notation is pure sugar: it emits no event, and the pointful spelling keeps grading identically. Scope is per file, after the declaration (not across import yet). The course standard library's leading type parameters are implicit (Set.image, Set.preimage, Set.mem, Function.comp, Rel.comp, …), so a ∈ A, f '' A, A ⊆ B, A ∩ B need no α β — write the mathematics, not the telescope.
• Multi-file projects — start a file with import Logic and the whole import closure is compiled as one program: declarations from imported modules are in scope for diagnostics, hover, completion and code actions, and go to definition jumps into the imported module. The import line itself is a link — click the module name (lib.Set in import lib.Set) to open that module's file. An optional sokonanoda.toml at the project root names the module root (Logic ↔ Logic.sokonanoda, Lib/And.sokonanoda ↔ Lib.And); without a manifest the entry file's own directory is the root, so two files next to each other just work. Errors are attributed to the file that caused them (import-not-found, import-cycle, …). Editing an imported module re-checks the files that depend on it right away — unsaved edits included — and find references / rename work across the whole project.
• Project tree — an Explorer view (项目) shows the import closure around the active file: the module root and where it came from (a sokonanoda.toml path, or "zero config: the entry file's directory"), every module in topological order with its status — compiled, load-failed (the root cause, e.g. a missing import), or blocked (a victim of another module's failure) — plus per-module declaration/error counts and the project-level diagnostics. Click a module to open it; click the root to open the manifest. The status bar tooltip names the project too, and a single file (no import) says so instead of showing an empty tree. Refresh with the view's refresh button or Sokonanoda: Refresh Project View (刷新项目视图).
• Course map — an 11-unit structured course with verified solutions (propositional logic first; by tactic blocks early for fast feedback; universes only when you naturally ask "what's the type of a function type?"; induction split into two units; relations & connectives in unit 9, reading proofs & synthesis in unit 10, modules & projects in unit 11 — per the locked plan in docs/design/course-syllabus.md §0 and unit 11 in docs/design/imports-and-projects.md).

A real editing experience

• Completions (keywords, in-scope binders, prelude names)
• Go-to-definition, rename and find references — all across imported modules; document highlight stays within the file
• Inlay hints showing the expected type at each hole — and the result of every #check (#check Nat → Nat : Type 0, Lean-Infoview style); #check <def> shows the declaration card instead — type and := <body>, notation-folded, exactly like the Infoview card (#check Set.subset → def Set.subset : ∀ {α : Type}, Set α → Set α → Prop := fun {α : Type 0} (A B : Set α) => ∀ (x : α), x ∈ A → x ∈ B). Only def gets a body (a theorem/axiom/inductive still shows the type only) — this is a deliberate divergence from Lean 4, requested 2026-10-15
• set_option pp.explicit true (a line in the file, Lean-compatible) makes #print / #check <expr> / #reduce show implicit arguments (… := @Iff.refl (@Set.mem α a A)); pp.all true is the sledgehammer. The default is unchanged (implicit arguments hidden)
• Code actions: introduce-and-refine templates, exact suggestions, restart scaffolds — every suggestion is kernel-verified before it's offered
• Semantic highlighting (including sorry), folding ranges, smart select that visualises precedence
• Restart the language server in place (Sokonanoda: Restart Server (重启服务器)) after rebuilding or refreshing the binary — no window reload needed (extension updates themselves still apply on reload)
• Greek binder letters (α, β, …) render plainly — the extension turns VS Code's confusable-character box off for .sokonanoda files by default
• Notation input, the Lean 4 way: type the abbreviation and press Space — \and → ∧, \alpha → α, \in → ∈ , \sub → ⊆ , \powerset → 𝒫 (it also lands as soon as the word is complete, so \alpha becomes α while you type)
• Notation is navigable: hover a notation symbol to see three things — what it expands to (Set.mem), its own signature (Set.mem : forall (α : Type 0), α -> Set α -> Prop), and how to type it; the hover box covers exactly the symbol (so ⁻¹' and ×ˢ are framed correctly). F12 / ctrl+click on a notation symbol jumps to the infix:/prefix:/postfix: line that declared it — across import, into the library module. The built-in symbols (∧ ∨ ↔ ¬ ≠ =) jump to their registration line in the prelude source, and so do the target names inside those comments (And → inductive And, Eq → axiom Eq); targets that live in a course library you have not imported say so in the hover instead of failing silently.
• Hover inside a tactic: the goal state entering that tactic, and — when the cursor is on a name (apply Set.ext, exact h, …) — a divider followed by that name's own type. On numbers, brackets or strings nothing is added, so the goal panel reads exactly as before.
• Every tactic has a page, and the pages ship inside the extension (0.88.0): hover a tactic keyword (intro, exact, rfl, unfold, match, …) and the hover adds a one-line summary plus a plain-text 完整文档：F12. Press F12 there to open that tactic's page — what it does, when to use it, what the kernel checks behind it, the errors you can hit and the way out. All 16 pages plus their index are packaged into the extension (docs/tactics/*.md), so they open offline with no external site. A tactic added later without a page fails the build instead of shipping a broken link.
• The four commands ship too, and their keywords are navigable (2026-10-11): #check, #reduce, #print and set_option each have a page — what it prints, when to reach for it, what the kernel does behind it, the errors and the way out, plus the boundaries (set_option pp.explicit reveals implicit arguments; it only affects command output). Press F12 on the command keyword itself to open that page (#check → check.md); the pages are packaged into the extension (docs/commands/*.md) and open offline. Argument positions keep their own answers — F12 on the name in #check id still jumps to the declaration, and set_option's option/value have no target.
• Compile progress you can see: the status bar switches to a compiling… state, the Infoview shows a three-line progress block, and the overview ruler marks the document being compiled (sokonanoda.progress.throttleMs throttles the in-between refreshes; no fake percentage is shown). It only lights up for compiles that actually take a while (sokonanoda.progress.showDelayMs, default 300 ms) — the server recompiles on every keystroke and a teaching-sized file finishes in about a millisecond, so showing it immediately meant type a letter, flash once
• Readable declarations: the Infoview prints types, := values and ⊢ goals at body size with generous line height (no double-dimming), and sokonanoda.infoview.fontScale scales them to taste
• The Infoview shows the project (0.73.0): manifest path, module root, entry, the module table, the counts and the artifact/compiler line — the same soko/project answer the sidebar tree uses, forwarded as-is (no extra round trip: the CLI's query project touches compiled/*.tmp). A requires mismatch appears as a visible warning block at the top of the section, not a tooltip — that mismatch silently disables the project cache, so every file would otherwise be recompiled from scratch on every open with nothing on screen to explain it.
• The built-in prelude is navigable too: F12 on Or, And, Iff, False, Eq.refl, … opens the prelude source (the same bytes the checker installs, materialized as a real read-only-by-convention file) and lands on the declaration line.

Typing notation (\and → ∧, \alpha → α)

Write the abbreviation and press Space — that is the same gesture as Lean 4: \alpha + Space → α , \a + Space → α , \in + Space → ∈ (a word that is still a prefix of a longer key waits for the separator, so \in is not turned into ∈ before you are done). A completed word lands even earlier — \alpha becomes α as soon as you type the a. Bullet ·: type \. (Lean's punctuation key; alias \centerdot) — the tactic bullet is not a notation symbol, but it is on the same input table.

Logic and set theory first:

Greek letters — the spelled-out name, plus the short keys Lean 4 has (letter rows read lower case · upper case):

The keys are copied key-for-key from Lean 4, so the muscle memory transfers — with one documented exception: Lean 4 has no \Mu (its capital mu is \GM only), so this table accepts both \GM (Lean's key) and \Mu (the spelled-out name the other 23 capitals use); hovering a symbol shows the same information (∈ → "输入：\in（别名 \mem）"), and so does hovering a Greek-letter variable (α → "输入：\alpha（别名 \a）"). Ordinary typing is never touched: a lone \ (the set-difference symbol) is never rewritten, indentation and suggestion acceptance keep working, and a word that is still a prefix of a longer abbreviation waits instead of guessing.

A short key like \a is a prefix of \alpha / \approx / \and, so it waits while you keep typing and lands once the word is closed — that is Lean's own rule, and it is why the short keys are unambiguous. Lean's single-letter keys that point at logic symbols (\v → ∨, \i → ∩, \o → ∘, \r → →) are deliberately not taken: \i giving ∩ while \in gives ∈ would be a trap.

.sokonanoda files do not auto-close brackets (editor.autoClosingBrackets: "never" for this language): the automatic ) collides with the automatic notation replacement — VS Code forgets which ) it inserted once the extension edits the line, so the ) you type is no longer skipped over and the line ends up with an extra bracket (visible in a whole proof: exact h))). Type the closing bracket yourself, or set "[sokonanoda]": { "editor.autoClosingBrackets": "languageDefined" } if you prefer the auto-close and never edit inside a pair.

Two more behaviours worth knowing:

• How a word lands (Lean 4's rule): a separator — Space, punctuation — closes the word and finishes it (\in → ∈ , \sub → ⊆ , \a → α ), and a word that is no longer a prefix of any longer key lands immediately (\alpha → α). While you keep typing letters a prefix waits (\an waits for \and, \in waits for \inter, \a waits for \alpha). Turning sokonanoda.input.eager off disables the automatic replacement (then Tab, which the extension also binds while a \-word is being typed, is the only way to force one).
• Pasting never rewrites — a replacement only fires for a single character typed at the caret, so text you paste (even a full \alpha) stays exactly as pasted. Press Space or Tab after it if you want it turned into a symbol.
• Undo — a replacement is a single edit, so one undo takes it back in one step; with several cursors, each abbreviation is rewritten in that same single edit.

Vim users (VSCodeVim)

\ is also VSCodeVim's leader (vim.leader also defaults to \), and vim takes the key first in NORMAL mode — so a file that opens in NORMAL mode swallows \alpha as a vim command before the extension ever sees it. Change both settings together (that is the same escape hatch Lean 4 offers as lean4.input.leader):

{ "sokonanoda.input.leader": ",", "vim.leader": "," }

Then ,alpha + Space → α — the leader is honoured everywhere (the word before the cursor, the Tab keybinding's when clause, and the "pending word" highlight). Also press i before typing: NORMAL mode never inserts text, whatever the leader is. An empty sokonanoda.input.leader falls back to \.

Two vim-specific traps are handled for you:

• The caret stays right after the symbol. VSCodeVim re-applies its own caret after an extension edit; that used to push the caret past an auto-closed ), so every following keystroke landed one character too far right ((\alpha + Space + x came out as (α) x). The extension now writes the caret itself after a replacement — the same workaround Lean 4's client uses for vim (updateUnchangedSelections).
• Vim's own edits are not "typing". Only a single character inserted at the caret can trigger a replacement, so normal-mode o / p / P / . no longer rewrite a pending abbreviation on a neighbouring line.

Install & use

1. Install this extension from the Marketplace — VS Code picks the package with the server bundled for your platform.
2. Open any .sokonanoda file (or the playground.sokonanoda that ships in the repo — 12 exercises, zero to theorem).
3. That's it. The server binary lives in bin/<platform>/ inside the extension; the client and its bundled kernel are built from the same release, so there is no version drift.

The server is discovered bundled-first by default:

1. the bundled bin/<target>/sokonanoda-lsp[.exe] (repairs a lost executable bit automatically) — the client and its kernel are built from the same release, so there is no version drift;
2. the version-pinned download cache — only used by the fallback package for platforms with no bundled build (e.g. Linux armhf), and always pinned to this extension's own release tag, never latest.

sokonanoda.serverPath / SOKONANODA_LSP_BIN and workspace target/debug|release builds are ignored unless you opt in with the sokonanoda.serverOverride setting (default false). This prevents a stale local build (a common cause of "the server is still 0.26.0" surprises) from silently overriding the bundled server. Use Sokonanoda: Doctor (诊断服务器与版本) any time to see which server is in use, its source (bundled / override / cache), the running vs extension version, and other version-skew issues.

No Lean toolchain. The kernel ships inside the server; on platforms with a bundled package everything works fully offline.

Teaching with AI agents

The sokonanoda-lang repo ships three agent skills that any skill-aware agent (Claude Code, opencode, …) can load:

opencode's startup plugin (.opencode/plugins/sokonanoda.ts) already wires the language server for .sokonanoda files, so opening this repo in opencode gives you kernel-checked diagnostics in the agent's own editor loop. The same --json event stream (sokonanoda --json file, sokonanoda watch) is the integration surface for any tooling you want to build.

The same grading verdict is also available as one JSON object: sokonanoda query <op> (check/state/goals/holes/hints/reduce) answers a single question for agents and scripts — query state answers "what is still missing at this position" without scanning the whole event stream. scripts/soko query … is the harness-neutral form of the same command.

Build and rebuild the compile cache

Sokonanoda: Build (编译项目，预热缓存)（alt+b）在大项目上是分钟级：它编整个项目， 每个文件各编一遍自己那一份 import 闭包（文件之间不共享）。实测 courses/set-theory（35 个文件）约 2.5 分钟（debug CLI、冷热都一样—— 冷热差异取决于项目缓存有没有命中，见 docs/PERF.md）。只想快速看一个文件时 直接打开它即可，不必先 build（要只编一个文件用 CLI： sokonanoda build <file.sokonanoda>）。

The compiler keeps a persistent compile cache (.sokonanoda → compiled report), so the second run of a file — and the first keystroke in a project — are hits instead of full recompiles. Two commands drive it from the editor:

• Sokonanoda: Build (编译项目，预热缓存) (alt+b) — compile the project: the module root the language server reports for the active document (soko/project → root), or the first workspace folder while the server has not answered yet. It is never "just the file you have open" — the CLI compiles exactly what you hand it, so passing the file made a 35-file course report 1 个文件. The result line reports files · compiled · hit · failed. It shows progress while it runs (0.73.0): the CLI's per-file event stream drives the status bar ($(sync~spin) Sokonanoda: 3/13 文件 · lib/Set.sokonanoda), the Infoview's three-line progress block and the overview ruler, and a VS Code progress notification carries a cancel button — cancelling kills the CLI subprocess.
• Sokonanoda: Rebuild (清空编译缓存后重编译) (alt+shift+b) — the same, but first runs sokonanoda rebuild <module root> (0.85.0: the CLI's own rebuild subcommand, one process — it equals clean + build, where clean ≡ build --clean) to drop the cache, i.e. "recompile everything from scratch" (it clears both the global cache and the module root's .sokonanoda/). Project artifacts live in <module root>/.sokonanoda/ — a self-ignoring .gitignore (one line, *) keeps them out of your repository, so there is nothing to configure; add .sokonanoda/ to your own .gitignore only if you want it visible there too (committing the artifacts needs git add -f) — and the language server reads that directory first, so build warms exactly what the editor then opens. Single-file entries still live in the global cache.
• Sokonanoda: Clean Cache (清除编译缓存) — clear the cache and stop: no compile follows. It runs build --clean <module root>, which clears both the global cache and the module root's .sokonanoda/compiled/, and reports the three numbers from the CLI's build.clean event (清掉 N 条缓存（全局 X · 项目 Y）). Use it when you want the next compile to start from scratch but do not want to pay for a rebuild right now. SOKONANODA_NO_PROJECT_ARTIFACTS=1 opts back into the global-only behaviour.

Both write the CLI's JSON Lines events (build.file / build.clean / build.summary) to the sokonanoda build output channel, refresh the exercise/project/course views afterwards (a warm cache changes what they show), and warn — never fail silently — when a file does not compile.

build/rebuild time out after sokonanoda.build.timeoutMs (default 300000 ms; 0 = no limit) — a cold build of a whole course can exceed the default, and the timeout message names the setting so you know where to change it.

• Sokonanoda: Install Command Line (安装命令行) — copy the CLI that ships inside this extension to ~/.local/share/sokonanoda/bin/, so you get a sokonanoda command without downloading anything (no network, no mirror, no cargo). Because it installs the bundled binary, its version is the extension's version by construction — and the command verifies that by running --version and comparing the answer, so a stale build is reported instead of silently installed. On an extension upgrade, a previously installed standalone copy is upgraded automatically from the new VSIX (without one ever having been installed, nothing is installed for you); the PATH line is recognized whether the extension wrote it or you added it yourself.

Warming on open — set sokonanoda.warmCacheOnOpen to true and the extension runs one build over the workspace root in the background when the window activates, so the first unit you open is already a cache hit. Off by default: it costs CPU/IO, and "opening the editor" itself gets slower — the other side of the same complaint. It never steals focus (progress goes to the sokonanoda build channel) and never errors (a failed warm-up just means nothing was pre-built; Sokonanoda: Doctor (诊断服务器与版本) tells you why).

The course map

The 「课程」tree shells out to the sokonanoda CLI (it aggregates all course units — the language server itself tracks several documents but answers one project closure at a time). The CLI ships in the same platform package as the server, so it works out of the box; in a development host without a staged bin/, a workspace target/{debug,release} build is used instead.

Requirements

• VS Code 1.106+ (the Infoview uses an extension-contributed secondary-side-bar container)
• No network needed on platforms with a bundled package; the fallback package for other platforms downloads once (or use sokonanoda.serverPath to point at a local build)

Links

• Repository & docs: github.com/ColorlessBoy/sokonanoda-lang
• Release notes: CHANGELOG

License

Apache-2.0