Zulip Chat Archive

Stream: new members

Topic: Correct sequence to create a Githubable Lean project

Lars Ericson (Dec 05 2020 at 23:14):

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 (Dec 05 2020 at 23:14):


Kenny Lau (Dec 05 2020 at 23:15):

leanproject new my_project

Lars Ericson (Dec 05 2020 at 23:19):

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

Kevin Buzzard (Dec 05 2020 at 23:20):

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 (Dec 05 2020 at 23:21):

You can have lots of lean files in one repository.

Lars Ericson (Dec 05 2020 at 23:24):

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 (Dec 05 2020 at 23:25):

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 (Dec 05 2020 at 23:27):

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

Kevin Buzzard (Dec 05 2020 at 23:27):

you are talking nonsense.

Marc Huisinga (Dec 05 2020 at 23:28):

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

Kevin Buzzard (Dec 05 2020 at 23:29):

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 (Dec 05 2020 at 23:30):

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

Lars Ericson (Dec 05 2020 at 23:30):

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

Lars Ericson (Dec 05 2020 at 23:31):


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


Marc Huisinga (Dec 05 2020 at 23:32):

you can find pretty much everything you need for using git using google, given that practically every software engineer uses it :)

Lars Ericson (Dec 05 2020 at 23:33):

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

Lars Ericson (Dec 05 2020 at 23:35):

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 (Dec 05 2020 at 23:36):

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 (Dec 05 2020 at 23:36):

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

Lars Ericson (Dec 05 2020 at 23:36):

Thank you @Kevin Buzzard I will follow that advice.

Lars Ericson (Dec 05 2020 at 23:37):

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

Kenny Lau (Dec 05 2020 at 23:39):


Kevin Buzzard (Dec 06 2020 at 00:07):

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 (Dec 06 2020 at 00:14):

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 (Dec 06 2020 at 00:17):

looks good i think

Last updated: Dec 20 2023 at 11:08 UTC