Lean 4 web editor

Stream: lean4

[Alexander Bentkamp]

I have worked a little more on a web editor for Lean 4. Here is how it looks like so far: https://adam.math.uni-duesseldorf.de/

It's still missing a few features, but it is pretty usable already. In contrast to the Lean3 web editor, it is running on a server since there are issues with compiling Lean 4 to web assembly. To secure the server, Lean is running in a gVisor container. The source code is here: https://github.com/hhu-adam/lean4web.

[Gabriel Ebner]

Have you tried how many users can use the editor simultaneously?

[Alexander Bentkamp]

I tried opening ten tabs, all busy with heavy computation, and it didn't seem to hurt very much. But I haven't tested where the limit is.

[Gabriel Ebner]

What machine are you running it on?

[Alexander Bentkamp]

8 cores, 20 GB memory

[Gabriel Ebner]

If you play your cards right, that might be enough for 100 simulateneous users.

[Alexander Bentkamp]

Is memory the issue or CPU?

[Gabriel Ebner]

I'd be mostly worried about memory.

[Alexander Bentkamp]

Ok, it might get worse with mathlib then, right?

[Gabriel Ebner]

If you've got too little CPU, then Lean will just become a bit slower. But if you've got too little memory, then you can't start Lean at all.

[Alexander Bentkamp]

I am afraid the server might even kill random processes at that point...

[Gabriel Ebner]

Alexander Bentkamp said:

Ok, it might get worse with mathlib then, right?

We're doing mmap now, so it should be much better than in Lean 3. But there's still a memory overhead proportional to the size of mathlib. The best thing would be to test it out.

[Gabriel Ebner]

Do you know if gVisor shares mmaped files across containers?

[Alexander Bentkamp]

no idea, this is my first time to hear about mmap :-)

[Reid Barton]

Can the mmap be shared between Lean processes?

[Sebastian Ullrich]

Yes!

[Reid Barton]

Nice, and then does Lean somehow avoid building in-memory data structures that are linear size in the amount of imports (e.g., the environment)?

[Sebastian Ullrich]

No, as Gabriel said it's still proportional. In particular, there's a hash map from imported constant names to their module and declaration. If Lean was module-based instead of namespaces-based, i.e. a declaration's full name unambiguously identified the module it comes from, this might have been avoided.

[Kevin Buzzard]

Something for lean 5 maybe

[Alexander Bentkamp]

We've moved it to https://lean.math.uni-duesseldorf.de

[Alexander Bentkamp]

I think the Lean4 web editor is ready to be released to the public now. Could you link to it from the community website? If you think that it's still missing something, let me know!
@Rob Lewis @Patrick Massot @Eric Wieser

[Eric Wieser]

I think adding a link to the lean4 web editor to the community website, which AFAIK contains only Lean 3 content, would be very confusing!

[Mario Carneiro]

well, we probably need to consider changing that at some point...

[Eric Wieser]

We certainly could do with a page mentioning Lean 4 and linking to the lean 4 website (and that editor)

[Mario Carneiro]

How about a new page for "lean 4 content" linked from the homepage and filled with TBD stuff about lean 4 / mathlib4?

[Eric Wieser]

But we already have enough confused new users who install things/find the web editor for Lean X and then run code intended for Lean (7-X).

[Eric Wieser]

We could probably do with inserting some 3s on the existing pages too

[Alexander Bentkamp]

I see, maybe https://github.com/leanprover/lean4 would be a better place then? @Sebastian Ullrich

[Sebastian Ullrich]

/cc @Leonardo de Moura @Sarah Smith

[Scott Morrison]

I think we should already be rewriting the leanprover-community webpage, explaining that we have a deprecated library based on Lean 3, and are busy porting to Lean 4.

[Jason Rute]

As precedent, during the Scala 2 to Scala 3 transition the website homepage reflected very clearly that there were two versions with different documentation, installation instructions, etc. https://user-images.githubusercontent.com/332812/145356305-6a759841-6a05-4260-86aa-50f9245e4422.png

[Eric Wieser]

There's the extra confusion for Lean that we have the leanprover-community vs leanprover distinction; it was really important for Lean 3 to steer people away from the really old Lean 3.4.2, but for Lean 4 we probably want to take advantage of all the nice documentation MSR is producing.

[Alexander Bentkamp]

We moved again, now with a shorter url: https://lean.math.hhu.de

[Patrick Massot]

Let me take the opportunity to mention this is really cool!

[Sebastian Ullrich]

With widget infoview even, hadn't noticed that before!

[Scott Morrison]

Shall we update the "view in playground" widget that shows up in Zulip, to send people here?

