branches/different versions of lean...

Stream: new members

[Pietro Lavino]

I am in the process of trying to commit to Mathlib 4 in a specific branch my professors gave me access to, so I created a local branch connected to the remote one in a directory in my computer along a main branch. I was then encountering issues as whenever I was switching between the two branches within vs code the .lean file I was running the code on would have each time to be rebuilt. I then figured out I had to be because the two branches the local main and the local one associated with the remote one in Mathlib were running different versions of lean. I hence updated lean on my local main branch to match. but now the .lean file seems to not work on either of the branches because it was written with lean 4.8 while now both branches are in leanprover/lean4:v4.9.0-rc1. what should I do? Thank you

[Kevin Buzzard]

Is your professor also a mathlib maintainer? If not then your claim that your professor gave you push access to a specific branch of mathlib is suspicious. Or are you talking about a fork which your professor made?

Whatever this remote copy of mathlib is, if you make a local clone of that copy then by definition you'll be using the same version of lean (and of mathlib) as the copy, and if you're a beginner then it's very unlikely that you're being asked to change either which version of lean or of mathlib that you're using in your code. So I'm confused about how you even ended up in a situation where you have two different versions of Lean on the go.

[Pietro Lavino]

Yeah it was fork as you said. The different version of lean came up as I cloned the repository into another preexisting one which created some issues.

[Kevin Buzzard]

yeah, you're better off just cloning the entire repo. No two versions of mathlib are exactly alike, they're like snowflakes, there are hundreds of them with new versions appearing every day and they're all incompatible with each other.