Building a basic project

Stream: new members

[Aditya Siram]

I managed to build and run a basic Lean project using a source compiled lake, the binary prints Hello, world! as expected but there were some build time warnings I couldn't understand:

> lake init foo
warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
> lake build
 [0/6] Building Foo.Basic
[1/6] Compiling Foo.Basic
[1/6] Building Foo
[2/6] Compiling Foo
[2/6] Building Main
stderr:
cc: warning: /usr/lib/libgmp.so: linker input file unused because linking not done
stderr:
cc: warning: /usr/lib/libgmp.so: linker input file unused because linking not done
[5/6] Compiling Main
stderr:
cc: warning: /usr/lib/libgmp.so: linker input file unused because linking not done
[6/6] Linking foo

[Alex J. Best]

I've also seen these warnings recently (when building mathlib iirc, on ubuntu)