refactor: eliminate FileIdent.mod

[mhuisi]

No description provided.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b09e33f76b4cff04f8e9b21a1f6b75f15926553b --onto 9063adbd51334f68608bad14cd298e6315e718d4. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-21 18:40:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b09e33f76b4cff04f8e9b21a1f6b75f15926553b --onto e9a1c9ef63d8e53803c16077f03e2dacd4a890bd. You can force reference manual CI using the force-manual-ci label. (2026-01-21 18:40:15)

[mhuisi]

!bench

[leanprover-radar]

Benchmark results for 538d689 against b09e33f are in! @mhuisi

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• ✅ build//instructions: -2.2G (-0.0%)

Large changes (1✅)

• ✅ identifier auto-completion//instructions: -9.2G (-11.2%)

Small changes (4✅)

• ✅ build/module/Lean.Server.FileSource//bytes .olean: -37kiB (-26.9%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Server.FileSource//bytes .olean.private: -9kiB (-12.1%)
• ✅ build/module/Lean.Server.FileSource//instructions: -99.5M (-7.9%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Server.Watchdog//instructions: -576.4M (-2.4%) (reduced significance based on *//lines)