[Scott Morrison]

I turned it on, but URL unencoding is not working correctly. I don't think there's anything that can be done at the zulip end.

[Alexander Bentkamp]

@Scott Morrison Fixed!

[Scott Morrison]

Could we arrange so that this moves to the latest lean4-nightly at regular intervals?

[Scott Morrison]

Most days there is a bugfix relevant to mathlib4 porting. (I just tried out using the web interface and realised it was behind the nightly.)

[Arthur Paulino]

This is amazing! Great work.
Feature proposal: custom escaping character for inputting unicode

[Alexander Bentkamp]

@Scott Morrison Should we move it to the latest lean4-nightly or to the latest mathlib4? If we use the latest lean4-nightly, we might no longer be able to support importing mathlib... Or maybe there should be both variants available?

[Alexander Bentkamp]

@Arthur Paulino Thanks! I will look into the custom escaping character.

[Alexander Bentkamp]

For now, I've manually updated to the latest mathlib4

[Alexander Bentkamp]

@Arthur Paulino Ok, the unicode escape character can now be customized in the settings!

[Alexander Bentkamp]

I'd also like to move the project into https://github.com/leanprover-community if possible. Who manages that github organization?

[Kevin Buzzard]

Re whether to support mathlib or not: if a computer scientist wants to try lean 4 they can just follow the installation instructions. If a mathematician wants to try mathlib4 then they have to clone a repo which means learning about and installing git and possibly figuring out how to use the command line; these are things which are much more likely to be alien to them. So you get much greater gains by supporting mathlib4 because it's lowering the barrier far more, in some sense. We might want to consider also having some toy examples which users can select and play with. I always found the default lean 3 community web editor very intimidating; the start up screen is a bunch of CS stuff which I would always quickly delete if showing the editor off live to mathematicians.

[Patrick Massot]

Alexander Bentkamp said:

I'd also like to move the project into https://github.com/leanprover-community if possible. Who manages that github organization?

I'm sorry I didn't get back to you about that. We discussed it among maintainers but there is no super easy way to transfer the repo. We either need to temporarily make you an owner of the GitHub org or you need to temporarily make someone the owner of your repo.

[Alexander Bentkamp]

@Kevin Buzzard Right, I'll try to set up an automatic update to the latest Mathlib4. Do you have some toy examples that you'd like to see in there?

[Alexander Bentkamp]

@Patrick Massot No problem, I've made you admin of lean4web, lean4game, and duper. If I need to make somebody else admin, let me know.

[Patrick Massot]

I tried the move on https://github.com/leanprover-community/lean4game. @Alexander Bentkamp, you should have an invite to a leanprover-community/lean4web team which maintains that repo as well as a personal invitation as an admin of this repository. Once you'll have confirmed everything works nicely I'll do the same for the other two repos.

[Kevin Buzzard]

Alexander Bentkamp said:

Kevin Buzzard Right, I'll try to set up an automatic update to the latest Mathlib4. Do you have some toy examples that you'd like to see in there?

Here are some really dumb examples:

import Mathlib.Tactic.Ring -- import the `ring` tactic

-- let R be a commutative ring (for example the real numbers)
variable (R : Type) [CommRing R]

-- let x and y be elements of R
variable (x y : R)

-- then (x+y)*(x+2y)=x^2+3xy+2y^2

example : (x+y)*(x+2*y)=x^2+3*x*y+2*y^2 := by
  -- the `ring` tactic solves this goal automatically
  ring

import Mathlib.Data.Rat.Order -- import the rationals
import Mathlib.Data.Rat.Init -- import notation ℚ for rationals
import Mathlib.Tactic.Linarith -- a linear arithmetic tactic

-- let `x`, `y` and `z` be rationals
variable (x y z : ℚ)

-- let's prove that if `x < y` and `y + 3 < z + 10` then `x + 37 < z + 44`
example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by
  linarith -- the `linarith` tactic can do this automatically

-- let's prove that (x+y)^2=x^2+2*x*y+y^2

example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
  ring -- the `ring` tactic can do this automatically

import Mathlib.Logic.Equiv.Basic -- import the theory
-- of bijections as functions with two-sided inverses

-- Let X, Y and Z be sets
variable (X Y Z : Type)

-- Then there's a bijection between functions `X × Y → Z`
-- and functions from `X` to (the space of functions from `Y` to `Z`).

