diff options
Diffstat (limited to '')
| -rw-r--r-- | AGENT.md | 221 | ||||
| -rw-r--r-- | Main.lean | 865 | ||||
| -rw-r--r-- | README.md | 171 |
3 files changed, 729 insertions, 528 deletions
@@ -1,165 +1,208 @@ # Lean-Based Knowledge Base Agent Instructions -You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` command-line tool. Every addition is type-checked by Lean's kernel, ensuring logical consistency. +You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` CLI. Every addition is type-checked by Lean's kernel at `check`/`commit` time. --- -## 1. Key Design Principle: Explicit Domains +## 1. Key Design Principles -Every declaration belongs to a **domain** that you name explicitly using `in <Domain>`. Each domain is stored as a separate `<Domain>.lean` file in the KB root. There is no automatic classification. +**Explicit domains.** Every declaration belongs to a domain you name with `in <Domain>`. Each domain is a `<Domain>.lean` file. Load only the domain(s) you need for a given task. -**Choose domains based on what you want an agent to load together.** For example: -- `Ontology` — base types (`Entity`, `Person`, `Place`, …) that everything else depends on -- `People` — instances, properties, and facts about specific people -- `Geography` — instances and facts about places -- `Finance` — financial formulas and data -- `Physics` — physical constants and laws +**Persistent state.** The KB stores a `--@kb` metadata header before every Lean declaration in each domain file. On startup, `kb` scans all domain files and reconstructs the full declaration list automatically — no state is lost between sessions. -An agent loading only `People` facts into its context window would run: `kb list all of People`. +**Exit codes.** Every command returns exit code `0` on success or `1` on error. Scripts can detect failure without parsing output. --- ## 2. Session Start Protocol -```bash -# Orient yourself: see what domains and declarations exist -kb list all -kb domains stats +State is loaded automatically from domain files on startup. There is no need to re-add anything between sessions. -# Recall declarations in a specific domain -kb list all of Ontology -kb list all of People +```bash +kb status # git status + domain summary +kb domains stats # declaration counts per domain and kind +kb list all # full declaration list ``` --- ## 3. Adding Knowledge -Every `add` command requires `in <Domain>` at the end. - -| Command | Purpose | Example | -|---------|---------|---------| -| `kb add type <n> [extends <Parent>] in <D>` | Declare a type | `kb add type Person extends Entity in Ontology` | -| `kb add instance <n> : <Type> in <D>` | Declare an individual | `kb add instance socrates : Person in People` | -| `kb add prop <n> : <DomType> -> <Range> in <D>` | Declare a property | `kb add prop birthYear : Person -> Nat in People` | -| `kb add rel <n> : <D1> -> <D2> -> Prop in <D>` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` | -| `kb add fact <fact> in <D>` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` | -| `kb add rule <n> : <statement> in <D>` | Add a logical rule | `kb add rule ancestors_transitive : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in Ontology` | -| `kb add def <n> <params> : <Type> := <body> in <D>` | Define a shortcut | `kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance` | +Every `add` command requires `in <Domain>` at the end. Both `→` and `->` are accepted as type arrows. -### Notes +| Command | Example | +|---------|---------| +| `add type <n> [extends <P>] in <D>` | `kb add type Person extends Entity in People` | +| `add instance <n> : <Type> in <D>` | `kb add instance socrates : Person in People` | +| `add prop <n> : <DomType> -> <Range> in <D>` | `kb add prop birthYear : Person -> Nat in People` | +| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | `kb add rel bornIn : Person -> Place -> Prop in People` | +| `add fact <fact> in <D>` | `kb add fact birthYear(socrates) = 470 in People` | +| `add rule <n> : <stmt> in <D>` | `kb add rule anc : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in People` | +| `add def <n> <params> : <Type> := <body> in <D>` | `kb add def ytd (r : Float) : Float := Float.log 2 / r in Finance` | -- Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. -- Fact syntax: `prop(inst) = value` or `rel(inst1, inst2)`. -- Domains are created automatically when first used — no `create domain` step needed. -- Put base types in a shared domain (e.g. `Ontology`) that other domains can depend on. +**Fact syntax:** `prop(inst) = value` or `rel(inst1, inst2)`. --- -## 4. Querying the Knowledge Base +## 4. Reading the Knowledge Base -| Command | Description | Example | -|---------|-------------|---------| -| `kb eval <expr>` | Compute a value | `kb eval "yearsToDouble 0.05"` | -| `kb query <prop>` | Ask if a proposition is provable | `kb query "even (2 + 2)"` | -| `kb list all of <Domain>` | List all declarations in a domain | `kb list all of People` | +| Command | Description | +|---------|-------------| +| `list all [of <Domain>]` | List all declarations, optionally restricted to one domain | +| `list types / instances / props / rels / facts / rules / defs [of <D>]` | Filter by kind | +| `show def <n>` | Print the full Lean source of a declaration | +| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` in Lean | +| `search <text>` | Full-text search across declaration names, Lean source, and domain names | +| `deps <n>` | Show what `<n>` uses (forward) and what uses `<n>` (reverse) | + +### Examples + +```bash +kb get birthYear(socrates) # → 470 +kb get atomicNumber(gold) # → 79 -### Query semantics +kb search socrates # all decls mentioning socrates +kb search "-> Nat" # all props/facts mapping to Nat -- `kb eval` runs Lean's `#eval` on the expression. -- `kb query` attempts to prove the proposition using `decide`, `aesop`, or `simp`. Returns `Yes`, `No`, or `Unknown`. +kb deps birthYear +# Dependencies of [prop] birthYear (People): +# uses: [type] Person (People) +# used by: [fact] fact_birthYear_socrates (People) +``` --- -## 5. Checking Consistency and Committing +## 5. Querying -Add all facts first, then verify and commit in one step: +### Basic query (default tactics: `first | decide | aesop | simp`) ```bash -kb check -kb commit "Added Socrates and basic ontology" +kb query "even (2 + 2)" +# Status: Yes +# Tactic: first | decide | aesop | simp +# Proof: +# theorem _kb_proof : even (2 + 2) := ... ``` -`kb check` rewrites `KnowledgeBase.lean` to import every domain file on disk, injects cross-domain imports where needed, then runs `lake build`. `kb commit` does the same before committing to Git. +### Query with custom tactic script -**Do not check after each individual fact.** Batch your additions, then check once. +```bash +kb query "birthYear socrates = 470" using decide +kb query "∀ n : Nat, n + 0 = n" using simp +kb query "Nat.Prime 17" using native_decide +kb query "x + y = y + x" using ring +``` ---- +Returns: +- `Status: Yes` + proof term — proposition is provable with the given tactics +- `Status: No` + Lean output — a contradiction was found +- `Status: Unknown` + Lean output — tactics ran out without a result -## 6. Example Workflow +### Eval ```bash -# Base ontology (shared types everything else depends on) -kb add type Entity in Ontology -kb add type Person extends Entity in Ontology -kb add type Place extends Entity in Ontology -kb add type City extends Place in Ontology - -# Domain-specific properties and relations -kb add prop birthYear : Person -> Nat in People -kb add rel bornIn : Person -> Place -> Prop in People +kb eval "yearsToDouble 0.07" +kb eval "List.length [1, 2, 3]" +``` -# Instances -kb add instance socrates : Person in People -kb add instance athens : City in People +--- -# Facts -kb add fact birthYear(socrates) = 470 in People -kb add fact bornIn(socrates, athens) in People +## 6. Removing Declarations -# Verify and commit everything at once -kb check -kb commit "Added Socrates and basic person/place ontology" +```bash +kb rm birthYear +# Warning: the following declarations reference 'birthYear': +# [fact] fact_birthYear_socrates (People) +# Consider removing dependents first. +# Removed 'birthYear'. ``` +`rm` is metadata-block aware — it removes the exact `--@kb` block and its Lean source for the named declaration, regardless of how many lines the source spans. + --- -## 7. Removing Declarations +## 7. Verifying and Committing + +Add a batch of declarations, then check and commit once: ```bash -kb rm <name> +kb check +kb commit "Added Socrates and basic ontology" ``` -The tool warns if other declarations depend on the one being removed. Remove dependents first. +`check` syncs cross-domain imports and runs `lake build` to verify the entire KB. `commit` does the same before running `git commit`. **Do not check after every individual addition** — batch your additions and check once. --- -## 8. Reusable Definitions +## 8. Example Workflow ```bash -kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance -kb eval "yearsToDouble 0.05" -kb list defs -kb show def yearsToDouble +# Base types +kb add type Entity in People +kb add type Person extends Entity in People +kb add type Place extends Entity in People +kb add type City extends Place in People + +# Properties and relations +kb add prop birthYear : Person -> Nat in People +kb add rel bornIn : Person -> Place -> Prop in People + +# Instances and facts +kb add instance socrates : Person in People +kb add instance athens : City in People +kb add fact birthYear(socrates) = 470 in People +kb add fact bornIn(socrates, athens) in People + +# Inspect +kb deps birthYear +kb search athens +kb get birthYear(socrates) + +# Query +kb query "birthYear socrates = 470" using decide + +# Verify and persist +kb check +kb commit "Added Socrates and basic person/place ontology" + +# Next session: kb loads all of the above automatically from People.lean ``` --- ## 9. Best Practices -- **Put base types in one domain** (e.g. `Ontology`) so all other domains can import it cleanly. -- **Group by agent-loadable context**: a domain should contain what an agent needs for a specific task. -- **Use meaningful domain names**: `People`, `Physics`, `Finance`, `Geography` — not `Domain1`. -- **Prefer `def` over `axiom` for computed facts** — definitions are safer and evaluable. -- **Run `kb check` once after a batch** of additions, not after each one. -- **Commit with descriptive messages** so the KB history is readable. +- **Batch additions, check once.** `lake build` is slow; don't call `check` after every fact. +- **Use `deps` before `rm`** to understand what will break. +- **Use `search` before `add`** to avoid duplicate declarations. +- **Choose tactics deliberately**: `native_decide` for decidable propositions, `omega` for linear arithmetic, `norm_num` for numeric computations, `ring` for ring equalities. +- **Put base types in a shared domain** so dependent domains can import them cleanly. +- **Use meaningful domain names** matching the planned structure: `People`, `Physics`, `MoneyFinance`, `EarthSciences`, etc. --- ## 10. Session End Protocol ```bash -kb commit "Session summary: what was added" -kb list all # Review final state -kb domains stats # Confirm counts are as expected +kb check # verify everything compiles +kb commit "Session: what was added" # persist to git +kb domains stats # confirm final counts ``` --- -## 11. Need Help? +## 11. Error Handling -```bash -kb help +All errors print a one-line summary and return exit code `1`: + +``` +Error: type 'Person' already exists. +Error: 'birthYear' not found. +Error: unknown command 'add type Person'. + Hint: add commands require `in <Domain>`. Run 'help' for usage. ``` -Lean error messages are forwarded directly. A typical error like `unknown identifier 'Person'` means the type was declared in another domain file that hasn't been imported yet — run `kb check` to sync imports, or check that you added the base type before its dependents. +Check exit codes in scripts: +```bash +kb add type Person in People || echo "Add failed, continuing..." +``` @@ -4,10 +4,6 @@ open Lean IO -------------------------------------------------------------------------------- -- 1. Data structures --- --- Every declaration carries an explicit `domain` chosen by the user. --- Domains are arbitrary identifiers (e.g. "Ontology", "Physics", "Finance"). --- Each domain maps to a single <domain>.lean file in the KB root. -------------------------------------------------------------------------------- inductive KBCommand where @@ -22,8 +18,11 @@ inductive KBCommand where | Remove (name : String) | List (what : String) (filter : Option String) | ShowDef (name : String) + | Get (expr : String) + | Search (query : String) + | Deps (name : String) | Eval (expr : String) - | Query (prop : String) + | Query (prop : String) (tactics : Option String) | Check | Commit (msg : String) | Status @@ -33,154 +32,221 @@ inductive KBCommand where | Exit deriving Repr +/-- A single KB declaration. + Written to disk as a structured metadata comment immediately before the Lean source: + --@kb kind=<k> name=<n> domain=<d> + <lean source line(s)> + This lets the tool reconstruct full state on startup by scanning domain files. -/ structure KBDecl where kind : String -- "type" | "instance" | "prop" | "rel" | "fact" | "rule" | "def" name : String - lean : String -- Lean 4 source text emitted to disk - domain : String -- user-chosen domain stem (becomes <domain>.lean) + lean : String -- Lean 4 source (may be multi-line) + domain : String -- stem of the .lean file (without extension) deriving Repr, Inhabited structure KBState where root : System.FilePath decls : Array KBDecl +/-- Result of a command — drives exit codes in non-interactive use. -/ +structure CmdResult where + ok : Bool -- false → exit code 1 + continue : Bool -- false → user typed 'exit', stop the REPL + +def cmdOk : CmdResult := { ok := true, continue := true } +def cmdErr : CmdResult := { ok := false, continue := true } +def cmdQuit : CmdResult := { ok := true, continue := false } + -------------------------------------------------------------------------------- --- 2. Lean-4-safe utility functions +-- 2. Utility functions -------------------------------------------------------------------------------- -/-- True when `needle` appears anywhere in `haystack`. -/ def strContains (haystack needle : String) : Bool := if needle.isEmpty then true else (haystack.splitOn needle).length > 1 -/-- Remove duplicate strings from a list, keeping first occurrence. -/ def dedupStrings (xs : List String) : List String := xs.foldl (fun acc x => if acc.contains x then acc else acc ++ [x]) [] -/-- ASCII-only lowercase. -/ def strToLower (s : String) : String := s.map fun c => if c.toNat >= 'A'.toNat && c.toNat <= 'Z'.toNat then Char.ofNat (c.toNat + 32) else c +/-- Split on the LAST occurrence of `sep` and return (before, after). -/ +def splitOnLast (s sep : String) : Option (String × String) := + let segs := s.splitOn sep + if segs.length < 2 then none + else some + ((segs.dropLast |> String.intercalate sep).trim, + segs.getLast!.trim) + -------------------------------------------------------------------------------- --- 3. Command parsing +-- 3. Metadata format and persistence -- --- Every `add` command requires an explicit `in <Domain>` suffix that names the --- destination file. Both `→` and `->` are accepted as type arrows. +-- Every declaration on disk is stored as: +-- --@kb kind=<k> name=<n> domain=<d> +-- <lean source line 1> +-- [<lean source line 2> ...] +-- (blank line) -- --- Syntax: --- add type <Name> [extends <Parent>] in <Domain> --- add instance <name> : <Type> in <Domain> --- add prop <name> : <DomType> -> <Range> in <Domain> --- add rel <name> : <D1> -> <D2> -> Prop in <Domain> --- add fact <fact> in <Domain> --- add rule <name> : <statement> in <Domain> --- add def <name> <params> : <T> := <body> in <Domain> +-- Parsing all domain files on startup fully reconstructs KBState.decls. +-------------------------------------------------------------------------------- + +def metaPrefix : String := "--@kb " + +def encodeMetaLine (d : KBDecl) : String := + s!"{metaPrefix}kind={d.kind} name={d.name} domain={d.domain}" + +/-- Parse a "--@kb ..." header. Returns (kind, name, domain) or none. -/ +def parseMetaLine (line : String) : Option (String × String × String) := do + guard (line.startsWith metaPrefix) + let fields := (line.drop metaPrefix.length).splitOn " " + let mut kind := ""; let mut name := ""; let mut domain := "" + for f in fields do + if f.startsWith "kind=" then kind := f.drop "kind=".length + if f.startsWith "name=" then name := f.drop "name=".length + if f.startsWith "domain=" then domain := f.drop "domain=".length + if kind.isEmpty || name.isEmpty || domain.isEmpty then none + else some (kind, name, domain) + +/-- Extract all --@kb-annotated declarations from the text of one domain file. -/ +def parseDomainFile (contents : String) : Array KBDecl := + let lines := contents.splitOn "\n" + let mut decls : Array KBDecl := #[] + let mut i := 0 + while i < lines.length do + match parseMetaLine lines[i]! with + | none => i := i + 1 + | some (kind, name, domain) => + i := i + 1 + let mut leanLines : List String := [] + while i < lines.length && !(lines[i]!.startsWith metaPrefix) do + leanLines := leanLines ++ [lines[i]!] + i := i + 1 + let lean := + (leanLines.reverse.dropWhile String.isEmpty).reverse + |> String.intercalate "\n" + decls := decls.push { kind, name, lean, domain } + decls + +/-- Scan all domain .lean files in `root` and reconstruct the declaration list. -/ +def loadState (root : System.FilePath) : IO (Array KBDecl) := do + let reserved := ["KnowledgeBase", "lakefile", "_kb_tmp"] + let entries ← System.FilePath.readDir root + let stems := entries.toList.filterMap fun e => + let fname := e.fileName + if fname.endsWith ".lean" then + let stem := fname.dropRight ".lean".length + if reserved.contains stem then none else some stem + else none + let mut all : Array KBDecl := #[] + for stem in dedupStrings stems do + let path := root / (stem ++ ".lean") + if ← path.pathExists then + all := all ++ parseDomainFile (← IO.FS.readFile path) + return all + +-------------------------------------------------------------------------------- +-- 4. Command parsing -------------------------------------------------------------------------------- def parseCommand (line : String) : Option KBCommand := - -- Normalise Unicode → so either arrow style works. let normalised := line.trim.replace "→" "->" let parts := normalised.splitOn " " |>.filter (not ∘ String.isEmpty) - let raw := line.trim -- used for suffix-style extraction + let raw := line.trim match parts with - -- ── init ──────────────────────────────────────────────────────────────── | ["init", dir] => some (.Init dir) - -- ── add type ──────────────────────────────────────────────────────────── + -- add type | ["add", "type", name, "in", dom] => some (.AddType name none dom) | ["add", "type", name, "extends", par, "in", dom] => some (.AddType name (some par) dom) - -- ── add instance ──────────────────────────────────────────────────────── + -- add instance | ["add", "instance", name, ":", ty, "in", dom] => some (.AddInstance name ty dom) - -- ── add prop ──────────────────────────────────────────────────────────── + -- add prop | ["add", "prop", name, ":", dt, "->", rng, "in", dom] => some (.AddProp name dt rng dom) - -- ── add rel ───────────────────────────────────────────────────────────── + -- add rel | ["add", "rel", name, ":", d1, "->", d2, "->", "Prop", "in", dom] => some (.AddRel name d1 d2 dom) - -- ── add fact (suffix style: everything between "add fact " and " in <D>") + -- add fact (suffix style — last " in " is the domain separator) | "add" :: "fact" :: _ => - -- Find " in " as a domain separator (last occurrence wins). - let body := raw.drop "add fact ".length - let segs := body.splitOn " in " - if segs.length >= 2 then - let dom := segs.getLast!.trim - -- Rejoin all but the last segment in case the fact itself contains " in " - let fact := (segs.dropLast |> String.intercalate " in ").trim - some (.AddFact fact dom) - else none - -- ── add rule (suffix style) ───────────────────────────────────────────── + match splitOnLast (raw.drop "add fact ".length) " in " with + | some (fact, dom) => some (.AddFact fact dom) + | none => none + -- add rule | "add" :: "rule" :: name :: ":" :: _ => let afterColon := raw.drop ("add rule " ++ name ++ " : ").length - let segs := afterColon.splitOn " in " - if segs.length >= 2 then - let dom := segs.getLast!.trim - let stmt := (segs.dropLast |> String.intercalate " in ").trim - some (.AddRule name stmt dom) - else none - -- ── add def ───────────────────────────────────────────────────────────── - -- Syntax: add def <n> <params> : <type> := <body> in <Domain> + match splitOnLast afterColon " in " with + | some (stmt, dom) => some (.AddRule name stmt dom) + | none => none + -- add def | "add" :: "def" :: name :: _ => - let afterName := raw.drop ("add def " ++ name ++ " ").length - let domSegs := afterName.splitOn " in " - if domSegs.length < 2 then none - else - let dom := domSegs.getLast!.trim - let defBody := (domSegs.dropLast |> String.intercalate " in ").trim - let colonSegs := defBody.splitOn " : " - if colonSegs.length < 2 then none - else - let params := (colonSegs.headD "").trim - let typeBody := (colonSegs.tail |> String.intercalate " : ").trim - let assignSegs := typeBody.splitOn " := " - if assignSegs.length < 2 then none - else - let ty := (assignSegs.headD "").trim - let body := (assignSegs.tail |> String.intercalate " := ").trim - some (.AddDef name params ty body dom) - -- ── other commands (no domain argument) ────────────────────────────────── - | ["rm", name] => some (.Remove name) - | ["list", what] => some (.List what none) - | ["list", what, "of", f] => some (.List what (some f)) - | ["show", "def", name] => some (.ShowDef name) - | "eval" :: _ => some (.Eval (raw.drop "eval ".length)) - | "query" :: _ => some (.Query (raw.drop "query ".length)) - | ["check"] => some .Check - | "commit" :: _ => some (.Commit (raw.drop "commit ".length)) - | ["status"] => some .Status - | ["domains"] => some .Domains - | ["domains", "stats"] => some .DomainsStats - | ["help"] => some .Help - | ["exit"] => some .Exit - | _ => none + let afterName := raw.drop ("add def " ++ name ++ " ").length + match splitOnLast afterName " in " with + | none => none + | some (defBody, dom) => + match splitOnLast defBody " := " with + | none => none + | some (lhs, body) => + match splitOnLast lhs " : " with + | none => none + | some (params, ty) => some (.AddDef name params ty body dom) + -- rm + | ["rm", name] => some (.Remove name) + -- list + | ["list", what] => some (.List what none) + | ["list", what, "of", f] => some (.List what (some f)) + -- show / get / search / deps + | ["show", "def", name] => some (.ShowDef name) + | "get" :: _ => some (.Get (raw.drop "get ".length)) + | "search" :: _ => some (.Search (raw.drop "search ".length)) + | ["deps", name] => some (.Deps name) + -- eval + | "eval" :: _ => some (.Eval (raw.drop "eval ".length)) + -- query [using <tactics>] — split on last " using " + | "query" :: _ => + let body := raw.drop "query ".length + match splitOnLast body " using " with + | some (prop, tacs) => some (.Query prop (some tacs)) + | none => some (.Query body none) + -- build / git + | ["check"] => some .Check + | "commit" :: _ => some (.Commit (raw.drop "commit ".length)) + | ["status"] => some .Status + -- domain info + | ["domains"] => some .Domains + | ["domains", "stats"] => some .DomainsStats + -- meta + | ["help"] => some .Help + | ["exit"] => some .Exit + | _ => none -------------------------------------------------------------------------------- --- 4. File-system helpers +-- 5. File-system helpers -------------------------------------------------------------------------------- def domainPath (root : System.FilePath) (domain : String) : System.FilePath := root / (domain ++ ".lean") -/-- Append `decl` to a domain file, creating it with a module header if new. -/ -def appendToDomain (root : System.FilePath) (domain decl : String) : IO Unit := do - let path := domainPath root domain +/-- Write a declaration to disk: metadata header then Lean source, then blank line. -/ +def appendToDomain (root : System.FilePath) (d : KBDecl) : IO Unit := do + let path := domainPath root d.domain unless (← path.pathExists) do - IO.FS.writeFile path s!"-- Knowledge Base: {domain}\n\n" - let handle ← IO.FS.Handle.mk path .append - handle.putStrLn decl - handle.flush + IO.FS.writeFile path s!"-- Knowledge Base: {d.domain}\n\n" + let h ← IO.FS.Handle.mk path .append + h.putStrLn (encodeMetaLine d) + h.putStrLn d.lean + h.putStrLn "" + h.flush def runProc (cmd : String) (args : Array String) (cwd : Option String := none) : IO (UInt32 × String) := do let child ← IO.Process.spawn { - cmd := cmd - args := args - cwd := cwd - stdout := .piped - stderr := .piped + cmd := cmd; args := args; cwd := cwd + stdout := .piped; stderr := .piped } let stdoutTask ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated let stderrOut ← child.stderr.readToEnd @@ -195,7 +261,7 @@ def runProcPrint (cmd : String) (args : Array String) (cwd : Option String := no return code -------------------------------------------------------------------------------- --- 5. Lean snippet generators +-- 6. Lean snippet generators -------------------------------------------------------------------------------- def genType (name : String) (parent : Option String) : String := @@ -215,190 +281,246 @@ def genProp (name domType range : String) : String := def genRel (name dom1 dom2 : String) : String := s!"opaque {name} : {dom1} → {dom2} → Prop" -/-- Parse a fact string and produce a Lean axiom. - Accepted syntax: - `prop(inst) = value` → `axiom fact_prop_inst : prop inst = value` - `rel(inst1, inst2)` → `axiom fact_rel_inst1_inst2 : rel inst1 inst2` -/ def genFact (fact : String) : String := - let byOpenParen := fact.splitOn "(" - if byOpenParen.length < 2 then - -- No parentheses: bare `lhs = rhs` + let byParen := fact.splitOn "(" + if byParen.length < 2 then let byEq := fact.splitOn "=" if byEq.length >= 2 then let lhs := (byEq.headD "").trim let rhs := (byEq.tail.headD "").trim s!"axiom fact_{lhs} : {lhs} = {rhs}" - else - s!"-- unrecognised fact: {fact}\n-- expected: prop(inst) = val or rel(a, b)" + else s!"-- unrecognised fact: {fact}" else - let funcName := (byOpenParen.headD "").trim - let afterOpen := byOpenParen.tail |> String.intercalate "(" - let byClose := afterOpen.splitOn ")" - let argsStr := (byClose.headD "").trim - let args := argsStr.splitOn "," |>.map String.trim - let tag := args.foldl (· ++ "_" ++ ·) funcName - let argStr := String.intercalate " " args + let funcName := (byParen.headD "").trim + let afterOpen := byParen.tail |> String.intercalate "(" + let byClose := afterOpen.splitOn ")" + let argsStr := (byClose.headD "").trim + let args := argsStr.splitOn "," |>.map String.trim + let tag := args.foldl (· ++ "_" ++ ·) funcName + let argStr := String.intercalate " " args let afterClose := byClose.tail |> String.intercalate ")" - let byEq := afterClose.splitOn "=" + let byEq := afterClose.splitOn "=" if byEq.length >= 2 then - let rhs := (byEq.tail.headD "").trim - s!"axiom fact_{tag} : {funcName} {argStr} = {rhs}" + s!"axiom fact_{tag} : {funcName} {argStr} = {(byEq.tail.headD "").trim}" else s!"axiom fact_{tag} : {funcName} {argStr}" -def genRule (name stmt : String) : String := - s!"axiom {name} : {stmt}" - -def genDef (name params type body : String) : String := +def genRule (name stmt : String) : String := s!"axiom {name} : {stmt}" +def genDef (name params type body : String) : String := s!"def {name} ({params}) : {type} := {body}" -------------------------------------------------------------------------------- --- 6. Duplicate check +-- 7. Duplicate check -------------------------------------------------------------------------------- def isDuplicate (state : KBState) (kind name : String) : Bool := state.decls.any (fun d => d.kind == kind && d.name == name) -------------------------------------------------------------------------------- --- 7. Add handlers (domain is always explicit — no auto-classification) +-- 8. Add handlers -------------------------------------------------------------------------------- def addType (stateRef : IO.Ref KBState) (name : String) (parent : Option String) - (domain : String) : IO Unit := do + (domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "type" name then - println s!"Error: type '{name}' already exists."; return - let lean := genType name parent - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "type", name, lean, domain } } - let ext := parent.map (fun p => s!" (extends {p})") |>.getD "" - println s!"Added type '{name}'{ext} → {domain}.lean" + println s!"Error: type '{name}' already exists."; return cmdErr + let d : KBDecl := { kind := "type", name, lean := genType name parent, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } + println s!"Added type '{name}'{parent.map (" (extends " ++ · ++ ")") |>.getD ""} → {domain}.lean" + return cmdOk -def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO Unit := do +def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "instance" name then - println s!"Error: instance '{name}' already exists."; return - let lean := genInstance name typeName - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "instance", name, lean, domain } } + println s!"Error: instance '{name}' already exists."; return cmdErr + let d : KBDecl := { kind := "instance", name, lean := genInstance name typeName, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } println s!"Added instance '{name} : {typeName}' → {domain}.lean" + return cmdOk -def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO Unit := do +def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "prop" name then - println s!"Error: property '{name}' already exists."; return - let lean := genProp name domType range - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "prop", name, lean, domain } } + println s!"Error: property '{name}' already exists."; return cmdErr + let d : KBDecl := { kind := "prop", name, lean := genProp name domType range, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } println s!"Added property '{name} : {domType} → {range}' → {domain}.lean" + return cmdOk -def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO Unit := do +def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "rel" name then - println s!"Error: relation '{name}' already exists."; return - let lean := genRel name dom1 dom2 - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "rel", name, lean, domain } } + println s!"Error: relation '{name}' already exists."; return cmdErr + let d : KBDecl := { kind := "rel", name, lean := genRel name dom1 dom2, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } println s!"Added relation '{name} : {dom1} → {dom2} → Prop' → {domain}.lean" + return cmdOk -def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO Unit := do +def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO CmdResult := do let state ← stateRef.get - let declName := "fact:" ++ fact - if isDuplicate state "fact" declName then - println s!"Warning: fact already exists: {fact}"; return let lean := genFact fact - appendToDomain state.root domain lean - let newDecl : KBDecl := { kind := "fact", name := declName, lean, domain } - stateRef.modify fun s => { s with decls := s.decls.push newDecl } + -- The canonical name is the axiom name embedded in the generated source. + let axiomName := + if lean.startsWith "axiom " then + (lean.drop "axiom ".length).splitOn " " |>.headD ("fact:" ++ fact) + else "fact:" ++ fact + if isDuplicate state "fact" axiomName then + println s!"Warning: fact '{axiomName}' already exists."; return cmdErr + let d : KBDecl := { kind := "fact", name := axiomName, lean, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } println s!"Added fact: {fact} → {domain}.lean" + return cmdOk -def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO Unit := do +def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "rule" name then - println s!"Error: rule '{name}' already exists."; return - let lean := genRule name stmt - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "rule", name, lean, domain } } + println s!"Error: rule '{name}' already exists."; return cmdErr + let d : KBDecl := { kind := "rule", name, lean := genRule name stmt, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } println s!"Added rule '{name}' → {domain}.lean" + return cmdOk -def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO Unit := do +def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO CmdResult := do let state ← stateRef.get if isDuplicate state "def" name then - println s!"Error: definition '{name}' already exists. Use 'rm {name}' first."; return - let lean := genDef name params type body - appendToDomain state.root domain lean - stateRef.modify fun s => { s with decls := s.decls.push { kind := "def", name, lean, domain } } - println s!"Added definition '{name} ({params}) : {type} := {body}' → {domain}.lean" + println s!"Error: definition '{name}' already exists. Use 'rm {name}' first."; return cmdErr + let d : KBDecl := { kind := "def", name, lean := genDef name params type body, domain } + appendToDomain state.root d + stateRef.modify fun s => { s with decls := s.decls.push d } + println s!"Added definition '{name}' → {domain}.lean" + return cmdOk -------------------------------------------------------------------------------- --- 8. Remove handler +-- 9. Remove — metadata-block aware +-- +-- Rewrites the domain file, skipping the entire --@kb block for the named decl. +-- This is atomic and correct regardless of how many lines the Lean source spans. -------------------------------------------------------------------------------- -def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO Unit := do +def rewriteFileRemovingDecl (path : System.FilePath) (target : String) : IO Unit := do + if !(← path.pathExists) then return + let lines := (← IO.FS.readFile path).splitOn "\n" + let mut kept : List String := [] + let mut i := 0 + while i < lines.length do + match parseMetaLine lines[i]! with + | some (_, mname, _) => + if mname == target then + -- Skip this metadata line and all following non-metadata content. + i := i + 1 + while i < lines.length && !(lines[i]!.startsWith metaPrefix) do + i := i + 1 + -- Skip exactly one trailing blank line if present. + if i < lines.length && lines[i]!.isEmpty then i := i + 1 + else + kept := kept ++ [lines[i]!] + i := i + 1 + | none => + kept := kept ++ [lines[i]!] + i := i + 1 + IO.FS.writeFile path (String.intercalate "\n" kept) + +def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := do let state ← stateRef.get let targets := state.decls.filter (fun d => d.name == name) if targets.isEmpty then - println s!"Error: '{name}' not found."; return + println s!"Error: '{name}' not found."; return cmdErr let dependents := state.decls.filter (fun d => d.name != name && strContains d.lean name) unless dependents.isEmpty do - println s!"Warning: these declarations reference '{name}':" - for dep in dependents do - println s!" [{dep.kind}] {dep.name}" - println "Remove dependents first for a consistent KB." + println s!"Warning: the following declarations reference '{name}':" + for dep in dependents do println s!" [{dep.kind}] {dep.name} ({dep.domain})" + println " Consider removing dependents first." + for domain in dedupStrings (targets.map (·.domain)).toList do + let _ ← rewriteFileRemovingDecl (domainPath state.root domain) name stateRef.modify fun s => { s with decls := s.decls.filter (fun d => d.name != name) } - let domains := dedupStrings (targets.map (·.domain)).toList - for domain in domains do - let path := domainPath state.root domain - if ← path.pathExists then - let contents ← IO.FS.readFile path - let kept := contents.splitOn "\n" |>.filter (fun l => !strContains l name) - IO.FS.writeFile path (String.intercalate "\n" kept) println s!"Removed '{name}'." + return cmdOk -------------------------------------------------------------------------------- --- 9. List / ShowDef +-- 10. List / ShowDef / Search / Deps / Get -------------------------------------------------------------------------------- def normKind (w : String) : String := - if w == "types" then "type" - else if w == "instances" then "instance" - else if w == "props" then "prop" - else if w == "rels" then "rel" - else if w == "facts" then "fact" - else if w == "rules" then "rule" - else if w == "defs" then "def" - else w + match w with + | "types" => "type" | "instances" => "instance" | "props" => "prop" + | "rels" => "rel" | "facts" => "fact" | "rules" => "rule" + | "defs" => "def" | _ => w -def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String) : IO Unit := do +def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String) + : IO CmdResult := do let state ← stateRef.get let nk := normKind what - let matchKind : KBDecl → Bool := + let matchKind : KBDecl → Bool := if nk == "all" then fun _ => true else fun d => d.kind == nk let matchFilter : KBDecl → Bool := match filter with | none => fun _ => true | some f => let fl := strToLower f - fun d => - strContains (strToLower d.name) fl || - strContains (strToLower d.domain) fl || - strContains (strToLower d.lean) fl + fun d => strContains (strToLower d.name) fl || + strContains (strToLower d.domain) fl || + strContains (strToLower d.lean) fl let hits := state.decls.filter (fun d => matchKind d && matchFilter d) if hits.isEmpty then println s!"(no {what} found)" - else for d in hits do - println s!"[{d.kind}] {d.name} ({d.domain})" + else for d in hits do println s!"[{d.kind}] {d.name} ({d.domain})" + return cmdOk -def showDef (stateRef : IO.Ref KBState) (name : String) : IO Unit := do +def showDef (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := do let state ← stateRef.get let hits := state.decls.filter (fun d => d.name == name) - if hits.isEmpty then println s!"'{name}' not found." - else for d in hits do + if hits.isEmpty then println s!"Error: '{name}' not found."; return cmdErr + for d in hits do println s!"-- [{d.kind}] {d.name} (domain: {d.domain})" println d.lean + return cmdOk + +def searchDecls (stateRef : IO.Ref KBState) (query : String) : IO CmdResult := do + let state ← stateRef.get + let q := strToLower query + let hits := state.decls.filter fun d => + strContains (strToLower d.name) q || + strContains (strToLower d.lean) q || + strContains (strToLower d.domain) q + if hits.isEmpty then + println s!"No results for '{query}'." + else do + println s!"{hits.size} result(s) for '{query}':" + for d in hits do + println s!" [{d.kind}] {d.name} ({d.domain})" + for l in d.lean.splitOn "\n" do + if strContains (strToLower l) q then println s!" {l.trim}" + return cmdOk + +def showDeps (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := do + let state ← stateRef.get + match state.decls.find? (fun d => d.name == name) with + | none => println s!"Error: '{name}' not found."; return cmdErr + | some d => + let forward := state.decls.filter fun o => + o.name != name && strContains d.lean o.name + let reverse := state.decls.filter fun o => + o.name != name && strContains o.lean name + println s!"Dependencies of [{d.kind}] {name} ({d.domain}):" + if forward.isEmpty then println " uses: (none)" + else do + println " uses:" + for dep in forward do println s!" [{dep.kind}] {dep.name} ({dep.domain})" + if reverse.isEmpty then println " used by: (none)" + else do + println " used by:" + for dep in reverse do println s!" [{dep.kind}] {dep.name} ({dep.domain})" + return cmdOk -------------------------------------------------------------------------------- --- 10. Eval / Query +-- 11. Eval / Get / Query -------------------------------------------------------------------------------- def buildImports (state : KBState) : IO String := do @@ -411,272 +533,289 @@ def buildImports (state : KBState) : IO String := do def runLeanSnippet (state : KBState) (snippet : String) : IO (UInt32 × String) := do let imports ← buildImports state - let tmpPath : System.FilePath := state.root / "_kb_tmp.lean" - IO.FS.writeFile tmpPath (imports ++ "\n" ++ snippet ++ "\n") - let result ← runProc "lean" #[tmpPath.toString] (some state.root.toString) - try IO.FS.removeFile tmpPath catch _ => pure () + let tmp := state.root / "_kb_tmp.lean" + IO.FS.writeFile tmp (imports ++ "\n" ++ snippet ++ "\n") + let result ← runProc "lean" #[tmp.toString] (some state.root.toString) + try IO.FS.removeFile tmp catch _ => pure () return result -def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO Unit := do +def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO CmdResult := do let state ← stateRef.get let (code, out) ← runLeanSnippet state s!"#eval {expr}" - if code == 0 then println out - else do - println s!"Lean error evaluating `{expr}`:" - println out + if code == 0 then println out.trim; return cmdOk + else do println s!"Lean error evaluating '{expr}':\n{out.trim}"; return cmdErr -def queryProp (stateRef : IO.Ref KBState) (prop : String) : IO Unit := do +/-- `get <prop>(<inst>)` — evaluate a property applied to an instance. + Parses "prop(inst1, inst2)" → `#eval prop inst1 inst2`. -/ +def getVal (stateRef : IO.Ref KBState) (expr : String) : IO CmdResult := do let state ← stateRef.get - let snippet := - "set_option maxHeartbeats 4000 in\n" ++ - s!"#check (by first | decide | aesop | simp : {prop})" - let (code, out) ← runLeanSnippet state snippet + let evalStr := + let byParen := expr.splitOn "(" + if byParen.length >= 2 then + let func := (byParen.headD "").trim + let args := ((byParen.tail |> String.intercalate "(").splitOn ")").headD "" |>.trim + let argList := args.splitOn "," |>.map String.trim |> String.intercalate " " + s!"{func} {argList}" + else expr + let (code, out) ← runLeanSnippet state s!"#eval {evalStr}" + if code == 0 then println out.trim; return cmdOk + else do println s!"Error evaluating '{expr}':\n{out.trim}"; return cmdErr + +/-- Enhanced query with optional user-supplied tactic and proof term output. + Syntax: query <prop> [using <tactic-script>] + Default tactics: first | decide | aesop | simp + On success: prints "Status: Yes" and the proof term via #print. + On failure: prints "Status: No" or "Status: Unknown" with the Lean error. -/ +def queryProp (stateRef : IO.Ref KBState) (prop : String) (tactics : Option String) + : IO CmdResult := do + let state ← stateRef.get + let tacs := tactics.getD "first | decide | aesop | simp" + let pname := "_kb_proof" + let thm := s!"set_option maxHeartbeats 8000 in\ntheorem {pname} : {prop} := by {tacs}" + let (code, out) ← runLeanSnippet state thm if code == 0 then - println "Yes (provable)" - else if strContains out "false" || strContains out "False" then - println "No (contradiction found)" + -- Also fetch the proof term. + let (_, printOut) ← runLeanSnippet state (thm ++ s!"\n#print {pname}") + println s!"Status: Yes" + println s!"Tactic: {tacs}" + let proofLine := printOut.trim + unless proofLine.isEmpty do println s!"Proof:\n{proofLine}" + return cmdOk + else if strContains out "false" || strContains out "False" || + strContains out "contradiction" then do + println s!"Status: No" + println s!"Tactic: {tacs}" + println s!"Lean output:\n{out.trim}" + return cmdErr else do - println "Unknown (could not prove or disprove with decide / aesop / simp)" - unless out.isEmpty do println out + println s!"Status: Unknown" + println s!"Tactic: {tacs}" + println s!"Lean output:\n{out.trim}" + return cmdErr -------------------------------------------------------------------------------- --- 11. Build / commit / status --- --- syncRootModule rewrites KnowledgeBase.lean to import every domain file that --- currently exists on disk, then injects `import <base>` into any domain file --- that references names from another domain file it knows about. --- This ensures `lake build` compiles the entire KB, not just the root stub. +-- 12. Build / Commit / Status -------------------------------------------------------------------------------- -/-- Collect all domain stems that have a .lean file in the KB root. -/ def existingDomains (root : System.FilePath) : IO (List String) := do let reserved := ["KnowledgeBase", "lakefile", "_kb_tmp"] - let entries ← System.FilePath.readDir root - let stems := entries.toList.filterMap fun e => - let name := e.fileName - if name.endsWith ".lean" then - let stem := name.dropRight ".lean".length + let entries ← System.FilePath.readDir root + return dedupStrings <| entries.toList.filterMap fun e => + let fname := e.fileName + if fname.endsWith ".lean" then + let stem := fname.dropRight ".lean".length if reserved.contains stem then none else some stem else none - return dedupStrings stems -/-- Rewrite KnowledgeBase.lean to import all existing domain files. - Also prepend cross-domain imports into domain files that need them, - based on which domains are known to this session. -/ def syncRootModule (root : System.FilePath) (state : KBState) : IO Unit := do let allDomains ← existingDomains root - -- Build a mapping: domain → set of other domains it directly references. - -- A domain file references another if any of the *other* domain's declared - -- names appear in its own declaration texts. for domain in allDomains do - let ownDecls := state.decls.filter (fun d => d.domain == domain) - let otherDomains := allDomains.filter (· != domain) + let ownDecls := state.decls.filter (fun d => d.domain == domain) + let others := allDomains.filter (· != domain) let mut needed : List String := [] - for other in otherDomains do + for other in others do let otherDecls := state.decls.filter (fun d => d.domain == other) - -- Does any own decl's lean text mention a name from `other`? - let referenced := ownDecls.any fun od => - otherDecls.any fun od2 => strContains od.lean od2.name - if referenced then needed := needed ++ [other] - -- Inject missing imports at the top of the domain file. + if ownDecls.any fun od => otherDecls.any fun od2 => strContains od.lean od2.name then + needed := needed ++ [other] if !needed.isEmpty then let path := domainPath root domain if ← path.pathExists then let contents ← IO.FS.readFile path let missing := needed.filter (fun imp => !strContains contents s!"import {imp}") unless missing.isEmpty do - let newHeader := (missing.map (fun imp => s!"import {imp}")).foldl - (· ++ "\n" ++ ·) "" - IO.FS.writeFile path (newHeader ++ "\n" ++ contents) - -- Rewrite the root module. - let mut rootContent := "-- KnowledgeBase root module (auto-generated by kb)\n\n" - for stem in allDomains do - rootContent := rootContent ++ s!"import {stem}\n" - IO.FS.writeFile (root / "KnowledgeBase.lean") rootContent + let header := missing.map (fun imp => s!"import {imp}") |> String.intercalate "\n" + IO.FS.writeFile path (header ++ "\n\n" ++ contents) + let mut root' := "-- KnowledgeBase root module (auto-generated)\n\n" + for stem in allDomains do root' := root' ++ s!"import {stem}\n" + IO.FS.writeFile (root / "KnowledgeBase.lean") root' -def checkKB (stateRef : IO.Ref KBState) : IO Unit := do +def checkKB (stateRef : IO.Ref KBState) : IO CmdResult := do let state ← stateRef.get syncRootModule state.root state println "Running `lake build`…" let code ← runProcPrint "lake" #["build"] (some state.root.toString) - println (if code == 0 then "✓ Consistent (build succeeded)." - else "✗ Build failed — see errors above.") + if code == 0 then println "✓ Consistent (build succeeded)."; return cmdOk + else do println "✗ Build failed — see errors above."; return cmdErr -def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO Unit := do +def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO CmdResult := do let state ← stateRef.get let dir := state.root.toString syncRootModule state.root state println "Verifying before commit…" let buildCode ← runProcPrint "lake" #["build"] (some dir) if buildCode != 0 then - println "Commit aborted: build failed. Fix errors and retry."; return + println "Commit aborted: build failed."; return cmdErr let _ ← runProcPrint "git" #["add", "."] (some dir) let code ← runProcPrint "git" #["commit", "-m", msg] (some dir) - if code == 0 then println s!"Committed: \"{msg}\"" - else println "(Nothing new to commit — working tree clean.)" + if code == 0 then println s!"Committed: \"{msg}\""; return cmdOk + else do println "(Nothing to commit — working tree clean.)"; return cmdOk -def showStatus (stateRef : IO.Ref KBState) : IO Unit := do +def showStatus (stateRef : IO.Ref KBState) : IO CmdResult := do let state ← stateRef.get - let dir := state.root.toString println "=== git status ===" - let _ ← runProcPrint "git" #["status", "--short"] (some dir) - println "\n=== session summary ===" - println s!" KB root : {state.root}" - println s!" decls : {state.decls.size} declaration(s) in memory this session" + let _ ← runProcPrint "git" #["status", "--short"] (some state.root.toString) + println "\n=== knowledge base ===" + println s!" root : {state.root}" + println s!" decls : {state.decls.size} loaded" + let domains := dedupStrings (state.decls.map (·.domain)).toList + for dom in domains do + let n := (state.decls.filter (fun d => d.domain == dom)).size + println s!" {dom}: {n}" + return cmdOk -------------------------------------------------------------------------------- --- 12. Init +-- 13. Init -------------------------------------------------------------------------------- -def initKB (dir : String) : IO Unit := do +def initKB (dir : String) : IO CmdResult := do let root : System.FilePath := System.FilePath.mk dir - let mkCode ← runProcPrint "mkdir" #["-p", dir] - if mkCode != 0 then println s!"Error: could not create '{dir}'."; return + if (← runProcPrint "mkdir" #["-p", dir]) != 0 then + println s!"Error: could not create '{dir}'."; return cmdErr IO.FS.writeFile (root / "lakefile.lean") "import Lake\nopen Lake DSL\n\npackage KnowledgeBase where\n\nlean_lib KnowledgeBase where\n" IO.FS.writeFile (root / "KnowledgeBase.lean") "-- KnowledgeBase root module\n-- Run `kb check` to populate this file.\n" - let _ ← runProcPrint "git" #["init"] (some dir) - let _ ← runProcPrint "git" #["add", "."] (some dir) - let _ ← runProcPrint "git" #["commit", "-m", "Initial kb scaffold"] (some dir) + let _ ← runProcPrint "git" #["init"] (some dir) + let _ ← runProcPrint "git" #["add", "."] (some dir) + let _ ← runProcPrint "git" #["commit", "-m", "Initial kb scaffold"] (some dir) println s!"Initialised knowledge base in '{dir}'." + return cmdOk -------------------------------------------------------------------------------- --- 13. Domain listing / stats +-- 14. Domain info -------------------------------------------------------------------------------- -def listDomains (stateRef : IO.Ref KBState) : IO Unit := do - let state ← stateRef.get +def listDomains (stateRef : IO.Ref KBState) : IO CmdResult := do + let state ← stateRef.get let domains := dedupStrings (state.decls.map (·.domain)).toList - if domains.isEmpty then - println "(no domains in current session — use 'add … in <Domain>' to create one)" + if domains.isEmpty then println "(no domains loaded — use 'add … in <Domain>' to create one)" else do - println "Domains active this session:" + println "Domains:" for dom in domains do let n := (state.decls.filter (fun d => d.domain == dom)).size println s!" {dom} ({n} declaration(s))" + return cmdOk -def domainsStats (stateRef : IO.Ref KBState) : IO Unit := do - let state ← stateRef.get +def domainsStats (stateRef : IO.Ref KBState) : IO CmdResult := do + let state ← stateRef.get let domains := dedupStrings (state.decls.map (·.domain)).toList - println "=== Domain statistics (current session) ===" - if domains.isEmpty then - println " (none)" - else - for dom in domains do - let ds := state.decls.filter (fun d => d.domain == dom) - println s!" {dom}: {ds.size} declaration(s)" - for k in ["type","instance","prop","rel","fact","rule","def"] do - let n := (ds.filter (fun d => d.kind == k)).size - if n > 0 then println s!" {k}: {n}" - println "\n=== By kind (all domains) ===" + println "=== Domain statistics ===" + if domains.isEmpty then println " (none)" + else for dom in domains do + let ds := state.decls.filter (fun d => d.domain == dom) + println s!" {dom}: {ds.size}" + for k in ["type","instance","prop","rel","fact","rule","def"] do + let n := (ds.filter (fun d => d.kind == k)).size + if n > 0 then println s!" {k}: {n}" + println "\n=== By kind ===" for k in ["type","instance","prop","rel","fact","rule","def"] do let n := (state.decls.filter (fun d => d.kind == k)).size if n > 0 then println s!" {k}: {n}" println s!"\n Total: {state.decls.size}" + return cmdOk -------------------------------------------------------------------------------- --- 14. Help text +-- 15. Help -------------------------------------------------------------------------------- def helpText : String := "Lean4 Knowledge Base CLI (kb)\n" ++ - "Usage: <command> [arguments]\n\n" ++ - "Every declaration must specify its destination domain file explicitly\n" ++ - "with `in <Domain>`. Domain names are arbitrary identifiers; each becomes\n" ++ - "a <Domain>.lean file in the KB root.\n\n" ++ - "Commands:\n" ++ - " init <dir>\n" ++ - " Create a new knowledge base repository in <dir>.\n\n" ++ - " add type <Name> [extends <Parent>] in <Domain>\n" ++ - " Declare a new type, optionally as a subtype of <Parent>.\n\n" ++ - " add instance <name> : <Type> in <Domain>\n" ++ - " Declare a named individual of the given type.\n\n" ++ - " add prop <name> : <DomType> -> <Range> in <Domain>\n" ++ - " Add a property mapping a type to a value type.\n\n" ++ - " add rel <name> : <D1> -> <D2> -> Prop in <Domain>\n" ++ - " Add a binary relation between two types.\n\n" ++ - " add fact <fact> in <Domain>\n" ++ - " Assert a fact. Syntax: prop(inst) = val or rel(a, b).\n\n" ++ - " add rule <name> : <statement> in <Domain>\n" ++ - " Add a universally quantified axiom.\n\n" ++ - " add def <name> <params> : <Type> := <body> in <Domain>\n" ++ - " Define a reusable computed shortcut.\n\n" ++ - " rm <name>\n" ++ - " Remove a declaration (warns about dependents).\n\n" ++ - " list <types|instances|props|rels|facts|rules|defs|all> [of <filter>]\n" ++ - " List declarations, optionally filtered by name/domain/content.\n\n" ++ - " show def <name>\n" ++ - " Print the Lean source of a named declaration.\n\n" ++ - " eval <expr>\n" ++ - " Evaluate a computable Lean expression via #eval.\n\n" ++ + "All `add` commands require `in <Domain>` — each domain is a <Domain>.lean file.\n\n" ++ + "ADD\n" ++ + " add type <n> [extends <Parent>] in <D>\n" ++ + " add instance <n> : <Type> in <D>\n" ++ + " add prop <n> : <DomType> -> <Range> in <D>\n" ++ + " add rel <n> : <D1> -> <D2> -> Prop in <D>\n" ++ + " add fact <fact> in <D> prop(inst) = val or rel(a, b)\n" ++ + " add rule <n> : <statement> in <D>\n" ++ + " add def <n> <params> : <Type> := <body> in <D>\n\n" ++ + "READ\n" ++ + " list <types|instances|props|rels|facts|rules|defs|all> [of <Domain>]\n" ++ + " show def <n> Lean source of a declaration.\n" ++ + " get <prop>(<inst>) Retrieve a property value (runs #eval).\n" ++ + " search <text> Full-text search across names, Lean source, domains.\n" ++ + " deps <n> Forward and reverse dependency graph for a declaration.\n" ++ + " eval <expr> Run #eval on a Lean expression.\n\n" ++ + "QUERY\n" ++ " query <prop>\n" ++ - " Try to prove a proposition (Yes / No / Unknown).\n\n" ++ - " check\n" ++ - " Sync imports and run lake build to verify the whole KB.\n\n" ++ - " commit <message>\n" ++ - " Verify then git-commit all changes.\n\n" ++ - " status\n" ++ - " Show git status and session summary.\n\n" ++ - " domains\n" ++ - " List all domains active in this session with declaration counts.\n\n" ++ - " domains stats\n" ++ - " Detailed breakdown of declarations per domain and kind.\n\n" ++ - " help Show this message.\n" ++ - " exit Quit.\n\n" ++ - "Example workflow:\n" ++ - " add type Entity in Ontology\n" ++ - " add type Person extends Entity in Ontology\n" ++ - " add type Place extends Entity in Ontology\n" ++ + " query <prop> using <tactic-script>\n" ++ + " Attempt to prove a proposition. Default tactics: first | decide | aesop | simp\n" ++ + " Returns Status: Yes / No / Unknown and the proof term on success.\n\n" ++ + "BUILD & GIT\n" ++ + " check Sync imports + lake build to verify whole KB.\n" ++ + " commit <message> Verify then git-commit all changes.\n" ++ + " status git status + domain summary.\n" ++ + " rm <n> Remove a declaration (warns about dependents).\n\n" ++ + "DOMAINS\n" ++ + " domains List domains with declaration counts.\n" ++ + " domains stats Breakdown per domain and kind.\n\n" ++ + " init <dir> Create a new KB repository.\n" ++ + " help | exit\n\n" ++ + "EXIT CODES 0 = success 1 = error\n\n" ++ + "PERSISTENCE State is stored as --@kb metadata in each domain file and\n" ++ + " reloaded automatically on startup.\n\n" ++ + "EXAMPLE\n" ++ + " add type Entity in People\n" ++ + " add type Person extends Entity in People\n" ++ " add instance socrates : Person in People\n" ++ " add prop birthYear : Person -> Nat in People\n" ++ " add fact birthYear(socrates) = 470 in People\n" ++ + " get birthYear(socrates)\n" ++ + " deps birthYear\n" ++ + " search socrates\n" ++ + " query birthYear socrates = 470 using decide\n" ++ " check\n" ++ " commit \"Added Socrates\"\n" -------------------------------------------------------------------------------- --- 15. Main REPL loop +-- 16. Main REPL loop -------------------------------------------------------------------------------- -partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Bool := do +partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO CmdResult := do match parseCommand line with | none => - println s!"Unknown command: '{line}'." - println "Type 'help' for usage, including required 'in <Domain>' syntax." - return true + println s!"Error: unknown command '{line}'." + println " Hint: add commands require `in <Domain>`. Run 'help' for usage." + return cmdErr | some cmd => match cmd with - | .Init dir => initKB dir - | .AddType n p dom => addType stateRef n p dom - | .AddInstance n t dom => addInstance stateRef n t dom - | .AddProp n dt rng dom => addProp stateRef n dt rng dom - | .AddRel n d1 d2 dom => addRel stateRef n d1 d2 dom - | .AddFact f dom => addFact stateRef f dom - | .AddRule n s dom => addRule stateRef n s dom - | .AddDef n p t b dom => addDef stateRef n p t b dom - | .Remove n => removeDecl stateRef n - | .List w f => listDecls stateRef w f - | .ShowDef n => showDef stateRef n - | .Eval e => evalExpr stateRef e - | .Query p => queryProp stateRef p - | .Check => checkKB stateRef - | .Commit m => commitChanges stateRef m - | .Status => showStatus stateRef - | .Domains => listDomains stateRef - | .DomainsStats => domainsStats stateRef - | .Help => println helpText - | .Exit => return false - return true + | .Init dir => initKB dir + | .AddType n p dom => addType stateRef n p dom + | .AddInstance n t dom => addInstance stateRef n t dom + | .AddProp n dt rng dom => addProp stateRef n dt rng dom + | .AddRel n d1 d2 dom => addRel stateRef n d1 d2 dom + | .AddFact f dom => addFact stateRef f dom + | .AddRule n s dom => addRule stateRef n s dom + | .AddDef n p t b dom => addDef stateRef n p t b dom + | .Remove n => removeDecl stateRef n + | .List w f => listDecls stateRef w f + | .ShowDef n => showDef stateRef n + | .Get e => getVal stateRef e + | .Search q => searchDecls stateRef q + | .Deps n => showDeps stateRef n + | .Eval e => evalExpr stateRef e + | .Query p t => queryProp stateRef p t + | .Check => checkKB stateRef + | .Commit m => commitChanges stateRef m + | .Status => showStatus stateRef + | .Domains => listDomains stateRef + | .DomainsStats => domainsStats stateRef + | .Help => println helpText; return cmdOk + | .Exit => return cmdQuit partial def main : IO Unit := do + let root : System.FilePath := System.FilePath.mk "." + let decls ← loadState root + let stateRef ← IO.mkRef (KBState.mk root decls) + if decls.size > 0 then + println s!"Loaded {decls.size} declaration(s) from KB." println "Lean4 Knowledge Base CLI — type 'help' for commands, 'exit' to quit." - let stateRef ← IO.mkRef (KBState.mk (System.FilePath.mk ".") #[]) let rec loop : IO Unit := do IO.print "kb> " let line ← (← IO.getStdin).getLine let trimmed := line.trim unless trimmed.isEmpty do - let cont ← processCommand stateRef trimmed - unless cont do return + let result ← processCommand stateRef trimmed + unless result.continue do return loop loop @@ -6,74 +6,92 @@ A persistent, formally verified knowledge base stored as a Git repository of Lea ## Core Concepts -- **Persistent**: stored as `.lean` files in a Git repository — survives across sessions. +- **Persistent**: state is stored as `--@kb` metadata comments in each domain file and reloaded automatically on startup — no state is lost between sessions. - **Formally verified**: every addition is type-checked by Lean's kernel at `kb check` / `kb commit` time. - **Domain-organised**: declarations are grouped into named domain files. Each domain is one `.lean` file. An agent can load a specific domain into its context without loading the entire KB. - **Version-controlled**: full history, branching, and reproducibility via Git. +- **Agent-friendly**: all commands return exit code `0` on success and `1` on error, with structured one-line error messages. + +--- + +## Persistence Model + +Every declaration written to disk is preceded by a metadata header: + +``` +--@kb kind=prop name=birthYear domain=People +opaque birthYear : Person → Nat +``` + +On startup, `kb` scans all `*.lean` domain files in the current directory, parses these headers, and reconstructs the full declaration list. This means: + +- Restarting `kb` is safe — all prior work is reloaded. +- The `--@kb` format is the source of truth; the Lean code is preserved exactly for the compiler. +- `rm` removes the entire `--@kb` block and its Lean source atomically, regardless of how many lines the source spans. --- ## Planned Domain Structure -The KB is organised into four top-level sections. Each subsection corresponds to one domain file — the natural unit an agent loads for a focused query. For example, an agent answering a chemistry question loads only `Chemistry`; one doing financial calculations loads only `MoneyFinance`. +The KB is organised into four top-level sections. Each subsection is one domain file — the natural unit an agent loads for a focused task. ### Mathematics | Domain file | Coverage | |-------------|----------| -| `LogicSetTheory` | Symbolic logic and foundations: Boolean algebra, set theory, transfinite numbers | -| `Probability` | Quantification of likelihood: games of chance, Bernoulli's trials, probability formulas, probability distributions | -| `AppliedMathematics` | Optimization, numerical analysis, dynamic systems, fractals, game theory, packing and covering objects | -| `ElementaryMath` | Arithmetic, fractions, percentages; reasoning about parity and sign of underspecified values | +| `LogicSetTheory` | Boolean algebra, set theory, transfinite numbers | +| `Probability` | Games of chance, Bernoulli's trials, probability formulas and distributions | +| `AppliedMathematics` | Optimization, numerical analysis, dynamic systems, fractals, game theory, packing | +| `ElementaryMath` | Arithmetic, fractions, percentages; parity and sign of underspecified values | | `Algebra` | Variables, number systems, algebraic operations and symbols | | `Geometry` | Plane, solid, coordinate, transformations, high-dimensional, packing, curves, polyforms, topology, tilings | | `Plotting` | Functions, equations, parametric plots, inequalities, number lines, polar plots | -| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms, continuity, domain & range | +| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms | | `DifferentialEquations` | Ordinary (ODE) and partial (PDE) differential equations | | `Statistics` | Descriptive statistics, inference, regression, random variables | -| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special, number-theoretic, representation formulas | +| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special functions | ### Science & Technology | Domain file | Coverage | |-------------|----------| -| `Physics` | Mechanics, oscillations & waves, statistical physics, thermodynamics, electricity & magnetism, optics, relativity, nuclear, quantum, particle, astrophysics, constants, principles, effects, fluid mechanics | -| `Chemistry` | Chemical elements, molecules, ions, quantities, reactions, thermodynamics, solutions, cheminformatics, quantum chemistry, functional groups, bonds & orbitals, nuclear chemistry | +| `Physics` | Mechanics, thermodynamics, electromagnetism, optics, relativity, nuclear, quantum, particle, astrophysics, fluid mechanics, physical constants | +| `Chemistry` | Elements, molecules, ions, quantities, reactions, thermodynamics, solutions, quantum chemistry, bonds & orbitals, nuclear chemistry | | `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems | -| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables, measurement devices | -| `HealthMedicine` | Physical exercise, human anatomy, medical codes, blood alcohol content, mortality data, diseases, medical computations, vision, medical tests, nuclear medicine, health-care statistics, drugs & prescriptions, public health | -| `TechnologicalWorld` | Communications, satellites, barcodes, space probes, photography, structures, nuclear power, nuclear explosions, carbon footprint, inventions, web & computer systems | -| `Materials` | Alloys, bulk materials, material hardness, minerals, plastics, woods, material chemistry | -| `ComputationalSciences` | Cellular automata, substitution systems, Turing machines, complexity, algebraic codes, fractals, image processing, hashing | +| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables | +| `HealthMedicine` | Anatomy, medical codes, blood alcohol, mortality, diseases, medical computations, drugs, public health | +| `TechnologicalWorld` | Communications, satellites, barcodes, space probes, nuclear power, carbon footprint, inventions, web & computer systems | +| `Materials` | Alloys, bulk materials, hardness, minerals, plastics, woods, material chemistry | +| `ComputationalSciences` | Cellular automata, Turing machines, complexity, algebraic codes, fractals, image processing, hashing | | `EarthSciences` | Geology, geodesy & navigation, oceanography, atmospheric sciences, climate | | `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants | | `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere | -| `FoodScience` | Food composition, nutrition, dietary references & standards, food comparison & combinations, food physics | +| `FoodScience` | Food composition, nutrition, dietary standards, food physics | ### Society & Culture | Domain file | Coverage | |-------------|----------| -| `Education` | International education, universities, school districts, standardized tests, education statistics | +| `Education` | International education, universities, school districts, standardized tests | | `People` | Biographical and demographic data on notable individuals and public figures | -| `ArtsMedia` | Movies, television, video games, notable texts, periodicals, comics, fictional characters, popular curves, mythology, music | -| `History` | Historical numbers, historical periods, genealogy, historical events, historical countries, military conflicts, world leaders, inventions | -| `WordsLinguistics` | Word properties, languages, document length, notable texts, transliterations, Morse code, Soundex, encodings, emotions | -| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income tax, sales tax | +| `ArtsMedia` | Movies, television, video games, notable texts, periodicals, comics, mythology, music | +| `History` | Historical periods, genealogy, events, countries, military conflicts, world leaders, inventions | +| `WordsLinguistics` | Word properties, languages, transliterations, Morse code, Soundex, encodings | +| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income and sales tax | | `DatesTimes` | Dates, calendars, time systems | | `FoodNutrition` | Nutritional data and dietary guidelines | -| `Demographics` | Health care, age/sex, gender equality, business, citizenship, crime, education, income & employment, language, race, marriage, mobility, religion, military, HDI | +| `Demographics` | Health care, age/sex, gender, education, income, crime, marriage, religion, military, HDI | ### Everyday Life | Domain file | Coverage | |-------------|----------| | `PersonalHealth` | Physical exercise, food and nutrition, child growth & development | -| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, gasoline, food, electricity prices | +| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, prices | | `Entertainment` | Music, films, artworks, cultural productions | | `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena | -| `DatesAnniversaries` | Calendar information, celebrations, time zone calculations, time math, anniversaries | -| `Travel` | Weather, cost of living, flight data, gasoline prices, points of interest, travel distances | +| `DatesAnniversaries` | Calendar information, celebrations, time zones, anniversaries | +| `Travel` | Weather, cost of living, flight data, gasoline prices, points of interest | | `HouseholdMath` | Everyday calculations and measurements | | `Programming` | Algorithms, data structures, programming concepts | | `Hobbies` | Recreational activities and personal projects | @@ -81,21 +99,6 @@ The KB is organised into four top-level sections. Each subsection corresponds to --- -## Knowledge Representation - -| Kind | Description | Lean form | -|------|-------------|-----------| -| **Type** | A category or class | `opaque Person : Type` | -| **Subtype** | A type extending another | `opaque Philosopher : Type` + coercion axiom | -| **Instance** | A named individual | `opaque socrates : Person` | -| **Property** | A function from a type to a value | `opaque birthYear : Person → Nat` | -| **Relation** | A binary predicate | `opaque bornIn : Person → Place → Prop` | -| **Fact** | An asserted value or relation | `axiom fact_birthYear_socrates : birthYear socrates = 470` | -| **Rule** | A universally quantified axiom | `axiom ancestors_transitive : ∀ x y z, …` | -| **Definition** | A named computable expression | `def yearsToDouble (r : Float) : Float := …` | - ---- - ## CLI Commands ### Adding knowledge *(all require `in <Domain>`)* @@ -112,21 +115,33 @@ The KB is organised into four top-level sections. Each subsection corresponds to Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. -### Inspecting knowledge +### Reading knowledge | Command | Description | |---------|-------------| -| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations, optionally filtered by domain | +| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations | | `show def <n>` | Print the Lean source of a declaration | -| `domains` | List all domains active this session with declaration counts | -| `domains stats` | Detailed breakdown per domain and kind | +| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` | +| `search <text>` | Full-text search across names, Lean source, and domain names | +| `deps <n>` | Show forward dependencies (what `<n>` uses) and reverse dependencies (what uses `<n>`) | +| `eval <expr>` | Evaluate a Lean expression via `#eval` | ### Querying | Command | Description | |---------|-------------| -| `eval <expr>` | Evaluate a computable Lean expression via `#eval` | -| `query <prop>` | Attempt to prove a proposition (Yes / No / Unknown) | +| `query <prop>` | Attempt to prove a proposition. Returns `Status: Yes/No/Unknown`. | +| `query <prop> using <tactic-script>` | Same with a custom tactic. On success, prints the proof term. | + +Default tactic sequence: `first | decide | aesop | simp`. + +Useful custom tactics: +- `decide` — fully decidable propositions +- `native_decide` — faster for large decidable computations +- `omega` — linear arithmetic over `Nat` and `Int` +- `norm_num` — numeric computations +- `ring` — ring equalities +- `simp [myLemma]` — simplification with specific lemmas ### Build and version control @@ -135,8 +150,15 @@ Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. | `init <dir>` | Create a new KB repository | | `check` | Sync imports and run `lake build` to verify the whole KB | | `commit <message>` | Verify then `git commit` all changes | -| `status` | Show `git status` and session summary | -| `rm <n>` | Remove a declaration (warns about dependents) | +| `status` | Show `git status` and domain summary | +| `rm <n>` | Remove a declaration and its metadata block (warns about dependents) | + +### Domain info + +| Command | Description | +|---------|-------------| +| `domains` | List all loaded domains with declaration counts | +| `domains stats` | Detailed breakdown per domain and kind | --- @@ -148,53 +170,50 @@ Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. 2. Inspects which domains reference names declared in other domains, and injects the necessary `import` lines. 3. Rewrites `KnowledgeBase.lean` to import all domain files so `lake build` compiles everything. -Add a batch of declarations, then run `check` once at the end rather than after each individual addition. +Add a batch of declarations, then run `check` once — not after each individual addition. + +--- + +## Exit Codes + +Every command exits with `0` on success and `1` on error (duplicate declaration, name not found, build failure, parse failure). This allows agent scripts to detect failure without parsing output: + +```bash +kb add type Person in People && echo "OK" || echo "FAILED" +``` --- ## Example Workflow ```bash -# Initialise -kb init ./myKB -cd myKB +kb init ./myKB && cd myKB -# Base types in the People domain +# Add a batch kb add type Entity in People kb add type Person extends Entity in People kb add type Place extends Entity in People kb add type City extends Place in People - -# Properties and relations kb add prop birthYear : Person -> Nat in People kb add rel bornIn : Person -> Place -> Prop in People - -# Instances and facts kb add instance socrates : Person in People kb add instance athens : City in People kb add fact birthYear(socrates) = 470 in People kb add fact bornIn(socrates, athens) in People -# Verify and commit +# Inspect +kb deps birthYear # forward and reverse dependency graph +kb search athens # full-text search +kb get birthYear(socrates) # → 470 + +# Query +kb query "birthYear socrates = 470" using decide +# Status: Yes +# Proof: ... + +# Verify and persist kb check kb commit "Added Socrates and basic person/place ontology" -# Agent loads only the People domain for a biographical query -kb list all of People +# Next run: all state reloads automatically from People.lean ``` - ---- - -## Query Capabilities - -- **Computational**: `kb eval "yearsToDouble 0.05"` — runs `#eval` on any computable Lean expression. -- **Logical**: `kb query "even (2 + 2)"` — attempts to prove the proposition using `decide`, `aesop`, or `simp`. -- **Selective loading**: `kb list all of Physics` — an agent pulls only the Physics domain into its context for a focused query. - ---- - -## Extensibility - -- Domain files from the planned structure are created on first use — no separate setup step needed. -- Definitions (`kb add def`) become permanent reusable shortcuts stored in Lean files. -- The KB grows incrementally across sessions — each `kb commit` is a checkpoint in Git history. |