test(faces): prove a Python-face program runs end-to-end (face → wasm → result)#684
Merged
Conversation
… → result) The README's headline is "faces are the product" — a program in a familiar surface, elaborated to the affine core, compiled to wasm. That path had never been exercised as *running code*, only parsed. This proves it: - test/e2e/fixtures/python_face_runnable.pyaff — Python-shaped source (`def`, `if/else`, recursion), `# face: python` pragma. - test/e2e/python_face_e2e.sh — compiles it THROUGH the Python face to core-WASM and asserts main() === 5170 (fac(5)=120 + sum_to(100)=5050). Skips loudly (exit 0) without the compiler or node; AFFINESCRIPT_BIN overrides the binary path. Observed (node 26, dune 3.24 build): Compiled fixtures/python_face_runnable.pyaff -> pf.wasm (WASM) main() = 5170 (expected 5170) PASS: Python-face program ran end-to-end (face -> wasm -> correct result) Recursion, not a loop, on purpose: proving the face path surfaced two real bugs, filed with minimal repros: - #683 — the Python face drops the trailing `;` on the last statement of a while/for body (tail-position detection doesn't distinguish loop bodies from value bodies), so face-authored loops don't yet compile. Recursion's tail line is a value expression, which the face handles correctly. - #682 — `total` is rejected as a variable name in let-binding / assignment position (the `TOTAL` soft-keyword's ident-recovery is incomplete). The fixture avoids that name. So this is an honest end-to-end proof of the face→wasm path today, and a regression lock, with the known loop gap tracked in #683. Gates: dune build 0; face e2e PASS; doc-truthing OK; soundness ledger all-5 OK. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
The README's headline is "faces are the product" — write a familiar surface, get the affine core underneath, compiled to wasm. That path had never been exercised as running code, only parsed (the scan flagged "faces exist but no face-authored program is proven end-to-end to wasm"). This closes that.
test/e2e/fixtures/python_face_runnable.pyaff— Python-shaped source (def,if/else, recursion) with a# face: pythonpragma.test/e2e/python_face_e2e.sh— compiles it through the Python face to core-WASM and assertsmain() === 5170(fac(5)=120 + sum_to(100)=5050). Skips loudly without the compiler/node;AFFINESCRIPT_BINoverrides the path.Two real bugs the faces path surfaced (filed)
Recursion is used deliberately, because proving this found:
;dropped on the last statement of a while/for loop body #683 — the Python face drops the trailing;on the last statement of awhile/forbody (tail-position detection doesn't distinguish loop bodies from value bodies), so face-authored loops don't yet compile. Recursion's tail line is a value expression, which the face handles correctly.totalrejected as a variable name in let-binding / assignment-target position #682 —totalis rejected as a variable name inlet-binding / assignment position (theTOTALsoft-keyword's ident-recovery is incomplete).An honest end-to-end proof of the face→wasm path today, a regression lock, with the loop gap tracked in #683.
Gates
dune build0 · face e2e PASS · doc-truthing OK · soundness ledger all-5 OK.🤖 Generated with Claude Code