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.

I guess the way around this is to convert the messages to strings and back?

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?

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.

To be clearer, you should probably have a "vertical" box around your whole message, and replace the line breaks by box separators.

Thanks, I see. I guess there is some markup syntax to do this. Could you please point me to the relevant documentation?

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

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?

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.

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