branch not building?

Stream: general

[Benjamin Davidson]

I have what seems to be a technical problem.
I downloaded a new branch of mathlib for the sake of creating a new PR, which I did. Later, I wanted to update that branch to include the most recent changes to mathlib. As usual, I pulled from github then did a leanproject get-cache. Now, the branch won't build (I think that's the problem), with the status bar instead reading "checking 1 file" no matter what files I open or close, and it attempts to check that file until my computer goes into overdrive. I rebased and tried to build the branch (I aborted the build after an exceedingly long period of time) but to no effect.
Does anyone have any idea what the issue could be or how I could go about resolving this? If there is no obvious solution, am I able to delete this branch and download a new one and still be able to push changes to my PR from the new branch?

[Mario Carneiro]

did you build? leanproject build

[Mario Carneiro]

also leanproject check can be used to diagnose when the editor is slow

[Johan Commelin]

Can you try

# on your branch
git commit -am wip # just to make sure you don't loose stuff
git checkout master
leanproject get-cache
git checkout - # back to your branch
git merge master
leanpkg build

[Benjamin Davidson]

Mario Carneiro said:

did you build? leanproject build

Yes, but I aborted after about an hour and a half.

[Patrick Massot]

We won't be able to help you without a more specific description that allow us to reproduce your problem.

[Patrick Massot]

What is the PR you are talking about?

[Benjamin Davidson]

Patrick Massot said:

What is the PR you are talking about?

#4945

[Patrick Massot]

So your goal is to rebase this PR on master, right?

[Patrick Massot]

Could you try the following steps:

• Upgrade your mathlib tools, presumably by running pip install -U mathlibtools or pipx install -U mathlibtools if you use pipx
• leanproject get mathlib:ftc2
• cd mathlib_ftc2
• leanproject rebase
• Try to continue working

[Benjamin Davidson]

Johan Commelin said:

Can you try

# on your branch
git commit -am wip # just to make sure you don't loose stuff
git checkout master
leanproject get-cache
git checkout - # back to your branch
git merge master
leanpkg build

I tried this but the problem persists.

[Patrick Massot]

This is not the correct instructions set.

[Patrick Massot]

Could you please try to follow my suggestions?

[Patrick Massot]

It works here.

[Benjamin Davidson]

Do I need to install something to be able to use pip? I get a "command not found" error. I am running a zsh terminal on a Mac.

[Patrick Massot]

Maybe it's called pip3

[Patrick Massot]

How did you install leanproject originally?

[Benjamin Davidson]

The instructions on the website.

[Patrick Massot]

Did you try pipx?

[Patrick Massot]

Because those instructions seem to use pipx

[Benjamin Davidson]

Yes. It, too, was not found.

[Patrick Massot]

I'm afraid you'll need to wait for a MacOS user to come nearby. But you would do yourself a favor by learning how to use python on your computer. That will probably be useful for many other things.

[Benjamin Davidson]

Patrick Massot said:

Maybe it's called pip3

It recognized pip3, but I get the following error:

ERROR: Could not install packages due to an EnvironmentError: [Errno 13] Permission denied: 'RECORD'
Consider using the `--user` option or check the permissions.

[Patrick Massot]

We could fix that but I'm afraid that would start messing up your python setup and lead to confusion by having two separate copies of the mathlib tools. The automated procedure you followed when installing should have installed pipx. We need to understand why you're not finding pipx anymore.

[Benjamin Davidson]

I have python on my computer as a part of Anaconda. But I don't recall ever installing anything in terminal, nor was I familiar with the pip common or any of its variations until now.

[Patrick Massot]

I see. Using Anaconda is definitely a bad idea here. While waiting for a MacOS or Anaconda user, you can still fix your issue by hand.

[Patrick Massot]

• leanproject get mathlib:ftc2
• cd mathlib_ftc2
• git checkout master
• git pull
• leanproject get-cache
• git checkout ftc2
• git rebase master
• Try to continue working

[Benjamin Davidson]

I should have been clearer: I use VSCode for lean. I happen to have Anaconda installed on my computer as well.

[Patrick Massot]

This has nothing to do with VSCode vs "I-choose-pain-emacs"

[Benjamin Davidson]

Something must be very wrong because now I get the "command not found" error for leanproject...

[Patrick Massot]

What about installing Linux?

[Anne Baanen]

Have you re-logged in on your computer since installing? There are some .profile/.bashrc files that don't get loaded by default I believe.

