Creating a Lean project in a repo

Stream: new members

[Ashvni Narayanan]

I am trying to create a new repo with Lean in it. I created the repo on Github and then cloned it locally. Then I used leanproject get mathlib, however, when I push to the repo, the mathlib folder does not get pushed/is not visible. I understand this is because there are some untracked git files in the folder. How can I solve this?
Any help is much appreciated, thank you!

[Eric Rodriguez]

Do you mean the _target folder? That's not meant to be pushed, I don't think. That's all tracked in the leanpkg.toml file

[Patrick Johnson]

File .gitignore contains the list of files (or file patterns) that git does not push to the remote repository. You can edit the file manually.

[Ashvni Narayanan]

Eric Rodriguez said:

Do you mean the _target folder? That's not meant to be pushed, I don't think. That's all tracked in the leanpkg.toml file

But all the files seem to be stored in there? Also my src folder is empty

[Eric Rodriguez]

Look at the leanpkg.toml. It will say that your repository has a copy of mathlib in it, and what specific version

[Eric Rodriguez]

That does get pushed, and whenever someone wants the lean project, they can just point leanproject at it and it'll do all the required work

[Ashvni Narayanan]

Apologies, I am quite confused. I want a local src to work with/add Lean files to. But the src folder I obtain when I add mathlib to my repo is empty.

[Eric Rodriguez]

src is your files! mathlib will be in _target. Try making a file there and importing some mathlib import.

[Ashvni Narayanan]

Ok, I think I understand now. This is working, thank you!

[Eric Wieser]

Why did you do leanproject get mathlib? You should only do that if you're working on mathlib itself, not if you're making a project that depends on mathlib

[Ashvni Narayanan]

I see, should I be undoing anything?

[Kevin Buzzard]

You create a new project with leanproject new name_of_my_project, and it will make a new project and add mathlib as a dependency. You then put your new files in /src (which will be empty). You can import mathlib files and it all works automatically.

[Ashvni Narayanan]

Thank you!

[Chandan Sah]

Hii

[Chandan Sah]

image.png

[Chandan Sah]

image.png
I was following the instructions mentioned in this page. But on typing "Select Default Profile" on the command palette of VS code, these four options showed up, but GIT Bash did not show up. Can anyone tell why this might be happening? Because I feel I followed the instructions very carefully

[Kevin Buzzard]

Is this Windows? Did you try turning it off and on again?

[Chandan Sah]

Yes it is windows.

I restarted the PC once

[Chandan Sah]

@Kevin Buzzard

[Eric Wieser]

Just to confirm; is git installed on your system?

[Chandan Sah]

Yes

[Eric Wieser]

I don't really understand why that step is there in the instructions; everything ought to work fine in powershell too

[Eric Wieser]

You just have to be aware that most instructions for using terminals will be given for bash, so you'll occassionally have to use different spellings

[Mauricio Collares]

But if you want to debug the Git Bash issue: Do you see Git Bash as an option if you click on the down arrow to the right of where it says "powershell" on your screenshot (same line as "Problems", "Output", "Terminal" and so on)?

[Mauricio Collares]

If not, then you're probably seeing the same issue as https://stackoverflow.com/questions/68068359/gitbash-not-showing-up-as-a-terminal-option-in-visual-studio-code/68140594#68140594. They have a few workarounds, but haven't determined a root cause. Do you use an old (pre-1903) Windows 10 version by any chance?

[Mauricio Collares]

If you're on a sufficiently new version of Windows 10, this part of the setup process should have installed a Terminal profile for you, and you can check the relevant directory (either %appdata%\Microsoft\Windows Terminal\Fragments\Git or %localappdata%\Microsoft\Windows Terminal\Fragments\Git) to see if something is messed up.

[Mauricio Collares]

If you can still find your Git for Windows install logs in your temp folder, that might be useful for debugging too.