Stream: general

Topic: WebAssembly on website

Heather Macbeth (Jul 07 2020 at 20:03):

@Patrick Massot Is there any way to edit the default Lean code that shows up in WebAssembly? At the moment it is the following:

-- Live WebAssembly version of Lean
#eval let v := lean.version in let s := lean.special_version_desc in string.join
["Lean (version ", v.1.repr, ".", v.2.1.repr, ".", v.2.2.repr, ", ",
if s ≠ "" then s ++ ", " else s, "commit ", (lean.githash.to_list.take 12).as_string, ")"]

example (m n : ℕ) : m + n = n + m :=
by simp [nat.add_comm]


I think the #eval statement (full of CS stuff like strings) could be rather forbidding for a brand-new mathematician user, especially with the 3-line green underline.

I mention it because the Lean community website has several prominent links to this page:

• on the homepage, this is one of the first links (text: "Try the online version of Lean")
• in the navigation bar, this is one of the first links (text: "Try it!"/"Lean online")

So this could be a lot of people's first encounter with Lean.

An alternative would be to change just those two links so that they lead to a special beginner file in WebAssembly, either the existing file with the #eval deleted or the first file of the tutorial project.

Patrick Massot (Jul 07 2020 at 20:04):

The answer is yes, but this is a question for @Bryan Gin-ge Chen

Patrick Massot (Jul 07 2020 at 20:04):

And I agree this doesn't look nice and welcoming.

Ruben Van de Velde (Jul 07 2020 at 20:06):

I think it may come from here: https://github.com/leanprover-community/lean-web-editor/blob/da9a3114bedf1825ae3f8d12d51e556a7db21c01/src/index.tsx#L738

Rob Lewis (Jul 07 2020 at 20:06):

I guess the very simple workaround is linking to https://leanprover-community.github.io/lean-web-editor/#code=%20 instead.

Rob Lewis (Jul 07 2020 at 20:07):

But yeah, I'd be happy to see the default changed.

That's cunning!

Heather Macbeth (Jul 07 2020 at 20:07):

I think that having something like the current example

example (m n : ℕ) : m + n = n + m :=
by simp [nat.add_comm]


is great, and more welcoming than the blank page.

Heather Macbeth (Jul 07 2020 at 20:08):

By the way, hello, @Ruben Van de Velde , and congratulations on doing that Hahn-Banach PR!

Rob Lewis (Jul 07 2020 at 20:08):

The url is a bit longer

Heather Macbeth (Jul 07 2020 at 20:09):

And, to workshop this even further, maybe a tactic mode proof would be more welcoming than a term mode proof ...

Bryan Gin-ge Chen (Jul 07 2020 at 20:10):

Sorry about that. The code there was just to help me debug things and I never bothered to switch it. I can change it to anything you guys want.

Patrick Massot (Jul 07 2020 at 20:11):

simp is a bit too much for nat.add_comm _ _

Patrick Massot (Jul 07 2020 at 20:12):

We can use nat.add_comm m n if we don't want it to look mysterious

Johan Commelin (Jul 07 2020 at 20:13):

How about the infinitute of primes proof as the default?

Rob Lewis (Jul 07 2020 at 20:13):

Bryan Gin-ge Chen said:

Sorry about that. The code there was just to help me debug things and I never bothered to switch it. I can change it to anything you guys want.

I've actually found it useful before since I don't know how often the web editor updates its Lean version :) but I'm sure I'm the odd one out there, hah.

Johan Commelin (Jul 07 2020 at 20:13):

(Not the mathlib scramble-golf... but a nice one.)

Patrick Massot (Jul 07 2020 at 20:15):

It would be nice but only if you can do it without too much imports since I guess that would slow down the webpage.

Heather Macbeth (Jul 07 2020 at 20:15):

Rob Lewis said:

I've actually found it useful before since I don't know how often the web editor updates its Lean version :) but I'm sure I'm the odd one out there, hah.

One could keep the default code the same, and change just those two links to something more beginner-friendly.


Heather Macbeth (Jul 07 2020 at 20:18):

I also think that the first file of the tutorial project is very beginner-friendly (as an alternative to the infinitude of primes); but a nearly blank page with just one or two short examples is also beginner-friendly.

Bryan Gin-ge Chen (Jul 07 2020 at 20:53):

Rob Lewis said:

I've actually found it useful before since I don't know how often the web editor updates its Lean version :) but I'm sure I'm the odd one out there, hah.

It's a little less direct, but you can also sort of check by clicking the purple (?) link and scrolling down to see the commits of the libraries that are included.

Mario Carneiro (Jul 07 2020 at 21:59):

Why not add a function to lean core that does what the #eval does? That way you can just write #eval lean.print_version or something to see that, and it doesn't have to go in the default code

Heather Macbeth (Jul 07 2020 at 22:00):

Good idea, and even if it were in the default code, it would not look forbidding.

Bryan Gin-ge Chen (Jul 07 2020 at 22:51):

