Writing SPL

Spindle Lisp (SPL) is the small language zetl reads when you ask it to reason over your vault. This page walks through the syntax by example — no formal grammar, just enough to start writing useful theories.

Requires --features reason at install. See Installation.

Where SPL goes

SPL lives in two places:

Fenced code blocks inside any Markdown file, tagged spl.
Standalone .spl files anywhere in the vault.

# Q2 Release

We're tracking the release of the next minor version here.

```spl
(given core-features-done)
(given docs-drafted)
```

zetl merges every spl block and every .spl file across the vault into one combined theory before reasoning. A fact stated on one page can feed a rule defined on another. This is the point — rules and facts can live next to the prose that motivated them.

Facts

A fact is something you assert to be true. Use (given ...):

(given project-approved)
(given has-owner)
(given budget-signed-off)

One fact per line is conventional. The thing you are asserting (project-approved) is called a literal. Literals are lower-case identifiers with dashes — zetl does not care about the particular word you pick, only that you spell it the same way everywhere.

To state the absence of something, prefix with ~ or write (not ...):

(given (not blocked))

Rules: normally and always

Rules say if the body holds, the head holds. Two flavours:

normally — a defeasible rule. Holds by default, but can be defeated by a stronger rule or a defeater. Produces +d / -d conclusions.
always — a strict rule. Cannot be defeated. Produces +D / -D conclusions.

(given project-approved)
(given has-owner)
(given code-merged)
(given docs-updated)
(given tests-green)
(given qa-signed-off)

; Defeasible: ordinarily true
(normally r-ready-to-start
  (and project-approved has-owner)
  ready-to-start)

; Strict: no exceptions
(always r-complete
  (and code-merged docs-updated tests-green qa-signed-off)
  complete)

The first token after normally/always is the rule’s label — a short name you can refer to later. Labels are optional but helpful: proof trees and conflict reports use them to point back at the exact rule.

The body can be a single literal or an (and ...) of several. An implicit “all of these must hold” binds the conjunction.

Defeaters

A defeater blocks a conclusion without asserting the opposite. Useful for exceptions:

(given open-critical-bug)

(except d-critical-bug
  open-critical-bug
  (not ready-to-ship))

If open-critical-bug is true, any defeasible rule concluding ready-to-ship is blocked. This is how you write “normally yes, except when …” without tangling up your main rules.

Preferences

When two rules compete — one says ready, another says not ready — zetl flags the conflict. To resolve it, declare which rule wins:

(prefer d-critical-bug r-ready-to-start)

Reads: “prefer d-critical-bug over r-ready-to-start”. The critical-bug defeater trumps the normal readiness rule.

Comments

Lines starting with ; are ignored:

; Superiority rules for Q2
(prefer d-critical-bug r-ready-to-start)

SPL has three modal operators that wrap a literal to express permission, obligation, or prohibition:

Operator	Meaning	Example
`(may X)`	X is permitted	`(may (edit ?user ?page))`
`(must X)`	X is obligatory	`(must (review ?document))`
`(forbidden X)`	X is forbidden	`(forbidden (publish ?draft))`

Use them as the head of a rule:

(given signed-contract)

(normally contract-requires-payment
  signed-contract
  (must pay))

They compose with defeasible reasoning — a narrower forbidden rule can defeat a broader may rule via (prefer ...). This is how Access Control expresses policy like “editors can edit research, except in research/private/.”

Learning more

SPL is implemented by spindle-rust, which ships a formal reference: grammar, every keyword, temporal operators, arithmetic constraints, trust-weighted claims. If you’re writing anything non-trivial, open its docs alongside this page.

A realistic vault example

Imagine a project-tracking vault. You have a page per project, plus a theories/ folder with the shared rules.

In projects/Acme Website.md:

# Acme Website

Client: Acme Corp. Owner: Priya. Budget: approved Q1.

```spl
(given acme-approved)
(given acme-has-owner)
(given acme-budget-signed-off)
```

In theories/project-readiness.spl:

; A project is ready to start when approval, ownership, and budget are all in.
(normally r-acme-ready
  (and acme-approved acme-has-owner acme-budget-signed-off)
  acme-ready-to-start)

