Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 17 Packages Wiki Activity Actions 147
open-standards/jouleclaw/jouleclaw-rs/crates/jouleclaw-oracle-lean
History
Exact
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Transaction Science 93d9b7ec16 jouleclaw-oracle-lean's tests: a mock toolchain is written by a process of its own 
The tests wrote each mock `lean` script in this process, then ran it. A fork
copies the forker's open descriptors into its child until that child's exec,
so a sibling test's spawn could hold the script open for writing at the moment
it ran. exec then failed with ETXTBSY, and the oracle rightly reported a
toolchain it could not start: `lean-toolchain-missing` where the test expected
`lean-timeout`, and the same in three other tests of the crate.

`sh` now writes the script, and has exited before the test goes on, so this
process never holds a descriptor for it. The timeout test also prints the
oracle's message when it fails, which is how the cause was read.

16 runs at a time, 8 test threads each, on Linux arm64: 23 of 4,800 runs failed
before, all `Text file busy (os error 26)`; 0 of 4,800 after.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-11-07 01:30:31 -05:00
..
src jouleclaw-oracle-lean's tests: a mock toolchain is written by a process of its own 2026-11-07 01:30:31 -05:00
Cargo.toml Cargo: no minimum-supported-version floor, because the policy is latest stable 2026-11-03 17:42:20 -05:00
README.md docs: drop vanity test-counts (no-vanity-metrics policy) 2026-06-07 19:00:28 -04:00

README.md

jouleclaw-oracle-lean

Scope: jouleclaw-oracle::Oracle impl backed by a Lean 4 toolchain. The candidate's content is written to a temp file; lean is invoked; exit code maps to Verdict { Pass | Fail }.

Relation to jouleclaw-formalize

These two crates are complementary, not duplicative. They gate different stages of the same proof chain:

  1. Informal claim → Lean source (translation): the faithfulness gate. jouleclaw-formalize::FaithfulnessChecker verifies that the Lean encoding actually expresses the English claim the human intended. Without this, you can rigorously prove the wrong theorem.

  2. Lean source → exit code (compilation): the correctness gate. This crate's LeanOracle::verify invokes the compiler and treats exit 0 as proof acceptance.

A production proof-carrying-code pipeline runs BOTH:

claim --[jouleclaw-formalize]--> Lean source --[jouleclaw-oracle-lean]--> Verdict
            ^                                          ^
       faithfulness                              compiler exit

If you skip jouleclaw-formalize, the Verdict::Pass from this crate means "this Lean source compiles" — not "the Lean source proves the claim the user actually made." That distinction is the same distinction the AlphaProof / AlphaGeometry literature makes: compiler feedback only rules out hallucinations if the formalization is faithful.

What ships

  • LeanOracle (Oracle trait impl)
  • LeanOracleConfig { toolchain, timeout, workdir, extra_flags }
  • LeanOracleError { ToolchainMissing | Io | Timeout }
  • Mock-lean test harness (no real Lean install required)