[Merged by Bors] - feat(meta/widget): Add css classes for indentation as required by group and nest.

[DanielFabian]

this is a transplant of leanprover-community/lean#439

the relevant css section looks more or less like this:

        .indent-code {
            text-indent: calc(var(--indent-level) * -1ch);
            padding-left: calc(var(--indent-level) * 1ch);
        }

For details, one can play around here: https://jsfiddle.net/xbzhL60m/45/

[EdAyers]

Can you try replacing [cn $ "highlight_" ++ c.to_string] with [cn c.to_string]? There are already some CSS classes which style particular colours.

[EdAyers]

I guess a problem is that you want the highlighting colours to be theme-dependent so that they are readable for both light and dark themes.

[DanielFabian]

BTW, would it be possible to inline the .indent-code class for now (i.e. use style instead of cn)? Then we could test it without modifying the extension.

Unfortunately not. We need to change the CSS in the extension in such a way, that the whole subgoals become display:inline-block as opposed to display:inline what they are now. If you do it only on one tag, it completely moves stuff around and it's not even in the same order anymore.

I was in contact with @EdAyers about this and understood, that we can take a look at the vscode extension shortly, this is mostly preparatory work, really.

[gebner]

LGTM. Maybe @EdAyers wants to look at this as well (there is a demo webpage linked from the PR in the lean repo).

bors d=EdAyers

[gebner]

This should probably be translated to one of the classes like hot-pink that are already in tachyon.

[DanielFabian]

I'd rather not do that. Because it encodes a hard mapping between mathlib's source code and the plugin, whereas the CSS class is conceptually much more flexible. Plus highlighting might also be encoded with other means than color like italics or bold. From an accessibility point-of-view, I'd rather have the CSS handle that, if it's ok.

[EdAyers]

Everything about the lean widget system already assumes a hard mapping, namely it assumes that a CSS library called Tachyons is being used. So any styling choices should be made in the lean code not in a separate CSS file (I admit indent-level is an exception). I don't think it makes sense to have color.red mean anything other than colouring the text red.

[EdAyers]

