[senamakel]

Summary

Follow-up to #21, which merged before its two review threads were addressed. These are the fixes for those threads.

• Lock wait counts against the request's timeout (Codex P2 on Make the Lean service safe for concurrent checks of one project #21). build_package now acquires the project lock with lock.acquire(timeout=timeout). If the lock isn't free in time it raises subprocess.TimeoutExpired, which run_guarded already maps to status "timeout". The build then gets only the time left after the wait. Before this, a request queued behind a long build could block well past its own timeout.
• The restaging regression test is ordered by events, not sleeps (Codex P1 on Make the Lean service safe for concurrent checks of one project #21). The first compile signals that it has started. The second request edits the source and signals that it is about to build. The compile then waits up to 0.5 s for a restage, signalled after build.stage returns, before re-reading its source. With the lock in place, no restage can run in that window. Without it, one does, and the test fails. The timing can only make the test pass wrongly when the lock is missing, never fail wrongly when it is present.

Public API / behaviour changes

A /check that waits for another request's build of the same project now returns status: "timeout" once its timeout is used up, instead of waiting indefinitely.

Validation

• test_a_request_waiting_for_the_lock_gives_up_at_its_timeout (new) failed on main (the request was still blocked after 3 s with a 0.3 s timeout), and passes now.
• test_a_restage_waits_for_the_build_in_progress (rewritten) failed 3 of 3 runs with the lock temporarily removed, and passes with it.
• python3 -I -W error -m unittest discover -s docker/lean: 39 tests OK, 3 of 3 runs.
• Rust is untouched, so the cargo contract commands were not run.

Refs #21

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

Summary by CodeRabbit

• Bug Fixes
  • Build requests now honor their timeout while waiting for another build to finish.
  • Restaging waits until an in-progress build completes, helping ensure builds use a consistent source state.

[tinysweeper]

Tiny Sweeper review

Reviewed head: 960561156d6c018e901b5c0dc27b3c72b7ddfc3a

Verdict: Ready for maintainer review · Priority: none
Coverage: Reviewed 2 of 2 files.
Pull request purpose (title): Bound the Lean build…

Diagnostics and supporting details

Full summary

Pull request purpose (title): Bound the Lean build-lock wait by the request timeout; deflake the restage test. Tiny Sweeper completed its review; deterministic results follow.

Review snapshot

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

Completeness: Complete
Test assessment: No supported feature-to-test mapping was available; this does not mean tests are absent or passed.

Features

• Modified — Bounded project-lock acquisition in build_package: A request waiting on a busy project's lock can no longer block past its own deadline; it either wins the lock within the timeout or raises `subprocess.TimeoutExpired`, which `run_guarded` maps to a `timeout` status. (docker/lean/server.py def build_package(project, mods, timeout, run=subprocess.run):)

Tests

No supported feature-to-test mapping was produced. Test execution is not inferred.

Findings

No active actionable findings.

Before merge

None.

Agent review details

critique

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The bounded acquire and remaining-time derivation are traced as coherent: the lock is released only after the build returns, so a request that waited sees a correspondingly shorter compile budget and the timeout is charged once; no reachable input was found that makes the code misbehave and no rule violation was found. The lane notes it could not read the call sites of `build_package` and did not confirm whether any caller relies on the old total-time semantics.
• Lane summary: The change replaces `with build.project_lock(...)` with a bounded `acquire(timeout=...)` and derives the build's remaining time from the same monotonic start, raising `subprocess.TimeoutExpired` — which `run_guarded` already maps to a `timeout` status — when the lock is not won in time. I traced the interaction with `build_modules`, which passes `remaining` to `run(..., timeout=...)`; because the lock is released only after the build returns, a request that waited for the lock now sees a correspondingly shorter compile budget, so the timeout is charged once rather than twice. I could not read the parts of `docker/lean/server.py` around the call sites of `build_package`, and did not confirm whether any caller relies on the old total-time semantics, but I found no reachable input that makes the code misbehave and no rule violation. _The code index is behind this pull request (indexed at `135bb8179b80`), so retrieved context may be out of date._

security

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The lock is still held across staging and the build and released in a `finally`, so no path leaks the lock; `time` and `subprocess` are already imported in server.py. No reportable defect found.
• Lane summary: The change converts the blocking `with build.project_lock(...)` in `build_package` into an explicit `acquire(timeout=...)`/`release()` pair so a request waiting on a busy project's lock is bounded by its own deadline, and rewrites the affected concurrency tests to be event-ordered plus adds a stalling-waiter test. The lock is still held across staging and the build and released in a `finally`, so no path leaks the lock; `time` and `subprocess` are already imported in server.py. No reportable defect found. _The code index is behind this pull request (indexed at `135bb8179b80`), so retrieved context may be out of date._

tests

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Lane summary: `build_package` now takes the project lock with a deadline and passes the remaining budget to `build_modules`, and the diff adds a test that the waiter gives up at its timeout (failing if `lock.acquire` is ever called without one) plus an event-ordered rewrite of the restage test. The new branch and its error path are exercised, and the `TimeoutExpired` it raises is already mapped to `status: timeout` by `run_guarded`, so I found no defect worth blocking on. _The code index is behind this pull request (indexed at `135bb8179b80`), so retrieved context may be out of date._

commits

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: No sensitive content in committed files.
• Lane summary: No sensitive content in committed files. _The code index is behind this pull request (indexed at `135bb8179b80`), so retrieved context may be out of date._

description

• Conclusion: Success
• Scope reviewed: all assigned evidence
• Positive: The code matches the description: `build_package` acquires the project lock under the request's timeout and passes the remaining time to the build, and the restage test rewrite plus lock-timeout test are present; no defect that would fail or misbehave for a reachable input was found.
• Lane summary: The change makes `build_package` acquire the project lock under the request's timeout and pass the remaining time to the build, plus rewrites the restage test to be event-ordered and adds a lock-timeout test; the code matches the description and I found no defect that would fail or misbehave for a reachable input. _The code index is behind this pull request (indexed at `135bb8179b80`), so retrieved context may be out of date._

Evidence and run details

• Models: ladder/vectors-oai3, deepseek-v4.1-flash
• Spend: $0.001863
• Tokens: 250558 input · 5236 output · 80896 cached · 178 embedding
• Updated: 2026-10-26T05:24:13Z

Head	State	Pass summary
960561156d6c	ready for maintainer review	0 active finding(s), 0 resolved finding(s) (at 2026-10-26T05:24:13Z)

[coderabbitai]

Caution

Review failed

The pull request is closed.

Walkthrough

build_package now counts project-lock wait time against the request timeout. Concurrency tests verify restaging coordination and confirm that a request waiting for the lock exits with a timeout.

Changes: Timed build lock handling

Layer / File(s)	Summary
Lock timeout and concurrency coverage docker/lean/server.py, docker/lean/test_server_concurrency.py	build_package uses timed lock acquisition, passes the remaining timeout to build.build_modules, and releases the lock in a finally block. Tests coordinate restaging with events and verify that lock waiting can time out.

Priority: Not assessed

Estimated code review effort: 2 (Simple) | ~12 minutes

Change: Bug fix

Sequence Diagram(s)

sequenceDiagram
  participant BuildRequest
  participant build_package
  participant ProjectLock
  participant build_modules
  BuildRequest->>build_package: Start build with request timeout
  build_package->>ProjectLock: Acquire lock within timeout
  ProjectLock-->>build_package: Lock acquired
  build_package->>build_modules: Build with remaining timeout
  build_package->>ProjectLock: Release lock in finally
  ProjectLock-->>build_package: Timeout if lock is not acquired in time

Loading

Possibly related PRs

• tinyhumansai/supermath#21: Introduced build_package, per-project locks, and concurrency tests that this change extends.

Suggested reviewers: tinysweeper

Merge Risk: Low · up to 96056

A request can occasionally report success after its timeout, and the restaging test may miss the regression it is meant to catch. These are bounded issues to fix or explicitly accept before merging.

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 checks the waiting clock,
Then hops aside to free the lock.
The build gets time that still remains,
While tests keep source edits in their lanes.
The bunny thumps: timed builds are clear!}

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

[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:24:30.530428Z	9605611	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.

[tinysweeper]

tinysweeper found nothing blocking. Approving.

Diagnostics

Total spend: $0.0019