Zulip Chat Archive

Stream: general

Topic: branch not building?


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 10 2020 at 07:33):

did you build? leanproject build

view this post on Zulip Mario Carneiro (Nov 10 2020 at 07:34):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 10 2020 at 07:58):

What is the PR you are talking about?

view this post on Zulip Benjamin Davidson (Nov 10 2020 at 07:59):

Patrick Massot said:

What is the PR you are talking about?

#4945

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:04):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:17):

This is not the correct instructions set.

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:17):

Could you please try to follow my suggestions?

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:17):

It works here.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:27):

Maybe it's called pip3

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:27):

How did you install leanproject originally?

view this post on Zulip Benjamin Davidson (Nov 10 2020 at 08:33):

The instructions on the website.

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:34):

Did you try pipx?

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:34):

Because those instructions seem to use pipx

view this post on Zulip Benjamin Davidson (Nov 10 2020 at 08:35):

Yes. It, too, was not found.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:50):

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

view this post on Zulip Benjamin Davidson (Nov 10 2020 at 09:07):

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

view this post on Zulip Patrick Massot (Nov 10 2020 at 09:07):

What about installing Linux?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 10 2020 at 09:09):

He installed a long time ago.

view this post on Zulip Anne Baanen (Nov 10 2020 at 09:11):

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

view this post on Zulip 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.

view this post on Zulip 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
  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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Benjamin Davidson (Nov 11 2020 at 05:01):

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

view this post on Zulip 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.

view this post on Zulip Benjamin Davidson (Nov 11 2020 at 05:45):

Okay, I was just making sure.

Where can I find instructions on how to uninstall leanproject?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Nov 11 2020 at 05:52):

you might be able to just install it again

view this post on Zulip Benjamin Davidson (Nov 11 2020 at 06:07):

Okay I'll give it a try

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Lacker (Nov 11 2020 at 06:43):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Lacker (Nov 11 2020 at 06:51):

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

view this post on Zulip Kevin Lacker (Nov 11 2020 at 06:53):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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