Zulip Chat Archive

Stream: new members

Topic: creating git project


view this post on Zulip Jalex Stark (Mar 05 2020 at 23:50):

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?

view this post on Zulip Reid Barton (Mar 06 2020 at 05:29):

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

view this post on Zulip Jalex Stark (Mar 06 2020 at 06:43):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 07:04):

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

view this post on Zulip Johan Commelin (Mar 06 2020 at 07:45):

@Jalex Stark Do you have an account on github?

view this post on Zulip Johan Commelin (Mar 06 2020 at 07:46):

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.

view this post on Zulip Johan Commelin (Mar 06 2020 at 07:47):

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

view this post on Zulip Johan Commelin (Mar 06 2020 at 07:47):

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

view this post on Zulip Enrico Borba (Mar 06 2020 at 18:22):

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?

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:22):

It should look like the sample project.


Last updated: May 11 2021 at 13:22 UTC