feat: "sine qua non" premise selection

[kim-em]

This PR implements the "Sine Qua Non" premise selection algorithm, as used by e.g. Vampire. It needs further tuning/tweaking, which I'll get to once the premise selection benchmark is available. Note this uses an environment extension which prepares the necessary index for every file, and I remain concerned that this could be expensive.

[nomeata]

Note this uses an environment extension which prepares the necessary index for every file, and I remain concerned that this could be expensive.

This requirement sounds similar to what loogle needs for efficient local usage. Maybe some general infrastructure for efficiently indexing lean module can emerge - for example we only expect interactive use to use these indices, do we? So maybe a separate lake facet is the right direction?

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1e86f81.
There were significant changes against commit 19533ab:

  Benchmark     Metric                     Change
  =========================================================
- Init size     bytes .olean                 2.3%
+ stdlib        grind canon                 -4.3% (-27.2 σ)
- stdlib        number of imported bytes     1.6%
- stdlib size   bytes .olean                 1.0%

[leanprover-radar]

Benchmark results for d8d3a82 against 1981c62 are in! @kim-em

Minor changes (2)

• stdlib//instructions changed by -0.1% (✅).
• workspaceSymbols with new ranges//instructions changed by +0.7% (🟥).

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-29 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-10-29 23:19:58)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e2f5938e74276a12dbfe235b280e3ff38e4533c2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-30 07:02:33)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-11002 built against this PR, but testing failed. (2025-10-30 00:22:57) View Log
• ✅ Mathlib branch lean-pr-testing-11002 has successfully built against this PR. (2025-10-30 01:58:26) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2f5938e74276a12dbfe235b280e3ff38e4533c2 --onto 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-30 07:02:32)
• ✅ Mathlib branch lean-pr-testing-11002 has successfully built against this PR. (2025-10-31 02:53:55) View Log

[kim-em]

The Mathlib build has been benchmarked at https://speed.lean-lang.org/mathlib4/compare/72db3d3f-fbdf-432f-b858-f0c07dad7bd7/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=ea5bbdd2d4743ff825b820efcd88f133609bbf6a

It's fairly favourable: there is increased quite a bit more time spent in olean serialization, but not appreciable change in wall-clock time. 0.5% increase in olean sizes.

Those seem acceptable to me, so I'm going to merge this soon.