Force explicit brackets in VS Code?

Stream: new members

[Stuart Presnell]

Is there a way to get VS Code to explicitly write all the brackets that it normally suppresses, e.g to write (a + b) - c rather than a + b - c?

[Yaël Dillies]

There should be some argument to set_option that does this.

[Stuart Presnell]

I've tried set_option pp. and looked through the autocomplete suggestions but nothing seems to be the thing I want. Is there documentation for set_option somewhere? (I didn't have much luck with a Google search for "mathlib set_option")

[Kyle Miller]

#help options

[Kevin Buzzard]

Wait! I think that what Yael means is "someone should write such code", not "such code already exists".

[Stuart Presnell]

Ah! That would explain why I couldn't find it! :)

[Kyle Miller]

It seems possible to implement without much difficulty. In lean/src/frontends/lean/pp.cpp there's a function add_paren_if_needed that could decide that they're always needed. There are other functions, too, that seem to decide whether to add parens, like pp_num, pp_notation_child, and maybe some things about pretty printing universe levels.

[Patrick Johnson]

I suggest that we do not include parentheses in function application. For example, f x y z should not be (((f x) y) z), but (f x y z) is fine. Otherwise, the output of pp.all will be even less readable than it is now.

[Patrick Massot]

I'm also interested in an option to force some more parentheses, for teaching purposes. I guess this doesn't require modifying cpp files. I think we can add it in tactic.interactive_expr. This has the advantage that anyone can use it in a project, it doesn't have to be in mathlib. This is what I do to use #5440 for teaching. I'd be very grateful if someone understanding the widget framework could show how to tun every a+b into (a+b) by modifying that file.

[Alex J. Best]

Ok its not what you really want or pretty but I just tried a quick experiment with a much more low-level feature, custom info view css:

• Open Vscode settings, go to "Lean: Info view style"
• Paste in

.expr-boundary:before {content: '(';} .expr-boundary:after { content: ')'; }

• close and re-open the info view and you get:
  Screen-Shot-2022-01-12-at-17.19.41.png
  

[Kyle Miller]

I have a reason to dig into the pretty printer for something else anyway -- seeing as there's more interest in a parens option, I'll create a lean PR for it. (Maybe I'll figure out how to do #5440, too, @Patrick Massot)

[Patrick Massot]

Thanks! What do you mean by "do #5440"? This PR already works perfectly. Do you mean adding a config option?

[Patrick Massot]

In the mean time I managed to do what I suggested except that I'm stuck at adding a config option.

[Patrick Massot]

I tried to hack tactic.is_trace_enabled_for but I can't get it to work

[Patrick Massot]

It's really a pain that adding options is not easy

[Kyle Miller]

Patrick Massot said:

Thanks! What do you mean by "do #5440"? This PR already works perfectly. Do you mean adding a config option?

I mean get it implemented directly in the pretty printer along with a configurable option

[Patrick Massot]

Nice

[Patrick Massot]

I would still be really interested in getting help with my option issue. Maybe @Rob Lewis could have a look? I put my file at https://gist.github.com/PatrickMassot/5700bded8c1536f4bd470df3852de6f2

[Patrick Massot]

The line that does nothing is 148

[Patrick Massot]

At the very bottom there an example that fails

[Patrick Massot]

Replacing line 148 by match tt with ... makes the example work

[Patrick Massot]

I'm not insisting on using a trace option, any way of having some sort of custom option would be good.

[Rob Lewis]

I have no idea about widgets. It seems like maybe it's reading options from a different environment or something

[Patrick Massot]

Thanks for trying. Maybe @Gabriel Ebner could help then?

[Patrick Massot]

I have another meta question for Rob. In the following code, is it possible to rewrite foo so that it looks like foo' (which doesn't work at all)?

import tactic.basic

namespace tactic.interactive
setup_tactic_parser
open tactic

