Zulip Chat Archive

Stream: new members

Topic: leanproject get vs git clone

ZainAK283 (Jul 21 2020 at 17:15):

What's the difference between, say:
leanproject get lftcm2020
git clone git@github.com:leanprover-community/lftcm2020?

Kenny Lau (Jul 21 2020 at 17:18):

@ZainAK283 the former downloads the oleans (compiled lean files) as well

ZainAK283 (Jul 21 2020 at 17:19):

So in general I should do the former when possible?

Kenny Lau (Jul 21 2020 at 17:25):


Kevin Buzzard (Jul 21 2020 at 17:40):

The difference is that if you fire up VS Code afterwards and open a file in the repo, then you have a 1 hour wait if you used git clone, until the orange bars go away and Lean starts responding to keypresses.

Last updated: Dec 20 2023 at 11:08 UTC