cache issues

Stream: new members

[Josha Dekker]

I'm trying to run 'lake exe cache get', but I keep getting weird errors. It thinks my checkout has diverged, how do I fix that?

(base) joshadekker@Joshas-MBP-2 mathlib4 % lake exe cache get
Warning: recommended `curl` version ≥7.81. Found 7.79.1
Attempting to download 22 file(s)
Downloaded: 0 file(s) [attempted 22/22 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 4059 file(s)
unpacked in 118 ms
(base) joshadekker@Joshas-MBP-2 mathlib4 %

[Josha Dekker]

same problem with 'get!' instead of 'get' by the way

[Kevin Buzzard]

Are you able to upgrade your curl? I'm on 7.81 and everything is working fine for me right now.

[Josha Dekker]

I'll have to find that out, I haven't done that before!

[Ruben Van de Velde]

And you're on a clean version of master?

[Josha Dekker]

I'm not sure, I probably have messed up somewhere...

[Kevin Buzzard]

What does git status report?

[Josha Dekker]

(base) joshadekker@Joshas-MBP-2 mathlib4 % git status
On branch JADekker_gamma_distribution
Your branch and 'origin/JADekker_gamma_distribution' have diverged,
and have 9 and 11 different commits each, respectively.
  (use "git pull" if you want to integrate the remote branch with yours)

nothing to commit, working tree clean
(base) joshadekker@Joshas-MBP-2 mathlib4 %

[Josha Dekker]

(base) joshadekker@Joshas-MBP-2 mathlib4 % git pull
hint: Diverging branches can't be fast-forwarded, you need to either:
hint:
hint:   git merge --no-ff
hint:
hint: or:
hint:
hint:   git rebase
hint:
hint: Disable this message with "git config advice.diverging false"
fatal: Not possible to fast-forward, aborting.

[Josha Dekker]

so something messy is going on, as this branch used to be on origin/master

[Kevin Buzzard]

OK so that explains it (don't worry about upgrading curl).

[Josha Dekker]

so how do I proceed? rebase to origin/master?

[Kevin Buzzard]

You or someone else seems to have pushed 11 commits to github which aren't on the machine you're using now, and you have pushed 9 different commits on the same branch to your machine.

[Kevin Buzzard]

How you proceed all depends on how to want to resolve that issue. Do you want all 20 of those commits on your branch? If so then just merge origin/JADekker_gamma_distribution into your local JADekker_gamma_distribution.

[Kevin Buzzard]

" this branch used to be on origin/master" doesn't make sense; your branch and origin/master are two different branches of the repo.

[Josha Dekker]

Okay, thank you! I'll try and figure it out!

[Josha Dekker]

I'm terribly messing things up with my local branch, I'm happy with how #9408 was at https://github.com/leanprover-community/mathlib4/pull/9408/commits/30e2d9bbc5963b936c94e27ac2edabf47a97a68f. Any way to just go back there/work from there again?

[Josha Dekker]

I clearly don't have a too good understanding of GIT...

[Josha Dekker]

I tried this, but that didn't work

(base) joshadekker@Joshas-MBP-2 mathlib4 % git switch JADekker_gamma_distribution
Switched to branch 'JADekker_gamma_distribution'
Your branch and 'origin/JADekker_gamma_distribution' have diverged,
and have 6 and 12 different commits each, respectively.
  (use "git pull" if you want to integrate the remote branch with yours)
(base) joshadekker@Joshas-MBP-2 mathlib4 % git switch origin/JADekker_gamma_distribution
fatal: a branch is expected, got remote branch 'origin/JADekker_gamma_distribution'
hint: If you want to detach HEAD at the commit, try again with the --detach option.
(base) joshadekker@Joshas-MBP-2 mathlib4 % git switch origin/JADekker_gamma_distribution
fatal: a branch is expected, got remote branch 'origin/JADekker_gamma_distribution'
hint: If you want to detach HEAD at the commit, try again with the --detach option.
(base) joshadekker@Joshas-MBP-2 mathlib4 %

[Mauricio Collares]

Do you mind if I force push to your branch? Previous head for the branch was e203bf7f19, in case we need it for some reason.

[Josha Dekker]

No problem!

[Josha Dekker]

I'm happy as long as it goes back to something like https://github.com/leanprover-community/mathlib4/pull/9408/commits/30e2d9bbc5963b936c94e27ac2edabf47a97a68f, and I can start working again!

[Mauricio Collares]

You'll have to run git fetch origin; git reset --hard origin/JADekker_gamma_distribution

[Ruben Van de Velde]

I suggest the following:

git checkout -b backup-JADekker_gamma_distribution
git checkout JADekker_gamma_distribution
git fetch origin
git reset --hard origin/JADekker_gamma_distribution

[Josha Dekker]

Mauricio Collares said:

You'll have to run git fetch origin; git reset --hard origin/JADekker_gamma_distribution

You're a life-saver! Thank you!

[Josha Dekker]

Ruben Van de Velde said:

I suggest the following:

git checkout -b backup-JADekker_gamma_distribution
git checkout JADekker_gamma_distribution
git fetch origin
git reset --hard origin/JADekker_gamma_distribution

so next time I mess up, I should run that block of code so no-one has to save me with a force push?

[Ruben Van de Velde]

Ask again next time, there's many ways to mess up with git :)

[Josha Dekker]

Thank you!

[Josha Dekker]

@Ruben Van de Velde Okay, so I tried your recommendation from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lifting.20real.20to.20complex/near/411186496, after which lake exe cache get stopped working, so I thought I'd run the above code snippet that you sent, but I think that I messed something up again...

[Josha Dekker]

(base) joshadekker@Joshas-MBP-2 mathlib4 % lake exe cache get!
Warning: recommended `curl` version ≥7.81. Found 7.79.1
Attempting to download 4080 file(s)
Downloaded: 2524 file(s) [attempted 4080/4080 = 100%] (61% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 2524 file(s)
unpacked in 1970 ms
(base) joshadekker@Joshas-MBP-2 mathlib4 % git checkout JADekker_filter_from_prop
git merge origin/master
git push origin JADekker_filter_from_prop
Already on 'JADekker_filter_from_prop'
Your branch is up to date with 'origin/JADekker_filter_from_prop'.
Already up to date.
Everything up-to-date
(base) joshadekker@Joshas-MBP-2 mathlib4 % git checkout -
b backup-JADekker_filter_from_prop
Switched to a new branch 'backup-JADekker_filter_from_prop'
(base) joshadekker@Joshas-MBP-2 mathlib4 % git checkout J
ADekker_filter_from_prop
Switched to branch 'JADekker_filter_from_prop'
Your branch is up to date with 'origin/JADekker_filter_from_prop'.
(base) joshadekker@Joshas-MBP-2 mathlib4 % git fetch orig
in
remote: Enumerating objects: 22, done.
remote: Counting objects: 100% (22/22), done.
remote: Compressing objects: 100% (8/8), done.
remote: Total 22 (delta 14), reused 16 (delta 14), pack-reused 0
Unpacking objects: 100% (22/22), 11.65 KiB | 350.00 KiB/s, done.
From https://github.com/leanprover-community/mathlib4
   d4fee1b64b..6ed900982a  destutter_coequiv -> origin/destutter_coequiv
   40d8eea9d6..f40d993303  put-sanity -> origin/put-sanity
   a32d5d9006..4362da572b  various-tidy-2 -> origin/various-tidy-2
(base) joshadekker@Joshas-MBP-2 mathlib4 % git reset --ha
rd origin/JADekker_gamma_distribution
HEAD is now at b8b8aa83f9 style : changed def to lemma
(base) joshadekker@Joshas-MBP-2 mathlib4 %

[Josha Dekker]

Screenshot-2024-01-04-at-14.23.02.png
Now it wants to do this

[Josha Dekker]

Screenshot-2024-01-04-at-14.23.46.png
But if I press that, it tells me this

[Josha Dekker]

I'm probably doing stuff that I shouldn't, how do I undo it?
Setting it back to
https://github.com/leanprover-community/mathlib4/pull/9200/commits/6cfec982e2f641177e3227083170c2025551c96a
or
https://github.com/leanprover-community/mathlib4/pull/9200/commits/4b8ab06bb53483fe8f21a887b7d427cc4dcf535f
would both be fine !

[Mauricio Collares]

The problem is in the very last step; you ran git reset --hard origin/JADekker_gamma_distribution instead of git reset --hard origin/JADekker_filter_from_prop. You can just run the correct version of the last command and it should fix your local files.