Zulip Chat Archive

Stream: general

Topic: VS Code weird parentheses


Patrick Johnson (Jan 26 2022 at 18:53):

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 (Jan 26 2022 at 18:54):

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

Eric Rodriguez (Jan 26 2022 at 18:55):

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 (Mar 24 2022 at 19:00):

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 (Mar 24 2022 at 19:30):

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

Eric Wieser (Mar 24 2022 at 20:28):

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

Kevin Buzzard (Mar 24 2022 at 20:31):

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

Eric Rodriguez (Mar 24 2022 at 20:33):

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

Eric Rodriguez (Mar 24 2022 at 20:34):

docs#zmod.units_equiv_coprime

Eric Rodriguez (Mar 24 2022 at 20:40):

image.png

Eric Rodriguez (Mar 24 2022 at 20:40):

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

Patrick Massot (Mar 24 2022 at 20:47):

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

Patrick Johnson (Mar 25 2022 at 15:06):

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 (Mar 25 2022 at 15:21):

@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 (Mar 25 2022 at 15:24):

wait what? Can someone explain where I type this?

Eric Rodriguez (Mar 25 2022 at 15:24):

image.png

Gabriel Ebner (Mar 25 2022 at 15:25):

@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 (Mar 25 2022 at 15:26):

css.png Wrong search, right?

Eric Rodriguez (Mar 25 2022 at 15:26):

yeah, in the settings UI

Floris van Doorn (Mar 25 2022 at 15:26):

Press ctrl+, and type in the resulting search bar

Kevin Buzzard (Mar 25 2022 at 15:26):

thanks

Kevin Buzzard (Mar 25 2022 at 15:29):

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 (Mar 25 2022 at 21:01):

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 (Mar 26 2022 at 01:35):

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

Patrick Johnson (Mar 26 2022 at 10:30):

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.


Last updated: Dec 20 2023 at 11:08 UTC