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.
Do you have an example somewhere?
show some failed attempts?
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".
Ltac2 Eval Printf.printf "foo".doesn't - even after importing Ltac2.Printf).
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.
So, contrarily to Gallina, notation scopes are not automatically attached to definitions, only to notations.
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?
I assumed that notations are only influenced by scopes.
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
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.
it's not a scope, it's a whole parsing entry I think
also Ltac2 Notation is like Tactic Notation in this regard
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.
gallina scopes don't change the parser
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.
Ltac2 scopes are nothing like term notations, they define grammar rules, period.
The printf thing is a hack to make it palatable, it actually desugars to something pretty involved.
OCaml has a similar built-in hack, btw.
ocaml is type directed though, if you do
"foo" : _ format it works
Yeah, my point was about the disambiguation between quoted strings and formats.
internally it desugars to a fancy GADT
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