Getting an existing Lean 3 project with leanproject

Stream: new members

[Jiekai]

Is there a way to check if leanproject get tutorials is successful?

[Jiekai]

When the get command fails after the tutorials directory is created, it would be nice if leanproject can detect it.

[Jiekai]

BTW in the mathlib-tools README, pip install . is used for dev.
Is there any difference between pip install . and pip install -e .?

[Yakov Pechersky]

pip install -e doesn’t put the package (as source code) in your site-packages, wherever that is, but rather adds the directory you're pointing to (in this case, the one you're in) to the pythonpath. So that means that if you edit the source at the directory you're in, those changes will be used whenever that package is imported.

[Jiekai]

info: downloading component 'lean'
 10.0 MiB /  10.0 MiB (100 %)   1.8 MiB/s ETA:   0 s
info: installing component 'lean'
configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.

What does the downloading component 'lean' part doing?

[Kevin Buzzard]

It's downloading the correct version of lean to be used in the tutorials