; Blocker: if the legal review is outstanding, we are not ready regardless.
(except d-acme-legal
  acme-legal-pending
  (not acme-ready-to-start))

Later, in meetings/2026-03-15 Acme Kickoff.md:

Legal flagged a concern about the privacy policy wording.

```spl
(given acme-legal-pending)
```

Run zetl reason status --literal "acme*" and you’ll see acme-ready-to-start go from +d to -d the moment the meeting note is saved. Remove the given once legal clears it, and the conclusion flips back. The rules never moved — only the facts.

A few habits that pay off

Prefix literals by project or theme. acme-approved reads better than approved, and it prevents collisions as the vault grows.
Keep always rules rare. Strict rules are brittle. Save them for genuine invariants.
Name every rule you might want to defeat or prefer. Bare defeasible rules work fine, but labels make conflict reports readable.
Put evergreen rules in .spl files and point-in-time facts inside the page they belong to. Rules are stable; facts come and go.

Backlinks

Linked Pages

What is SPL

Requires --features reason at install time. See Installation.

SPL is Spindle Lisp — a small Lisp-family language for writing rules. zetl extracts SPL from your vault and draws conclusions: “if a project is approved and has an owner, it’s ready to start”. This page is a gentle orientation; see Writing SPL for the syntax reference.

Why a second language at all

Most of your vault is prose — the thing humans are good at reading. But some knowledge is best expressed as a rule, not a paragraph. “Any release candidate must have a green test run and up-to-date docs” is easier to write (and check) as a rule than as a checklist you hope to follow.

SPL lets you write those rules inside your notes, alongside the prose they explain. zetl then reasons over all the SPL in the vault at once — a single combined theory — and tells you what follows.

The shape of SPL

SPL is parenthesised. Facts and rules are S-expressions:

(given docs-updated)
(given tests-pass)

(normally r-ready
  (and docs-updated tests-pass)
  release-candidate)

Reading top to bottom: two facts, then a rule named r-ready that says normally, if both facts hold, conclude release-candidate. Run reasoning and zetl will report +d release-candidate — defeasibly proved.

“Normally” is load-bearing. SPL is a defeasible logic: a conclusion can be drawn by default, and then withdrawn when stronger contrary evidence appears. See What is Defeasible Reasoning for what this means and why it matters for knowledge that isn’t strictly mathematical.

Proof Trees

zetl reason explain <literal> shows why a conclusion holds. The output is a proof tree: the rules that fired, the facts they rested on, and any defeaters that were considered. This page is about when and how to read one.

Requires --features reason at install. See Installation.

What a proof tree is

When zetl concludes that some literal holds (or doesn’t), it found — or failed to find — a chain of rules and facts that lead to that literal. A proof tree is that chain laid out as text:

The root is the literal you asked about.
Each node is a rule that fired, labelled with the rule’s name.
Each leaf is a fact (given) or a dead end (a body literal that couldn’t be proved).
Defeaters that were considered — and either won or were overridden — appear alongside the main chain.

Every node carries provenance: the source file, line number, and page name where that rule or fact was written. You can walk from any conclusion back to the exact prose that originated it.

The command

zetl reason explain "acme-ready-to-start"

By default the output is JSON. Three other formats are available via --as:

`--as`	What you get
`json`	Structured proof tree (default)
`table`	A tabular view of nodes, rules, and sources
`natural`	English prose: “The literal X is defeasibly provable because …”
`dot`	Graphviz DOT source — pipe to `dot -Tpng` for a diagram

There is also --depth N (default 10) which caps how deep the tree goes. Unbounded trees in large vaults can be overwhelming; 4 or 5 is usually enough for day-to-day use.

Running Queries

Once your vault contains some SPL, zetl reason is how you ask questions of it. This page walks the everyday command surface: status, conflicts, export, and provenance.

Requires --features reason at install. See Installation.

`reason status` — the default view

zetl reason status prints every conclusion the combined theory produces, tagged with +D, -D, +d, or -d (see What is Defeasible Reasoning for what those mean).

cd ~/notes
zetl reason status

In a TTY you get a table. Piped or redirected, you get JSON — same data, machine-readable.

Filters

Status output gets long fast. A few flags keep it manageable:

