2023.07.26
https://www.youtube.com/watch?v=yTJi5xI1TrI
最近
思った
未だに命題論理の段階で止まってるんですか？と言われれば泣きながらそうですと答える他ない メモ
lean-toolchainを見ずに，flake.nix及び固定されたflake.lockでLean 4のバージョンを固定している気がする これによって毎回Leanのビルドが走り，大変なことになる
よって現段階ではやめたほうが良いと思う．
また依存関係をわざわざNix側でも固定する必要が多分あり，しかも依存先にNix Flakesがない場合は完全に詰むので…（ここはちゃんと調査していない） おとなしくelan/Lakeを使ったほうがいいというのが現時点の回答になる（多分）