Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-10-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-10-07 13:46:26)
• ✅ Mathlib branch lean-pr-testing-5631 has successfully built against this PR. (2024-10-07 23:06:29) View Log

Interesting. We just run into this issue in https://github.com/opencompl/lean-mlir/pull/673/files. In particular, we use native_decide which fails and then run in a kernel error. For some reason try native_decide does not fail, but succeeds and we get an error only on the function overall. This PR is not fixing this, but maybe adds a data-point that there are also automated uses of native_decide that fail and where we trigger the same kernel errors.

The same issue crops up at #5574, where checking the proof to throw an error message when bv_check fails to check the LRAT proof effectively doubles the execution time. So we decided to not go ahead with the approach, but it's a shame, since the error message that results from using an older LRAT proof with a newer bv_check is a little inscrutable.

In an ideal world, there would be some sort of API that can request the kernel to check a proof from Meta code, and returns either a "checked proof handle", or an error, which can then be handled at meta-time.

It seems complex to implement such a feature, though, as the kernel would then need to maintain such "checked proof handles", which is bad for TCB.

It seems complex to implement such a feature, though, as the kernel would then need to maintain such "checked proof handles", which is bad for TCB.

This function already mostly exists, it's called a theorem!

IIRC, a tactic can add new theorems to the environment, so we can have decide or bv_decide generate the proof term. Then, it adds that proof to the environment as a theorem, to get the kernel to check it. If type-checking fails (I assume we can catch that?) we can throw a meaningfull errro in the tactic. Otherwise, if type-checking succeeds, we can emit the new theorem in our original proof, so that we don't have to recheck the proof

That's clever! This would allow us to half the processing time of decide everywhere - at the expense of lots of theorems proving 0 < 1 over and over again.

Maybe this can hook into the ”abstract proofs” machinery used elsewhere.

We could think of some threshold heuristic, I can imagine that for small statements like 0 < 1 the overhead of adding a new theorem to the kernel could be more than just running the meta checker like we do currently.

Maybe this can hook into the ”abstract proofs” machinery used elsewhere.

I'm not sure I know what you're referring to here, what is this abstract proofs machinery?

We could think of some threshold heuristic, I can imagine that for small statements like 0 < 1 the overhead of adding a new theorem to the kernel could be more than just running the meta checker like we do currently.

That's a possibility, if we can make it robust (run with a low number of heartbeats). But the incidental complexity and unpredictabiliy of such a design is a bit worrysome.

Maybe this can hook into the ”abstract proofs” machinery used elsewhere.

I'm not sure I know what you're referring to here, what is this abstract proofs machinery?

I'll have to look for it myself, but I've seen .proof_1 definitions show up. Likely something related to

Ah, but it's not the abstracted proofs where I saw lean use previously defined helpers from unrelated definitions, but the match compiler: