Michael Soegtrop (Apr 10 2024 at 11:22): Michael Soegtrop (Apr 10 2024 at 11:22):When I combine messages made from Coq term and new lines - either in printf or with Message.concat, I get an unexpected indenting. I wonder if this is a bug or a feature I don't understand. This can be quite annoying when printing largish structures. Below is some example code:
Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.
Ltac2 string_newline () := String.make 1 (Char.of_int 10).
Ltac2 Notation nl := string_newline ().
Ltac2 coq_terms_1 () := '(forall (a b : nat), a+b=b+a).
Ltac2 coq_terms_2 () := '(forall (a b : nat), (((((((a+b=b+a /\ a+b=b+a) /\ a+b=b+a) /\ a+b=b+a) /\ a+b=b+a) /\ a+b=b+a) /\ a+b=b+a) /\ a+b=b+a) /\ True).
(* why is there an extra new line after every 2nd line *)
Ltac2 Eval printf "%t%s%t%s%t%s%t%s" (coq_terms_1 ()) nl (coq_terms_1 ()) nl (coq_terms_1 ()) nl (coq_terms_1 ()) nl .
(* here the indenting gets really weird for each other term *)
Ltac2 Eval printf "%t%s%t%s" (coq_terms_2 ()) nl (coq_terms_2 ()) nl .
the output is:
(forall a b : nat, a + b = b + a)
(forall a b : nat, a + b = b + a)
(forall a b : nat, a + b = b + a)
(forall a b : nat, a + b = b + a)
- : unit = ()
(forall a b : nat,
(((((((a + b = b + a /\ a + b = b + a) /\ a + b = b + a) /\ a + b = b + a) /\
a + b = b + a) /\ a + b = b + a) /\ a + b = b + a) /\
a + b = b + a) /\ True)
(forall a b : nat,
(((((((a + b = b + a /\ a + b = b + a) /\
a + b = b + a) /\
a + b = b + a) /\
a + b = b + a) /\ a + b = b + a) /\
a + b = b + a) /\ a + b = b + a) /\ True)
- : unit = ()
My expectation would be that each %t or Message.of_constr is indented individually, but apparently they are indented after putting the message together in some smart way, but not smart enough to recognise the newlines.
Michael Soegtrop (Apr 10 2024 at 11:27):I guess the way around this is to convert the messages to strings and back?
Michael Soegtrop (Apr 10 2024 at 11:38):Indeed wrapping the terms I don't want to be indented in:
Ltac2 no_indent (m : message) := Message.of_string (Message.to_string m).
solves the issue. But I guess I should create an issue that the indenter does not understand newlines?
Guillaume Melquiond (Apr 10 2024 at 11:50):Yes and no. Coq directly uses the boxing mechanism of the Format library, which indeed does not understand newlines. But this will not be fixed. You should instead modify your code so that it properly opens and closes boxes around newlines.
Guillaume Melquiond (Apr 10 2024 at 11:51):To be clearer, you should probably have a "vertical" box around your whole message, and replace the line breaks by box separators.
Michael Soegtrop (Apr 10 2024 at 12:22):Thanks, I see. I guess there is some markup syntax to do this. Could you please point me to the relevant documentation?
Guillaume Melquiond (Apr 10 2024 at 12:30):I don't know if it is documented for Ltac2. But here is the relevant part for Coq's notations: https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#use-of-notations-for-printing
Gaëtan Gilbert (Apr 10 2024 at 12:34):I don't think we expose APIs to do boxing in ltac2
probably we should
also maybe ltac2 formats should understand box annotations like ocaml Format.printf?
Michael Soegtrop (Apr 10 2024 at 12:44):Yes, IMHO some access to this API is needed in Ltac2. I can live for the time being with the "to string to message" method, but better control over this would be very useful.
Michael Soegtrop (Apr 10 2024 at 12:46):Would it be possible to have Ltac2 message primitives which correspond to the elements described in the documentation linked by Guillaume?
Last updated: Oct 12 2024 at 11:01 UTC