閃光のハサウェイ

いや、前作見てなくて。一応、最初に「前作は」みたいなのがくっついているんだが、よくわからんまま

まぁ、でも、見てても同じだろうな

女の子がからむと、こんな感じでしょ的な話でもある。でも、そこに予知能力みたいなのいれるの?

あんまりよろしくない。まわりがちやほやするのも含めて

絵がきれいってのは、そうだったかも。戦闘シーンのぴこんぴこんも、まぁ、それっぽいかな

桜

風邪ひいてたり、寒かったりで、あんまり桜はみなかったんだけど、今日は

　暑い。天気がよい

なので、結構、桜をみました

agda 2.9 の続き

% agda --version
Agda version 2.8.0

% ~/.local/bin/agda --version
Agda version 2.9.0

agda Sheaf.agda 410.01s user 3.28s system 99% cpu 6:54.04 total
~/.local/bin/agda Sheaf.agda 342.05s user 2.26s system 99% cpu 5:44.73 total
~/.local/bin/agda -j7 Sheaf.agda 574.62s user 93.03s system 117% cpu 9:27.13 total

これは、並列処理すると遅くなる感じ。でも、新しい方が、ちょっと速いのか

~/.local/bin/agda --warning=UnusedImports Sheaf.agda

これは、一応、動いているらしい

agda 2.9

agda で unused module import を見つけたい。どうも agda-unused という command はあるらしい

なんだが、agda そのものでやるべきだよね? と思ってさがしてみると

agda-2.9

にはあるらしい。なんだが、homebrew では 2.8.0.1 まで。2.9 だと並列処理も入る

なので、開発 version にいく気になった

で、ghcup ってので version わけすると chatgpt はいうのだが、defalut は9.6。agda が使っているのは9.12.2

まぁ、

1039 21:33 ghcup list
1040 21:35 ghcup install ghc 9.12.2
1041 21:38 ghcup set ghc 9.12.2

で、良いらしい

いままで、一番スムースかも

動くかどうかは、これから

風邪でおとなしくしてます

熱はないんだが、咳がな

先週の木曜から

Yoga

近所のイタメシ屋にあった怪しいのみもの

ネクターみたいなもの。それほど甘くない

ドラゴンズ

なんか、北谷に来てるのね

AEON の中のガチャガチャが、ドラゴンズのものになってました