Ltac2: provide access to boxing API in printf

[MSoegtropIMC]

Is your feature request related to a problem?

It is hard to structure large Ltac2 output, because it does not provide access to the boxing / formatting mechanisms of the pretty printer. Using newlines in printf leads to strange indenting.

Here is an example:

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 = ()

Proposed solution

Ltac2 could provide a set of message objects which correspond to the formatting tokens described in:

https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#use-of-notations-for-printing

One can then combine these with content via Message.concat.

Alternative solutions

Provide (backslash) escapes for formatting in in printf format strings. This would also make sense in addition to the above.

Additional context

See Zulip discussion

https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Unexpected.20indenting.20of.20coq.20terms

[SkySkimmer]

#18988