Weird behavior of get-c

Stream: general

[Bolton Bailey]

I was working with my mentee on mathlib and he was having trouble with orange bar hell. Something strange was happening that I haven't seen before: He merged master, ran leanproject get-c --rev origin/master, and restarted lean, but the orange bars didn't go away. Any idea what could cause this?

[Yaël Dillies]

That usually happens when you've modified a file early in the import tree. Can you make sure that didn't happen?

[Bolton Bailey]

Yeah, that's not the case

[Bolton Bailey]

We actually got it working by switching to the master branch, doing it all again, then switching back to the work branch

[Bolton Bailey]

But then we visited other files in the tree and it went back to orange

[Yaël Dillies]

Did he merge master or origin/master?

[Bolton Bailey]

origin/master

[Yaël Dillies]

And how far apart did you run the git merge and leanproject get-c commands? It might have very well happened that a commit landed in between.

[Bolton Bailey]

It was only a few minutes I think it didn't change in between

[Bolton Bailey]

Actually, nvm, seems like it did change

[Yaël Dillies]

That might be worth checking! A few minutes is largely enough.

[Yaël Dillies]

Ahah

[Kevin Buzzard]

That surely shouldn't matter: get-c will get the best possible cache. If you really want to diagnose you could just see which cache you got and then compare that commit with the commit you're working on and see if there are commits not covered by the cache.

[Yaël Dillies]

No, Kevin, not when you run it with the --rev attribute.

[Kevin Buzzard]

You should be running it with the "get me the best possible oleans" option, right?

[Yaël Dillies]

Agreed, but I don't even know what's the correct way to do this.

[Bolton Bailey]

I'm just confused because I always run get-m, but that didn't work for him

[Bolton Bailey]

Ok, it's working for him now, thanks Yael for the tip

[Bolton Bailey]

Kevin Buzzard said:

You should be running it with the "get me the best possible oleans" option, right?

Are you saying that if I just merge master to a branch with sorries in it, and run leanproject get-c, that it will fetch the oleans for the correct version of master? When I do this with get-m, I expect it to tell me it can't find the oleans.

[Mario Carneiro]

I think it will walk up the commit history until it finds one that has oleans. If there are multiple options then it shows both and you can pick

[Bolton Bailey]

Do I have to use the --fallback option?

[Kevin Buzzard]

get-m or get-c won't work just after a merge because the machines haven't had a chance to make your oleans yet. The correct thing to do is to not merge if you want to work! When you've finished working, merge and then commit, and then in a few hours' time get-c will work for you.

I'm saying that if you merge master to a branch with sorries then it is possible to use leanproject get-c to fetch oleans for the version of master which you just merged into your branch. However if you edited logic.basic or some other file high up then this won't do you any good.

If you're working on mathlib you should never use get-m, you should always use get-c.

[Mario Carneiro]

I miss up

[Bolton Bailey]

They won't make oleans at all, because there are sorrys and probably bugs that cause compilation to fail, right?

[Mario Carneiro]

pretty sure it still makes oleans if there are bugs

[Bolton Bailey]

Oh interesting

[Mario Carneiro]

at least, for all files upstream of the bugs (which is usually what you need to work on the bugs)

[Bolton Bailey]

Right, we're just working on a new file not imported by anything

[Bolton Bailey]

Still, what I want is to be able to pull work that Sean does and have it run, and if my oleans are from a different version of master, then it won't compile.

[Bolton Bailey]

What I want to be able to do is go to any of my branches and get the most recent ancestor of that commit that has oleans, and fetch those.

[Mario Carneiro]

If they aren't changing files high up the file hierarchy then you can pull files from them and not much will be invalidated

[Bolton Bailey]

But if I switch branches to work on another project of mine, my oleans will be different

[Mario Carneiro]

and keep in mind that there is no hard limit here; worst case scenario is you end up building a big chunk of mathlib on your computer

[Mario Carneiro]

when I have to go change logic.basic for a leaf file I'm working on, I just run lean --make my_file.lean and come back in 5 minutes

[Mario Carneiro]

you can use get-c to switch branches without losing oleans, that's the main purpose of it

[Eric Wieser]

The "walk the history" options only happen if you ask for them with --fallback

[Eric Wieser]

The default behavior is to walk the history to look for older caches, but not to actually download them

[Bolton Bailey]

Walking the history indeed seems like a nice feature. Is this newly added? I don't see it in my version of leanproject

(base) 3:00:00 mathlib #=# leanproject get-c -h
Usage: leanproject get-c [OPTIONS]

  Restore cached olean files.

Options:
  --force     Get cache even if the repository is dirty.
  --rev TEXT  A git sha.
  -h, --help  Show this message and exit.
(base) 3:01:03 mathlib #=# leanproject --version
leanproject, version 1.0.0
(base) 3:01:06 mathlib #=#

[Anne Baanen]

I think so, looks like version 1.1.0 was created the day after this feature was added (https://github.com/leanprover-community/mathlib-tools/pull/113)

[Bolton Bailey]

Mario Carneiro said:

pretty sure it still makes oleans if there are bugs

I was surprised when you told me this because I didn't think this was true. Sure enough, I'm working on my Complexity theory PR and when I run leanproject get-c, I get

(base) 17:56:21 mathlib #=# leanproject get-c
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/9c3228d4c16de2826a8229e36d805e3273d7178b.tar.xz to /Users/boltonbailey/.mathlib/9c3228d4c16de2826a8229e36d805e3273d7178b.tar.xz
Failed to fetch cached oleans

Am I missing something here?

[Bolton Bailey]

I guess the issue is that it's still building, it just shows up as an X on github. My bad

[Eric Rodriguez]

there was an azure issue recently, but it should be fixed. maybe try push an empty commit to trigger a rebuild?

[Bolton Bailey]

No, the issue is that it's still building, the X is just due to the fact that it failed the linter. So it shows as an "X" on github, despite the fact that the build is still going. I guess I thought it would show as a yellow dot until all the in progress tests were done.