[proof engine] Forbid tactic code to raise exceptions

[ejgallego]

Motivated by the recent discussion on Zulip about exceptions and
tactics, we move forward with the porting of tactic code to the
monadic proof engine and forbid tactics to raise non-critical
exceptions.

Instead, tactics calling exceptional code should catch and reify the
exception locally and use the proper proof engine API tclZero.

I think this is a very long due cleanup.

I hope @ppedrot likes this!

As of now, this is a draft, and not yet ready for benchmark. Stdlib
compiles, test suite is close to pass.

This should be combined with the work on PR #XXXX that adds exception
static analysis to Coq's codebase.

Next step is to remove wrap_exceptions, but that will require some
more tweaks as it appears is some critical paths.

(Hint: Click "hide whitespace" on the GH review tab to see relevant changes better)

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[ppedrot]

Actually, I am not sure I like this. It's part of the spec that enter blocks capture whatever exceptions are raised there. It's a bit fragile (you have to be sure that the exception-raising block is not inadvertently wrapped into a closure) but it also makes the code easier to read and to debug.

What should be totally forbidden is to raise exception from within the monadic layer, which is a different story.

[SkySkimmer]

This should be combined with the work on PR #XXXX that adds exception
static analysis to Coq's codebase.

What's this about?

[ejgallego]

Actually, I am not sure I like this. It's part of the spec that enter blocks capture whatever exceptions are raised there. It's a bit fragile (you have to be sure that the exception-raising block is not inadvertently wrapped into a closure) but it also makes the code easier to read and to debug.

What should be totally forbidden is to raise exception from within the monadic layer, which is a different story.

Not sure I understand your what you mean in your comment, the idea here is that tactics should indeed never raise and rely on enter and friends having that compat layer, but instead use the proper engine primitive for failure which is tclZero. Maybe we can chat about it in the call / working group? Or would you mind expanding more / going to Zulip?

My main motivation is that I'd like for values of type Proofview.tactic to be 100% pure in the medium-term. I think this is a good idea and would help with many goals (sic). But that is the main point a comptemtion IMHO to decide if this PR is good or not.

There are a few more pieces missing to make this PR a reality tho, related to what @SkySkimmer was asking IMHO we also need:

• to forbid user_err in any code use by tactics, and instead use the right exception
• to annontate functions with the exceptions they raise and use a static analyzed (PR incoming)

as to make this robust and realitistic, as we can't hope to make all code fucntional in one go, or to port the pretyper to the monad. We could by the way wrap a few usages here in a monadic API, but that depends on how we feel about code.

[SkySkimmer]

My main motivation is that I'd like for values of type Proofview.tactic to be 100% pure in the medium-term.

In the case of enter it's the goal -> tactic which raises not the tactic

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[ejgallego]

My main motivation is that I'd like for values of type Proofview.tactic to be 100% pure in the medium-term.

In the case of enter it's the goal -> tactic which raises not the tactic

Yes, how would it be otherwise?

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.