Zulip Chat Archive

Stream: lean4

Topic: lake problem, perhaps macos specific?


Scott Morrison (Nov 11 2021 at 05:50):

I reported an issue with lake not rebuilding after modifying lean-toolchain, but unfortunately it doesn't reproduce for @Mac. I'm wondering if it could be an OS issue. Is there someone with a macos system who could test it out for us?

Scott Morrison (Nov 11 2021 at 05:51):

On any machine with elan you should be able to:

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
git checkout 64f9c43eb9a75fb4c5989ac711623d06e9696e60
lake --version # says: Lake version 3.0.0-pre (Lean version 4.0.0-nightly-2021-11-07)
lake build
echo "leanprover/lean4:nightly-2021-11-10" > lean-toolchain
lake --version # says: Lake version 3.0.0-pre (Lean version 4.0.0-nightly-2021-11-10)
lake build  # returns immediately

The problem I'm seeing is that the final lake build returns immediately, whereas Mac is seeing the correct behaviour, that lake rebuilds the library.

Mac (Nov 11 2021 at 06:10):

@Scott Morrison your question of whether it was OS specific made me curious and I tried it on WSL and now I can reproduce the issue!

Mac (Nov 11 2021 at 06:13):

Currently, I rebuild between versions by rebuilding whenever the hash of lean changes. I think the problem here is that the hash isn't changing on non-Windows systems

Mac (Nov 11 2021 at 06:22):

Yep, just verified -- that is it.

Mario Carneiro (Nov 11 2021 at 06:25):

how is it possible for lean --version to change without the hash of the executable changing?

Scott Morrison (Nov 11 2021 at 06:30):

Presumably the hash calculation is not actually reading the executable.

Mac (Nov 11 2021 at 06:35):

@Scott Morrison nope, the hash calculation does hash the entire executable's binary contents.

Scott Morrison (Nov 11 2021 at 06:37):

oooh.. maybe this is some weirdness about how elan delegates.

Mac (Nov 11 2021 at 06:37):

yeah, that is what I am thinking

Mac (Nov 11 2021 at 06:38):

or, more accurately was thinking, the problem is that I am hashing the actually executable within the ttoolchain's bin dir, not the delegator in elan's bin dir.

Mac (Nov 11 2021 at 06:39):

so I am actually a little stumped

Mac (Nov 11 2021 at 06:46):

I though maybe I was just really unlucky and my short 64-bit hash was encountering clashes, but no. For me, the binaries for nightlies 2021-11-05, 2021-11-07, and 2021-11-10 (i.e., those at <home>/.elan/toolchains/<toolchain>/bin/lean) all have the same SHA256 hash.

Mac (Nov 11 2021 at 06:46):

@Sebastian Ullrich any idea what is going on here?

Sebastian Ullrich (Nov 11 2021 at 06:49):

Ah, I thought you were using the git hash? Hashing lean is not really meaningful without also hashing libleanshared.

Mac (Nov 11 2021 at 06:53):

@Sebastian Ullrich using the githash was and idea of mine, but for now I had just been hashing the binary. Once reason I did this is because it changes to docs and the like would not invoke unnecessary rebuilds. Would hashing lean + libleanshared be sufficient? Or do I need to / should I use the githash?

Sebastian Ullrich (Nov 11 2021 at 06:55):

It should be sufficient. Until we further mix it up, but that shouldn't happen anytime soon.

Sebastian Ullrich (Nov 11 2021 at 06:56):

Just remember that the lib is in bin/ on Windows but lib/lean/ otherwise

Sebastian Ullrich (Nov 11 2021 at 06:57):

Not sure how often we have pure-docs nightlies though, and how often people update between them. It might not be worth it.

Mac (Nov 11 2021 at 07:00):

@Sebastian Ullrich quick question, because I don't remember, does libleanshared have a dll extension on Windows, dynlib on Mac, and so otherwise?

Sebastian Ullrich (Nov 11 2021 at 07:00):

dylib, but yes

Mac (Nov 11 2021 at 07:01):

oops I had been misspelling it in Lake then. XD -- otherwise, good to know!


Last updated: Dec 20 2023 at 11:08 UTC