## Stream: new members

### Topic: Stopping VSCode from recompiling mathlib

#### 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.

#### Patrick Massot (Oct 04 2020 at 10:00):

Why did you edit the leanpkg.toml?

#### 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.

#### Patrick Massot (Oct 04 2020 at 10:27):

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

#### Patrick Massot (Oct 04 2020 at 10:27):

I did exactly what you wrote and everything works fine.

#### Patrick Massot (Oct 04 2020 at 10:28):

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

#### 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)?

#### 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 !

#### 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?

#### 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.

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:20):

How do you kill your server?

#### 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.

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:20):

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

#### Kevin Lacker (Oct 15 2020 at 22:20):

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

#### 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.

#### 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

#### 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

Right

#### 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?

#### Kevin Lacker (Oct 15 2020 at 22:24):

try just typing "Lean" and looking through the options

#### Bryan Gin-ge Chen (Oct 15 2020 at 22:24):

Oh sorry, it's ctrl+shift+p

#### 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

#### 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

#### 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)

#### Scott Morrison (Oct 15 2020 at 22:27):

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

#### 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.

#### 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

#### 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.

#### Scott Morrison (Oct 15 2020 at 22:29):

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

Hopefully less!

#### 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?

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

I am working on a branch of the main repo

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:30):

Scott Morrison said:

Hopefully less!

Let me try again!

#### Kevin Lacker (Oct 15 2020 at 22:31):

try running leanproject get-cache before building

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:32):

I am going to, give me 30 sec

#### 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

#### Bryan Gin-ge Chen (Oct 15 2020 at 22:33):

Which file(s) are you editing, exactly?

#### Bryan Gin-ge Chen (Oct 15 2020 at 22:33):

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

#### 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)

#### 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

#### Bryan Gin-ge Chen (Oct 15 2020 at 22:34):

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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:35):

Bryan Gin-ge Chen said:

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

#### 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 .

#### 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.

#### 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.

#### 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...

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:38):

(and it looks very much as before)

#### 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

#### 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.

#### 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".

#### 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?

#### 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)

#### 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 ;-)

#### 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

#### 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.

#### 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.

#### 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.

#### Bryan Gin-ge Chen (Oct 15 2020 at 22:48):

But that looks to be difficult at this point.

#### 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?

#### 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

#### 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.

#### 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.

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:50):

And what do I do in that case?

#### 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.

#### Kevin Lacker (Oct 15 2020 at 22:50):

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

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:51):

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

#### Kevin Lacker (Oct 15 2020 at 22:52):

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

#### Kevin Lacker (Oct 15 2020 at 22:52):

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

#### Kevin Lacker (Oct 15 2020 at 22:52):

it looks like you did a merge which failed

#### 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"

#### Kevin Lacker (Oct 15 2020 at 22:53):

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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:53):

But how is it possible that I changed 313 files?

#### 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

#### 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?

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:54):

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

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:55):

worked a bit, then commit+pushed.

#### Scott Morrison (Oct 15 2020 at 22:56):

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

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:57):

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

shrug

#### Filippo A. E. Nuccio (Oct 15 2020 at 22:57):

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

#### Scott Morrison (Oct 15 2020 at 22:57):

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

#### Scott Morrison (Oct 15 2020 at 22:57):

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

#### 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

#### Scott Morrison (Oct 15 2020 at 22:58):

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

#### Kevin Lacker (Oct 15 2020 at 22:58):

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

#### 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

#### Scott Morrison (Oct 15 2020 at 22:58):

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

#### 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

#### 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

#### Kevin Lacker (Oct 15 2020 at 22:59):

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

#### Kevin Lacker (Oct 15 2020 at 22:59):

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

#### Kevin Lacker (Oct 15 2020 at 22:59):

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

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:00):

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

#### Kevin Lacker (Oct 15 2020 at 23:00):

there are several layers to this answer

#### 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

#### Scott Morrison (Oct 15 2020 at 23:01):

Do you ever run leanproject up?

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:01):

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

#### 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

#### 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?

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:06):

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

#### 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

#### Kevin Lacker (Oct 15 2020 at 23:07):

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

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:08):

Yes - very bad idea, I suppose.

#### 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

#### 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

#### 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

#### 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

#### 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?

#### 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

#### Kevin Lacker (Oct 15 2020 at 23:13):

I mean that you committed the change that broke the build

#### 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

#### Kevin Lacker (Oct 15 2020 at 23:14):

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

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:15):

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

#### 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.

#### 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

#### 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

#### 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..

#### 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.

#### Kevin Lacker (Oct 15 2020 at 23:20):

restart the lean server

done

orange bars...

#### Kevin Lacker (Oct 15 2020 at 23:21):

you're sure you're on master?

#### 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'.

git pull

done

#### Kevin Lacker (Oct 15 2020 at 23:22):

leanproject get-cache

going on...

done

#### Kevin Lacker (Oct 15 2020 at 23:23):

now see if things compile

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:23):

now yes, everything nice and smooth

#### Kevin Lacker (Oct 15 2020 at 23:24):

great. now you can go fix your borked branch

#### 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".

#### 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?

yeah

#### 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.

#### Kevin Lacker (Oct 15 2020 at 23:26):

mmm no you should not need to merge anything

#### Kevin Lacker (Oct 15 2020 at 23:26):

all you're doing is rolling back your branch

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:27):

(the last commit this morning where everything was fine)

yep

#### Kevin Lacker (Oct 15 2020 at 23:27):

some sort of git reset

#### 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.

#### 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

#### Filippo A. E. Nuccio (Oct 15 2020 at 23:29):

It makes sense indeed.

#### 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.

#### Kevin Lacker (Oct 15 2020 at 23:30):

no problem. good luck ;-)

#### 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?

#### 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 @...

#### 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.

#### 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?

#### Filippo A. E. Nuccio (Oct 16 2020 at 00:12):

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

#### 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.

#### Filippo A. E. Nuccio (Oct 16 2020 at 00:12):

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

Cool!

#### 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

#### 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)

#### 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

#### 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.

#### 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.

#### 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).

#### 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?

#### Anne Baanen (Oct 16 2020 at 10:10):

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

#### Filippo A. E. Nuccio (Oct 16 2020 at 10:11):

Probably yes, thanks!

Last updated: May 08 2021 at 04:14 UTC