Concrete Languages

Directory: quilt/src/langs/

Each language lives in its own subdirectory and contributes (at minimum) a lang.rs implementing Language and optionally a meta.rs implementing MetaLanguage.

Rust (rs) — host + meta

Files: langs/rust/lang.rs, langs/rust/meta.rs (generated), langs/rust/ops.rs

The Rust language is the primary host language. It supports:

• Parsing via the forked tree-sitter-rust (hole placeholder {}).
• Full MetaLanguage implementation generated by bootstrap from mk_meta.rs.quilt.
• runnable via quilt (uses rust-script).

Variadic nodes

"block" and "source_file" have Arity::Variadic. Inside a block quote, each child is emitted with .emit(&mut b_); into an imperative QTermBuilder block:

{
    let mut b_ = tb("block");
    b_.write("{");
    child1.emit(&mut b_);
    child2.emit(&mut b_);
    b_.write("}");
    b_.b()
}

Key operators (Rust meta-language)

Glyph	Expands to	Result
↑x	x.qlift()	A QTerm whose code reconstructs x
↓expr	expr.reduce()	Evaluate expr at generation time via rust-script
⟨N⟩	name("ident")	An identifier node

QLift trait (ops.rs)

QLift is implemented for:

• Arc<QTerm> — recursively builds constructor code.
• str / String — becomes a string_literal node.
• char — becomes a char_literal node.
• All integer types — become integer_literal nodes.

reduce (ops.rs)

QTerm::reduce::<T>() compiles the term via rust-script, runs it, and deserializes the returned value via postcard. The script is given a cargo manifest in its frontmatter that points back to the local quilt crate.

---

Python (py) — host + meta

Files: langs/python/lang.rs, langs/python/meta.rs, langs/python/ops.rs

Python uses the forked tree-sitter-python (hole placeholder __HOLE__). Its MetaLanguage emits Python code targeting the quilt Python runtime (see Python Bindings).

Differences from the Rust meta-language

Aspect	Rust	Python
Builder method	.c(&child)	.c(child) (no &)
Cmd sequences	&[..] Rust slice literal	[..] Python list
Variadic block	{ let mut b_ = tb(..); b_.emit(..); b_.b() }	fluent chain .e(child1).e(child2).b()
Statement-splice	supported (via named b_)	not supported — ground ← is an error

Rust's variadic block is a block expression, so it can bind let mut b_ = tb(..) and let ground statements append to it. Python has no statement-block in expression position, so the block is built as a fluent chain instead — which binds no name, and puts the hole in argument position where a ground for would not even parse. A ground ← is therefore a hard error naming the alternative (PythonMetaLanguage::emit_str, issue #152); it used to expand to emit(b_), referencing a name nothing had bound. A ← at sky depth still defers to the next stage, as always.

Build the sequence with your own builder in ground code and splice the finished term — this needs no accumulator from the expander, and goes through wrap_child's .e(..) chain like any other child:

b = tb("block")
for i, n in enumerate(names):
    if i:
        b.n()          # the separator Rust's ground loop writes as `NL.←`
    b.e(↖print(↙name(n)↘)↗)
body = b.b()
out = ↖def f():
    ↙body↘
↗
print(out.coparse())

def f():
    print(a)
    print(b)

quilt invokes python3 for Python files and sets PYTHONPATH to include the quilt-python directory.

Python operators

Glyph	Expands to
↑(x)	qlift(x) into Python; qlift_html(x) into an HTML quote
⟨N⟩	name("ident")

Python's lift is written prefix (↙↑(x)↘), unlike Rust's postfix x.↑: the spelling is a free function because a qlift method can't hang off builtin ints and strings.

Python also has a LiftTo marker type (Python in lift/mod.rs), so a Rust host can lift values into quoted Python (python↖ … ↙x.↑↘ … ↗): integers, floats, bools, and strings lift to the corresponding literals, and slices/Vecs lift element-wise to list literals.

---

TypeScript (ts) — host + meta

