Zulip Chat Archive

Stream: lean4

Topic: nightly updates

Arthur Paulino (Jun 26 2022 at 11:21):

Using leanprover/lean4:nightly-2022-06-25 is causing this error very often. A consistent (?) way to reproduce it is playing around with go-to-definition with ctrl+click. Please notice my CPU usage skyrocketing :rocket:
img

Arthur Paulino (Jun 26 2022 at 12:22):

More on this: I went to a definition to check the IO API and it downloaded a lean from a different toolchain. Maybe it's related

Wojciech Nawrocki (Jun 26 2022 at 18:11):

I have also been seeing this error.

Lars König (Jun 27 2022 at 10:15):

I also get this error a lot. @Sebastian Ullrich could this be caused by #1241? Reverting both commits fixed this for me (as far as I can tell).

Sebastian Ullrich (Jun 27 2022 at 10:28):

Yes, seems likely

Sebastian Ullrich (Jun 28 2022 at 11:54):

I wasn't able to reproduce this one yet, even though Leo said it also happened to him using Emacs. In any case, let's make it much easier to figure such things out on at least one platform: https://github.com/leanprover/lean4/pull/1258.

Sebastian Ullrich (Jun 28 2022 at 17:13):

Should be fixed with https://github.com/leanprover/lean4/pull/1259

Arthur Paulino (Jul 11 2022 at 12:25):

Hello!
I wanted to test today's nightly (2022-07-11) and no file could be compiled. I think there was something wrong with the Lake file. Has the lakefile.lean format changed again?

Sebastian Ullrich (Jul 11 2022 at 12:30):

Could you elaborate?

Sebastian Ullrich (Jul 11 2022 at 12:34):

I just updated one project without problems

Arthur Paulino (Jul 11 2022 at 13:09):

This happens with every file:
image.png
Might as well be some incompatibility with the vscode extension, idk

Gabriel Ebner (Jul 11 2022 at 13:11):

What error do you get on line 1?

Arthur Paulino (Jul 11 2022 at 13:18):

object file
'/home/arthur/.elan/toolchains/leanprover--lean4---nightly-2022-07-11/lib/lean/Lean/Environment.olean'
of module Lean.Environment does not exist

Sebastian Ullrich (Jul 11 2022 at 13:24):

Looks like a corrupted elan download

Sebastian Ullrich (Jul 11 2022 at 13:24):

Try removing and reinstalling the nightly

Arthur Paulino (Jul 11 2022 at 13:29):

Will try soon

Arthur Paulino (Jul 11 2022 at 15:24):

It was in fact a corrupted toolchain. Removing it and reinstalling solved the issue.
But it does ring a bell for a checksum verification since it seemed like a correct installation was being taken for granted when, in fact, my toolchain was corrupted

Nicolas Rouquette (Jul 17 2022 at 20:03):

The Yatima-Lang Compiler opens fine in vs code; it uses leanprover/lean4:nightly-2022-07-11.
With leanprover/lean4:nightly-2022-07-12 or leanprover/lean4:nightly-2022-07-17 there are two strange errors that I do not understand:
image.png
Can someone explain what is going on?

Mac (Jul 17 2022 at 20:05):

Name and Expr have too many parameters in their pattern match. The last parameter of each (e.g. Name.hash, Expr.data) was eliminated in favor of a computed field. Removing the trailing underscore in the pattern match should fix the issue.

Nicolas Rouquette (Jul 17 2022 at 20:09):

Ah, right! Thanks.

Last updated: Dec 20 2023 at 11:08 UTC