Zulip Chat Archive

Stream: lean4

Topic: Lean 4 web editor


Alexander Bentkamp (Nov 03 2022 at 16:59):

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 (Nov 03 2022 at 17:42):

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

Alexander Bentkamp (Nov 03 2022 at 17:47):

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 (Nov 03 2022 at 17:47):

What machine are you running it on?

Alexander Bentkamp (Nov 03 2022 at 17:49):

8 cores, 20 GB memory

Gabriel Ebner (Nov 03 2022 at 17:50):

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

Alexander Bentkamp (Nov 03 2022 at 17:50):

Is memory the issue or CPU?

Gabriel Ebner (Nov 03 2022 at 17:51):

I'd be mostly worried about memory.

Alexander Bentkamp (Nov 03 2022 at 17:52):

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

Gabriel Ebner (Nov 03 2022 at 17:52):

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 (Nov 03 2022 at 17:52):

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

Gabriel Ebner (Nov 03 2022 at 17:53):

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 (Nov 03 2022 at 17:53):

Do you know if gVisor shares mmaped files across containers?

Alexander Bentkamp (Nov 03 2022 at 17:54):

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

Reid Barton (Nov 04 2022 at 07:21):

Can the mmap be shared between Lean processes?

Sebastian Ullrich (Nov 04 2022 at 08:40):

Yes!

Reid Barton (Nov 04 2022 at 10:37):

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 (Nov 04 2022 at 10:40):

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 (Nov 04 2022 at 20:01):

Something for lean 5 maybe

Alexander Bentkamp (Nov 15 2022 at 16:49):

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

Alexander Bentkamp (Nov 17 2022 at 09:56):

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 (Nov 17 2022 at 09:57):

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 (Nov 17 2022 at 09:58):

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

Eric Wieser (Nov 17 2022 at 09:58):

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

Mario Carneiro (Nov 17 2022 at 09:59):

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

Eric Wieser (Nov 17 2022 at 10:00):

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 (Nov 17 2022 at 10:00):

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

Alexander Bentkamp (Nov 17 2022 at 10:02):

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

Sebastian Ullrich (Nov 17 2022 at 10:18):

/cc @Leonardo de Moura @Sarah Smith

Scott Morrison (Nov 17 2022 at 11:43):

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 (Nov 17 2022 at 15:14):

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 (Nov 17 2022 at 23:03):

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 (Nov 22 2022 at 15:26):

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

Patrick Massot (Nov 22 2022 at 15:38):

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

Sebastian Ullrich (Nov 22 2022 at 15:42):

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

Scott Morrison (Nov 22 2022 at 23:55):

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

Scott Morrison (Nov 22 2022 at 23:59):

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 (Nov 23 2022 at 07:47):

@Scott Morrison Fixed!

Scott Morrison (Nov 30 2022 at 20:12):

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

Scott Morrison (Nov 30 2022 at 20:13):

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 (Nov 30 2022 at 21:02):

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

Alexander Bentkamp (Dec 01 2022 at 08:29):

@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 (Dec 01 2022 at 08:42):

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

Alexander Bentkamp (Dec 01 2022 at 08:50):

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

Alexander Bentkamp (Dec 01 2022 at 10:00):

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

Alexander Bentkamp (Dec 01 2022 at 10:06):

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

Kevin Buzzard (Dec 01 2022 at 10:16):

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 (Dec 01 2022 at 10:52):

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 (Dec 01 2022 at 11:17):

@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 (Dec 01 2022 at 11:26):

@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 (Dec 01 2022 at 12:35):

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 (Dec 01 2022 at 12:36):

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 (Dec 01 2022 at 12:37):

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 (Dec 01 2022 at 12:40):

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 (Dec 01 2022 at 12:40):

Sure

Alexander Bentkamp (Dec 05 2022 at 08:47):

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 (Dec 08 2022 at 15:27):

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 (Jan 03 2023 at 13:37):

The server seems not to be running any more

Wojciech Nawrocki (Jan 19 2023 at 16:31):

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 (Feb 10 2023 at 03:08):

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 (May 06 2023 at 06:42):

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

Jon Eugster (May 06 2023 at 07:01):

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 (May 06 2023 at 09:03):

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 (May 06 2023 at 16:00):

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 (May 06 2023 at 16:13):

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 (May 06 2023 at 16:38):

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 (May 06 2023 at 19:54):

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

Jon Eugster (May 06 2023 at 19:55):

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

Kevin Buzzard (May 07 2023 at 00:14):

NNG3 is open source and basically abandoned


Last updated: Dec 20 2023 at 11:08 UTC