Files: langs/typescript/lang.rs, langs/typescript/meta.rs, langs/typescript/ops.rs

TypeScript uses the forked tree-sitter-typescript (hole placeholder __HOLE__). Its MetaLanguage emits calls into the quilt-wasm runtime — the same builder API as the Python runtime, reached over wasm-bindgen instead of PyO3 — so a .ts.quilt metaprogram runs unchanged in a browser and on the CLI.

TypeScript operators

Glyph	Expands to
↑(x)	qlift(x) into TypeScript; qlift_html(x) into an HTML quote
↓	reduce() (postfix: term.↓ → term.reduce())
←	no spelling — ground emit is an error
⟨T⟩	QTerm
⟨N⟩	name("ident")

Lift is written prefix (↙↑(x)↘), like Python's and for the same reason. Emit has Python's limitation too — a fluent chain with no named accumulator — so a ground ← is the same hard error, pointing at the same alternative (#152). TypeScript could host an accumulator where Python cannot, since an IIFE gives it statements in expression position; the blocker is the runtime half, where WasmBuilder.e consumes rather than mutates its builder and WasmQTerm exposes no emit method.

Reduce on the CLI

↓ needs to do something the runtime cannot do alone: a generated stage's coparse() is often still Quilt source — a program that itself quotes — so reducing it means re-expanding first, and the expander is not part of the runtime crate. Each host solves that differently:

Host	↓ runs the code via	Re-expands with
Rust	rust-script	(compiled in)
Python	exec / eval	shells out to $QUILT
TypeScript	node:vm	shells out to $QUILT

The TypeScript backend lives in quilt-wasm/node/index.mjs, which quilt run binds to the bare quilt specifier (see quilt run). It is the CLI twin of examples/web/quilt-rt.js, which does the same job in the browser by calling an in-page WASI expander instead of a binary. Before #153 only the browser half existed, so ↓ worked in the playground and not on the command line.

Two properties follow from being on Node rather than in a page:

• Block-aware. Evaluation goes through node:vm, whose script completion value is the trailing expression — so a stage may run statements and then end in the value it produces, exactly as quilt-python documents and as a Rust block does. The browser shim, limited to new Function("return (…)"), takes a single expression.
• Really TypeScript. A stage carrying type annotations is stripped (module.stripTypeScriptTypes) before evaluation, so it need not be annotation-free JavaScript.

examples/staged_pow.ts.quilt is the three-stage program this makes runnable; bin/test-ts runs it and the ↓ unit tests.

---

HTML (html) — target only

Files: langs/html/lang.rs, langs/html/mod.rs

HTML is a target-only language: it can appear inside quotes (html↖<p>Hello</p>↗) but is never the ground host and has no MetaLanguage. The Rust or Python host's meta-language drives expansion.

The HTML grammar is based on the forked tree-sitter-html with hole support.

Usage in a *.rs.quilt file:

let frag: Arc<QTerm> = html↖<div class="foo">↙content↘</div>↗;

---

WGSL (wgsl) — target only

Files: langs/wgsl/lang.rs, langs/wgsl/mod.rs

WebGPU Shading Language — used in *.wgsl.rs.quilt files where the extension chain is ["rs", "wgsl"]. Bare quotes inside such a file default to WGSL, while the ground language is Rust.

WGSL is target-only: no MetaLanguage.

Usage in shaders.wgsl.rs.quilt:

// Bare ↖…↗ defaults to WGSL here:
let shader = ↖
    @vertex
    fn vs_main(@builtin(position) pos: vec4<f32>) -> @builtin(position) vec4<f32> {
        return pos;
    }
↗;

---

SQL (sql, mysql, mariadb) — target only

Files: langs/sql/lang.rs, langs/sql/mod.rs

A permissive, multi-dialect SQL grammar (the DerekStride/tree-sitter-sql fork), target-only: no MetaLanguage. Used inside a Rust or Python host, or as the non-ground member of a chain in a *.sql.rs.quilt file.

The reason to quote SQL rather than build a query with format! is what crossing the boundary means. A value spliced with ↑ becomes a literal node, not text — LiftTo<Sql> for str produces one literal token spelled as standard SQL with every ' doubled — so a value cannot close the literal and continue the statement:

let name = "x'; DROP TABLE members; --";
let q = sql↖SELECT id FROM members WHERE org = ↙name.↑↘↗;
// SELECT id FROM members WHERE org = 'x''; DROP TABLE members; --'

examples/sql_query.rs.quilt is the worked version. The escaping is verified rather than asserted: the conformance battery reparses every lifted literal in this grammar, and the property suite (#161) re-runs that over generated strings drawn from an alphabet that includes both ' and \.

Dialects: sql vs mysql

The three names are one grammar under three annotations. The parse is identical; what differs is the string escape, because MySQL and MariaDB in their default sql_mode read a backslash inside '…' as an escape character and the SQL standard does not (#233):

annotation	marker	escapes	correct for
sql	Sql	' → ''	the SQL standard, PostgreSQL with standard_conforming_strings = on (default since 9.1), SQLite, SQL Server
mysql, mariadb	MySql	' → '', \ → \\	MySQL/MariaDB in the default mode

let v = r"C:\path\";
sql↖    … p = ↙v.↑↘↗   // p = 'C:\path\'    ← MySQL sees an unterminated string
mysql↖  … p = ↙v.↑↘↗   // p = 'C:\\path\\'  ← MySQL sees C:\path\

There is no spelling correct in both, which is why the dialect is annotated rather than guessed: doubling the backslash fixes MySQL and silently corrupts the value under the standard, where 'a\\' is two characters. sql is the default because standard/PostgreSQL is the larger target; if you generate for MySQL, say so on the quote.

The two escapers agree on every value that contains no backslash, so this only bites where it matters.

What holds that claim up is a round-trip property, not just a reparse: quilt-conformance/tests/properties.rs models each dialect's own reading of a single-quoted literal (from the dialects' rules, not from the escapers) and asserts it inverse to the escaper over generated strings — plus two negative tests pinning that neither dialect's escaping is safe for the other, so the pair cannot quietly collapse into one.

Two fragment shapes

SQL's program holds statements, so a whole statement parses on its own:

let q = sql↖SELECT * FROM t WHERE id = ↙id.↑↘↗;   // tag: `statement`

A bare expression — the shape a composable predicate takes — has no place in the grammar at all. SqlLanguage::parse_pre retries such a fragment inside SELECT … and strips the wrapper back off, the same technique Lean uses with #check …:

let pred = sql↖org = ↙name.↑↘↗;                   // tag: `binary_expression`
let q = sql↖SELECT id FROM members WHERE ↙pred↘↗;

Gotcha: a statement quote in Rust tail position is emitted, not returned

The expander reads a statement-kinded quote sitting in host statement position as "emit me into the enclosing builder" (the is_stmt_like heuristic in multi.rs). That is what you want inside an emit loop and not what you want from a function that returns a fragment, so bind it first:

fn q() -> Arc<QTerm> {
    let query = sql↖SELECT 1↗;   // `sql↖SELECT 1↗` alone here would emit
    query
}

Gotcha: LiftTo is implemented for str, not for &str

Matching through a reference binds &&str, which method resolution stops at. match *self (or *name) is the fix; the same applies to every target.

Holes

__QUILT_HOLE__ matches this grammar's identifier regex, so holes need no grammar patch — they work in predicate, select-expression, relation-name and IN-list position, and since #221 inside a token too.

Statement position needs the wrapper, because no SQL statement begins with an identifier (#234). parse_pre wraps a hole that stands alone on its line in SELECT …, parses, and strips the wrapper back out, so the hole ends up a direct child of program:

let script = sql↖
    CREATE TABLE members (id INT);
    ↙seed↘;
    ANALYZE members;
↗;

The hole must be alone on its line, apart from a trailing ;. That is deliberately narrower than scanning for separators: a ; inside a string literal is ordinary text in the flat node stream, and a scanner that split on it would wrap holes that are not in statement position at all. Anything the rule declines falls back to the ordinary parse error.

Two consequences worth knowing:

• Mid-script, the source must carry the ; — ↙a↘ SELECT 1; is ill-formed SQL whatever fills the hole, so it stays an error rather than being papered over. program lets only the last statement go unterminated, and a hole there may too.
• Emitting a sequence into statement position works, but the separators are yours to place, exactly as in nix_module.rs.quilt's list: put ; between the emitted statements and let the source's own ; terminate the last one.

sql↖
    SELECT 0;
    ↙{ for (i, s) in stmts.into_iter().enumerate() {
        if i > 0 { sym(";").←; NL.←; }
        s.←;
    } }↘;
↗

---

Zsh (zsh) and Bash (bash) — target and host

Files: langs/shell/mod.rs, langs/shell/meta.rs, langs/shell/ops.rs, langs/zsh/lang.rs, langs/zsh/mod.rs, langs/bash/lang.rs, langs/bash/mod.rs

Shell languages, parsed via the forked tree-sitter-zsh / tree-sitter-bash grammars. They can appear inside quotes (zsh↖…↗, bash↖…↗) and, since issue #151, drive generation themselves. Both also have LiftTo marker types (Zsh, Bash in lift/mod.rs) so Rust values can be lifted into shell fragments.

tree-sitter-zsh is a fork of tree-sitter-bash, so the two dialects share almost all of their node kinds — and used to answer Language::arity from two independently maintained match arms that had drifted: bash claimed for_statement, while_statement, function_definition and nine more kinds that zsh's table omitted despite zsh's grammar defining every one, so an emit into a zsh for body compiled differently from the identical bash one with no diagnostic (issue #150).

Each dialect now derives its own table from its own grammar (bin/gen-arity, issue #202), which fixes that at the source rather than by asking the two to share one hand-written answer: a construct both grammars spell the same way classifies the same way because the grammars agree, and a kind only one grammar defines simply never appears in the other's table. Where the forks genuinely part company the tables part company too — zsh's function_definition is repeat1(field('name', …)), since function a b c { … } defines three functions at once and bash has no such syntax. grammar_tags::bash_and_zsh_agree_on_shared_kinds holds the two to agreement on every shared kind, pinning each real exception with its reason so a new divergence still has to be looked at.

langs/shell/mod.rs remains, but only for the part no grammar rule answers: is_expr_tag, the Quilt-level judgement about which tags name an expression rather than a statement, which both providers still share for the reason #150 gives.

As a host (string-based meta)

ShellMetaLanguage makes a shell drive generation, on the Nix and Lean model: no runtime library, generated code represented as plain double-quoted shell words. A .bash.quilt file therefore expands to an ordinary bash script that, run, prints the generated code — which is what makes the #!/usr/bin/env bash shebang BashLanguage has always declared reachable at last (issue #151, where the two were 🟡 for promising a quilt run that could not work). One implementation serves both dialects, carrying a ShellDialect marker, for the reason the tag tables are shared: they double-quote identically, so two copies would be two things to drift.

#!/usr/bin/env quilt
units=(nginx postgres redis)
for u in "${units[@]}"; do
  echo ↖systemctl enable --now ↙$u↘↗
done

expands to echo "systemctl enable --now $u" inside the same loop, and quilt run prints one systemctl enable --now … line per unit. See examples/shell_host.bash.quilt.

A host unquote splices verbatim — the one place this host departs from the Nix template. Nix wraps its splices in ${…} because a Nix expression carries no sigil of its own; every shell expression that produces a value already carries one ($name, ${arr[0]}, $(cmd), $((1 + 2))), and each interpolates as written inside "…" without word-splitting. Wrapping would be actively wrong: ${$(cmd)} is a syntax error. Two consequences worth knowing: write the unquote body unquoted, since it lands inside the metaprogram's own "…" and adding quotes closes that literal and reopens it (leaving the value unquoted — shell concatenation, which is the one habit this model inverts); and a bare word body splices as literal text, because a word is not an expansion.

Escaping is lift::sh_dquote_escape, shared with the LiftTo<Bash>/LiftTo<Zsh> impls so that a lifted value and the literal text around it — which land in the same generated word — cannot escape two different ways. $, `, " and \ in the generated code are data, so the generated script expands them, not the metaprogram.

Four of the five operator glyphs refuse. An operator spelling is spliced into the ground source and applied prefix to what follows, and a shell has no prefix-applied word operators — juxtaposition is command invocation, and a command is not a word. So:

glyph	why there is no spelling	what to write instead
↑	a shell value is already text; the identity would spell as nothing, making the glyph an invisible no-op	↙…↘
⟨N⟩	same — a name is its own text	↙…↘
←	no b_ accumulator (as Lean, #132) and the shell's join takes its operand inside a substitution, not after a prefix	collect and splice the join: ↙$(printf '%s\n' "${frags[@]}")↘
↓	needs the QTerm runtime no string host ships	compute in ordinary shell, splice with ↙…↘
⟨T⟩	the shell is untyped	drop the annotation

Each fails loudly with that advice rather than leaking a placeholder into a generated script; conformance/spec/bash.toml pins the errors so they stay actionable.

A hole used to have to be a whole word here: __QUILT_HOLE__ lexes as a plain word, and hole detection matched a node whose byte range equalled the hole's, so inside a "…" string, inside a comment, or glued to adjacent text (↙u↘.service is one word) the surrounding token swallowed it and the parse failed. build_nodes now splits that token around the hole instead (issue #221), so all four positions work. The fix is in treesitter.rs, not in either shell grammar — the forks' quilt_hole rule is still parked, since tree-sitter generate panics on it — and being below the grammars it applies to every language at once.

---

Nix (nix) — target and host

Files: langs/nix/lang.rs, langs/nix/meta.rs, langs/nix/ops.rs, langs/nix/mod.rs

The Nix expression language, parsed via the forked tree-sitter-nix grammar. Nix is purely expression-oriented — a whole file is a single expression — so every fragment is an Expr and unquotes splice into expression positions; there are no statements.

The hole token is __QUILT_HOLE__, a plain Nix identifier (so it parses as a variable_expression in any expression position; the range-based hole detection in treesitter.rs recognises it).

As a target

Quote and splice Nix fragments inside another host (nix↖…↗). Nix has a LiftTo marker type (Nix in lift/mod.rs): strings lift to double-quoted string_expressions (with ${ escaped to keep them inert), integers/floats to integer_expression/float_expression, booleans to the true/false builtins, and slices/Vecs to space-separated list_expressions. See examples/nix_module.rs.quilt:

let drv = nix↖
    pkgs.stdenv.mkDerivation {
      pname = ↙pname.↑↘;
      buildInputs = ↙build_inputs↘;
    }
↗;

As a host (string-based meta)

NixMetaLanguage makes Nix drive generation. Unlike the Rust/Python hosts, which emit builder calls into a QTerm runtime, the Nix host has no runtime library: meta.rs/ops.rs represent generated code as plain Nix strings. A quote ↖…↗ becomes a Nix string literal, a host unquote ↙x↘ becomes Nix's own ${x} antiquotation, and ↑ spells toString. So a .nix.quilt file expands to a Nix metaprogram that, evaluated (nix eval), yields the generated code as a string. Static sub-structure is flattened inline, so a literal fragment is one flat string, not a tower of ${"…"}.

The string model is language-agnostic (a Nix host can generate any target), but has no b_ accumulator, so emit is functional rather than imperative. Nix is a pure expression language: there are no statements and nothing to mutate, so "append one term to b_, once around the loop" has no counterpart. Its functional reading does — build the list of fragments with map, then hand the whole list to ←, which joins it into the surrounding container (NixMetaLanguage::emit_str, issue #155):

let
  services = [ "web" "db" "cache" ];
in
  nix↖[ ↙← (map (s: nix↖"↙s↘"↗) services)↘ ]↗

← spells builtins.concatStringsSep "\n" — builtins-only, since this host ships no runtime library — and like ↑/toString it is applied prefix, by juxtaposition: write ← xs, not xs.←. The separator is a newline because it is the only one correct for both container kinds: Nix is whitespace-insensitive, so [ "web"\n"db" ] is the list the source meant, and a line-oriented target (bash, python, …) gets one statement per line rather than a run-on. Two limits follow from the model: joined fragments are not re-indented (the same is already true of any multi-line ↙x↘ splice), and a container whose elements need some other separator — a comma-separated formals, say — wants builtins.concatStringsSep directly, which is exactly what ← partially applies. A ← at sky depth still defers to the next stage, as always. See examples/nix_emit.nix.quilt.

Ground ↓ is still an error — reducing a term needs the QTerm runtime this host doesn't have, so compute the value in ordinary Nix and splice it with ↙…↘. ⟨T⟩ has no spelling either, since Nix is untyped (and ⟨T⟩ is not staged, so this holds inside a quote too); ⟨N⟩ is toString, the identity on a string. See examples/nix_host.nix.quilt:

let
  attr = "enabled";
  package = "hello";
in
  nix↖{
    ↙attr↘ = true;
    default = ↙package↘;
  }↗

expands to the Nix metaprogram let … in "{\n ${attr} = true;\n default = ${package};\n}".

---

Lean (lean, lean4) — target and host

Files: langs/lean/lang.rs, langs/lean/meta.rs, langs/lean/ops.rs, langs/lean/mod.rs

Lean 4, parsed via the forked tree-sitter-lean grammar. Lean's grammar is layered module → command → term, and tactics and do-elements are modeled as ordinary terms inside a by / do body — so one hole rule reaches term, tactic and do-element position.

The hole token is __QUILT_HOLE__, and — as with Nix — the grammar needs no patch at all: it already matches Lean's identifier regex ([a-zA-Z_][a-zA-Z_0-9'!?]*), so it parses as an identifier, hence a _term_atom, in every term, tactic, do-element, declaration-name and binder position. The range-based hole detection in treesitter.rs recognises it by byte range.

A hole at whole-command position (namespace D ↙decl↘ end D) is not directly parseable — no Lean command starts with a bare identifier — so LeanLanguage::parse_pre recovers: it wraps each hole that sits alone on its own line in #check …, the smallest command taking an arbitrary term, and strips the wrapper back out of the parsed tree. Only the wrappers Quilt introduced are removed (holes are counted in tree order), so a #check ↙x↘ the author wrote survives untouched. The recovery is a third fallback, tried only after a plain parse and the bare-term wrapper both fail, so it cannot regress a fragment that already parses.

What remains unavailable is emit (←) into a top-level sequence of commands, which needs a variadic module container that a bare-hole quote does not produce. Emit works into by / do bodies, which are the Variadic containers; for declaration sequences, build the list in the host and join it (as examples/lean_specialize.rs.quilt does). Issue #133 covers the grammar change that would make both direct.

The same limit applies within a declaration: an inductive's constructor list and a structure's field list are variable-length but are not Variadic containers, and neither lean↖| Color.red => 0↗ nor lean↖red : Nat↗ parses standalone — a bare arm or binder is neither a command nor a term. Those lines are assembled host-side too. Variable-length terms have no such problem: fold them, as examples/lean_datatypes.rs.quilt does for its if/else chain and its + chain.

Examples

File	Covers
examples/lean_specialize.rs.quilt	Rust host, Lean target: specialized defs, their simp lemmas, emit into do
examples/lean_do_pipeline.rs.quilt	do-notation — generated <- binds, pure let, emit into a do block
examples/lean_datatypes.rs.quilt	inductive and structure declarations, folded term bodies, theorems whose bound is generation-time data
examples/lean_tactics.rs.quilt	tactic proofs — emit into a by block, proof-script length driven by the schema
examples/lean_host.lean.quilt	Lean as a host (string-based meta)

Each of the target examples prints Lean to stdout; the generated code compiles and its theorems prove under Lean 4 (quilt examples/lean_tactics.rs.quilt > out.lean && lean out.lean).

Because a hole's spelling is the same everywhere it appears, LeanProvider classifies it by its parent (hole_kind): under a by / do body it is a Stmt, directly under module an Item, and anywhere else an Expr.

Lean's module holds commands, not terms, so a bare term fragment (lean↖n + 1↗) would not parse on its own — unlike Rust or Python, whose source_file accepts a bare expression. LeanLanguage therefore retries a failed parse inside #check …, the smallest command taking an arbitrary term, and strips the wrapper back off, which is what makes term-level composition (lean↖↙acc↘ * x↗) work.

As a target

Quote and splice Lean fragments inside another host (lean↖…↗). Lean has a LiftTo marker type (Lean in lift/mod.rs): integers lift to num_lits (negatives as a unary_op, since num_lit is unsigned), floats to scientific_lits, booleans to Lean's true/false constants, strings to str_lits, and slices/Vecs to comma-separated list_lits.

let thm = lean↖theorem add_zero (n : Nat) : n + ↙zero.↑↘ = n := by
  ↙tactic↘↗;

Gotcha: monadic bind is ←, which is also Quilt's emit glyph

Lean spells monadic bind ← — the same character Quilt uses for emit. Inside a quote, a bare ← is consumed by Quilt as an emit operator and never reaches the Lean parser, so the whole do block fails to parse with a stray __QUILT_HOLE__ where the bind was:

// WRONG — the ← below is consumed by Quilt as an emit:
let p = lean↖def m : IO Unit := do
    let x ← IO.getStdout
    pure ()↗;

Error: Parsed with errors: ["def m : IO Unit := do\n", "    let x __QUILT_HOLE__ IO.getStdout\n", …]

Write Lean's ASCII alias <- instead. It means exactly the same thing to Lean, has no meaning to Quilt, and passes through untouched:

let p = lean↖def m : IO Unit := do
    let x <- IO.getStdout
    pure ()↗;

This is what examples/lean_do_pipeline.rs.quilt uses throughout, and it is the recommended spelling for generated monadic Lean — it needs no Quilt knowledge from the reader. (Issue #141 adds \← as an escaped alternative; until it lands, <- is the only spelling that works.)

↑ and ↓ are the same kind of hazard — they are Lean's coercion and lowering notation as well as Quilt's lift and reduce — but those have always been escapable as \↑ and \↓.

Gotcha: a hole cannot go inside a string literal

Lean lexes a whole string literal as one token, so a __QUILT_HOLE__ inside "…" or s!"…" never becomes a node and the splice fails with "Ran out of holes for unquote":

lean↖IO.println s!"↙name↘ -> done"↗   // WRONG: hole inside a string literal

Lift the value into a Lean string and concatenate instead:

lean↖IO.println (↙name.↑↘ ++ " -> done")↗

Lean's own {…} interpolation over a Lean binder is unaffected — that is evaluated at Lean runtime, not a Quilt splice, so s!"total = {total}" inside a quote is fine as long as total is a Lean name.

Splices carry a term, not a precedence level

Application in Lean is left-associative, so splicing an application where an atom is expected silently reassociates:

lean↖IO.println (toString ↙chain↘)↗    // WRONG: toString applied to two arguments
lean↖IO.println (toString (↙chain↘))↗  // right

Parenthesise in the surrounding quote whenever the spliced term may not be atomic.

As a host (string-based meta)

LeanMetaLanguage makes Lean drive generation. Like the Nix host — and unlike the Rust/Python hosts, which emit builder calls into a QTerm runtime — the Lean host has no runtime library: meta.rs/ops.rs represent generated code as plain Lean strings. A quote ↖…↗ becomes an interpolated string literal s!"…", a host unquote ↙x↘ becomes Lean's own {x} interpolation, and ↑ spells toString. So a .lean.quilt file expands to a Lean metaprogram that, evaluated, yields the generated code as a String. Static sub-structure is flattened inline, so a literal fragment is one flat string, not a tower of {s!"…"}.

Braces in the generated code are escaped as \{, which matters constantly in Lean — implicit binders {α : Type}, structure instances, set-builders. A closing } needs no escape.

The string model is language-agnostic (a Lean host can generate any target), but has no b_ accumulator, so emit/splice in ground loops is unsupported — build sequences functionally (List.map, String.intercalate). A ground ← is a hard error saying exactly that (LeanMetaLanguage::emit_str); a ← at sky depth still defers to the next stage, as always. Ground ↓ is likewise an error — reducing a term needs the QTerm runtime this host doesn't have, so compute the value in ordinary Lean and splice it with ↙…↘. The other two glyphs do have spellings: a fragment is a String, so ⟨T⟩ is String and ⟨N⟩ is id. Both are applied by juxtaposition like ↑/toString — write ⟨N⟩ v, not ⟨N⟩(v), which is not application in Lean. See issue #132 for the rationale and the path to a real QTerm runtime for Lean.

def attr := "simp"
def name := "add_zero"
#eval lean↖@[↙attr↘] theorem ↙name↘ (n : Nat) : n + 0 = n := by simp↗

expands to the Lean metaprogram … s!"@[{attr}] theorem {name} (n : Nat) : n + 0 = n := by simp".

---

Text (txt) — target only

Files: langs/text/lang.rs, langs/text/mod.rs, langs/text/meta.rs

Plain text. Useful when you want to quote an arbitrary string fragment without language-specific parsing.

It also has a MetaLanguage — the identity meta. Rust and Python translate a quoted fragment into builder calls, Nix and Lean into string literals; text has no expressions to translate into, so TextMetaLanguage holds the object-level code as unparsed lines: same tags, same cmds, same text. Expanding a text-hosted quote yields the quoted term itself, so ↖…↗ contributes its body, a ground ↙x↘ reads straight through, and a nested quote keeps its glyphs for the next stage. The operator spellings are the other half of that fact: ↑ ↓ ← ⟨T⟩ ⟨N⟩ each need a host expression to expand into, so each is a hard error naming a real host rather than a placeholder leaking into the output.

Text is absent from omni.rs's metas section, so Omni never selects it — the meta is reached by wiring text into a Single/DictMulti by hand, which is what the tests in langs/text/meta.rs do.

---

Bootstrap (bs) — internal only

Files: langs/bootstrap/lang.rs, langs/bootstrap/meta.rs, langs/bootstrap/strlift.rs

The bootstrap language is used exclusively during the self-hosting step that generates langs/rust/meta.rs. It does not use tree-sitter; instead it parses Rust code using the production RustLanguage, then lifts by building strings (strlift.rs) and re-parsing them. This is slower but avoids the chicken-and-egg problem of needing meta.rs to generate meta.rs.

See Bootstrap for details.

---

Feature flags

Each language is gated behind a Cargo feature with the same name (quilt/Cargo.toml):

[features]
default = ["python", "rust", "text", "bootstrap", "wgsl", "html", "zsh", "bash", "sql"]
parse = ["dep:tree-sitter", "dep:tree-sitter-quilt", "dep:tree-sitter-rust", "dep:tree-sitter-python"]
bash  = ["dep:tree-sitter-bash", "parse"]
html  = ["dep:tree-sitter-html", "parse"]
sql   = ["parse"]   # ~42MB of vendored parser.c — see quilt/Cargo.toml
wgsl  = ["dep:tree-sitter-wgsl", "parse"]
zsh   = ["dep:tree-sitter-zsh", "parse"]
python = []
rust   = []
text   = []
bootstrap = ["parse"]

The parse feature gates everything that needs tree-sitter (the Quilt-source parser, the Language providers, Omni, Multi's parse path). With default-features = false the crate is runtime-only (the QTerm builders, qlift, coparse) and builds for wasm32-unknown-unknown — this is how nanobots-codegen consumes it.

The Omni type is built only from features that are enabled, via #[cfg(feature = "…")] gates throughout langs/omni.rs.