meta def foo : tactic unit :=
do
   goal ← get_goal >>= infer_type,
   match goal with
   | (expr.pi n _ t b) := do trace "a", skip
   | _ := do trace "b"
   end

meta def foo' : tactic unit :=
do
   { `(∀ %%n : %%t, %%b) ← get_goal >>= infer_type,
     trace "a", skip } <|> do { trace "b", skip}
   end

end tactic.interactive

[Patrick Massot]

The motivation is first readability but also I'd like to have a more complicated pattern in my real use case.

[Gabriel Ebner]

Here you go: https://gist.github.com/gebner/87defe68efaac3de248d1f0639fcff2e

[Patrick Massot]

Thank you so much Gabriel!

[Patrick Massot]

Is tactic.get_bool_option the key thing I was missing?

[Julian Berman]

(Line 543 should say "1 goal" instead of "1 but")

[Gabriel Ebner]

I think that's French.

[Julian Berman]

Aha! TIL.

[Patrick Massot]

Oh yes, this is all for French speaking teaching

[Patrick Massot]

Having a tactic that switches this on is perfectly fine , but I'm still curious to know whether it could be done with a set_option

[Gabriel Ebner]

Patrick Massot said:

Is tactic.get_bool_option the key thing I was missing?

Trace options are kind of special, is_trace_enabled_for doesn't look at the options. I think get_bool_option `trace.parens ff would work as well (if you wanted to abuse the trace option).

[Gabriel Ebner]

set_option is hard because afair there is no way to register options from the Lean side.

[Patrick Massot]

But there is still declare_trace that sounded promising

[Gabriel Ebner]

I mean sure if you want set_option trace.parens true then that should work (declare_trace + get_bool_option).

[Patrick Massot]

Ok, I'll try for learning purposes but I'll probably keep the tactic anyway.

[Patrick Massot]

Julian, there are other teaching tweaks in this file. For instance the "goals accomplished message" is not only translated, it's also written bigger, because math is hard.

[Patrick Massot]

For the record: using the trace option does indeed work.

[Patrick Massot]

and we can have both: the trace option and the switching tactic.

[Patrick Massot]

Last question for Gabriel : is the if-then-else bool.tt ← tactic.get_bool_option `trace.parens ff | pure s, a normal trick? I was searching around stuff like when and gave up because I had other issues.

[Gabriel Ebner]

For the record, another option would be to add a checkbox in the goal view. This is not that complicated, see here for an example with a counter: https://github.com/leanprover-community/lean/blob/a8cf8a0c9ea19a633baeb3aa7e8d706b86c2c0f9/tests/lean/widget/widget2.lean

[Patrick Massot]

That would be really nice! Would you know how to make that persistent?

[Gabriel Ebner]

is the if-then-else bool.tt ← tactic.get_bool_option `trace.parens ff | pure s, a normal trick?

I think I used it pretty often in Lean 3, although not everyone liked it. In Lean 4 you can also use the slightly more readable if !(← getBoolOption `trace.parens) then return s.

[Patrick Massot]

I mean more persistent than the tactic state filtering.

[Kevin Buzzard]

...which we can't make persistent, right?

[Kevin Buzzard]

although around here you get the impression that anything can happen nowadays

[Gabriel Ebner]

Patrick Massot said:

That would be really nice! Would you know how to make that persistent?

Unfortunately that's just as impossible as the tactic state filtering.

[Patrick Massot]

Yes Kevin, that's why I was asking.

[Kevin Buzzard]

Lean 4?

[Patrick Massot]

Ritual question: Lean 4?

[Gabriel Ebner]

In Lean 4 all of this happens on the vscode/editor side. So: persistent tactic filters → super easy, I hope that Chris will do this soon; French localization → impossible from the Lean side, you'll need to PR it to the vscode extension.

[Gabriel Ebner]

(More parentheses → probably doable by adding a custom delaborator)

[Patrick Massot]

The impossible localization is bad news :sad:

[Patrick Massot]

I didn't know Chris is working on this. Which Chris do you mean btw?

[Gabriel Ebner]

Impossible to do from the Lean side, you can still customize the extension though (but I realize that this is organizationally much harder).

[Gabriel Ebner]

Chris Lovett.

[Patrick Massot]

It's dinner time. I need to go. Thanks again for all your help!

[Kyle Miller]

What do we think about this?

set_option pp.parens true

#check @nat.add_assoc
/- nat.add_assoc : ∀ (n m k : ℕ), (((n + m) + k) = (n + (m + k))) -/

example (x y z : ℕ) : x + y - z = x + y * z - y :=
begin
  /- ⊢ (((x + y) - z) = ((x + (y * z)) - y)) -/
end

example (f : ℕ → ℕ → ℕ) : f 2 (f 3 4 + 1) + 2 = f 1 2 :=
begin
  /- ⊢ ((f 2 (f 3 4 + 1) + 2) = f 1 2) -/
end

example (x y z : ℤ) : x - -3 = -2 + x :=
begin
  /- ⊢ ((x - (-3)) = ((-2) + x)) -/
end

(Ping: @Stuart Presnell)

[Kyle Miller]

The implementation is just to wrap anything that is notation in parentheses, which seemed to be the smallest modification I could do that would get this feature to work, without adding way too many parentheses.

[Kyle Miller]

To create a PR, should I push directly to the lean repository? Or can I do it from a fork? (This is my first lean PR, and I don't have write access.)

[Kyle Miller]

Diff: https://github.com/leanprover-community/lean/compare/master...kmill:kmill_pp_parens?expand=1

[Reid Barton]

Outermost parentheses seem superfluous, but otherwise it looks good!

[Stuart Presnell]

I agree that it would be nice to get rid of the outermost brackets, but otherwise this looks like just what I was hoping for!

[Patrick Massot]

Getting rid of outermost parentheses looks really hard, it requires a more global analysis. This output is also what you get with my implementation based on widgets.

[Kyle Miller]

I had also considered an approach where pp.parens overrides the precedences of notation to convince lean to add more parentheses, but I couldn't convince myself that it would always produce correct output.

[Kyle Miller]

Even if the outermost parentheses seem superfluous, at least there's this invariant that every notation has a corresponding set of parentheses wrapping it. All the examples above are equalities, so we see outermost ones.

In contrast, in this example there are no outermost parentheses so we know the top-level expression is not notation:

example (p : ℕ → ℕ → Prop) : p (1 + 2) 3 :=
begin
  /- ⊢ p (1 + 2) 3 -/
end

[Kyle Miller]

@Patrick Johnson Since you mentioned pp.all, what I learned looking through the source code is that, contrary to its name, it just overrides a handful of pretty printer options. Here's a complete list, for the curious:

• pp.implicit true
• pp.proofs true
• pp.coercions true
• pp.notation false
• pp.universes true
• pp.full_names true
• pp.beta false
• pp.numerals false
• pp.strings false
• pp.binder_types true
• pp.generalized_field_notation false

[Kevin Buzzard]

Oh wow, I had assumed that there was nothing between eg pp.proofs true and pp.all. I had no idea I had such fine control over output. This is surely helpful for debugging

[Mario Carneiro]

I will often use pp.implicit true and/or pp.notation false as a minimal set of options to see what I want (usually implicit typeclass arguments) without as much stuff as pp.all

[Kevin Buzzard]

Yes you've told me that before, but in situations where you need more I'd not realised that there are still many options available. I guess I'm yet to find out if this is useful in practice

[Alex J. Best]

@Kyle Miller, how feasible do you think a version of this option in lean 4?

[Kayla Thomas]

Did this become an option in Lean 4?

[Kyle Miller]

Not yet, but I was just looking into it the other day.

[Kayla Thomas]

Cool. Thank you.