Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

In the format library, are boxes intended to implicitly break? #7804

Closed
vicuna opened this issue Jun 10, 2018 · 8 comments
Closed

In the format library, are boxes intended to implicitly break? #7804

vicuna opened this issue Jun 10, 2018 · 8 comments

Comments

@vicuna
Copy link

vicuna commented Jun 10, 2018

Original bug ID: 7804
Reporter: herbelin
Assigned to: @Octachron
Status: resolved (set by @Octachron on 2018-06-11T12:29:44Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.06.1
Category: standard library
Duplicate of: #7720
Related to: #7913
Monitored by: ralfj @gasche

Bug description

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).

Steps to reproduce

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.

@vicuna
Copy link
Author

vicuna commented Jun 10, 2018

Comment author: @Octachron

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 #7720 and #1596), boxes opened at a position greater than 2 are rejected to the left if the englobing box does not fit on the left.

@vicuna
Copy link
Author

vicuna commented Jun 10, 2018

Comment author: herbelin

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.

@vicuna
Copy link
Author

vicuna commented Jun 10, 2018

Comment author: @Octachron

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.

@vicuna
Copy link
Author

vicuna commented Jun 10, 2018

Comment author: herbelin

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.

@vicuna
Copy link
Author

vicuna commented Jun 10, 2018

Comment author: @Octachron

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.

@vicuna vicuna closed this as completed Jun 11, 2018
@vicuna
Copy link
Author

vicuna commented Jun 11, 2018

Comment author: herbelin

Hi, we discussed further the issue at coq/coq#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).

@vicuna
Copy link
Author

vicuna commented Jun 11, 2018

Comment author: @Octachron

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.

@vicuna
Copy link
Author

vicuna commented Jun 11, 2018

Comment author: herbelin

OK, I opened a feature request at 7807.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants