Where is the place for noob questions like fixing install?

Stream: general

[bgl gwyng]

Hello I'm new to lean and also new to Zulip. It's a bit confusing to me where I should ask very basic questions.

[Bolton Bailey]

You can ask here, or (as Patrick recently pointed out) in the new members channel.

[bgl gwyng]

Thanks!

I'm trying to find out why lake build failed with the following error message

✖ [8/8] Building «lean-playground»
trace: .> gcc -o ././.lake/build/bin/lean-playground ././.lake/build/ir/Main.c.o.export ././.lake/build/ir/LeanPlayground/Basic.c.o.export ././.lake/build/ir/LeanPlayground.c.o.export -L /nix/store/1n9nj8wdk92ssmp0cfqgdj3bhs52d740-lean4-4.18.0/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lstdc++ -lLake  /nix/store/h89gh873zcsfjjp7w0f2mw357np32br7-gmp-with-cxx-6.3.0/lib/libgmp.so -L/nix/store/k7ahgbgfjhw3lr8g8vdpxns2y538h3zg-libuv-1.50.0/lib -luv -lm -ldl -pthread
info: stderr:
/nix/store/s40y31bdn82sj6daaxid1bn3p7la03lv-binutils-2.43.1/bin/ld: cannot find : No such file or directory
collect2: error: ld returned 1 exit status
error: external command 'gcc' exited with code 1
Some required builds logged failures:
- «lean-playground»
error: build failed

I tested that the first gcc ... run and it succeed. So I'm suspecting lake did something more after running gcc and it failed. What was it then?
https://github.com/bglgwyng/lean-playground
Here is my repo and what I did is almost just lake new and lake build.

[bgl gwyng]

When I ran gcc -o ././.lake/build/bin/lean-playground ... It successfully emitted outputs in .build directory and the binaries worked well also.

[Sebastian Ullrich]

Your Lean is improperly packaged. Please use elan (also in Nixpkgs) to install Lean.

[bgl gwyng]

Thanks! Just removing pkgs.lean4 from buildInputs worked!