Java を OS Xの.app に

ずーっと前に誰かにやってもらったことがあったな。TreeVNC は Java でかかれているので、

　　Java install して java -jar TreeVNC.jar で動かす

とかやっていたんですが、自分ではそれが普通だとしてもね。Java 入れるの拒否られたり。

gradle osx .app あたりでググると、

　　https://github.com/crotwell/gradle-macappbundle/wiki/Intro

というわけで、gradle に数行付け加えるだけで作ってもらえます。らくちん。plugins は gradle file に先頭にないとだめらしい。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Applications/TreeVNC/rev/b26c934c2bfb

おっと、icon 作らないとだめか。OmniGraffle にMac Icon用のキャンバスがあるので、それで作って、png で export 。それを、

　　https://iconverticons.com/online/

の Web service で変換すればよいらしい。Xcode にそういうコマンドがあるべきなんじゃないの?

これで配布用の dmg も作れるのか。えらいな。

QNAP 6TB

全部入れ替えるのはお金がないので2本だけ6TBに。本当は8TBにしたかったんだけど、GoodWill に在庫がないとうので。なんか12TBまで出るんだって?

なんですが、スムーズにはいかず。

　　外付けUSB HDD case で6TBをQNAPに接続して
　　設定に出てくるので ext4 で初期化

までは良かったんですが、

　　2台目をつないで初期化したら、全部見えなくなった

あれ? で、いろいろやるんだけど、1本目がたまに見えるぐらい。そういえば

　　firmware update あるな

で update したんですが、どうにもこうにもだめ。OS X側では問題なくつながる。仕方がないので、

　　QNAPのを一本外して、そこに6TBを入れる

で認識しました。HDD CaseとQNAPの相性かなあ。で、中で rsync でコピーして、コピーしたのを外す。そこに6TB二つ目をさす。なんだが、

　　volumeを作れない

ぐ。なにそれ。どうも、さぼって電源切って、HDDを抜くってのをやったのが悪いらしい。ちゃんとメニューから外すってやらないとだめか。でも、

　　reboot で認識

しました。

なのだが、抜いたHDDが system だったらしく、

　　これまでに入れた zsh とか perl とかがパァ

ひどい。で、opkg ってのをいれれば良いんですが、これもいれ方が前と違う... いろいろ飛んだけどまあいいか。

4本をRAID5にしてしまうと、こういう部分的に入れ返るってのは微妙。できるんだろうけど。本当は、

　　QNAP筐体を二つ用意してミラーする

ってのが良いんでしょうけど、お金がかかるのがね。QNAPのZFSってのはどうなんだろう?

でも、もうしばらくすれば、Cloud Storageに10TB置いても問題なくなると予想します。

着替え

通勤途中で、うっかり ingress の寄り道とかしないでも、

　　汗びっしょり

になったりするので、着替えを持ってきてます。ますが、

　　パンツだけない

ぐ。適当にタオルではさんで乾かして我慢するか。

水泳を再開したいと思うけど、なかなか機会がつかめない。8月は9日ぐらいから東京か。それも、まだ決めてません。

GoodWill でお買い物

HDDとかUSB切り替え器とか、細かいものは自分でかってしまった方が事務の方も楽らしい。

でも、いろいろないものが。

