missing ppSpace for mathport?

Stream: mathlib4

[Jireh Loreaux]

@Mario Carneiro this is very minor, but I've noticed that convert (foo) gets translated as convert(foo) by mathport, and similarly filter_upwards [foo] with bar is translated as filter_upwards [foo]with bar. I assume this is a missing ppSpace somewhere? If so, where is the appropriate place to add it?

[Yury G. Kudryashov]

Two more whitespace bugs:

• rw h at h1⊢ (no space before ⊢)
• an line with several spaces after each calc block.

[Mario Carneiro]

I take it you haven't seen !4#4519 then :)

[Mario Carneiro]

I was planning to merge that immediately after the nightly bump PR, and incorporate them both in the next mathport bump

[Mario Carneiro]

Actually I'm not sure what you mean about calc @Yury G. Kudryashov , I think I saw some suboptimal spacing in calc but wasn't able to get it to look the way I want without a custom formatter. Currently I believe it shows as one of:

calc
  a = b := pf
  _ = c := pf

or

calc
  a
  _ = b := pf
  _ = c := pf

depending on which form of calc is being used

[Mario Carneiro]

I wanted to put the a on the same line as the calc token, but it's actually parsed as a term with an optional trailing := pf part (where if the proof is present then the term in question is a = b and if not it is a), so the common term prefix isn't actually common as far as pretty printing is concerned

[Yury G. Kudryashov]

There is a line with indentation and no other symbols right after each calc block.

[Yury G. Kudryashov]

E.g., line 88 in this file: https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Analysis/Calculus/ContDiff.lean

[Mario Carneiro]

lean4#2251

[Yaël Dillies]

I also noticed split at h.

[Mario Carneiro]

you can use this to test out the lean formatter:

import Lean
open Lean PrettyPrinter
def fmt (stx : CoreM Syntax) : CoreM Format := do PrettyPrinter.ppTerm ⟨← stx⟩

#eval fmt `(if c then do t else e)

[Mario Carneiro]

there were a lot of spacing bugs, I fixed about 200 issues across the board (core, aesop, std, mathlib). Please check if it hasn't already been fixed, or wait for it to make it into mathport