`lake init` create a default `.git` directory with potientially wrong defaults

[fredokun]

Using lake init or lake new creates a .git subdirectory with default options if none exists. However this doesn't work in a mono-repo situation, and moreover git init is very often used with extra options (e.g. default branch is most often main and not master in modern times). I would suggest at least making this enabled with an explicit (and configurable) option.

[tydeu]

Adding an Lake option for init/new that passes the option through to the Git CLI (ala -W for C compilers) is a good idea and would be nice to have. However, looking at the git init docs, there are not many relevant options for Lean project, so I consider this low priority.

As for the branch name, Lake would prefer projects have a single standard default branch as this makes it easier to perform version updates. I still don't object to making it configurable in the manner I mentioned, but it is also not high priority as a result.

[fredokun]

Fair enough, this is rather low priority (as a user) ... --template=<template_directory> is an option I personally use a lot. Also, please consider an option indicating not to create a .git subdirectory by default (imagine a monorepo with several lean packages inside, if you create the subpackage with lake new the .git of the subpackage will mess up with the main repo (this is exactly what happened in my case) ... You can also imagine someone using another VCS, perhaps a future one developed in LeanX.

[mik-jozef]

To me, more important than passing options to git is the option not to create a git repository at all.

And I believe this should be the default behavior as well. One reason is monorepos where the .git directory already exists in a parent folder (I got burned with this, as I had an existing repo and suddenly all my commits etc. disappeared). The other is that creating a git folder goes against (at least my) expectations -- it breaks separation of concerns, ignores the possibility one could use a different version control system, and is also inconsistent with at least one similar widely used tool -- npm init does no such thing.

[tydeu]

@mik-jozef

And I believe this should be the default behavior as well ,,, ignores the possibility one could use a different version control system, and is also inconsistent with at least one similar widely used tool -- npm init does no such thing.

Unfortunately, at the moment, the Lean/Lake package ecosystem is intimately tied with Git (and to some extent, GitHub). If the system diversified, I could definitely see this change, but until that happens I think the common setup is the appropriate default. Also, other well-regarded package managers, e.g. cargo, do initialize Git upon package creation as well.

[Ruben-VandeVelde]

A case came up on Zulip of someone who was (intentionally) creating a new package within an existing git repository, which caused some confusing issues. I think lake should detect this case and either warn or not initialize its own repository at all. For reference, cargo init has a --vcs flag:

--vcs vcs Initialize a new VCS repository for the given version control system (git, hg, pijul, or fossil) or do not initialize any version control at all (none). If not specified, defaults to git or the configuration value cargo-new.vcs, or none if already inside a VCS repository.

[haoxins]

I submitted a PR for this, only creating a new .git dir when not in the git work tree. https://github.com/leanprover/lean4/pull/5789 get the info by git rev-parse --is-inside-work-tree