　　USB Felica Reader 割と普通に見かけたんだけどな
　　USB C MBP用電源 (これは探す所が違ってるな

いくつかUSB Cなものも見かけましたが、まだ来てない感じだな。

だいたい Macユーザは、まだ広まってないコネクタをいろいろ使う羽目になるんだよな。いつものこととはいえ。

FBのボタンの位置

相変わらず、卒業生が残していった Java のソースと格闘してます。comit miss で時間取られることが多い。しくしく。

それとは菅家ないく、

　　FacebookのURLは、Safari で開ける

ことにしてます。そうすれば Safari 側に履歴が残るし、MBPとも連携できるし。Echofon には「リンクをSafariで開ける」オプションがあるので、他のアプリも見習って欲しい。つうか、履歴が共通であれば文句はないんだが。

なのだが、

　　Facebok iPhone アプリからだと、Open in Safari が上のメニューにある時と、下のメニューにある時の二つのケースがある

Twitterだと上になるのかな? ださいこと止めて欲しいなぁ。Share menu があるんですが、そんなの使わんし。それが上に出たり、下に出たりするらしい。

Share menuを使わないのは、share した履歴が、FBにしか残らないから。FBの検索性の悪さは半端じゃない。なので、投稿はmh/blogger経由。こうすれば、Bloggerの検索が使えるし、ATOM経由でバックアップも取れます。

昔は Blogger との自動連携があったのにな。Twitter は、たまにArchive取ってきてます。EvernoteにWeb貼る人もいるけど、BlogとかTwitterに残すので僕は良いかな。

iTunes Match

Apple Music は使ってません〜 なんか人に Music FM 勧められたが... それはともかく、

　　コピーしなくても登録すると upload したものが全部聞ける

ってのは良いですね。61GBぐらい持っているらしいけど、そのうち聞くのは1/10もないだろうかなぁ。

Matchしたら256Kbpsがdown loadできるとかあったけど、落ちてきたのは .mp3 だ。ちょっと話違う感じ。まぁ、文句はないですが。

写真の方は37GBか。そっちも、Google Photos に上げてしまうのが簡単な気がする。

その二つがなければノートPCの移行は極めて楽。それでも380GB使ってるな。

iCloud は家族割引ができたら考えます。MobileMe にはあったのに。

辞書

昔々、電子ブックという8cm CDROM baseの本があってな。そのフォーマットを解析するってのがちょっと流行ってました。

で、それを、

　　Keyword Description

形式のファイルにして、sort してやって、Perlで書いたファイルの2分探索を使うと、CUIな辞書の出来上がり。

今は、OS XにOEDとか付いてるし。でも、コマンドラインから使えるのは便利かな。look.pl ってのには、

　　# This legacy library is deprecated and will be removed in a future
　　# release of perl.

とか書いてあるのだが、代わりのものがなんなのかが良くわからないんだよな。まあ、sqlite で書き直しても良いけど、

　　別に DB にするほどのものじゃないよね?

普通のファイルなので grep して別に問題ない。全文検索させても良いが、数メガから数十メガだと別に grep で問題ないらしいです。

広辞苑とかは dserver 経由で使っていたらしいけど、さすがに、それは使わないな。動かそうと思えば動くのだろうけど。そこまでやるならググるよな。普通。

Evernote vs OneNote

iPhone 3G 時代から使っているEvernote。悪くないですね。研究とか仕事では使わない。いや、メモぐらいには使うかな。初期のiPhoneは写真の公開とかメモの同期、そして音声メモもなくて、それを Evernote が全部可能にしていたので、必須アプリの一つだったと思います。Apple はEvernoteを買収するべきだったと思う。そして、iTools/.Mac/MobileMe/iCloundをEvernoteで統一しても良かったんだよね。iCloundの次は何?

なんですが、当のEvernoteは迷走して低迷。現在では特にパッとしたアプリとは言いづらい。対抗馬は、

　　　MSのOneNote

でしょう。昔はOffice 365使ってないとだめとかあったらしいが、今は無料! Evernoteは月60MBまで無料なので、OneNoteの方が微妙に勝ってるかも。

昔、入れたんだよな。Evernoteからの移行ツールがあるらしく、試してみようかなと思ってます。

一つの理由は、

　　　Evernoteのbackupは自明じゃない

ってのがあるな。OS X 上のEvernote.appを使うと、local copy は取れるようなんですが、backup とはちょっと違う。ググるとノート一つ一つコピれみたいなことが書いてある。それは、ちょっとなぁ。

今朝も、Evernote ちょっと落ちてたみたいだし。OS X上のEvernote.app を入れたら60MBの制限に引っかかったので、この機会にOneNoteに移るってのはありだろうなぁ。

自分のカラオケの持ち歌書いたり、Ingressのpass code取っておいたり、比較的どうでもいい会議のメモとか。あとは名刺ですね。写真撮ってEvernoteに入れるだけ。名刺が容量食ってるんだよな。

当のEvernoteは「名刺管理に使えます」とか宣伝しないんだよね。まぁ、確かに 3G の頃はカメラの解像度が低くて無理だったんですが。

まぁ、昔のよしみがあるからな。Evernote がんばれと言っておこう。

　　　https://evernote.com/

パイオニア AV アンプ

SCLX87で、この前、iPhoneから音がでるように設定するのに妙に苦労した奴ですが... (LANがおかしかった)

BDレコーダの音が出ないというメッセージが。入力切替なんじゃないのと放置してたんですが、家に戻って見てみると、確かに出ない。

アンプの電源を切ってスルーにしてもテレビから音声は出ない
iPhoneは鳴る
HDMIでつながってる機器の音声はすべてだめ(PS3とか)

ってわけで行き詰まったんですが、

アンプの電源リセット

で治りました。'まぁ、そんなもんだよね。スルーで出ないってのは酷いとは思った。

スカパーのアンテナ

一つのアンテナから二本のスカパーの線とBSの線が出てるのを使っているんですが、スカパーの片方が映らなくなって。アンテナケーブルだろうなと思って見てみると、案の定、サッシから入れる平らな線のアダプタの所で芯線が折れてる。外にある部分だからなぁ。

3Cだか5Cだか良くわからなかったので、コネクタを両方買ってきてもらったんですが、どうも、4Cっぽい。あらあら。結局、3Cのコネクタを無理やり差し込んで修理完了。

これ多分、昔、台風で飛んでったアンテナ側に付いていたコネクタなんだよな。ちゃんと溶着テープ使わないとぼろぼろに。外す時にナットの部分が欠けた。それを「別にいいや」で適当に使っていたらしい。まぁ、長持ちした方か。

なんかスカパーはもう一つ衛星上げようとしているらしいけど、次はネットなんじゃないかなあ。ただ、

　　　くそなコピー制御がどんどん酷くなってる

ので、もう見るのを止めてしまうかも。低画質にも慣れてきてるし。そもそも放送はフルHDでないわけだし。

録画BDメディアの現状はAACSをなんとかすれば良いだけなので、それほど酷くはないんですけどね。ちょっと面倒くさいけど。

そういえば、BD-R/REを入れるいつもの箱をGood Willで扱わなくなってしまったので、ちょっと困ってるのだった。

琉大 Open Campsu

まぁ、いつも通りなんですが、今年はプロ3の学生が二人という問題が... でも、その二人にプレゼンしてもらいました。ありがとうございました。まぁ、プロ3は「自分のやりたいプログラミングなどのプロジェクトを年間の単位をもらってやる」というものなので、そもそも沢山の学生が取るようなものではない気がする。一つは Game Jam 関連、一つは Erastic Search の紹介という感じでした。

「画像処理はどこですか」とか聞かれましたが、やっている先生はいるのですが、オープンキャンパスには出てなくて。オープンキャンパスに出し物を出すかどうかは、教官の根性と嗜好の問題だからなぁ。流行りの深層学習ぐらいは出して欲しかった気もしますが、まぁ、まったく業績ににはならないからね。代休取らされる割に大変なので、やったもの損と思っている人は多いかも。

でも、大学の質は結局は入ってくる学生によると思う。特にうちの大学は偏差値で選ぶような大学ではないし。学生に聞いてみると「オープンキャンパスでシス管の学生が楽しそうに発表していたから」とか「先生が楽しそうに説明していたから」とか「ファイヤー和田という先生がいたから」とか、まぁ、なんか、効果あるみたいです。

作成したビデオ見せるだけ見たいな展示もあったけど、在籍している学生が楽しそうなのは重要だと思う。いや、1年次の学生が「授業楽しいです」とかビデオでいっているのをみると「こいつ、'まだ、OSの楽しい授業受けてないしな」とは思いました。

なんか去年の学生がIGDAからのpingを無視していたという問題が発覚して。その応答もやってました。30分もかからずに終わるんだから、できないんだったら相談しろよ。単に英語のアンケートに答えるだけだろ?

Emacs-25 char width problem solved.

Emacs-25 を Terminal mode ( emacs -nw )で使うと、Agdaの→とかλのEmacsの認識位置がずれる問題ですが解決しました。

Emacs側で、

(char-width ?→)
2

となっているのがだめ。

Perl 側では、

Unicode::GCString->new("→")->columns
1

ふーん。Emacs の char-width は char-table に入っているので、それを書き換えればよいらしい。力武氏とか様々な人がいじっているわけですが...

Perl のchar widthの出力に合わせることにしたら治りました。EmacsのGUI modeへの影響はありません。修正した、eaw.el は以下に置きました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Applications/14x14ja/

Terminal.app でも xterm でも、違うフォントを使っても問題ないらしい。

14x14ja は、まだ足りない記号がかなりあるらしい...

xterm の font

xterm まだ使っているのは、k14 font が好きなのと速いのなんですが.... まぁ、k14 はいいんだけど、

もう少し大きくできないの?

ってのはあるよな。X.org は Xft が入っているので、TTFでもOTFでも使えて、標準でOS X付属のフォントが使えます。なのだが、

　　　xlsfonts は対応してない

は? その代わり、

fc-list :scalable=true family

ってのを使うらしいです。で、-fn の代わりに、

xterm -fa 'Menlo' -fs 36 -g 80x24

とかするらしい。なかなか調子良い。

なんだけど、unicodeなフォントを表示すると、

u n i c o d e な フ ォ ン ト

みたいになってしまう。どうもxtermは最大幅のグリフで位置を計算するらしく使い物にならないです。で、

-cjk_width
-mk_width
-xrm 'UXTerm*ForcePackedFont: true'

とかの brain damaged な option があるんですが、どれもだめ。どうも、 -fa を使うと、 -cjk_width は無視されるっぽい。

http://running-dog.net/2011/10/post_303.html

とか

http://vega.pgw.jp/~kabe/vsd/k14/

とか、割とだめな状況だな。まぁ、レガシーなので、誰もやらんだけだけど。Propotional font に対応した xterm ってのは現存しないみたい。

Terminal.app でも、状況は同じでただ、

文字のspacingを調整するオプションが付いてる

で、まぁ、適当にやるとちゃんと表示されるらしいです。

X11

もはや、知る人は珍しい、X Window System ですが、しつこく使ってます。なのだが、

Perl/Tk が動かない

Tcl/Tk は、tcl 言語を除けば使いやすいGUI libraryなんだけど、それを Perl から使えるようにしたものですね。Aquaでそのまま使えれば良いのだが、なぜか、X11。Tcl.Tk は Aqua で動くので、さぼっているだけでしょう。というか、GUIはAPIが多いので移植するのは大変なんだよな。

DB<2> $m = MainWindow->new
zsh: abort perl -de 0

かなり初期の部分で落ちるので、Tk.pm の実装の問題だなと思って、lldb でdebugしようとするんですが、つまらんセキュリティのせいでままならん。でも、root でやればなんとかなった。stack trace を見ると...

5 libsystem_c.dylib`__chk_fail_overflow
6 libsystem_c.dylib`__strcpy_chk
7 Tk.bundle`AllocStringEntry
8 Tk.bundle`Tcl_CreateHashEntry

strcpy_chk? あぁ、なんか、strcpy をそれに強制的にmapしたんだな。で、ソースから直そうかと思ったですが「元のソースは、どうせgithubだろ?」と探しに行ったら、

https://github.com/eserte/perl-tk
cpanm baseのソースと違う

なるほど。で、git diff してみると、

strcpy が軒並み memcpy に書き換えられてる

まぁ、そうだよな。で、git から取ってきたので、ちゃんと動きました。なのだが、

Xquartz のApplication menuからだと起動しない

くそ〜どういうこと? で、menu の所に、>& /tmp/ers と書けるということがわかったので、

Tk::Event object version 804.033 does not match bootstrap parameter 804.032 at /System/Library/Perl/5.18/XSLoader.pm line 95.

そうか、違うTkを見てるな。なんどか install したからな。

perlbrew ってのがあって、複数の版のperlを使い分けられるものなんですが、それが悪さをしているらしい。Perlは、Ruby とか Python と違って、minor version で雨後かなくなるってのは珍しい(最近は少しある)ので、不要なんだよ。なんだが、Tkが動かなかったので入れてしまったのですが、さっそくやられました。

X11の起動には zsh ではなく sh を使っていたんだけど、perlbrewは zsh の修正にいくらしい。そもそも、

system 関係のライブラリのperlを個人のコマンドでversion毎に切り替えるのか?

なので、環境変数を unset して/

/usr/bin/perl Makfile.PL
make -j 4
sudo make install

で、構築しなおし。まぁ、xinitrc をzshに直しても良かったんだが...

XQuartz のApplication menuは、

　　~/Library/Preferences/org.macosforge.xquartz.X11.plist

にあるので、これをコピーすれば、そのまま移行できるのですが、

　~/Library/Caches/org.macosforge.xquartz.X11

の削除が必要でした。Time Machine で full inherite するなら、それも自動的に行われるわけですが...

次は、xterm の font 設定の話なはずです。

MBPの付属品

なんか、いろいろと買わないと...

＊ USB-C な電源
＊ USB-C なHDケース
＊ USB-C なHDMIアダプタ

いや、USB-C/USB/HDMIアダプタは用意してあったんですが、HDMIの接触が悪いのが不評らしいです。

電源ケーブルを兼ねるイサーネットが通るようなのがあるとうれしいかも。

HDMIアダプタは泣いている人をけっこうみたので「USB-Cなプロジェクタが出たら解決じゃね?」とか思いましたが、自分では、

＊ 自作のTree VNCで、教室に設置されてる固定PCに接続して表示

で問題ないです。プロジェクタにはWifiでつなげるのが普通になるはずだったんじゃないのか? そういえば、Apple TVってどこにいったんだ?

Ingress event

Niantic の人が来るとかで、7/5 にIngressの集まりがあったので行ってきました。まぁ、苦手な方なんだけど。うだうだするのも良いよね。

カフェの営業が始まっていて、カレーがあったので、ちょっとひかれたんですが、なぜか食べず。 まぁ、そのうちに。

blog を毎日書くことにしていた時期があったんだが、最近はさぼってるな〜

フロイトの随伴関手定理

Agda で圏論を証明していくシリーズですが、ようやっとフロイトの随伴関手定理まで終わりました。Hihger order categorical logic だと2 page、しかも、課題になってる。

内容的には、圏Aがcomplete(Limitiが存在する)で、U:A→BがLimitを保存するなら、圏Bのすべての対象bに対して、コンマ圏 b↓U が preinitial small full subcategory を持てば、U には随伴関手があるってもの。長い。

証明は段階を追っていて、

1. Complete な圏が preinitial small full subcategory を持てば initial object (任意のaに対して i → a なユニークな射があるi) がある。

preinitial small full subcategory ってのが、良くわからなかったんだけど、Aの部分圏ってのは要するに関手 S : A → A で送った先のことだとわかったら、任意のAの対象 a に対して、F(pi) → a という(ユニークとは限らない)射があるってことだとわかりました。この部分は丁寧に説明されていたので、割とすぐにできました。

で、次は、

2. if A is complete and G preserve limit, Comma Category F↓G is complete i.e. it has limit for Γ : I → F↓G

で、コンマ圏を定義することに。FにLimitの保存が要求されてないところが肝らしいです。これは激ムズだったんですが、3月ぐらいに片付けたみたい。この次は、

3. U : A → Sets, K{*}↓U has preinitial full subcategory iif U is representable

なんですが、AとUの条件が書いてない。2を使うはずなので、ないのは変なんだが。prepresentableってのは、米田関手 A → Hom (a,-) つまり、AからAの射の集合への関手に U が同相だってことらしい。つまり、Uは米田関手だとして片方向は証明してよいわけね。

ここで、もしかして、Sets の Completenessを使うんじゃないかと思って、まぁ、使わないんだけど、証明はするべきだなと思った。思ったんですが、結構、時間食ったのだが、Product と Equalizer はできたんだけど、Limit が直接に作れない。Product と Equalizer があれば Limit はできるという証明があるんですが、それにも、うまくマッピングできず。で、Stack overflow に投げたんですが、まだ、解答はきてないです。Agda の推論能力がちょっと足りないんじゃないかと思ってます。

結局、Uが米田関手なら K{*}↓U にinitial objectがあって、initial objectがあれば U が representable だってのは、AとUの条件抜きに証明できた。でも、2を使うには、UがLimitを保存するってのと、AがCompleteだってのが必要なんだが... AがCompleteってのは、さすがにでるわけないんだけど、UがLimitiを保存するってのは、AがCompleteならできそうだったんですが...

黄色の本(Category theory for working mathematian)を読み直したら「UがLimitを保存するから明らか」と書いてあって、結局、仮定だったのか。証明できそうだったはなんだったんだ。(後から見たらUのLimitの保存は使ってませんでした。representableならばUはLimitを保存するから仮定は必要ない)

ここまで来ると、K{b}↓U の initial object が universal mapping の解だってのを示せば、それから随伴関手ができるというわけ。これは、ここまでくれば、まぁ、楽勝。

というわけで、寄り道を除けば、2が一番難しかったみたい。黄色の本では equalizer と product の保存から導出してるな。

あとやるとすれば、Beck theorem か Kan extension でしょうけど、まぁ、やらんかな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/9242298cffa8/freyd2.agda