WebAssembly on website

Stream: general

[Heather Macbeth]

@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]

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

[Patrick Massot]

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

[Ruben Van de Velde]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Patrick Massot]

That's cunning!

[Heather Macbeth]

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]

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

[Rob Lewis]

The url is a bit longer

[Heather Macbeth]

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

[Bryan Gin-ge Chen]

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]

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

[Patrick Massot]

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

[Johan Commelin]

How about the infinitute of primes proof as the default?

[Rob Lewis]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

Do you mean begin and end around the calc block?

[Bryan Gin-ge Chen]

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]

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]

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

[Bryan Gin-ge Chen]

Ah, OK. Sure, that makes sense.

[Yakov Pechersky]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Yakov Pechersky]

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]

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]

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]

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]

You can also do this:

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