Sup is not longer Sup

Stream: mathlib4

[Patrick Massot]

What happened to Sup? In Lean 3:

import data.real.basic

variable (s : set ℝ)
#check Sup s -- ℝ

In Lean 4:

import Mathlib.Data.Real.Basic

variable (s : Set ℝ)
#check Sup s -- Type

[Patrick Massot]

Oh Sup is now the typeclass!

[Patrick Massot]

But mathport clearly doesn't know about this.

[Patrick Massot]

Although there is a #align has_Sup.Sup SupSet.sSup line :man_shrugging:

[Eric Wieser]

Mathport doesn't know that Sup is has_Sup.Sup, I think

[Patrick Massot]

I see

/-- Class for the `sSup` operator -/
class SupSet (α : Type*) where
  sSup : Set α → α
#align has_Sup SupSet
#align has_Sup.Sup SupSet.sSup

[Eric Wieser]

I think the export command in Lean3 is too hard for mathport to accurately understand

[Patrick Massot]

I guess improving mathport is no longer worth the trouble.

[Mario Carneiro]

mathport is not EOL yet

[Mario Carneiro]

but namespaces / name resolution has always been hard for mathport

[Patrick Massot]

What about the fact that it produced

theorem ρ_eq_one {x : ℝ} : ρ x = 1 ↔ x ≤ 1 / 2 := by rw [ρ, projI_eq_one];
  constructor <;> intros <;> linarith

that needs to be fixed to

theorem ρ_eq_one {x : ℝ} : ρ x = 1 ↔ x ≤ 1 / 2 := by
  rw [ρ, projI_eq_one]
  constructor <;> intros <;> linarith

[Mario Carneiro]

keep in mind that most mathport formatting bugs are actually formatter formatting bugs and occur just as much to pretty printed exprs and any future code-writing tools like source formatters or code actions

[Mario Carneiro]

yes I am aware of this issue, I wrote the code with the bug in it and there is a long comment in the lean core PR explaining why it's hard to do better

[Mario Carneiro]

(in short, when deciding whether to use one line or a new line it doesn't have the context to know whether it will overflow the line)

[Mario Carneiro]

so it uses the heuristic that if you used semicolons between every tactic then you want it on one line