lean4のプロジェクト作成、既存leanファイルの配置,build,実行を一括でやるスクリプト

コード
https://github.com/xiangze/all_in_one_lean4_project_geneator

https://zenn.dev/articles/24d33f3ebabfa0
でもまだ完全ではなく、Project名の大文字小文字、lakeの実行スクリプトの配置場所などで混乱し、ChatGPTですら一発で動かせなかったのでまとめスクリプトを作りました。オプションでmathlib仕様不使用を選択可能、外部leanファイル配置のオプションで選択可能です。

Makefileを使えばビルドのみ、実行のみもできるようになります。

使い方

Usage: ./all_in_one_generator.sh [-m|--mathlib] [--src FILE] [--as ModuleName] <project_name>

  -m, --mathlib     : mathlib を依存に追加（cache get も実行）
  --src FILE        : 外部 Lean ファイルをプロジェクトへ取り込み
  --as ModuleName   : 取り込み先モジュール名（既定: Math → Math.lean）
  <project_name>    : プロジェクト名（実行ターゲット名は正規化されます）

使用例

• without mathlib

./all_in_one_generator.sh proj

• with mathlib fibonacci.leanを読み込み

./all_in_one_generator.sh proj1_math -m --SRC fibonacci.lean

Peoject名/Basic.leanは必要ないらしいです。

上記のプロジェクトを実行してもプロジェクト名/Basic.leanというファイルは生成されないのですが問題ないのでしょうか
ChatGPT:思考時間: 46s

結論：問題ありません。
project名/Basic.lean は Lake が自動生成する標準ファイルではありません。多くの教材や雛形で “自分のライブラリ用の最初の1枚” として <Lib名>/Basic.lean を置く慣習があるだけで、作らなくてもプロジェクトは正常に動きます（Main.lean だけで実行できます

試行錯誤
https://chatgpt.com/share/68b46b77-2930-8008-bc04-b4347eab2ea3

Reference

https://speakerdeck.com/unaoya/zheng-ming-zhi-yuan-xi-leanniru-men-siyou?slide=40

ChatGPTの書いたコードはちゃんとの動くか

https://zenn.dev/xiangze/articles/1f7cc0e71b4959

https://zenn.dev/xiangze/articles/d6b5cc490d5007

月$2000プランではimportから関数の名前空間までlean3とごっちゃになっていて指摘しても直してくれません。

ためになる本

https://www.lambdanote.com/products/leanbook