pretty printer + brackets

Stream: general

[Eric Rodriguez]

image.png

is this considered a bug or a feature?

[Eric Wieser]

Bug

[Eric Wieser]

But I think it's a font rendering bug in webkit / blink

[Eric Wieser]

I've seen it in doc-gen too

[Floris van Doorn]

I've also seen this sometimes. I think it usually only happens when coercion arrows are present.

[Kevin Buzzard]

This is the "random close-bracket in the wrong place" bug I think?

[Patrick Massot]

Some of my students see this bug everywhere and it's driving me crazy, especially since I can't reproduce it on any computer I can access to. I think fixing this should be very high priority but I don't see how to help without being able to reproduce.

[Mario Carneiro]

is the second close bracket considered a bug?

[Mario Carneiro]

because I see that all the time

[Eric Wieser]

I think only the ) in the blue box is the bug

[Eric Wieser]

Because the reading order has to backtrack vertically which isn't how reading is supposed to work

[Eric Wieser]

I see this bug a lot for ↥, but it seems not to happen for ⇑ for me

[Eric Wieser]

Putting the cursor at the beginning of this line does it for me:
https://github.com/leanprover-community/mathlib/blob/0cc3cd54efb97332e973e0ff1ca94dbd486899eb/src/algebra/direct_sum_graded.lean#L584

[Eric Wieser]

image.png

[Eric Wieser]

This also reproduces it for me:

import algebra.pointwise

example (S : set ℕ) : ↥(S + S) = ↥(S + S) := sorry  -- goal view is wonky at the sorry

[Patrick Massot]

I see no issue at all

[Patrick Massot]

in Eric's two examples

[Eric Wieser]

With what font?

[Eric Wieser]

This is a font / CSS issue I think

[Patrick Massot]

DevaVu sans mono

[Eric Wieser]

I see it with Consolas on Windows

[Eric Wieser]

The CSS specifies the indents in terms of "ch", the width of an 0. In consolas, that character is considerably narrower than an 0:
image.png

[Eric Rodriguez]

it's a font thing for sure; just installed dejavu sans mono and it's fixed itself
image.png

[Patrick Massot]

@Edward Ayers do you think you could fix this issue now that we understood where it comes from?

[Patrick Massot]

Does anyone know a simple way to explain how to install DejaVu sans mono on Windows or Mac? I mean simple enough that students could understand.

[Eric Rodriguez]

its super easy on windows, just get the files, double click them and there's an install button

[Eric Rodriguez]

image.png

[Eric Wieser]

Here's a #mwe: bad.html edit: i messed that up

[Scott Morrison]

Similarly on a mac. Download the zip file, unzip it, double click on a font file, and click "install font":
Screen-Shot-2021-05-03-at-9.16.38-pm.png

[Patrick Massot]

Thanks Eric and Scott, I'll try to tell my students to try this.

[Eric Wieser]

If I change ch to ex in the CSS the problem goes away

[Eric Wieser]

Actual mwe copied out of vscode: bad.html

[Eric Wieser]

Which is weird, because ch is supposedly the width of a 0, and ex the width of an x... Which are the same in a monospace font

[Patrick Massot]

Your bad example displays fine here. Maybe I don't have that font and my browser falls back to a good one.

[Eric Rodriguez]

i also thought ex was width, but just googled and it seems ex is height of x (which is the same, but not the same as height of 0? unsure)

[Eric Rodriguez]

not sure if Linux has consolas Patrick

[Eric Wieser]

Ah, in that case my proposed fix is not a justified one

[Edward Ayers]

The autoindenting CSS strikes again

[Edward Ayers]

The problem is that get getting the pretty indenting in CSS to work is a little hacky. I think that the correct approach would be to take full control of newlines and so on based on the width of the view, but I think that would be quite a lot of work.

[Eric Wieser]

Presumably the text reflowing would be a JavaScript job within the view window

[Eric Wieser]

But I agree, that sounds like a lot of work

[Edward Ayers]

Ideally no. Because it breaks the abstraction of Lean sending widgety HTML.

[Edward Ayers]

But practically yes do it with javascript

[Eric Wieser]

Oh, I assumed the goal view was special-cased

[Edward Ayers]

No it's all done by lean

[Eric Wieser]

Alternatively: output every character in the goal view in its own span with min-width set to 1ch

[Eric Wieser]

But that increases the textual size of the html by an order of magnitude

[Edward Ayers]

The dream of widgets was that absolutely all of the presentation code would be in Lean, so you wouldn't have to ever worry about javascript. But there are lots of places where that breaks so I don't think it's worth holding on to that abstraction in the cases where it is clearly awkward.

[Edward Ayers]

Eric Wieser said:

But that increases the textual size of the html by an order of magnitude

I suspect this would actually have ok performance.

[Eric Wieser]

Maybe it's sufficient to put a span around every word with min-width proportional to its number of characters

[Edward Ayers]

yeah that might work

[Edward Ayers]