I guess it's awkward for people who have a kind of colourblindness where they can't distinguish certain colours from black or white (idk if that's possible). I don't think we will have cases where it is necessary for the user to be able to distinguish the highlight colours to understand the format string.

[bors]

✌️ EdAyers can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[gebner]

BTW, would it be possible to inline the .indent-code class for now (i.e. use style instead of cn)? Then we could test it without modifying the extension.

[EdAyers]

We should hold merging this until the indent-code class is in vscode repo.

BTW, would it be possible to inline the .indent-code class for now (i.e. use style instead of cn)? Then we could test it without modifying the extension.

Maybe... I'm not sure if React styles supports these CSS variable calculations yet. Another approach is to use the customCSS vscode setting.

"lean.infoViewStyle": ".indent-code { text-indent: calc(var(--indent-level) * -1ch); padding-left: calc(var(--indent-level) * 1ch);}"

[EdAyers]

Doesn't seem to be working quite right for me:

You can see that it is adding an indent before the [ even though a newline wasn't inserted. It also cancels the padding of the expressions inside the tooltip and adds some unwanted indents to the explicit args list/

[EdAyers]

How did you get your output in the jsfiddle to have newlines non-breaking spaces?

[DanielFabian]

you need all elements to be display:inline-block. Then it behaves as you would want. Also you nee the text-indent to be negative, whilst the padding-left is positive.

[EdAyers]

I think not all elements need to be display:inline-block, just the one which has the block.

[DanielFabian]

could you share the HTML you used to draw this? I think I had similar kinds of artifacts previously, too

[EdAyers]

Sorry for deleting previous comment. Here is a simpler example of the problem:

[DanielFabian]

Ah, yes, I had exactly these kinds of artifacts, until everything, including \|- was inline-block.

[EdAyers]

The inner inline block is linebreaking prematurely, I guess because the width linebreak calculation is taking in to account the indentation / padding wrong. It's not in the CSS standard yet but in the future it should be possible to use text-indent: 4ch hanging instead: https://developer.mozilla.org/en-US/docs/Web/CSS/text-indent

[DanielFabian]

The problem with text-indent is, that it's being ignored for inline elements. That's why I had to make inline-block. And I wouldn't be too worried about using fairly new features as what we're running is essentially chrome, I believe.

[EdAyers]

hanging is not implemented in chrome yet

[DanielFabian]

How did you get your output in the jsfiddle to have newlines non-breaking spaces?

non-breaking spaces I get by using   instead of ' '. Ideally, we get from the format string, where there is a format.line. In these cases, we'd use ' ' and   everywhere else.

[gebner]

I just played around with the jsfiddle a bit. The --indent-level variable is completely unnecessary, right? We could just use [style "text-indent" "-1ch", style "padding-left" "1ch"] instead (substitute 1 by the nesting level, but everything uses 1 afaict).

[DanielFabian]

yes, in principle, The main idea was about not hard-coding that 1ch, but rather have css decide if 1ch is the right amount. On the other hand, from lean we do get the intent that this is supposed to be indented by 1 unit, so I just thought, we can let css handle the concrete amount by how much. But yes, we could also hard-code 1ch.

[DanielFabian]

Having the --indent-level just meant that we only have one parametric class vs. one class per indentation.

[gebner]

I think the weird rendering is due to directly nested indent-code elements:
https://jsfiddle.net/5jdshv0a/

[gebner]

Some experience reports from the documentation PR:

1. If you don't directly nest these spans, the rendering is reliable.
2. I only needed a single class, no variables.
3. It seems to be a bit of a black art how to translate group and nest into spans, because they have slightly different semantics. If you use group, then I found that it will break before the comma in ∀ (x : α), x = x. This is really ugly. So I've tried only using nest instead. This mostly works fine, except that ∀ (x : α) (y : α) (z : α), x < y ∧ y < z can be broken like this:

∀ (x : α) (y :
    α) (z : α),
  x < y ∧ y < z

(example here: https://gebner.github.io/mathlib_docs/control/traversable/basic.html#is_lawful_traversable)

leanprover-community/doc-gen#47

[DanielFabian]

one thing we could do, is make the space after : an  , you probably don't want to ever break after the colon.

[gebner]

But wouldn't you then get this?

∀ (x : α) (y
    : α) (z : α),
  x < y ∧ y < z

Ideally we'd have a span around (y : α).

[DanielFabian]

not span, because span has no meaning. What we really want is a non-breaking space. But the point is, the format from lean already has that info. It has a notion of spaces and lines. Whereas a line is something that can break, and a space cannot. So we should carry that info from C++ into the eformat, ideally. Because then we can encode breaking and non-breaking spaces correctly.

But just a span does not prevent breaking.

[gebner]

Regarding the wider discussion points:

First of all, I don't think there is a way to faithfully support the current format API in CSS. There is a huge semantic gap between format.group and display: inline-block. Concretely, format.group prints newlines as newlines if and only if the contents do not fit on the current line. I don't see any way to simulate this behavior in CSS.

Therefore, I believe we either need quick-to-implement hacky heuristics, or some extension to the current format code like an explicit new format.html_group constructor. (A third option would be to simulate the formatting using javascript.)

Extending the current format code (and pretty-printer) is a significant undertaking, though. May I remind you that the days of Lean 3 are numbered, and we will soon pay allegiance to the Clover. On the other hand, this could be an experiment that makes it into Lean 4, I don't know. The CSS-based formatting is less powerful (and hence uglier) than the Wadler-Leijen pretty-printer, so we can't get rid of the "old" one.

Maybe it is enough to distinguish between format.line and format.space, as you mentioned. This would be interesting (and also a bit of work to find out), but I'm sceptical.

If we start building custom heuristics, then on one hand, we'll diverge from the current pretty-printer very quickly.

I don't think the Lean 3 pretty printer is ever going to change anymore.

On the other hand, format was really meant to be the thing that would tell how things ought to be rendered. It does contain information about where line breaks are allowed and it contains the information by how much to indent.

The information in the format object is not a pretty-printer-agnostic description of how the text should be rendered. It has a precise semantics (see the Wadler paper), and we tune the format objects so that the one implementation we have prints it nicely.

Additionally, the format object also contains one more piece of information, which is at least as important as the two you mentioned. Namely the group information, which tells us that several line breaks can only be inserted together.

I'd really suggest just writing a new pretty-printer from scratch. It's not that hard and it could be more closely aligned to what HTML can and cannot do.

I wouldn't underestimate the effort here. You'd also need a lot of API that is only accessible from C++ at the moment (like notations, etc.).

[DanielFabian]

Fair enough, just one last comment. The behaviour or introducing line breaks if and only if the content doesn't fit is very much what a browser does all the time. In fact, it does it, whenever you don't disallow line breaks. Hence the distinction between ' ' and  . For all other points, I get where you're coming from.

[gebner]

Mmmh, maybe I wasn't clear enough. If the following doesn't fit on a single line, it will take up 10 lines (because all of the linebreaks were activated):

format.group $ format.nest 1 $ "[" ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x," ++ format.line ++
"x" ++ "]"

https://leanprover-community.github.io/lean-web-editor/#code=meta%20def%20f%20%3A%3D%0Aformat.group%20%24%20format.nest%201%20%24%20%22%5B%22%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%2C%22%20%2B%2B%20format.line%20%2B%2B%0A%22x%22%20%2B%2B%20%22%5D%22%0A%0A%23eval%20tactic.trace%20%24%20f.to_string%20%28options.mk.set_nat%20%60pp.width%20100%29%0A%23eval%20tactic.trace%20%24%20f.to_string%20%28options.mk.set_nat%20%60pp.width%2010%29

[DanielFabian]

Ah gotcha

[EdAyers]

Yeah this is way more difficult to implement than I was hoping it would be. When I originally wrote tagged_format I was just kinda hoping there would be a clever CSS trick that would be good enough, and Daniel almost got that working but there are still cases where it doesn't work properly because of some annoying inaccessible linebreaking logic. Lean 4 also makes me think that an expedient solution to the main cases should be preferred to an all-singing all-dancing pp. Since we have information about expression boundaries, perhaps there could be a button where you can collapse subexpressions or demand that the args for a given function be rendered one argument per line with an indent.

[EdAyers]

Suppose that the interactive_expr.mk routine knew the width of the viewport in characters, how hard would it be then to write some lean code that formatted overflow on a newline with an indent?

[EdAyers]

Would something like 2021706 work?

[EdAyers]

It tracks the length of the current line with a counter and then wraps the rest of the expr in a div if it overflows a fixed column count. It looks ugly rn but as a POC is it the right approach?

[EdAyers]

Eg:

But you could imagine tweaking the algo so that it is a bit more sensible than this.

[gebner]

@EdAyers If you have the screen width available, then you should just implement the formatting algorithm that format uses. See the Wadler paper for the classic introduction. I believe @digama0 has a Lean version of format lying around that could be reused.

The "insert newline on overflow" approach is pretty much was the CSS version does, AFAICT. I don't think we need to reimplement that in Lean. The heuristics used in the mathlib documentation seem to work mostly fine (maybe the trailing closing parentheses could be cleaned up though).

[EdAyers]

Right so could we just set the screen width to be a constant for now?

[gebner]

To be honest, I would prefer even the current slightly buggy version of this PR over a fixed screen width.

[DanielFabian]

I think getting the screen width from JavaScript would in principle enable us to use the correct format code in lean. Then you could have an adjustable Wadler-based pretty printer. We probably could even back-port it from lean 4 in the worst case.

But without it, I too think the current CSS-based version is a better trade-off.

[EdAyers]

I have a question, did the Wadler formatter ever work in the vscode extension?

[EdAyers]

Looks mostly good to me now. Thanks @gebner for sorting that out, much easier than implementing a formatter!
Sometimes there are still some issues in the type tooltip if there is a really big argument, it will add linebreaks. So the quick fix there is to allow one to turn off the indenting system.

[EdAyers]

Let's save the fix for above for another PR

bors r+

[bors]

👎 Rejected by label

[EdAyers]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests