task 477: spawn follow-up 485 (HML fix) + flag leanprover#607 defect in Zulip draft

Task 485: migrate Cslib/Logics/HML/LogicalEquivalence.lean to leanprover#607's
4-arg HasLogicalEquivalence API (blocks whole-library CI on pr607).
Zulip coordination draft updated with the discovered-issue note and a
collaborative heads-up clause to fmontesi.

Session: sess_1783880050_660057

Author: benbrastmckie

specs/476_divide_modal_prs_coordinate_607/artifacts/zulip-coordination.md

@@ -4,6 +4,8 @@
 
 **Re-verify before posting** (as of 2026-07-11): #607 is CI-green and consolidated into `Foundations/Logic/Operators.lean` (adds `HasBox`/`HasDiamond`/dynamic-logic typeclasses; still ◇-primitive with `box := ¬◇¬φ`). #648 (box-primitive prop base), #662 (box-primitive modal), and #649 (LTL) were all rebased onto current upstream/main on 2026-07-11 and now report `mergeable=MERGEABLE`; CI was re-triggered on the new tips (`pending` at rebase time). Pre-rebase branch tips are preserved as `backup/{648,662,649}-pre-rebase-jul11`. Before posting, confirm all three CI runs went green.
 
+**Discovered issue in #607 itself** (task 477, follow-up task 485): while reworking #662 onto a both-primitive basis stacked on #607, the whole-library build was found to fail on #607's own tip — `Cslib/Logics/HML/LogicalEquivalence.lean` still instantiates the **old 3-arg** `LogicalEquivalence` class, but #607's `Foundations/Logic/LogicalEquivalence.lean` already upgraded that class to a **4-arg** signature (adds the inference-system param `S`). HML appears to have been missed when Modal and CLL were migrated to the new `HasLogicalEquivalence` API. Confirmed pre-existing and independent of #662 via `git stash` isolation on a pristine `pr607` base. This blocks `checkInitImports`/`shake`/`test` for the entire library (all pull in the `Cslib.lean` aggregator). Verify this is still present before mentioning it (fmontesi may fix it upstream first). Task 485 tracks a narrow instance migration if a local fix is preferred.
+
 ---
 
 Hi @fmontesi,
@@ -14,4 +16,6 @@ To shrink the pile a little before then, I've tried to arrange things so each PR
 
 I'm glad to see both □ and ◇ as primitive since we'll need both eventually for the intuitionistic and minimal systems (IK, CK). Necessitation and K still touch only □, so the proof theory doesn't get any heavier. I will refactor #662 onto a both-primitive basis so it lines up with #607.
 
+One small heads-up from doing that refactor: `Cslib/Logics/HML/LogicalEquivalence.lean` still uses the old 3-arg `LogicalEquivalence`, which now clashes with the 4-arg class #607 introduces — it looks like HML was missed when Modal and CLL were migrated, and it currently breaks the whole-library build on #607's tip (independent of my modal work). A small instance migration mirroring the Modal/CLL ones should sort it; happy to push that as a tiny PR against #607 if that's easiest.
+
 Everything else we can take one at a time, as you suggested — happy to walk through it whenever suits. Enjoy the time away, and talk on the 23rd.

specs/TODO.md

@@ -1,5 +1,5 @@
 ---
-next_project_number: 485
+next_project_number: 486
 ---
 
 # TODO
@@ -11,7 +11,7 @@ next_project_number: 485
 **Dependency Waves**:
 | Wave | Tasks | Blocked by | Topics |
 |------|-------|------------|--------|
-| 1 | 36,37,181,226,300,317,393,396,400,405,407,425,438,440,441,449,461,462,463,465,466,468,474,477,478,479,480,481,482,483,484 | -- | propositional logic, modal logic, temporal logic, ... |
+| 1 | 36,37,181,226,300,317,393,396,400,405,407,425,438,440,441,449,461,462,463,465,466,468,474,477,478,479,480,481,482,483,484,485 | -- | propositional logic, modal logic, temporal logic, ... |
 | 2 | 39,40,215,301,375,409,430,450,451,456,469 | 36,37,181,317,407,425,449,465 | propositional logic, modal logic, temporal logic, ... |
 | 3 | 41,413,414,475 | 39,40,181,215,300,301,375,468,469 | foundations, modal logic, code hygiene |
 | 4 | 412,476 | 41,475 | code hygiene |
@@ -82,6 +82,7 @@ next_project_number: 485
 465 [PR READY] — Review PR #607 (logical operators): post GitHub review covering t
 466 [PR READY] — Post comment on PR #648 linking the Zulip primitive-bot plus efq 
 474 [PR READY] — Draft Zulip replies confirming CSLib meeting attendance to Montes
+485 [NOT STARTED] — Fix pre-existing defect in PR #607 (leanprover/cslib): Cslib/Logi
 
 ### Tableau Infrastructure
 
@@ -95,6 +96,16 @@ next_project_number: 485
 
 ## Tasks
 
+### 485. Fix pr607 hml logicalequivalence migration
+- **Status**: [NOT STARTED]
+- **Task Type**: cslib
+- **Topic**: PR & Upstreaming
+- **Dependencies**: None
+
+**Description**: Fix pre-existing defect in PR #607 (leanprover/cslib): Cslib/Logics/HML/LogicalEquivalence.lean instantiates the old 3-arg LogicalEquivalence class, but #607 upgraded that class to a 4-arg signature (adds inference-system param S). Migrate the HML instance to the new HasLogicalEquivalence API, mirroring what #607 already did for Modal/LogicalEquivalence and CLL. This blocks whole-library CI (checkInitImports, shake, test) on the pr607 base, independent of #662. Discovered during task 477. (Follow-up from task #477)
+
+---
+
 ### 484. Metalogic conservative extension modularity
 - **Status**: [NOT STARTED]
 - **Task Type**: cslib

specs/state.json

@@ -1,6 +1,17 @@
 {
-  "next_project_number": 485,
+  "next_project_number": 486,
   "active_projects": [
+    {
+      "project_number": 485,
+      "project_name": "fix_pr607_hml_logicalequivalence_migration",
+      "status": "not_started",
+      "task_type": "cslib",
+      "topic": "PR & Upstreaming",
+      "description": "Fix pre-existing defect in PR #607 (leanprover/cslib): Cslib/Logics/HML/LogicalEquivalence.lean instantiates the old 3-arg LogicalEquivalence class, but #607 upgraded that class to a 4-arg signature (adds inference-system param S). Migrate the HML instance to the new HasLogicalEquivalence API, mirroring what #607 already did for Modal/LogicalEquivalence and CLL. This blocks whole-library CI (checkInitImports, shake, test) on the pr607 base, independent of #662. Discovered during task 477. (Follow-up from task #477)",
+      "parent_task": 477,
+      "created": "2026-07-12T19:01:39Z",
+      "last_updated": "2026-07-12T19:01:39Z"
+    },
     {
       "project_number": 477,
       "project_name": "refactor_pr_662_stack_on_607",