VS Code weird parentheses

Stream: general

[Patrick Johnson]

import tactic

example (f : ℕ → bool) : f 0 ↔ true → f 0 :=
begin
  --
end

Screenshot

Why are the closed parentheses on a new line?
If we remove import tactic, then it is rendered as normal.

[Eric Rodriguez]

fonts, I feel like there was some work to get this working with all fonts but it didn't really go far

[Eric Rodriguez]

if you use DejaVu Sans Mono it should fix itself (you don't need to change your editor font, you can just change the infoview font using the "Lean: Info View Style" setting (I do .font-code { font-family: "DejaVu Sans Mono" })

[Patrick Johnson]

It was working nice so far with DejaVu Sans Mono, but today I saw the issue again. Is there an alternative font to fix this?

import tactic
structure A := (x : list ℕ)
example : nonempty A :=
begin
  let x : A := ⟨[]⟩,
  use x,
end

Screenshot

[Eric Rodriguez]

damn, and it seems that all those glyphs are dejavu sans mono as well, not a "backup" glyph :(

[Eric Wieser]

Did we decide this was a vscode issue or a WebKit/blink issue?

[Kevin Buzzard]

You can see it in the docs too, if this helps: brackets.png

[Eric Rodriguez]

yikes, we changed the font to avoid this exact thing happening

[Eric Rodriguez]

docs#zmod.units_equiv_coprime

[Eric Rodriguez]

image.png

[Eric Rodriguez]

interestingly, it's the character being too _small_; if you make it bigger using CSS stuff, the stuff works

[Patrick Massot]

I thought we got rid of this bug last year, but it indeed came back this year, punishing my students using windows.

[Patrick Johnson]

This resolves the issue for any font (the only problem is that some long expressions may not always span across multiple lines):

.expr > .expr-boundary { white-space: pre-wrap !important }
.expr-boundary span { white-space: pre !important }

Screenshot.png

[Alex J. Best]

@Patrick Johnson nice, I think we should add this to the tips and tricks page https://leanprover-community.github.io/tips_and_tricks.html, do you want to add it or shall I?
Is it the case that one can now use any font for the info view or is dejavu sans mono still best?

[Kevin Buzzard]

wait what? Can someone explain where I type this?

[Eric Rodriguez]

image.png

[Gabriel Ebner]

@Patrick Johnson Instead of the tips&tricks page could you please PR the change to doc-gen and the vscode extension? This is an honest bug, we should fix it for everyone.

[Kevin Buzzard]

css.png Wrong search, right?

[Eric Rodriguez]

yeah, in the settings UI

[Floris van Doorn]

Press ctrl+, and type in the resulting search bar

[Kevin Buzzard]

thanks

[Kevin Buzzard]

I'm still not 100% sure what I should be doing but if it's going to be fixed upstream maybe I'll just wait

[Patrick Johnson]

Instead of the tips&tricks page could you please PR the change to doc-gen and the vscode extension? This is an honest bug, we should fix it for everyone.

It's more like a workaround rather than a fix. With this patch, long expressions may sometimes overflow horizontally.

VS Code extension doesn't seem to be generating inline CSS attributes. That seems to happen in mathlib, in particular here. Only the outer-most expr-boundary should have pre-wrap, nested expressions should only be pre. Unfortunately, I can't test it, because compiling mathlib locally is out of reach for my machine. Please feel free to open PR yourself if you can make it work.

[Johan Commelin]

You can make the PR, push to github, wait for CI to compile, and then fetch the oleans using leanproject, right?

[Patrick Johnson]

Yes, but given that I'm not very familiar with meta programming in Lean, it may result in a very long chain of trial-and-error attempts, triggering many CI runs and taking a lot of time. It will definitely be easier for someone who already knows how stuff works.