[senamakel]

Summary

`/check` requests for files of the same project could compile the same stale module at once, both writing one `.olean`/`.ilean`, and a reader could load a half-written olean. A restage could also rewrite sources under a build in progress (`STAGING` only serialised staging against staging). The rsi-ralph scorer will issue about 4 concurrent `lean_check` calls per candidate, so this has to be safe.

Fix: staging and `build_modules` now run together under a per-project lock (`build.project_lock`, keyed by the real path of the project's `lean/` dir) in a new `server.build_package`. Same-project requests build serially; different projects take different locks and still build in parallel. Elaboration after the build is outside the lock. Oleans are also written atomically (compile to `*.tmp`, then `os.replace`), so a failed or timed-out compile leaves no partial olean that `stale` would treat as fresh.

Related issue

None.

API or behavior changes

None to the HTTP API. Locks are per process; one service per builds dir and projects volume.

Validation

• `python3 -I -W error -m unittest discover -s docker/lean`: 38 tests OK
• Rust is untouched, so the cargo contract commands were not run. CI does not run the Python tests in `docker/lean`.

Tests

`docker/lean/test_server_concurrency.py`, written first and confirmed failing against the unlocked code (5 of 6 failed; the different-projects test passes both before and after, as it should):

• two_checks_of_one_projects_volume_never_compile_a_module_at_once
• two_checks_of_one_staged_project_never_compile_a_module_at_once
• a_restage_waits_for_the_build_in_progress
• checks_of_different_projects_build_at_the_same_time
• a_failed_compile_leaves_no_olean_behind
• a_timed_out_compile_leaves_no_olean_behind

No Lean needed: a fake `run` records overlapping compiles.

Documentation

`docker/lean/README.md` (new "Concurrent checks" section) and the `server.py` and `build.py` docstrings.

Checklist

• The change is focused on one logical change
• No new `#[allow(...)]`, `#[ignore]`, or relaxed lints
• No secrets, tokens, or `.env` contents in the diff or the description

Co-authored-by: Medulla medulla@tinyhumans.ai

Summary by CodeRabbit

• Performance

  • Checks for different projects can now build in parallel, while builds and staging for the same project are serialized. Elaboration can proceed concurrently after compilation.

• Reliability

  • Failed or timed-out builds no longer leave incomplete compiled outputs behind. Existing compiled outputs are preserved unless a build succeeds.

[tinysweeper]

Tiny Sweeper review

Reviewed head: 135bb8179b80e952a95386a72ba60a032f6e03d5

Verdict: Ready for maintainer review · Priority: none
Coverage: Reviewed 4 of 4 files.
Pull request purpose (title): Make the Lean servic…

Diagnostics and supporting details

Full summary

Pull request purpose (title): Make the Lean service safe for concurrent checks of one project. Tiny Sweeper completed its review; deterministic results follow.

Review snapshot

Change surface	Files	Review signal	Count
Production	2	Active findings	0
Tests	1	Noted findings	0
Documentation	1	Resolved findings	0
Configuration	0	Pending checks/questions	0

Completeness: Complete
Test assessment: Test coverage is assessed from changed tests and lane evidence; execution is not claimed without trusted check data.

What changed

A new `project_lock` in build.py keys a per-realpath threading.Lock, and a new `server.build_package` holds it across staging (`ensure_package`) and `build_modules`, with the lock released before elaboration. `build_modules` now compiles to `.tmp` files and `os.replace`s them into place, removing temporaries in a `finally`. A new test module, test_server_concurrency.py, exercises serialisation, restaging under a compile, parallel projects, and cleanup after failed and timed-out compiles. README and docstrings describe the behavior.

Features

• Added — Per-project lock for staging and building: Concurrent checks of one project serialize through a lock keyed by the real path of the project's `lean/` directory and held across `ensure_package` and `build_modules`, while different projects take different locks and build in parallel; the lock is released before elaboration. (docker/lean/server.py def release():, docker/lean/build.py def build_modules(lean_dir, modules, packages, timeout, run=subprocess.run):, docker/lean/README.md the decision is [ADR 0003](../../docs/adr/0003-run-lean-as-a-pinned-service.md).)
• Modified — Atomic olean/ilean writes: `build_modules` compiles to `.tmp` outputs and renames them into place via `os.replace` only after Lean succeeds, removing temporaries in a `finally`, so a failed or timed-out compile leaves no partial olean that `stale` would treat as fresh. (docker/lean/build.py def build_modules(lean_dir, modules, packages, timeout, run=subprocess.run):)
• Added — `build_package` server entry point: `build_package` consolidates staging plus building under the project lock and returns `(lean_dir, LEAN_PATH)`; `ensure_package` remains the staging step invoked inside the lock. (docker/lean/server.py def ensure_package(project):, docker/lean/server.py def release():)
• Added — Concurrency documentation: The README gains a "Concurrent checks" section and the build.py/server.py docstrings describe the locking and atomic-write behavior, including the per-process lock caveat. (docker/lean/README.md the decision is [ADR 0003](../../docs/adr/0003-run-lean-as-a-pinned-service.md).)

Tests

• new test module — `AtomicOleans.test_a_failed_compile_leaves_no_olean_behind` and `test_a_timed_out_compile_leaves_no_olean_behind` assert that a failed or timed-out fake compile leaves no olean and an empty output directory.: The tests lane answered with no findings on these cases. Execution was not observed by the reviewer. (docker/lean/test_server_concurrency.py)

Findings

No active actionable findings.

Before merge

None.

Agent review details

critique

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Lane summary: Reviewed 4 files; 0 findings. _The code index is behind this pull request (indexed at `46f1624d923e`), so retrieved context may be out of date._

security

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The security lane answered with no findings across the 3 reviewable files; README.md was not security-reviewed as prose data.
• Lane summary: Reviewed 3 files; 0 findings. 1 file was not security-reviewed: docker/lean/README.md (prose or tabular data). _The code index is behind this pull request (indexed at `46f1624d923e`), so retrieved context may be out of date._

tests

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The tests lane answered with no findings, reporting the new tests pin each invariant with fakes and would fail if the locking or atomic rename were removed.
• Lane summary: The change adds a per-project lock around staging and building in build_package and makes olean/ilean writes atomic via .tmp + os.replace, with a new test module that exercises serialisation, restaging under a compile, parallel projects, and cleanup after failed and timed-out compiles. The tests pin each of the stated invariants with fakes and would fail if the lock or the atomic rename were removed, so the change looks sound; the only caveat is that `project_lock` keyed on the `lean/` directory and the atomic write inside `build_modules` are not independently pinned by a test in the diff (the atomic path is only reachable through the fakes and is asserted, so this is acceptable). _The code index is behind this pull request (indexed at `46f1624d923e`), so retrieved context may be out of date._

commits

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The commits lane answered with no findings, reporting no sensitive content in committed files.
• Lane summary: No sensitive content in committed files. _The code index is behind this pull request (indexed at `46f1624d923e`), so retrieved context may be out of date._

description

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The description lane answered with no findings on accuracy of the description against the change.
• Lane summary: The change adds a per-project lock around staging and module compilation and writes oleans atomically, with matching tests and documentation; the description accurately covers all of it. One concern: on the projects-volume path, the lock key and the directory being built can differ, so the serialisation the description promises does not hold for that path. _The code index is behind this pull request (indexed at `46f1624d923e`), so retrieved context may be out of date._

Evidence and run details

• Models: ladder/vectors-oai3, deepseek-v4.1-flash
• Spend: $0.000941
• Tokens: 519480 input · 8213 output · 2048 cached · 516 embedding
• Updated: 2026-10-26T05:10:30Z

Head	State	Pass summary
135bb8179b80	ready for maintainer review	0 active finding(s), 0 resolved finding(s) (at 2026-10-26T05:10:30Z)

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-26T05:11:22.857393Z	135bb81	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[coderabbitai]

Caution

Review failed

The pull request is closed.

Walkthrough

Lean package staging and compilation now use per-project locks. Compiler outputs are written to temporary files before promotion. New tests check same-project serialization, cross-project concurrency, restaging, and failed or timed-out compilations.

Changes: Lean build synchronization

Layer / File(s)	Summary
Project locks and atomic compiler outputs docker/lean/build.py, docker/lean/test_server_concurrency.py	project_lock(source_dir) shares a lock for callers using the same real source path. build_modules writes .olean and .ilean outputs to temporary files, promotes available outputs after successful compilation, and removes leftover temporaries. Tests check that failed and timed-out compiles leave no .olean file.
Locked package builds and concurrency coverage docker/lean/server.py, docker/lean/test_server_concurrency.py, docker/lean/README.md	build_package locks package staging and module compilation. elaborate uses this helper. Tests cover concurrent checks, restaging, and parallel builds for different projects. The README documents the locking behavior, elaboration concurrency, atomic writes, and deployment constraint.

Priority: Not assessed

Estimated code review effort: 3 (Moderate) | ~20 minutes

Change: Bug fix

Sequence Diagram(s)

sequenceDiagram
  participant elaborate
  participant build_package
  participant project_lock
  participant build_modules
  elaborate->>build_package: stage and build imported modules
  build_package->>project_lock: acquire project lock
  build_package->>build_modules: compile modules
  build_package-->>elaborate: return build directory and Lean path

Loading

Possibly related PRs

• tinyhumansai/supermath#13: Adds Workspace::single for candidate checkouts outside the projects root. PR #21 stages and builds such roots under a lock keyed by their real lean/ path.

Suggested reviewers: tinysweeper

Merge Risk: Low · up to 135bb

A rare output-promotion failure can leave an incomplete build marked fresh, and the documented elaboration limit is inaccurate. Both have localized corrections; the PR is mergeable with those fixes or explicit owner acceptance.

Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

_{A rabbit guards the build queue tight,
While project locks keep paths in line.
Temp files wait, then outputs land,
Two projects compile side by side.
Checks hop through, and tests confirm.}

_{Comment @coderabbitai help to get the list of available commands.}

[tinysweeper]

tinysweeper found nothing blocking. Approving.

Diagnostics

Total spend: $0.0009

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 135bb8179b

ℹ️ 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".