Repository navigation
Make SSH stages recoverable after local interruptions - #68
hyperpolymath wants to merge 12 commits into
Conversation
1a1f14f to
534a459
Compare
534a459 to
24f42ec
Compare
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 24f42ec8f1
ℹ️ 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".
Retain phylogeny outputs only when the journal identity and retrieval receipt verify them. Clear stale outputs before network access so an unavailable host or failed replacement cannot leave an old tree available for placement. Upload command and worker scripts to unique temporary names, verify their checksums, and rename them into place before launch. Exercise interrupted uploads, recovery and cancellation, and valid versus stale phylogeny receipts. Report each unit file and remote regression in test logs, and bound the CI test step to make a stalled recovery regression diagnosable.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f0992480f9
ℹ️ 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".
A status probe briefly owns run.lock. A detached worker could lose its nonblocking acquisition to that probe and exit, leaving the caller polling a ready attempt indefinitely. Tolerate the brief probe and acknowledge the worker's durable launch marker before polling begins. Missing startup acknowledgement is now a bounded, retryable failure. Force the conflicting lock order in a regression, require output retrieval and cleanup, and allow cold CI compilation during fixture startup.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 776952fe15
ℹ️ 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".
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
A callback that catches every exception swallowed a cancellation, and a completed attempt whose retrieval failed left the stage wedged: its exit marker made `start` refuse and a zero exit made `retry` refuse. Reclaim a superseded preparation whose worker was never installed, and reuse the live master when cancelling instead of opening a second connection that a password-only deployment cannot answer. The worker now treats a failure to publish its exit marker, and a detached child that exits before recording one, as a retryable failure rather than leaving the controller polling a state that cannot appear. Recovery replays the retained remote log when the stage truncated its local copy, and the internal protocol runs under LC_ALL=C so a translated diagnostic cannot be parsed as a protocol reply. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
The recovery-path fixture had already finished its command, so the interrupt test could only show that the journal was removed, not that a live attempt was stopped. Run the workload until it is cancelled instead, and take the attempt directory from the fixture rather than from a receipt it deliberately does not have. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Wrapping the capture command in setenv changed its argv, so a caller that rewrites the first element to install a control path and configuration file -- the SSH recovery fixture does exactly that -- rewrote the wrapper instead of ssh and the fixture could not connect. The locale is not this change's concern; drop it rather than change the contract the tests rely on. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
`setsid` forks, so the PID `start` tracked exits at once and the liveness check I added treated every successful launch as a failure. Probe the one thing that actually predicts the detached child's death -- whether its log can be opened -- and leave the existing launch-marker wait in place. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Address the unresolved review threads on #68. Vary: a completed attempt whose outputs were never retrieved is now prepared by a new worker `replay` request instead of `retry`. `retry` refuses a successful attempt, so once the exit marker was kept every later run called a request that always failed before reaching the fetch and the stage stayed wedged. Keeping the marker is what makes the attempt retrievable, including after a required output is reported missing on a zero exit, so the fetch path and the marker now agree. - Report required outputs a zero-exit attempt did not write, keep the zero-exit barrier, and retrieve from the same attempt on the next run. - Replay the retained remote log before cleanup removes it, byte-wise and idempotently, and stop the DADA2 stages truncating a log whose journal is retained (matching the phylogeny stage). - Retry `start` when a status probe transiently owns the execution lock, which previously failed a launch whose worker had given up waiting. - Tolerate the runner's own journal and owner lock in the log drift guard, and model the replay transition in the Agda protocol proof. - Post the loopback-SSH suite's output as a CI annotation, because its job log is not readable from outside GitHub. Regenerated per-workflow journals need no migration: the runner only issues `replay` for an attempt whose marker it retained. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
First run with a working SSH step, so these surfaced for the first time. - Superseded attempts: `cleanup` refuses an attempt that is already terminal, so reclaiming an `exit 0` preparation left its directory behind. Add `reclaim`: a worker-installed but non-running attempt is removed directly, while a running one still goes through `cancel`, which stops the process group before removing anything. - Log drift guard: the journal's owner lock is seen by the scan too. - Tests: three pre-existing cases could not pass as written. The retrieval case changed the command (a different identity, so it superseded rather than replayed); the reclamation case used a different log name (no journal was superseded); the swallowed-interrupt case read the wrong base directory and expected launching where it had already been killed. Each now exercises the path it describes. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
- A one-shot command cannot both omit its output and be retrievable; the missing-required-output case has its own test, so the wedging test uses an interrupted download, which is the other way an attempt completes with no receipt. - A callback that swallows an InterruptException is indistinguishable from one that finished, so the case is named for what it actually guarantees: an interrupt with a live workload cancels it and removes the attempt. The interrupt unwrapping itself is unit-tested beside it. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
fetch wraps an interrupted task in TaskFailedException, so the assertion now inspects the exception the stage raised. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
…ord (#13) Closes out the three open Codex review threads and the Codecov findings on `JoshuaJewell/MetaManifold-WebUI#68`. - `notes/0004-pr68-ssh-recovery-coverage.patch`: one `git format-patch` commit onto PR head `5115109`, adding regression cases for all 18 changed lines Codecov reported uncovered (12 in `remote_session.jl`, 5 in `phylogeny.jl`, 1 in `remote_exec.jl`). Verified with `git apply --check` and `git am` in a clean shallow clone, plus a token-level Julia structure check. - `notes/pr68-ssh-recovery-review.md`: maps each of the three review findings to the fixes already present at `5115109`, records the exact Codecov figures, the four green CI checks, `mergeable_state: clean`, and the permission boundary that prevents this session from resolving the threads or merging the external PR. - `notes/README.md`: indexes the two new files. Production code in this repository is unchanged; the proofs and Julia package CI should be unaffected. --------- Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
…ps (upstream PR 68) (#323) ## Change and reason [JoshuaJewell#68](JoshuaJewell#68) has two open items at head `5115109`: - Codecov reports 94.59% patch coverage, with 18 lines missing in `remote_session.jl` (12), `phylogeny.jl` (5) and `remote_exec.jl` (1). - One review finding is still open: "Retry attempts that finish without required outputs". A command that exits 0 without a required output wedged the stage. `replay` cannot fix this, because it cannot make a file appear that the command never wrote. **Production change** (`src/pipeline/remote_session.jl`, one branch): - A zero exit that omits a required output is now retired. The attempt is cleaned up and its journal is archived as `*.missing-outputs-<uuid>`. An explicit rerun then launches a fresh attempt. - If the host refuses the cleanup, the journal stays. The remote attempt keeps its owner, and the next run retries the retirement. - This is the existing `expire-succeeded` transition of the Agda protocol model (`succeeded 0 n ↦ removed 0 n`). No new transition is needed. Please confirm that this reading of the model is the intended one. **Tests** (three files): - The retirement and the fresh relaunch, and the refused retirement that keeps the journal. - A durable cancel request stops the old attempt of the same stage before a new one launches. - Receipt recovery replays the remote log before cleanup removes it. - The other lines that Codecov listed: the fetch error, a refused sweep, both superseded-journal branches, the owned-transport close, phylogeny's local and remote log branch, and the quoting in `verify_remote_sizes`. This work starts from an earlier patch that was never run (`notes/0004-pr68-ssh-recovery-coverage.patch` in MetaManifold-Evidence). I ran it, and added three things it lacked: the refused-retirement test, the same-stage cancel test, and the log-replay assertion. This pull request targets the branch of upstream PR 68. A merge here updates that pull request. ## Validation Julia 1.12.5, R 4.3.3, Linux, from the repository root. 1. Coverage, with the same flags as CI: ```bash julia --project=. -t 2 --code-coverage=user --compiled-modules=no test/runtests.jl test_remote_stages.jl test_phylogeny.jl ``` Result: 426 pass, 0 fail. Every instrumented line that this branch adds since upstream `89be534` is covered: `remote_session.jl` 295 of 295, `phylogeny.jl` 7 of 7, `remote_exec.jl` 1 of 1. 2. Planted faults. I ran 14 deliberate corruptions of the changed lines, one at a time. The suite caught 12 at once. Two survived: a skipped cancel on a durable cancel request, and a skipped log replay on receipt recovery. I added a test for each, and each test now fails with its fault in place. Result: 14 of 14 caught. 3. Baseline. At `5115109`, three existing "cancel kills the process group" assertions fail in my sandbox, with and without this change. The cause is the sandbox: its PID 1 is slow to reap killed processes, so `kill -0` on the group still succeeds for a moment. Inside a private PID namespace (`unshare --pid --fork --mount-proc`) all tests pass. The upstream CI passed these tests at `5115109`. Not run: `test/remote_ssh.jl` (needs a real SSH server), the Agda audit (no Agda in my sandbox; the model is unchanged), the full suite, and the frontend tests. No workflow runs on this pull request, because `ci.yml` on this branch starts only for pull requests into `main`. The upstream CI and Codecov run after the merge. ## Scope - One production branch changes behaviour, as described above. Everything else is tests. - The three open review threads on PR 68 need a reply and a resolve by someone with write access to the upstream repository. Draft replies are in `notes/pr68-ssh-recovery-review.md` in MetaManifold-Evidence. - These regressions are Linux only (`flock`, `setsid`). The suite skips them elsewhere. - No lockfile change. ## Contribution checks - [x] I followed [CONTRIBUTING.md](https://github.com/JoshuaJewell/MetaManifold-WebUI/blob/main/CONTRIBUTING.md). - [x] This branch starts at the head of PR 68 (`5115109`) and contains no merges from fork main. - [ ] Every commit is signed and shows as Verified. (The managed signing identity decides this.) - [ ] CI has run and passes. (No workflow runs here. See Validation.) - [x] Existing licensing, citation and acknowledgement text is unchanged. --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZoTPXfxg1C85rVNx78)_ Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Stopping the local server during an SSH stage previously left its workflow marked running and could kill the remote command and delete its files. The shared runner now journals one detached attempt per workflow, allowing an explicit rerun to reconnect to live work or retrieve completed outputs without another upload.
Closes #66.
-redo. Preserve published outputs only when both the journal identity and receipt match; otherwise clear them before contacting SSH so a failed new attempt cannot expose an old tree.--safe --without-KAgda protocol model in the existing proof suite. No runtime dependency or lockfile change.Local validation used Julia 1.12.5, R 4.5.0, bun 1.4.3, Agda 2.6.4.3 and standard-library 2.1:
The final targeted Julia run passed 465 assertions; the standalone production-worker protocol suite passed 114; the actual SSH suite passed 15; frontend tests passed 65. The frontend build, Agda tree, axiom/reachability audit, Bash syntax check and REUSE 6.2.0 passed. The targeted local invocation used
--compiled-modules=existingand an isolated R 4.5.0 runtime. CI uses the repository's pinned bun 1.3.10.An additional local experiment passed 9 assertions with the pinned IQ-TREE 3.1.4 binary (archive checksum matched the existing pin). Through the production runner over a local transport, a 24-sequence alignment ran with
-m GTR+G -b 10 -nt 2 -seed 7 -cptime 1. After a checkpoint appeared, the owned worker was killed; retry reused it without uploading, IQ-TREE reported that it resumed the checkpoint and restored its initial tree, and a completed tree was retrieved. This experiment adds no runtime or CI dependency.Full CI run 42411663705 passed on 776952f: 3,147 assertions passed, with 5 existing optional-tool skips, including the integration and server smoke suites. The separate real-SSH test, frontend build and tests, Agda proofs, REUSE compliance and coverage check also passed. The complete biological phylogeny end-to-end test skipped both locally and in CI because not all five external tools were installed; the additional pinned IQ-TREE checkpoint experiment above covers the tool involved in this issue. Unit-file and remote-regression progress is logged, and the CI test step has a 25-minute limit.
The Agda theorems concern the explicit protocol model, not a proved refinement to Julia/Bash. OS locking, filesystem/process semantics, SSH, SHA-256 collision resistance, fresh attempt identifiers and a stable remote runtime remain assumptions. Recovery is an explicit rerun, not automatic server-startup resubmission. Tools without internal checkpoints restart after a remote-process failure; failed-work expiry requires later runner activity. See
docs/guide/remote-execution.mdfor the theorem-to-implementation map and operational limits. No unconditional end-to-end correctness claim is made.