From 6e4cc40caa54f8ee3dd5a70dcb308b8f252915c3 Mon Sep 17 00:00:00 2001 From: Steven Enamakel Date: Mon, 26 Oct 2026 05:16:40 +0000 Subject: [PATCH 1/4] test(lean): cover restage ordering and lock timeout Replace the sleep-based ordering in the restage test with events so the edit and second request are guaranteed to land before the first compile reads its source, and add a test asserting that a request waiting on the project lock gives up at its own timeout rather than blocking. Auto-committed-on: cuttlefish Co-authored-by: Medulla --- docker/lean/test_server_concurrency.py | 34 +++++++++++++++++++++++--- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/docker/lean/test_server_concurrency.py b/docker/lean/test_server_concurrency.py index 02db84b..3fc8dc0 100644 --- a/docker/lean/test_server_concurrency.py +++ b/docker/lean/test_server_concurrency.py @@ -99,26 +99,54 @@ def same_project_serialises(self, volume): self.assertEqual(len(probe.compiles), 2, "the later requests reuse what the first built") def test_a_restage_waits_for_the_build_in_progress(self): + # Ordered by events, not sleeps: the edit lands and the second request + # is on its way before the first compile reads its source back, and + # the compile gives the restage a generous window to run under it. project = self.project("p", volume=False) source = os.path.join(project, "lean", "Supermath", "Shared.lean") + compiling, requested, restaged = threading.Event(), threading.Event(), threading.Event() seen = [] + stage = B.stage + + def watched_stage(*args, **kw): + if compiling.is_set(): + restaged.set() + return stage(*args, **kw) def run(argv, **kw): before = read(argv[-1]) - time.sleep(0.15) + if not compiling.is_set(): + compiling.set() + requested.wait(5) + restaged.wait(0.5) # times out unless the restage runs under this compile seen.append(before == read(argv[-1])) return Probe(0)(argv, **kw) def edit_then_build(): - time.sleep(0.05) + compiling.wait(5) write(source, "import Mathlib\n-- edited\n") os.utime(source, (2_000_000_000, 2_000_000_000)) + requested.set() S.build_package(project, ["Supermath.Top"], 10, run) - errors = in_threads([lambda: S.build_package(project, ["Supermath.Top"], 10, run), edit_then_build]) + B.stage = watched_stage + try: + errors = in_threads([lambda: S.build_package(project, ["Supermath.Top"], 10, run), edit_then_build]) + finally: + B.stage = stage self.assertEqual(errors, []) self.assertTrue(seen and all(seen), "a source changed under a compile") + def test_a_request_waiting_for_the_lock_gives_up_at_its_timeout(self): + project = self.project("p", volume=True) + lock = B.project_lock(os.path.join(project, "lean")) + with lock: + started = time.monotonic() + with self.assertRaises(subprocess.TimeoutExpired): + S.build_package(project, ["Supermath.Top"], 0.3, Probe(0)) + waited = time.monotonic() - started + self.assertLess(waited, 2.0, "the wait for the lock ignored the request's timeout") + def test_checks_of_different_projects_build_at_the_same_time(self): first, second = self.project("a", True), self.project("b", False) both = threading.Barrier(2, timeout=5) From 23c27ac06b307aec8419d6cc7ff455ee78f562f3 Mon Sep 17 00:00:00 2001 From: Steven Enamakel Date: Mon, 26 Oct 2026 05:21:10 +0000 Subject: [PATCH 2/4] test: run lock timeout check on a separate thread The lock timeout test now issues the build from a worker thread while the main thread holds the project lock, so the request's own timeout is what ends the wait. The previous version measured elapsed time inside the locked section, which could pass or fail depending on scheduling rather than on the timeout being honoured. Auto-committed-on: cuttlefish Co-authored-by: Medulla --- docker/lean/test_server_concurrency.py | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/docker/lean/test_server_concurrency.py b/docker/lean/test_server_concurrency.py index 3fc8dc0..761fbd8 100644 --- a/docker/lean/test_server_concurrency.py +++ b/docker/lean/test_server_concurrency.py @@ -139,13 +139,23 @@ def edit_then_build(): def test_a_request_waiting_for_the_lock_gives_up_at_its_timeout(self): project = self.project("p", volume=True) - lock = B.project_lock(os.path.join(project, "lean")) - with lock: - started = time.monotonic() - with self.assertRaises(subprocess.TimeoutExpired): + outcome = [] + + def request(): + try: S.build_package(project, ["Supermath.Top"], 0.3, Probe(0)) - waited = time.monotonic() - started - self.assertLess(waited, 2.0, "the wait for the lock ignored the request's timeout") + outcome.append("built") + except subprocess.TimeoutExpired: + outcome.append("timeout") + + with B.project_lock(os.path.join(project, "lean")): + waiter = threading.Thread(target=request) + waiter.start() + waiter.join(3) + gave_up = not waiter.is_alive() + waiter.join(5) + self.assertTrue(gave_up, "the wait for the lock ignored the request's timeout") + self.assertEqual(outcome, ["timeout"]) def test_checks_of_different_projects_build_at_the_same_time(self): first, second = self.project("a", True), self.project("b", False) From 7b92acc67fd97be1900b3841cb8d6e1963573d4e Mon Sep 17 00:00:00 2001 From: Steven Enamakel Date: Mon, 26 Oct 2026 05:21:24 +0000 Subject: [PATCH 3/4] fix(lean): count lock wait against the build timeout The project lock is now acquired with a timeout instead of blocking indefinitely, so a request that cannot get the lock in time raises subprocess.TimeoutExpired rather than hanging. The build then runs with only the time remaining from the original timeout. Auto-committed-on: cuttlefish Co-authored-by: Medulla --- docker/lean/server.py | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/docker/lean/server.py b/docker/lean/server.py index d289a4b..1449f6f 100644 --- a/docker/lean/server.py +++ b/docker/lean/server.py @@ -120,10 +120,21 @@ def build_package(project, mods, timeout, run=subprocess.run): staging cannot rewrite sources under a compile. Requests for other projects take other locks and build in parallel. The lock is released before the caller elaborates: that only reads the finished oleans. + + Waiting for the lock counts against `timeout`: a request that cannot get + it in time raises `subprocess.TimeoutExpired`, and the build gets only + what is left. """ - with build.project_lock(os.path.join(project, "lean")): + lock = build.project_lock(os.path.join(project, "lean")) + started = time.monotonic() + if not lock.acquire(timeout=max(timeout, 0)): + raise subprocess.TimeoutExpired("build " + project, timeout) + try: + remaining = max(timeout - (time.monotonic() - started), 0.001) lean_dir = ensure_package(project) - return lean_dir, build.build_modules(lean_dir, mods, PACKAGES, timeout, run) + return lean_dir, build.build_modules(lean_dir, mods, PACKAGES, remaining, run) + finally: + lock.release() def run_guarded(operation): From 960561156d6c018e901b5c0dc27b3c72b7ddfc3a Mon Sep 17 00:00:00 2001 From: Steven Enamakel Date: Mon, 26 Oct 2026 05:21:54 +0000 Subject: [PATCH 4/4] test(lean): capture stage result before signalling restaged The watched stage wrapper now calls the underlying stage function before checking the compiling flag, so the restaged event is only set once the stage has actually run. This avoids a race where the event could be signalled before the stage result was produced. Auto-committed-on: cuttlefish Co-authored-by: Medulla --- docker/lean/test_server_concurrency.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docker/lean/test_server_concurrency.py b/docker/lean/test_server_concurrency.py index 761fbd8..62bc805 100644 --- a/docker/lean/test_server_concurrency.py +++ b/docker/lean/test_server_concurrency.py @@ -109,9 +109,10 @@ def test_a_restage_waits_for_the_build_in_progress(self): stage = B.stage def watched_stage(*args, **kw): + staged = stage(*args, **kw) if compiling.is_set(): restaged.set() - return stage(*args, **kw) + return staged def run(argv, **kw): before = read(argv[-1])