Stream: new members
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
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
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
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
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):
Lars Ericson (Dec 05 2020 at 23:30):
OK so I need the
git command which causes the resulting leanproject directory to save to
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 code
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
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: May 11 2021 at 14:11 UTC