Lean tutorial broken

Stream: general

[Ken Roe]

I need to give a one hour talk on Lean tomorrow. I was thinking of using the tutorial at https://leanprover.github.io/introduction_to_lean/. However, the interactive mode is broken. Is there another tutorial that I can use?

[Patrick Massot]

I used to have a small demo somewhere, let me search

[Mario Carneiro]

you could use the tutorial and use vscode or the newer web interface in another window

[Patrick Massot]

https://github.com/leanprover-community/mathlib/commit/bf36dd1e66d373c53666ca4579649f767955ed42

[Patrick Massot]

It's probably slightly out of date

[Patrick Massot]

And it's clearly math oriented

[Rob Lewis]

Are there particular lines that are broken? It seems to work fine for me in Chrome.

[Kevin Buzzard]

It's working for me in Firefox 66.0.3 on Ubuntu

[Jeremy Avigad]

Most of the stuff in "introduction to Lean" has been moved to the first two chapters of https://avigad.github.io/programming_in_lean/, and should be working there. (I'll finish revising it and declare it "done" over the summer, when the semester is over.)