https://live.lean-lang.org/

Stream: general

[Joachim Breitner]

https://live.lean-lang.org/ is neat! How is is set up to contain possibly malicious code? I see that network doesn’t work, and that all file systems are ro from the point of view of the lean process. (run_cmd is quite neat for that :-D)

[Sebastian Ullrich]

See https://github.com/leanprover-community/lean4web/blob/main/server/bubblewrap.sh :) . There may be some extra FRO configuration on top

[Utensil Song]

It makes use of Bubblewrap which is a low-level unprivileged sandboxing tool. The security policies can be configured. Lean 4 Game uses the same technology with similar setup.

[Jason Rute]

I need to update my links. I see you already changed where the link for running block code in Zulip. The Lean community webpage Try it online link probably needs to change. Also do you plan to make the code in the Lean manual (and maybe similar documentation like TPIL and FPIL) runnable via this website? I see the manual code now has greyed out namespace Ex suggesting something like this.

[Sebastian Ullrich]

Unfortunately a hardcoded playground association seems to be one of many mdBook limitations /cc @David Thrane Christiansen

[David Thrane Christiansen]

I'm definitely thinking about the best way to do this in the short and long term, but there's not an immediate plan today

[Utensil Song]

A quick css hack to make https://live.lean-lang.org dark again in case anyone is also interested: https://gist.github.com/utensil/552f47cd687290c1131da0a79cc7dff9

I use it via https://github.com/openstyles/stylus/ .

It looks like this:

image.png

I've tried to cover obvious edge cases, but sure it's not exhaustive.

[Jon Eugster]

@Utensil Song Thank you for the dark theme template! I now added a dark mode setting to the editor. The change is already live at our test-playground: lean.math.hhu.de. I assume it will make its way to live.lean-lang.org too in the next update cycle.

[Utensil Song]

I just noticed that live.lean-lang.org can't copy-paste the full infoview into comment, it will drop anything involves types(maybe widgets), leaving only text, e.g.

image.png

[Jon Eugster]

Interesting. Seems somehow specific to error messages. I opened lean4web#13, as I might not have the time to look into it myself this week.

[Matt Diamond]

Is anyone else running into issues with live.lean-lang.org?

[Matt Diamond]

I'm seeing unknown package 'Mathlib' for some reason

[Jon Eugster]

indeed. I know @Joachim Breitner tried to update it today. Maybe the lake project isnt built properly?

meanwhile, lean.math.hhu.de works as an non-updated backup

[Joachim Breitner]

It seems the installation fell prey to

May 07 06:00:23 nixos gpwdr6h3z9wqx1m3pz6pimgdhspzan8x-update-leanproject[4009958]: Unfortunately, you have a broken Lean v4.8.0-rc1 installation.
May 07 06:00:23 nixos gpwdr6h3z9wqx1m3pz6pimgdhspzan8x-update-leanproject[4009958]: Please run `elan toolchain uninstall leanprover/lean4:v4.8.0-rc1` and try again.

Rekicking it.

[Joachim Breitner]

And now it rebuilds all of mathlib, as if the cache was broken by the change to batteries?
Nevermind, just lake’s confusing output

[Joachim Breitner]

Should be working again!

[Joachim Breitner]

(Same issue on loogle as well… :hammer_and_wrench: )

[Tyler Josephson ⚛️]

How much traffic can live.lean-lang.org handle? If I were to direct a class of say, 10, or 30, or 50 people to try the website all at once, would it be fine?

[Henrik Böving]

@Joachim Breitner what does the infra think^^

[Kim Morrison]

(My uninformed guess, going off my memory of previous iterations, is that 10 would be fine and 50 would be scary.)

[Jon Eugster]

You can also use lean.math.hhu.de simultaneously if you experience capacity limits, that's an identical clone. From my memory, the capacity there should be somewhere around 70+, but I havent really tested that, and that capacity is shared with (NN-)Game players. (and you might want to give me a heads-up if you depend on that being functioning at a specific time)

[Jon Eugster]

(almost identical clone. The available project like "nightly" or "duper demo" might differ)

[Utensil Song]

Jon Eugster said:

(almost identical clone. The available project like "nightly" or "duper demo" might differ)

Just noticed that DuperDemo is not working. It might need some update since the bump.

[Jon Eugster]

with "not working" you mean "working perfectly fine but still on v4.7.0", aren't you? Just updated it now to the newest Duper and hopefully fixed the auto-update script, thanks for the notice!

[Utensil Song]

Somehow what I was expriencing is it stuck at import Duper. Thanks for the bump and now it works!

[Jon Eugster]

Utensil Song said:

Somehow what I was expriencing is it stuck at import Duper. Thanks for the bump and now it works!

weird, it worked when I tried. But sometimes I get weird (lake/lean) errors that are fixed with reloading, and I never took the time to look into that...

[Shanghe Chen]

Hi is live.lean-lang.org considering add a share feature that shortens the url. Or any recommended url shortened service for this?

