Binaries are not relinked when Lean version changes

[gebner]

To reproduce:

lake +leanprover/lean4:nightly-2022-03-01 new linktest
cd linktest
lake build
echo leanprover/lean4:nightly-2022-03-02 >lean-toolchain
lake build

Note that the second lake build does not rebuild build/bin/linktest.

[tydeu]

@gebner Sorry, but I can't reproduce this. For me, running the following shell script:

set -ex
rm -rf linktest
lake +leanprover/lean4:nightly-2022-03-01 new linktest
cd linktest
lake build
echo leanprover/lean4:nightly-2022-03-02 > lean-toolchain
lake build

Produces (on Windows 10 MSYS2):

++ rm -rf linktest
++ lake +leanprover/lean4:nightly-2022-03-01 new linktest
++ cd linktest
++ lake build
> LEAN_PATH=.\build\lib <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-01\bin\lean.exe .\.\Linktest.lean -R .\. -o .\build\lib\Linktest.olean -i .\build\lib\Linktest.ilean -c .\build\ir\Linktest.c
> <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-01\bin\leanc.exe -c -o .\build\ir\Linktest.o .\build\ir\Linktest.c -O3 -DNDEBUG
> LEAN_PATH=.\build\lib <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-01\bin\lean.exe .\.\Main.lean -R .\. -o .\build\lib\Main.olean -i .\build\lib\Main.ilean -c .\build\ir\Main.c
> <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-01\bin\leanc.exe -c -o .\build\ir\Main.o .\build\ir\Main.c -O3 -DNDEBUG
> <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-01\bin\leanc.exe -o .\build\bin\linktest.exe .\build\ir\Main.o .\build\ir\Linktest.o
++ echo leanprover/lean4:nightly-2022-03-02
++ lake build
> LEAN_PATH=.\build\lib <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-02\bin\lean.exe .\.\Linktest.lean -R .\. -o .\build\lib\Linktest.olean -i .\build\lib\Linktest.ilean -c .\build\ir\Linktest.c
> <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-02\bin\leanc.exe -c -o .\build\ir\Linktest.o .\build\ir\Linktest.c -O3 -DNDEBUG
> LEAN_PATH=.\build\lib <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-02\bin\lean.exe .\.\Main.lean -R .\. -o .\build\lib\Main.olean -i .\build\lib\Main.ilean -c .\build\ir\Main.c
> <elan-home>\toolchains\leanprover--lean4---nightly-2022-03-02\bin\leanc.exe -c -o .\build\ir\Main.o .\build\ir\Main.c -O3 -DNDEBUG

That is, changing the toolchain does cause a rebuild.

[gebner]

That is, changing the toolchain does cause a rebuild.

Right, it causes a rebuild. Except for linktest.exe, which is not updated.

[tydeu]

@gebner Oops, I missed that! You are right.