Zulip Chat Archive

Stream: new members

Topic: Stopping VSCode from recompiling mathlib


view this post on Zulip Donald Sebastian Leung (Oct 04 2020 at 08:23):

I just created a new project by executing leanproject new kata, edited leanpkg.toml to contain the following:

[package]
name = "kata"
version = "0.1"
lean_version = "leanprover-community/lean:3.20.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "da66bb81bf0466335bae82077f0c335dfe53aeb3"}

and executed leanproject get-mathlib-cache. I then opened my project folder in VSCode and created a new file Preloaded.lean with the following contents:

import data.equiv.basic data.pnat.basic

The orange bar at the import line stays for well over a minute, and system statistics indicate that CPU usage increases to 100%, with all 4G of RAM and 1.5G of swap (of 2G total) being used in the meantime, suggesting that (parts of) mathlib was being recompiled. How do I stop this from happening? I thought that leanproject get-mathlib-cache used to do the job but maybe I misremembered.

view this post on Zulip Patrick Massot (Oct 04 2020 at 10:00):

Why did you edit the leanpkg.toml?

view this post on Zulip Donald Sebastian Leung (Oct 04 2020 at 10:24):

The toy Lean examples I use for Codewars have been tested with a version of mathlib from about a week ago and I've just been asked to add an example involving a mathlib dependency. I thought it would be easier to pin mathlib and build my new example on that specific commit instead of running all of my previous examples with the newest mathlib.

But now that I think about it, it would probably be easier to just use the newest mathlib and run all of the existing examples against it, especially considering that none of them have any meaningful dependency on mathlib AFAIK.

view this post on Zulip Patrick Massot (Oct 04 2020 at 10:27):

That being said I'm not able to reproduce your issue.

view this post on Zulip Patrick Massot (Oct 04 2020 at 10:27):

I did exactly what you wrote and everything works fine.

view this post on Zulip Patrick Massot (Oct 04 2020 at 10:28):

What happens if you quit VSCode and type leanproject build in the kata folder?

view this post on Zulip Donald Sebastian Leung (Oct 09 2020 at 07:32):

Apologies for the late reply, I used the newest mathlib when constructing my Lean examples as I mentioned earlier, but I realized I had to stick to a fixed mathlib version anyway for updating the Lean content on Codewars in order to ensure reproducibility, and so got another chance to reproduce this issue.

What happens if you quit VSCode and type leanproject build in the kata folder?

I get the following output, produced within a second or two:

Building project kata
configuring kata 0.1
mathlib: trying to update _target/deps/mathlib to revision da66bb81bf0466335bae82077f0c335dfe53aeb3
> git checkout --detach da66bb81bf0466335bae82077f0c335dfe53aeb3    # in directory _target/deps/mathlib
Previous HEAD position was f6836c16f chore(scripts): update nolints.txt (#4547)
HEAD is now at da66bb81b feat(*): preparations for roots of unity (#4322)
> lean --make src
/home/dsleung/Desktop/kata/src/InitialSolution.lean:3:0: warning: declaration 'zero_point_nine_recurring_is_one' uses sorry
/home/dsleung/Desktop/kata/src/Solution.lean:16:48: error: unknown identifier 'one_div_pos_of_pos'
/home/dsleung/Desktop/kata/src/Solution.lean:20:10: error: unknown identifier 'one_div_le_of_one_div_le_of_pos'
/home/dsleung/Desktop/kata/src/Solution.lean:12:0: warning: declaration 'zero_point_nine_recurring_is_one' uses sorry
/home/dsleung/Desktop/kata/src/SolutionTest.lean:1:0: warning: imported file '/home/dsleung/Desktop/kata/src/Solution.lean' uses sorry
propext
classical.choice
quot.sound
[sorry]
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.

I suppose that means mathlib is not being recompiled in this case (but it still definitely is in VSCode)?

view this post on Zulip Donald Sebastian Leung (Oct 09 2020 at 07:33):

Update: Upon returning to VSCode after running leanproject build once, it seems that mathlib is no longer being recompiled. Thanks @Patrick Massot !

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:15):

I think my VSCode, or Lean installation, has something really wrong in it; after 5/10 minutes of work it "randomly" (so seems to me, at least) start compiling the whole library. And therefore I cannot work anymore... Is anyone experiencing the same problem? Suggestions?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:16):

