lake build do not produce a binary

Stream: new members

[Marco Maggesi]

Hello! I'm new to Lean. I'm reading https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html
I have a problem: After

lake new greeting
cd greeting
lake build

I would expect to find a binary greeting in ./build/bin
The building completes without errors, but no file is created.
Any clue? Thanks for help

[Marco Maggesi]

BTW: lake exe says **error:** missing executable target

[Marco Maggesi]

And lakefile.lean looks exactly as listed in https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html.

[Ruben Van de Velde]

lake exe greeting seems to work

[Mauricio Collares]

$ .lake/build/bin/greeting
Hello, world!

(but Ruben's suggestion is better)

[Mauricio Collares]

Note that Functional Programming in Lean was tested with Lean 4.1.0. You may encounter other small changes if you use a newer Lean version. If you create the project with lake +leanprover/lean4:v4.1.0 new greeting, you will be using Lean 4.1.0. If you prefer to use the most recent version of Lean, then searching Zulip should be enough to find explanations for the relevant changes (for example, you will need to replace by simp by by decide or by by simp +decide in a few places), but feel free to ask if you don't find what you're looking for. Also, see this comment by the book author for more details on when the book will be updated.

[Marco Maggesi]

Both suggestions works.
Thanks a lot @Ruben Van de Velde and @Mauricio Collares !