Zulip Chat Archive

Stream: new members

Topic: creating git project


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?

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

Jalex Stark (Mar 06 2020 at 06:43):

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

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?

Johan Commelin (Mar 06 2020 at 07:45):

@Jalex Stark Do you have an account on github?

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.

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.

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.

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?

Kevin Buzzard (Mar 06 2020 at 18:22):

It should look like the sample project.


Last updated: Dec 20 2023 at 11:08 UTC