lake exe checkdecls on Windows

Stream: lean4

[Floris van Doorn]

I get an error when building lake exe checkdecls on Windows, with errors very similar to the previous errors with lake exe mk_all found here.
The error is when compiling checkdecls:

Floris@Dell-E MINGW64 ~/projects/carleson (master)
$ lake exe checkdecls
✖ [4/4] Building checkdecls
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\leanc.exe -o .\.\.lake/packages\checkdecls\.lake\build\bin\checkdecls.exe .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export -leanshared
info: stderr:
ld.lld: error: undefined symbol: l_Lake_findInstall_x3f
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)

ld.lld: error: undefined symbol: l_Lake_LakeOptions_mkLoadConfig
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)

ld.lld: error: undefined symbol: l_Lake_CliError_toString
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)

ld.lld: error: undefined symbol: l_Lake_loadWorkspace
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)

ld.lld: error: undefined symbol: l_Array_foldlMUnsafe_fold___at_Lake_serve___spec__1
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(l_main___lambda__1)

ld.lld: error: undefined symbol: initialize_Lake_CLI_Main
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(initialize_Main)

ld.lld: error: undefined symbol: l_Lake_defaultConfigFile
>>> referenced by .\.\.lake/packages\checkdecls\.lake\build\ir\Main.c.o.export:(.refptr.l_Lake_defaultConfigFile)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- checkdecls
error: build failed

(pinging @Utensil Song and @Sebastian Ullrich since found/fixed the issue last time)

[Sebastian Ullrich]

Does the fix at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/automatically.20generate.20ProjectName.2Elean/near/444253802 apply?

[Sebastian Ullrich]

This hasn't been addressed upstream yet, no

[Floris van Doorn]

Oh, I expected that there was a fix in Lean, not in mk_all. I'll check.

[Sebastian Ullrich]

I filed #5050 to keep track of it

[Floris van Doorn]

Yes, adding the weakLinkArgs := #["-lLake"] to the lean_exe options fixes this.

[Floris van Doorn]

lean4#5050

[Sebastian Ullrich]

Argh, I will never remember what prefix to use on what Zulip...

[Yaël Dillies]

Maybe we should have user-specific rules for linkifiers :grinning_face_with_smiling_eyes:

[Sebastian Ullrich]

I don't want to imagine what kind of edge cases that would introduce on e.g. quoting someone :) ...

[Floris van Doorn]

https://github.com/PatrickMassot/checkdecls/pull/3 @Patrick Massot

[Patrick Massot]

Did you check this doesn’t break the library on user-friendly OSs?

[Floris van Doorn]

No, that is not easy for me atm

[Yaël Dillies]

You can check by opening the PR in gitpod

[Yaël Dillies]

... although I'm not sure how to point to a non-master version of leanblueprint?

[Floris van Doorn]

I just checked that it still works in Github codespaces