RFC: Realizalbe constants error handling

[nomeata]

Context

We have a few definitions that are lazily realized when they are actually used (equational theorems, functional induction theorem, the splitter, and there are more to come). For some of them the construction can fail, and it seems unlikely that we’ll make all of them work always anytime soon.

Status quo

If the process then every attempt to use the constant will run the process again. Log messages and exceptions are shown, in addition to a “unknown constant 'foo.bar'” error message.

Problem

This is not great because the work is repeated unnecessarily (e.g. imagine a try split in a tactic, trying to create the splitter over and over again), and the error messages are likely confusing to the user if the user is not aware of how realizable constants work.

This is also the reason why using #check foo.induct shows error messages twice, because #check happens to try to elaborate the name in different ways, and each attempts a realization.

Ideally, the visible behavior is as close as possible to the mental model of the users, which is that these realizable constants either had existed all along, or simply don’t exist.

Proposal

To get closer to that ideal, I suggest

• To introduce a persistent env extension failedRealizations that stores the name of realizable constants that failed to realize. This is used to avoid trying to futilely realize a constant over and over again.
• Log and error messages from the generation process are hidden by default (so that to the user it looks as if the constant is there or not.)
• With set_option debug.realization true the messages are shown.

Variants

I thought about storing the log and error messages in the env extension so that it can be queried with a #print realization_errors foo.induct or so, but seems overkill. Maybe for debugging we’ll need a way to force realization even if there is an entry in failedRealizations.

[Kha]

#5864 should ensure error messages are printed at most once, all other elaboration threads will see a sorried-out constant. I don't think it's a good idea to hide error messages by default, I'd rather annotate them with the proper context.

[nomeata]

(Let’s pause this discussion until parallelism lands)

[nomeata]

Related: #6066, #6065, #6067. Worth looking at them together.