うっかり brew upgrade

うっかり、Windows な仕事を引き受けてしまって。普通だったら絶対やらないんですけどね。大学にあるかと思った Windows の iso image は家に。

なので、VM を作るのは後まわし。で、もらった zip のファイルを見ると、

　　化け化けな日本語ファイル名が

だから、Windows は嫌なんだってば。前に、unzip command にpatchを当てた気が。もっとも、既に patch があるらしい。でも、zip を open して　 zsh な

function fixname1 {
foreach name ( "$@" )
new=$(perl -e print\ \"$name\\n\"\; | nkf -w )
mv ${==name} ${==new}
end
}

で治るらしい。== が何かとかは思い出したくもないですが、空白の扱い関係らしい。

まぁ、日本語ファイル名を使う人には、ベトナム語なファイル名で苦しむ呪いをかけておきました。

なんだが、unzip 作ろうと思った所で、うっかり、

　　brew upgrade

なんか結構溜まってる。いや、まだ high sierra なんですが。

で、ばっちり、agdaが動かない。だよな〜　

emacsが illegal opcode

これは、.elc を削除すればよいらしい。さらに、

~/.agda/default

の中の順番が重要らしい。standard-library を先にしろと。 さらに、

　　_≡_

が import されない。

open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )

で明示的に import する必要があるらしい。

ここまで来るまで少し時間がかかったが、でも、これでなんとかなったみたい。

3/13 には Agda の implementator な meeting があるので、これとは別に agda そのものも作らないとだめなみたい。うーん。なかなかつらいな。

いや、楽しみではあるんですが。

unzip なファイル? とりあえずは読めたが、また、明日。今日は、じんじんに呼び出されたので行ってきます。