Including lean projects in other repos

Stream: new members

[Paul Rowe]

I have a GitHub repo that I share with some collaborators. I have recently formalized some of our work in Lean, and I would like to check the Lean sources into our shared repo. However, since leanproject new creates its own git repository, git won't let me add the directory. Will it work if I simply delete the git info in my project? I understand git submodules are a thing, but from what I have read, that doesn't seem to be what I want. For example, I would much prefer that updates to my Lean project resulted in updates to the larger repo (since there are no dependencies).

I would appreciate any advice for how to manage this.

[Julian Berman]

Your Lean work functions as you'd like already?

[Anne Baanen]

As far as Git is concerned, there is no issue. I don't know any part of leanproject that requires the files to sit directly in there, so I think you should be good to go.

[Julian Berman]

If so you don't need to use leanproject new, you can just put it in its current form into the repo -- if you already have a .git folder in it and you're willing to get rid of its commit history you can yeah get rid of it

[Paul Rowe]

Fantastic. That's what I was hoping to hear. The Lean files are currently stable, and I don't care about the commit history. I got thrown off by something I read saying that a Lean project always has a git repo as part of it. I was worried it would cause problems with the Lean.

[Paul Rowe]

Thanks to both of you. I love that I can get questions resolved so quickly in this community!

[Anne Baanen]

Paul Rowe said:

Fantastic. That's what I was hoping to hear. The Lean files are currently stable, and I don't care about the commit history. I got thrown off by something I read saying that a Lean project always has a git repo as part of it. I was worried it would cause problems with the Lean.

Perhaps that sentence should be completed with "has a git repo as part of it, unless you know what you're doing." :)

[Anne Baanen]

Paul Rowe said:

Thanks to both of you. I love that I can get questions resolved so quickly in this community!

You're welcome! I'm happy that my "procrastination" is helping others :)