Zulip Chat Archive

Stream: general

Topic: I accidentally changed a core file


Kenny Lau (Sep 06 2018 at 14:02):

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

Kenny Lau (Sep 06 2018 at 14:03):

Do I need to rebuild Lean?

Keeley Hoek (Sep 06 2018 at 14:06):

do you use elan

Kenny Lau (Sep 06 2018 at 14:06):

I don't

Kevin Buzzard (Sep 06 2018 at 14:06):

why not just download the binary again?

Keeley Hoek (Sep 06 2018 at 14:06):

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

Kenny Lau (Sep 06 2018 at 14:09):

oh nvm I did the standard trick and it worked again

Kenny Lau (Sep 06 2018 at 14:09):

(standard trick = turning it off and on again)

Kenny Lau (Sep 06 2018 at 14:11):

I still think something has changed

Kenny Lau (Sep 06 2018 at 14:12):

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 (Sep 06 2018 at 14:15):

I think it's alright

Kevin Buzzard (Sep 06 2018 at 14:17):

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

Keeley Hoek (Sep 06 2018 at 14:23):

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 (Sep 06 2018 at 14:43):

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

Keeley Hoek (Sep 06 2018 at 14:44):

yes definitely

Keeley Hoek (Sep 06 2018 at 14:47):

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 (Sep 06 2018 at 14:48):

oh ok


Last updated: Dec 20 2023 at 11:08 UTC