Correct sequence to create a Githubable Lean project

Stream: new members

[Lars Ericson]

I created a repository for my Lean files on GitHub.

I cloned my repository to a directory on my Ubuntu computer.

I CD'd to the directory and ran code on a file. There was no Lean there.

I then ran leanproject new in the directory.

Now I can't commit to my original GitHub. I think it think's it is mathlib. It is giving me this message after I do a git push:

fatal: The current branch master has no upstream branch.
To push the current branch and set the remote as upstream, use

    git push --set-upstream origin master

What is the right way to set up my own repository of Lean files and work with it in such a way that commits to it don't try to commit to mathlib?

Also, look at [the docs](), what is an "oleans" file?

I can relocate my set of .lean files, I just need to know the directory structure that leanproject expects, where to put my files in that structure, so that they can be their own github repository, not intertwined with the Lean distribution.

[Kevin Buzzard]

https://leanprover-community.github.io/leanproject.html

[Kenny Lau]

leanproject new my_project

[Lars Ericson]

That has a .git subdirectory. So it is creating a repository instance. Where do I clone my Git repository? Under src?

[Kevin Buzzard]

One project, one repository. .git directory is always in the root of a git repo. I don't understand what you are not following here.

[Kevin Buzzard]

You can have lots of lean files in one repository.

[Lars Ericson]

I have my own .lean file repository, https://github.com/catskillsresearch/grundbegriffe. It just has lean files.

When I do leanproject new grundbegriffe, it does

git checkout --detach d4bd4cdaabcfddfb4215dca26b317aa32030bf79

This creates a directory that has a .git repository structure. I can't do git clone https://github.com/catskillsresearch/grundbegriffe.git directly into this, because it will have it's own .git file because it is it's own repository.

I think the answer is that I should do my git clone under src.

Kevin do you understand what my confusion is? Two separate repositories can't have .git files in the same subdirectory.

[Kevin Buzzard]

I don't understand why you can't just start again, make a project with leanproject, and put all your lean files in that properly-made correctly-formatted project (in src), and now you have a working project which you can push to github at your leisure.

[Lars Ericson]

Because if I push it to github I will be pushing it to your github, which might be considered impolite.

[Kevin Buzzard]

you are talking nonsense.

[Marc Huisinga]

@Lars Ericson you can set which remote repo you want to push to with git

[Kevin Buzzard]

If you make a project with leanproject then it is just a standalone git project, it is not connected to github in any way.

[Marc Huisinga]

(see https://git-scm.com/docs/git-remote)

[Lars Ericson]

OK so I need the git command which causes the resulting leanproject directory to save to https://github.com/catskillsresearch/grundbegriffe.git.

[Lars Ericson]

so

git remote add -m https://github.com/catskillsresearch/grundbegriffe.git

?

[Marc Huisinga]

you can find pretty much everything you need for using git using google, given that practically every software engineer uses it :)
https://docs.github.com/en/free-pro-team@latest/github/using-git/adding-a-remote

[Lars Ericson]

I appreciate the advice. For now I will go with this sequence:

leanproject new lean
cd lean/src
git clone https://github.com/catskillsresearch/grundbegriffe.git
cd grundbegriffe
code

[Lars Ericson]

Because at the level of src it still thinks it's in the originally cloned repository. If I do it that way and cd into src/grundbegriffe, then it thinks it's in my repository and forgets about the parent repository.

[Kevin Buzzard]

I would instead recommend that you delete your grundbegriffe repo, which is not a correctly formatted lean repo, and instead create a repo with leanproject and then push that repo to github. Your error was dumping a bunch of lean files on github in an incorrectly formatted way and until you fix this error by deleting the repo you are bound to have problems.

[Kevin Buzzard]

The code you posted above will create two git projects which is not what you want.

[Lars Ericson]

Thank you @Kevin Buzzard I will follow that advice.

[Lars Ericson]

The lean files still want to go in src, correct? As opposed to in the main directory.

[Kenny Lau]

yes

[Kevin Buzzard]

You could clone a repo like the tutorial project, following the instructions on the website I linked to above, if you want to check what a correctly-formatted project looks like.

[Lars Ericson]

Final solution, for an existing set of .lean files in directory oldproject:

leanproject new grundbegriffe
mv oldproject/*.lean grundbegriffe/src/.
cd grundbegriffe
git add .gitignore leanpkg.toml src
git commit -m "first commit"
git remote add origin https://github.com/catskillsresearch/grundbegriffe.git
git push -u origin master

[Marc Huisinga]

looks good i think