)]}'
{
  "commit": "4c1e0c354cb6708debb581ba43701dd40b35f3c9",
  "tree": "44cfadcb7ae0a473176bd66d6fd93470e5c234a5",
  "parents": [
    "c381c62060ec407ec850dac9d6542156b0c24b7d"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Mar 23 20:44:25 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Mar 23 20:44:25 2026 -0700"
  },
  "message": "feat: add extensible state mechanism for SymM\n\nThis PR add `SymExtension`, a typed extensible state mechanism for `SymM`,\nfollowing the same pattern as `Grind.SolverExtension`. Extensions are\nregistered at initialization time via `registerSymExtension` and provide\ntyped `getState`/`modifyState` accessors. Extension state persists across\n`simp` invocations within a `sym \u003d\u003e` block and is re-initialized on each\n`SymM.run`.\n\nThis enables modules (e.g., the upcoming arithmetic normalizer) to\nregister persistent state without modifying `Sym.State` directly.\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c1eada667a3a3e761d5f76bb92e53d7a775629f8",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/SymM.lean",
      "new_id": "96efba119777d4a851561e21628c9b392f5d2980",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/SymM.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "54fea0a141056d8ccea2382b01dc17348672de1f",
      "new_mode": 33188,
      "new_path": "tests/pkg/sym_ext/SymExt.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "667c63ed3d72f4c856bc9f7390971018da718367",
      "new_mode": 33188,
      "new_path": "tests/pkg/sym_ext/SymExt/Decl.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "1fe5a5984cb53fefc4805fbf9f9bb05318be802d",
      "new_mode": 33188,
      "new_path": "tests/pkg/sym_ext/lakefile.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "03eeda634a47a52cdb516e8bb2468bab0801158a",
      "new_mode": 33188,
      "new_path": "tests/pkg/sym_ext/lean-toolchain"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "b911bf4de8dacd9b69fa1d2b6802d3a37ce89f99",
      "new_mode": 33188,
      "new_path": "tests/pkg/sym_ext/run_test.sh"
    }
  ]
}