Zulip Chat Archive

Stream: new members

Topic: Correct sequence to create a Githubable Lean project


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 23:14):

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

view this post on Zulip Kenny Lau (Dec 05 2020 at 23:15):

leanproject new my_project

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 23:21):

You can have lots of lean files in one repository.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 23:27):

you are talking nonsense.

view this post on Zulip Marc Huisinga (Dec 05 2020 at 23:28):

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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Dec 05 2020 at 23:30):

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

view this post on Zulip 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.

view this post on Zulip Lars Ericson (Dec 05 2020 at 23:31):

so

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

?

view this post on Zulip 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 :)
https://docs.github.com/en/free-pro-team@latest/github/using-git/adding-a-remote

view this post on Zulip 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
code

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 23:36):

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

view this post on Zulip Lars Ericson (Dec 05 2020 at 23:36):

Thank you @Kevin Buzzard I will follow that advice.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 05 2020 at 23:39):

yes

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Dec 06 2020 at 00:17):

looks good i think


Last updated: May 11 2021 at 14:11 UTC