Guillaume Melquiond (Feb 03 2022 at 17:41): 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.
Guillaume Melquiond (Feb 03 2022 at 17:41):Do you have an example somewhere?
Gaëtan Gilbert (Feb 03 2022 at 17:43):show some failed attempts?
Guillaume Melquiond (Feb 03 2022 at 17:51):Ltac2 Eval Printf.printf "foo".
I think you need the notations. This works:
Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.
Ltac2 Eval printf "foo".
(But Ltac2 Eval Printf.printf "foo".doesn't - even after importing Ltac2.Printf).
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.
Guillaume Melquiond (Feb 03 2022 at 18:01):So, contrarily to Gallina, notation scopes are not automatically attached to definitions, only to notations.
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.
Oh, I didn't know that notations in Gallina can be accessed with module path prefixes. Is this indeed so?
Michael Soegtrop (Feb 03 2022 at 18:03):I assumed that notations are only influenced by scopes.
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 *)
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.
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
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.
Gaëtan Gilbert (Feb 03 2022 at 18:39):gallina scopes don't change the parser
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.
Pierre-Marie Pédrot (Feb 03 2022 at 21:41):Ltac2 scopes are nothing like term notations, they define grammar rules, period.
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.
Pierre-Marie Pédrot (Feb 03 2022 at 21:42):OCaml has a similar built-in hack, btw.
Gaëtan Gilbert (Feb 03 2022 at 21:44):ocaml is type directed though, if you do "foo" : _ format it works
Pierre-Marie Pédrot (Feb 03 2022 at 21:44):Yeah, my point was about the disambiguation between quoted strings and formats.
Pierre-Marie Pédrot (Feb 03 2022 at 21:45):internally it desugars to a fancy GADT
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: Oct 08 2024 at 16:02 UTC