sorry warning not shown when Elab.async is disabled

Stream: lean4

[Eric Wieser]

In this example, the sorry warning on the second theorem is conditional:

set_option Elab.async false

theorem sorry_in_proof1 : False := by
  as_aux_lemma => sorry -- warning

theorem sorry_in_proof2 : False := by
  as_aux_lemma => sorry  -- no sorry warning here unless you comment out `Elab.async`

[Eric Wieser]

This is presumably because in the synchronous case mkAuxTheorem is reusing an existing auxiliary theorem

[Markus Himmel]

A variant of this was fixed in lean4#10388, so possibly the same fix should be added to the as_aux_lemma tactic.

[Eric Wieser]

Should this be built into mkAuxTheorem?

[Markus Himmel]

To me it's not 100% clear that disabling the cache like this always desirable, even when invoking mkAuxTheorem somewhere deep in some other thing.

[Eric Wieser]

(for what it's worth, I ran into this while debugging #lean4 > Kernel error in list index notation, since omega calls mkAuxTheorem)

[Kyle Miller]

The 10388 fix is a bit of a hack, justified by being simple to reason about, and the cost to not caching terms with sorry is fairly localized.

Another justification for it is the following. What is special about sorry is that its identity matters — after all, it records a source position, and even if it's a bare sorryAx, we want to attribute the sorry to the current declaration. The aux lemma cache is keyed by the type of the proof, and it does not take the proof itself into consideration. When there is a sorry, we might say that the sorries themselves should be part of the key. Disabling the cache when there is a sorry is a way to ensure the sorry actually makes it into the environment.