basic housekeeping question

Stream: new members

[Igor Khavkine]

I want to get a better idea of how to locally manage several Lean projects that all use Mathlib and work my way up to making a Mathlib PR. I installed Lean via VSCode on Linux, with any required command line tools available.

[Igor Khavkine]

I've so far created one Lean project in VSCode, which seems to have download an entire copy of Mathlib into the project directory. Suppose I will have created multiple distinct Lean project directories, which all would be using Mathlib. How do I install a copy of Mathlib that could be shared by all the different projects? Perhaps this is explained in standard documentation, but it's not so obvious to me where.

[Igor Khavkine]

Finally, I presume that to make a pull request I'd eventually need to locally clone the Mathlib git repository, create a new branch and make changes in it. How does one set up new Lean projects that use the local edited copy of Mathlib?

[Newell Jensen]

https://leanprover-community.github.io/contribute/index.html

[Newell Jensen]

That should help answer most of your questions. You can have multiple local branches for your different PRs from the single cloned Mathlib repository.

[Igor Khavkine]

Thanks. I've had a look at that. It doesn't answer the question of how not to download an entire copy of Mathlib for each new Lean project. I'm sure it's obvious once you know how. But at the moment I don't know how.

[Newell Jensen]

When you say Lean projects are meaning some other folder/directory outside of the repository directory?

[Igor Khavkine]

Yes. Say just one Lean file in a separate directory, which imports Mathlib and proves some other things.

[Newell Jensen]

AFAIK, in that regard you have to have an entire copy in that directory since the Lean/Mathlib/VScode "ecosystem" is very dependent on directory structure.

[Kyle Miller]

One way people work is to work on projects within mathlib. I have a folder in the Mathlib directory of my own files and experiments. This arrangement makes it easier to contribute things since you're already in mathlib.

[Igor Khavkine]

OK, so maybe I'm thinking about this wrong. What is the most common configuration?

Option A: One directory set up by VSCode (say AllLeanStuff/). Then individual proof projects are subdirectories (AllLeanStuff/proj1/, AllLeanStuff/proj2, ...). Then I can see how the copy of Mathlib downloaded by VSCode into AllLeanStuff/ is share by the other sub projects.

Option B: One directory where a copy of Mathlib is stored (say UneditedMathlib/), then separate directories that contain independent Lean projects (say proj1/, proj2/, ...) all of which import Mathlib by setting some path to UneditedMathlib/. In that case setting up an EdittedMathlib/ directory would allow proj1/, proj2/, ... to selectively choose one or the other copy of Mathlib by a setting some path.

[Igor Khavkine]

Option B is what I originally had in mind. But maybe that's not the standard workflow that people use.

[Igor Khavkine]

Kyle Miller said:

One way people work is to work on projects within mathlib. I have a folder in the Mathlib directory of my own files and experiments. This arrangement makes it easier to contribute things since you're already in mathlib.

Am I right in guessing that these files of your own are also tracked by git within the public Mathlib repository (maybe in a separate branch from the main one)?

[Eric Wieser]

Yes, but you could also keep them in a private fork if that's a concern

[Kyle Miller]

If the files are meant to eventually be contributed, yes, they're in a branch (maybe not public) and they're usually stored somewhere sensibly inside the Mathlib tree. If they're just one-off experiments, I might not track them with git, and I eventually delete them.

[Newell Jensen]

Igor Khavkine said:

Kyle Miller said:

One way people work is to work on projects within mathlib. I have a folder in the Mathlib directory of my own files and experiments. This arrangement makes it easier to contribute things since you're already in mathlib.

Am I right in guessing that these files of your own are also tracked by git within the public Mathlib repository (maybe in a separate branch from the main one)?

That is only if you push though, you can keep a local branch without having it tracked from upstream

[Igor Khavkine]

OK, thanks. That explains a bit what people do in practice.

[Kyle Miller]

I usually also have multiple copies of Mathlib cloned so I can do multiple incompatible things at once (I also contribute to Lean itself, so one of them uses a development version). I just waste disk space myself, but I know some contributors use git worktree to share the git database across multiple clones.

[Kyle Miller]

I haven't heard of anyone doing it, but maybe you could use git worktree to share the copy of mathlib between different Lean projects? You'd still have multiple copies of the cache in each mathlib's working tree though.

[Igor Khavkine]

Hmm, the one Lean project directory I have seems to have eaten up 4+GB. :thinking:

[Igor Khavkine]

I'll give it a shot setting up a cloned copy of Mathlib and play around with branches within it.

[Kyle Miller]

On my old laptop I use gitpod and let the fine people at gitpod worry about all the disk space I'm using, and on my desktop, I'm spoiled and have a very large hard drive.

[Newell Jensen]

Igor Khavkine said:

I'll give it a shot setting up a cloned copy of Mathlib and play around with branches within it.

Another thing to keep in mind as you switch between the local branches is that you will usually need to update with lake exe cache get since the snapshots between the branches most likely will be different if you updated Mathlib in between the different branch creations.