Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: Totally lost

Roman Fedorov (Jul 15 2020 at 08:27):

I was just trying to get the file Floris was talking about in the morning session but I have not idea what he is talking about. He talks about "repository I cloned yesterday" but I did not clone anything yesterday. I tried "leanproject get tutorials" and it created a directory "tutorials" in my lean directory with an extra copy of mathlib. But it does not have the file Floris was working on... I am sorry for such stupid questions. Should I read a tutorial on git before proceeding?

Johan Commelin (Jul 15 2020 at 08:28):

@Roman Fedorov Sorry.

Johan Commelin (Jul 15 2020 at 08:28):

leanproject get lftcm2020 will get you started

Johan Commelin (Jul 15 2020 at 08:29):

You don't need to do the rest of his command

Johan Commelin (Jul 15 2020 at 08:30):

@Roman Fedorov Also, please join the Zoom session. Then a tutor can help you with further questions.

Roman Fedorov (Jul 15 2020 at 08:30):

Thanks!

Johan Commelin (Jul 15 2020 at 08:31):

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

Floris van Doorn (Jul 15 2020 at 13:14):

Ah, I forgot in my introduction that there would be people skipping the first two days!

Scott Morrison (Jul 15 2020 at 15:20):

btw --- LftCM is having some social time in the main Zoom room, if anyone wants to join

Last updated: Dec 20 2023 at 11:08 UTC