Flag	Shows
`--positive`	Only `+D` and `+d` conclusions
`--negative`	Only `-D` and `-d` conclusions
`--definite`	Only `+D` and `-D` (the strict layer)
`--defeasible`	Only `+d` and `-d` (the soft layer)
`--literal "release*"`	Wildcard filter on the literal name (`*` and `?` supported)

Combine them. “What are all the things my Acme project is currently defeasibly committed to?” becomes:

zetl reason status --positive --defeasible --literal "acme*"

What is Defeasible Reasoning

A short primer on the kind of logic zetl uses when you ask it to reason over your notes. No symbols, no formal notation — just an explanation of why this flavour of logic suits knowledge work.

Requires --features reason at install. See Installation.

Classical logic: everything is final

In classical logic, facts combine and the conclusion is permanent. If you write down that every bird flies, and that Tweety is a bird, then Tweety flies. Forever. Adding new information can only produce new conclusions — it can never retract one you already made.

That rule works beautifully inside a maths textbook. It breaks almost immediately when you try to write down the actual state of a research project, a release plan, or a set of beliefs you formed over six months of reading. Real knowledge is provisional. You revise it. You hedge. You say “normally X, but not when Y”.

Defeasible logic: conclusions have strength

Defeasible reasoning lets you write rules that are normally true but can be defeated by stronger evidence. In a project-tracking vault you might write:

Normally, a release candidate is ready if core features are done, docs are written, and tests pass.
Except when there is an outstanding critical bug.

Both rules live in the theory at the same time. When zetl reasons over them, the defeater wins if its conditions hold — the release is blocked. If the bug is later fixed, the block lifts and the conclusion flips. You never rewrote the rules; you just added and removed facts.

This is exactly how thinking about ongoing work feels. “We’re on track — unless the client pushes back on the design.” “The proposal is done — except we still need a legal review.” You already reason this way. zetl just gives you a notation for it.

Access Control

zetl’s access model has two layers. The built-in layer — three roles plus glob-based page scoping — covers the 90% case: readers, editors, admins, optionally confined to a folder. The optional layer — SPL-based deontic rules — lets you express richer policies (“editor everywhere except billing/**”, “read access only between 9:00 and 17:00”) using the same reasoning engine that powers What is defeasible reasoning.

The three roles

Role	View	Edit	Invite	Admin UI
`reader`	yes	no	no	no
`editor`	yes	yes	no	no
`admin`	yes	yes	yes	yes

A user’s role is set on the invitation that brought them in (see Invitations) and can be changed later from /_admin/users. There’s no implicit hierarchy beyond this table — an editor isn’t a superset of admin, they’re just different.

Page scoping with globs

When you issue an invitation you can restrict which pages the recipient reaches at all:

zetl invite --as Alice --role editor --pages "research/**"

The scope is a glob against vault-relative paths. projects/* matches direct children of projects/. projects/** matches everything recursively. You can pass only one --pages at invite time; for more intricate patterns, use deontic rules below.

Pages outside the scope are invisible — not just uneditable. An out-of-scope page won’t appear in search, won’t show up in the graph, and returns 404 if requested by URL. This is a deliberate minimum-surface choice: users don’t learn about documents they can’t touch.

Deontic rules with SPL

Requires --features reason at install time. See Installation.

Installation

zetl ships prebuilt binaries for Linux, macOS, and Windows. The installer script handles platform detection, download, and wiring up the man page and shell completions. If you prefer to build from source, that path is documented below too.

Prebuilt binaries (recommended)

macOS and Linux:

curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

The script detects your OS and architecture, downloads the right tarball, installs the binary to ~/.local/bin, and generates the man page and shell completions.

Windows:

Download zetl-windows-x86_64.zip from files.anuna.io/zetl/latest, extract zetl.exe, and place it somewhere on your PATH.

Pinning to a specific version

VERSION=0.6.1 curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

Custom install location

INSTALL_DIR=/usr/local/bin curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

Writing SPL

Where SPL goes

Facts

Rules: normally and always

Defeaters

Preferences

Comments

Modal operators

Learning more

A realistic vault example

A few habits that pay off

Related

Backlinks