Prepare proof-pilot for crates.io: kernel-arbitrated LLM proof completion for Lean 4#18
Conversation
proof-pilot is domain-agnostic — a kernel-arbitrated LLM proof-completion loop for Lean 4 with anti-cheat and deterministic replay — and every non-ZK Lean user who adopts it discovers scribe. This decouples the scribe-isms and makes the package self-contained: - notes.rs: guidance is now domain-neutral. NotesStyle lets an embedder attach per-pattern worked-example citations + a reference-library line; render_notes_styled carries them, render_notes stays generic. scribe-cli supplies the lean/ZkGadgets citations, so scribe's NOTES.md is unchanged; the proof-pilot binary emits generic guidance. - lsp_feedback.rs: the Python LSP bridge is embedded via include_str! and materialized to a temp path when no repo-local copy exists, with a PROOF_PILOT_LSP_SERVER override — LSP mode works from the published crate, not just the repo checkout. - Cargo.toml: full crates.io metadata (description, repository, docs.rs, keywords, categories, readme). Crate-level rustdoc with a quick-start; crates/proof-pilot/README.md pitched at general Lean users. - examples/prove_sum_comm.rs: a plain arithmetic lemma through the loop — the non-ZK demonstration. cargo package -p proof-pilot builds standalone (verify build green). The crate name is unclaimed on crates.io. Publishing is deliberately left as a manual step.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2b81f90b84
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| decides. | ||
|
|
||
| ```sh | ||
| proof-pilot MyProject/Theorem.lean --lake-dir MyProject --max-iters 10 |
There was a problem hiding this comment.
When users follow this new crates.io quick start from an installed proof-pilot, the binary still defaults to reading prompts/lean-prover.md and exits if that file is missing (src/main.rs defines that repo-relative default and aborts on read failure). That prompt lives outside crates/proof-pilot, so the documented standalone command fails before constructing the backend unless the caller supplies their own --system-prompt, which blocks the publishable-package path this change is adding.
Useful? React with 👍 / 👎.
| } | ||
| } | ||
| Err("could not find scripts/lsp-server.py — run from the repo root".to_string()) | ||
| let dir = std::env::temp_dir().join("proof-pilot"); |
There was a problem hiding this comment.
When the installed crate falls back to the embedded script, this writes to std::env::temp_dir()/proof-pilot, which is commonly a shared /tmp location on Unix rather than the per-user path the comment describes. If another account or a previous root-run has already created /tmp/proof-pilot without write permission, create_dir_all can succeed but the subsequent script write fails, so --lsp aborts even though the bridge is bundled; use a user-specific or securely-created temp path instead.
Useful? React with 👍 / 👎.
1 participant
Extracts proof-pilot as a standalone, publishable crate — "kernel-arbitrated LLM proof completion for Lean 4, with anti-cheat and deterministic replay" — serving every Lean user; every non-ZK adopter discovers scribe.
Decoupling
NotesStylelets an embedder attach per-pattern worked-example citations + a reference-library line (render_notes_styled);render_notesstays generic. scribe-cli supplies thelean/ZkGadgetscitations, so scribe's NOTES.md output is unchanged; the bareproof-pilotbinary now emits generic guidance.include_str!and materialized to a temp path when no repo-local copy exists (PROOF_PILOT_LSP_SERVERoverride available) —--lspworks from the published crate, not just a repo checkout.#-prefixed top-level commands, not#audit_axiomsspecifically).Packaging
examples/prove_sum_comm.rs: a plain arithmetic lemma through the loop — the non-ZK demonstration.cargo package -p proof-pilotbuilds standalone (verify build green); package list is self-contained.--samples-per-iterin the 0.1 API per the sequencing decision (scribe judge (SOUND / UNSOUND / UNDETERMINED) + best-of-n sampling #17 landed first).Publish checklist (manual, after merge)
cargo login(crates.io token)cargo publish -p proof-pilot --dry-runcargo publish -p proof-pilotThe name
proof-pilotis unclaimed on crates.io (verified against the API). Publishing is deliberately not automated — it is an outward-facing, irreversible action.