Eggshell keeps a deliberately small semantic core. Before proposing a new
operator or persistent data type, show why the behavior cannot be expressed by
the existing Value, All, Outcome, Occurrence, Inquiry, Receipt, and
scoped Union machinery.
Install the toolchain pinned in lean-toolchain, then run:
lake build eggshell eggshell_tests
EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" \
.lake/build/bin/eggshell_testsTests must use an isolated absolute EGGSHELL_DATA_ROOT; they refuse the normal
user data directory. Keep public claims tied to completed, reproducible measurements.
Build search_tests and run .lake/build/bin/search_tests to exercise the shipped
local search provider. Its MiniLM numerical runtime and model must already be
cached; the test uses offline mode and makes no generative model requests.
For performance work, total tokens mean input plus reasoning output plus final
output. Quality non-regression and .egg growth are constraints; tool count and
elapsed time are diagnostics.
Keep changes focused, remove replaced code, update user documentation with the
same change, and explain the invariant being preserved. Do not commit models,
vector caches, .egg authorities, generated build output, credentials, or
private benchmark transcripts.
plugins/eggshell contains the directory package's skill, hooks, and portable
launcher. The standalone installer embeds its manifest and hooks in
Eggshell/Install.lean; the existing test enforces that those definitions match.
Build eggshell, eggshell_package, and setup_package_tests, then run
.lake/build/bin/setup_package_tests when changing setup or packaging.
These native tests check configuration preservation, read-only inspection,
runtime checksums, ZIP readability, and deterministic packaging.
The manually dispatched Plugin package workflow builds and tests all four
platform runtimes, then runs the Lean eggshell_package executable. It publishes a small
eggshell-codex-plugin.zip and runtime archives whose names include their content
hashes on the release matching the plugin version. The same tested archives also
replace the standalone downloads and their SHA-256 files; runtime.json records
the source commit and archive checksums. The version and release tag stay unchanged.
The ZIP pins the exact runtime
URLs and SHA-256 values; hooks never download dependencies.
A package build is separate from OpenAI directory submission and approval. Before publishing a listing, inspect the uploaded package, confirm the hooks and helpers survive normalization, and test setup and a related two-chat handoff in the target Codex environment.