geolog-zeta-fork/notes/003-project-status.md

Project Status

Version: 0.1.0 (Early stage, but functional)

---

Codebase Size

What	Count
Rust source code	~30,000 lines
Test code	~8,000 lines
Example .geolog files	~2,300 lines across 30 files
Source files	84
Unit tests	137 (all passing)
Integration tests	31 (all passing)

---

What Works Well

These features are complete and reliable:

Core Engine

• Parser — reads .geolog files, gives helpful error messages
• Type checker — catches mistakes like using undefined sorts
• Chase algorithm — derives facts from rules correctly
• Equality handling — when rules say x = y, elements are properly merged

Examples That Run

cargo run -- examples/geolog/graph.geolog        # Simple directed graph
cargo run -- examples/geolog/preorder.geolog     # Reflexive, transitive relation
cargo run -- examples/geolog/transitive_closure.geolog  # Shows chase in action
cargo run -- examples/geolog/category.geolog     # Category theory basics

Interactive Features

• REPL with command history
• Inspect any theory or instance
• Run chase interactively
• Save/load with version history

---

What Mostly Works

These features work but have limitations:

Parameterized Theories

You can define theories that depend on other instances:

theory (N : PetriNet instance) Marking {
  token : Sort;
  token/of : token -> N/P;  // References N's places
}

Limitation: Nested instances (instances inside instances) only partially work.

Model Search

The solver can find models satisfying axioms, but:

• Works best for small models
• Some search strategies are incomplete
• No timeout handling

---

Known Gaps

Things That Don't Work Yet

Feature	Status
Product types in conclusions	Functions returning records don't fully work
Existentials over products	exists p : [x:M, y:M]. ... fails
Field projections in equations	x.field = y doesn't compile

Example of What Fails

// This works:
forall x : M. |- exists y : M. f(x) = y

// This doesn't work (product sort in existential):
forall x : M. |- exists p : [a:M, b:M]. g(x) = p

Silent Failures

When the tensor compiler can't handle an axiom, it silently skips it. This can be confusing — your axiom looks fine but nothing happens.

// This axiom might be silently skipped if it has unsupported patterns:
ax/complex : forall x. premise |- [a: x, b: x] some_relation;
// No error, but also no effect

---

TODOs in the Code

These are marked in the source with // TODO:

Location	What's Missing
src/repl.rs:84	Theory type not fully stored in metadata
src/overlay.rs:380	Copying functions between structures
src/store/query.rs:61	Batch loading for better performance
src/store/instance.rs	External references between instances
src/query/to_relalg.rs	Some relational operators

---

Test Coverage

What's Tested

Area	Tests
Type checking	14 unit tests
Chase algorithm	Comprehensive unit tests
Parser	4 unit tests + snapshot tests
Examples	31 integration tests (one per example file)
Random inputs	11 property-based test suites

Running Tests

cargo test              # Run all tests
cargo test unit_chase   # Run only chase tests
cargo test --release    # Run with optimizations (faster)

Fuzzing

The fuzz/ directory has fuzzing targets that generate random inputs to find crashes:

cargo +nightly fuzz run fuzz_parser

---

What's Being Worked On

According to code comments and structure:

1. Lean4 formalization — Mathematical proofs about correctness (in proofs/)
2. Better disjunction handling — Currently fires both branches, should choose one
3. Query plan improvements — More efficient execution