might get some clipping

[Eric Wieser]

Assuming we don't wrap within words right now

[Eric Wieser]

Min-width shouldn't clip

[Eric Wieser]

It should just insert extra space sometimes

[Edward Ayers]

yeah an alternative might be to just add some extra space whenever there is a grouping in the pretty-printed sexpr

[Edward Ayers]

The styles to fiddle with are in https://github.com/leanprover-community/mathlib/blob/9c86e38141b94bcd23665717f26c1da1622c59a7/src/tactic/interactive_expr.lean#L157

[Patrick Massot]

Isn't there at least a temporary fix swapping ex and ch or whatever?

[Edward Ayers]

@Eric Wieser sorry why did setting it as ex work?

[Edward Ayers]

Eric Wieser said:

If I change ch to ex in the CSS the problem goes away

Why was this crossed out sorry?

[Eric Wieser]

Because it is a bad idea

[Eric Wieser]

ex is for vertical spacing

[Edward Ayers]

So for context, @Daniel Fabian spotted a trick where you can emulate Wadler-style pretty printing in CSS by setting the text indentation to be a negative number and padding to be minus that number, then if that block can't fit on one line, it will linebreak with an apparent indent. But what is happening here (which I unfortunately didn't observe because I have a all-unicode monospaced font) is some width calculating maths in the browser is messing up and it is linebreaking because of the different-width characters.

[Edward Ayers]

Eric Wieser said:

ex is for vertical spacing

But did it actually fix the problem?

[Edward Ayers]

Maybe we could use px

[Edward Ayers]

@Eric Wieser how do I use your bad.html mwe?

[Edward Ayers]

should it just render bad or do I need to change the width of the viewport?

[Eric Wieser]

It should just render badly

[Edward Ayers]

In chrome?

[Eric Wieser]

Anything other than 1ch will not indent right when it's actually supposed to wrap

[Eric Wieser]

Chrome on windows

[Edward Ayers]

Do you know if there are any linux fonts where this bug happens?

[Edward Ayers]

got it

[Edward Ayers]

@Eric Wieser please could you have a go at changing the ex → em?

[Edward Ayers]

never mind it breaks for me

[Edward Ayers]

wow

[Edward Ayers]

This bug is mad

[Edward Ayers]

@Eric Wieser please could you try the bad example with 0.9ch?

[Eric Wieser]

The bug is easier to reproduce another way

[Eric Wieser]

Change 1ch to 2ch

[Edward Ayers]

where?

[Eric Wieser]

And instead of using the weird arrow character that is too narrow, compare a one char prefix with a two char prefix

[Eric Wieser]

Everywhere

[Eric Wieser]

The cause is that \u-| is less than 1ch wide

[Eric Wieser]

I can give you a better repro tomorrow

[Edward Ayers]

no need I've found a small one

[Eric Wieser]

Did you find the ascii-only repro?

[Edward Ayers]

Yeah you get it whenever the text-indent minus text-indent is lower greater than the minwidth char

[Edward Ayers]

so if you use a non-monospace font then you get it p quickly

[Eric Wieser]

Right, but you can get it for monospace ascii too

[Edward Ayers]

Yes by setting it to 2ch

[Edward Ayers]

since that is a greater width than the narrowest char

[Eric Wieser]

That sounds like the reverse of what you said above

[Edward Ayers]

text indent is negative

[Edward Ayers]

ygwim

[Edward Ayers]

So the quick-and-dirty solution is to set it to use 0.9ch or whatever width these offending chars are

[Edward Ayers]

maybe just set it as 0.5ch

[Edward Ayers]

and then the quest begins to find a way of indenting stuff that doesn't require this hack

[Edward Ayers]

in the first place

[Eric Wieser]

0.5 makes the line wrapping look a little weird though

[Edward Ayers]

what is the biggest number you can get away with?

[Edward Ayers]

I think that the main pain point is windows users with consolas

[Eric Wieser]

\_l is pretty darn narrow

[Eric Wieser]

Frankly just putting coe_sort in a 1ch box would fix all the problems I actually see often

[Edward Ayers]

Ok maybe let's do that for now, and a few other common killers

[Edward Ayers]

I'll have another go tomorrow

[Eric Rodriguez]

just to make everything even more annoying, this can even happen with DejaVu Sans Mono depending on the screen resolution and stuff (if I make the widget screen-wide, it goes away but that's clearly undesirable :b there's some other wider element way above in the goal view, and for some reason it doesn't allow this to be wider because of it)

image.png

(polynomial_galois_group.lean:243)

[Alex J. Best]

I actually put my info view as a horizontal split instead, so below my code rather than beside it, for this sort of reason, I find it far easier to read that way even if having less lines of the source code visible is occasionally annoying.

[Eric Wieser]

Eric, that image doesn't seem to show the same bug

[Eric Wieser]

I think that's working as intended, or at least could be construed to be; unlike the original report, it's not actively breaking the reading order