creating git project

Stream: new members

[Jalex Stark]

This wonderful page https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md
has instructions on how to do 2 related tasks:

1. given some lean code on my computer, make it the kind of thing that has a package name and can depend on mathlib
2. given someone else's git repo, make a local copy of it on my computer that has the structure of 1

How do I take the output of process 1 and give it the structure required to be an input of process 2?

[Reid Barton]

I'm not sure I understand the question. Is the answer "put it on github"? Process 1 will create a git repository

[Jalex Stark]

Sure, that sounds like an answer. Do you have any advice on how to implement it?

[Kevin Buzzard]

Any question about git or GitHub can be answered using Google, in my experience. This is not Lean-specific, right?

[Johan Commelin]

@Jalex Stark Do you have an account on github?

[Johan Commelin]

That would be the first step.
After that, create a git repository in the account, but don't create a README or LICENSE, it should be completely empty.

[Johan Commelin]

Finally, github will show you instructions on how to link this github repo to an existing repo.

[Johan Commelin]

The output of your step (1) is already an existing repo. You can now link that to your repo on github.

[Enrico Borba]

I think the question is more about the directory structure of the git repo. What should that look like for packages that can be installed by leanpkg?

[Kevin Buzzard]

It should look like the sample project.