Lean Live bug? "expected type" folded by default

Stream: general

[Kenny Lau]

example : 37 = 57 := by sorry

Open the above code in Lean Live, and put your cursor before 57, and notice that the "Expected Type" info is folded by default:

image.png

Is this intended?

[Aaron Liu]

I don't like it, but I saw some discussion before and my impression is that it's intended

[Patrick Massot]

That’s 100% intended. Kenny, there is a tension here because Lean4web has several incompatible use cases.

One extreme case is people who want to take a look at Lean without installing anything on their computer. Those are total beginners, they may even feel that installing git is complicated (see another thread in this channel). For them, the expected type panel is extremely confusing.

The other extreme is expert users who come here on Zulip to help people. They follow the link from code blocks and land in live-lean where they want to see all the complexity to debug problems.

Now Lean4web needs to choose a default value and the answer is pretty obvious: we pick the beginner friendly value.

[Patrick Massot]

However this is not the end of the story. If you want to help, you can expose a setting to do that. There are two levels: the settings dialog you get in the Lean4web menu and the url scheme. This simply need some work. If the current situation bothers you enough, you can contribute this.

[Patrick Massot]

https://github.com/leanprover-community/lean4web/commit/8b3e3c8dde9397be59db4ec203b00f514e91119d is an example exposing a setting to the menu.

[Patrick Massot]

https://github.com/leanprover-community/lean4web/commit/8c690f4c89fd83b08d1dda9a35b9f8253c64523f is an example allowing to set something through the url.

[Patrick Massot]

The first option (adding a settings to the settings dialog) seems really easy, and then you can tell your browser to remember your settings (there is a setting for this!).

[Mario Carneiro]

Patrick Massot said:

That’s 100% intended. Kenny, there is a tension here because Lean4web has several incompatible use cases.

...

Now Lean4web needs to choose a default value and the answer is pretty obvious: we pick the beginner friendly value.

I think it is weird that lean4web and the default lean installation have different opinions about what the beginner friendly value is

[Yaël Dillies]

I agree with Mario here: Why is hiding the expected type beginner-friendly?

[Mario Carneiro]

I'm not even disagreeing with this point, I'm just saying it's some kind of dysfunction that different parts of the intial experience are disagreeing about what the ideal initial experience is

[Mario Carneiro]

maybe there is a case to be made for hiding the expected type, but I would like that case to be made upstream on the extension