- cat lean-toolchain
- elan toolchain list
- elan show だとダウンロードが始まる
- cat lakefile.lean
- cat .git/HEAD デタッチされているか？
- git branch
- git rev-parse カレントブランチ
- git tag
- git rev-parse $(git tag | tail -1)
- git log --oneline
- git rev-parse $(git log --oneline | head -1 | cut -f1 '-d ')
- git checkout コミットのハッシュ
- cat lake-manifest.json | jq -c '.packages[]|.git|[.name, .url, .rev]'
- /bin/find -name '*.c' -or -name Makefile
最近のパッケージでは次があるはず。
- lean-toolchain
- lakefile.lean
- lake-manifest.json
これだけ揃っていればビルドできる可能性が高い。
外部Cソースをコンパイルするには cc コンパイラードライバーが、標準的なCLIで使える必要がある。gccでも大丈夫かもしれないが、clangが安心だろう。
