## Stream: general

### Topic: git bisecting

#### Kevin Buzzard (Nov 09 2019 at 21:05):

I have heard people (e.g. Reid) talking about bisecting. I have a problem. The schemes repo was written by @Ramon Fernandez Mir and it compiled with June mathlib but doesn't compile with master right now. He is busy doing an MSc (in Amsterdam) and has offered to fix the code but I thought it might be nice to locate the commit of mathlib which broke the repo (and then get it compiling with that commit, and then repeating the process). The code seems very well-written to me and I'm hoping that isolating the breaking commits will make fixing things up easy.

The question: can I just type one command on the command line and then go to bed tonight, and wake up tomorrow with the output saying "it was this mathlib commit wot broke it"? I am envisaging just pulling a mathlib commit, running update-mathlib or just compiling the schemes repo with uncompiled mathlib, and then choosing another commit depending on whether the compilation returns 0 or not. I can't be the first person to be in this situation (or does everyone fix all their repos immediately after they break?)

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:10):

git bisect run xxx.sh is what you need

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:11):

you need to prepare a script first, let's call it compile.sh

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:11):

this compile.sh returns 0 if everything compiles, return non 0 otherwise.

#### Kevin Buzzard (Nov 09 2019 at 21:14):

Well that should be easy to write -- I hadn't realised it was going to be this easy. Sorry, I should have googled. Hmm wait though, I am a bit unclear about this. Mathlib is the upstream repo which broke my repo, so I should be running git bisect in _target/deps/mathlib? And should the script change the leanpkg.toml of my repo?

#### Kevin Buzzard (Nov 09 2019 at 21:15):

@Reid Barton do you do this sort of thing on a regular basis?

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:15):

sorry i forgot to mention git bisect start, git bisect bad and git bisect start, those are what you need to do before git bisect run compile.sh

#### Kevin Buzzard (Nov 09 2019 at 21:16):

But are these to solve problems of the form "my repo has stopped compiling, and I want to work out which commit broke it"?

#### Kevin Buzzard (Nov 09 2019 at 21:16):

My problem is "a dependency updated and this broke my repo"

#### Reid Barton (Nov 09 2019 at 21:16):

I have done it occasionally, but not in the context of a package using mathlib as a dependency. Rather I just have a standalone file (in my mathlib checkout) and I test whether it compiles after checking out each new version of mathlib.

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:17):

I need to think about it, but I think it is possible

#### Reid Barton (Nov 09 2019 at 21:17):

Though come to think of it, moving the contents of your package src/ alongside mathlib's src/ has a nonzero chance of just working

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:17):

I can even do if for you, and you can just sleep and wait for my result :)

#### Kevin Buzzard (Nov 09 2019 at 21:17):

I just had that very same dirty thought

#### Kevin Buzzard (Nov 09 2019 at 21:18):

Lemme try Reid's horrible approach first, it might work.

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:21):

and yes, I agree in this case you should run git bisect in a mathlib git repo, then run some commands to: 1. delete _target/deps/mathlib, 2. copy a new mathlib from the git repo to _target/deps/mathlib 3. compile again

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:22):

Reid's approach seems simpler, if you happen to be able to simplify your problem to a standalone minimal test case

#### Reid Barton (Nov 09 2019 at 21:23):

But if you use leanpkg build to build then it will go and check out the commit specified by the leanpkg.toml file. So if you try this approach be sure to run lean --make src directly

#### Kevin Buzzard (Nov 09 2019 at 21:27):

Will it be possible to massively save time by using cache-olean somehow?

#### Kevin Buzzard (Nov 09 2019 at 21:28):

The copying in from src seems safe to me, there are no duplicate file or directory names. I want to find out when src/instances/affine-scheme.lean stopped compiling, because this file compiles iff the repo compiles.

#### Reid Barton (Nov 09 2019 at 21:33):

Okay, then you can use git bisect with lean src/instances/affine-scheme.lean as the command to test

#### Kevin Buzzard (Nov 09 2019 at 21:33):

what will happen with the olean files? Do I just not worry?

Should be fine

#### Reid Barton (Nov 09 2019 at 21:35):

I don't know anything about using cache-olean

#### Kevin Buzzard (Nov 09 2019 at 21:37):

I'm going to go with something like lean -M6000 --make src/instances/affine-scheme.lean. Hmm, what is a minimum safe value for this? I don't want compilation to fail because of memory issues; conversely I don't want to freeze my machine.

#### Kevin Buzzard (Nov 09 2019 at 21:38):

oh this is great, I think hardly any of mathlib got compiled. Oh I think all my problems are solved, other than which commit broke the repo. Many thanks @Qian Hong (wechat: fracting) and @Reid Barton ! I'll be back in the morning complaining that my house burnt down.

#### Reid Barton (Nov 09 2019 at 21:39):

Yes, if you're lucky then you actually don't need to build much of mathlib and then it is much faster than you would otherwise expect.

#### Qian Hong (wechat: fracting) (Nov 09 2019 at 21:41):

And if you are unlucky, then there might be more than one commits broke the build, some of broken commits might be fixed by following commits, and then new broken commits introduced... In that case there is no guarantee git bisect can return the "right" broken commit you want

#### Kevin Buzzard (Nov 09 2019 at 21:43):

I'm sure it's broken for multiple reasons, I just thought it might be interesting to find the first place where it broke.

#### Reid Barton (Nov 09 2019 at 21:45):

You have no guarantee to find the first place, just some place

#### Kevin Buzzard (Nov 09 2019 at 21:45):

Let's assume that on no occasion did it break and then magically get fixed.

Last updated: May 17 2021 at 22:15 UTC