leanblueprint new fails

Stream: general

[Yujie Wang]

I've tried to do the blueprint part, and in step 3, I couldn't run the "leanblueprint new" successfully in terminal or the file.
May I ask what should I do? I couldn't find useful information online or with AI
image.png

[Julian Berman]

Your VSCode makes it look like you don't have a Lean project.

[Julian Berman]

Are you trying to create a Lean project and then a blueprint for it?

[Julian Berman]

Oh no wait it's me who doesn't understand what VSCode is showing there on the top vs the bottom of the sidebar.

[Julian Berman]

Putting leanblueprint new definitely belongs in the terminal (the black pane) there not in the lean file -- can you show what ls and pwd show in there?

[Yujie Wang]

image.png
Hi thanks! here's the ls and pwd

[Julian Berman]

OK good, that looks OK. Let's see if I can see anything in the blueprint docs now.

[Julian Berman]

Can you show leanblueprint --version as well?

[Yujie Wang]

image.png
hmmm it shows the same thing

[Julian Berman]

Oh interesting, that's an unrelated leanblueprint bug which I can reproduce, but not related to your actual question. Is your project pushed somewhere I can test perhaps? (EDIT: oh right, I'm pretty sure I've even noticed this --version thing before on other projects but it's WONTFIXed on the click repo.)

[Julian Berman]

@Yujie Wang given we couldn't check what the version you have is via --version, you also can just run pip install -U leanblueprint if you haven't already. I just want to be sure you're on the latest version.

[Yujie Wang]

https://github.com/pitmonticone/LeanProject.
Hi yes I just used this template and followed the instructions

[Yujie Wang]

image.png

[Julian Berman]

Yujie Wang said:

https://github.com/pitmonticone/LeanProject.
Hi yes I just used this template and followed the instructions

Yes good understood! But is your repository itself pushed perhaps? Just to see if I can reproduce your issue. Alternatively, can you perhaps tell me what you get from running python -c 'import git; print(git.Repo(".", search_parent_directories=True))'?

[Yujie Wang]

sure! let me try
image.png

[Julian Berman]

So that's what's wrong, now the question is why. If you run git status what do you get?

[Yujie Wang]

image.png

[Yujie Wang]

Hi i‘m trying to push mine

[Julian Berman]

And if you run ls .git what does that say? I am very suspicious of the directory name you have (it makes me think you have multiple working trees set up), but I am also going to assume you didn't do that yourself and that none of that means anything to you, and something (some tool) has given your repository a strange git repository setup, but we'll figure it out.

[Yujie Wang]

image.png

[Julian Berman]

There's a space there -- ls .git

[Yujie Wang]

https://github.com/CusYojo/wpf-test

[Yujie Wang]

image.png

[Yujie Wang]

Thanks ! I've pushed!

[Julian Berman]

Something has changed!

[Julian Berman]

Try running leanblueprint new again, does it work?

[Yujie Wang]

Oh! yes! It works!

[Yujie Wang]

image.png

[Yujie Wang]

Thanks! What happened???

[Julian Berman]

Once again I know what, but not how I'm afraid. We must have said the right incantation to the computer gods. A quick explanation is that as I said I was suspicious of your directory name. You had something that said weierstrass-p-function-main as your directory name. Usually in git this indicates that you've used something like git worktree but I assumed you wouldn't be using that unless you knew what it did, so it's more likely something that was clicked in VSCode ran that kind of operation for you. And in that state, gitpython (which leanblueprint uses) wasn't able to understand what you had. As part of you pushing your repo you must have clicked something which got you back to a normal git repository state which I could tell because I saw the -main disappeared. But I don't know enough about VSCode to be able to tell you which button to avoid I'm afraid. I think you should be good to go now though!

[Yujie Wang]

Thanks Julian! yes you're right, I didn't use the gitworktree. The disappeared -main is because I pulled again, named the new file and repeated the same thing I did. But anyway it's great that I can keep doing this now! So many thanks to you!

[Julian Berman]

Pleasure.