Moving lecture notes to Lean 4

Stream: Lean for teaching

[Thorsten Altenkirch]

I am planning to move my lecture notes which are Lean 3 based to Lean 4 before the Autumn.

I am concerned because the lecture notes contain embedded lean code which runs in the browser. My impression is that web based lean 4 is server based (is this correct)? Can I just use web based lean 4 as I have been using lean 3 without having to set up a server?

Apart from this what are the main issues which I need to address?
Thanks a lot,
Thorsten

[Jon Eugster]

Yes you should be able to use it exactly the same way!

You will need to be online to use the web editor now but on the flip side, you can also use it on a toaster without any hardware restrictions.

[Thorsten Altenkirch]

Jon Eugster said:

Yes you should be able to use it exactly the same way!

You will need to be online to use the web editor now but on the flip side, you can also use it on a toaster without any hardware restrictions.

Have you got a link to the lean enabled toaster?

[Kevin Buzzard]

I had Lean running natively in emacs in an Ubuntu chroot on my rooted cheap Android phone in 2017, which was about as good as a toaster

[Kevin Buzzard]

Lean would certainly make it get petty hot, at least