Documentation

The bindings files

flow init --log WORKLOG.md and library init --kept --scan records --scan WORKLOG.md write the first two files, and with the formal plugin formal init --workspace lean writes the third; they are the schema, with every binding explained where it stands. The kit’s tests hold this page to what each init writes.

flow.toml

# flow.toml — the flow's bindings for THIS project.  Every path is relative to this file's
# directory.  The `flow` skill reads it; the project's own instructions name the log, the
# gates and the rest.

[paths]
records = "records"                 # one file per record: ideas/ tasks/ questions/ findings/ archive/
index = "records/INDEX.md"          # generated by `flow index`; `flow check` fails on drift
archive = "records/archive"         # closed tasks move here at their closing transition
directions = "records/directions.md" # owner-owned: an `## Inbox` slot and `## Directions`
log = "WORKLOG.md"                 # the dated log whose top entry `flow state` prints
# reflow_module = "scripts/reflow.py"   # exports reflow_text(text): one sentence per line; built-in otherwise
# markdownlint_config = ".markdownlint.jsonc"  # a NEW violation after a write reverts it

[prefixes]
idea = "idea"
question = "question"
task = "task"
finding = "finding"
id_width = 4

[hand]
# Active tasks an owner may hold; 0 = unlimited.  `init` made the last owner named here the
# decision owner — the person the owner-only tasks go to, never ranked — but what binds is
# `decision_owners` under [task] below.
agent = 2
owner = 0

[task]
kinds = ["work", "design", "prose", "survey", "upkeep", "community", "decision"]
default_kind = "work"
question_optional_kinds = ["upkeep", "community", "decision"]   # the kinds a task may be minted in with no question
decision_kinds = ["decision"]     # owner-only work: never ranked; a decision gates a landing, never a start
decision_owners = ["owner"]   # a task of a decision kind is minted under this owner's hand; empty for none
[question]
sizes = ["small", "medium", "large"]

[finding]
# The four status roles, named as the project says them: verified needs a declaration of the
# manifest, stated a document's statement or row, empirical a probe, refuted a guard or a probe.
verified = "verified"
stated = "stated"
empirical = "empirical"
refuted = "refuted"
# Findings shard by the document that registers them (records/findings/<paper>/).
shards = []

[evidence]
# A declaration manifest: a text file listing `Module.Path name` per line (a prover library's
# declaration list is the instance); `manifest_roots` are the directories a `Path.ext#name`
# item is looked up under.  Absent, declaration evidence is unchecked and the check says so.
# manifest = ["scripts/decls.txt"]
# manifest_roots = ["src"]
# manifest_extension = "lean"   # required beside manifest: the extension the cited paths carry
# A probes register: a Markdown table whose first column names each self-asserting script.
# probes = "probes/README.md"

[library]
# The reference library, when the project has one: the command that answers `keys`.  Unset, the
# flow asks the library skill installed beside the flow skill, else `library` on PATH, either only
# where a library.toml stands at the root; `command = []` asks none.
# command = ["library"]

[index]
recent_findings = 10
oldest_ideas = 5

library.toml

# library.toml — the reference library's bindings for THIS project.  Every path is relative
# to this file's directory.  The `library` skill reads it.

[paths]
library = "library"                 # cards/<key>.md, one per work; INDEX.md, generated by `library index`
store = "library/.store"            # IGNORED by version control: fetched copies and the derived full-text index
kept = "library/kept"             # TRACKED: copies nothing can fetch again
# reflow_module = "scripts/reflow.py"   # exports reflow_text(text): one sentence per line; built-in otherwise

[card]
kinds = ["article", "book", "chapter", "preprint", "thesis", "report", "document", "web", "repository", "dataset"]

[cite]
# A work is cited by this prefix and its card's key, `lib:jen1990`.  `library cited` and
# `library related` compute the citing sites from these files and directories (*.md under a
# directory) and store nothing.
prefix = "lib:"
scan = ["records", "WORKLOG.md"]

[entries]
# The documents whose `## References` entries are tied to cards; each entry must agree with exactly
# one card.  Empty where the documents cite by key.
documents = []
heading = "References"

[internal]
# A card naming a tracked file of the project (`file`) is an internal document — a report, a survey,
# anything made here or handed in.  Every file under these directories has its card; no bound
# document's reference entry may be tied to one.
kinds = ["report", "document"]
directories = []

[claims]
# The shapes of a sentence that credits a document against a named work, as regular expressions;
# the defaults are generic — a project with a prover adds its own words (`first formalization`,
# `machine-checked`, `in any prover`).
# shapes = []

[copy]
# Prints a PDF's text with a form feed between pages; `{file}` stands for the kept copy.
text_command = ["pdftotext", "-layout", "{file}", "-"]

[find]
limit = 10

formal.toml

Only with the formal plugin, for a project with a Lean workspace (here lean/); /formal:formal-init fills the package roots and the manifest’s command from what formal probe finds.

# formal.toml — the prover side's bindings for THIS project.  Every path is relative to this
# file's directory.  The `formal` plugin's skills read it; the project's own instructions
# name the documents' gates and the rest.

[workspace]
dir = "lean"                 # the prover workspace: the Lake package (or packages) the prover session works in
instructions = "lean/AGENTS.md"   # the prover session's standing rules, read first by the agent whatever its runtime; a template is the handoff skill's references/workspace-instructions.md

[manifest]
# The declaration manifests, one per package, in the row grammar `formal --help` prints;
# `flow` resolves declaration evidence against the same files.  Regenerated by the prover
# session after the last declaration change, with the command below run in the workspace.
files = ["scripts/decls.txt"]
generate = "lake env lean --run DeclManifest.lean --roots <Root> --out ../scripts/decls.txt"

[packages]
# library root = the package directory it sits in, relative to the workspace: `<Root>.lean`
# and `<Root>/` are there.  One line per root.
# Lib = "."

[documents]
# The documents whose cited declaration names (backticked) are read at a landing, as globs
# from the project root.
scan = ["papers/*.md"]

[handoff]
# The project's own directories (its documents, its scripts) a handoff may name: a path into one
# arrives `../`-prefixed, since the prover session runs from the workspace.
root_dirs = ["papers", "docs"]
# Phrases a handoff never carries (material the prover session must not learn of).
banned = []
# The records directory and the id prefixes: a prompt naming a record as a source must carry
# the docstring-register warning, since a docstring renders into the public artifact.
records = "records"
id_prefixes = ["idea", "question", "task", "finding"]