Id key not required, apparently

[NorfairKing]

I see:

ParseError "Error in $[18].committer: key \"id\" not found"

when using g.iplcn2.commitsForR.

[NorfairKing]

https://docs.github.com/en/rest/commits/commits?apiVersion=2022-11-28

The example here shows that that's intentional.

[NorfairKing]

Here is the full response for leanprover/lean4 at the moment:

[
  {
    "sha": "520cdb2038fab6cd1a58b61eb3c305e5cd1aa4bd",
    "node_id": "C_kwDOB7kabNoAKDUyMGNkYjIwMzhmYWI2Y2QxYTU4YjYxZWIzYzMwNWU1Y2QxYWE0YmQ",
    "commit": {
      "author": {
        "name": "Sebastian Ullrich",
        "email": "sebasti@nullri.ch",
        "date": "2025-12-12T11:42:42Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T11:42:42Z"
      },
      "message": "feat: do not have `meta` imply `partial` (#11587)\n\nThis PR adjusts the new `meta` keyword of the experimental module system\nnot to imply `partial` for general consistency.\n\nAs the previous behavior can create confusion return types that are not\nknown to be `Nonempty` and few `def`s should be `meta` in the first\ncase, this special case does not appear to be worth the minor\nconvenience.",
      "tree": {
        "sha": "620932cb376b1231305baf217084bbf5f8102e40",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/620932cb376b1231305baf217084bbf5f8102e40"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/520cdb2038fab6cd1a58b61eb3c305e5cd1aa4bd",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO//CCRC1aQ7uu5UhlAAAPYEQAJbAQb0bs2a9ccS9B8yuI1IX\nEaNn+ZSJ+K3X8LVu4BuXI6izUecRsbDgluo0XcEKRxTLFg/WWT9e2YcH07py5ml0\n9QGmrigPmpAovTNI29CDAG3DVRIehhOX5uIHmnAY7DChy8TWNuRKu9luKsT9t4RI\n3kTYMBh8W/dftcEuxs7mQ5JuF23iiU4G4BzoMrcAzKFQofsHtQBdh3+kHrZ/Jt4g\nc1yz4dYRIW3UWt78S9HvNPTkVkWmwB2r2dCfuUdETmN+JH7JiIO6HdzIFOqX29XF\nI++DBrlEbzqhjBL/jYLl+bokvL2IYCmQvwHhNE7cjHMCjk0UNpyK/6fEtBefSrCz\nwu5/IMaUcGCDqGMLg/NP+E34NFqkmd4OGJcN5N8U6htTROHbRYFRXiIE2A/v8px+\nWsGslGogXUv8GLrCGZvP+7Pe4zVDY/wL3U6iYlNbyBJcc9Non6e4I1eF1Q31VpUt\nGk2srIV716Ms3t4oGdS3e0+ImYpSXKeqzaxp/NseaqRzxRXjvJKmaifU9PN2vAe6\ncov2N9FljQFIFuFa02xqPxTqWdeJhhX9/6u4w9kLaEhbYYsUObhfAKObcfzopjZ9\npC0k1a1fQM66UUfy94HLFhV1uEvrug/bNjM2rWjFiEs8KwwuQssA0hZLJLgPV3rx\nd0b6V+NzWAguU1QdFjra\n=xZv6\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 620932cb376b1231305baf217084bbf5f8102e40\nparent 9f74e71f101ae47b03c17a6552ec418153802d92\nauthor Sebastian Ullrich <sebasti@nullri.ch> 1765539762 +0100\ncommitter GitHub <noreply@github.com> 1765539762 +0000\n\nfeat: do not have `meta` imply `partial` (#11587)\n\nThis PR adjusts the new `meta` keyword of the experimental module system\nnot to imply `partial` for general consistency.\n\nAs the previous behavior can create confusion return types that are not\nknown to be `Nonempty` and few `def`s should be `meta` in the first\ncase, this special case does not appear to be worth the minor\nconvenience.",
        "verified_at": "2025-12-12T11:42:58Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/520cdb2038fab6cd1a58b61eb3c305e5cd1aa4bd",
    "html_url": "https://github.com/leanprover/lean4/commit/520cdb2038fab6cd1a58b61eb3c305e5cd1aa4bd",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/520cdb2038fab6cd1a58b61eb3c305e5cd1aa4bd/comments",
    "author": {
      "login": "Kha",
      "id": 109126,
      "node_id": "MDQ6VXNlcjEwOTEyNg==",
      "avatar_url": "https://avatars.githubusercontent.com/u/109126?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/Kha",
      "html_url": "https://github.com/Kha",
      "followers_url": "https://api.github.com/users/Kha/followers",
      "following_url": "https://api.github.com/users/Kha/following{/other_user}",
      "gists_url": "https://api.github.com/users/Kha/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/Kha/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/Kha/subscriptions",
      "organizations_url": "https://api.github.com/users/Kha/orgs",
      "repos_url": "https://api.github.com/users/Kha/repos",
      "events_url": "https://api.github.com/users/Kha/events{/privacy}",
      "received_events_url": "https://api.github.com/users/Kha/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "9f74e71f101ae47b03c17a6552ec418153802d92",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/9f74e71f101ae47b03c17a6552ec418153802d92",
        "html_url": "https://github.com/leanprover/lean4/commit/9f74e71f101ae47b03c17a6552ec418153802d92"
      }
    ]
  },
  {
    "sha": "9f74e71f101ae47b03c17a6552ec418153802d92",
    "node_id": "C_kwDOB7kabNoAKDlmNzRlNzFmMTAxYWU0N2IwM2MxN2E2NTUyZWM0MTgxNTM4MDJkOTI",
    "commit": {
      "author": {
        "name": "Sebastian Ullrich",
        "email": "sebasti@nullri.ch",
        "date": "2025-12-12T11:20:20Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T11:20:20Z"
      },
      "message": "perf: avoid kernel env block in `realizeConst` (#11617)",
      "tree": {
        "sha": "7dde48492c89b0056c85bdebf5fe8a6d5962bc57",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/7dde48492c89b0056c85bdebf5fe8a6d5962bc57"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/9f74e71f101ae47b03c17a6552ec418153802d92",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO/qECRC1aQ7uu5UhlAAAX6cQAC8i6DxsUYKnulnhqVNUkcXC\nUvgTugu+Qh7RE3vnVp+HbE1Y2dMnmoYm6z8fXuVyLH/AWN4/CZmAks1rbE6iwDgC\nC32IR2/+7N2WtPuO81O0myc3j4ta7iUwLWyw6HGy8KyIf/+mH5aUp/wm68fi0zSg\ncqIgpmjtuE2/3oSS8yt7bvC0SZczh16F5GwLGKlaAJx2eQJVwBPEdCReGycyaA6J\ngDRidqakLlvdeXW/tIUIWfJQpp08WmPwgDYDFMQ3LsmZRRtIIm6dZM3erCGA+9N8\nxMGdJoIOPZphbshaGQb8g7soSgfyawYyU3QwMVjEa0LM7TCd3uUSnQtngsbsNn+l\nvL9qHUudm2TgJ7loQahVQoyKe2oNwvQAZbTsVd4FJck8keV8uYAqOEl80hDZkQ9z\nAXUY3BeeemnTgwgap8loyVp6qQCW+nsWJw7NkrKLu5f4VQoTELXDfLi4zL054XQj\nukKbIiZcAYdRr8ILSWhXHvhfyoWA8qeBvgV5Ru1k/i2ftN0GOwpX0KQp0ydxtUtN\nZaJm21u98egWK7wCJcCLepYYnjgeC2Qpw8L0gpm9agCsMgx6+h3201F8qkClEgnJ\n6ajhMiRYayg3mNJnm+tOSPD/4Zs6/uZx+fAU3iXg5Db50oXA0decRYJdYzrvyFlm\nPK0HTjEOmRNI8PS9o6e2\n=3ZS9\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 7dde48492c89b0056c85bdebf5fe8a6d5962bc57\nparent ad02aa159c96aa78a01a5fff0e77413da3933094\nauthor Sebastian Ullrich <sebasti@nullri.ch> 1765538420 +0100\ncommitter GitHub <noreply@github.com> 1765538420 +0000\n\nperf: avoid kernel env block in `realizeConst` (#11617)\n\n",
        "verified_at": "2025-12-12T11:20:36Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/9f74e71f101ae47b03c17a6552ec418153802d92",
    "html_url": "https://github.com/leanprover/lean4/commit/9f74e71f101ae47b03c17a6552ec418153802d92",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/9f74e71f101ae47b03c17a6552ec418153802d92/comments",
    "author": {
      "login": "Kha",
      "id": 109126,
      "node_id": "MDQ6VXNlcjEwOTEyNg==",
      "avatar_url": "https://avatars.githubusercontent.com/u/109126?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/Kha",
      "html_url": "https://github.com/Kha",
      "followers_url": "https://api.github.com/users/Kha/followers",
      "following_url": "https://api.github.com/users/Kha/following{/other_user}",
      "gists_url": "https://api.github.com/users/Kha/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/Kha/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/Kha/subscriptions",
      "organizations_url": "https://api.github.com/users/Kha/orgs",
      "repos_url": "https://api.github.com/users/Kha/repos",
      "events_url": "https://api.github.com/users/Kha/events{/privacy}",
      "received_events_url": "https://api.github.com/users/Kha/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "ad02aa159c96aa78a01a5fff0e77413da3933094",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/ad02aa159c96aa78a01a5fff0e77413da3933094",
        "html_url": "https://github.com/leanprover/lean4/commit/ad02aa159c96aa78a01a5fff0e77413da3933094"
      }
    ]
  },
  {
    "sha": "ad02aa159c96aa78a01a5fff0e77413da3933094",
    "node_id": "C_kwDOB7kabNoAKGFkMDJhYTE1OWM5NmFhNzhhMDFhNWZmZjBlNzc0MTNkYTM5MzMwOTQ",
    "commit": {
      "author": {
        "name": "Kim Morrison",
        "email": "477956+kim-em@users.noreply.github.com",
        "date": "2025-12-12T10:40:04Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T10:40:04Z"
      },
      "message": "chore: remove ≥6 month old deprecations (#11627)",
      "tree": {
        "sha": "b4e39def0a36fe738606999b9d798d942bbced8c",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/b4e39def0a36fe738606999b9d798d942bbced8c"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/ad02aa159c96aa78a01a5fff0e77413da3933094",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO/EUCRC1aQ7uu5UhlAAAhSwQAFNYgtz/fPaq4D7W9/yjWmGi\nPP4e8CajRotfcCmitvcOzc47SF3/9M6ZtRFBdkYT3/UM6EXmeeH5l1TlloLrsV2v\nZ7gsFLrb9vbW2MQeG42+fKVdxZkXEkKfrhNxuGAdvlRG16X+WsFbWH7wyK22mq3v\nKmQtP+kh0sop+6LboeW/ZzGhbWaBhAlQwiCRG5HtDcbN5z3e2JCaZCM1BzoouC1v\nhhYfaY1bdogiYIWepaNUVrMskglbZAZ5SIAz33mID9oBgC6J3kM4S/3uCYdFkQH7\nVKgZ8sEMOiatGb9Owav4ArwoAaKEcjEMegACP6ISd7b0U9+khm5ez72tva4Zn0ca\ncarSB3d3RvrgyOa6yNIAZrT7kPB/lZJZKZ0Y8ot5AQRVPfV+xL1zEPj6CoEsl6zb\n0vsdThvZVKyRtSs/2l6aLpgtBMAVxVBqk7isgXXxdJGxAA3EVMgL3UiQZ3zvYm2D\nK1Jq2ikiCNpj1sIJOfm4+L5nS0xQ4ryYK6lO+KQCUTaLhxCEGL8ifwRJ4FIvH19K\nB3pSB3D8gXkPbchZJcLwl1ml26RJZ/5AKqS2Mvyz3YzCoW6FqOS7eod86E/IrJid\n72qeCFLfrWjVOkvBsOiBzgNgb4jhm2SLUoNIwRhTTPcvfWiGNdkUdNvFUTsrHK1t\nNmiRheYBUgeoOEdMyzYJ\n=FTUc\n-----END PGP SIGNATURE-----\n",
        "payload": "tree b4e39def0a36fe738606999b9d798d942bbced8c\nparent 07645775e6fa87d7e48ae5cb1a535d65a22d8f2b\nauthor Kim Morrison <477956+kim-em@users.noreply.github.com> 1765536004 +1100\ncommitter GitHub <noreply@github.com> 1765536004 +0000\n\nchore: remove ≥6 month old deprecations (#11627)\n\n",
        "verified_at": "2025-12-12T10:40:21Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/ad02aa159c96aa78a01a5fff0e77413da3933094",
    "html_url": "https://github.com/leanprover/lean4/commit/ad02aa159c96aa78a01a5fff0e77413da3933094",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/ad02aa159c96aa78a01a5fff0e77413da3933094/comments",
    "author": {
      "login": "kim-em",
      "id": 477956,
      "node_id": "MDQ6VXNlcjQ3Nzk1Ng==",
      "avatar_url": "https://avatars.githubusercontent.com/u/477956?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/kim-em",
      "html_url": "https://github.com/kim-em",
      "followers_url": "https://api.github.com/users/kim-em/followers",
      "following_url": "https://api.github.com/users/kim-em/following{/other_user}",
      "gists_url": "https://api.github.com/users/kim-em/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/kim-em/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/kim-em/subscriptions",
      "organizations_url": "https://api.github.com/users/kim-em/orgs",
      "repos_url": "https://api.github.com/users/kim-em/repos",
      "events_url": "https://api.github.com/users/kim-em/events{/privacy}",
      "received_events_url": "https://api.github.com/users/kim-em/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
        "html_url": "https://github.com/leanprover/lean4/commit/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b"
      }
    ]
  },
  {
    "sha": "07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
    "node_id": "C_kwDOB7kabNoAKDA3NjQ1Nzc1ZTZmYTg3ZDdlNDhhZTVjYjFhNTM1ZDY1YTIyZDhmMmI",
    "commit": {
      "author": {
        "name": "Wojciech Różowski",
        "email": "wojciech@lean-fro.org",
        "date": "2025-12-12T09:55:55Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T09:55:55Z"
      },
      "message": "feat: add decidable equality to `DHashMap`/`HashMap`/`HashSet` and their extensional variants (#11421)\n\nThis PR adds decidable equality to `DHashMap`/`HashMap`/`HashSet` and\ntheir extensional variants.\n\nStacked on top of #11266.",
      "tree": {
        "sha": "9797ae7d614e11069e6a3d858fc1471a6e332192",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/9797ae7d614e11069e6a3d858fc1471a6e332192"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO+a7CRC1aQ7uu5UhlAAA1mgQAHacc3agmtSyqA8gDYH8JfG4\negslORHm/GbVaBkGPCiPYK6ku5MNPqqF4SMyGuCL7kUBkkIBjjycWg1MMFj5usnQ\nkAs0wyYXNFjkZtgScZYE+gIE1FLiTqG5DFUroDHxQlFRxXu1VMyI9V7rPvXrFwnm\nsaHy4Z1CulaJ4tQJc5SaudKTTzwBUPd5TNRWjlkAN1GlczehpGpUy4fHNpd/D6xD\n+lGTRx8Gi/JBhDB623ncMSAy5TxB1U7Ub790+5UtiAvmCutpAATN8LUN1ubfc94P\n9Q4kQX2t0C+LjQD+aVKz7l4R1oxb9Gmy0GkoGtNqap6mUt46v7iEzILrntF8Xfdy\n5M5y6R4D7lyYyVTcGro0J8E751LgNO4ofErbU0HIDaA+3ZGxiRoNahZqWAQNcyBf\nsRtSraFT8KhM6JhyTLd3HVOF4Kqplamnb7il7Az5dKXUrnOn3WyBMRYua6MRIjIh\n1z6Kv1RSsMRBqzXGm+j9WkuSJMfNSJXXC61DqDYQoK1sIvmaTefjCDkEzhcSq7pq\n2+SxBQOV8MfAdrZyFsu8tVvBz+psFN8RikEGx1vsY+4Xs42WyHEXTt3FItSMA2nC\nEK9v/4exqWDQt0iA+EuHnDAic1Uu69+XTJaVYudIVzShoAkW+X4P92nSf+iTf7fL\nrw3JiCCNhNPBZHMAk1u0\n=ijrv\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 9797ae7d614e11069e6a3d858fc1471a6e332192\nparent a984e1791342f59264d02cfbdfe9a61d5e41fc29\nauthor Wojciech Różowski <wojciech@lean-fro.org> 1765533355 +0100\ncommitter GitHub <noreply@github.com> 1765533355 +0000\n\nfeat: add decidable equality to `DHashMap`/`HashMap`/`HashSet` and their extensional variants (#11421)\n\nThis PR adds decidable equality to `DHashMap`/`HashMap`/`HashSet` and\ntheir extensional variants.\n\nStacked on top of #11266.",
        "verified_at": "2025-12-12T09:56:12Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
    "html_url": "https://github.com/leanprover/lean4/commit/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/07645775e6fa87d7e48ae5cb1a535d65a22d8f2b/comments",
    "author": {
      "login": "wkrozowski",
      "id": 43882352,
      "node_id": "MDQ6VXNlcjQzODgyMzUy",
      "avatar_url": "https://avatars.githubusercontent.com/u/43882352?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/wkrozowski",
      "html_url": "https://github.com/wkrozowski",
      "followers_url": "https://api.github.com/users/wkrozowski/followers",
      "following_url": "https://api.github.com/users/wkrozowski/following{/other_user}",
      "gists_url": "https://api.github.com/users/wkrozowski/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/wkrozowski/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/wkrozowski/subscriptions",
      "organizations_url": "https://api.github.com/users/wkrozowski/orgs",
      "repos_url": "https://api.github.com/users/wkrozowski/repos",
      "events_url": "https://api.github.com/users/wkrozowski/events{/privacy}",
      "received_events_url": "https://api.github.com/users/wkrozowski/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "a984e1791342f59264d02cfbdfe9a61d5e41fc29",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/a984e1791342f59264d02cfbdfe9a61d5e41fc29",
        "html_url": "https://github.com/leanprover/lean4/commit/a984e1791342f59264d02cfbdfe9a61d5e41fc29"
      }
    ]
  },
  {
    "sha": "a984e1791342f59264d02cfbdfe9a61d5e41fc29",
    "node_id": "C_kwDOB7kabNoAKGE5ODRlMTc5MTM0MmY1OTI2NGQwMmNmYmRmZTlhNjFkNWU0MWZjMjk",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-12T09:32:31Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T09:32:31Z"
      },
      "message": "fix: missing condition at `normalizePattern` in `grind` (#11629)\n\nThis PR adds a missing condition in the pattern normalization code used\nin `grind`. It should ignore support ground terms.",
      "tree": {
        "sha": "0f41c965a9a19765c67cc64a0f96295d5c23bf6e",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/0f41c965a9a19765c67cc64a0f96295d5c23bf6e"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/a984e1791342f59264d02cfbdfe9a61d5e41fc29",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO+E4CRC1aQ7uu5UhlAAAMhEQAIAUkIX3CjlIrZ10TpVBB+fH\n+bjeZqqv47UAeS8Nf4W/89Ik1ochHGf7AE+RwiuwO6mnIvT5XbUej8ihKj9ogghu\nghGKnRMlyPh6smZ9OxuK2pEKG2S5puhEw/YNkQGdzNdNIL4LIHr/yyRa+OEisgvZ\nYw/QNbgqHJkckUo1YK3A3tGrB2HzGwhlFnaup8OIiX7WPVoX1Tv+Z33lqw2oA0Fw\nfNnubeJpaA31RJSwIwZgGKtwh8edqz8zgDEG/Hwzkvr21GKhsIGqsybLvGoUGehi\n/HQW+H3tsymgAOFME/viYmCrOBncJudvT4qZ6y/2VrRzPzRS4Q0AznjkMQp/tSiA\nnzGqyyekcMfY608venl5ztRBNvqSiOnF7K1He1GXxMeoQK8Nk5tY9+B6kQvWSojq\nIejAFnUm+nSI2dGe0HqDmMOOR9YX3GL5JLEBN4y0dxhw14eKTDWQ06+A2wKFBXwh\nA2/zuMQxj64NoGvfuY977NAl3oH6YxdYMZzkcd9Y4SjtILEwhPjat3W+BvIsk4cS\nladqr+HzrweMXVDv0r6F22zkGXp1mn8tfIjnoP7hGL2pdP5HCOWAJsvYZvGrjtsE\n5CqThUOietyKh4SA2udyEJYa7EEzgvwKmL5i3FTfD8/Y/04o0uZ6TsdH6LeZOyyV\nGNDSkcuxKetO6zTaIjbI\n=LhRj\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 0f41c965a9a19765c67cc64a0f96295d5c23bf6e\nparent 8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8\nauthor Leonardo de Moura <leomoura@amazon.com> 1765531951 +0100\ncommitter GitHub <noreply@github.com> 1765531951 +0000\n\nfix: missing condition at `normalizePattern` in `grind` (#11629)\n\nThis PR adds a missing condition in the pattern normalization code used\nin `grind`. It should ignore support ground terms.",
        "verified_at": "2025-12-12T09:32:40Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/a984e1791342f59264d02cfbdfe9a61d5e41fc29",
    "html_url": "https://github.com/leanprover/lean4/commit/a984e1791342f59264d02cfbdfe9a61d5e41fc29",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/a984e1791342f59264d02cfbdfe9a61d5e41fc29/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
        "html_url": "https://github.com/leanprover/lean4/commit/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8"
      }
    ]
  },
  {
    "sha": "8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
    "node_id": "C_kwDOB7kabNoAKDgyMjBiYWY2ZGIxYzBlYjFmNmQyYWRlOWIxNGVmODE0MmM2ZTljZjg",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-12T09:10:49Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T09:10:49Z"
      },
      "message": "feat: add a few `Semiring` normalization rules to `grind` (#11628)\n\nThis PR adds a few `*` normalization rules for `Semiring`s to `grind`.",
      "tree": {
        "sha": "a2ad836fae1ceca19446303630d9868787822b7f",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/a2ad836fae1ceca19446303630d9868787822b7f"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO9wpCRC1aQ7uu5UhlAAATeEQAAwskPR7juFy3tvI9GQ7DgST\ni/YNuoAJA65IN2pr50R9ncuVhHD0tUt1jQZqMY75JC5usKz6fKLSFlvnZK8MqY5R\nrJmq45TMjRsb9gJnoTLXZKIDFxEApiKAQ2Q27CDBa7NdhzWmhORRjNh29pncixRp\nlkQhAAtEzwHWtD41lucahaIwH3zHvlKWYoivrTLpgxfWJ+XM3wiS5j57Z64SJfq7\n0wfHdiIrFpItZQn7gPsEA1mNnVcHRWAKzi3JT4IecyAXFVEOkQZB340Jmx04GAho\n1BzPoovYUTDxBp2tr5gygP83pMnB4t9ZdrtbPVPx+2AjOxyKmTKe62rP5cTKRjYw\nSJbT7YN8noaJWFh32SGmSYf0LIk5HK7S2ErAj9ofN9YgWr8kLiQtFyt8h00qC8Vh\nxQ50BJDoz68AjOQn3wYqIvNk0I0vXIYaT8bino6AI9+bdsHNxqn91FF9GhV+3XE5\n2IrSWeCDGvSq6T3Dq46gG/blziRh9+jUFgS4Bobszq6Hz2NJQBd2aoJkb3rBGJAP\nkyrUWMQ30T14cB2E1hjgBMX3TdmheJISQGFU8fN2WG6b9nFZeNI5f7tqgAhKNmZ9\nd8At7tQ8JZFZCX/rGhrdTRIf4nzM0PVjH2rYCQMd4M0UhZr8aL6mvX/QyGhg9Ocf\n6AgT/9bGPmo1r1yWR2lk\n=wsDB\n-----END PGP SIGNATURE-----\n",
        "payload": "tree a2ad836fae1ceca19446303630d9868787822b7f\nparent fc26c8145c730d24eb3946c7019d7cf83a9e3b51\nauthor Leonardo de Moura <leomoura@amazon.com> 1765530649 +0100\ncommitter GitHub <noreply@github.com> 1765530649 +0000\n\nfeat: add a few `Semiring` normalization rules to `grind` (#11628)\n\nThis PR adds a few `*` normalization rules for `Semiring`s to `grind`.",
        "verified_at": "2025-12-12T09:11:06Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
    "html_url": "https://github.com/leanprover/lean4/commit/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/8220baf6db1c0eb1f6d2ade9b14ef8142c6e9cf8/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
        "html_url": "https://github.com/leanprover/lean4/commit/fc26c8145c730d24eb3946c7019d7cf83a9e3b51"
      }
    ]
  },
  {
    "sha": "fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
    "node_id": "C_kwDOB7kabNoAKGZjMjZjODE0NWM3MzBkMjRlYjM5NDZjNzAxOWQ3Y2Y4M2E5ZTNiNTE",
    "commit": {
      "author": {
        "name": "Sebastian Ullrich",
        "email": "sebasti@nullri.ch",
        "date": "2025-12-12T08:56:08Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T08:56:08Z"
      },
      "message": "chore: realization of private def should run in private scope (#11618)\n\nIn fact the scope should be solely determined by the def name but this\nbreaks some existing realizer, so postponed.",
      "tree": {
        "sha": "40f8aac151c0a8ac391c5fa65b5072ede1f1147f",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/40f8aac151c0a8ac391c5fa65b5072ede1f1147f"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO9i4CRC1aQ7uu5UhlAAAwg8QAJ2SGeQ8sDOROOF5RfXsWrFD\nAX/VqiZGvRO2XoQQnjiajy4nvy8RXQRBliN1Eyg2Gefy4ZNNJGd6foRzzZ5xx0JB\nQoH5VJjK5CfGhqHCc9z5eAMglFAMP1UoedYHmO+SFv/beOUZncgN8MSDK2NIGnpn\nDh/8He61JjOOVLmVcJkEKZG83peSa6yWDWq4UNGluHPCdewwIbrXnnb1Y9LKwZ6l\nJSoV17hfIzEjh606cfidH5UvMCoydbXuXCxBds+AeYkK9S7xnx46YLKkIkcjSlH7\n4H5C6M0PE/PmsLT57LD++csWP4m9xB+AiePxcVcx+mY3/QK6lU2U1yUMLiKQmh8i\nXmpI/mv7BNo40QqCa62HscnpPbp/Cgug2FRT3E9xrYV4WxRX9n0UC4jdfXGayG+Q\nTLJObwd9QdPqMDawGHTLZpzeBtc7GUb8DhrE4JdsODckluO0F4xUxDnBH49GBp8D\nBLeoBkKdFkUSg4uVrC4N6AQJ1cybxU/pIV2adETYkFrNqPE+0jbiQA6e9musXAia\nhilmRIhSzYzZ2vXBpIr5Aq+Bulpnh0pGOntcoE5TXN5mg/WAnlEjHaOiAc7YfFYD\nv98OEXteTt0FeUh4/zzOZTqEDMDJxqFPuF3wqbCoEdWPX+pRhyDxKENgrkNEfAxA\nQj3aSldTpC4/RAKkwtC3\n=zjpQ\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 40f8aac151c0a8ac391c5fa65b5072ede1f1147f\nparent 9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e\nauthor Sebastian Ullrich <sebasti@nullri.ch> 1765529768 +0100\ncommitter GitHub <noreply@github.com> 1765529768 +0000\n\nchore: realization of private def should run in private scope (#11618)\n\nIn fact the scope should be solely determined by the def name but this\nbreaks some existing realizer, so postponed.",
        "verified_at": "2025-12-12T08:56:24Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
    "html_url": "https://github.com/leanprover/lean4/commit/fc26c8145c730d24eb3946c7019d7cf83a9e3b51",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/fc26c8145c730d24eb3946c7019d7cf83a9e3b51/comments",
    "author": {
      "login": "Kha",
      "id": 109126,
      "node_id": "MDQ6VXNlcjEwOTEyNg==",
      "avatar_url": "https://avatars.githubusercontent.com/u/109126?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/Kha",
      "html_url": "https://github.com/Kha",
      "followers_url": "https://api.github.com/users/Kha/followers",
      "following_url": "https://api.github.com/users/Kha/following{/other_user}",
      "gists_url": "https://api.github.com/users/Kha/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/Kha/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/Kha/subscriptions",
      "organizations_url": "https://api.github.com/users/Kha/orgs",
      "repos_url": "https://api.github.com/users/Kha/repos",
      "events_url": "https://api.github.com/users/Kha/events{/privacy}",
      "received_events_url": "https://api.github.com/users/Kha/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
        "html_url": "https://github.com/leanprover/lean4/commit/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e"
      }
    ]
  },
  {
    "sha": "9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
    "node_id": "C_kwDOB7kabNoAKDllNGY5ZDMxN2JkNWIyN2JkNDNiNzZiYTgxMWZkZjhhOWY2ZDI3OWU",
    "commit": {
      "author": {
        "name": "Wojciech Różowski",
        "email": "wojciech@lean-fro.org",
        "date": "2025-12-12T08:30:36Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T08:30:36Z"
      },
      "message": "feat: add BEq to `DTreeMap`/`TreeMap`/`TreeSet` and their extensional variants (#11404)\n\nThis PR adds BEq instance for `DTreeMap`/`TreeMap`/`TreeSet` and their\nextensional variants and proves lemmas relating it to the equivalence of\nhashmaps/equality of extensional variants.\n\nStacked on top of #11266",
      "tree": {
        "sha": "aa50027e2d6ad79129b3bfd54e8f365b6b40d11b",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/aa50027e2d6ad79129b3bfd54e8f365b6b40d11b"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO9K7CRC1aQ7uu5UhlAAAnAUQAFWwAP9B7vBe2Cd/AiRSYrvv\nz887vdhi1P/adMu58LXp6WHrmPKVOQwkys5fGZp+1crOD7U+jS+i/l+rkBKaUNzG\nyxna1NrGdp2pXipAOqGsJSVIxQdVve45uZMqbdhp/pFB6e3E67DkaTTR7Vj+/KjC\ndOJL4m+koQDOxUAy/vQB4lgg5xd/AwOz7ZtIBGCLe6XJio9LkBF819dXISEQnGA9\ne2632a3tBySFPm66HtW5NprY1cA/dJzNJigIEO8zqgRVOSow1TH8HZd4jm+eJqJb\nQak1jX6eUN7tNiONaGgBevIRMmUfWCvK9nihLN8Z0ZaFTyWiH7otaVV0IulJj/8I\nW7yBhgykdBTWKoPpOByRJjCMssl9i42mUWG+/BqLLU8r1xqIfmTGlNdzynsuGK89\nYRFd441c2MthkezQpyVUJbZTWFMYM1XzD5KB63cCxixNufgZvYJ1gBnf6rzVLjFz\nrAxivZ8RnJRp45Xfl7dK3aknak7MYJEZBVgCbb2t527G5ueWcnshPM0QgfX33nbW\n5KgsYt7Z01ZnB1TJVBzLGEltxTvxqvqmPL5pkkDTVi05Eki+KHT1kyrVRDzu7UaJ\nnrAm1zc3ytL0x8eh0Y05mijpGTJaXJLj8ym5pY8J51/bBuOotoMFuV8SsxWSNTO2\nLBakv08wfKjxbkH6iUUL\n=JW56\n-----END PGP SIGNATURE-----\n",
        "payload": "tree aa50027e2d6ad79129b3bfd54e8f365b6b40d11b\nparent 3937af3d7518cf2612939c59711921c5f5ef6701\nauthor Wojciech Różowski <wojciech@lean-fro.org> 1765528236 +0100\ncommitter GitHub <noreply@github.com> 1765528236 +0000\n\nfeat: add BEq to `DTreeMap`/`TreeMap`/`TreeSet` and their extensional variants (#11404)\n\nThis PR adds BEq instance for `DTreeMap`/`TreeMap`/`TreeSet` and their\nextensional variants and proves lemmas relating it to the equivalence of\nhashmaps/equality of extensional variants.\n\nStacked on top of #11266",
        "verified_at": "2025-12-12T08:30:52Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
    "html_url": "https://github.com/leanprover/lean4/commit/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e/comments",
    "author": {
      "login": "wkrozowski",
      "id": 43882352,
      "node_id": "MDQ6VXNlcjQzODgyMzUy",
      "avatar_url": "https://avatars.githubusercontent.com/u/43882352?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/wkrozowski",
      "html_url": "https://github.com/wkrozowski",
      "followers_url": "https://api.github.com/users/wkrozowski/followers",
      "following_url": "https://api.github.com/users/wkrozowski/following{/other_user}",
      "gists_url": "https://api.github.com/users/wkrozowski/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/wkrozowski/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/wkrozowski/subscriptions",
      "organizations_url": "https://api.github.com/users/wkrozowski/orgs",
      "repos_url": "https://api.github.com/users/wkrozowski/repos",
      "events_url": "https://api.github.com/users/wkrozowski/events{/privacy}",
      "received_events_url": "https://api.github.com/users/wkrozowski/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "3937af3d7518cf2612939c59711921c5f5ef6701",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/3937af3d7518cf2612939c59711921c5f5ef6701",
        "html_url": "https://github.com/leanprover/lean4/commit/3937af3d7518cf2612939c59711921c5f5ef6701"
      }
    ]
  },
  {
    "sha": "3937af3d7518cf2612939c59711921c5f5ef6701",
    "node_id": "C_kwDOB7kabNoAKDM5MzdhZjNkNzUxOGNmMjYxMjkzOWM1OTcxMTkyMWM1ZjVlZjY3MDE",
    "commit": {
      "author": {
        "name": "Wojciech Różowski",
        "email": "wojciech@lean-fro.org",
        "date": "2025-12-12T08:03:00Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T08:03:00Z"
      },
      "message": "feat: add a lemma relating `minKey?` and `min?` for `DTreeMap` (#11528)\n\nThis PR adds lemmas relating `minKey?` and `min?` on the keys list for\nall `DTreeMap` and other containers derived from it.",
      "tree": {
        "sha": "929f8d3c404caa15311aaae12ef38724b728546e",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/929f8d3c404caa15311aaae12ef38724b728546e"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/3937af3d7518cf2612939c59711921c5f5ef6701",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO8xECRC1aQ7uu5UhlAAAP0MQADAzQ6Blm3U7+hx+Yx/WL+nV\nJiES3UpMSQjtJNch3/kG+lGWUdSH1oH6YmJCKVZAW+nnPGVQ8210zRTzoZYQIfyH\npf3kUV/CVADXn1khhmlkxsbvJ/l5K20G+GzxYwZ/0v2Z5XfAygH5gzwHlaE+x1XS\n3YRZZsVkUiVHav0NNVyXvgvzju8T0Z4CRTph8w+B2mULyW9i/wvAgwEpTPC6oaqi\nOLeM7mWw5lCUYrvKNuchYejcP/xiWIPmc2fRSNC7dIhqsMMpAfB+ocsaEgAEGd5h\nty5QN1JfujPvw2lQu8JmGQS58JDm+Ol0yPuStMQGcInz9ztJ27gjAixR8P1GrL5X\n2ONkOj2o5g/+1UkO5sFnEqxCghBfR5sdKcvye4PGyHI4k18oRAt0SE+xBvNNxWVn\ngFYSVjp4jueumNPXKXqicQpEdQmS/BYcf9UdC8GipHk48uqj8wNhwcPStRE7o6e1\n1LEOOGzENVB1lE97A2DHOjVIOiiFaR8dgLVMwQgPv/afLCvCLk6bUy9UrVCjEUQL\n39Ykif25TQDXqt4SEszXLQKogos9cmONCgJM6TnqfBGFRPYCoXRy47jTnuS7yKYL\nmNFtHiWVOf7zLq2MvBbvO35/wNdMax9bSi3zBUDG96+s+8O39ntqeLZTuQ6CGhK8\nxwY1s9Mv6lwzHO4onOcD\n=NPY/\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 929f8d3c404caa15311aaae12ef38724b728546e\nparent 646df6ba16b3f68de539a085456c323e160e206d\nauthor Wojciech Różowski <wojciech@lean-fro.org> 1765526580 +0100\ncommitter GitHub <noreply@github.com> 1765526580 +0000\n\nfeat: add a lemma relating `minKey?` and `min?` for `DTreeMap` (#11528)\n\nThis PR adds lemmas relating `minKey?` and `min?` on the keys list for\nall `DTreeMap` and other containers derived from it.",
        "verified_at": "2025-12-12T08:03:17Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/3937af3d7518cf2612939c59711921c5f5ef6701",
    "html_url": "https://github.com/leanprover/lean4/commit/3937af3d7518cf2612939c59711921c5f5ef6701",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/3937af3d7518cf2612939c59711921c5f5ef6701/comments",
    "author": {
      "login": "wkrozowski",
      "id": 43882352,
      "node_id": "MDQ6VXNlcjQzODgyMzUy",
      "avatar_url": "https://avatars.githubusercontent.com/u/43882352?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/wkrozowski",
      "html_url": "https://github.com/wkrozowski",
      "followers_url": "https://api.github.com/users/wkrozowski/followers",
      "following_url": "https://api.github.com/users/wkrozowski/following{/other_user}",
      "gists_url": "https://api.github.com/users/wkrozowski/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/wkrozowski/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/wkrozowski/subscriptions",
      "organizations_url": "https://api.github.com/users/wkrozowski/orgs",
      "repos_url": "https://api.github.com/users/wkrozowski/repos",
      "events_url": "https://api.github.com/users/wkrozowski/events{/privacy}",
      "received_events_url": "https://api.github.com/users/wkrozowski/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "646df6ba16b3f68de539a085456c323e160e206d",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/646df6ba16b3f68de539a085456c323e160e206d",
        "html_url": "https://github.com/leanprover/lean4/commit/646df6ba16b3f68de539a085456c323e160e206d"
      }
    ]
  },
  {
    "sha": "646df6ba16b3f68de539a085456c323e160e206d",
    "node_id": "C_kwDOB7kabNoAKDY0NmRmNmJhMTZiM2Y2OGRlNTM5YTA4NTQ1NmMzMjNlMTYwZTIwNmQ",
    "commit": {
      "author": {
        "name": "Eric Wieser",
        "email": "efw@google.com",
        "date": "2025-12-12T03:00:17Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T03:00:17Z"
      },
      "message": "feat: add lemmas about `EStateM.run` (#11600)\n\nThis PR adds a few lemmas about `EStateM.run` on basic operations.",
      "tree": {
        "sha": "5fb68d91898250d3ea992dde8b268860d893e914",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/5fb68d91898250d3ea992dde8b268860d893e914"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/646df6ba16b3f68de539a085456c323e160e206d",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO4VICRC1aQ7uu5UhlAAA5EwQACg4cnLlSLYFVprfk02P3qMX\n42y+Y//CsI6gbmmpF1zm0nVWHL8N2UHPSEZ2xOUekXcoOx/Ij3DG5ebPO48+SH8b\nK/74BeeoDnsMfgNmQreRbMtMzNeBo7kptHrs9dxNUWgy233zAdimB6G0DI7SlO4Z\nvnRrrSp9lpka6cj9j8At6ZzrFRjRm7Yt0yoPxP9L8xm/u1LBo386PVk1YuKr2B4c\nUmMi5C+ZuyAp9hDGVag9tIEDdsWJElTUJvE9G4//346enc4Td/fN9WSfpRsJIVNu\nCveANM7lk2wHJyyVgxk9/hQZwCQ4wDyDl9zElbSmk3LE9o8FOlkW+ZWq4ktZ6QeZ\nB3SWUOrZZLhUq4/w4ZwJBOOvKuTyBWrw9CKb0Oyc6lDaV+dgFw3FncYXfV6PDgbu\n6DCBkrcA+mLHFSVldwAM5F7jS4LDlh0crb3qeYdDh0adMxvnqcwA80oVLi2lQRvw\n+DA33B38eQ61+ssrOsQhhPB2cvSPA1100/SDyUfoTN1et2WFx3uttWu7oNrTbpQ8\n9oPBMrSiin86Kqk7dVFjFE+sImCJX5AwNxg/NBma1DXhAg2iz8HyIwPRCF0uQkJT\nXbMVUSIR4WxbIG/Mj9jP4YPtnJa7iH4FMu8SGW0nwD8uE3udg/eSITT0pJvIuU9B\nE2GyHVpyn9k+q1QIKN+p\n=5PGm\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 5fb68d91898250d3ea992dde8b268860d893e914\nparent 552fa10a60c5a413f8ed3718c5510439235f3d2b\nauthor Eric Wieser <efw@google.com> 1765508417 -0800\ncommitter GitHub <noreply@github.com> 1765508417 +0000\n\nfeat: add lemmas about `EStateM.run` (#11600)\n\nThis PR adds a few lemmas about `EStateM.run` on basic operations.",
        "verified_at": "2025-12-12T03:00:25Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/646df6ba16b3f68de539a085456c323e160e206d",
    "html_url": "https://github.com/leanprover/lean4/commit/646df6ba16b3f68de539a085456c323e160e206d",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/646df6ba16b3f68de539a085456c323e160e206d/comments",
    "author": {
      "login": "eric-wieser",
      "id": 425260,
      "node_id": "MDQ6VXNlcjQyNTI2MA==",
      "avatar_url": "https://avatars.githubusercontent.com/u/425260?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/eric-wieser",
      "html_url": "https://github.com/eric-wieser",
      "followers_url": "https://api.github.com/users/eric-wieser/followers",
      "following_url": "https://api.github.com/users/eric-wieser/following{/other_user}",
      "gists_url": "https://api.github.com/users/eric-wieser/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/eric-wieser/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/eric-wieser/subscriptions",
      "organizations_url": "https://api.github.com/users/eric-wieser/orgs",
      "repos_url": "https://api.github.com/users/eric-wieser/repos",
      "events_url": "https://api.github.com/users/eric-wieser/events{/privacy}",
      "received_events_url": "https://api.github.com/users/eric-wieser/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "552fa10a60c5a413f8ed3718c5510439235f3d2b",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/552fa10a60c5a413f8ed3718c5510439235f3d2b",
        "html_url": "https://github.com/leanprover/lean4/commit/552fa10a60c5a413f8ed3718c5510439235f3d2b"
      }
    ]
  },
  {
    "sha": "552fa10a60c5a413f8ed3718c5510439235f3d2b",
    "node_id": "C_kwDOB7kabNoAKDU1MmZhMTBhNjBjNWE0MTNmOGVkMzcxOGM1NTEwNDM5MjM1ZjNkMmI",
    "commit": {
      "author": {
        "name": "Kim Morrison",
        "email": "477956+kim-em@users.noreply.github.com",
        "date": "2025-12-12T02:59:35Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T02:59:35Z"
      },
      "message": "feat: `@[suggest_for ℤ]` and `@[suggest_for ℚ]` annotations (#11596)\n\nThis PR adds `@[suggest_for ℤ]` on `Int` and `@[suggest_for ℚ]` on\n`Rat`, following the pattern established by `@[suggest_for ℕ]` on `Nat`\nin #11554.\n\n\n🤖 Prepared with Claude Code\n\nCo-authored-by: Claude Opus 4.5 <noreply@anthropic.com>",
      "tree": {
        "sha": "7e829a5345dc993cd21ead4f29ff7b5f220668b5",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/7e829a5345dc993cd21ead4f29ff7b5f220668b5"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/552fa10a60c5a413f8ed3718c5510439235f3d2b",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO4UnCRC1aQ7uu5UhlAAAKqMQAANiwcMdJHsq0zKL+x8TNG6U\nmISktnoDpRrFUcnrUhpi/Px/YB9ePFKOvY0SgtaDqHPsvQ30YLtxi6fuKkqFVGAs\nzROA6zHZ1iQduR+ZfAj2nQK87YJPFEs1x5wL3DOjZuF5QqyECj3z7VrzMHt+lIzA\nOk7IV4H9DjVuBjhh7qYqXPlqXOPkYAggsPaHBmWk/azJ3K20axsubSmc0TLnmW4u\ncJtppxRAPpV0M3HFM0/kA23WHWSUICMVrpYY9361KSe6EwcQxG3SmbYbOApzzIZ5\nTmayxvvu2RdqiJCsXlOAFhSbDYvXLiAvVVFmLMfjZ/BZ3Rl5Fxmv0vlHFawTNGe5\njBdMljHUTMXERVeTNXUTwAi/xEDxwreF9hlBJHQJxFHjuh3jwhDwbMn36zY8f71f\nHrT7x75afzx80PERAygbE7qeRdxKdermMy2ddQh9gqIqTZj2C19XxYPWmZo1/qm3\nFlSBpBhTpNL+qrvz3/SZ7wlzd1RhA/R6YrTY4hr4IXOSskYjfPzf127/mGo06C24\nlG28eYkId1E0Jgztp8pf2Aj8L+m83IBCQN3JHhv5PCqUay9RUKd4l+8pw5aStw7n\nQdFJGWGlbqQ/PWEl5pNa1PY8EqSj9cVIkUZiWZcRyDcbouALCtfZERmXBYKKIwkR\nNnNw4yCJvURMw+X2G1U/\n=ytFQ\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 7e829a5345dc993cd21ead4f29ff7b5f220668b5\nparent 7d2dbe87871decc0ae502fd30b8805d0ff6def43\nauthor Kim Morrison <477956+kim-em@users.noreply.github.com> 1765508375 +1100\ncommitter GitHub <noreply@github.com> 1765508375 +0000\n\nfeat: `@[suggest_for ℤ]` and `@[suggest_for ℚ]` annotations (#11596)\n\nThis PR adds `@[suggest_for ℤ]` on `Int` and `@[suggest_for ℚ]` on\n`Rat`, following the pattern established by `@[suggest_for ℕ]` on `Nat`\nin #11554.\n\n\n🤖 Prepared with Claude Code\n\nCo-authored-by: Claude Opus 4.5 <noreply@anthropic.com>",
        "verified_at": "2025-12-12T02:59:51Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/552fa10a60c5a413f8ed3718c5510439235f3d2b",
    "html_url": "https://github.com/leanprover/lean4/commit/552fa10a60c5a413f8ed3718c5510439235f3d2b",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/552fa10a60c5a413f8ed3718c5510439235f3d2b/comments",
    "author": {
      "login": "kim-em",
      "id": 477956,
      "node_id": "MDQ6VXNlcjQ3Nzk1Ng==",
      "avatar_url": "https://avatars.githubusercontent.com/u/477956?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/kim-em",
      "html_url": "https://github.com/kim-em",
      "followers_url": "https://api.github.com/users/kim-em/followers",
      "following_url": "https://api.github.com/users/kim-em/following{/other_user}",
      "gists_url": "https://api.github.com/users/kim-em/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/kim-em/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/kim-em/subscriptions",
      "organizations_url": "https://api.github.com/users/kim-em/orgs",
      "repos_url": "https://api.github.com/users/kim-em/repos",
      "events_url": "https://api.github.com/users/kim-em/events{/privacy}",
      "received_events_url": "https://api.github.com/users/kim-em/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "7d2dbe87871decc0ae502fd30b8805d0ff6def43",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/7d2dbe87871decc0ae502fd30b8805d0ff6def43",
        "html_url": "https://github.com/leanprover/lean4/commit/7d2dbe87871decc0ae502fd30b8805d0ff6def43"
      }
    ]
  },
  {
    "sha": "7d2dbe87871decc0ae502fd30b8805d0ff6def43",
    "node_id": "C_kwDOB7kabNoAKDdkMmRiZTg3ODcxZGVjYzBhZTUwMmZkMzBiODgwNWQwZmY2ZGVmNDM",
    "commit": {
      "author": {
        "name": "Robert Maxton",
        "email": "robert.maxton42@gmail.com",
        "date": "2025-12-12T02:57:49Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-12T02:57:49Z"
      },
      "message": "feat: expose `decidable_of_bool` (#11625)\n\nThis PR adds `@[expose]` to `decidable_of_bool` so that\nproofs-by-`decide` elsewhere that reduce to `decidable_of_bool` continue\nto reduce.",
      "tree": {
        "sha": "2f5eb62815a455b0ba635a9793f305257f64613c",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/2f5eb62815a455b0ba635a9793f305257f64613c"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/7d2dbe87871decc0ae502fd30b8805d0ff6def43",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpO4S9CRC1aQ7uu5UhlAAArV4QADfjY9KTi+HX3Iz+XqH7yHgS\nf4vagl8tv7WAQF3thsEvR0wgt6WrKv/tNBFHgNO2c8tks221FBaXD+ua/Nk6BZP6\n1uwb0qoGVemkaqgBfrA6Bt0jB2LqAtZQWNyhR50NfKnCLG6BSVSGx/8K2PYPSw8a\nRGfqty8yymbe79kqDO0SY4E5TAjc16PRJBUPiiIh1/N6j3EC2O7vBNBtJNAjWeZP\npXSHANXumbThMawCNf/r95Ua1c49iH4D5WfibxuMnbneHvqZcFrkGrfQnmnOUop6\nZ7cfEfPupUun92zW4Nh2+1mv9ahmSyh4nodHRK3zcrEOIR+TtUp2k1C72m8jwkFJ\nhxKp8aTZol18447wIOaDpUHNQHVN2mkAascUIvP2nGrmlob9QRTnmBW8hXohFhfk\nXOLJwc3g5xxPNJSnGIMCSqOtmquMW9mb5FQp1/2cFTXeEyQ/Oy3fkdTBnYWUgVGw\nZUt8F0KR5tFPPImU5bnRErSCSQTyEkpfrZWPgGPd5nwQQWY2lfRhKUgC3K9OIt+/\nZ4ylfB+e2Z/gXb/4jTJ8ETE6dw6SMrtrTT/rS2RocyHn49zxbRSjB3TElV18Sy8r\nT3xGn2EvaOMJuZm4jredUdY4lEGt6Fxxa5XtRo+L/2n66LXKEeJuvp70JG5Evber\niknZxJB4M5je4W11BDO2\n=djN3\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 2f5eb62815a455b0ba635a9793f305257f64613c\nparent 3bd1dd633f29de1dd0ea0e23833da7710bdb1c25\nauthor Robert Maxton <robert.maxton42@gmail.com> 1765508269 -0800\ncommitter GitHub <noreply@github.com> 1765508269 +0000\n\nfeat: expose `decidable_of_bool` (#11625)\n\nThis PR adds `@[expose]` to `decidable_of_bool` so that\nproofs-by-`decide` elsewhere that reduce to `decidable_of_bool` continue\nto reduce.",
        "verified_at": "2025-12-12T02:58:05Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/7d2dbe87871decc0ae502fd30b8805d0ff6def43",
    "html_url": "https://github.com/leanprover/lean4/commit/7d2dbe87871decc0ae502fd30b8805d0ff6def43",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/7d2dbe87871decc0ae502fd30b8805d0ff6def43/comments",
    "author": {
      "login": "robertmaxton42",
      "id": 13130661,
      "node_id": "MDQ6VXNlcjEzMTMwNjYx",
      "avatar_url": "https://avatars.githubusercontent.com/u/13130661?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/robertmaxton42",
      "html_url": "https://github.com/robertmaxton42",
      "followers_url": "https://api.github.com/users/robertmaxton42/followers",
      "following_url": "https://api.github.com/users/robertmaxton42/following{/other_user}",
      "gists_url": "https://api.github.com/users/robertmaxton42/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/robertmaxton42/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/robertmaxton42/subscriptions",
      "organizations_url": "https://api.github.com/users/robertmaxton42/orgs",
      "repos_url": "https://api.github.com/users/robertmaxton42/repos",
      "events_url": "https://api.github.com/users/robertmaxton42/events{/privacy}",
      "received_events_url": "https://api.github.com/users/robertmaxton42/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
        "html_url": "https://github.com/leanprover/lean4/commit/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25"
      }
    ]
  },
  {
    "sha": "3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
    "node_id": "C_kwDOB7kabNoAKDNiZDFkZDYzM2YyOWRlMWRkMGVhMGUyMzgzM2RhNzcxMGJkYjFjMjU",
    "commit": {
      "author": {
        "name": "Robert J. Simmons",
        "email": "442315+robsimmons@users.noreply.github.com",
        "date": "2025-12-11T21:40:16Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T21:40:16Z"
      },
      "message": "feat: identifier suggestions on some autobinding failures (#11621)\n\nThis PR causes Lean to search through `@[suggest_for]` annotations on\ncertain errors that look like unknown identifiers that got incorrectly\nautobound. This will correctly identify that a declaration of type\n`Maybe String` should be `Option String` instead.\n\n## Example\n\n```\nexample : Except String Unit := return .ok ()\n```\n\n```\nFunction expected at\n  Result\nbut this term has type\n  ?m.1\n\nNote: Expected a function because this term is being applied to the argument\n  String\n\nHint: The identifier `Result` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.\n\nPerhaps you meant `Except` in place of `Result`?\n```\n\nThe last line is added by this PR.",
      "tree": {
        "sha": "ee8218804c649a0215e2547b222aba4a61ac7f7d",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/ee8218804c649a0215e2547b222aba4a61ac7f7d"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOzpQCRC1aQ7uu5UhlAAAH3IQADt/NWeMbn/p3M73IkOtVAW2\n93Wu+aeiMmMxkameeaUb5dk9/SXsyUxMVyss1XExOTIRl8XMIJcqEZa2Se4nyVOk\n6yhA0p/uJw8prBD0zhwLZBQvKmIn3cKAde7FiVPGvCQmc89ytEJEF5h1D5uywhcl\nHtj/1aNQBZMB5LJt6VvX5kjj4/6NjjBrnKQeVC5BXCPuGttQrA6BvijP0UZSCK/+\nbsgPnv3th3wiU39KInJChXvTcL8EWoQdiXxcyimotZw74hgNfOR0fnuo0IcXddAL\n9avzu4kjF02AA2AdgAGiWwCGb6DdiJKNIZnWYQtvGyK7tCl83/NidZ5vkPlseT54\n8kcLpbCs6zuUujG/ysl0FCwTNhxWwHc+5PQOGEvQzT9MhU8ROVg1yZfcKfxhzF/N\nOph+F8l/usJR0qHh6WpFSf/aBs3xxxOXQpotZ7pbj1IpCD8D9lGRPU3bN7iOrC6j\nfA4mD7UmQR7ZCVuAQKQCfz8y4spBDy+imX+bS9ShDHrZai3Q+qn4DZBr6/OHPFli\nB5ZljdW2q8bop+bAxfjhR3KjJvYEXjEkB6PE0c1X7kMKqA6CcQuhdY7rClY1Fvhb\n2ircyUcgwFm+h2yI/OOpEP6MG/VqTPX4lSZBWpr356tnCqCSffOUwXO4Iz07e6m6\nK5SuoBSXFRgWSRN84MYa\n=E1za\n-----END PGP SIGNATURE-----\n",
        "payload": "tree ee8218804c649a0215e2547b222aba4a61ac7f7d\nparent d824f7e0858e81d7d06726fcd1b5b415a48676ad\nauthor Robert J. Simmons <442315+robsimmons@users.noreply.github.com> 1765489216 -0500\ncommitter GitHub <noreply@github.com> 1765489216 +0000\n\nfeat: identifier suggestions on some autobinding failures (#11621)\n\nThis PR causes Lean to search through `@[suggest_for]` annotations on\ncertain errors that look like unknown identifiers that got incorrectly\nautobound. This will correctly identify that a declaration of type\n`Maybe String` should be `Option String` instead.\n\n## Example\n\n```\nexample : Except String Unit := return .ok ()\n```\n\n```\nFunction expected at\n  Result\nbut this term has type\n  ?m.1\n\nNote: Expected a function because this term is being applied to the argument\n  String\n\nHint: The identifier `Result` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.\n\nPerhaps you meant `Except` in place of `Result`?\n```\n\nThe last line is added by this PR.",
        "verified_at": "2025-12-11T21:40:32Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
    "html_url": "https://github.com/leanprover/lean4/commit/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/3bd1dd633f29de1dd0ea0e23833da7710bdb1c25/comments",
    "author": {
      "login": "robsimmons",
      "id": 442315,
      "node_id": "MDQ6VXNlcjQ0MjMxNQ==",
      "avatar_url": "https://avatars.githubusercontent.com/u/442315?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/robsimmons",
      "html_url": "https://github.com/robsimmons",
      "followers_url": "https://api.github.com/users/robsimmons/followers",
      "following_url": "https://api.github.com/users/robsimmons/following{/other_user}",
      "gists_url": "https://api.github.com/users/robsimmons/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/robsimmons/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/robsimmons/subscriptions",
      "organizations_url": "https://api.github.com/users/robsimmons/orgs",
      "repos_url": "https://api.github.com/users/robsimmons/repos",
      "events_url": "https://api.github.com/users/robsimmons/events{/privacy}",
      "received_events_url": "https://api.github.com/users/robsimmons/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "d824f7e0858e81d7d06726fcd1b5b415a48676ad",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/d824f7e0858e81d7d06726fcd1b5b415a48676ad",
        "html_url": "https://github.com/leanprover/lean4/commit/d824f7e0858e81d7d06726fcd1b5b415a48676ad"
      }
    ]
  },
  {
    "sha": "d824f7e0858e81d7d06726fcd1b5b415a48676ad",
    "node_id": "C_kwDOB7kabNoAKGQ4MjRmN2UwODU4ZTgxZDdkMDY3MjZmY2QxYjViNDE1YTQ4Njc2YWQ",
    "commit": {
      "author": {
        "name": "Robert J. Simmons",
        "email": "442315+robsimmons@users.noreply.github.com",
        "date": "2025-12-11T19:47:18Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T19:47:18Z"
      },
      "message": "feat: identifier suggestions for non-dotted identifiers (#11619)\n\nThis PR allows Lean to present suggestions based on `@[suggest_for]`\nannotations for unknown identifiers without internal dots. (The\nannotations in #11554 only gave suggestion for dotted identifiers like\n`Array.every`->`Array.all` and not for bare identifiers like\n`Result`->`Except` or `ℕ`->`Nat`.)",
      "tree": {
        "sha": "e76b2d88538748b46eef442435dae0563c4a79eb",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/e76b2d88538748b46eef442435dae0563c4a79eb"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/d824f7e0858e81d7d06726fcd1b5b415a48676ad",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOx/VCRC1aQ7uu5UhlAAAJswQAEvcg+gh7X4G+HFBkIzUDPz4\n1AYe8/A18j6gJmpe+Vqk8+gKD0wAqk57RansiiibsgHUg+5fyZUiqxN0lFpWTaGF\nbkq1bBHbepyE9mx4RylqyEJT0GzOY2jk+IyEGWog0gHJ0S1/kTp9sdn08Jv/Skvm\nRU6iq6tREQJmYTw8XRyha2phrFENPBzM714+PwbEdKCtZ5YP8Ic1+2sTFCWlQXCQ\nEVTDcTTisn48dHM+tLh8BA+qwYPMuy9jeXUSMNliBTkxcHYVC3iAq7bRnCPqHeXK\nY5DcVpBE0UH1lR8zRgWW+nb2hI2b/uSqsoxtZfT1rgJuI+R3n0k2SeiVTrMPlPdC\nulQXkhP53wIWuOBDDmjtoV2bcFpE2UpKvgar5Ek+KyMdoBipbz8YaezoIPgzFEcp\n4NeWFTTCS1N5p+QF4hGBOzORb+pgmpd7kWa7jkzP/ageyfFPDfMYALBrzL29/pcZ\nZlN4pz30c0bfZZR534+8Qmg+r2IbX544SY3RHrbz40FOVUSZdeWB8yDbJ8P7p8Tg\neqOwp3ZjztpFLWDhi1rTPLlw0zsxeiDaslgzTcz2vf3vkhs727Lv1clW3gLBX7X3\nVSCs39c8+u7bDpAnsKrko/OR6feJh1Vb/N/iw1WkYjUoHnlbmmw7w4dOxW/ErR1O\nxW7SKBpY4HX4asCE4GZW\n=Hif6\n-----END PGP SIGNATURE-----\n",
        "payload": "tree e76b2d88538748b46eef442435dae0563c4a79eb\nparent 381c0f2b615a98a5efbe08b90a5e808e23d9b550\nauthor Robert J. Simmons <442315+robsimmons@users.noreply.github.com> 1765482438 -0500\ncommitter GitHub <noreply@github.com> 1765482438 +0000\n\nfeat: identifier suggestions for non-dotted identifiers (#11619)\n\nThis PR allows Lean to present suggestions based on `@[suggest_for]`\nannotations for unknown identifiers without internal dots. (The\nannotations in #11554 only gave suggestion for dotted identifiers like\n`Array.every`->`Array.all` and not for bare identifiers like\n`Result`->`Except` or `ℕ`->`Nat`.)",
        "verified_at": "2025-12-11T19:47:34Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/d824f7e0858e81d7d06726fcd1b5b415a48676ad",
    "html_url": "https://github.com/leanprover/lean4/commit/d824f7e0858e81d7d06726fcd1b5b415a48676ad",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/d824f7e0858e81d7d06726fcd1b5b415a48676ad/comments",
    "author": {
      "login": "robsimmons",
      "id": 442315,
      "node_id": "MDQ6VXNlcjQ0MjMxNQ==",
      "avatar_url": "https://avatars.githubusercontent.com/u/442315?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/robsimmons",
      "html_url": "https://github.com/robsimmons",
      "followers_url": "https://api.github.com/users/robsimmons/followers",
      "following_url": "https://api.github.com/users/robsimmons/following{/other_user}",
      "gists_url": "https://api.github.com/users/robsimmons/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/robsimmons/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/robsimmons/subscriptions",
      "organizations_url": "https://api.github.com/users/robsimmons/orgs",
      "repos_url": "https://api.github.com/users/robsimmons/repos",
      "events_url": "https://api.github.com/users/robsimmons/events{/privacy}",
      "received_events_url": "https://api.github.com/users/robsimmons/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "381c0f2b615a98a5efbe08b90a5e808e23d9b550",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/381c0f2b615a98a5efbe08b90a5e808e23d9b550",
        "html_url": "https://github.com/leanprover/lean4/commit/381c0f2b615a98a5efbe08b90a5e808e23d9b550"
      }
    ]
  },
  {
    "sha": "381c0f2b615a98a5efbe08b90a5e808e23d9b550",
    "node_id": "C_kwDOB7kabNoAKDM4MWMwZjJiNjE1YTk4YTVlZmJlMDhiOTBhNWU4MDhlMjNkOWI1NTA",
    "commit": {
      "author": {
        "name": "Sebastian Graf",
        "email": "sgraf1337@gmail.com",
        "date": "2025-12-11T17:44:52Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T17:44:52Z"
      },
      "message": "fix: proper error messages for `Std.Do` tactic invokations without arguments (#11509) (#11607)\n\nThis PR makes argument-less tactic invokations of `Std.Do` tactics such\nas `mintro` emit a proper error message \"`mintro` expects at least one\npattern\" instead of claiming that `Std.Tactic.Do` needs to be imported.\n\nCloses #11509.",
      "tree": {
        "sha": "f6fdd2984479cc5db4b0ee5fb1227df2baea61e4",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/f6fdd2984479cc5db4b0ee5fb1227df2baea61e4"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/381c0f2b615a98a5efbe08b90a5e808e23d9b550",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOwMkCRC1aQ7uu5UhlAAAhsMQAAWph9OSwjkRk3yDOaUIbE+F\nA37AnY3h8G5PHiPmOY0d1dJ9+YyoneZftibftC/vfNfXVH3XdNeSrDIJCpqNadG8\nkxZaupJ7zYU3quO7Pnh2muqi02kjq2pUUlz4OZfqcfifAfTPsITvBYzEB58rRYLG\nxltgY7CFAUOAt5qI38C5qk5+Pq8JYcdgD9naEwudz9X4by9KUoaaYHrSR0Cbl3YJ\nnHp/Ric1ejTu9Fv4MRyZD9QJoa012GI02OrHwS2G9/fXOpczG2wNVFar1YUnJRqf\nSrxSfkKjKgOBg5MJi2qetTypUBz8Ctr0vi14JPdL+an9wZJD94w1oW6lbGFkDVa8\nTTMDPKMeCAfmaZisZkk+WS0id69XLDJTAvKiJpaQl4ivPfBajYxsBctMNHXLUX43\n9VoDtOz9gM3jAMq5a3/PEw3UXFIWD2ZEkzuxZ1ZJOv4Y/agXuZKkFRe2DFNmQEg5\nvzI6cE0A9AeIgNFP/yRQkvbJMRRaKkD7c88NI6kqPAka9Xp16nm6IOJYYD9Gbrmu\nvGqDRGFscx6qgP2RupQDV5AB3RhVb3UMY5XettrnH+vxgsQS/GFwx9AOko6R4vZP\nxEj6agOGMJh3e/+hC1QN900tbUncHZ5BB9d5/m7/FH4nkGFZJI7VODX5+q7Pz4ve\nIQHZ+inXgIneqsFdRPdg\n=fMNR\n-----END PGP SIGNATURE-----\n",
        "payload": "tree f6fdd2984479cc5db4b0ee5fb1227df2baea61e4\nparent 2d3dec41ca8c1fe670dba2afc2147904e4854409\nauthor Sebastian Graf <sgraf1337@gmail.com> 1765475092 +0100\ncommitter GitHub <noreply@github.com> 1765475092 +0000\n\nfix: proper error messages for `Std.Do` tactic invokations without arguments (#11509) (#11607)\n\nThis PR makes argument-less tactic invokations of `Std.Do` tactics such\nas `mintro` emit a proper error message \"`mintro` expects at least one\npattern\" instead of claiming that `Std.Tactic.Do` needs to be imported.\n\nCloses #11509.",
        "verified_at": "2025-12-11T17:45:08Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/381c0f2b615a98a5efbe08b90a5e808e23d9b550",
    "html_url": "https://github.com/leanprover/lean4/commit/381c0f2b615a98a5efbe08b90a5e808e23d9b550",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/381c0f2b615a98a5efbe08b90a5e808e23d9b550/comments",
    "author": {
      "login": "sgraf812",
      "id": 1151264,
      "node_id": "MDQ6VXNlcjExNTEyNjQ=",
      "avatar_url": "https://avatars.githubusercontent.com/u/1151264?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/sgraf812",
      "html_url": "https://github.com/sgraf812",
      "followers_url": "https://api.github.com/users/sgraf812/followers",
      "following_url": "https://api.github.com/users/sgraf812/following{/other_user}",
      "gists_url": "https://api.github.com/users/sgraf812/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/sgraf812/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/sgraf812/subscriptions",
      "organizations_url": "https://api.github.com/users/sgraf812/orgs",
      "repos_url": "https://api.github.com/users/sgraf812/repos",
      "events_url": "https://api.github.com/users/sgraf812/events{/privacy}",
      "received_events_url": "https://api.github.com/users/sgraf812/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "2d3dec41ca8c1fe670dba2afc2147904e4854409",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/2d3dec41ca8c1fe670dba2afc2147904e4854409",
        "html_url": "https://github.com/leanprover/lean4/commit/2d3dec41ca8c1fe670dba2afc2147904e4854409"
      }
    ]
  },
  {
    "sha": "2d3dec41ca8c1fe670dba2afc2147904e4854409",
    "node_id": "C_kwDOB7kabNoAKDJkM2RlYzQxY2E4YzFmZTY3MGRiYTJhZmMyMTQ3OTA0ZTQ4NTQ0MDk",
    "commit": {
      "author": {
        "name": "Sebastian Ullrich",
        "email": "sebasti@nullri.ch",
        "date": "2025-12-11T17:24:01Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T17:24:01Z"
      },
      "message": "perf: avoid blocking on proof elaboration in `Environment.hasUnsafe` (#11606)",
      "tree": {
        "sha": "b836f5b552b406c695fcc4e52209623dbd3da07b",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/b836f5b552b406c695fcc4e52209623dbd3da07b"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/2d3dec41ca8c1fe670dba2afc2147904e4854409",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOv5BCRC1aQ7uu5UhlAAABVsQABXvqd8y0aZGbO9HZlwlr5b9\noIi3tSgzl7u0vp745vv5DtyOvOXoJ8+SwazTJm7mhdXDX5CkE2HJbcRQ/eIPgHDk\n57l3I6rUUyw/TbZItGqcebGTjID8F0JnnqhoVqh8pYz6FH9uClbHISUi5JvtCa2A\nVVKJoXUrE0e5BIq2f2jwOOLAhbs50RPjIhhXxZVExNnQqGOB7Rg7FwulHBcdBP4a\nwrJSyaKdZSBPforoxma2eZuxdJpAf3xW2ErW8ECIR96VmyjRuMQOSNRI5h9lnxFZ\nEW6CLcXkGDsTa06jGa8ocyyI+OE21/RIm14AD4cp4QwZcmLXWnisGKmUDUNyZEZq\nVS1V37M0tJvjd8USn0jrmH8Iw5Ag6RF5hPY1knv2IG4rbprBy2xdV/I/Z6rzGUam\n8mXV6D0+hlNHBSDXmXtQh0Hw+1iHnQRVuk5KdlMXtCeXXZWrf6JoUdYEwOdglF+r\nK96GrnKzmz6WuqHqwTvRe9hO6sRG2n3/jSyQGn8UnVgvhFbJ7BrqkNCPa++RubTl\n6yQdv6XenR09MRX3WnMQRzVXgTBnH5nUT1oJRHdHF/2ewOsiCc4aoEsxmzIESzwa\nCjCrQAyQlic/v4TXOUxednYvatBjmSFiPxFKxMBjJWY7HKCOZ8gtM1degjiYbBkB\nIYO+3tO4GsR972kBVYYH\n=CrXE\n-----END PGP SIGNATURE-----\n",
        "payload": "tree b836f5b552b406c695fcc4e52209623dbd3da07b\nparent cec9758c2d2b34f586e896777d08f1a1edc8dbd5\nauthor Sebastian Ullrich <sebasti@nullri.ch> 1765473841 +0100\ncommitter GitHub <noreply@github.com> 1765473841 +0000\n\nperf: avoid blocking on proof elaboration in `Environment.hasUnsafe` (#11606)\n\n",
        "verified_at": "2025-12-11T17:24:18Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/2d3dec41ca8c1fe670dba2afc2147904e4854409",
    "html_url": "https://github.com/leanprover/lean4/commit/2d3dec41ca8c1fe670dba2afc2147904e4854409",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/2d3dec41ca8c1fe670dba2afc2147904e4854409/comments",
    "author": {
      "login": "Kha",
      "id": 109126,
      "node_id": "MDQ6VXNlcjEwOTEyNg==",
      "avatar_url": "https://avatars.githubusercontent.com/u/109126?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/Kha",
      "html_url": "https://github.com/Kha",
      "followers_url": "https://api.github.com/users/Kha/followers",
      "following_url": "https://api.github.com/users/Kha/following{/other_user}",
      "gists_url": "https://api.github.com/users/Kha/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/Kha/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/Kha/subscriptions",
      "organizations_url": "https://api.github.com/users/Kha/orgs",
      "repos_url": "https://api.github.com/users/Kha/repos",
      "events_url": "https://api.github.com/users/Kha/events{/privacy}",
      "received_events_url": "https://api.github.com/users/Kha/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
        "html_url": "https://github.com/leanprover/lean4/commit/cec9758c2d2b34f586e896777d08f1a1edc8dbd5"
      }
    ]
  },
  {
    "sha": "cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
    "node_id": "C_kwDOB7kabNoAKGNlYzk3NThjMmQyYjM0ZjU4NmU4OTY3NzdkMDhmMWExZWRjOGRiZDU",
    "commit": {
      "author": {
        "name": "Garmelon",
        "email": "joscha@plugh.de",
        "date": "2025-12-11T16:10:27Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T16:10:27Z"
      },
      "message": "chore: measure dynamic symbols in benchmarks (#11568)\n\nAdd back the dynamic symbol measurements that were removed in #11264.",
      "tree": {
        "sha": "aa7ebfb281cd3aa5856cd7920408513543c2b7dc",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/aa7ebfb281cd3aa5856cd7920408513543c2b7dc"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOu0CCRC1aQ7uu5UhlAAA04wQADXcT52L8e9dQTkcsvfy67RV\n7ju3UEDq1gsxYD2ac2yOnqSQF3SvzfSFdnC7kXFQl7lVPjwbbZk2rXac9t7UWkXn\nJIBXH2qjXUzeWj32W57B92R7vtryJm0O4ZLKv9mHokpStyRovL9MD1lOwk2e+VO1\nKGfy0kanLqK+Gf5kyHLd4CoSBsVxDdaRbw+P8EDYXmpQchfP50Oy3h+R3jhUnSoF\nRrRo3UpBpeOlNg5LUf7r515xstt2DFDjNZFit4/5zCg4r38j9iK5czV3RpPaFf4S\nKr6j+ov0dmS3zdfJe8Sc658PMoRGsqcDNCOmjwGqCSgkaro0dtvsmlKLaVv7aDEr\n+A17PLvVsYe2X6IGFKCaO95Hn0AuLCenPD2d6S+0s8tF7OCLvFMpTxc4u/IOdPKu\nVeFM5kJrMrMLSAw6hPR5UqRDoZKm+i6b77hQk7A2BFzDzxFSqh171IOMpsvmNbak\nejBty0mt4HLDtZpCFkslNhgYfqLpIbRfcbWpCpKVbzFBaS47ghYw4ksg0GRiAKg+\nLy7AbbxOWFoAQwKlpuXvsJNv+QdcoAj27WnamUNKWcGz2g0uAcWu+KvvghV2Zap1\n3AHgh14cQhT5w4xA7eDrANfWuHKL7pYJy9c14Uq+AbCOdF/cKFETJ7ewqM0KcCbg\nrRbDy3/IY4Q7T0xiffmS\n=8uAe\n-----END PGP SIGNATURE-----\n",
        "payload": "tree aa7ebfb281cd3aa5856cd7920408513543c2b7dc\nparent c4477939d07116df842258bf8f9267deea51c466\nauthor Garmelon <joscha@plugh.de> 1765469427 +0100\ncommitter GitHub <noreply@github.com> 1765469427 +0000\n\nchore: measure dynamic symbols in benchmarks (#11568)\n\nAdd back the dynamic symbol measurements that were removed in #11264.",
        "verified_at": "2025-12-11T16:10:43Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
    "html_url": "https://github.com/leanprover/lean4/commit/cec9758c2d2b34f586e896777d08f1a1edc8dbd5",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/cec9758c2d2b34f586e896777d08f1a1edc8dbd5/comments",
    "author": {
      "login": "Garmelon",
      "id": 11077553,
      "node_id": "MDQ6VXNlcjExMDc3NTUz",
      "avatar_url": "https://avatars.githubusercontent.com/u/11077553?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/Garmelon",
      "html_url": "https://github.com/Garmelon",
      "followers_url": "https://api.github.com/users/Garmelon/followers",
      "following_url": "https://api.github.com/users/Garmelon/following{/other_user}",
      "gists_url": "https://api.github.com/users/Garmelon/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/Garmelon/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/Garmelon/subscriptions",
      "organizations_url": "https://api.github.com/users/Garmelon/orgs",
      "repos_url": "https://api.github.com/users/Garmelon/repos",
      "events_url": "https://api.github.com/users/Garmelon/events{/privacy}",
      "received_events_url": "https://api.github.com/users/Garmelon/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "c4477939d07116df842258bf8f9267deea51c466",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/c4477939d07116df842258bf8f9267deea51c466",
        "html_url": "https://github.com/leanprover/lean4/commit/c4477939d07116df842258bf8f9267deea51c466"
      }
    ]
  },
  {
    "sha": "c4477939d07116df842258bf8f9267deea51c466",
    "node_id": "C_kwDOB7kabNoAKGM0NDc3OTM5ZDA3MTE2ZGY4NDIyNThiZjhmOTI2N2RlZWE1MWM0NjY",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T15:42:42Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T15:42:42Z"
      },
      "message": "feat: `Int.subNatNat` in `grind` (#11615)\n\nThis PR adds a normalization rule for `Int.subNatNat` to `grind`.\n\nCloses #11543",
      "tree": {
        "sha": "9fc040efb716255fcb7b16d4d9818a0533720745",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/9fc040efb716255fcb7b16d4d9818a0533720745"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/c4477939d07116df842258bf8f9267deea51c466",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOukYCRC1aQ7uu5UhlAAAAlAQACNtZ1zer2yc0j2/tEuNGX5/\nv7tcYSDy6isPTGcS+ZPe5kJkuva/M3tE3m4ehE5mCMYk12dSt/BOnf9zWPavrmlp\noSl6SWYGwlOOguEJGjk1iKaD1CstUfGcndUU26VL7GJZrAu3kgQazmtxGODxka5m\nYP+pstf+1x8zpDcEd4+oR7vB9bMHQazqz3nx3MoDpRMw4kZn3vfhoIEQ91p9XfV+\n2Hh+v4ThMCEFipSrdlWKcc9KaabBmzi0Nwll4iUUg/UT4HPIWPUNZFC5uYh0sLZ0\nwyfsGAzPSlkAe5Sw4kDCL8XTteP8OivTXnavXvxBMrdrwdDRrW0HozD5ua7L5WrI\nMTrsy/G1p3v9XL+nevIK3e6TzYS92GPXpkw4fNaD7Ln4M2yCxz2ky48K+UR+liC+\nOhXRbISi8PklX2z7ti028WLwRuSfBj1A/qEodkd+uZ9vqguOxnGmBi9Fpu9ftefH\nKCXp30A9/QMUEyV1S9Wb649nNGIdByNm2qX6i2mVFH9TJW6ZPmJlM1EvUl9KIMKN\nkWaa7Y0GBgRfT669gZIYiG/4LWMYNKHQCnGh++rH5EjpiPemK4BB9zkEkrjssS5b\nlar5onW51KtsOY9NBHV1z9olUWFCpyrSmuNpBu7sEzIOWdNH9Kr9E/2XoaSg+SR7\n9+p1mTkGeEd+y5msAvDo\n=aUMO\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 9fc040efb716255fcb7b16d4d9818a0533720745\nparent 864acddb4a2e3c0f584b24db333a901be3ee6c6f\nauthor Leonardo de Moura <leomoura@amazon.com> 1765467762 +0100\ncommitter GitHub <noreply@github.com> 1765467762 +0000\n\nfeat: `Int.subNatNat` in `grind` (#11615)\n\nThis PR adds a normalization rule for `Int.subNatNat` to `grind`.\n\nCloses #11543",
        "verified_at": "2025-12-11T15:54:01Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/c4477939d07116df842258bf8f9267deea51c466",
    "html_url": "https://github.com/leanprover/lean4/commit/c4477939d07116df842258bf8f9267deea51c466",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/c4477939d07116df842258bf8f9267deea51c466/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "864acddb4a2e3c0f584b24db333a901be3ee6c6f",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/864acddb4a2e3c0f584b24db333a901be3ee6c6f",
        "html_url": "https://github.com/leanprover/lean4/commit/864acddb4a2e3c0f584b24db333a901be3ee6c6f"
      }
    ]
  },
  {
    "sha": "864acddb4a2e3c0f584b24db333a901be3ee6c6f",
    "node_id": "C_kwDOB7kabNoAKDg2NGFjZGRiNGEyZTNjMGY1ODRiMjRkYjMzM2E5MDFiZTNlZTZjNmY",
    "commit": {
      "author": {
        "name": "Lean stage0 autoupdater",
        "email": "",
        "date": "2025-12-11T15:53:31Z"
      },
      "committer": {
        "name": "Lean stage0 autoupdater",
        "email": "",
        "date": "2025-12-11T15:53:31Z"
      },
      "message": "chore: update stage0",
      "tree": {
        "sha": "511db0f5e261f4b7d14d1f58d1247ba05788142c",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/511db0f5e261f4b7d14d1f58d1247ba05788142c"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/864acddb4a2e3c0f584b24db333a901be3ee6c6f",
      "comment_count": 0,
      "verification": {
        "verified": false,
        "reason": "unsigned",
        "signature": null,
        "payload": null,
        "verified_at": null
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/864acddb4a2e3c0f584b24db333a901be3ee6c6f",
    "html_url": "https://github.com/leanprover/lean4/commit/864acddb4a2e3c0f584b24db333a901be3ee6c6f",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/864acddb4a2e3c0f584b24db333a901be3ee6c6f/comments",
    "author": {

    },
    "committer": {

    },
    "parents": [
      {
        "sha": "26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
        "html_url": "https://github.com/leanprover/lean4/commit/26ff270e28c3c76bb78e47bd5bfdb065a813cfab"
      }
    ]
  },
  {
    "sha": "26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
    "node_id": "C_kwDOB7kabNoAKDI2ZmYyNzBlMjhjM2M3NmJiNzhlNDdiZDViZmRiMDY1YTgxM2NmYWI",
    "commit": {
      "author": {
        "name": "Robert J. Simmons",
        "email": "442315+robsimmons@users.noreply.github.com",
        "date": "2025-12-11T15:21:33Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T15:21:33Z"
      },
      "message": "fix: better performance for `@[suggest_for]` (#11598)\n\nThis PR fixes a performance issue resulting from misusing persistent\nenvironment extensions that was introduced in #11554.",
      "tree": {
        "sha": "1d71d10adf6a464a3194592c30fb44ba156f7b6a",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/1d71d10adf6a464a3194592c30fb44ba156f7b6a"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOuGNCRC1aQ7uu5UhlAAAcg0QAKvCBw7WC/rTuBRYHA/hfRVb\nCLMm98D6Bx35NvflPdYWrRe+TI1hb0bYzAQPsrrR0AFgd1R1k4xkrmAtneJIpPNm\n3l0j+9vruRQMDgT2c4U9iIkvLM/DYXB4w33jjmiyX3E2XENgUZ0AxxvcwHcnqRue\nmWsZ3rctpkdt7Br1fJ8/U4YrX8y4xSMueWlRO+ePKMc20PJDv1jKJsvokGePpXSD\nZePGuCXghm65LKr6QAIBoZ8nMk7kLhYkQ2Z7wEoEO1Zcz5jyrZaYGDWAt9E6oR1G\nzNKNZ4Be+ZmKZeg/jRetB8nAGu/mUmrZMd0Ya3nRChQulB1KgtEh12TG5fi1PbyD\nStxGsAgYb0qzWgYfFKGOLdJS3HRKWsAa+s+B3sa0q6oFdTXibKB3MM1Ri0Kq4Z4c\naKXC5oAj31nEPRiyHECrG70XyeKqxSsQeq6lPveo7S6LM9Qj4DojL80iRQf5W7Kf\njzIpkxVjiCsVhPVxCO3GzkPpgjKNZDSoe6cEbWlQMe2KgB7TdI1bavxL4/g0inoe\nbucifmVZN89AU3wuE4tL5dPcoTaeEonwosg4X6b9JlWInKMAvXKQX3yWAhMGjFYT\nM68sAL+9gQiC+GyBKVUQbvF48GAKrBD4MToU2IRIwIeaNmUSWqQa+/yoCyZtCQ1D\nDWvVo8qehlA22xwlI71Y\n=lNQJ\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 1d71d10adf6a464a3194592c30fb44ba156f7b6a\nparent 6469890178986678af97999948b0dd7173554af2\nauthor Robert J. Simmons <442315+robsimmons@users.noreply.github.com> 1765466493 -0500\ncommitter GitHub <noreply@github.com> 1765466493 +0000\n\nfix: better performance for `@[suggest_for]` (#11598)\n\nThis PR fixes a performance issue resulting from misusing persistent\nenvironment extensions that was introduced in #11554.",
        "verified_at": "2025-12-11T15:21:49Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
    "html_url": "https://github.com/leanprover/lean4/commit/26ff270e28c3c76bb78e47bd5bfdb065a813cfab",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/26ff270e28c3c76bb78e47bd5bfdb065a813cfab/comments",
    "author": {
      "login": "robsimmons",
      "id": 442315,
      "node_id": "MDQ6VXNlcjQ0MjMxNQ==",
      "avatar_url": "https://avatars.githubusercontent.com/u/442315?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/robsimmons",
      "html_url": "https://github.com/robsimmons",
      "followers_url": "https://api.github.com/users/robsimmons/followers",
      "following_url": "https://api.github.com/users/robsimmons/following{/other_user}",
      "gists_url": "https://api.github.com/users/robsimmons/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/robsimmons/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/robsimmons/subscriptions",
      "organizations_url": "https://api.github.com/users/robsimmons/orgs",
      "repos_url": "https://api.github.com/users/robsimmons/repos",
      "events_url": "https://api.github.com/users/robsimmons/events{/privacy}",
      "received_events_url": "https://api.github.com/users/robsimmons/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "6469890178986678af97999948b0dd7173554af2",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/6469890178986678af97999948b0dd7173554af2",
        "html_url": "https://github.com/leanprover/lean4/commit/6469890178986678af97999948b0dd7173554af2"
      }
    ]
  },
  {
    "sha": "6469890178986678af97999948b0dd7173554af2",
    "node_id": "C_kwDOB7kabNoAKDY0Njk4OTAxNzg5ODY2NzhhZjk3OTk5OTQ4YjBkZDcxNzM1NTRhZjI",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T14:32:54Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T14:32:54Z"
      },
      "message": "fix: apply ring normalizer to equalities coming from `grind` to core to `lia` (#11613)\n\nThis PR ensures we apply the ring normalizer to equalities being\npropagated from the `grind` core module to `grind lia`. It also ensures\nwe use the safe/managed polynomial functions when normalizing.\n\nCloses #11539",
      "tree": {
        "sha": "f049ec821e58eca84e675c0f16389f2a3fc589d3",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/f049ec821e58eca84e675c0f16389f2a3fc589d3"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/6469890178986678af97999948b0dd7173554af2",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOtYlCRC1aQ7uu5UhlAAA8UgQACj+OFtbWcNNvqY1iCOQMM/p\nlLgBfEndIfuvEq186MyMmq34BjcR6VqvCh2H400kGBLTiIaqEXTFyvw05DqGa2uV\nKqWvAqW4xDGoNCc6MbNNOO1ZLUXq7skgRj7r5pEoRUg+be8bSTulIW9vOtiEy2yM\nuDLkLexs2uB44h5Q65ftMAN9pJuNic17kRstgF61RdB69avbAzqLf37oinxD7NEx\nVwnXg+TQCi6LAEx2k3LK1TnppOvzoQ954xjjgRrNNIr7cs1lSyJuOVSxRIFsMZOF\nXvB6tmstH4L1utmODTTwwaXi9iInZk3Wsiy854rfPOy4awxZLEmGdmRrLh0dZ2pR\nb0PGCLwcPxFkp+Ki2ETjuUAo6xgsy6O3n71yhLUi3cQ4lbILfOnxitw6Qsb6xA2b\nmfLWaJGhfXCE0pgtl1RSsNja9L4xk7PQh0bUKcHu/67WZzP5Vgp/Wd1zVuOz6PU1\nPTA93Ojw5yEy5vablb7liTrKUaMHrPQqmJbLOt6OCYla1+a+fIruTXnfjNUUqaXh\nJyIniD2vNyNWeY/WzmxooVxSMI69JP+1Pr344SdZE9E56qXNrsR+8O3hzFtCh08x\nIkfi5oSrdb+SHdkim1VHvYr1OvKdjPgl+Y2AnQh/e0/R+J1CDpIIvGt+X4ynJdSM\nH9/ESi8y1sE6d7eipDjP\n=Txn4\n-----END PGP SIGNATURE-----\n",
        "payload": "tree f049ec821e58eca84e675c0f16389f2a3fc589d3\nparent 37f9984d7165f2ca61db0479cea8d68e58e4fb24\nauthor Leonardo de Moura <leomoura@amazon.com> 1765463574 +0100\ncommitter GitHub <noreply@github.com> 1765463574 +0000\n\nfix: apply ring normalizer to equalities coming from `grind` to core to `lia` (#11613)\n\nThis PR ensures we apply the ring normalizer to equalities being\npropagated from the `grind` core module to `grind lia`. It also ensures\nwe use the safe/managed polynomial functions when normalizing.\n\nCloses #11539",
        "verified_at": "2025-12-11T14:33:10Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/6469890178986678af97999948b0dd7173554af2",
    "html_url": "https://github.com/leanprover/lean4/commit/6469890178986678af97999948b0dd7173554af2",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/6469890178986678af97999948b0dd7173554af2/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "37f9984d7165f2ca61db0479cea8d68e58e4fb24",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/37f9984d7165f2ca61db0479cea8d68e58e4fb24",
        "html_url": "https://github.com/leanprover/lean4/commit/37f9984d7165f2ca61db0479cea8d68e58e4fb24"
      }
    ]
  },
  {
    "sha": "37f9984d7165f2ca61db0479cea8d68e58e4fb24",
    "node_id": "C_kwDOB7kabNoAKDM3Zjk5ODRkNzE2NWYyY2E2MWRiMDQ3OWNlYThkNjhlNThlNGZiMjQ",
    "commit": {
      "author": {
        "name": "Lean stage0 autoupdater",
        "email": "",
        "date": "2025-12-11T12:37:21Z"
      },
      "committer": {
        "name": "Lean stage0 autoupdater",
        "email": "",
        "date": "2025-12-11T12:37:21Z"
      },
      "message": "chore: update stage0",
      "tree": {
        "sha": "b44306df6eccc6a593e00b8b43246f155d53feaa",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/b44306df6eccc6a593e00b8b43246f155d53feaa"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/37f9984d7165f2ca61db0479cea8d68e58e4fb24",
      "comment_count": 0,
      "verification": {
        "verified": false,
        "reason": "unsigned",
        "signature": null,
        "payload": null,
        "verified_at": null
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/37f9984d7165f2ca61db0479cea8d68e58e4fb24",
    "html_url": "https://github.com/leanprover/lean4/commit/37f9984d7165f2ca61db0479cea8d68e58e4fb24",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/37f9984d7165f2ca61db0479cea8d68e58e4fb24/comments",
    "author": {

    },
    "committer": {

    },
    "parents": [
      {
        "sha": "138476d63588416d7066c6795d74b8e3ced27691",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/138476d63588416d7066c6795d74b8e3ced27691",
        "html_url": "https://github.com/leanprover/lean4/commit/138476d63588416d7066c6795d74b8e3ced27691"
      }
    ]
  },
  {
    "sha": "138476d63588416d7066c6795d74b8e3ced27691",
    "node_id": "C_kwDOB7kabNoAKDEzODQ3NmQ2MzU4ODQxNmQ3MDY2YzY3OTVkNzRiOGUzY2VkMjc2OTE",
    "commit": {
      "author": {
        "name": "Joachim Breitner",
        "email": "mail@joachim-breitner.de",
        "date": "2025-12-11T11:50:37Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T11:50:37Z"
      },
      "message": "fix: noConfusion shape info mistake (#11611)\n\nThis PR fixes a `noConfusion` compilation introduced by #11562.\n\nfixes #11610.",
      "tree": {
        "sha": "2743436d72eb5b259fc5f8d8f9f0e02aaefaaca9",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/2743436d72eb5b259fc5f8d8f9f0e02aaefaaca9"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/138476d63588416d7066c6795d74b8e3ced27691",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOrAcCRC1aQ7uu5UhlAAAM5UQACZ8FTvfWWNsyN5ubUN4EldA\nTSwKRJpGtzxj0P1toHnSHkrZVvzyuotdCb7Jw+q1k85z9v+mNtxSn1LfNKzYBIIE\nfaeZGhvcugsLE9MsBNMSwUfiL2wfawE1w0GiGtDg81xNIaOzf9ftmQmFSL+EW6Op\n9CiMtQwdhiDLYmxqv0h64IDl2MFXyOFlX/bJAdvmSjGYMIeSHUPRAax4waXZGAsI\noRXDbuUg64beBTf2sy14H4x0nYlfHWsdmZPnkbYWWGCZsfIuiyvUXHgFkcsbiQUU\nFrnbInNYeZ83M83bu8RGaHmcWQG4e4T05LF67/yurBxIXSUIbVKMn1n+2+Xku1J9\nCUZ95JHU0kOW+8igiweO5HkDqXbXM9steBBcrFFZJGn5XWunRJshFXyDSdgeI+rA\nQmM/RhET5YMdhq2xLeGIIymVk+DCEh9vEe23vhXqRYaWXSPqYoOmmT+ivFzbPJzS\nsGG5HyUMTz+hHP604Sc7umWZDej7GKfNlfo1IbUn+odRSia4ts9xHkS4z6YMCYJN\nNangK7GF9yYqmopVA1twc/mfVjElrAl5pMWuGBAlUaWLzCuQdJunAZ+YeVTsp6M9\n1zudWsILqBH1Uf7Uw4V0MMdsRAq7imLGvUubxii4OaduifB0spIfkU9JXT66mluV\nXMY9wseUvF30drgPnhjn\n=bNlN\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 2743436d72eb5b259fc5f8d8f9f0e02aaefaaca9\nparent ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1\nauthor Joachim Breitner <mail@joachim-breitner.de> 1765453837 +0100\ncommitter GitHub <noreply@github.com> 1765453837 +0000\n\nfix: noConfusion shape info mistake (#11611)\n\nThis PR fixes a `noConfusion` compilation introduced by #11562.\n\nfixes #11610.",
        "verified_at": "2025-12-11T11:50:53Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/138476d63588416d7066c6795d74b8e3ced27691",
    "html_url": "https://github.com/leanprover/lean4/commit/138476d63588416d7066c6795d74b8e3ced27691",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/138476d63588416d7066c6795d74b8e3ced27691/comments",
    "author": {
      "login": "nomeata",
      "id": 148037,
      "node_id": "MDQ6VXNlcjE0ODAzNw==",
      "avatar_url": "https://avatars.githubusercontent.com/u/148037?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/nomeata",
      "html_url": "https://github.com/nomeata",
      "followers_url": "https://api.github.com/users/nomeata/followers",
      "following_url": "https://api.github.com/users/nomeata/following{/other_user}",
      "gists_url": "https://api.github.com/users/nomeata/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/nomeata/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/nomeata/subscriptions",
      "organizations_url": "https://api.github.com/users/nomeata/orgs",
      "repos_url": "https://api.github.com/users/nomeata/repos",
      "events_url": "https://api.github.com/users/nomeata/events{/privacy}",
      "received_events_url": "https://api.github.com/users/nomeata/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
        "html_url": "https://github.com/leanprover/lean4/commit/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1"
      }
    ]
  },
  {
    "sha": "ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
    "node_id": "C_kwDOB7kabNoAKGVhMTBiZGYxNTQxM2MyNWJkMzYxZGI1MWY5ZjljNWEyN2ZlN2UzZTE",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T10:42:17Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T10:42:17Z"
      },
      "message": "feat: improve case-split heuristic in `grind` (#11609)\n\nThis PR improves the case-split heuristics in `grind`. In this PR, we do\nnot increment the number of case splits in the first case. The idea is\nto leverage non-chronological backtracking: if the first case is solved\nusing a proof that doesn't depend on the case hypothesis, we backtrack\nand close the original goal directly. In this scenario, the case-split\nwas \"free\", it didn't contribute to the proof. By not counting it, we\nallow deeper exploration when case-splits turn out to be irrelevant.\nThe new heuristic addresses the second example in #11545",
      "tree": {
        "sha": "c826af49fa627ea2629dadb3b0a895a796238cda",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/c826af49fa627ea2629dadb3b0a895a796238cda"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOqAYCRC1aQ7uu5UhlAAAniMQAGG6fsouyGJ34mMDcjrag9Uz\nL9kYoh4Y/4EN/31ni0SApxcJx72kp3Y+r05zAf7vixebb+svzG4GNN8RgNFBvqIK\n9W/Tr6Ul2P1YQby1WNCuBOkZb9VZIMFeNx7Y7veoDrl1st/AU5hNvHzqhb48m87G\nxgNVQmYDaYEfxDXhHJO00vIMCT+7NIdwApMc9GxA9mzQ9N2vf0jLkvte/9LGDkKU\nH1D1qnBLysqNtzr9Eu9wCBPkcW1PEH2GR+xAv/5Bpk1VXruAwFg45+SjylI9t7Ke\nYWUWu0AZmPKrxEGCLlFJ1Ir4JfvnGmoZuBpIYaq6GqKHCNiohxhLI8KysT8f7SL1\nC50ZjCDOR7AzhJKFVwd45IIVoKmStxCGJycYQ0oB7e5GcfXRoLVAuKHm8jC5uZrC\nuL3jVVp+avZtC7Fq0hdHZNLLyDaPSwAiY9lvFuK0ccCjMrdHF6Jl7IfkzmiCtZZV\njcmtDIA1KsqcAV0a20vLqpt0cWKSCs2/cfvVqQ4jYukTCfQTxeDvm0Ef1ZUw3gut\nw7IAfsGIOlUnnDeFQM6tua9VOj9pBetI6iMK/WKjQEAJ7u+ZEXX2YtiRUTHuc5J1\ndD47nLHmB5k/dgLZt70IuaNFPR+MLjCd6e3DzSZ/RaR3TC7UWDn+FWaC9DAcpDeB\nzGTwNHK2dy/cnMsbYBwI\n=itsw\n-----END PGP SIGNATURE-----\n",
        "payload": "tree c826af49fa627ea2629dadb3b0a895a796238cda\nparent b8c53b1d290f1c657beca787dfc9a0478d05966e\nauthor Leonardo de Moura <leomoura@amazon.com> 1765449737 +0100\ncommitter GitHub <noreply@github.com> 1765449737 +0000\n\nfeat: improve case-split heuristic in `grind` (#11609)\n\nThis PR improves the case-split heuristics in `grind`. In this PR, we do\nnot increment the number of case splits in the first case. The idea is\nto leverage non-chronological backtracking: if the first case is solved\nusing a proof that doesn't depend on the case hypothesis, we backtrack\nand close the original goal directly. In this scenario, the case-split\nwas \"free\", it didn't contribute to the proof. By not counting it, we\nallow deeper exploration when case-splits turn out to be irrelevant.\nThe new heuristic addresses the second example in #11545",
        "verified_at": "2025-12-11T10:42:33Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
    "html_url": "https://github.com/leanprover/lean4/commit/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/ea10bdf15413c25bd361db51f9f9c5a27fe7e3e1/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "b8c53b1d290f1c657beca787dfc9a0478d05966e",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/b8c53b1d290f1c657beca787dfc9a0478d05966e",
        "html_url": "https://github.com/leanprover/lean4/commit/b8c53b1d290f1c657beca787dfc9a0478d05966e"
      }
    ]
  },
  {
    "sha": "b8c53b1d290f1c657beca787dfc9a0478d05966e",
    "node_id": "C_kwDOB7kabNoAKGI4YzUzYjFkMjkwZjFjNjU3YmVjYTc4N2RmYzlhMDQ3OGQwNTk2NmU",
    "commit": {
      "author": {
        "name": "Henrik Böving",
        "email": "hargonix@gmail.com",
        "date": "2025-12-11T10:39:02Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T10:39:02Z"
      },
      "message": "chore: remove IR elim dead branches (#11576)\n\nThis PR removes the old ElimDeadBranches pass and shifts the new one\npast lambda lifting.\n\nThe reason for dropping the old one is its general unsoundness and the\nfact that we want to do refactorings on the IR part. The reason for\nshifting the current pass past lambda lifting, is that its analysis is\nimprecise in the presence of local function symbols. I experimented with\nthe exact placement for a while and it seems like it is optimal here.\nOverall we observe a slight regression in the amount of C code\ngenerated, likely because we don't propagate information into lambdas\nbefore lifting them anymore. But generally measure a slight performance\nimprovement in general.",
      "tree": {
        "sha": "e37e909d109587540bef7ee99337993edf654ee5",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/e37e909d109587540bef7ee99337993edf654ee5"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/b8c53b1d290f1c657beca787dfc9a0478d05966e",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOp9WCRC1aQ7uu5UhlAAAr5kQAHVRcW8pERzXu+7hi9vIS724\njqJEbZTZzq6Vtmr1xj8MFXO2jlfvw1SGPq9jg7Q+jhvbXfiuErBbKB5nhk5RjC1E\nLibVTd0KZIf/UJFZYEnGyH3McarI2jT2IZuZRcqRETK/pqOa58Ij5I6QNJu2D7Qr\nh4EC6/rDeRQOvyRHlcWd7AMM4XS3BJpOg7tJA5iPD9S3TO6CZevDH7TMBL62m3fA\n6nlm7D7hmTnhH9jWOkY/OtGHoTMkLkw7ViuqcCVhJGMR48F8n/1LRpViVkwktcgp\nhaV2eTRmEuFvxbhZcfucZlVO1hFWrVkPyuFPxPjiaWByYGHED+MjBHQUmBElN1o8\nrJFqmhazN4ClzApepdBjhoA9N9Sbc56VwS3MhNzpv6szWYWrz8Ju09oHUSLrOYUY\ngyavpWTgYWt2RWxiIBSXwF9SO7lFlRUpzouIBt3ABin0kv07tfkh8bvIbHgSeLPS\n39yQK3+ZKJISren9W1J1BFOpb9YEJqIg7VGuWpabDzTqnL9uRGitvS0uMKFN6m56\nlz+rElNq4h+/UAU05o6sFlduloq4Dw22Iu0+yeqhrnKHqFxcs/250mRVvpvAlAbO\n1lEX5LnrSGYRgzRjjgjZJWvP3tAFQ8aHcH73aA4c3F1XlLPPaDUSkUertHwyAowY\nTwSQNtFsIoD0YonBfm0i\n=R3DJ\n-----END PGP SIGNATURE-----\n",
        "payload": "tree e37e909d109587540bef7ee99337993edf654ee5\nparent e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7\nauthor Henrik Böving <hargonix@gmail.com> 1765449542 +0100\ncommitter GitHub <noreply@github.com> 1765449542 +0000\n\nchore: remove IR elim dead branches (#11576)\n\nThis PR removes the old ElimDeadBranches pass and shifts the new one\npast lambda lifting.\n\nThe reason for dropping the old one is its general unsoundness and the\nfact that we want to do refactorings on the IR part. The reason for\nshifting the current pass past lambda lifting, is that its analysis is\nimprecise in the presence of local function symbols. I experimented with\nthe exact placement for a while and it seems like it is optimal here.\nOverall we observe a slight regression in the amount of C code\ngenerated, likely because we don't propagate information into lambdas\nbefore lifting them anymore. But generally measure a slight performance\nimprovement in general.",
        "verified_at": "2025-12-11T10:39:18Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/b8c53b1d290f1c657beca787dfc9a0478d05966e",
    "html_url": "https://github.com/leanprover/lean4/commit/b8c53b1d290f1c657beca787dfc9a0478d05966e",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/b8c53b1d290f1c657beca787dfc9a0478d05966e/comments",
    "author": {
      "login": "hargoniX",
      "id": 33270164,
      "node_id": "MDQ6VXNlcjMzMjcwMTY0",
      "avatar_url": "https://avatars.githubusercontent.com/u/33270164?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/hargoniX",
      "html_url": "https://github.com/hargoniX",
      "followers_url": "https://api.github.com/users/hargoniX/followers",
      "following_url": "https://api.github.com/users/hargoniX/following{/other_user}",
      "gists_url": "https://api.github.com/users/hargoniX/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/hargoniX/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/hargoniX/subscriptions",
      "organizations_url": "https://api.github.com/users/hargoniX/orgs",
      "repos_url": "https://api.github.com/users/hargoniX/repos",
      "events_url": "https://api.github.com/users/hargoniX/events{/privacy}",
      "received_events_url": "https://api.github.com/users/hargoniX/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
        "html_url": "https://github.com/leanprover/lean4/commit/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7"
      }
    ]
  },
  {
    "sha": "e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
    "node_id": "C_kwDOB7kabNoAKGU3ZjRmYzliYWY5MGMzYTY0ZmRiYTdkZjAwY2RiYjcxNWQ4MzkyYjc",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T10:33:48Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T10:33:48Z"
      },
      "message": "fix: theorems without parameters in `grind` E-matching (#11604)\n\nThis PR fixes how theorems without parameters are handled in `grind`.\n\nThis is a better fix than #11579\n\n---------\n\nCo-authored-by: Kim Morrison <kim@tqft.net>",
      "tree": {
        "sha": "b42b03517803b890ae8fd82dc1f7284362455f93",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/b42b03517803b890ae8fd82dc1f7284362455f93"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOp4bCRC1aQ7uu5UhlAAA/O8QAEtX5fq9bVS1+l+VyFcIsSvV\nCOKGx69MPzQqyaitBAqPokUPSSgO8S+zFikTysrH6a2i22E6BmuPQ3olnvD0Of0T\n2oWURoT4k/NEQQ84BApx6oH24aWZrYaCJkSHpx6fgPfcDFSZ6yL0m0f14hYyFS0u\n+ViLfX2YokXUMOTgQyqaJgalYH1DVJHHssJdd92WaTIkbJ6bvQKYKWD1akhi1sUu\nqn4SUtsk72yW7seYJN1/pwceo01xjxrjQGdBGbo7MFcw6XTeZ0zfr6u/P6PHbQ3Z\n2Y5sJVvyjMrhP3GXPbisQqS3RpmUZHHjDvbxFqmos5IeRRIt+YokooyUT31INYno\nC2pmAkOD2cltXhccEMyncKLwiryXSmydmnP7C6bedupmAn29Nx83z8lL0EJRYszh\n7VZ1DxyZaXNaegA99gosDLvTmShpomZBlXL3b35ZHfV63t8iWiAyH/iKRAzUdFVM\n0aASdaJrvHMUVVnnxanvC9XZBZYIp56RieyK0Hf1ihW3+ikVZLQDDo9uOOnwsyh8\nX4AcTBWMtiAHwGRnIv+rOyj7t0mVjEwVoSsXrGrgVOiuA6okNzRs/FJBKnQ5U/x5\nksvQS8CrAqtKu6cNggD3/Og/cjHoo2JXb1+mmtJUvWQcil9H8BrG/iPki6omh/PN\nycsXCi4YCRdoGyqCHCBf\n=Q4KC\n-----END PGP SIGNATURE-----\n",
        "payload": "tree b42b03517803b890ae8fd82dc1f7284362455f93\nparent d145b9f8ee211d5f369c49065d7abd4bc6c9def8\nauthor Leonardo de Moura <leomoura@amazon.com> 1765449228 +0100\ncommitter GitHub <noreply@github.com> 1765449228 +0000\n\nfix: theorems without parameters in `grind` E-matching (#11604)\n\nThis PR fixes how theorems without parameters are handled in `grind`.\n\nThis is a better fix than #11579\n\n---------\n\nCo-authored-by: Kim Morrison <kim@tqft.net>",
        "verified_at": "2025-12-11T10:34:04Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
    "html_url": "https://github.com/leanprover/lean4/commit/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/e7f4fc9baf90c3a64fdba7df00cdbb715d8392b7/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
        "html_url": "https://github.com/leanprover/lean4/commit/d145b9f8ee211d5f369c49065d7abd4bc6c9def8"
      }
    ]
  },
  {
    "sha": "d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
    "node_id": "C_kwDOB7kabNoAKGQxNDViOWY4ZWUyMTFkNWYzNjljNDkwNjVkN2FiZDRiYzZjOWRlZjg",
    "commit": {
      "author": {
        "name": "Mac Malone",
        "email": "tydeu@hatpress.net",
        "date": "2025-12-11T09:28:44Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T09:28:44Z"
      },
      "message": "chore: lake: mv `targets` test to `tests` (#11592)\n\nThis PR moves Lake's `tests/lake/examples/targets` test from `examples`\nto `tests` (and thus disabling it by default).\n\nIt is being\n[flaky](https://github.com/leanprover/lean4/actions/runs/20111185289/attempts/1)\nfor some unknown reason, so I am disabling until I have a better\nopportunity to debug it.",
      "tree": {
        "sha": "9428d1c67f89911fa02d4fcdd24a6a7c5edd5fc6",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/9428d1c67f89911fa02d4fcdd24a6a7c5edd5fc6"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOo7cCRC1aQ7uu5UhlAAADZMQAAtBIvNKnGoG4BgpU5CBMjcx\n5FhI8eRh+lM0n6bj62r8AEnHF6eIDLuGvf1TCkKIV7+ErzLysRMr5PQ3z7igZXLX\n2gxleBx2GyqJWBPXa83BsRdIgANfbxWCCPtrK2ofEOOSjUT32ZcKddET8LgDHqKH\nMhfxCuF74nFyxXSwPm5KmfB43R89mPpyGAmzI7Ac8HTopzuq1l27n+ftWmeltNCm\n0PusJMrk/wBkIIrDUbzmzNV1kasOFGjTc3HroixN36LrPv2tHVEWg4XKex5cptV5\nWs3xhcHUdTiqedBMZc03kOsdZXiaBJ9O+RpmKE/s99+wNXQJ9dpeAVYe7n4R25+1\nAudXQXq9URqLnH9fbN169WaVEaEq+X0816P+5f23JYIOnltxzYBe//34iqOH1rAE\ntf5sPj4GcSP70tpzOTkZO5EDCSTxKz1et/eZg6/lhnmjFeayqRCqc6HTID0H0NTH\nwZfXjT6XuOC2K1VRxEAy6JfDhQi3GF3RHRlmipOH2zfqFdhtQJZbCP1mbNMpIp/E\nJfS1KN5o88fJpwfdNGzhEY4cCJG1KeKbwRrT7DLs9Wiysi2IpW/r5CJbkf01KdMC\n1oZVPeT18XnVJlKKuxQQq+oWQHTpoI401ssG8MMoax9bUwQsMZOcUqfmB7Z7lqkN\nWIEmWpgy6NnI4u5pjS/6\n=FVit\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 9428d1c67f89911fa02d4fcdd24a6a7c5edd5fc6\nparent 05a81248dfe0ddf2b258c066156d909d9668e222\nauthor Mac Malone <tydeu@hatpress.net> 1765445324 -0500\ncommitter GitHub <noreply@github.com> 1765445324 +0000\n\nchore: lake: mv `targets` test to `tests` (#11592)\n\nThis PR moves Lake's `tests/lake/examples/targets` test from `examples`\nto `tests` (and thus disabling it by default).\n\nIt is being\n[flaky](https://github.com/leanprover/lean4/actions/runs/20111185289/attempts/1)\nfor some unknown reason, so I am disabling until I have a better\nopportunity to debug it.",
        "verified_at": "2025-12-11T09:29:00Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
    "html_url": "https://github.com/leanprover/lean4/commit/d145b9f8ee211d5f369c49065d7abd4bc6c9def8",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/d145b9f8ee211d5f369c49065d7abd4bc6c9def8/comments",
    "author": {
      "login": "tydeu",
      "id": 9020483,
      "node_id": "MDQ6VXNlcjkwMjA0ODM=",
      "avatar_url": "https://avatars.githubusercontent.com/u/9020483?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/tydeu",
      "html_url": "https://github.com/tydeu",
      "followers_url": "https://api.github.com/users/tydeu/followers",
      "following_url": "https://api.github.com/users/tydeu/following{/other_user}",
      "gists_url": "https://api.github.com/users/tydeu/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/tydeu/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/tydeu/subscriptions",
      "organizations_url": "https://api.github.com/users/tydeu/orgs",
      "repos_url": "https://api.github.com/users/tydeu/repos",
      "events_url": "https://api.github.com/users/tydeu/events{/privacy}",
      "received_events_url": "https://api.github.com/users/tydeu/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "05a81248dfe0ddf2b258c066156d909d9668e222",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/05a81248dfe0ddf2b258c066156d909d9668e222",
        "html_url": "https://github.com/leanprover/lean4/commit/05a81248dfe0ddf2b258c066156d909d9668e222"
      }
    ]
  },
  {
    "sha": "05a81248dfe0ddf2b258c066156d909d9668e222",
    "node_id": "C_kwDOB7kabNoAKDA1YTgxMjQ4ZGZlMGRkZjJiMjU4YzA2NjE1NmQ5MDlkOTY2OGUyMjI",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T08:44:47Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T08:44:47Z"
      },
      "message": "fix: power internalization in `grind linarith` (#11605)\n\nThis PR fixes a bug in the internalizer of `a^p` terms in `grind\nlinarith`.\n\nCloses #11597",
      "tree": {
        "sha": "fea7335b10c2ef33dc895c3fb46fa491318d1512",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/fea7335b10c2ef33dc895c3fb46fa491318d1512"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/05a81248dfe0ddf2b258c066156d909d9668e222",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOoSOCRC1aQ7uu5UhlAAAAv4QAHg3embSrPGWNMRC7wA73gx+\nZoulXiDerpExZvJ+O8ZfEYGQrEAlqVdGS1p6asz3IiMZg2XK3TEWloJJsCSva3rU\nxcAk0nioYstN6aBVIL04gevohtMC0KL+VMvuC9Hy+nHdp0blzJ3TJpfDUXdteW13\nBijogd+VnYEtl/RKmbvPBj9POWOXfnG3YDNnonTp+q7bz98iZ4nRsBstejWIOCj4\nYv2/7CkIypjtukQY6XjSeWBbh78KesBMQC/ECw/GDHl86Fo8oV5HvUZKPZB50pH7\nEAgYEOeQvZ2+9iN8hE/UnWoIso2XsNDFhsYhKxr0g0ZrQhAA3vQk0t95nleml+YD\n8DVhy5UUrxeKKYjtDBbT7TbfIhsPjuYrco1luZTdurfheuZMbkOmDs9JrJH/nmyn\nQoc9Y770VqxgC1LUqjQOqGy6As+7h96K2njgcjkCG3RIDiVv6NqkU+/LH9G0D4JB\noObA4ouDzgvSKOT72L9I/NmC1B+lZ+guuwMRLBYdRN+W+Wqb68P9v+9f3thOG2lO\nuuTGl29/FCwdgPeB7T+NYsPmjPkeEDrz5ugz2bYoSea5uvhPas0T2WQkxUNHU85G\ngP5CGO2+pbAYgkpnNaCJ8evd/phAp58ajPrZV9ttfvliy5c3C56+vH8DNaaqIpfE\nuGrVYlU9EumxDjuveQbE\n=r6os\n-----END PGP SIGNATURE-----\n",
        "payload": "tree fea7335b10c2ef33dc895c3fb46fa491318d1512\nparent 9928cf3d64a5df1349c38ad173a479d41d113e92\nauthor Leonardo de Moura <leomoura@amazon.com> 1765442687 +0100\ncommitter GitHub <noreply@github.com> 1765442687 +0000\n\nfix: power internalization in `grind linarith` (#11605)\n\nThis PR fixes a bug in the internalizer of `a^p` terms in `grind\nlinarith`.\n\nCloses #11597",
        "verified_at": "2025-12-11T08:45:03Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/05a81248dfe0ddf2b258c066156d909d9668e222",
    "html_url": "https://github.com/leanprover/lean4/commit/05a81248dfe0ddf2b258c066156d909d9668e222",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/05a81248dfe0ddf2b258c066156d909d9668e222/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "9928cf3d64a5df1349c38ad173a479d41d113e92",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/9928cf3d64a5df1349c38ad173a479d41d113e92",
        "html_url": "https://github.com/leanprover/lean4/commit/9928cf3d64a5df1349c38ad173a479d41d113e92"
      }
    ]
  },
  {
    "sha": "9928cf3d64a5df1349c38ad173a479d41d113e92",
    "node_id": "C_kwDOB7kabNoAKDk5MjhjZjNkNjRhNWRmMTM0OWMzOGFkMTczYTQ3OWQ0MWQxMTNlOTI",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T08:17:40Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T08:17:40Z"
      },
      "message": "chore: revert fix: ground theorems as `grind` parameters\" (#11603)\n\nThis PR reverts leanprover/lean4#11579",
      "tree": {
        "sha": "7624d649b3241c727bad2a59dda04cb27adca677",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/7624d649b3241c727bad2a59dda04cb27adca677"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/9928cf3d64a5df1349c38ad173a479d41d113e92",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOn40CRC1aQ7uu5UhlAAAXYEQAKScLZ1R+SVTfIGz9c53uiAc\nW349WIR0BPLLZlf1ezRPQD2KKAnja1B6L+OJVMDSLt1SYh3u4QAI85P848D3SB/E\nPoDPegIFRLWQd8C/c/qHQvag9b+J2zkUYbEUDP8DU8tFRd65lahXGsNro7wLN3m/\noevXIMY7mfVC7BNmG4vD3N+v3HwaKvO9qqJANrz5tqLRTnbVLWWRRgVvYmFg+Nki\n+TGzxjernpN4zFPvjBvdkM2FB+0xvjqivNWkFpbV/n/BrOcJW6Z0e3zH0z7SirVJ\nnvth/wm1rPrK0hrRQbsJC1+B4pNBZdXQRO7p5FLdyvtTBnn1VyhkCKD1w/5r6ykg\nrfzEuGpWW/CGxZE3A191omX4IeGG/cBIymFnV4Z8DJbdybrinNPSzAIgF6c9HRvJ\nuW+XLaZtzCEI2544AsyrA9BKb9UIh0em0YkMwWhqOY0pr+iKjk4E7HmQI3DEizGc\nrkbJVvKSNR4bPUlAgbmFnoOY1nsD+EG6Wfg+JJADCuz6SNwPLsHM/B2nBb+vqHSg\nMwF3lC2NhI6FZL3Hj37pfnC30bvPk87allEX3TMJWpnj+rwHNQKbxtSUR6+QwDXv\nPNQuvSArh3tzeLj9/UfSZaS+ybiFTdAqZcCaNnss8R04BII1LiU88pVokInt4s8t\nywYEg+hqKcItWJyPR09C\n=SdV1\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 7624d649b3241c727bad2a59dda04cb27adca677\nparent aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389\nauthor Leonardo de Moura <leomoura@amazon.com> 1765441060 +0100\ncommitter GitHub <noreply@github.com> 1765441060 +0000\n\nchore: revert fix: ground theorems as `grind` parameters\" (#11603)\n\nThis PR reverts leanprover/lean4#11579",
        "verified_at": "2025-12-11T08:17:57Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/9928cf3d64a5df1349c38ad173a479d41d113e92",
    "html_url": "https://github.com/leanprover/lean4/commit/9928cf3d64a5df1349c38ad173a479d41d113e92",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/9928cf3d64a5df1349c38ad173a479d41d113e92/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
        "html_url": "https://github.com/leanprover/lean4/commit/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389"
      }
    ]
  },
  {
    "sha": "aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
    "node_id": "C_kwDOB7kabNoAKGFhNGFmZjI4MGI5ZDFmNmMxZDgyZjJiMzY2MWQ2ZTQ5ZTlmNWYzODk",
    "commit": {
      "author": {
        "name": "Leonardo de Moura",
        "email": "leomoura@amazon.com",
        "date": "2025-12-11T07:43:21Z"
      },
      "committer": {
        "name": "GitHub",
        "email": "noreply@github.com",
        "date": "2025-12-11T07:43:21Z"
      },
      "message": "fix: ground theorems as `grind` parameters (#11579)\n\nThis PR ensures that ground theorems are properly handled as `grind`\nparameters. Additionally, `grind [(thm)]` and `grind [thm]` should be\nhandled the same way.\n\n---------\n\nCo-authored-by: Kim Morrison <kim@tqft.net>",
      "tree": {
        "sha": "12c713d3b6a5a327dc81982fad3b0e15e117061b",
        "url": "https://api.github.com/repos/leanprover/lean4/git/trees/12c713d3b6a5a327dc81982fad3b0e15e117061b"
      },
      "url": "https://api.github.com/repos/leanprover/lean4/git/commits/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
      "comment_count": 0,
      "verification": {
        "verified": true,
        "reason": "valid",
        "signature": "-----BEGIN PGP SIGNATURE-----\n\nwsFcBAABCAAQBQJpOnYpCRC1aQ7uu5UhlAAAADkQAHrai8UHUY0HKOgJFiOpmgob\nLiwbXu2iUsHWpRcRHYWOhSmTnrh9JJkp3ca2XW6Wikp3tsgpfUyySNl2LVVCy56h\nQrqa3zTZa7KqoL/IphcgdjboFx4Yv7cStHWP+P+EBawMrxepl0i/wIDFmI5a1VW2\n/HLl7X64ytNNFoXUscnLuCw/auj6aSloCQNNfe8v0mXJKnYlGYvWObAFGI1AQuXP\n8oWturr2Y/+8zwnDoXwfaCirXO10JZksP4DrteTg8EJrz2TmNt46rLfhvYyKNMTK\nQtc6c/Cuqw7ChLGiJCAR0t4luvB7T4K6VCxyozeBbRoag9+FwKstb7GZUxJt/NEx\nVAj4Q4ou3RwKWiT3HOwiPnjV0nZx+XDdyrU+0yd8eyFKAKQz5LtvlVf0N6UQlW2k\nyPdena1sPWsSJe0Tkxzj94W6gonDP4mwtKfOUO7X1+rRbLQzvCgyaoJK4HE0n49o\nBTwUSOl2kxTTkzTEsAKivfVUo124b5nbTry5s84VM5oWCuuVdI/+WvxmZGb/U9zt\nwQHGC0I5Jg3/dH8QMws8X+HFKCtiDndKmD3yCizZ+sbmC+9KvbZuSyXXbGYMQGHr\nT+zbEFH4t7ndV4h3JLOZFJInNVlmNMs7Y+XZ7J8ePpfr7aPTaogboNGJnkRoykDM\nJQBLXLRf398KmSqeo8sC\n=l3vb\n-----END PGP SIGNATURE-----\n",
        "payload": "tree 12c713d3b6a5a327dc81982fad3b0e15e117061b\nparent eee58f4506d28a14c9a171165f999445a0663d93\nauthor Leonardo de Moura <leomoura@amazon.com> 1765439001 +0100\ncommitter GitHub <noreply@github.com> 1765439001 +0000\n\nfix: ground theorems as `grind` parameters (#11579)\n\nThis PR ensures that ground theorems are properly handled as `grind`\nparameters. Additionally, `grind [(thm)]` and `grind [thm]` should be\nhandled the same way.\n\n---------\n\nCo-authored-by: Kim Morrison <kim@tqft.net>",
        "verified_at": "2025-12-11T07:43:38Z"
      }
    },
    "url": "https://api.github.com/repos/leanprover/lean4/commits/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
    "html_url": "https://github.com/leanprover/lean4/commit/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389",
    "comments_url": "https://api.github.com/repos/leanprover/lean4/commits/aa4aff280b9d1f6c1d82f2b3661d6e49e9f5f389/comments",
    "author": {
      "login": "leodemoura",
      "id": 2778936,
      "node_id": "MDQ6VXNlcjI3Nzg5MzY=",
      "avatar_url": "https://avatars.githubusercontent.com/u/2778936?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/leodemoura",
      "html_url": "https://github.com/leodemoura",
      "followers_url": "https://api.github.com/users/leodemoura/followers",
      "following_url": "https://api.github.com/users/leodemoura/following{/other_user}",
      "gists_url": "https://api.github.com/users/leodemoura/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/leodemoura/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/leodemoura/subscriptions",
      "organizations_url": "https://api.github.com/users/leodemoura/orgs",
      "repos_url": "https://api.github.com/users/leodemoura/repos",
      "events_url": "https://api.github.com/users/leodemoura/events{/privacy}",
      "received_events_url": "https://api.github.com/users/leodemoura/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },
    "parents": [
      {
        "sha": "eee58f4506d28a14c9a171165f999445a0663d93",
        "url": "https://api.github.com/repos/leanprover/lean4/commits/eee58f4506d28a14c9a171165f999445a0663d93",
        "html_url": "https://github.com/leanprover/lean4/commit/eee58f4506d28a14c9a171165f999445a0663d93"
      }
    ]
  }
]

As you can see there are two shapes of committers here:

    "committer": {
      "login": "web-flow",
      "id": 19864447,
      "node_id": "MDQ6VXNlcjE5ODY0NDQ3",
      "avatar_url": "https://avatars.githubusercontent.com/u/19864447?v=4",
      "gravatar_id": "",
      "url": "https://api.github.com/users/web-flow",
      "html_url": "https://github.com/web-flow",
      "followers_url": "https://api.github.com/users/web-flow/followers",
      "following_url": "https://api.github.com/users/web-flow/following{/other_user}",
      "gists_url": "https://api.github.com/users/web-flow/gists{/gist_id}",
      "starred_url": "https://api.github.com/users/web-flow/starred{/owner}{/repo}",
      "subscriptions_url": "https://api.github.com/users/web-flow/subscriptions",
      "organizations_url": "https://api.github.com/users/web-flow/orgs",
      "repos_url": "https://api.github.com/users/web-flow/repos",
      "events_url": "https://api.github.com/users/web-flow/events{/privacy}",
      "received_events_url": "https://api.github.com/users/web-flow/received_events",
      "type": "User",
      "user_view_type": "public",
      "site_admin": false
    },

and

    "committer": {

    },

[NorfairKing]

The same goes for author, it seems:

    "author": {

    },