Wrong path in 2.4 "Meow!"

[lunaticabs]

Please quote the text that is incorrect:

echo "It works!" | ./build/bin/feline

In what way is this incorrect?

The path in here should be ./.lake/build/bin/feline. Because the current path should be in root directory in a project folder in general.

[david-christiansen]

The book is currently targeting a version of Lean that's a couple of months old. But this will indeed need fixing the next time I update it to the current version (which needs doing soon, much has changed!).

Thanks!

[fpottier]

The problem still to be still present. Section 2.3 says: After a number of build commands scroll by, the resulting binary has been placed in build/bin. Running ./build/bin/greeting results in Hello, world!. The prefix .lake/ is missing.

[david-christiansen]

This is now fixed in the update to Lean 4.18 that just came out. Thank you!