feat: unknown identifier code action and the module system

[Kha]

This PR ensures that the code action provided on unknown identifiers correctly inserts public and/or meta in modules

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-13 17:49:50)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f7ed15800246e6532d0fd01c5856f59a9bf9679f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-20 17:48:41)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11164 has successfully built against this PR. (2025-11-13 19:11:02) View Log
• ✅ Mathlib branch lean-pr-testing-11164 has successfully built against this PR. (2025-11-19 18:07:03) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f7ed15800246e6532d0fd01c5856f59a9bf9679f --onto a106ea053fec080a50204b0ad6dadc69bc3f0937. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 17:48:40)

[Kha]

!bench

[leanprover-radar]

Benchmark results for 2074dca against d464b13 are in! @Kha

Major changes (12)

• Init.Data.BitVec.Lemmas//instructions changed by +58.3% (🟥).
• Init.Data.List.Sublist async//instructions changed by +87.3% (🟥).
• Init.Prelude async//instructions changed by +535.3% (🟥).
• Std.Data.DHashMap.Internal.RawLemmas//instructions changed by +69.0% (🟥).
• Std.Data.Internal.List.Associative//instructions changed by +400.1% (🟥).
• big_beq//instructions changed by +1.1% (🟥).
• grind_bitvec2.lean//instructions changed by +25.5% (🟥).
• grind_list2.lean//instructions changed by +19.1% (🟥).
• identifier auto-completion//instructions changed by +1.9% (🟥).
• mut_rec_wf//instructions changed by +8.5% (🟥).
• riscv-ast.lean//instructions changed by +152.8% (🟥).
• stdlib//instructions changed by +60.9% (🟥).

Minor changes (2)

• big_beq_rec//instructions changed by +0.6% (🟥).
• iterators (elab)//instructions changed by +0.8% (🟥).

[Kha]

!bench

[leanprover-radar]

Benchmark results for 30dc746 against d464b13 are in! @Kha

Major changes (1)

• identifier auto-completion//instructions changed by -5.1% (✅).

[mhuisi]

!radar

[leanprover-radar]

Benchmark results for e8b0217 against d464b13 are in! @mhuisi

Major changes (2)

• identifier auto-completion//instructions changed by +2.2% (🟥).
• stdlib//instructions changed by +7.5% (🟥).

Minor changes (1)

• Init.Prelude async//instructions changed by +0.5% (🟥).

[Kha]

!bench

[leanprover-radar]

Benchmark results for 656587e against fc6e045 are in! @Kha

Runs (2)

• other exited with code 2 (🟥)
• stdlib exited with code 2 (🟥)

[Kha]

!bench

[leanprover-radar]

Benchmark results for abdbc4c against f7ed158 are in! @Kha

Major changes (2)

• identifier auto-completion//instructions changed by +2.2% (🟥).
• size/stdlib/.ilean//bytes changed by +8.9% (🟥).

Minor changes (2)

• Init.Prelude async//instructions changed by +0.5% (🟥).
• stdlib//instructions changed by +0.2% (🟥).

[mhuisi]

Did this test case change intentionally?

[Kha]

reverted

[mhuisi]

Does this logic need to be adjusted here, depending on the modifiers?

[Kha]

We could upgrade an existing import to public instead of inserting it but at that point we're encroaching a bit upon Shake territory