Copy & Paste of FPiL code

Stream: general

[Asei Inoue]

@David Thrane Christiansen

Since the transition to the verso version, copying and pasting FPiL (Functional Programming in Lean) code causes formatting issues. It would be great if you could make the code easier to copy.

[Asei Inoue]

this is a typical copy-paste result:

def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size :=
by


omega

    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      insertSorted (arr.swap i' i) ⟨i',
by

simp [*]
⟩

[David Thrane Christiansen]

Will do!

[Asei Inoue]

Thank you!!

[David Thrane Christiansen]

OK, a fix is deployed in Verso. I'm out of time to get it deployed in the books today, but I'll do it tomorrow. Thanks for pointing this out!

[Asei Inoue]

@David Thrane Christiansen

Thank you very much. I have one more request.

I feel that the syntax highlighting is somewhat insufficient for me:

• The highlighting is mostly in black and white, making it hard to read due to a lack of color.

• In particular, it's difficult to distinguish between comments and non-comment code.

• While it's understandable that commands introduced via macros may not be recognized as such, I would like to see proper highlighting at least for the standard Lean commands that are built into the language.

I apologize in advance if this is a difficult request.

[David Thrane Christiansen]

While it's true that there aren't presently colors in the highlighting, it does already distinguish the categories that you're asking for (with the exception of comments, which I'll look into soon). It uses boldface for keywords/atoms (e.g. if, #eval, def), italic for local bindings (function parameters, let-bindings, section variables), and upright normal-weight font for constants. What further distinctions are missing?

Unlike a regexp-based post-hoc solution, Verso's highlighted code uses Lean's understanding of the code. That means that the cases tactic is highlighted as a tactic name, while a local variable called cases is highlighted as a local variable, and it means that commands introduced by macros are indeed recognized as such.

[Asei Inoue]

What further distinctions are missing?

I liked how the previous mdbook version of FPiL made it easy to distinguish between code and prose. The colorful syntax highlighting made it clear, even from a distance, which parts were code. With Verso's code rendering, the background of the code blocks is transparent and the code itself is not colored, making it hard to tell them apart from the surrounding text. I feel this makes documents rendered with Verso harder to read.

I don't think differences like bold or italic fonts are very easy to notice. Using color allows for a wider range of syntactic elements to be distinguished, and I think it's also easier to perceive those differences.

Unlike a regexp-based post-hoc solution, Verso's highlighted code uses Lean's understanding of the code.

I didn't know Verso was that sophisticated. Sorry for not realizing that. Thank you for letting me know.

[Asei Inoue]

@David Thrane Christiansen (missing ping)

[David Thrane Christiansen]

Thanks for expanding on your experience. I've got one more follow-up question, just to make sure I work on the right problems: in your last message, it sounded like the biggest challenge was telling comments apart from other code, and to a lesser extent distinguishing keywords from other tokens. In this message, it sounds like it's telling code apart from the other text in the book. Have I misunderstood something?

[Arthur Paulino]

I want to second that using different colors for different language token kinds is better than using different typography styles. That's how I believe most of us have been reading code on several different programming platforms. Bold/boxed/italic styles could be reserved for code comments, since Lean comments are sensitive to markdown syntax (at least on VSCode).

[Asei Inoue]

@David Thrane Christiansen

Sorry if my opinion was unclear. Let me try to summarize it myself as follows:

1. I want it to be easy to distinguish between comments and non-comment parts within code.

2. I want there to be a clear stylistic difference between code blocks and prose.

3. When it comes to showing syntactic distinctions—such as keywords—within code, using font differences like bold or italic isn't very visually clear. Using color seems to be a better option.

[David Thrane Christiansen]

Out of curiosity, would you want the same for math mode?

[Asei Inoue]

@David Thrane Christiansen

I understand that "math mode" refers to TeX notation.
As for the TeX parts, I personally don’t feel they need to be colored differently from the rest.
Unlike code, I prefer that TeX expressions blend in naturally with the surrounding text.

It might seem inconsistent to treat code and mathematical expressions differently.
Even I’m not entirely sure why I feel this way.
However, code often needs to be copied for local execution, whereas mathematical expressions don’t usually have that use case.
Because of this, code needs to be more clearly distinguishable, and I also feel that, compared to math, code is harder to read when displayed without color.

[Yaël Dillies]

As your resident colorblind person, I must remind you that using color as a mean to carry syntactic information must be done parcimoniously. Grayscale is fine, however, for example code blocks could very feasibly be slightly grayed out

[David Thrane Christiansen]

One of the big reasons I haven't put lots of color on it yet is that any scheme needs to be widely accessible. Don't worry, there will always be redundant signalling of information beyond just color - the bold and italic aren't going away, though they may be augmented with color as well.

[David Thrane Christiansen]

Another challenging aspect of color scheme selection is that we need to be able to signal focus too (like "the proof state for the highlighted region looks like THIS" or "the syntax for anonymous functions extends out to the enclosing parentheses, as highlighted here:"), and these combinations need to have enough contrast and be accessible. That's why it's super valuable to hear concrete difficulties from a variety of people - thanks again @Asei Inoue and @Yaël Dillies

[Yaël Dillies]

In this regard, the doc-gen3 system we had for focus was amazing.
Excerpt from docs3#mul_assoc

[David Thrane Christiansen]

That is really great - I'd really like to get something like that in Verso. But it's different from writing a document that's directing the readers to look at a particular point in the code, and then highlighting it to attract attention.

[Yaël Dillies]

Oh I see! I thought the process was going the other way around, ie where the reader was trying to get more information from a specific part of the code

[David Thrane Christiansen]

Also important!

[Patrick Massot]

Couldn’t we get different CSS sheets for different people, with a dropdown menu somewhere to choose?