)]}'
{
  "commit": "156f68f2b849a6324014fa1ff6833fde77b267b4",
  "tree": "13345ae1ec7e00b1f46dce71bc528c76f4b2c4c8",
  "parents": [
    "ecdcc6289d39c798bf33651abaab59e5f80a4426"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Oct 15 12:43:54 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Wed Oct 21 12:02:21 2026 +0000"
  },
  "message": "perf: build the `FileMap` of a parser input only once\n\nThis PR makes `Lean.Parser.mkInputContext` compute the `FileMap` of its input only once, after normalizing line endings. Its `endPos` and `endPos_valid` parameters, which required computing the `FileMap` of the original input as well, are removed; callers that parse a part of a file with an existing `FileMap` should use `InputContext.mk` with that `FileMap` instead.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "310b1cc781cda1fc41dea76a7bde8c1396d8e4d3",
      "old_mode": 33188,
      "old_path": "src/Lean/Parser/Extension.lean",
      "new_id": "a032718eb0327b5457104baee088d8b57a93b398",
      "new_mode": 33188,
      "new_path": "src/Lean/Parser/Extension.lean"
    },
    {
      "type": "modify",
      "old_id": "55d0df922b978b1c25b8a033dfdc53c783f374ac",
      "old_mode": 33188,
      "old_path": "tests/elab/parseEnd.lean",
      "new_id": "d615b41115574aef1b2a98ad35923b14491b3421",
      "new_mode": 33188,
      "new_path": "tests/elab/parseEnd.lean"
    }
  ]
}