Stream: Ltac2

Topic: ✔ assert notation

Michael Soegtrop (Nov 10 2023 at 08:32):

I am using notations like:

Ltac2 Type exn ::= [ VST2_failure (message) ].
Ltac2 throw_VST2 fmt := Message.Format.kfprintf (fun msg => Control.throw (VST2_failure msg)) fmt.
Ltac2 Notation "throw_VST2" fmt(format) := throw_VST2 fmt.

Now I wanted to have a similar notation for an assert which throws only if a supplied Ltac2 boolean is false. I want this done so that the printf is not evaluated in case the test passes, since I tend to pass large %t arguments or recursive %a arguments. I find this rather tricky to do because I don't see an easy way to consume the extra arguments of the format in case the test passes. Should I define a dummy kfprintf function? Is there an easy way to do this?

Janno (Nov 10 2023 at 08:51):

@Rodolphe Lepigre might know how to deal with this

Gaëtan Gilbert (Nov 10 2023 at 09:48):

I think ocaml defines a dummy function for this (ikfprintf)

Rodolphe Lepigre (Nov 10 2023 at 10:19):

That is indeed the only way I know how to do that.

Gaëtan Gilbert (Nov 10 2023 at 10:49):

https://github.com/coq/coq/issues/18292

Michael Soegtrop (Nov 10 2023 at 11:18):

Thanks! I thought I missed something obvious, but apparently it just isn't that trivial.

Notification Bot (Nov 10 2023 at 11:19):

Michael Soegtrop has marked this topic as resolved.

Last updated: Oct 12 2024 at 13:01 UTC