I should also add that in "normal times" my whole system seems very slow, each type I make a small modification it takes some 5 to 10 seconds to get to work again, which is a LOOOOONG time if you keep on writing things.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:19):

I also am seeing frequent over-recompilations. I kill my lean server and restart it pretty often. Usually that fixes it. Otherwise, I switch to master branch, pull, rerun leanproject get-cache, and see if that fixes it. Usually it does - maybe I'm causing these problems by doing something inappropriate with branches, I dunno. If that does fix it then merging the new master into my branch fixes my original problem

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:20):

How do you kill your server?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 22:20):

Random library recompilation: some tips are (a) close files you're not working on (b) restart VS Code.

5 to 10 seconds of orange bars: this just sounds like you used an expensive tactic early on in a proof and it is being run again and again. So it's "bad code" in some sense.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:20):

(btw are you also using VSCode? On Win, Mac?)

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:20):

C-c C-r in emacs. Or just with ps aux and kill from a terminal

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:21):

In VS Code you can hit ctrl+P (or cmd+P on a mac) and type "Lean: restart". You can also bind a key to this command.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:21):

Kevin Buzzard said:

Random library recompilation: some tips are (a) close files you're not working on (b) restart VS Code.

5 to 10 seconds of orange bars: this just sounds like you used an expensive tactic early on in a proof and it is being run again and again. So it's "bad code" in some sense.

Could very possibly be: what are the typical " bad" tactics? I guess simp is one

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:21):

emacs on linux. vscode isn't doing the recompilation itself, right? it's communicating out to some lean process

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:22):

Right

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:24):

Bryan Gin-ge Chen said:

In VS Code you can hit ctrl+P (or cmd+P on a mac) and type "Lean: restart". You can also bind a key to this command.

I tried with ctrl+P, the bar when I can write opens but when I type Lean: restart I just get a "No matching result' error... am I missing something?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:24):

try just typing "Lean" and looking through the options

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:24):

Oh sorry, it's ctrl+shift+p

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:26):

It restarted but it is compiling everything again. Probably @Kevin Buzzard is right, my code must be terrible

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:26):

is it also recompiling your import statements at the top of the file? or is it only recompiling code that you wrote yourself

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:27):

I believe it is recompiling the whole library (there are orange bars on the left, where the library is, and all over the file, from the first line down to where I am writing)

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:27):

I would recommend: open a terminal, run leanproject build, then use ctrl-shift-p "Lean: restart".

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:28):

If leanproject build is recompiling everything, then either you have edited a file low in hierarchy, and need to either

  1. commit your branch and let continuous integration compile everything, or
  2. let leanproject build complete locally.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:28):

Scott Morrison said:

I would recommend: open a terminal, run leanproject build, then use ctrl-shift-p "Lean: restart".

Thanks, I had tried this in the afternoon. the leanproject build command took a hour or so (is it normal?), and then Lean worked for some 10/15 minutes. After that, it begun compiling everything again

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:28):

If leanproject build returns relatively quickly (say, at most 10s, hopefully much less), and you then restart the lean server and still see orange bars, then we really have a problem.

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:29):

No, if you have up-to-date olean then leanproject build should take at most 10s.

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:29):

Hopefully less!

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:29):

are you working on a branch of the main repo, or on a fork of the project, or how do you have that set up?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

I am working on a branch of the main repo

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

(which is Anne's repo, actually, Vierkantor-dedekind-domain)

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

Scott Morrison said:

Hopefully less!

Let me try again!

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:31):

try running leanproject get-cache before building

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:32):

I am going to, give me 30 sec

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:33):

Now I get an error, but I think this comes from the fact that I have just pull and the server must be compiling

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:33):

Which file(s) are you editing, exactly?

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:33):

An hour doesn't seem unreasonable if you're editing something really low level.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:34):

BTW: Is this related to the fact that after almost every pull I receive an e-mail with an error saying [leanprover-community/mathlib] Run failed: continuous integration - Vierkantor-dedekind-domain (8bd048d)

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:34):

You can turn those notifications off from your GitHub settings.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:34):

Bryan Gin-ge Chen said:

Which file(s) are you editing, exactly?

I am editing the file on Dedekind Domains, I don't think it is low level

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:34):

Also, you should be getting those from pushes, not pulls...

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:35):

Bryan Gin-ge Chen said:

You can turn those notifications off from your GitHub settings.

