leanproject pull

Stream: general

[Johan Commelin]

Should there be a leanproject pull that does git pull and leanproject get-mathlib-cache?
I see people getting confused by changed tomls and lots of breaking code because they use leanproject up.

[Yakov Pechersky]

What happens if it pulls, but the oleans haven't been uploaded yet?

[Johan Commelin]

I think that's unlikely to happen. If people only use leanproject up to bump mathlib, and then push. Then others can lp pull to see the results.

[Eric Wieser]

Isn't this what the git hooks that leanproject provides were meant to be for?

[Eric Wieser]

So that git pull gets the cache

[Eric Wieser]

But also so does git checkout some_old_branch_with_an_older_mathlib

[Kevin Buzzard]

I never use leanproject up because I don't really understand what it does. For the liquid project I always do git pull, leanproject get-m, leanproject build.

[Johan Commelin]

Eric Wieser said:

Isn't this what the git hooks that leanproject provides were meant to be for?

Probably, but maybe lp pull could still do the same thing?

[Patrick Massot]

I just added a pull command to leanproject because the combination git pull && leanproject get-mathlib-cache (orgit pull && leanproject get-cache when working on mathlib) is so common and requires some additional care when upstream bumps mathlib. Please upgrade your leanproject using pip install -U mathlibtools and report any issue.

[Johan Commelin]

I just tried this on LTE, and it seems to work flawlessly

$ lp pull
Pulling from origin
Looking for lean-liquid oleans for a80e1d714
  locally...
  Found local lean-liquid oleans
Located matching cache
Applying cache
  files extracted: 1721 [00:07, 244.17/s]

[Filippo A. E. Nuccio]

Works perfectly for me as well.

[Johan Commelin]

Hmm, I'm having trouble with this in LTE:

lean-liquid$ leanproject get-mathlib-cache
SHA b'fbc9e5e306b8cd0a8ecccdb759ca09f16c44af86' could not be resolved, git returned: b'fbc9e5e306b8cd0a8ecccdb759ca09f16c44af86 missing'

[Eric Wieser]

Hmm, I think there's a missing git fetch that I might have removed by accident

[Eric Wieser]

Probably because I thought it made no sense for get-cache. Clearly it makes sense for get-mathlib-cache

[Eric Wieser]

Can you run with --debug to get the full traceback?

[Johan Commelin]

@Eric Wieser sorry, I already did a cd _target/deps/mathlib and leanproject get-cache. Now the problem is no longer reproducible.

[Johan Commelin]

Probably after another mathlib bump I can post the debug trace.

[Johan Commelin]

@Eric Wieser This is not the output I am looking for, right?

lp get-mathlib-cache
Looking for lean-liquid oleans for 6ea816834
  locally...
  Found local lean-liquid oleans
Located matching cache
Applying cache
  files extracted: 1752 [00:07, 235.14/s]

I think it did what I intended: extracting 1752 files looks like it was working with mathlib oleans. But the output is talking about lean-liquid oleans. Is that a bug?

[Eric Wieser]

Oh whoops, that's a bug for sure!

[Eric Wieser]

I guess the project name is populated wrongly in get-mathlib-cache

[Eric Wieser]

https://github.com/leanprover-community/mathlib-tools/blob/89426c098138f2c1270f05eca59360354863fd25/mathlibtools/lib.py#L583 is the wrong line

[Eric Wieser]

self.name should be "mathlib"

[Floris van Doorn]

I just had the same error (ping)

[Eric Wieser]

https://github.com/leanprover-community/mathlib-tools/pull/119 fixes the bug in the message

[Eric Wieser]

CI fails on that PR, but it fails on master too (due to updates to mypy)

[Patrick Massot]

@Eric Wieser Do you know what changed in mypy?

[Eric Wieser]

No idea, it looks like it was already broken in the last commit you pushed. Presumably it just got cleverer and looks for things it didn't look for before

[Patrick Massot]

Too bad, it sounded like you had something precise in mind

[Patrick Massot]

I'll investigate

[Eric Wieser]

I had a quick look; maybe it's an upstream bug in GitPython?

[Eric Wieser]

https://github.com/gitpython-developers/GitPython/issues/1095

[Eric Wieser]

Previously it had no type information, now it seems to have incomplete ones

[Eric Wieser]

A better issue link is https://github.com/gitpython-developers/GitPython/issues/1349

[Eric Wieser]

At any rate, the fix is probably just to tell mypy to be quiet somehow

[Eric Wieser]

From the error log:

mathlibtools/git_helpers.py:5: error: Name "git.Commit" is not defined
mathlibtools/git_helpers.py:10: error: Name "git.Commit" is not defined
mathlibtools/git_helpers.py:58: error: Name "git.Commit" is not defined
mathlibtools/git_helpers.py:63: error: Module has no attribute "Commit"
mathlibtools/lib.py:429: error: Incompatible types in assignment (expression has type "None", variable has type "Repo")
mathlibtools/lib.py:673: error: Argument 1 to "Path" has incompatible type "Union[str, PathLike[Any], None]"; expected "Union[str, PathLike[str]]"
mathlibtools/lib.py:954: error: Unsupported right operand type for in ("Callable[[], IterableList[Head]]")

The first four and the last one are probably a bug in the upstream mypy stubs, the 5th is mypy being annoying because it now knows how to ask what type something is and can't deduce Optional[T] from if x then: y = z else y = None, the 6th looks like a mixture of an actual possible crash in a corner case we don't care about and some str/bytes stupidity, and the last one also looks like a bug

[Patrick Massot]

I can confirm I locally managed to go from zero error to errors with updating GitPython (without updating mypy)

[Eric Wieser]

Maybe we just pin gitpython for now?

[Patrick Massot]

No, I think I can fix things anyway.

[Patrick Massot]

There was one remaining weird failure, I gave up on that one.