degraded hover experience on #check

Stream: lean4

[Kevin Buzzard]

This is on 4.10.0-rc1.

theorem bar (P Q R : Nat) : P + Q + R = R + Q + P := by omega

#check bar -- can't work out associativity of `+` with hover in the infoview
#print bar -- no problem here

Inspecting the theorem statement by hovering in the infoview, I would expect to be able to see how the statement is being parsed, e.g. I would expect that hovering over both the +s in P + Q + R should tell me where the brackets are. This works with #print but it's not working for me with #check (either in VS Code or with the web editor). Are other people experiencing this? Is this expected?

[Kyle Miller]

Wow, that's not good, thanks for the report.

[Kyle Miller]

This should be fixed in lean4#4665

[Kyle Miller]

This turned out to have been around since 4.8.0, when a refactor accidentally made #check pretty print using the pp.tagAppFns option. This option is working as intended, but having it active during #check is not intended.