Stream: Ltac2

Topic: Notation scopes for Printf


view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:41):

Speaking of notation scopes, I completely failed at using Printf. I could not convince Coq to produce a format string instead of a plain string.

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:41):

Do you have an example somewhere?

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 17:43):

show some failed attempts?

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:51):

Ltac2 Eval Printf.printf "foo".

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 17:54):

I think you need the notations. This works:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.
Ltac2 Eval printf "foo".

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 17:55):

(But Ltac2 Eval Printf.printf "foo".doesn't - even after importing Ltac2.Printf).

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 17:57):

Yes. I should have made it clearer that Import Printf was not helping. But indeed, removing Printf actually works. I would not have thought of that.

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 18:01):

So, contrarily to Gallina, notation scopes are not automatically attached to definitions, only to notations.

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 18:01):

This is so because there is a printf function and a printf notation:

Ltac2 printf fmt := Format.kfprintf print fmt.
Ltac2 Notation "printf" fmt(format) := printf fmt.

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 18:02):

Oh, I didn't know that notations in Gallina can be accessed with module path prefixes. Is this indeed so?

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 18:03):

I assumed that notations are only influenced by scopes.

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 18:05):

From Coq Require Import Reals.
Definition foo := RbaseSymbolsImpl.Rplus 0. (* actually 0%R *)
Definition bar := Nat.add 0. (* actually 0%nat *)

view this post on Zulip Michael Soegtrop (Feb 03 2022 at 18:17):

Ah, I got you wrong - I thought you mean you can access the notation with the Printf. prefix.

You are right, one can't attach a notation scope to arguments of Ltac2 functions - I think this is fair enough since it is not so common that one needs this and I would say it is fine to define notations in these cases.

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 18:18):

it's not a scope, it's a whole parsing entry I think
also Ltac2 Notation is like Tactic Notation in this regard

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 18:27):

Sure, but Ltac1 had close to no type system. Since Ltac2 does have a type system, it would be great to have the same feature as Gallina, i.e., scopes associated to types.

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 18:39):

gallina scopes don't change the parser

view this post on Zulip Guillaume Melquiond (Feb 03 2022 at 20:04):

It depends. Custom entries look a lot like a change of parser. Sure, this is not as powerful as directly writing a parser in OCaml. But it is still on a whole different level than Gallina's usual notations.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 21:41):

Ltac2 scopes are nothing like term notations, they define grammar rules, period.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 21:42):

The printf thing is a hack to make it palatable, it actually desugars to something pretty involved.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 21:42):

OCaml has a similar built-in hack, btw.

view this post on Zulip Gaëtan Gilbert (Feb 03 2022 at 21:44):

ocaml is type directed though, if you do "foo" : _ format it works

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 21:44):

Yeah, my point was about the disambiguation between quoted strings and formats.

view this post on Zulip Pierre-Marie Pédrot (Feb 03 2022 at 21:45):

internally it desugars to a fancy GADT

view this post on Zulip Michael Soegtrop (Feb 04 2022 at 08:11):

printf is already several orders of magnitudes better than the previous message system. Of course things can be further improved, but we all have only finite time. After about 2 years of Ltac2 usage I can say that I am very happy with it and also with the improvements done since then. I take this as opportunity to give a big thank you to @Pierre-Marie Pédrot! And I am looking forward to what proof automation grand master @Guillaume Melquiond is doing with it!

Btw.: IMHO what is missing most in Ltac2 is not new features, but more extensive documentation.


Last updated: Jan 31 2023 at 11:01 UTC