Skip to content

Move retrieval and integrations to Lean with checked contracts - #1

Merged
o8vm merged 4 commits into
mainfrom
harness-adapters
Sep 12, 2026
Merged

o8vm merged 4 commits into
mainfrom
harness-adapters

Conversation

@o8vm

@o8vm o8vm commented Sep 12, 2026

Copy link
Copy Markdown
Collaborator

Eggshell now runs retrieval selection, setup decisions, plugin packaging, and the independent harness adapters in Lean. Python is limited to FastEmbed inference and the existing NumPy kernels; the Codex engine does not import the adapter package. The README describes the experimental adapter boundary and the unchanged scope of the published token measurements.

The production functions carry 29 audited Lean contracts covering selection bounds and identity, preserved configuration, adapter ownership, terminal journaling, and delivery acknowledgements. Process tests cover interrupted saves, stalled search, chat isolation, compaction, four adapter protocols, and installation ownership. OS, numerical, and host-delivery boundaries are documented explicitly.

Validation on macOS: all core, lifecycle, package/setup, and adapter tests passed; all 24 legacy-provider comparisons passed across lexical, semantic, and hybrid modes; OpenCode output tests and all five public sample tests passed. Linux and macOS CI must also pass before the 0.1.0 runtime refresh.

@o8vm
o8vm merged commit 6059647 into main Sep 12, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant