Leanproject in another git repository

Stream: general

[Bolton Bailey]

leanproject new adds git tracking to the project it creates. But what if I want to create a lean project in a subdirectory within another preexisting git-tracked directory. Can I create a lean project with mathlib without this git being added?

[Alex J. Best]

git tracking is really just a .git folder with a bunch of files in it. I see no problems with making a leanproject new and then simply deleting the .git folder.

[Mike Shulman]

What if I want to create a lean project in the root of an existing git repository? leanproject new fails with fatal: A branch named 'master' already exists.

[Mike Shulman]

Also, if there is no problem with deleting the .git folder after creating a new lean project, why does leanproject initialize a git repository at all?

[Jason Rute]

I think leanpkg is the more low level tool. leanproject I think was designed as a higher level tool to accommodate the needs of most lean community users including automatically making git repos, downloading mathlib, etc.

[Kevin Buzzard]

I think that if you want to make a new project you need to type leanproject new name-of-project. It will then create a directory with that name and you should be fine.

[Mike Shulman]

I don't want it in a new directory, I want it in the current directory, which already has a git repository. leanproject new without another argument creates a project in the current directory, but it also tries to create a new git repository.

[Mike Shulman]

How do I use leanpkg to do everything that leanproject new does except create a git repository?

[Jason Rute]

I could be wrong, but I don’t think leanproject or the files it creates uses any global paths, so a simple workaround is to make a project elsewhere and move it to where you want. I haven’t tested though.

[Jason Rute]

yeah, leanproject probably needs a parameter to turn git off if it is going to complain like this.

[Jason Rute]

For what it is worth, I think, besides convenience to most users, this is the reason for making each lean project a git repo: https://leanprover-community.github.io/leanproject.html#git-hooks

[Jason Rute]

But I don’t know the motivation for sure.

[Eric Wieser]

Each project needs to be its own git repo because leanpkg.toml refers to projects by their git urls. So nothing can depend on your project if it's not at the root of the repo.

[Eric Wieser]

I'm referring to lines like:

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "de62604b58cf61aad9188a41aa7d9f51cfe73245"}

This syntax only works if the repo has leanpkg.toml in the root, and there can obviously be only one such toml file

[Eric Wieser]

You can of course ignore this advice if you don't intend to ever list your package as a dependency of something else (or expect anyone else to ever want to do so)

[Jason Rute]

@Eric Wieser I assume even if the project needs to be a repo, there shouldn’t in theory be a problem putting a lean project (with a git repo at the root of the lean project) inside a larger git repo, right? (I’m not sure the #xy of doing that, but that seems to be what the OP wants.) I assume the current leanproject new is just being too cautious, right?

[Eric Wieser]

That would be a git submodule if you have a repo within a repo

[Eric Wieser]

Which would be fine, but is unlikely to be what the OP wants

[Jason Rute]

Yeah, I didn’t think that through. I agree this isn’t what the OP wants.

[Eric Wieser]

But yes, leanproject new is just being cautious. You can totally copy its generated files to wherever you want them

[Eric Wieser]

Just make sure to put the lean project.toml into the root of the new repo if you want dependencies to work

[Mike Shulman]

Thanks everyone! I do think it would be useful to be able to separate the setup necessary for using Lean locally in a given directory from the setup necessary for sharing that code to other projects.

[Eric Wieser]

It's likely not really worth the effort of making the change since Lean4 has a different package structure. Note that even leanpkg initassumes you want a git respository.