[Shanghe Chen]

Posting a raw url to the playground in zulip looks quite inconvenient and markdown link syntax sometimes failed to parse it like test

[Shanghe Chen]

Oh the above can be correctly parsed by the markdown syntax, a longer version that failed:

link%0A%20%20let%20h%3A%20Vector%20%CE%B1%20(n'%20%2B%20m%20%2B%201)%20%3D%20Vector%20%CE%B1%20(n'%20%2B%201%20%2B%20m)%20%3A%3D%20by%20simp%20%5BNat.add_assoc%2C%20Nat.add_comm%2C%20vector_eq%5D%0A%20%20let%20xy'%20%3A%3D%20cast%20h%20xy%0A%20%20exact%20xy'%0A%20%20)%0A%0Adef%20append%E2%82%81%20%7B%CE%B1%20%3A%20Type%20u%7D%20(x%20%3A%20Vector%20%CE%B1%20n)%20(y%20%3A%20Vector%20%CE%B1%20m)%20%3A%20Vector%20%CE%B1%20(n%2Bm)%20%3A%3D%0Amatch%20x%20with%0A%7C%20nil%20%3D%3E%20sorry%0A%7C%20cons%20h%20t%20%3D%3E%20sorry%0A%0Aend%20InductiveFamilies%0A）

[Ruben Van de Velde]

You can post the code between triple back ticks and get a link to l.l.o for free

[Bolton Bailey]

Like this (click the button in the corner)

namespace InductiveFamilies

inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons (a: α) {n : Nat} (b: Vector α n) : Vector α (n+1)

#check Vector.nil
#check Vector.cons 3 Vector.nil

#check Vector.recOn
-- Inductive_Families.Vector.recOn.{u_1, u} {α : Type u} {motive : (a : Nat) → Vector α a → Sort u_1} {a : Nat}
--   (t : Vector α a) (nil : motive 0 Vector.nil)
--   (cons : (a : α) → {n : Nat} → (a_1 : Vector α n) → motive n a_1 → motive (n + 1) (Vector.cons a a_1)) : motive a t

def length {α : Type u} (x : Vector α n) : Nat := n

theorem vector_eq (h : n = m) : Vector α n = Vector α m :=
congrArg (Vector α) h

def append {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
Vector.recOn (motive := fun (a : Nat) (b : Vector α a) => Vector α (a+m)) x
(by simp ; exact y)
(by
  intro a

[Shanghe Chen]

Yeah it works perfectly on the desktop environment. Thank you very much! In mobile phone I found the "load from zulip message" feature in l.l.o, although it’s no longer a "one click" thing.

[Jon Eugster]

as far as I know URL shortening usually means setting up a database that stores the pairs of shortened and original keys, which sounds like too much overhead. Adding a feature to integrate an external shortener seems more reasonable, if somebody feels like PRing that :)

On the other hand, the link above breaking sounds like a bug that should be fixed

[Shanghe Chen]

Yeah it is probably caused by some character like ' is not quoted in the url : https://live.lean-lang.org/#code=def%20a'%3A%3D1%0D%0Adef%20b'%3A%3D2 compares test

[Shanghe Chen]

Oh this works, the above code snippet not working is

namespace InductiveFamilies

inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons (a: α) {n : Nat} (b: Vector α n) : Vector α (n+1)

#check Vector.nil
#check Vector.cons 3 Vector.nil

#check Vector.recOn
-- Inductive_Families.Vector.recOn.{u_1, u} {α : Type u} {motive : (a : Nat) → Vector α a → Sort u_1} {a : Nat}
--   (t : Vector α a) (nil : motive 0 Vector.nil)
--   (cons : (a : α) → {n : Nat} → (a_1 : Vector α n) → motive n a_1 → motive (n + 1) (Vector.cons a a_1)) : motive a t

def length {α : Type u} (x : Vector α n) : Nat := n

theorem vector_eq (h : n = m) : Vector α n = Vector α m :=
congrArg (Vector α) h

def append {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
Vector.recOn (motive := fun (a : Nat) (b : Vector α a) => Vector α (a+m)) x
(by simp ; exact y)
(by
  intro a' n' x' xy'
  let xy := (Vector.cons a' xy')
  let h: Vector α (n' + m + 1) = Vector α (n' + 1 + m) := by simp [Nat.add_assoc, Nat.add_comm, vector_eq]
  let xy' := cast h xy
  exact xy'
  )

def append₁ {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
match x with
| nil => sorry
| cons h t => sorry

end InductiveFamilies

Cannot find a shorter example though

[Shanghe Chen]

Ah maybe it’s just too long for the markdown link syntax in zulip..

[Utensil Song]

Jon Eugster said:

as far as I know URL shortening usually means setting up a database that stores the pairs of shortened and original keys, which sounds like too much overhead. Adding a feature to integrate an external shortener seems more reasonable, if somebody feels like PRing that :smile:

In general, the potential information loss of a short url service is not a good thing.

Maybe a better way is to compress the code then convert to base64.

[Jon Eugster]

I think I once looked at compressing the lean code, and the results were really not that astonishing. Something like max. 20% shortage for long codes at the costs of overhead for short snippets.

[Jon Eugster]

Shanghe Chen said:

Ah maybe it’s just too long for the markdown link syntax in zulip..

I think its the character ) and for some reason the browser immediately turns %29 into ), so that seems like it's not as simple of a fix without changing the format, like using base64 as suggested. (which in turn might complicate how zulip messages link to the editor)

[Shanghe Chen]

Yeah it seems only that just zulip can’t handle it correctly. I tested some other markdown tools and it rendered without error. And the raw url can be opened correctly in the chrome browser too. Since I only used shortened url for temp sharing and I have got the above useful informations. It seems no necessary for any change :tada:

[Utensil Song]

Unfortunately, Zulip only supports url encoding for code.

[Max Nowak 🐉]

It would still be useful to have a database storage for a week, so that sharing a link in a presentation is easier. Alternatively, support some feature that grabs the code from a GitHub gist or other pastebin service, which is stored in the url?

[Eric Wieser]

I think that second feature exists?

[Jon Eugster]

indeed that's "Load" > "Load From URL" at the top

[Max Nowak 🐉]

OH! Wow I missed that, that's awesome.

[Shanghe Chen]

Hi I found that llo is also very nice using from a mobile phone. Using it in mobile env I find it is a little inconvenient for selecting text. Could it be possible with an option bringing the system panel rather than the vscode panel up? Using IOS in most editing environments if I hold touching the screen, the system panel with "paste/select/select all" shown and in llo the vscode command panel shown. Most of the time the vscode command panel works perfectly but not quite for selecting texts:

[Shanghe Chen]

RPReplay_Final1718943020.mp4

[Jon Eugster]

Thanks for the reminder. I was meaning to disable the context-menu on mobile at some point, as it doesn't seem to be working.

Generally, monaco doesn't have great mobile support, but you should add such bugs as issues on lean4web

[Shanghe Chen]

Thanks! Yeah sure i’ll add an issue on Github

[Mac Malone]

Joachim Breitner said:

Nevermind, just lake’s confusing output

Is there something here I could fix?

[Mac Malone]

(Oops. Just realized the message I replied to was older than I thought.)

[Joachim Breitner]

Indeed, output no longer confusing :-)

