Stream: Coq devs & plugin devs

Topic: Lost with tclFail/tclZERO/raise


view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:19):

Hi, I forgot a bit what is the rationale regarding when to use tclZERO, tclFAIL, or simply raise in tactics.
For instance, convert_concl has a raise NotConvertible but convert_gen has tclFailed (str "Not Convertible"). Is it expected?

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:19):

Isn't it that tclFAIL is only for LtacX's fail (or assimiliated, like LtacX pattern-matching)?

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:19):

And that in an enter blocks, it does not matter whether it is tclZERO or raise??

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 15:24):

raise in the closure of a Goal.enter is the same as ZERO
(NB the closure is before we go back to the monad, so eg Goal.enter (fun gl -> raise A; tclUNIT () >>= fun () -> raise B) the raise A is the same as tclZERO A but the raise B will not be properly caught)
Using raise in Goal.enter is perhaps fragile or bad style, but it is done a lot

for zero vs fail I think we generally prefer zero with a custom exception (not tclZERO (UserError Pp.(str "whatever")))

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:47):

There is also that Fail comes with a level which is decreased at each try, right?

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:50):

So, for convert_gen (and other places in tactics.ml), can I consider safe to replace the tclFAIL (str "Not Convertible") with raise NotConvertible (which gives the same error message)?

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:51):

Ah, and there is the question that tclZERO requires an info while raise requires nothing, and Loc.raise requires just a loc.

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 15:53):

tclzero does not require an info, it's optional

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 15:54):

Hugo Herbelin said:

So, for convert_gen (and other places in tactics.ml), can I consider safe to replace the tclFAIL (str "Not Convertible") with raise NotConvertible (which gives the same error message)?

I think it's fine
the default level for fail is 1 AFAIK so in try it behaves the same as any other tclZERO (ie the try succeeds doing nothing)

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:55):

Ok, right. And if I have just a loc, I can also get an info from it. So, tclZERO is enough.

view this post on Zulip Hugo Herbelin (Oct 10 2023 at 15:56):

OK thanks, it is for #18106 and I will push something.


Last updated: Oct 13 2024 at 01:02 UTC