I accidentally changed a core file

Stream: general

[Kenny Lau]

I accidentally changed a core file and everything is now shit. I honestly don't know what to do.

[Kenny Lau]

Do I need to rebuild Lean?

[Keeley Hoek]

do you use elan

[Kenny Lau]

I don't

[Kevin Buzzard]

why not just download the binary again?

[Keeley Hoek]

tears
did you build it from source? download a zip distribution?

[Kenny Lau]

oh nvm I did the standard trick and it worked again

[Kenny Lau]

(standard trick = turning it off and on again)

[Kenny Lau]

I still think something has changed

[Kenny Lau]

This is what I do:

cd /c/
git clone https://github.com/leanprover/lean
cd lean
mkdir -p build/release
cd build/release
cmake -DCMAKE_BUILD_TYPE=RELEASE -G Ninja ../../src
ninja
cd /c/
git clone https://github.com/leanprover/mathlib
cd mathlib
/c/lean/bin/leanpkg build

[Kenny Lau]

I think it's alright

[Kevin Buzzard]

I think that script looks OK, I mean, it will just download a reasonable version of everything

[Keeley Hoek]

sure. if you mess up the standard library again, it is enough to just cd into the "lean" folder you already have sitting around and git reset --hard HEAD (and avoid the waiting)

[Kenny Lau]

do I need to restart Lean after that? @Keeley Hoek

[Keeley Hoek]

yes definitely

[Keeley Hoek]

and I guess it is best to cd into build/release and run ninja again, but not obligatory (and ninja should be very fast compared to normal)

[Kenny Lau]

oh ok