[Tyler Josephson ⚛️]

@Jon Eugster Thanks for suggesting http://lean.math.hhu.de/ as an alternative to https://live.lean-lang.org! My tweet kinda went viral and I have ... 311 people registered for Lean for Scientists and Engineers - 13 in person, 88 only wanting to check out the recording, and 210 indicating interest in joining the online class (so far!). If even half show up on 2024-07-09T13:00:00-04:00, that's >100 people. So ... I'm contemplating the situation - it may be reckless for me to tell people "just use this URL and try it!" I'll probably instead point to local Lean installation instructions first, and suggest using a website if they run into installation issues. What do y'all think?

[Jon Eugster]

When Kevin did a lecture of the same magnitude and mentioned NNG there, not even closely half of them opened the website simultaneously, so it was all fine. But that depends on your format.

Might not be the worst stress testing to see if it is a problem after all, the logs will give insight on whether the servers ran full or not.

However, if they do considerable amount of Lean, the experience with a local installation/gitpod might be nicer anyways (e.g. saving)

Anyways, I perso ally are offline until the 18th probably, but I'd be intersted to look at the logs afterwards

[Joachim Breitner]

Tylor, if you find a way to stress test the live instance ahead of time (but how? 100 volunteers here? Some scripts controlling the browser) so that we can get some estimates on the resource usage we can probably beef up the virtual machine temporarily as needed.

Or you book a (virtual) machine just for your own use, and deploy it there (happy to help with the deployment).

The hard part seems to be estimating the resources needed.

[Jon Eugster]

For stress-testing, I believe just having multiple tabs open in your browser already simulates it quite well. At least for me last time I tested the limiting factor was that every user needed some fix amount of RAM. (i.e. to load mathlib)

[Joachim Breitner]

    PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND
3274580 lean4web  20   0 5276380   3.7g   3.3g S   0.0   6.0   0:28.35 /lean/bin/lean --worker file:///project/mathlib-demo.lean
…
3274079 lean4web  20   0 4645544   3.5g   3.3g S   0.0   5.6   0:03.32 /lean/bin/lean --worker file:///project/mathlib-demo.lean
3266157 lean4web  20   0 1947740   1.5g  35684 S   0.0   2.3   0:17.57 lean --server
3274576 lean4web  20   0 2005080   1.4g  35492 S   0.0   2.3   0:16.17 lean --server

So assuming the SHR is the memory that’s shared between the processes, then that’s ~400MB for each worker, plus 1.5G for each server (the latter sounds a bit high, isn’t the server just coordinating things). But maybe this is a too naive reading of linux process usage.