Well, but I am wondering whether this is a signal of an issue

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:35):

Bryan Gin-ge Chen said:

Also, you should be getting those from pushes, not pulls...

You're right, my mistake .

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:36):

Well, the runs are failing because the code that you're pushing has errors in the Lean or some linting issues. It's usually fine.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:37):

Kevin Lacker said:

try running leanproject get-cache before building

Ok, now I could download the cache. And I am going to rebuild.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:38):

Nope, the terminal window says > lean --make src, the fan is taking off and a minute has passed...

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:38):

(and it looks very much as before)

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:42):

Here's the log for the build triggered by your most recent commit: https://github.com/leanprover-community/mathlib/runs/1261674429

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:42):

You can see that the build hits an error on src/algebra/direct_limit.lean.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:42):

If that file isn't fixed, then you won't get oleans for anything "downstream".

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:43):

I see-but I have never touched that file myself. Can't I just copy the version in master and hope it helps?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:45):

(well, provided my pc won't explose in the coming minutes, which seems like the next probable event)

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:45):

your pc is fine, you'll have a mildly elevated risk of hard drive failures if it keeps running this way for the next 3 months straight ;-)

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:46):

even if you never touched that file, you must be causing the build breakage somehow, since it's working in master

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:46):

Filippo A. E. Nuccio said:

I see-but I have never touched that file myself. Can't I just copy the version in master and hope it helps?

This is unlikely to fix things.

I think @Anne Baanen can probably provide the best advice here.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:47):

I asked them a couple of times, but they don't seem to experience the same issue.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:47):

If it were me, I would git merge master and then try to fix all the conflicts and errors.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:48):

But that looks to be difficult at this point.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:48):

are you working on your own branch, or are you sharing a branch with a bunch of other people, and you all kind of simultaneously check in code without being totally sure it works?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:48):

Kevin Lacker said:

even if you never touched that file, you must be causing the build breakage somehow, since it's working in master

I agree, but I have no idea on how to figure where the breakage takes place. Expecially because I did the leanproject build this afternoon, it took a hour or so; and after ten minutes of work on the newly rebuild library, I went back where I was

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:49):

Well, technically we are three people working on this, but the other two members haven't touched the file in the last 3 weeks or so.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:49):

When you run leanproject build, you should pay attention to the output. If the word error shows up anywhere then things are broken.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:50):

And what do I do in that case?

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 22:50):

You will have to fix the error or get someone to fix it for you.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:50):

it looks like both you and Vierkantor have checked into the branch recently

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:50):

you can't look at just a single file - it's possible for a change in one file to break something in another file

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:51):

Well, if the other file is downstream wrt mine, right?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:51):

look at https://github.com/leanprover-community/mathlib/compare/Vierkantor-dedekind-domain

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:52):

it was passing checks as of commit https://github.com/leanprover-community/mathlib/commit/8c94fef07967472c2f839f4333f479888196efdb

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:52):

and then continuous integration broke here: https://github.com/leanprover-community/mathlib/commit/8bd048dc7a42350246468e323e4609c6bf1a2d31

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:52):

it looks like you did a merge which failed

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:53):

6 hours ago, you did a merge which had "313 changed files with 13,112 additions and 4,549 deletions"

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:53):

my guess is that one of those 313 files you changed had a problem

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:53):

But how is it possible that I changed 313 files?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:53):

(let alone the 13,112 additions)?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:53):

take a look, the commit where you did it is right here: https://github.com/leanprover-community/mathlib/commit/8bd048dc7a42350246468e323e4609c6bf1a2d31

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:54):

it looks like a massive merge, maybe you ran a huge git merge command without realizing it was a huge git merge command?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:54):

I am looking at that commit and am shocked...

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:55):

I don't think I merged anything: I opened git, checked with git status that I was up to date and opened VLCode

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:55):

worked a bit, then commit+pushed.

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:56):

It could just be that you merged master at that point.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:56):

git is kind of like a swiss army knife where one of the tools is a grenade. if you just kinda type one command wrong it can screw a lot of stuff up

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:57):

but I never type commands on git. I work directly and only in VSCode

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:57):

shrug

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:57):

For instance, it seems that I touched upon src/algebra/char_zero.lean

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:57):

How do you merge master into your working branch, then?

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:57):

Obviously the changes in that massive commit are changes other people have been making to master.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:58):