[Patrick Massot]

He installed a long time ago.

[Anne Baanen]

I meant since running pip{x,3} install.

[Benjamin Davidson]

I haven't, but I'm going to have to get back to this later. I gotta get to bed.

[Kevin Lacker]

you're only changing a single file in this branch. here's my recommendation of how to fix it simply.

1. the file where you made all your changes, make a copy of it somewhere else
2. delete your branch entirely
3. close your open "work in progress" pull request
4. check out master, run get-cache, make sure lean is working fine.
5. make a new branch. name it something different, the old name is cursed
6. copy your file with the changes back into this new branch
7. continue working on this new branch

my guess is that all the wackiness with your pip install is a red herring, and that the problem is that your get-cache failed because the git hash didn't match anything cached. but my guess doesn't have to be correct, this sequence of operations should fix it anyway

[Benjamin Davidson]

I logged out and back in but leanproject is still not found and I get the same error for pip3.

[Benjamin Davidson]

Kevin Lacker said:

my guess is that all the wackiness with your pip install is a red herring...

Would the same apply to why it's not recognizing leanproject?

[Kevin Lacker]

I don't know. But fixing your leanproject install is the step you can focus on first. I would remove all traces of leanproject you can find and just reinstall it from scratch.

[Benjamin Davidson]

How would that impact the branches I already have and have been working in?

[Bryan Gin-ge Chen]

They shouldn't be affected. leanproject is a python script which performs actions on your Lean projects and branches within them only when you call it. Uninstalling / reinstalling won't affect the Lean projects themselves. If you're worried, you can always push your branches to GitHub before making any changes.

[Benjamin Davidson]

Okay, I was just making sure.

Where can I find instructions on how to uninstall leanproject?

[Johan Commelin]

I guess this should be the way you uninstall any pip package. But I've never tried it.

[Kevin Lacker]

it depends how you installed it, which since you can't find it, might be hard to figure out

[Kevin Lacker]

you might be able to just install it again

[Benjamin Davidson]

Okay I'll give it a try

[Benjamin Davidson]

As you can probably tell, I really don't know anything about this sort of stuff, hence all the questions

[Benjamin Davidson]

I reinstalled lean and followed these steps from Patrick. It seems as though everything is in now order but I'm not sure how to tell whether or not I will run into future problems with this PR. I suppose that if I do I will have to follow Kevin's advice on ditching my PR and starting fresh.

[Kevin Lacker]

if your branch is building fine then it's probably all good

[Benjamin Davidson]

I also notice that I am now no longer signed in on VSCode, though I'm not sure how that relates to these other issues. I doubt it's of any importance, since I preformed git config --global --edit and everything in that file is as it should be, but is there a way I can sign back in? I don't see any obvious ways to do so.

[Bryan Gin-ge Chen]

What do you mean by "signed in on VS Code"? I don't think I've ever had to sign in to use VS Code (except when I was experimenting with the Live Share extension).

[Kevin Lacker]

i think he's referring to vscode's git integration

[Kevin Lacker]

if this is what you're referring to, see https://code.visualstudio.com/docs/editor/github

[Bryan Gin-ge Chen]

Ah, I see. I don't use that extension. I've only used the built-in version control interface, which doesn't require any sign-in.

[Benjamin Davidson]

It's not a mandated sign in, but in the past if I were to click on the "Accounts" icon on the bottom left of the VSCode environment it would display "Signed in as...". Now it notifies me that I am not signed in. Screen-Shot-2020-11-11-at-1.52.02-AM.png
Again, I doubt this is crucial, but I figured I'd mention it.

[Bryan Gin-ge Chen]

I've never used that before. I think it could be useful if you want to have the same settings in VS Code across different computers.

[Benjamin Davidson]

Kevin Lacker said:

if this is what you're referring to, see https://code.visualstudio.com/docs/editor/github

Hmm... I came across this before but I don't have the "Pull Requests and Issues" extension so I don't think that's what it was. Nor am I getting any prompts to authenticate github, so I don't think I can implement any of what they discuss in that article.

If it's of no consequence whether or not I'm signed in then it's fine, I'll just leave it and if I ever do get a prompt to sign in then great, if not, no big deal. To be honest, I have no recollection of signing in or authenticating anything in the first place, I just noticed that it is no longer displaying my account name.

[Kevin Lacker]

personally, i do not use the vscode + github integration anyway. it should be fine