)]}'
{
  "commit": "7b4b40f7fc78d34dd4d0810375b07d4e2d1964e0",
  "tree": "747c2aea563c5aca1459e34a901214e3fb34f4c3",
  "parents": [
    "aee6d42280defdf84888844e1ac16f3fc804ee7c"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 25 16:56:04 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Sun Sep 27 19:56:45 2026 +0000"
  },
  "message": "feat: make declaration-keyed extension entries write-once\n\nThis PR makes entries of declaration-keyed environment extensions write-once: writing a second entry for a declaration panics, and giving a declaration a second docstring through `add_decl_doc` is an error. A failed redeclaration also no longer replaces the declaration ranges of the existing declaration, which misdirected go-to-definition. Apart from catching accidental overwrites, this is a necessary prerequisite for validating type class resolution cache entries against declaration-keyed registries, such as equation theorems, without recording every read of them.\n\n`MapDeclarationExtension.insert` takes an `allowOverwrite` flag for deliberate replacements; no caller in core needs it. Its guard only serves to catch bugs, as the type class resolution cache will record writes through `insert`; the registries below are not recorded, so there the cache will rely on the guard. `addDeclarationRanges` keeps the first ranges reported for a declaration, and docstrings otherwise still replace an existing one, as metaprograms such as cross-reference attributes write them before a declaration\u0027s own docstring is added. The declaration-keyed registries kept in other extensions (structures, equation theorems, match equations, sparse `casesOn` declarations, definition height overrides) get the same guard, allowing idempotent re-registration; `setStructureParents` remains the one sanctioned update of a structure\u0027s entry. A rejected write keeps the existing entries, and the checks only consult the state visible on the current environment branch, so that a write never waits for the branch elaborating the declaration.\n\nThe guard caught docstrings in the standard library that were silently replaced: `add_decl_doc IterM.mk` after `structure Iter` meant `Iter.mk`, and `WellFounded.extrinsicFix`, its variants, `IterM.Total` and `Iter.Total` had placeholder docstrings, kept only to satisfy the missing-docs linter, that a later `add_decl_doc` referring to subsequent declarations replaced. These now opt out of the linter instead.\n\nCo-Authored-By: Claude Opus 5.5 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "05521f805790bb59704d688656b253aa6a86958d",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Iterators/Basic.lean",
      "new_id": "adb83749e09a455a6943a6bd753683903ff9f30f",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Iterators/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "bf43a94998a9fffad6f520ddd4ae13094d9f2c08",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Iterators/Consumers/Monadic/Total.lean",
      "new_id": "dd6b0061145ea48dec8d5bd0b0505802892ca6c8",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Iterators/Consumers/Monadic/Total.lean"
    },
    {
      "type": "modify",
      "old_id": "b3fd8e79c702b27be9d2649eeb55652cdc5b4b33",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Iterators/Consumers/Total.lean",
      "new_id": "73900bdb352964de108320c705fa4c9957c06805",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Iterators/Consumers/Total.lean"
    },
    {
      "type": "modify",
      "old_id": "dbacec595b1b5b985f9e99533d50151ee909a5f0",
      "old_mode": 33188,
      "old_path": "src/Init/WFExtrinsicFix.lean",
      "new_id": "17fc23683f5926e7bda3317c0a9a6704df55ead3",
      "new_mode": 33188,
      "new_path": "src/Init/WFExtrinsicFix.lean"
    },
    {
      "type": "modify",
      "old_id": "406579133874f8a772d61588fde4fda6c6ee33a2",
      "old_mode": 33188,
      "old_path": "src/Lean/DeclarationRange.lean",
      "new_id": "a67d3fb57b7243a12d90391fdca05d82ebf6a12c",
      "new_mode": 33188,
      "new_path": "src/Lean/DeclarationRange.lean"
    },
    {
      "type": "modify",
      "old_id": "3339bbe4dbe92b442fffaf5ba53eeef093331b69",
      "old_mode": 33188,
      "old_path": "src/Lean/DocString/Add.lean",
      "new_id": "79b563a8bd805c73d0be264ddba8d9c52442fe5e",
      "new_mode": 33188,
      "new_path": "src/Lean/DocString/Add.lean"
    },
    {
      "type": "modify",
      "old_id": "1faac25cc346fdf1ca13cfec3ddebe54826c4dec",
      "old_mode": 33188,
      "old_path": "src/Lean/DocString/Extension.lean",
      "new_id": "00c310a9849e94d4817e3d25e18b27a316836309",
      "new_mode": 33188,
      "new_path": "src/Lean/DocString/Extension.lean"
    },
    {
      "type": "modify",
      "old_id": "bd4ad9834f0c5be428c5d76506ca2235d47c4acc",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/BuiltinCommand.lean",
      "new_id": "10c837b15c4e46a0fb76b11b1563375893fcfb6c",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/BuiltinCommand.lean"
    },
    {
      "type": "modify",
      "old_id": "2be29e634ba290d10000319c1894ecf05daed264",
      "old_mode": 33188,
      "old_path": "src/Lean/EnvExtension.lean",
      "new_id": "1241457ead6a5e2118c73739aa37283917e140ee",
      "new_mode": 33188,
      "new_path": "src/Lean/EnvExtension.lean"
    },
    {
      "type": "modify",
      "old_id": "29dded6e147ce1b8b630061cafd3efea19df7d86",
      "old_mode": 33188,
      "old_path": "src/Lean/Environment.lean",
      "new_id": "6438dfe851d5814c2e95eb938d2944c2173cde41",
      "new_mode": 33188,
      "new_path": "src/Lean/Environment.lean"
    },
    {
      "type": "modify",
      "old_id": "f184572b0c27527135c75c4f34d47a021b7e8c5d",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Constructions/SparseCasesOn.lean",
      "new_id": "27de22b24abeef4de65c4e18bea4718a3bf48e12",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Constructions/SparseCasesOn.lean"
    },
    {
      "type": "modify",
      "old_id": "c20d482ac3768a3b66110cc5b0078a36dbc4bff2",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Eqns.lean",
      "new_id": "2de3978afa2bd1165e67cdf7db807219bfdb40bd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Eqns.lean"
    },
    {
      "type": "modify",
      "old_id": "07d1f07a1611212d0e1a73016b6f50797eb0c1c6",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/MatchEqsExt.lean",
      "new_id": "f89cf8740a7edee193c91ad1305493e1cad1a289",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/MatchEqsExt.lean"
    },
    {
      "type": "modify",
      "old_id": "77e580c4e57be3c5a26bc3411947584e07cb1098",
      "old_mode": 33188,
      "old_path": "src/Lean/Structure.lean",
      "new_id": "2327bf3a1ed4636e5ec94934bfc2cd808218534a",
      "new_mode": 33188,
      "new_path": "src/Lean/Structure.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "92acecb8d4221f28bd68153a27f10d0c4f423693",
      "new_mode": 33188,
      "new_path": "tests/elab/docStringTwice.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "75902b098a1632242b60cc55182328487577fce9",
      "new_mode": 33188,
      "new_path": "tests/elab/mapDeclExtWriteOnce.lean"
    }
  ]
}