you probably clicked "ok" to something in vscode that was actually a bad idea to click ok on

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:58):

It can't be anything other than merging master in your branch.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:58):

at any rate, what you want to do here is three steps

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 22:58):

This is something @Anne Baanen does, normally. I usually only work in my local copy of their branch

view this post on Zulip Scott Morrison (Oct 15 2020 at 22:58):

On the other hand, merging master is something you have to do at some point.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:58):

first, you made some changes after that massive merge. in this commit: https://github.com/leanprover-community/mathlib/commit/53a347b5d8c50f7b6d99fd94e2bb192b4688782e

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:58):

grab those changes and store them locally somehow. i would like, cut and paste them into a text file or something naive

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:59):

second, roll back your branch to before the merge broke everything

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:59):

probably google for some page of git commands, i never remember how to do this stuff

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:59):

third, reapply your changes that you intended to make, without doing that huge merge

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:00):

Thanks, I will do this. But I'd like to undestand where this came from. I haven't typed merge a single time today

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:00):

And I have been fighting against these issue since June or something

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:00):

there are several layers to this answer

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:01):

the most superficial answer is that it probably came from vscode, because most people set up vscode to interact with git. maybe you accidentally clicked some icon that does something

view this post on Zulip Scott Morrison (Oct 15 2020 at 23:01):

Do you ever run leanproject up?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:01):

Yes---I had been told it is more or less equivalent to get-cache

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:03):

the second level of answer is that the more you work against some branch that is super diverged from master, the more of these problems you will have. so you can avoid trouble by staying closer to master

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:04):

Well, but if @Anne Baanen merged yesterday the master with their branch, and I pulled right before starting to work, I was pretty close , no?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:06):

AHAH: In the meanwhile leanproject build has finished with tons and tons of errors

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:07):

both of you are super far away from master, this separate branch has been open since August 4

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:07):

were you getting a bunch of error emails from continuous integration that you were ignoring?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:08):

Yes - very bad idea, I suppose.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:11):

the thing to do when you get one is to look at the CI error - a page like this one: https://github.com/leanprover-community/mathlib/runs/1261674429

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:12):

if it seems like it's your fault, fix it. if it doesn't seem like it's your fault, look at the commit history. it's linked from that page if you click on the branch name. a page like this one: https://github.com/leanprover-community/mathlib/compare/Vierkantor-dedekind-domain

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:12):

the little X's on the right show you when the build was OK and when the build was broken

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:12):

in this case, you can see that there was an ok build earlier today, and then the first of the most recent block of X's is the commit you should be suspicious of

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:12):

and when you say "it's your fault" do you mean that there is a non-compiling file?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:13):

when I checked that commit, I saw that 1. you were the author and 2. it modified 300 files, which made me think aha looks like an accidental huge merge

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:13):

I mean that you committed the change that broke the build

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:13):

it might not be your fault if like, maybe there's something that breaks randomly once every 20 runs. then the test is at fault

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:14):

if you suspect something like that, have the CI system rerun the build

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:15):

namely? I mean, it will complain and won't build, no?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:16):

let's say the error is like, "error for free_comm_ring.lift, failed to synthesize type class instance". that sounds like your fault. but if the error is like, "error, hard drive failure detected, system rebooting." that doesn't sound like your fault.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:18):

yet I believe there must be some problem with my VSCode, or something. I have checkout to master, and again VSCode has been compiling for 5 minutes

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:18):

although I have simply get-cache and then opened VSCode, without typing a single character

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 23:19):

If you only git checkout, you don't have the corresponding olean files. So you'll need to build those locally or get them using leanproject get-cache..

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:20):

so I did: checkout, then get-cache, then opened VSCode. I went to a file (without editing) to see if the Infoview would work, and here I am since 5 minutes.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:20):

restart the lean server

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:20):

done

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:20):

orange bars...

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:21):

you're sure you're on master?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:21):

FAE@DESKTOP-MMB9C9K MINGW64 ~/Desktop/Lean/mathlib (Vierkantor-dedekind-domain)
$ git checkout master
Switched to branch 'master'
Your branch is up to date with 'origin/master'.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:22):

git pull

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:22):

done

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:22):

leanproject get-cache

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:23):

going on...

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:23):

done

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:23):

now see if things compile

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:23):

now yes, everything nice and smooth

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:24):

great. now you can go fix your borked branch

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:24):

