Zulip Chat Archive

Stream: new members

Topic: Getting an existing Lean 3 project with leanproject


Jiekai (Jul 12 2021 at 02:40):

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

Jiekai (Jul 12 2021 at 02:43):

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

Jiekai (Jul 12 2021 at 02:50):

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 (Jul 12 2021 at 03:07):

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 (Jul 12 2021 at 03:20):

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 (Jul 12 2021 at 09:00):

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


Last updated: Dec 20 2023 at 11:08 UTC