Stream: general

Topic: branch not building?

Benjamin Davidson (Nov 10 2020 at 07:03):

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 (Nov 10 2020 at 07:33):

did you build? leanproject build

Mario Carneiro (Nov 10 2020 at 07:34):

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

Johan Commelin (Nov 10 2020 at 07:34):

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 (Nov 10 2020 at 07:57):

Mario Carneiro said:

did you build? leanproject build

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

Patrick Massot (Nov 10 2020 at 07:58):

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

Patrick Massot (Nov 10 2020 at 07:58):

What is the PR you are talking about?

Benjamin Davidson (Nov 10 2020 at 07:59):

Patrick Massot said:

What is the PR you are talking about?

#4945

Patrick Massot (Nov 10 2020 at 08:04):

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

Patrick Massot (Nov 10 2020 at 08:10):

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 (Nov 10 2020 at 08:16):

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 (Nov 10 2020 at 08:17):

This is not the correct instructions set.

It works here.

Benjamin Davidson (Nov 10 2020 at 08:25):

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 (Nov 10 2020 at 08:27):

Maybe it's called pip3

Patrick Massot (Nov 10 2020 at 08:27):

How did you install leanproject originally?

Patrick Massot (Nov 10 2020 at 08:34):

Did you try pipx?

Patrick Massot (Nov 10 2020 at 08:34):

Because those instructions seem to use pipx

Patrick Massot (Nov 10 2020 at 08:36):

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 (Nov 10 2020 at 08:41):

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 (Nov 10 2020 at 08:43):

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 (Nov 10 2020 at 08:46):

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 (Nov 10 2020 at 08:49):

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 (Nov 10 2020 at 08:50):

• 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 (Nov 10 2020 at 08:50):

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

Patrick Massot (Nov 10 2020 at 08:50):

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

Benjamin Davidson (Nov 10 2020 at 09:07):

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

Anne Baanen (Nov 10 2020 at 09:09):

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 (Nov 10 2020 at 09:09):

He installed a long time ago.

Anne Baanen (Nov 10 2020 at 09:11):

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

Benjamin Davidson (Nov 10 2020 at 09:20):

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

Kevin Lacker (Nov 10 2020 at 18:30):

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
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 (Nov 11 2020 at 01:35):

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

Benjamin Davidson (Nov 11 2020 at 01:49):

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 (Nov 11 2020 at 04:36):

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 (Nov 11 2020 at 05:01):

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

Bryan Gin-ge Chen (Nov 11 2020 at 05:23):

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 (Nov 11 2020 at 05:45):

Okay, I was just making sure.

Where can I find instructions on how to uninstall leanproject?

Johan Commelin (Nov 11 2020 at 05:51):

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

Kevin Lacker (Nov 11 2020 at 05:51):

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

Kevin Lacker (Nov 11 2020 at 05:52):

you might be able to just install it again

Benjamin Davidson (Nov 11 2020 at 06:07):

Okay I'll give it a try

Benjamin Davidson (Nov 11 2020 at 06:08):

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

Benjamin Davidson (Nov 11 2020 at 06:41):

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 (Nov 11 2020 at 06:43):

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

Benjamin Davidson (Nov 11 2020 at 06:44):

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 (Nov 11 2020 at 06:50):

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 (Nov 11 2020 at 06:51):

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

Kevin Lacker (Nov 11 2020 at 06:53):

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

Bryan Gin-ge Chen (Nov 11 2020 at 06:54):

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 (Nov 11 2020 at 06:55):

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 (Nov 11 2020 at 06:56):

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 (Nov 11 2020 at 07:06):

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 (Nov 11 2020 at 07:55):

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

Last updated: May 13 2021 at 20:13 UTC