I have removed my Git info from VSCode, so it can't do "too much".

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:25):

Kevin Lacker said:

great. now you can go fix your borked branch

the steps you suggested before, right?

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:25):

yeah

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:25):

so I need to merge master with the other branch - I suspect I will get some 400 errors, or so.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:26):

mmm no you should not need to merge anything

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:26):

all you're doing is rolling back your branch

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:27):

to https://github.com/leanprover-community/mathlib/commit/8c94fef07967472c2f839f4333f479888196efdb, for instance?

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:27):

(the last commit this morning where everything was fine)

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:27):

yep

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:27):

some sort of git reset

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:28):

OK, I am going to. Yet you agree that it is strange that there are so many red crosses, no? I mean, looking back at the history of the branch.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:28):

well once you mentioned that you like to ignore emails about failing CI, it stopped surprising me that the history has a lot of failing points

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:29):

It makes sense indeed.

view this post on Zulip Filippo A. E. Nuccio (Oct 15 2020 at 23:29):

I will try to go back to that commit and keep better track of what happens. Thanks so much for the help, in the meanwhile.

view this post on Zulip Kevin Lacker (Oct 15 2020 at 23:30):

no problem. good luck ;-)

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 00:00):

@KevinLacker I am sorry, I am unable to get the things done, can I ask for more help?

view this post on Zulip Heather Macbeth (Oct 16 2020 at 00:07):

@Filippo A. E. Nuccio I don't know how to help you myself, but you can summon Kevin by writing @**name_here** rather than just @...

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 00:08):

Hi Heather! Thanks, I have realised that after I typed, but also realised he's not connected any more. And am trying to figure out things without disturbing other people.

view this post on Zulip Julian Berman (Oct 16 2020 at 00:11):

I didn't follow the whole thread -- are you trying to figure out the git reset piece though or something bigger than that?

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 00:12):

Thanks-I ended up resetting to a previous commit and now things are working.

view this post on Zulip Julian Berman (Oct 16 2020 at 00:12):

If it's just that I can likely help, it sounded like from the scrollback that you want git reset --hard somecommit, which is a slightly dangerous command to run in general but if we get somecommit right it's OK.

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 00:12):

Thanks anyhow, but I grab the chance to ask why is it so dangerous

view this post on Zulip Julian Berman (Oct 16 2020 at 00:14):

Cool!

view this post on Zulip Julian Berman (Oct 16 2020 at 00:15):

Uh -- simply that it throws away commits -- normally the sequence of changes that are made stays "the same", but git reset --hard essentially moves you to a particular ref and doesn't preserve where you were

view this post on Zulip Julian Berman (Oct 16 2020 at 00:15):

(it will also, if you've pushed those commits elsewhere, now cause you to need to use git push --force, which will now make everyone else you may work with have some pain when they try to pull)

view this post on Zulip Julian Berman (Oct 16 2020 at 00:16):

So yeah in general you should think twice about using it but it sounded like it was what you needed here

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 00:16):

I see, it certainly makes sense. I sometimes feel that git is a bit "overcautious" but I guess it's me.

view this post on Zulip Kevin Buzzard (Oct 16 2020 at 06:39):

(sorry, was sleeping). simp is not usually the culprit when you find yourself in the situation that every time you type something you have to wait for ten seconds. The more likely culprits are tidy and finish. Other possibilities: you are writing one 200 line proof instead of ten 20 line proofs, or maybe you are using a machine with less than 8 gigs of ram. In fact I sometimes struggle even with 8 gigs.

view this post on Zulip Kevin Buzzard (Oct 16 2020 at 06:57):

Note that this is an independent issue to things taking one hour to compile (which should never happen unless you're editing files deep in the system).

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 10:10):

Thanks! I am really trying to figure out together with @Anne Baanen what is going on and I hope to have a more efficient system soon. BTW: I remember that during LFTCM2020 during a break-up room with @Sophie Morel you told us about "your favorite tactic" or something like this, which instead of inserting a have, replaces the current goal with something new, that you will later need to explain being equivalent to the old one. Do I remember correctly, what was this tactic?

view this post on Zulip Anne Baanen (Oct 16 2020 at 10:10):

Are you thinking of docs#tactic.interactive.convert?

view this post on Zulip Filippo A. E. Nuccio (Oct 16 2020 at 10:11):

Probably yes, thanks!


Last updated: May 08 2021 at 04:14 UTC