pre-push(17.5): say when the engine cannot finish, and offer it in the background

--engine inline|background|off (hook: OUSAST_PUSH_ENGINE). background returns
after the quick tier and starts one detached explicit replay of the same base
and head (push/background.py), one at a time per artifact directory; its
artifact lands under <artifact dir>/engine/<repo key>/<head>.json and the next
run prints "Engine result for <head> from the previous push" once. A deadline
miss says so in one line naming the deadline and the background option. No
engine speed work. Requirement 9.5.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01EmM1j46qgKMh3zqD1QMwEo
This commit is contained in:
Marius Ciepluch
2026-10-02 22:31:14 +02:00
co-authored by Claude Opus 5.5
parent 511de4b75f
commit 66357ffea1
9 changed files with 392 additions and 10 deletions
+1
View File
@@ -58,6 +58,7 @@ GLOSSARY: dict[str, str] = {
"regions_truncated": "only the highest-ranked regions were examined (--max-regions)",
"files_unparsed": "some files could not be parsed by the engine",
"engine_off": "engine checks were switched off for this run (--engine off)",
"engine_background": "engine checks run in the background after this push; the next push shows their result",
"cross_partition_semantics_unresolved": "flows between languages in this repository are not followed",
"resolution": "the pushed ref could not be resolved ({detail})",
"push_input_failed": "the push input could not be read ({detail})",