MantisBT - OCaml
View Issue Details
0007804OCamlstandard librarypublic2018-06-10 10:322018-06-11 21:41
herbelin 
octachron 
normalminoralways
resolvedno change required 
4.06.1 
 
0007804: In the format library, are boxes intended to implicitly break?
I have an example of a hov box containing a box where the split is not done at the break hints of the outer box but at the position of the opening of the inner box. This looks strange but maybe this is how it is supposed to work (I did not find documentation about it).
Executing the following shows the issue:
<<
for i = 4 to 7 do
Format.set_margin i; Format.printf "@[a@ #@[b@]@ c@]@.@.";
done
>>

The output is
<<
a
#b
c

a #
b c

a #
b c

a #b c

>>

which shows that in the second and third case, a break is introduced by the inner box, while, intuitively, the break should have been done at the break hints of the outer box.

Apparently, this is due to the test "insertion_point > state.pp_max_indent" in function format_pp_token of format.ml. Couldn't have the lack of enough space detected already at the time of considering the preceding "official" break hint?

I shall use a workaround on my side but I'm still reporting it as I did not succeed to get an opinion on whether this is normal or not.
No tags attached.
duplicate of 0007720assigned octachron Format: spurious space at end of line 
Issue History
2018-06-10 10:32herbelinNew Issue
2018-06-10 10:56octachronRelationship addedduplicate of 0007720
2018-06-10 11:02octachronNote Added: 0019171
2018-06-10 12:19herbelinNote Added: 0019172
2018-06-10 12:35octachronNote Added: 0019173
2018-06-10 13:33herbelinNote Added: 0019174
2018-06-10 14:02octachronNote Added: 0019175
2018-06-11 14:29octachronStatusnew => resolved
2018-06-11 14:29octachronResolutionopen => no change required
2018-06-11 14:29octachronAssigned To => octachron
2018-06-11 17:48herbelinNote Added: 0019181
2018-06-11 20:59octachronNote Added: 0019182
2018-06-11 21:41herbelinNote Added: 0019183

Notes
(0019171)
octachron   
2018-06-10 11:02   
This is the expected behavior: `Format.set_margin 4` fixes the maximum box indentation to 2 and further calls to set_margin does not change the value of the maximum box indentation. Then as explained in http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html#1_Maximumindentationlimit [^] (amended by 0007720 and https://github.com/ocaml/ocaml/pull/1596 [^]), boxes opened at a position greater than 2 are rejected to the left if the englobing box does not fit on the left.
(0019172)
herbelin   
2018-06-10 12:19   
Thanks for the quick answer. I still don't understand well if this is because it would be too complicated/costly to implement a preference given to the explicitly given break hints but I'm at least taking your answer as a confirmation that this is the official specification of the algorithm (of course the phenomenon is not tied to small values of `set_margin`). Thanks again.
(0019173)
octachron   
2018-06-10 12:35   
It is not so much a question of complexity than a question of specification. Note also that the problem only appears with small values of max_indent, setting max_indent to margin - 1 (or margin - small_offset) generally avoids the issue.
(0019174)
herbelin   
2018-06-10 13:33   
It depends if by small you mean small in the absolute or relatively small. When I observed the phenomenon first, I had margin 78 and max_indent 49. For instance, the following also triggers the problem:

Format.set_margin 15;
Format.set_max_indent 10;
Format.printf " @[aaaaaaaaaaa@ #@[b@]@ c@]@.@."

but for 15 > max_indent > 10, I don't see the problem any more. Are you saying that with a sufficiently relatively large value of max_indent, I can ensure that the box would let the explicit break hints do their job? Thanks in advance for further help.
(0019175)
octachron   
2018-06-10 14:02   
I would say that you probably want to fix the max_indent value to margin - offset with a small value of offset (the starting value is 10). The maximum indentation value is here as a safety net to avoid opening a box at a position where there is not enough space left to print the box in a readable way. There is no way to disable this mechanism, but it would happen less frequently with small values of margin - max_indent.
(0019181)
herbelin   
2018-06-11 17:48   
Hi, we discussed further the issue at https://github.com/coq/coq/issues/7731 [^] [^] and we catch a glimpse of how the formatting algorithm could maybe slightly be improved though.

The question is about the specification of `max_indent`. Is `max_indent` suppose to give the limit to indentation (as the name suggests) or to give a limit to box opening?

What seems to happen in the algorithm is that no box is opened beyond `max_ident` (line 352 of the current version of format.ml). However, there might be boxes which do not lead to breaks, because the whole contents of the box fits without needing a break. Would such situation considered to be respectful of the `max_indent` specification?

If yes, it seems to me (within the limits of my understanding of the algorithm) that the question is whether it would be possible to make a finer test to decide if the opening of a box should insert an initial break or not. For instance, could it be possible to detect that we are in an outer box with a preceding `break` in this outer box and that this preceding `break` already checked that it was not necessary to break the line to display the forthcoming contents and thus, that the inner box which is part of this forthcoming contents shall not need to add a break itself and shall not violate the max_indent limit?

Hoping that my words are clear enough (it is not so easy to explain).
(0019182)
octachron   
2018-06-11 20:59   
I agree that the algorithm could be improved. I would suggest to open a separate ticket as a feature request with a link to the problematic Coq examples and a good specification of the requested behavior. But I am not sure if Format's current maintainer is open to such modification.
(0019183)
herbelin   
2018-06-11 21:41   
OK, I opened a feature request at 7807.