fix(sync): push deletes only with --force and skips remote-deleted configs (#792 G, H)

CLAUDE.md

@@ -962,6 +962,10 @@ kbagent sync pull --project ALIAS [--all-projects] [--force] [--theirs] [--dry-r
 kbagent sync status [--directory DIR]
 kbagent sync diff --project ALIAS [--all-projects] [--directory DIR] [--branch ID]
 kbagent sync push --project ALIAS [--all-projects] [--dry-run] [--force] [--allow-plaintext-on-encrypt-failure] [--branch ID] [--no-name-drift-warnings]
+# sync push --force (#792): push deletes remote configs and rows ONLY with --force; a plain push lists them
+#   under skipped_deletions (+ skipped_deletions_reason), also in --dry-run, whose summary.deleted counts only
+#   what push would delete. A config/row deleted on the remote since the last pull diffs as remote_deleted and
+#   is never re-created (it lands in skipped). Version gate in gotchas.md.
 # sync push (since 0.91.0, #686): the manifest baseline `pull_config_hash` is stamped from the API
 #   response (or a read-back), never from disk -- push-deployed multi-statement SQL transformations
 #   (and anything disabled in the UI whose local YAML lacks `is_disabled`) no longer show permanent

formal/sync/README.md

@@ -77,13 +77,13 @@ explores traces of up to 5 actions. BFS returns the shortest counterexample.
 | I7 never-fetched entry never deleted | **holds** (104,809 states, never-fetched initial entry) |
 | I1 no double create | violated: a promote push re-creates configs on every run; a resurrect followed by an `ENCRYPTION_FAILED` abort also creates a copy |
 | I2 push deletes only user-removed dirs | violated: **pull's stale-entry sweep deletes a directory the same pull just wrote, and the next push deletes the live remote config** |
-| I2b delete requires `--force` | violated: `push()` never reads `force` (S1) |
+| I2b delete requires `--force` | violated: `push()` never reads `force` (S1). Fixed in the code (G); the model is unchanged |
 | I5 pull keeps local work | violated: a remote delete plus a local edit ends with plain or `--force` pull deleting the edited directory silently |
 | I6 push then diff is clean | violated on `--branch` promote (finding D, since fixed in the engine; the TLA model is unchanged). Holds on production only (30,334 states) |
 | I8 manifest matches disk | violated: the stale sweep, and a promote write-back that records a `devt/` entry for a file in `main/` |
 | I9 an aborted push is atomic | violated (strong reading): the changes before the failing one reached the API and the manifest was never saved |
 | I11 no lost remote update | violated: an adopted file with a config id is diffed 2-way, so push reverts a UI edit |
-| I11b no silent resurrect | violated: a remote delete followed by any push re-creates the config, even with no local edit (S2) |
+| I11b no silent resurrect | violated: a remote delete followed by any push re-creates the config, even with no local edit (S2). Fixed in the code (H); the model is unchanged |
 | I12 a pull resolves REMOTE MODIFIED | violated: after a cosmetic edit, plain pull skips the file forever and `--force` raises a conflict (S3) |
 
 Each violation was checked against the code. The main ones were replayed
@@ -105,8 +105,8 @@ the regression test for each in `tests/test_sync_formal_counterexamples.py`.
 | D | `sync push --branch dev` (promote) creates another dev copy of a prod-only config on every push. **Fixed** (fix/792-dev-promote-duplicates): on the promote path the target-branch entry shadows the production entry for the same `main/` dir (`sync/branch_scope.py::_promoted_paths`) | TLA I6/I1 | HIGH | `test_d_promote_push_is_idempotent`, `test_d_promote_push_diff_is_clean_and_edits_update_the_dev_copy` (regression guards) |
 | E | An untracked file carrying a config id (`config new --push --output-dir` scaffold / adopted orphan) is diffed 2-way: push overwrites a UI edit made after the scaffold was written | TLA I11 | MED | `test_e_adopted_scaffold_push_does_not_overwrite_remote_edit` |
 | F | A push aborted by `ENCRYPTION_FAILED` leaves the manifest unsaved; the retry duplicates the change(s) the aborted push already applied | TLA I1b (model trace only; replayed live for this pilot) | MED | `test_f_aborted_push_does_not_duplicate_already_created_config` |
-| G | `sync push` deletes remote configs with no `--force`; the CLI help text says `--force` gates deletion (soft delete to trash since 0.89.0, restorable) | Spec S1, Lean F1, TLA I2b | MED (product decision) | `test_g_push_without_force_does_not_delete_remote_config` |
-| H | A config deleted remotely by another actor is silently re-created by the next push, no warning | Spec S2, Lean F2, TLA I11b | MED | `test_h_push_does_not_silently_resurrect_deleted_config` |
+| G | `sync push` deletes remote configs with no `--force`; the CLI help text says `--force` gates deletion (soft delete to trash since 0.89.0, restorable) | Spec S1, Lean F1, TLA I2b | MED -- **fixed** (push deletes only with `--force`) | `test_g_push_without_force_does_not_delete_remote_config` |
+| H | A config deleted remotely by another actor is silently re-created by the next push, no warning | Spec S2, Lean F2, TLA I11b | MED -- **fixed** (diff reports `remote_deleted`, push skips it) | `test_h_push_does_not_silently_resurrect_deleted_config` |
 | I | Moving a config's directory by hand (`mv`/`git mv`) is seen as remote DELETE + CREATE under a new id | Lean F3 | LOW-MED | `test_i_moving_config_dir_is_not_delete_plus_create` |
 | J | `sync pull --branch dev` reports untouched production configs as "removed" | Spec S4 | LOW | `test_j_branch_scoped_pull_does_not_report_other_branch_configs_removed` |
 | K | A cosmetic local edit (raw vs normalized hash) blocks pull from ever applying a real remote change; `--force` raises a conflict | Spec S3, TLA I12 | LOW (documented, conservative behavior) | `test_k_cosmetic_edit_is_conservative_not_unsafe` (unmarked regression guard, not xfail) |
@@ -120,10 +120,11 @@ and is deleted only by `--theirs`. That is what the I2 (sweep half), I5 and I8
 TLC/Lean rerun still reports them until the model's `Pull` is updated to match.
 Their tests are ordinary regression guards now.
 
-E, F, H and I reproduce on current code and are `xfail(strict=True)` (D is fixed) --
-flipping to a hard failure the moment a fix lands is the point: delete the
-`xfail` marker to adopt the fix. G is kept `xfail` too even though the fix
-direction is a product decision (see the test's docstring). J reproduces and
+E, F and I reproduce on current code and are `xfail(strict=True)` (D, G and H
+are fixed) -- flipping to a hard failure the moment a fix lands is the point:
+delete the `xfail` marker to adopt the fix. F's test now reaches the aborted
+create through a promote push, because push no longer re-creates the
+remote-deleted config its first version used. J reproduces and
 is `xfail`. K is deliberate, documented behavior, so it is an ordinary
 (unmarked) regression guard instead. B is fixed: its marker was removed
 and the test is now an ordinary regression guard.

plugins/kbagent/agents/keboola-expert.md

@@ -306,7 +306,10 @@ its absence is NOT a promise the entry is version-independent (see §1 Rule 6).
   `is_disabled: true` in `_config.yml` = config disabled (absent = enabled); a
   `never_fetched` warning on diff/push = run `sync pull` first; a non-zero
   `summary.orphaned` (0.89.0+, #649) = the manifest is targeted at another
-  branch's tree -- `sync pull` to re-target, never push. `sync status`
+  branch's tree -- `sync pull` to re-target, never push. Since vNEXT (#792)
+  `sync push` deletes only with `--force` (else `skipped_deletions`), and a
+  `- REMOTE DELETED` diff line = deleted on the remote, push never re-creates
+  it: `sync pull`, or `config restore` to keep it. `sync status`
   is local-only -- audit real drift with `sync diff`. On <= 0.90.1 a
   `~ REMOTE MODIFIED ... codes changed` on a config nobody touched is usually
   PHANTOM (issue #686: push stamped the baseline from disk); fixed in 0.91.0 --

plugins/kbagent/skills/kbagent-cicd-migration/SKILL.md

@@ -259,6 +259,8 @@ for the full mapping from the old `secrets.KBC_SAPI_TOKEN_*` / `vars.KBC_*` sche
   push is fail-closed by design.
 - `sync push --force` deletes remote configs removed locally. It is wired to
   the `allow_delete` workflow input (default off). Treat it like the old `--force`.
+  Without it push deletes nothing and lists the deletions (since vNEXT; older
+  kbagent deleted without `--force`, so `allow_delete` off did not stop them).
 - Tokens live **only** in GitHub secrets and are injected as env vars per step; the
   generated workflows never write a `config.json` to disk.
 - **Never run `--all-projects` in a directory that also holds a flat single-project

plugins/kbagent/skills/kbagent-promotion-pipeline/SKILL.md

@@ -40,19 +40,24 @@ two Storage API tokens (source, destination):
    (using a PAT, not the default token -- see
    [references/secrets-setup.md](references/secrets-setup.md)).
 2. **Validate** (`kbagent-promote-validate.yml`, on the PR) runs
-   `sync push --dry-run --project __env__ --directory <dir>` against the
+   `sync push --dry-run --force --project __env__ --directory <dir>` against the
    **destination** project's token, once per configured pipeline (the
    `paths:` trigger only gates whether the workflow runs at all, not which
    pipeline steps execute inside it -- every pipeline's dry-run always runs)
    -- this is the cross-project diff: *if this PR merges, here is exactly what
    changes in the destination project.* Read this before approving.
 3. **Push** (`kbagent-promote-push.yml`, on push to `main`) runs, in a
-   **separate job per pipeline**, `sync push --project __env__ --directory
+   **separate job per pipeline**, `sync push --force --project __env__ --directory
    <dir>` against the **destination** project's token, each job gated by the
    `prod` GitHub Environment (add required reviewers there -- every job run
    gets its own separate approval, so approving one pipeline never approves
    another).
 
+Both steps pass `--force`, so a config deleted in the source is deleted in
+the destination too. Without it `sync push` deletes nothing *(since vNEXT,
+#792)*; a pipeline generated before that relied on push deleting without
+`--force`, so regenerate it or add `--force` to both steps by hand.
+
 `main` therefore always represents "the last thing approved and pushed to
 every destination project" -- the reviewable source of truth the whole repo
 is built around. A promotion is: pull opens a PR -> validate shows the

plugins/kbagent/skills/kbagent-promotion-pipeline/scripts/generate_promotion_pipeline.py

@@ -10,12 +10,15 @@
      Pulls every pipeline's directory from its SOURCE project and opens/updates
      one PR against the main branch with the combined diff.
   2. kbagent-promote-validate.yml (pull_request against main)
-     For every pipeline, runs `sync push --dry-run` against the DESTINATION
-     project -- this is the cross-project diff: "if this PR merges, here is
-     exactly what changes in the destination project."
+     For every pipeline, runs `sync push --dry-run --force` against the
+     DESTINATION project -- this is the cross-project diff: "if this PR merges,
+     here is exactly what changes in the destination project."
   3. kbagent-promote-push.yml   (push to main, environment-gated)
      Pushes every pipeline's directory to its DESTINATION project once the PR
-     has merged.
+     has merged, with `--force`: a config deleted in the SOURCE is deleted in
+     the DESTINATION too. Without `--force`, `sync push` deletes nothing
+     (since vNEXT, #792), and the validate dry-run passes it for the same
+     reason, so it shows what the push does.
 
 Each pipeline needs two Storage API token secrets (`KBC_TOKEN_<NAME>_SOURCE` /
 `KBC_TOKEN_<NAME>_DEST`) and uses kbagent's `KBAGENT_PROJECT_FROM_ENV=1` /
@@ -364,7 +367,7 @@ def gen_validate(pipelines: list[Pipeline]) -> str:
         _pipeline_step(
             p,
             "Destination dry-run",
-            "push --dry-run",
+            "push --dry-run --force",
             p.dest_token_secret,
             p.dest_stack_url,
             json_output=True,
@@ -414,7 +417,9 @@ def _push_job(p: Pipeline) -> str:
         f"{_INSTALL_TOKEN}"
         "      # `sync push` encrypts #-secrets fail-closed by default. Do NOT add\n"
         "      # --allow-plaintext-on-encrypt-failure in CI.\n"
-        f"{_pipeline_step(p, 'Push', 'push', p.dest_token_secret, p.dest_stack_url)}"
+        "      # --force: a config deleted in the source is deleted here too;\n"
+        "      # without it, `sync push` deletes nothing.\n"
+        f"{_pipeline_step(p, 'Push', 'push --force', p.dest_token_secret, p.dest_stack_url)}"
     )