feat: support code actions in linters

[wkrozowski]

This PR adds the support for code actions to linters. When Elab.async is enabled, before a linter task is dispatched, we create a promise for the info tree node. Then, we accumulate newly added info trees through the linter execution and we resolve the promise inside of the linter task. Finally, on the main task, we modify the info tree (wrapped in command context) and add a new leaf, with an mvar id, that will eventually be filled with a promise value.

This PR also supports code actions in stateful linters (#14357), but does not offer such support for module linters, that fire at terminal commands and code actions from there do not surface to the info view.

Related to RFC #4363.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-15 19:04:08)
• ✅ Mathlib branch lean-pr-testing-14402 has successfully built against this PR. (2026-07-16 16:13:06) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9a61e83457592524905308f1fb63b4a5ebdcebd1 --onto 25ba8c3d3bcb1dded7ff5a6f3b6044b0a7970198. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-20 12:09:18)

[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 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-15 19:04:10)
• ✅ Reference manual branch lean-pr-testing-14402 has successfully built against this PR. (2026-07-16 15:19:12) View Log
• 🟡 Reference manual branch lean-pr-testing-14402 build against this PR didn't complete normally. (2026-07-16 15:19:20) View Log
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9a61e83457592524905308f1fb63b4a5ebdcebd1 --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-20 12:09:19)

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 3543a67 against 46cf2b9 are in. There are significant results. @wkrozowski

• 🟥 build//instructions: +10.0G (+0.09%)

Large changes (1✅)

• ✅ build/profile/interpretation//wall-clock: -2s (-2.44%)

Small changes (1✅, 8🟥)

• 🟥 build/lakeprof/longest rebuild path//instructions: +7.1G (+1.16%)
• 🟥 build/module/Lean.Elab.Command//instructions: +6.9G (+45.02%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Elab.InfoTree.Basic//instructions: +61.2M (+3.26%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.ModelUtil//instructions: +59.5M (+2.53%)
• 🟥 build/profile/linting//wall-clock: +1s (+5.17%)
• 🟥 compiled/rbmap_fbip//task-clock: +31ms (+9.47%)
• 🟥 compiled/rbmap_fbip//wall-clock: +31ms (+9.46%)
• 🟥 elab/big_beq//maxrss: +11MiB (+0.59%)
• ✅ elab/big_do//instructions: -22.4M (-0.12%)