Putting #eval lean.print_version in the default code wouldn't work for anyone using older versions of Lean. Of course, it would be fine for the community web editor, which is kept at the bleeding edge, but if we want to support multiple versions of Lean / multiple versions of mathlib in the future that will make it trickier.

I tested out the first file of the tutorial project and it takes around a minute to fully load on my laptop (and that's with all the resources already cached). Also, making edits to a file of that size in the web editor is much too laggy. I think something < 50 lines would be good, if anyone has any suggestions.

Heather Macbeth (Jul 07 2020 at 23:29):

Maybe something like this? Perhaps a slightly shorter-to-prove algebraic identity, if anyone has ideas.

import tactic.ring

/- Welcome to Lean!

Lean is a *proof assistant*.  It knows the axioms of standard mathematical objects such as ℤ :
-/
example (m : ℤ) :
(m - 1) * (m + 1) = m ^ 2 - 1 :=
calc (m - 1) * (m + 1)  = m * (m + 1) - 1 * (m + 1) : sub_mul _ _ _
... = m * (m + 1) - (m + 1)     : by rw one_mul
... = (m * m + m * 1) - (m + 1) : by rw mul_add
... = m * m + (m * 1 - (m + 1)) : add_sub_assoc _ _ _
... = m * m + (m - (m + 1))     : by rw mul_one
... = m^2 + (m - (m + 1))       : by rw ←pow_two
... = m^2 + (m - m - 1)         : by rw sub_add_eq_sub_sub
... = m^2 + (0 - 1)             : by rw sub_self
... = m^2 + (-1)                : by rw zero_sub
... = m^2 - 1                   : rfl

/- And it also has higher-level *tactics* to manipulate these axioms like a mathematican would. -/
example (m : ℤ) :
(m - 1) * (m + 1) = m ^ 2 - 1 :=
by ring


Yakov Pechersky (Jul 07 2020 at 23:33):

For ease of toying around with the example by the first-time-user, I'd add curly braces or use begin end. Otherwise, removing or adding lines will break the example as it is now

Bryan Gin-ge Chen (Jul 07 2020 at 23:37):

Do you mean begin and end around the calc block?

Bryan Gin-ge Chen (Jul 07 2020 at 23:38):

Removing or adding lines in the middle of proofs will break them regardless of whether they're wrapped in begin and end, right?

Yakov Pechersky (Jul 07 2020 at 23:40):

Yes, that's true, but I was thinking of something like

example (m : ℤ) :
(m - 1) * (m + 1) = m ^ 2 - 1 :=
begin
ring,
end


Yakov Pechersky (Jul 07 2020 at 23:41):

calc is super cool, but difficult to edit, because you have to also supply the statement you want to show.

Bryan Gin-ge Chen (Jul 07 2020 at 23:41):

Ah, OK. Sure, that makes sense.

Yakov Pechersky (Jul 07 2020 at 23:44):

Maybe have an in-between tactic style of

example (m : ℤ) :
(m - 1) * (m + 1) = m ^ 2 - 1 :=
begin
rw sub_mul,
rw one_mul,
rw mul_add,
rw add_sub_assoc,
rw mul_one,
rw pow_two,
rw sub_add_eq_sub_sub,
rw sub_self,
rw zero_sub,
refl
end


Yakov Pechersky (Jul 07 2020 at 23:45):

Which shows the user a simplified version of the calc proof, and this version is friendlier to scrolling through and seeing the goal change.

Bryan Gin-ge Chen (Jul 07 2020 at 23:49):

Sounds good. I might compress the rewrites to a single line using [ and ].

Bryan Gin-ge Chen (Jul 07 2020 at 23:50):

I'll add some comments too suggesting interesting places to put the cursor.

Yakov Pechersky (Jul 07 2020 at 23:51):

My inclination to have the rewrites on separate lines was the thought that a user would want to try their own rw ___. Having the rw in [ ] makes it more difficult to rearrange or insert, imo.

Bryan Gin-ge Chen (Jul 07 2020 at 23:55):

That's true. Though new users may have a hard time coming up with lemma names to use in rewrites.

Anyways, I'll wait for more explicit agreement. Any changes we decide on will be pretty easy to make and deploy, but I'd rather just do it once.

Mario Carneiro (Jul 08 2020 at 00:27):

Bryan Gin-ge Chen said:

Putting #eval lean.print_version in the default code wouldn't work for anyone using older versions of Lean. Of course, it would be fine for the community web editor, which is kept at the bleeding edge, but if we want to support multiple versions of Lean / multiple versions of mathlib in the future that will make it trickier.

An easy solution to that is

#eval lean.print_version -- warning: will not work on lean < 3.17


Mario Carneiro (Jul 08 2020 at 00:29):

If the community web editor will get a version picker in the future, then the code in the text box can also vary to match whatever is appropriate for that version. (It will probably not be necessary to include a #eval lean.version line in that case anyway since the version is stated in the picker.)

Gabriel Ebner (Jul 08 2020 at 07:07):

You can also do this:

#eval lean.version  -- doesn't look as pretty, but gets the information across


Last updated: May 11 2021 at 00:31 UTC