installation videos!

Stream: general

[Scott Morrison]

Hi everyone, in preparation for Lean for the Curious Mathematician next week, @Patrick Massot, @Johan Commelin and I have made some videos about setting up Lean. (Thanks also to those who've already reviewed these videos, and especially to @Anne Baanen for the new macos install procedure.)

There's a playlist, or you can jump to individual videos:

• Overview of the Lean software ecosystem
• Installing the Lean theorem prover (macos)
• Installing the Lean theorem prover (ubuntu)
• Installing the Lean theorem prover (windows)
• Working with Lean projects
• Making a pull request to mathlib

Feedback, suggestions, or requests for further videos welcome. It would be great to get any remaining bugs sorted out by Monday morning!

[Bryan Gin-ge Chen]

When I visit the playlist link I see a deleted video and two copies of "the Leanprover ecosystem" (as well as the rest of the videos).

ytss.png

[Patrick Massot]

Are you logged in as the Lean community?

[Bryan Gin-ge Chen]

No, I even visited in a private window.

[Patrick Massot]

Then we may need someone who knows about Youtube from the author side.

[Bryan Gin-ge Chen]

I think someone who can login as leanprover community should be able to edit the playlist.

[Patrick Massot]

I think I fixed it

[Kevin Buzzard]

I had a random Xena playlist showing two deleted videos the other day -- there is some kind of weirdness I don't understand properly. I wondered whether it was because I cancelled an upload at some point.

[Bryan Gin-ge Chen]

Looks good now, thanks!