Zulip Chat Archive

Stream: new members

Topic: Updating leanproject

Dan Stanescu (Jul 19 2020 at 14:40):

The version of leanproject on my Mac seems to be deprecated. When trying leanproject get -b mathlib:test1 say, as per @Scott Morrison video on mathlib contributions, it returns: Error: no such option: -b (the same command works on a more recent Lean installation on a different machine though). This older leanproject also doesn't know about the --version option. Moreover, leanproject global-upgrade doesn't upgrade it. Nevertheless, I could happily do leanproject up and my mathlib dependencies are at 3.17.1. The question is, how do I update this version of leanproject itself?

Scott Morrison (Jul 19 2020 at 14:43):

What does leanproject --version say?

Sebastien Gouezel (Jul 19 2020 at 14:43):

Does pip install --upgrade mathlibtools work?

Scott Morrison (Jul 19 2020 at 14:43):

(Or perhaps pip3, depending on your python setup.)

Dan Stanescu (Jul 19 2020 at 14:51):

Scott Morrison said:

What does leanproject --version say?

Just as I said, 

leanproject --version
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try "leanproject -h" for help.

Error: no such option: --version

Dan Stanescu (Jul 19 2020 at 14:53):

Sebastien Gouezel said:

Does pip install --upgrade mathlibtools work?

Yes! This gives me version 0.0.9. Thank you!

Last updated: Dec 20 2023 at 11:08 UTC