lake problem, perhaps macos specific?

Stream: lean4

[Scott Morrison]

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]

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]

@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]

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]

Yep, just verified -- that is it.

[Mario Carneiro]

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

[Scott Morrison]

Presumably the hash calculation is not actually reading the executable.

[Mac]

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

[Scott Morrison]

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

[Mac]

yeah, that is what I am thinking

[Mac]

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]

so I am actually a little stumped

[Mac]

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]

@Sebastian Ullrich any idea what is going on here?

[Sebastian Ullrich]

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

[Mac]

@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]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Mac]

@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]

dylib, but yes

[Mac]

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