Zulip Chat Archive

Stream: general

Topic: Mathlib compiling despite oleans

Adam Topaz (Feb 19 2021 at 15:18):

I think my lean installation is broken :( (see animated gif). Mathlib seems to always want to compile even with a fresh project where oleans are present. Any help / suggestions toward diagnosing the issue would be much appreciated.
test.gif

Bryan Gin-ge Chen (Feb 19 2021 at 15:23):

Random thought: is it possible that you inadvertently made changes to core Lean?

Adam Topaz (Feb 19 2021 at 15:24):

I don't even know how I would go about doing that, so I don't think that's the issue.

Rob Lewis (Feb 19 2021 at 15:25):

You could have jumped to a definition in core and accidentally changed it, maybe

Kevin Buzzard (Feb 19 2021 at 15:26):

You right-click on a definition, it opens up a core Lean file, you sneeze and accidentally hit the space bar, then you close your VS Code.

Rob Lewis (Feb 19 2021 at 15:26):

Does elan update fix this? I'm not sure

Adam Topaz (Feb 19 2021 at 15:26):

Let me try.

Adam Topaz (Feb 19 2021 at 15:26):

How do I purge a version of lean using elan?

Adam Topaz (Feb 19 2021 at 15:26):

I can purge 3.26.0 and reinstall, I guess.

Kevin Buzzard (Feb 19 2021 at 15:27):

That was how Patrick managed to fix up someone else who had did this recently.

Adam Topaz (Feb 19 2021 at 15:28):

Do I just remove the .elan/leanprover-community-lean-3.26.0 folder? Or is there an elan flag that does this?

Bryan Gin-ge Chen (Feb 19 2021 at 15:29):

You can use elan uninstall, I don't know why it doesn't show up in the help...

Rob Lewis (Feb 19 2021 at 15:29):

I'd do it through elan. elan toolchain uninstall

Adam Topaz (Feb 19 2021 at 15:29):

Gotcha.

Adam Topaz (Feb 19 2021 at 15:30):

yeah it doesn't show up in the elan help menu

Rob Lewis (Feb 19 2021 at 15:30):

elan toolchain help

Rob Lewis (Feb 19 2021 at 15:30):

There are subcommands

Adam Topaz (Feb 19 2021 at 15:30):

Ah!

Bryan Gin-ge Chen (Feb 19 2021 at 15:30):

Right, I guess elan uninstall is just short for elan toolchain uninstall.

Rob Lewis (Feb 19 2021 at 15:30):

Yeah, it's a little confusing, heh

Adam Topaz (Feb 19 2021 at 15:33):

Okay, that seemed to fix it! Thanks everyone!

Sebastian Ullrich (Feb 19 2021 at 15:38):

There was a suggestion once to have elan make Lean's files read-only on installation, but it hasn't found somebody willing to implement it so far

Adam Topaz (Feb 19 2021 at 15:40):

I did look at the quotient.lean file recently... I must have sneezed like Kevin said :rofl:

Johan Commelin (Feb 19 2021 at 16:08):

Sebastian Ullrich said:

There was a suggestion once to have elan make Lean's files read-only on installation, but it hasn't found somebody willing to implement it so far

I just saw it is on the frontpage of my todolist again :oops:

Sebastian Ullrich (Feb 19 2021 at 16:12):

...how many pages does your todolist have that it has a frontpage?

Johan Commelin (Feb 19 2021 at 16:14):

5 items per page... its on my phone

Johan Commelin (Feb 19 2021 at 16:35):

https://github.com/Kha/elan/pull/27

Johan Commelin (Feb 19 2021 at 16:35):

This seems to compile. But I've never used rust before... so it might be complete garbage

Sebastian Ullrich (Feb 19 2021 at 16:44):

So you didn't test it?

Kevin Buzzard (Feb 19 2021 at 16:54):

he never tested his perfectoid spaces either

Johan Commelin (Feb 19 2021 at 17:43):

Sebastian Ullrich said:

So you didn't test it?

Nope :see_no_evil:

Last updated: Dec 20 2023 at 11:08 UTC