Zulip Chat Archive

Stream: general

Topic: update mathlib in project

Bernd Losert (Jan 17 2022 at 16:49):

I have a project using mathlib, but it is not up-to-date. How do I update it?

Floris van Doorn (Jan 17 2022 at 16:51):

You can use leanproject up to update the version of mathlib you're using to the latest version, and download the new mathlib binaries. Then you can build it with leanproject build, but you manually have to fix all the errors that now occur.

Bernd Losert (Jan 17 2022 at 16:52):

OK. Thanks.

Bernd Losert (Jan 17 2022 at 17:16):

Hmm... the version that it updated to seems to be about 10 days older than master. Is this normal?

Yaël Dillies (Jan 17 2022 at 17:17):

Did you fetch master before?

Yaël Dillies (Jan 17 2022 at 17:18):

Actually, I'm not sure that's related :thinking:

Bernd Losert (Jan 17 2022 at 17:26):

This is the first time I am updating.

Yaël Dillies (Jan 17 2022 at 17:29):

No, I meant fetch the branch master, because I suspect that's where leanproject gets its new mathlib version from.

Bernd Losert (Jan 17 2022 at 17:31):

This is what it did:

mathlib: trying to update _target/deps/mathlib to revision f684721dbec28322690f799b214b545b298d22ba
> git checkout --detach f684721dbec28322690f799b214b545b298d22ba    # in directory _target/deps/mathlib
HEAD is now at f684721db chore(data/nat/prime): `fact (2.prime)` (#10441)

Bernd Losert (Jan 17 2022 at 17:32):

How does it decide which commit to upgrade to?

Floris van Doorn (Jan 17 2022 at 18:26):

I think the first line of output printed after running leanproject up is wrong/misleading.
At least, I used leanproject up today, the first line of output was

mathlib: trying to update _target/deps/mathlib to revision 48fd9f2589e1bac31896a82d5989df892902179f

But then it fetched the remote version and later in the output it said

mathlib: trying to update _target/deps/mathlib to revision 391bd215c6b4807ea216e337a3b2737455605db0

It ended up in the latter commit 391bd215.
So you might have the newest version of mathlib after all. You could check using cd _target/deps/mathlib/ && git branch

Bernd Losert (Jan 17 2022 at 20:23):

Nope:

bernd@Bernds-MBP:~/Repositories/convergence/_target/deps/mathlib$ git branch
* (HEAD detached at dd1242d2a)
  master

Bernd Losert (Jan 17 2022 at 20:26):

Hmm... since it's using git, I might as well just switch it to master.

Yakov Pechersky (Jan 17 2022 at 23:27):

Leanproject will also handle getting the oleans. You'll have to make sure to do that too

Bernd Losert (Jan 18 2022 at 22:39):

I managed to get it upgraded. Here's what I did:

Copied https://github.com/leanprover-community/tutorials/blob/master/leanpkg.toml into my project.
Ran leanpkg upgrade.
Went to the _target/deps/mathlib and ran GIT_HISTORY_DEPTH=1 sh scripts/fetch_olean_cache.sh.

Alex J. Best (Jan 18 2022 at 22:54):

leanproject is the tool we use to automate these steps, I wouldn't really recommend doing this by hand unless you really have a reason to.
Have you seen https://leanprover-community.github.io/leanproject.html ?

Alex J. Best (Jan 18 2022 at 22:56):

You certainly need a toml file for lean to know what your project and its dependencies are, but leanpkg and the last step should be replaced by using leanproject

Bernd Losert (Jan 18 2022 at 23:06):

I did have leanproject before, but that python dependency caused me issues.

Arthur Paulino (Jan 18 2022 at 23:26):

Bernd Losert said:

I did have leanproject before, but that python dependency caused me issues.

What kind of issues? I've ran into Python issues myself before

Bernd Losert (Jan 19 2022 at 11:41):

I remember there were problems with the python version, since this machine has at least one python version installed allready. I did not want to deal with it and I realized leanpkg was enough to do what I needed, so I never bothered to fix it.

Arthur Paulino (Jan 19 2022 at 12:04):

Alright, just what I suspected.
You can try installing miniconda, which is a Python environment manager.

Btw, installing miniconda could be recommended in the tutorial page if the user already has Python 2 installed and it is the default Python for system calls. What do you guys think?

Arthur Paulino (Jan 19 2022 at 12:06):

@Bernd Losert what does $ python --version say?

Bernd Losert (Jan 19 2022 at 12:25):

It says Python 2.7.18.

Julian Berman (Jan 19 2022 at 12:54):

You're on macOS it seems? Just brew install mathlibtools should be all you need

Eric Rodriguez (Jan 19 2022 at 13:01):

it's so annoying that apple still has python2 things :/

Julian Berman (Jan 19 2022 at 13:41):

Exposing system python on all OSes was a mistake. When Lean gets super popular and OSes start using it to ship verified portions of themselves make sure we don't let them put it on PATH :P

Last updated: Dec 20 2023 at 11:08 UTC