Zulip Chat Archive

Stream: new members

Topic: Updating leanproject


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 19 2020 at 14:43):

What does leanproject --version say?

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 14:43):

Does pip install --upgrade mathlibtools work?

view this post on Zulip Scott Morrison (Jul 19 2020 at 14:43):

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

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 07:19 UTC