example : (X × Y → Z) ≃ (X → (Y → Z)) :=
{ -- to go from f : X × Y → Z to a function X → (Y → Z),
  -- send x and y to f(x,y)
  toFun := fun f ↦ (fun x y ↦ f (x,y))
  -- to go from g : X → (Y → Z) to a function X × Y → Z,
  -- send a pair p=(x,y) to (g p.1) (p.2) where p.i is the i'th element of p
  invFun := fun g ↦ (fun p ↦ g p.1 p.2)
  -- Here we prove that if f ↦ g ↦ f' then f' = f
  left_inv := by
    intro f -- let f : X × Y → Z be arbitrary.
    rfl -- turns out f' = f by definition
  -- here we prove that if g ↦ f ↦ g' then g' = g
  right_inv := by
    intro g -- let f : X → (Y → Z) by arbitrary
    rfl -- turns out that g' = g by definition
}

import Mathlib.Logic.Basic -- basic facts in logic
import Mathlib.Tactic.LibrarySearch -- a tactic which searches for
-- theorems in Lean's mathematics library

-- Let P and Q be true-false statements
variable (P Q : Prop)

-- The following is a basic result in logic
example : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q := by
  -- its proof is already in Lean's mathematics library
  exact not_and_or

-- Here is another basic result in logic
example : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by
  library_search -- we can search for the proof in the library
  -- we can also replace `library_search` with its output

@Patrick Massot you probably have opinions on what should be here and how these suggestions should be changed if indeed you think they're useful for beginners who just stumble upon the web editor and want to experiment. I could imagine me as a mathematically-interested teenager stumbling upon this site and seeing these examples and being really intrigued.

[Patrick Massot]

There isn't much we can do without a real mathlib4. At some point we will hopefully be able to translate https://github.com/leanprover-community/tutorials/blob/master/src/exercises/00_first_proofs.lean

[Kevin Buzzard]

I think that toy examples are what people want to see. Young people like to see brief immediate stuff. I agree that we can do much more ambitious things when we have such fundamental objects as the real numbers, but we already have enough for toy examples as my examples show, and I think that people like playing with toy examples, especially if they can play around and edit them, which they'll be able to do in the web editor.

[Patrick Massot]

Sure

[Alexander Bentkamp]

Thanks to @Wojciech Nawrocki , widgets now work in the web editor:
https://lean.math.hhu.de/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover%2Flean4%2Fmaster%2Fdoc%2Fexamples%2Fwidgets.lean

[Jon Eugster]

Scott Morrison said:

Could we arrange so that this moves to the latest lean4-nightly at regular intervals?

The web editor now tells you which mathlib4 commit / lean4-nightly it is at (it should update automatically every hour).

[Eric Wieser]

The server seems not to be running any more

[Wojciech Nawrocki]

I was seeing intermittent errors recently where bundle.js would fail to download with net::ERR_CONTENT_LENGTH_MISMATCH. It seems to be working again however.

[Jon Eugster]

I think that was the server running out of space due to some bad garbage collection which is fixed since then.

If you ping me (or Alex) next time there are problems, I'm not reading this stream too often

[Tchsurvives]

what is the current status of lean4 web editor? I would love to contribute if help is needed @Jon Eugster

[Jon Eugster]

https://lean.math.hhu.de is running and updating bihourly to the newest mathlib-compatible version, and it has been working fine for the last months.

I don't think anybody is working on getting WASM for lean 4 to work to run Lean in the browser itself, if anybody wants to gove it a shot. But that might be a hard task...

An easy task might be to make the interface mobile-compatible:thinking:

[Kevin Buzzard]

That as far as I'm concerned would be massive. People have often complained that they can't play NNG3 on mobile (it's unplayable)

[Jon Eugster]

We will certainly make the game mobile accessible eventually, but what the web editor is concerned, its not too high on my priority list, so if anybody got already some spare time now...

[Bulhwi Cha]

I'm also interested in making NNG4 run natively on computers and mobile devices. However, I wonder how many people will want native Lean games.

[Tchsurvives]

Jon Eugster said:

I don't think anybody is working on getting WASM for lean 4 to work to run Lean in the browser itself, if anybody wants to gove it a shot. But that might be a hard task...

An easy task might be to make the interface mobile-compatible:thinking:

It seems like my only complaint about it on mobile is the font size. are there any other major concerns?
also is there a NNG in lean4? i couldn't find the src of NNG3, is it open source?

hearing what @Wojciech Nawrocki said about WASM in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/web.20editor/near/281494817, I think it sounds beyond my skillset for now, unless things have changed since then?

[Jon Eugster]

https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Lean.20Game.20Server

[Jon Eugster]

Indeed, its just the font size, top-menu and some thought about display arrangement of editor and infoview

[Kevin Buzzard]

NNG3 is open source and basically abandoned