【Lean4】Lakeで立ち上げたプロジェクトをビルドする

lake new [package_name]
でプロジェクトを作成して
cd [package_name]
でフォルダを移動して
lake build
でたぶんデフォルトのプロジェクトがビルドされる。
ビルドされたファイルは、
\build\bin\
にあるから、ターミナルから動かすと、
Hello, world!
と出てくれる。

本当はもっと高度なことがしたかったが、初歩の初歩で躓いて
ここまでしかできなかった。