git bisecting

Stream: general

[Kevin Buzzard]

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)]

git bisect run xxx.sh is what you need

[Qian Hong (wechat: fracting)]

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

[Qian Hong (wechat: fracting)]

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

[Kevin Buzzard]

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]

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

[Qian Hong (wechat: fracting)]

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]

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]

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

[Reid Barton]

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)]

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

[Reid Barton]

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)]

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

[Kevin Buzzard]

I just had that very same dirty thought

[Kevin Buzzard]

(about moving src)

[Kevin Buzzard]

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

[Qian Hong (wechat: fracting)]

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)]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

Should be fine

[Reid Barton]

I don't know anything about using cache-olean

[Kevin Buzzard]

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]

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]

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)]

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]

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]

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

[Kevin Buzzard]

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