動きました...

結構、いろいろバグってた... ちゃんとテスト書かないとバグが溜まるんだよな。引数の待ち合わせで送り忘れたり、子クラスのpublic method を親で上書きしてたり。

というわけで、今晩は安らかに眠れそうです。

よいお年を〜

再び、Java と格闘

行方不明になっていた学生に割り当てたプログラムを動かしていると、

　　なんか動かなくなってる

動いていたはずの version に戻しても動かないぞ... module の微妙な version の依存性とか外しつつ書いていったので戻れない...

動いていたと思ったのは幻覚だったのか?

良くある学生の...

先輩とか僕が書いたコードがわからないので、自分で独自なものを書くというやつですね。

独自に書くのはよいと思うのだが、もちろん動けば文句はないわけですが、動いてないのだと、

　　それって、僕の仕事を倍に増やしてないか?

「これ動いているんですか」みたいなことをいう学生もいるんだけど、まぁ、動かなくなる理由はたくさんあるんだけど、Mercurial をたどれば動いてた所にはたどり着くことが普通。

いろいろ気をつけてはいるんですが、やられてしまうことがあります。それもまた楽しいのが大学だな。

Java の Singleton

昔、学生に書いてもらった Alice っていう分散フレームワークなんですが、

　　Task scheduler とかが Singleton

ぐ。おかげで、

　　Java で複数 Thread でテストする

ってのが不可能。手元で InteliJ でデバッグできないです。Nat だとつなぎ先を複数用意しないといけないのだが、それもできない... さらに、

　　Java は fork できない

おおい。逃げ道ないんですけど。複数プロセス上げても、そこに何かを渡すには引数とか共有メモリとかめんどくさい... Thread local は遅いし、さらに混乱するだけ。

そして、残念ながら、

　　Singleton の除去は自明でも簡単でもない

DIコンテナみたいに必要なものをそろえて渡してやれば良いだけなんですが、Singleton で書いたが最後、

　　便利なので、どっからでも自由にアクセス

ということになってるので、まず、使用しているところを洗い出して、そこに渡す手段を作成時に用意するという作業が...

というわけなので、

　　どうせなら書き直した方がまし

ってな状況です。

DBコネクションとか Logger とかは Singleton にしろとか言っている人もいるようですが、

　　マルチCPU以前の古い常識

でしかないですね。単純に static を使った Singleton は禁止だと思う。

インスタンスが一つという状況はもちろんあるわけですが、それを大域変数で自由にアクセスってのは、Logger でももうないです。Haskell みたいに原理的に書けない言語とかもあるし。

年末年始は沖縄

プチエトワールのクリスマスディナーはおいしかったです。

最近は東京にいるパターンだったのですが、「少し短く頻繁に帰ろう」キャンペーンで。プロシンの日程もあれなので。でも、12/28に授業を入れられてしまったこともあったりしましたが。今年は避けられました。

昨日は夏並に暑くて、久しぶりに普天間廻ったんだけど、少し汗ばむ感じ。喜友名でどしゃぶりくらいましたが。今日は少し寒いな。

ラフォンテは年内で閉店

首里桃原にあるピザ釜持ってる広いレストラン。儀保駅から歩いて3分という立地(に後からなった)で便利だったんですけどね。

お昼は1620円のバフェなのか。もっと行けば良かったな。

結構、急に決まったみたいです。

今年は、浦添のそら豆も閉まってしまったし。普天間のラーメンまるよしの北谷への移転もちょっと痛かった。

研究室忘年会

直前まで論文書いてたりしましたが...

温野菜で鍋という安直な感じが学生っぽくて良いかな。

例年だと東京で大晦日にどんなコード書こうかと考えている頃ですが、今年はずーっと沖縄にいる予定です。なんのコード書こうかな。

そういえば今日は Papers3 から論文PDFのリンクhtmlを出力するPerl script を書きました。Papers2 とは微妙に違う。DBのtableの属性名が。でも、時間がかかったのは、rsync で空白を含むファイル名をどうやってコマンドラインで渡すかだったり。--protect-args !? いつできたの?

OS X で、なんかWindowがドックに格納されてしまう

って症状に長年困ってて、xterm 使ってる時が多いんだけど。でも、今日、

　　どうも、Command M 打ってるらしい

というのに気がつきました。Command Space で日本語にした後、「み」とか打つ時に、Command M と打ってるらしい。で、これに気がつけばググれる!

このダメなキーバインドを殺すにはシステム環境設定の

　　keyboard -> shortcuts -> app shortcuts

に、

　　Minimize
　　Minimize All

を何か「打ちそうもない」キーに割り当ててやればよいらしい。たとえば Command Control M とか。でも、少し落とし穴があって、

　　Minimise
　　Minimise All

という綴りを使っているアプリもあるらしい...

　　https://apple.stackexchange.com/questions/115562/how-do-i-disable-the-minimize-command-m-shortcut-in-mavericks

17年ぐらい気がつかなかったらしいです。

PathFinder の続き

なんか順調に直していたんですが...

　jdk にパッチを当ててる部分がある

それ自体はなんとかなったんですが、

　パッチを当てたmoudle と、そこから呼び出している自分のmoduleが cyclic

だと文句言われました。もちろん、cyclic なんだけど。それが何か? と思ってググってみると、

　https://developer.jboss.org/blogs/scott.stark/2017/04/14/critical-deficiencies-in-jigsawjsr-376-java-platform-module-system-ec-member-concerns

で、cycles between packages in different modules ができないのはまずいだろと文句を言っている人たちが...

というわけなので、jigsaw 側の問題らしく、回避できないっぽいです。少なくとも簡単な方法は思いつかない。逆に言えば、そこがなんとかなれば動きそうです。

たぶん、cyclic を許すとか lazy loading を許すとか、そんなswitchが入るんじゃなかろうか。というわけなので諦め。java 1.8 やればいいさ。

でも、コンパイラの授業でやろうと言っていた、CbC compiler の最新llvm/gcc 対応は、なんか学生が残りをやってくれたようです。少し問題はあるっぽいがだいたいできてる。すごい! えらい!

Java9 and Java Pathfinder

Starwars は見たのでネタバレだいじょうぶ〜　で、Fedora Linux Kernel の debug の方は片付いたので、

　　次は、Java Pathfinder on Java9

いや、Java8 では動いているので、別に無理して Java9 で動かす必要はないんですけどね。

で、Mercurital repository

　　http://babelfish.arc.nasa.gov/hg/jpf/jpf-core

から取ってくるわけですが、VM API使って Java で Model検査しようってものだからなぁ... last update 2/6 のjdk8u121用ですか。

というわけで、ばっちり ant build できない。

new Integer とかは無視して良いらしいけど、いろいろないと言っている。

Java9 で module system が導入されて、ついでに VM 系がどっかに追いやられたらしい。もう一つは、

　　Pathfinder は annotationsg classes　　 examples　　main　　　　peers　　　 tests

と module 分けされているのだが、Java9 では、module-info.java で

　　main/module-info.java
　　module gov.nasa.jpf {
　　　　requires jdk.unsupported;
　　　　requires java.logging;
　　　　requires java.management;
　　　　requires javafx.swing;
　　　　requires gov.nasa.jpf.annotation;
　　}

と明示的に記述してやらないといけないらしい。とググると出てくるわけですが、module-info.java は gov.nasa とかが置かれている top に置かないとだめらしい。

jpf は and なので、build.xml をいじるわけですが、

　　 <javac srcdir="src/main" destdir="build/main" includeantruntime="false"
　　　　　　debug="${debug}" deprecation="${deprecation}" classpathref="lib.path">
　　　　<compilerarg value="--module-path"/>
　　　　<compilerarg value="build/annotations"/>
　　　　<compilerarg value="--add-exports" />
　　　　<compilerarg value="java.xml/com.sun.org.apache.bcel.internal.generic=gov.nasa.jpf"/>
　　　　<compilerarg value="--add-exports" />
　　　　<compilerarg value="java.base/jdk.internal.misc=gov.nasa.jpf"/>

と、こんな感じで module path を指定してやると良いようです。

　　 ant |& grep　error
　　　 [javac] jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:111: error: cannot find symbol
　　　 [javac] jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:115: error: cannot find symbol
　　　 [javac] 2 errors
　　　 jpf-core/build.xml:103: Compile failed; see the compiler error output for details.

まで来たが...

が、まだ、動いてない... classes に Java5 互換用の java/lang とかある。java のpackage を上書きしているこいつ、なんとかなるのか?!

なんとかなるなら、御本家の方がなんとかしているんじゃないか説。動かないかもな〜

さらに ansible kernel build の続き

いろいろトラブったのですが、

　　make menuconfig

を ansible script から通す方法がない。結局、いろいろググりまくった挙句、

　　config file を取っておいて、それを送り込み
　　make olddefconfig

してやるのが良いみたい。これで、kernel build まで ansible で通りました。

で、build したソースを VM host にコピーして、build したVMを qemu の debug mode で立ち上げて出来上がり。

な、はずだったんですが、back trace が死んでる。

どうも、linux kernel は address randomize をするらしく、それを config の時に切ってやらないといけないらしいです。

　　http://tinyurl.com/y8oxjfw5

で、ansible から再 build 中。これで kernel debug できるかな?

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Ansible/fedora_kernel_build/

この ansible script 、来年は絶対に動かない予感。

Fedora build の続き

順調にいくかに見えたんですが...

　　ramfs がどうこう

とかいって動かない... でも、これを作ろうとすると、かなり面倒くさいらしい... くそ〜

やっぱり、fedora の中で kernel build した方が良いらしいです。で、自分で作り始めたんですが、去年10GBで失敗したので、

　　20GBにしたらやっぱり失敗

くそ〜　去年は30GB足したのだが、それでは多いかと思ったんだけどな。

で、

　　ansible 書くんじゃないか?

ですよね〜　で、ググってみたんですが、なんか適切なのがない。まぁ、そうだよな。毎年、Fedora の kernel build とかし3てる奴いるわけないし。

諦めて書き始めたんですが、git で取ってくると頃までは来たみたい。動くかな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Ansible/fedora_kernel_build/

Kernel debug

毎年のあれですが、今年は、学科のServer上で kernel build して、それを VM に copy するのが良いんじゃないかと。去年は VM の中で comiple しようとして disk image の拡張とかで死んだらしいので。

export INSTALL_PATH=/hoge/tmp
$ make -j 8 install

とすると、/hoge/tmp に Map と vmliniuz ができます。素晴らしい。

が、それを VM の中にどうやって持ってくの? 結局、IP address 申請して dhcp 取ってしまうのが簡単らしい。そうすれば rsync できる。

あとは、grub2/grub.cfg を書き換えて... というところで力尽きました。できるのか〜

そういえば、CbC の最新 gcc/llvm への対応は、llvm は学生が自力でやってくれたらしい。素晴らしい。指導の甲斐があった。gcc は、まだ、謎です。

カレーパーティは1/7にしようかと思ってます。

東京と沖縄のIngress

まぁ、なんとなく下火になってきたゲームも悪くはないというか... AXS と東京三菱がスポンサーを降りるらしい。

東京ではミッションやろうと思っていたのですが、一つしかやらなかったかも。キーばかり200個カプセルに入れて捨ててきました。Ingress って二周はしないとCF作れないんですが、いろんなところを一周しかしなかった。

Engineer 黒が近かったので帰り際に、持ってるVR/AXSを適当に刺してきたんですが、ちょっとダメだったかも。

なぜかと言うと、戻ってきたら、自分の縄張りがかなり緑だったので。しかも、適当に修復したら多重作られた... まぁ、落とされるゲームなので、あまり強いシールドは入れないようにしてるんですけどね。

で、まぁ、学校の行き帰りに落とすわけなんですが、バースターもレゾもシールドもまったく足りない。それでも、うちの奥様がご近所は守ってくれたみたいです。ありがとうございます。

ここしばらくは緑おとなしかったので油断してたかな。年末なので、みんなストレス溜まってるのかも。おかげで楽しいともいうか。

Felica の続き

B3の学生もだいたい決まったので、この前のFelicaの鍵をやってもらおうかなと。と思ったら、

　　それはもうできてます

的なコメントが学生から。え〜、なんだって。でも、だいぶ前の話だよな。じゃぁ、ソース見せてみろってことで、夕方から...

この前の nfcpy をやっぱり使っていて、だいたい動きそうなソースだ。ラズパイ用のリレーボード Piface を使っていたので、それを Pythong の dummy class に置き換える。

で、なんか socket 呼んでるので、その部分は comment out 。nfcpy の設定とかにいつも通りはまりましたが、

　　edy id は読めた!

その部分はちゃんと動いていたらしい。あとは、ldap と接続すればよいんですが、書いてあるコードは怪しいソケットルーチン。どうも学科のノートPC/VM管理ソフトである Akatsuki に接続しようとしていたらしいんですが... この部分は動いてないっぽい。そもそも、鍵開けてから閉める部分書いてないし。

うちは、edy id は ldap に入れてるので、ldapsearch でいいかな。で、Timer 使って on/off するように直してできあがり。簡単じゃん。

なんだけど、ldapsearch が遅い。edy id 部分に index 貼ってないからだな。できるはずだけど...

ミニコンポ

実家にあるソニーのミニコンポ(死語)ですが、なんか、CDトレイがだしっぱなしに... まぁ、主に J-Wave 聴くのにしか使ってないんですけどね。自室のOnkyoのレシーバーもだいぶ前に壊れちゃったんだよな〜

一階と二階に一つずつ置きたい所だが... そういえば、HAP-S1 ちょっと面白そう。

　　 http://www.sony.jp/system-stereo/products/HAP-S1/

スピーカーも怪しいが、まぁ、生きてるみたいだから。ところが、HAP-S1 は、

　　タイマーがない

え、この手のものって目覚ましに使うのが主流じゃないの? まぁ、このまま買わないかも...

安物の音で目覚ましってのもなあ。もっとも、沖縄では目覚ましなんて使ったことないんだけどさ。

しのはらとけむり

西池袋のラーメン屋さんですね。しのはらは、最近、結構行列してる。僕はけむりの方が好きなんだけど。

けむりで、うっかり「200円の特製トッピング」頼んだら、結構な量で食べるのに少し苦労しました。

しのはらは、今回は土曜日にたまたま空いたので入れました。行列している時に並ぶほどではないと思うんだが... でも、麺がしっかしていて、スープも良くできていて、流行るのも当然かな。

いつもの訪問

母方の四人姉妹もだいぶお歳で。母の妹が特養に入ったのですが、施設は変わらず。でも、前回来た時よりは調子が良さそうでした。もう、あんまり話も通じない感じではあるんですが、母を連れて会いにいくのが大切だと思ってます。

いかないと忘れられちゃうからな。

自分の未来でもあるんだけど、歳取ること自体は悪くないと思う。あの世代はネット使わないわけだけど、僕達が歳取る頃にはネット老人うるさいって感じになるんじゃんないかな。

独り言うるさい人とか、ひたすら布をたたんでいる人とか、ベッドで寝た切りとか。ひとそれぞれだな。

edy card

そういえば、なんか edy id が読めないなんて話があったなと思って、秋葉原で Felica reader を買ってきました。いや、大学のどっかにはあるはずなんだけど。千石にあったんですが、二つあった。どれだろう? で買ってきたのは、

　RC S380

Sony のUSBで繋げる奴ですね。

ソフトはいろいろあるが、python の nfc が S380をサポートしているらしい。他にもいろいろあるけど、S380 は動かない感じ。

で、
python examples/tagtool.py -v

で動くらしいんですが、だめっぽい。timeout とか言ってる。 nfc/tag/tt3_sony.py　の request_service の timeout を10倍にしたら動きました。なんだよ。

なんか、妙に大きな数値のfor文でスキャンするみたいなプログラムになっていて、くそなんですが... それに、どうも、

　polling base

らしい。うーん。まあ、でも edy id は読めたので良いか。

ハリーズ

前田のカレーのお店なんですが、おばちゃんが病気で、休みがち。年内は、

　　かわいいお姉さんがたが引き継いでくれるらしい!

火曜日頼んだ分だと、おばちゃんが作った分と遜色ないです。すばらしいです。

学生が卒業カレーみたいなのにも使っているらしく、がんばってくれると良いんですけどね。

ちょっと早めに出て Ingress

沖国大辺りを荒らしてから、お昼食べて大学へ。のんびりしたもんです。

Ingress だと運動として強度が低いってな話もあるけど、

　高血圧なんだから、そんなにがんばってもね

MoarVM 読み会最終日

最初は Rakudo 読み会だったんだけどな〜

午前中は、nqp と rakudo の文法規則を読んでました。だいたい Perl6 は nqp の5.5倍の大きさ。実際にトレースすることはできなかったんですけどね。

午後は、VM読もうということで、moar command を lldb で trace 。nqp のcommand line が出た所で、control-C 打って、lldb に。楽ちん。

でも、もはや、lldb は -O0 -g3 でも、引数がないとか変数が見えないとか。disass でレジスタから直接値を見るんですが、まぁ、疲れますね。

VMのregister は大域変数に取ってあって、オペランドからレジスタ名(数字)をとってきてアクセス。わかりやすい。レジスタには型はないので union 。それでいいのか?

で、jit のentry point を探すんですが、適当に「ここかな」というところに break point 。で、MoarVM のbyte code を graph ってのに変換する所は見つけて、それを emit ( native code を出力する) ところまではわかりました。

　nqp --target=mbc --output=fib.moarvm examples/fib.nqp
　moar --dump fib.moarvm

で、MoarVMのbyte code のdumpが見れます。

でも、

　　最適化しているところはどこだ?

どうも、inline 展開と、定数式展開ぐらいしかしてないみたい。いや、見つけられなかったので想像なんですが。

まぁ、そこで時間切れかな。

10時から18時までですが、遅れ気味に始めて、12時にはお昼休み。14時まで休んで、16時に休憩はさんで18時までなので、まぁ、そんなに大変と文句をいうほどのものではありません。

感想に「普段見れない河野先生が見れた」みたいなことを言った学生がいますが、あんまり変わらない奴なので、観測力がないだと思います。

でも、今回は割とスムーズだったかな。スライドもわかりやすかったし。

nqp

というわけで、朝から Rakudo 読み会なわけですが、

　まぁ、Perl6 が何ってところから

という感じで。下位言語の nqp から動かしてみるわけですが、

　say(1) を say (1) とすると動かない

なるほど〜　いろいろググって、

　http://edumentab.github.io/rakudo-and-nqp-internals-course/

これが割と良いので、今日は、だいたいこれを読んでました。最初は、

　nqp (Not quite Perl) の説明

で、それから、

　QAST ( nqp の抽象構文木)

そして、Grammer 、Action、byte code、VM と一通り。VMの実装はあんまり書いてなかったな。

pypy の時は結構苦労したんですが、Rakudo は、このslide のおかげでだいぶわかりやすい。もっとも、まだ、Rakudo を debugger から動かすのには成功してないのですが。

Grammer が class と同じレベルで built in なので、これまで見たコンパイラの中では一番奇麗かも。

コンパイラ自体は速いんですが、JVM/MoarVM 経由なのが起動が遅い原因かな。それで、JavaScript Engine に乗り換えようとしているのかも知れないな。

明日は、実際のコードと、VMの中身に突入してみる予定です。

Perl6 Rakudo

コンパイラの授業の〆は、Perl6 を読もうということで。12/2,3 10時から18時の予定です。工学部1号館321。最近は、ネット中継とかやってないんだよな。気が向けば設定するかもしれません。

今日は、LLVMをちょっとだけ読んだ後、Rakudoの準備。えーと?

　Perl6は、JVMまたはMoarVMの上で動く、
nqp で実装されている

　nqp は、JVMまたはMoarVMの上で動く
nqp で実装されている

　nqp compiler は、MoarVM/JVMのバイナリで提供されている

C compiler も Haskell compiler も、既存のC/Haskell compilerを前提としていて、

　真の意味での boot strap を失ってしまっている感じ

このあたりって、

　個体発生は系統発生を繰り返す

みたいにできないのかな。なんていうのかな、

　簡単なインタプリタ/コンパイラから細かい boot strap を繰り返して複雑なシステムが出来上がる

みたいにならないのかと。単純なシステムに fall back できないのは残念な感じ。

Perl6 を Perl6 (あるいは、その制限版である nqp )で記述すると言うのは、言語屋さんの自己満足に過ぎなくて、それが役に立つという状況になってない感じ。

で、わからないのが、

　nqp level で trace ってどうやるの?

ってことですね。nqp に debugger があれば、それで。あるいは、rakudo を Perl6 で動かせるなら、Perl6 debugger で。

でも、lldb/gdb level は用意されているようなんだが...

pypy でも、動かしてデバッグするまでにいろいろあったような。

nqp script 自体は、perl6 -mnqp hoge.nqp で動くようなんですが...

プロ4

好きかってなプログラミングをする授業プログラミング4ですが、今年は「勝手にどんどんやります」的な学生が4人ぐらい。なので、とっても楽です。

こじんまりとしてるのはそうだけど、あんまり高望みしてもね。このこじんまり感は今時の学生っぽい。

ちょっと前の学生は「ぶち上げて自爆」パターンが多かった気がする。

その前は自分で「ここまで、できるだろやれ」的な感じでやってた気がするな。着いてこれるなら、まぁ、良いんですけど。なかなか、そうもいかず。

サーバダウン

OSの授業でにこやかに、VMの課題をやろうと思ったら、

　　ssh できません

ぐ。先週も ssh できませんだったのに。先週は、NAT内のDNS serverと外向けのDNS server のどっちかを選ばないといけなくて、外向けを選ぶとNATの逆引きが中からできず ssh できない。内向けを選ぶと内部の外向けのサーバからは接続できなくなるという2択だったらしく。まぁ、どうせ外からは直接は接続できないので、適当な踏み台を選ぶだけの問題なんですけどね。

でも、いろいろ試してたら、

　　シス管のSlackになんか書いてあります

ってことで見てみると、

　　 今サーバー室に来てみてるけど, kernel 壊れたっぽい
　　 ```dracut-initqueue[259]: Warning: dracut-initqueue timeout
　　 Warning: /dev/centos/root does not exist
　　 Warning: /dev/centos/swap does not exist
　　 Warning: /dev/mapper/centos-root does not exist
　　 がでてboot 失敗してる

ってことで授業が終わってからの「シス管ミーティング」で、IPMI ( Dell の iDRAC っていう管理ソフト)経由で console にアクセスするんですが...

　　字が小さすぎて見えないよ

Javaのアプリでなんとかできるらしいんですが、さっぱり動かず。仕方ないので、サーバ室へ。要らないといったディスプレイスイッチで。

　　なんか緊急 shell かなんかに落ちてる。

「df コマンドないんです」え〜 でも、ls あるし、mount はあるし、fsck もあるぞ。log 見ると time out の連続かぁ。でも、sici RAID Controller の認識から sda1 sda2 までは正常なみたいだな。lvm command はあるんだが、

　　lvm pvscan

では何もでず。fsck もない。Boot しなおしてみると「ほら、Rescue boot あるじゃん」で立ち上げ見ると、さっきのと同じ。df ないし。しばらくいじっていたんですが、「CD付いてるし、CDからRescue しましょう」うんうん。

　　ちゃんと df, fdisk ある!
　　お、lvm pvscan でなんかでる。sr0? あ、そうか、CD差したからな

でも、もちろん、ぜんぜん、sda は表示されず。sda1 は boot partition で Linux 。なので、LVMからは認識しない。

で、いろいろググったんですが、lvm vgchange -a y しろとしか出てこず。lvm pvs で何も出ないのにそれは無意味だ。なんだが、

　　https://www.redhat.com/archives/linux-lvm/2006-November/msg00063.html
　　delete the partition within...

え、partition 削除するの? 結構、行き詰まっていたので、やってみるかと。partition はすぐに元に戻せるし。

　　delete してもなんにも起きず

ぐ。まぁ、なぁ。じゃあ、元に戻すか...

　　あれ? なんか、設定する値と、fdisk の示してる default value が違うんですが

じっと見てみると「0が一つ多い」ってことは、

　　一つ、partition が抜けてる?

そういえば、このシステムの設計実装した卒業生の城戸が slack に fdisk の出力載せてたっけ。良くわかるな。

　　結果的には、最初の一つのboot を除いて、全部、LVM volume

にしたら、それで lvm pvcan で認識しました。Rescue からはうまく認識しなかったんですが、

　　そのまま元ので立ち上げたら、上がりました。/etc/lvm の下がないと認識しないよな。

ここまで3時間。お疲れ様でした。でも、これくらいなら、今のシス管でも復帰できたんじゃないかな。

　　partition が壊れたのは、誰かがいじったせい

らしいので。command history に残っていたみたい。いろいろやって学ぶものだから、問題ありません。

研究室配属の季節

まぁ、それなりに人生を左右するイベントなんですが、どこに行ってもなんとかなるものなので。まぁ、相性もあるけど、それも、融通効かないわけでもないです。たかが2,3年だし。博士まで行くと結構長いが。

配属が決まると、カレーパーティだな。

その前に、コンパイラの授業の読み会があるはずです。

12/6-11 は東京にいますので、適当に呼び出してください。

というわけで、年末進行だな〜

Applicative Functor の続き

Applivative → Monoidal もできたので一通り終わりました。Applicative Law の使い方がさっぱりわからなかったんですが、

　　pure f <*> x = fmap f x

と、Haskelll の Applicative に書いてあって。これは、さらに関手の uniqueness から出ると。でも、Agda で書いた奴だと、そんな uniqueness なんか証明できそうにないんですが... でも、数字のリストとか、文字のリストとか確かに一意に決まる。

さらにググると、Free Theorem からでるとか書いてある。関手 fmap, fmap' に対して、

g o h ≈ k o f → fmap g o fmap' h ≈ fmap' k o fmap f

で、まさに関手の一意性なんんですが、そんな便利なものがあるのか? と思ったら、

　Agda では証明できないらしい
https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities

個々の具体的な関手では証明できるけど、可能な関手全部とかを取り扱うことはできないとかそんな理由らしいです。

でも、それがわかれば、あとは展開してまとめると同じ形になるって感じでした。

Ingress キリ番

100,000,000 は、あっというまに過ぎて諦めたんですが、今回は早めに。なんですが、5周年かなんかで、

　　AP倍

え、それって、偶数APしかもらえないってこと? 末尾は偶数。まぁ、諦めるかと思ったんですが、

　　なんか、末尾が奇数になる

履歴見ると、敵ポータルをグリフハックすると奇数になるらしい。あとは、

　　リンクで末尾6
　　リチャージで20
　　レゾアップグレードで130

あ、なんとかなるかな。で、琉大で調整したんです、

　　まだ10万AP足りず早過ぎた

なんですが、夜に屋富祖で少し壊したらあっという間にあと2万。

リンクはったり壊したりすると末尾が狂うし、グリフハックは禁止だしで、少しいらいらしましたが、最終的には寝床でリチャージで合わせました。

Applicative Functor and Monoidal Functor

なんか、Haskell のMonadがApplicative を要求するようになっていて、Monad を作るのが面倒になって困っていたんですが、そもそも、

　　なんで Applicative が必要なのか良くわからない

て問題が。

　　http://learnyouahaskell.com/functors-applicative-functors-and-monoids

とか、まぁ、面白いんだけど、

　　で、それって圏論的にはどうなの?

という疑問が。Functor は、

fmap :: ( a → b ) → f a → f b

で、これが関手の射の写像に対応するってのは、まぁ、わかる。だからなんなのってのは置いといて。

　　pure :: a -> f a
　　<*> :: f (a -> b) -> f a -> f b

こっちはなぁ。fmap の写像が関手、つまりHaskellのデータ構造に包まれてるみたいな感じ。

なのですが、MacLean には Applicative Functor とかなくて。で、

　　https://stackoverflow.com/questions/35013293/what-is-applicative-functor-definition-from-the-category-theory-pov

これによると、圏の積の構造を保存するFunctorである、Monoidal Functor と同じなんだとか書いてある。MacLean だと Monoidal Functor は一章使ってある。それかぁ。面倒くさそうなの避けていたんだけど。

で、Monoidal Functor ってのは、

unit :: f ()
φ :: (f a , f b ) → f ( a , b)

のことだそうです。あぁ、まぁ、積を写像しているような感じ。

** :: f a → f b → f ( a , b )
** x y = φ ( x , y )

としても良いらしい。逆に、

　　　φ ( x , y ) = ** x y

ですね。要するに引数に出てくる積は Curry 化でなくせるというわけ。そういう風に、Monoidal Functor から直積をなくしたのが Applicative Functor ってことね。

実際に、Monoidal functor と Applicative functor の相互変換もできるんですが、ちょっとしたパズルみたいな感じ。Sets だから射とかも集合の要素としてとってこれるので、変換できるらしい。つまり、

　　Sets 以外には Applicative Functor は無意味

な感じらしい。

ついでに Monoidal 圏と Monoidal Functor も Agda で1日で書けたんですが、忙しい時期にそんなことやってていいのか?

この後、Applivative law から Monodail law だすとか、その反対とか、Sets が Monodail 圏なこととか、いろいろやらないといけないようですが、ちょっと量が多い感じだな。


で、結局、Applicative Functor なんの役に立つの? ってことですが、まぁ、あんまり良くはわからないです。データ構造に写像も格納できて便利ってことかな。なんか最初の理解から進んでないぞ。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/808b03184fd3/monoidal.agda

沖縄寒い

今頃で20度切るのは珍しいんですけどね。南国行きたいとか言っているバカものも見かけました。

まぁ、Ingress にはちょうど良いです。うちのtop agentの cena 女史が faction change というのが最近の話題かな。Double Top とはやるな。

少しこまめに実家に行こうキャンペーンで12月上旬に、また東京にいこうと考えてます。その代わり、年末年始はパスかな。プロシンが後ろにずれたので、そんな感じにしようかと。

コンパイラの授業

いつもの授業ですけどね。途中から GCC とか LLVM とか読むわけですが、

　　放置していたGCC版のCbCを最新に対応させるか?

というわけで、GCCとLLVMの最新のを、うちのrepositoryに merge! いや、これ自体は授業とは関係ないんですが...

GCCは4.6から7なので、いろいろ変わっているわけですが...

　　ファイルの位置が変わっている

くらいかも。まぁ、そんなに簡単には移行できないだろうけどね。

GCCちょっと読んだので、来週はLLVMを読んで、その後は、12/1,2,3 で

　　Rakudo ( Perl6 実装)

を読もうかと思っています。YAPC もあるしな。

Windows 7 から Windows 10

まぁ、Windows とかロクなことには使ってないんですが...

　　OS X Marverkics 上のVMware Fusion 8.5 上の Windows 7

だったんですけどね。Windows 7 な Disk full とおっしゃる。VMだが60GBもあればいいでしょ? 100GBまで拡張するか。と、思ったら、

　　Snapshotを削除しないと拡張できない

え、てめーなにふざけたことをいってる。Snapshot こまめにとってるわけでないのですが、

　　VMWF は Snapshot の削除にとっても時間がかかる

まぁ、取りあえず削除は放り込んで... でも Diskfull って変だよな。っで、なんとかなったんですが、今度は、

　　共有フォルダに赤バツが付いてる

ぐ、なおらない。Windows って長く使ってると腐るんだよな。

そういえば、そろそろ Windows 10 にしても良いかな。それが罠だったわけですが...

Windows 10 は学科がライセンス保っているので、それをもらえば良いだけらしい。岡崎さんにDVDもあるとか言われたんですが「ないので、imageで」まぁ、それでも問題ないです。

で、image 落として、VMWare から入れるわけですが、

　　立ち上がって「インストールするイメージがない」で止まる

あれ? どういうこと? 8.5 で Windows 10 問題ないはずなんだけど。でも、新しいVMWare Fusion 入れてもいいか! と思ったら、

　　VMWare Fusion 10 は High Sierra でしか動かない

そこで諦めるべきだったんですが... いいや、ついでに High Sierra に上げるか。ところが、

　　App store が開かない

ぐ。なにそれ。そこでいつもの、

　　Shift 押しながら Safe boot

で、App store は治りました。そこから、High Sierra の install に。ちょっと待て。

　　Time Machine を止めて、別なHDDをつなげておく

そろそろ切り替えるべきだからな。よしよし。で、

　　問題なく High Sierra に

素晴らしい。そこで、VMware Fusion 10 を入れて。Windows 10が...

　　このハードはリアルモードをサポートしてません CPUID Early

は? 何言ってんので、しばらくぐぐったところ...

　　VMFware Fusion 10 は、2010 iMac では動かない

くそ〜 無駄足だったか。まぁ、それはMBPで使えば良いが... で、8.5 で Windows 10 が上がらないのはなんで?

　　簡易インストールを諦めてみると…

Windows のライセンスを入れるところで

　　ライセンスに対応するイメージがない

最初から言ってよ。なので、ライセンス無ならインストールできました。VMにinstallだとタイミングによって無効になったりするらしいが... こんなこともあろうかと、

　　ライセンスは二つもらっていた

ので、二つ目のラインセスを入れて解決。長い道のりだった...

Windows 10 ですか? キーボードの配置がJISでUSにならないのを除けば快適です。Windows 7 より遅いだけ。右クリックが多用されるので、Mac のマウスだと使い辛いかな。

コインランドリー

なんか、最近、派手で綺麗なコインランドリーが流行りらしく。うちの近所にもできてました。

で、少し冷かしに行ってみたところ、

　　河野先生ですよね

え? なんと、うちの卒業生が経営者らしく...

大学の勉強役に立った? と聞きましたが、普通にWebとかを使えただけで、直接には役に立ってないみたいです。

研究室にも、初期の頃のOBとか来てたな。ちょっと沖縄に戻ってくるのは早いんじゃない? とか思うけど、まぁ、それも良いか。

かばん壊れた

Twitter と同じこと書いてると言われるでしょうが、こっちにも書きます。年一回は壊れてる気がするよ。

バスから降りたら「バスっ」とかいう音とともにかばんが落下。もはや、いつものことなので驚きはしないんですが。

既に、付属の肩紐は使い物にならず実家の別なかばんの肩紐に交換済。なので、少し金具が元の違う。で、壊れたのは、肩紐側の金具かぁ。油さしておくべきだったかも。削れちゃうんだよね。

だいたい、革の方もリングになっているので、そこにOリングを通すのが良い。それが一番もつ。

　　最初から、Oリングにしておけよ!

と思います。デザイン的にもそっちの方が良いと思うし。

なんだけど、Oリングあったかな。4Fの実験室にいけばあるんじゃないか? メイクマンいけばあるのは知ってるのだが... なのだが、山田さんが「ここになはない。前も買った」というつれない返事。予算で買う時には余計に買うんだよ。秋葉原で電子部品買う時には必ず余計に買っていた。すごすごと部屋に戻ったのですが、

　　もう一度探したら、ロッカー置いてあったポーチの中にあった

旅行用のポーチでカミソリとか綿棒とか入っている奴。旅行には、Oリング必須だったのか。そうだろうなぁ。イギリスに行った時に既に、3.4kgのダイナブックをかばんで持ち歩いていたからな。

だた、キーホルダー用みたいな小さいやつなので、あまり保ちそうにないな。メイクマンにいくしかないか。少し余計に買うことにしよう。いや、既に買ってある可能性も高いな。

論理式と方向

いつもの Agda の話題ですが、論理式には方向がない 例えば、

　a = b

と書いてあっても、a が出力とか b が入力とかない。一方で、関数(λ式)には方向がある

λ x → y

では x が入力で、y が出力になります。

Agda だと、数学的構造は record や data で書きます。record は積で and でつながったもの、data は排他的論理和で case 文の集合みたいな感じ。

で、Agda の library とかを見ると、record Hoge と record IsHoge とかが組で出てる。良くわからなかったんだけど、どうも、

record Hoge ( input : InputType ) where
field
output : OutputType
isHoge : IsHoge input output

record IsHoge ( input : InputType ) (output : OutpoutType ) where
field
property : ppro inupt output

みたいに使うらしい。filed は名前と型、つまり、名前の付いた変数とか論理式が来るわけですが、record の引数は入力、field には出力、つまり、その数学的構造で存在が主張されるものを列挙します。例えば、有界な実数の集合には最大値にになる極限が存在して上界というとか、そんなの。

その入力と出力は数学的構造の性質(公理)が要求されるわけですが、それらは論理式なので方向性はない。それを IsHoge にわけて書くという方式らしい。

こうすると、

lemma1 : (input : InputType) → Hoge input → ...
lemma1 input hoge = ...

とすると、Hoge i での IsHoge の性質が使えるようになる。つまり、

∀ input → ∃ output such that IsHoge input output

というわけ。Hoge の存在を示す時には、

lemma2 : (input : InputType ) → Hoge input
lemma2 input = record { output = ... ; isHoge = record { property = ... } }

という風にするらしい。なるほど。

で、今までにやった圏論(クライスリ圏とかLimitとか)を、これにそって書き直したんですが...

　　仮定が余計とか、仮定が足りないとか

が若干でて、少しはまりました。一通り書き直して、だいぶ、見通しが良くなったみたい。普遍問題では入力は圏A,Bと関手Uで、それがUに対するLimitの存在につながるとか、ちょっとあやふやだったところが理解できたみたい。形式大事だな。

IsHoge のみで書くことも可能で、初期の頃のはそういう風に書いていて、必要なものは module input に書くとかしてたみたい。楽なんだけど、

Hoge → Fuga

みたいにならないで、

(x y z : ...) IsHoge x y z ... → IsFuga x w q

とかで、 x y z とかの仮定にいろいろ余計なものが入ったり、うっかり書きそびれたりしていたようです。

Programming 的には Hoge が interface で、IsHoge が実装だと言えないこともないかな。

Twitter の文字数

日本語 vs English だと

　焼肉 vs steak

っていう例を良く出すんですが、倍くらい違うみたいです。

Agda とかソースコードとか数式とかも twitter に書くのだが、すぐ足りなくなる...

なので、言語ではなくて文字でカウントして欲しいんだが。どういうカウントなんだろう。


Tweets 106K Following 5,989 Followers 5,907 Likes 94.4K

ぐらいなみたいだな。この間、6000 まで増やしたのに、また減ってる。思ったより Like 多いな。

目医者さん

「良くなってますね」

ということなので、まだ、少し残ってるようですが、薬は飲まなくて良くなったみたいです。

Retina で少し眼に負担をかけすぎたってのもあるかな。

生活習慣変えなければ、どうせ再発だとも思うけど... 血圧は低めになってきますが。

　　薬のせいもあるが、怪しい血圧計を新調した

のが大きいかな。

東京 short visit

既に帰ってきました。 母も歳なので、たまに長くいるよりも短くして、頻繁に行った方が良いかと思って。

でも、週末だけってのは「酒飲んで終わってしまう」なぁ...

　- * - * - * -

ついでに Agda も少しいじってました。初期の頃にやった equalizer と product から limit を作るという課題。Sets の Limit をやって、やっぱり少しおかしいことに気が付きました。

少し自力でやってみたがうまくいかず、Categories for Working Mathematician を見直すわけですが、

　　お前、前に読んだ時に何を読んでいたんだ?!

ってくらいに違うことが書いてあって。まぁ、でも、大筋は合ってたんだけど。一部の等式を、仮定を強力にして安易な証明ですませたらしい。だめだな。いや、おかしいとは思ったんだけど。Sets Completeness の時に使えなくて気がついた。

元の証明に Product 二つ足して東京にいる間にできたみたいです。

あと何やるのかは、まぁ、やっても良いものはたくさんあるが、Kan Extension とか、Cartesian Closed Category の一連とか。ZFC やってみるのも良いかな。

　- * - * - * -

なんか、xterm が勝手に focus 外れるんだよな。もう使ってる人はほとんどいないと思われるので誰にも聞けないところがつらい。

Blade Runner 2049

見てきました。なのでネタバレだいじょうぶになりました。

なんか時間の関係で4DXになりましたが、あんまり意味ないかな。4DXではまれる映画ってどんなものなんだろう?

年末にはスターウォーズも控えているのか。

こういう拡大再生産は、歌舞伎とか紅白歌合戦っぽいかな。

Sets の Completeness できた

集合と射の圏 Sets が Limit を持つっていう奴なんですが、なかなかできなくて。Product と Equalizer は割とはやく片付いたんだが。

6月ぐらいに Stack overflow に投げて諦めてたんですが、

　　8月に解答が付いていた

のに10月になってから気がつきました。

やっぱり、Heterogenous Equality を使うんだが、λ式を避けるとできるらしい。

そこから、また少しすったもんだはしたんですが、結果的には Heterogenous Equality の Functional Extensionallity と Irrelevance を書いてやるとできました。

3月ぐらいから、はまっていたので、ちょっとうれしいです。

https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda

PS4

PS3 の一台が壊れてしまったので、ちょっと不便をしてて。で、PS4 を買ってみました。初代がかっこいいのだが、安い最近ので。Pro ではありません。 DLNAクライアントは結構快適。さくさくだ。

残りのPS3も時間の問題なので、少し、残ってるPS3のゲームもやらないと。FF13 三部作とか... なので良くわかりませんが、PS4買ったのでPS3のゲームやってたりします。

歯医者さん

なんか左上の奥歯の奥が不調で。といってもたまに痛むぐらいなんですが。繰り返しの治療が必要らしい。これくらいが歯医者さんのお得意様なんだろうな。いや、もっと金かける人たちか。

治療するたびに詰め物をはずすわけですが、で、「外れない時は外れないのですからね」というわけで、

　　詰め物にポッチがある'

これが結構気になる。ポッチといっても小さいんだけど、別にもっと小さくてもいいんじゃないの?

　　ポッチ

としている必要ないだろと思うわけですが。

まぁ、気になったら来てくださいとか言われたけど、そこまででもないかなぁ。

どうせ細菌が住んでいるだけだろうとは思うのですが、身体のあちこちにそんな細菌の巣があるような気がする。たまに痛みます。

学生のやりたいこと

プログラミング3/4 は、自分のやりたいプログラミングプロジェクトをやる授業なわけですが...

　　学生のやりたいことって、実は、はっきりとはない

まぁ、そうだよなぁ。

それでも、4,5年前は、いろいろ言ってきたものなんですけどね。今は、

　　先生の顔色を伺って、望む答を探す

なんだよそれ。聞いているのは「自分のやりたいこと」なんだけど。そういう意味では、

　　機械学習をやりとか、VRをやりたい

とかは、僕のご意向とは違うよな。必要なら使うけどさ。

普段の自分の生活で「これが良くない」とか「これが欲しい」とかを見つけて、それを改良したり実現したりするってのもよいと思うんですが、

　　ちょっと、こじんまりとしているかなぁ

別にそれが悪いと言うわけでもないですが。TreeVNC とかは、そういう風にできたものだし。

先輩達のやってきた、あるいは、やろうとしてきたことを聞かせると「おぉ〜」とは反応しますが、それも期待の反応をしただけか?

ちまたのほげほげコンテストとかほげほげハッカソンとかメーカーなんちゃらも、

　　そういうアイデアの行き詰まり

の結果なのかも。何をすれば良いかわかってないのは、こちらの方かもな〜

クラウドの課題

OSの課題にさくらクラウド上にVMを作るってのを出しているんですが、

　　ssh でloginするぐらいしかしてないから、要らないんじゃないか

ってな話が。まぁ、学科のサーバ上にVM作るのと差はないからな。

でも、まぁ、その差がないってのを学ぶ課題ではあるんだけど。そもそもAPIが、さくらクラウドのとは違うので「ぼたんぽちぽち」感がない。

じゃぁ、どんな課題が良いのと聞いてみると、

　　Web service の tuning contest

って、この間やってたあれ? まぁ、出してもいいけど。

徐々にクラウドの比率が上がるんだろうとは思うんですけどね。センタ側ではAWS結構使われている説もあるらしく。

円の描画

ちまたで、Illustrator の円はベジェ曲線による近似で誤差があるみたいな話が。

昔、マイコンの自作をやってた時にはグラフィックスは自分で書くわけ。誰も書いてくれないので。それで、マイコン雑誌に載っていたのが、

　　DDA Algorithm http://tinyurl.com/qa48sjv

ですね。その当時、東工大では Fortran の演習があって。ちなみにカードだったんですが。それで DDA で円を書くのを提出したことが。「なんで、そんなのやってるの? 他にもアルゴリズムあるけど」みたいなコメントが付いてましたが、だったら、その他のを紹介して欲しかったかな。

で、それで実装した自前のグラフィックで遊んでました。まぁ、ライブラリ書いた時点でかなり満足してしまうものなんだけど。

その後、大学院でレーザプリンタが導入されるわけだけど、こいつにも「円を書く」とかいう機能はなくて。PostScript 以前の時代だから。で、

　　LaTeX書いた論文に図を載せる

とかいうと、やっぱり円を自分で書く羽目に。ところが、

　　円をアフィン変換する

必要がある。問題なのは楕円の回転ですね。DDAでやればできたんだろうけど、結構、面倒くさい。なので、

　　ベジェ曲線で近似する

方が簡単。ベジェ曲線自体の描画はやさしい。

いろんなベクタグラフィックスのフォーマットを相互変換する時にも、楕円の回転問題が出るので、ベジェを使ってました。

今は、主に OmniGraffle を使って SVG で表示してます。

Kindle 本

OSの教科書は Tanenbaum の Modern Operating System なんですが、一応、Kindle 本もあります。でも、

　　学生がなんか買えない

とか言ってる。おかしいなぁ。去年買って手元にあるんだけど。でも、unavailable とか出てる。

この Kindle 版かなりのクソで、

　　コピペができない

課題出す時に問題が写せない。なんだよ。さらに、

　　一つのデバイスでしか読めない

普通は、Kindle は登録デバイス全部で読めるんだけど、一回に一つの Kindle デバイスにしかdown load させない仕組みらしい。消せば他のデバイスに down load できます。

ま、重くないとか、その場で辞書ひけるとかの利点はあるんだが、

　　Kindle / Amazon くそすぎる

のは確か。まぁ、ペーパバックは買えるようなので、そっち買ってくださいってところだが...

なぜ、買えなくなったのかは謎だな。去年買ったのはとりあえず、そのまま読めてはいます。

英語アカウントと、日本語アカウントは、まだ使い分けているのだが、com/jp どっちもだめらしいです。

Modern Operating Systems: Global Edition
by Andrew S Tanenbaum et al.
Link: http://a.co/iFi1ipC

目医者さんと歯医者さん

眼の方は薬が効いているらしく、徐々に良くなっている感じ。診察でもそんな感じ。ちょっと、その眼底写真見せてくれませんか? まぁ、でも一喜一憂するものでないからなぁ。

歯の方は奥歯の方がちょっと奥がたまに痛くて。根治する必要があるらしく、9月は割と通ったのですが、

　　薬入れて仮止め、また来月

みたいな感じ。血圧の方も薬を少し強いのに替えられちゃったしな。

まぁ、徐々にお医者さんのお得意様になりつつある感じ。まぁ、どれもそんなに高くないのが助かってるんですけど。

どれも診察とかあんまりたいしたことないんだよな。検査専用のクリニックとか用意して、そこで引っかかったら診察とか言う方が診察待ち時間がなくて良いんじゃないかなぁ。


Ingress のイベントの方は 450 まで来ました。500は明日には取れるんじゃないかな。2000は沖縄でも数人取った人がいるようです。根性とJarvisとUltra Linkですね。キー取るのがかなりつらいらしいです。一日50ぐらいのペースだと、それほどはつらくないです。

iOS, OS X upgrade

そんなわけで、iOS と OS X の両方の version up をしました。ほとんど差がないな。

先に、iOS 側をupdate 。OS Xは、xcode を先に update してから、High Sierra に上げる方法で。OSのupgradeよりも xcode の方がでかい。

どちらも特に問題なく上がりました。この前、SIP は外したのだが、OSのupgrade をしても外れたままだ。

今回の目玉は、もしかすると、

　　iCloud drive のファミリー共有

かな。App store のファミリー共有は、あまりにうっとうしくって切ってしまったんですが、iCloud drive なら使えるかも。

設定は iCoundのWebからはできなくて、MBPのコンパネから。え、なんだそれ。その場でパスワード入れてもらう方式もあるようですが、invitation 送るのが普通だと思う。

で、iCloud drive の容量を増やして... ってこれも、コンパネからかぁ。2TBにしましたが、どのように使うかは謎です。

昔の iTools/.Mac/MobileMe の時にも iDisk は結構便利だったんだが、いきなりなくなるとはね。Apple の Internet に関するセンスのなさは、今でも同じらしい。iCloud が無料になったのは良いけど、昔から有料で使ってきたユーザに対して、その値段の分のサービスを提供できなかったのは残念過ぎた。

iCloud drive をファミリー共有ありで引き継げていたら、そのままお布施してたんじゃないかな。

iPhoneのbackup だけなら、無慮魚5GBで十分なんだよな。

-

OSを上げないと...

iOS側とOSX側と一緒に上げよう思ってますが、少し憂鬱。でも、OSの授業では「最新のOSで」といってるのでやらんとあかん...

IngressのCF event は348まで来ました。まぁ、500はなんとかなるみたいです。

Ingress CF challenge

100は割と簡単に取れました。廻りのガチ勢も100までは楽勝らしいです。うちには、

　　初日で1000な人とか、600な人とかが...

初日に140いったので「理論的に取れることを実証した」とは思うんですよね。consequences are demonstrated ってやつね。

500まではいくとは思うんですが、まあ、2000は良いかな〜 (つうか無理)

既にある多重を反転してポータルを落としてお代わりするというのが基本的な戦略なので、ポータルをあまり堅くしないという風になるのは良いかな。AXA x 2 とか良くないなと思っていたので。

コードギアス

Clamp のあのアニメですね。2006年なので、かなり前です。RD-Z1買ったばかりでリアルタイムで録画していたんですが...

　　全然観ず

まぁ、そうだよなぁ。歌舞伎と言うか宝塚というか、そういう絵なので。でも、当時、それなりに盛り上がったはずです。

観なかった理由は見直してみて、割とすぐにわかりました

　　ギアスの使い方がぜんぜんなっとらん! 人を使う呪術なんだから、自分が表に出るんじゃな〜い!

こういうのは自分がギアスを使われたと思わないようなギアスをかけるんだよ。本当はやりたかったこととかさ。生きなり正反対なことをやらせちゃだめ。

でも、まぁ、中二病アニメだからな。正しくワイドスクリーンしている気もする。お父さんな話だし。そう思えば、

　　ルルーシュ君がいじめられて、どんどん悪くなっていく

のが面白かったです。女の人はこういうの好きだよね? 彼の

　　やっちまったが仕方がない。状況を利用するだけ利用しよう

という態度はなかなかよいと思います。スザクも。終わり方も中二病的な自分勝手だったが、この話にはふさわしい感じ。

R2は展開も早くて、話も広がったので、楽しめました。劇場三部作は、また、機会があったらだな。

2000 CF

https://plus.google.com/+Ingress/posts/EoBBmU7Dhbx

2週間で100/500/2000 CFを作れというイベントですが、メダルがダサいのはまぁ良いとして、

　　常識で考えて2週間2000CFは無理

普段のingressでも一週間80CFぐらいは作っているらしいんだけど、一日140作らないとだめな計算。17倍は無理です。1日90CFは作ったことがあったと思うが...

この前のレゾ刺し3113はなんとかクリアしたけど、普段の3倍くらいだった。10倍やる日が4日あるとなんとかなったわけですけど。

CF(三角で囲ったポータル)の一点を反転させて、もう一度取るのをおかわりというわけですが、それを一日10回ぐらいやればいけるかも。 嘉数高台で最大で12CFとかだった気がする。一時間あればできて、それをお代わりすると、一時間は反転できなくて... まぁ、一回ぐらいは一日140CFとかできるかも知れないけど。一日400C 作れる日が5回あれば。

とかなんとかですが、結論的には2000CFは無理だと思います。500は、まぁ、二週間のうち、4日ぐらいCF作りまくる日があれば。

誰だよ、こんなの考え出したの。

Javaのpackage名

なんか gradle で jar を作るんだけど、その中に入ってないものがあって。test は自動的には含まれないらしい。それは、

　 from configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } + sourceSets.test.output

と build.gradle と書けば良いだけだったんですが...

package 名に大文字と小文字が混じっていて、しかも、test側とmain側で違う... あらら。どうも、

　　Java の package 名は小文字だけ(と.と_)

という規則があるらしいんですが、うっかりやられてしまったようです。

で、

　　hg mv Hoge hoge

とするのだが治らない。OS X のHFS+は大文字と小文字の区別で余計なことをするのが原因。ぐぐ。ぐぐると、Stack Overflow が引っかかる。さすがだよな。

　　hg rename Hoge tmp
　　hg rename tmp hoge

しろと。なるほど。いろいろ疲れるお話です。

最近、ちょっとやるべきことが多すぎるな。もう少し絞りたい。

VHS発掘

昔の8mm フィルムムービーとかは、DVD/DVに全部移したはずなんですが、

　　もっとも古いのがない

あれ〜　どうしたのかなぁ。なんとなく実家にもっていたような気が。でも、

　　実家にあったのはVHS x 3

物はあっているらしい。ちゃんとラベルが書いてある。その後にDVに移しなおしたので、そっちからのがあったはずなんですけどね。

VHSから元に戻してもいいかと思ったんですが一巻2千円らしい。ちょっと高いかな。まだ、機材あるんじゃないか?

なんですが、自分は Hi-8 派だったので、なんとVHSデッキが手元にない。まぁ、Hi-8デッキも既に動かないんですが。

で、同僚に聞いてみると...

　　みんな結構もってる

偉いです。岡崎先生がDV/VHSデッキをもってきてくれたので、それを試すんですが...

　　いきなりDVテープを食われた
　　VHSも動かず

まぁなぁ。躊躇なく蓋開けて(自分の物じゃないくせに...)、DVの方はばっちり絡まって。でも、VHSの方はロードしてるな。いけるかも。たぶん片方が絡まると、片方も止まる仕様だなきっと。

なぜか、DVDレコーダは生きているので、それに転送。S端子ケーブルという懐かしいものも発掘しました。

というわけで、VHS x 3 は無事にデジタル化できそうです。

中身ですか? 父母の結婚式とか、中学高校の運動会とか、万博とか遊園地とか... 箱根とか草津とか。まぁ、愛を感じるしろものだな。

初期のはゼンマイ式16mmを往復使うやつらしく、画質はぼろぼろ。おそらくフィルムの質がよろしくなかったらしい。Hi8でないムービー8みたい。白黒だけど。でも辛うじて祖父の顔とかは判別できる。

Ansible

Ansibleの課題が動かないという問題が発覚。でも、これって、

　　去年やったことを、今年苦労しないために Ansible 使う

だったのではないのか。問題は、

　　php が 5 から 7 に変わったことらしい

結局、

< - php-mysql
---
> - php-mysqlnd

ですか。いや、これどこから見つけてきたの?

https://runble1.com/php-mysqlnd/

あれ、PHP ではなくて、MySQL5.6 の問題か。謎だ。

OS補講

まぁ、たくさん落としてるからやらされるわけなんですが...

　　課題半分出せば通るとか思っている人たちが

結構、怒ってるんですけどね。「全部出せ」

なのだが、毎年、update しているので、たまに

　　解けない問題がある

でも、それが現実社会だろ? 答のわかってる問題ばかりじゃないからさ。教科書はタネンバウムなんですが、教科書の問題も

　　ううーん、それどうなの?

的なのがたまにある。まぁ、解けない理由でも書いて提出してください。

とはいえ、大半は、クッキングブックで、

　　やればできる

問題ばかりです。Fedora OSのinstallとか。実験と重なっているのもあるので整理しないといけないものも。

さらに「シス管に申請しないとできない課題」というものある。サーバの公開とかね。

　　シス管とつながるのも、技術者の必要な技術

だと思う。(それをきっかけにシス管に参加してもらえればうれしいし)

今回の補講は6人参加。もともと、卒研と重ならないようにという意図なので、3年次とかは素直に後期を取るのを選んでいるようです。

　　TAが手取り足取り教えてくれるんだがな

まぁ、自分のプライドもあるだろうし、自力で解きたい学生もいるみたい。でも、人に聞ける、聞ける人がいるのも、自分の技術力だと思う。そういうのを身につけて欲しいです。

動いた...

例年、4月はM2のコードの後始末をしていることが多くて... 今年も Jungle と格闘していたんですが、ようやっと分散版が動いたみたい。

Functional Java とかが使われていたんですが、このライブラリがダメダメで、Haskell 版に負けるとかいろいろ技を出していた。それの再実装とか、いろいろ修正してたんですが、分散版の方は放置で齟齬がいろいろ。

package名の修正とかいろいろやらかしているうちに、method名間違えたらしく、最後に治したのはその部分。でも、debug で追求すると言うよりは、

　　こういうメソッドあるはずはんだけどなあ

で、ぼーっと見ているうちに「あ、これじゃん。あるじゃん」。で、版管理をたどると写し間違いが見つかるという。ありがちだな。ま、うごいてめでたい。

8月の東京行とか、目が見えなくて少しお休みとか、まぁ、いろいろあったけど、実質的には3週間ぐらいだったみたいです。

分散プログラムのデバッグは複数のプロセスを上げることが多いのだけど、Javaは fork がなくて、ちょっとはまる。おかげで、手動で複数のプロセスをあげる羽目に。このあたりの自動化が InteliJ とかでは自明じゃない。おそらくはなんかできるんでしょうけど。

大域変数がなければ、thread で代用できるので、そのテストをJavaそのもので書けるのですが、

　　学生のコードで大域変数の使用を見落としていた

M2のコードを細かく見ると可哀想な所もあるからなぁ。たしか、Alice のコードは年末に里帰りして戻ってきたら「できあがって動いていた」ので、なおす暇がなかった。

2年前に取ろうと努力したことがあったんですが、量が多くて挫折... API も変更しないとだめだし。

　　大域変数、基本禁止しないとだめだろ!

でも、CUDA でもAPIが大域変数依存らしく、いろいろ動かないところが。いずこもおなじか。

まぁ、久しぶりに Alice 自分で書いてみると「お、これは楽だ」。学生もAlice書きやすいとかいってたんだけど、あんまり信じてなかったんだけど確かに楽。ただ、API構文が汚いのが欠点だな。ま、作り直しが楽しみです。

たかね

なんか、沖国大のローソンのそばにラーメン屋さんが。宜野湾図書館のそばのラーメン屋さんの姉妹店だそうです。

つけ麺ですが、タンメンもあるらしい。つけ麺は三竹寿風の太麺で割と良かったです。宜野湾の三竹寿は僕には重すぎるけど、ここのは大丈夫。

普天間のまるよしが北谷にいっちゃったので(真栄原からはバス乗り換え)、その替わりになるかな。

台風18号

名前で呼んでたのはどうなったんだ? 久しぶりの台風ですが、それてはいるのだが、

　　本島を巻き込むように廻るコース

らしいです。激しいってほどでもないが、雨風が。

靴に油塗って出勤しております〜　ついでに Ingress もね。少しは真栄原取り戻しました。

台風とは関係なく飲みに来いメールは来るし〜

Ingress の補給

Ingress は、ポータルをハックしないと武器とかバリヤーとか出ないので、補給しないといけないわけですが...

池袋から要町周辺は青のエージェントが多く、バス通り辺りがL8ポータルの事が多い。昔は谷端川の公園がL8だったりしたんですが、それは最近は許されないようです。

沖縄でも青エージェントは多いので、58沿いはL8が結構あったりする。なので、那覇までバスで出るだけで結構補給できます。

なんだが、

　　真栄原周辺を網羅的におとされり

するとさすがにな。やっぱり、補給仕様のファームかFFが欲しい所。東京はFFの方が主流かも。それは、それで楽しいです。沖縄だとFFは珍しいかな。

久しぶりに沖縄で補給しましたが、東京のFFの補給に比べるとゆっくりかも。フラッカー炊いて倍速とかだからな。まぁ、でも、30-40分公園でのんびりするのも良いかも。知り合いのエージェントとも会うし。

東京だとFFの後は焼いたりするんですが、放置される場合も。ファームがなければ全体のactivityが落ちるだけだと思うけど、敵に補給されるのは嫌という人たちもいるようですね。

blog は 2005年から

mixi でしたが、blogger の方に移してあります。

　　http://seeker-s-eye.blogspot.jp

今も facebook と両方に出してます。facebook は検索が恣意的で不便なので。前に何書いたか検索しないで書くのは危ない。まぁ、たしょうあれでもいいんだけど。

でも Netnews は 87 年からのが手元に。まぁ、黒歴史だけど。 というわけで30年分のblogが手元にあるわけですね。Bloggerの方でも12年か。

10年前何やってたかとか見れるのは面白い。2010年に2001年のデジカメの写真をDATから発掘とかしてるらしい。 LLVMは2011年から読み始めて、2013年には自分たちで修正できるようになっていたらしい。

目の注射

してきました。1時間半ぐらいで終わり。点眼で麻酔して注射されるだけだけど、まぶしいのがな。麻酔があるので別に痛くはなかったです。

一ヶ月後に健診だそうですが「また、注射ですか」と言ったら、ちょっと笑われた。まぁ、状況によっては、また注射なんだろうけど。

見えない時にはMBPの拡大機能を使っているんですが、解像度そのものを変えるかどうか検討中です。

まぁ、そもそも廻りの人に「それ見えるの?」とか言われるような解像度で使っていたので、無理あるんだよな。

Twonkey Media 復活

QNAP のversion upで、Twonkey Meida (DLNA サーバ) がなくなって、Plex 使ってたんですが、や0っぱりダメで。反省して、

　　Twonkey Media を本家からinstall

というのをやっみました。

　　http://twonkyforum.com/downloads/

から見ると、8.4.1 とかいうのが。

　　Qnap arm-x09 package
　　Qnap arm-x19 package
　　Qnap arm-x31 package
　　Qnap arm-x41 package
　　Qnap x86 package
　　Qnap x86-64 package

とあって、どれだがわからないのが残念ですが、431 なのでARMなんだけど... 結局、若い順に試して、x31 で動きました。これで現状復帰。ライセンス料取られたのは、ちょっとなっとくいかないが。

研究室にある Apple TV も赤外線リモコン探し出して動かしてみましたが、林檎の画面から進まず。USBでiTunes接続しても認識しないので、こちらはご臨終だな。新しく買うと1万5千円か。ちょっと高くない? 中身、ラズパイ程度でしょ?

DLNAサーバ

QNAPを4TB->6TBにした時に、Townkey DLNA server がなくなってしまいました。OS upgrade なら残ったらしいんだが... 手動で入れ直すとライセンスを買う必要があるらしいんですが、うまく動作せず。どうも、Townkey は transcode していたらしく、ちょっと遅かったんですが、まぁ、だいたい動いていたので、ちょっと残念。 QNAP付属のDLNAサーバは使い物にならず。で、Plex も試してみたのですが、なんかこれも動かず。なんだが、

　　東京から戻って、Plexをもう一度試してみると、なんか見れるのがある

う、うーん? 規則性が意味不明。古い奴なら見れるというわけでもないらしい。徐々に見えるものが増えてる気もする。QNAPはなんか無意味に動いているし。なんかやってるのか? 全体の5%程度が見れる感じか。

nPlayer で、iPad/iPhone側から CIFS mount してやるど見れるので、Apple TV 使うという手もありますが、無線LAN二重にアクセスするのはちょっとあほっぽいな。 クライアントにはPS3使っていたんですが、これもだいぶ古い。ソニーのテレビでDLNAサーバに接続するというのも可能。もっとも、DLNA自体がくそ古いわけなんだけど。 余ってる Mac Mini を繋げたこともありますが、テレビ見るのにPCのUI使うのもなんだかね。

TownKey DLNA server は割と快適だったので、PLex を放っておいて、全部、見れるようになるなら、それがいいかな。

まぁ、わりとわけわかです。PS3 も壊れちゃったので、なんか買うか? DQ11 がSwitchで動くようになったら、それでも買うのが良いかな。

洗濯機のUI

母が洗濯機の前に立ちすくんでいて。どうも、どのボタンを押して良いのかわからないらしい。これだよというんですが、

　　「一時停止と書いてあるから違う」

とおっしゃる。確かに「スタート/一時停止」と書いてある。その上に小さく「これっきり」とも書いてあるんですが...

なので、一時停止の所に黒いビニールテープを貼ったんですが、

　　ご丁寧にはがしてくれた人がいる

まぁ、だいたい誰かはわかるけどさ... とりあえず、マジックで塗りつぶしてみましたが、どうなることやら。

うちの洗濯機も壊れたとかで新しくなったのですが、

　　普段消えていて、スイッチを入れると光るボタン

いや、かっこいいんだけどさ。もう少し、

　　What you see is what you get

にしてもらえませんかね? 同じボタン連打でモード切り替えがだめだとか80年代の話だよね?

東京のIngress

池袋の54連の「かえるさんの洗濯バサミの見た風景」と「夏の大三角」を片付けて、ミッションのonyxは撮りました。

だいたい100位くらいだったみたいです。

目医者さんには「何か運動してる」と聞かれたので、Ingress と言ったら「いろんな場所にいってやるやつね。どんどんやりなさい」と言われました。

が、すでにガチ税なのに、これ以上できるのか? でも、まぁ、2014年の頃よりはさぼっているかも。

目医者さん

沖縄に戻ってきました。

東京にいる時に、なんか画面見えないなと思っていたんですが、見えてない部分があのに気がついたる。なので、目医者にいきたかったんですが、移転中だったり休みだったり。結局、沖縄ん戻ってから。

最初は真志喜の長濱眼科へ。

最近は、写真撮ったり、断層検査があったりで、「これは出血してますね」というわけで、黄斑浮腫だそうです。動脈硬化の結果らしい。まぁ、血圧高くて申請血管がとかいってたからなぁ。

投薬で様子をみて、だめなら比嘉眼科とか言われたので、紹介状出してもらって、そのまま比嘉眼科へ。診断は変わるわけではないですが、眼球に注射する薬があるらしい。

動脈だと緊急を要するらしいんですが、静脈だと薬で元に戻るといいねぐらいなみたいです。これくらいはまだ軽い方ですみたいなコメントをもらいましたが、気休めとしてはいいかも。

でもまぁ、動脈硬化は他にもいろいろあるからなぁ。まぁ、家系なんだけど。せいぜい気をつけます。

打ち上げ花火

なんとなく見てきたのですが、

　　こんなに子供っぽいのでは、ちょっと残念すぎる

「君の名は」を期待してはいけないってな知識はあったんですがね。

この手の繰り返しものには「繰り返しを通して成長する」ってのがあると名作になるのだが... それがまったくないと尻切れとんぼで終わるしかないってことですか。

女の子とがかわいければ良いんだよと開き直るのがせいぜいかな。男の子の妄想の世界でしたで終わってるわけだし。

P.K.Dick の Eye in the sky 的な脱出ものにすれば良かったのか?

Ingress Mission

順調に片付けていて、Misshon medal black までは来ました。

沖縄だと車前提なミッションが多くて。那覇まで出ればそれなりにはあるんですが。

池袋のはやポチだけで192あるそうであす。楽です。

夏の大三角は駅周辺30だったかな。今は「かえるさんの洗濯バサミが見た風景」をやってます。帰るまでには終わるでしょう。

このミッションは、緑がよってたかって削除したポータルを記念して作られたらしく、「全部 No で」といわれたので、だいたいそうしてます。

いつものお見舞い

母の妹のいる施設に母を連れてお見舞いに行ってきました。これをすると東京に来た用事の半分ぐらいが片付いた気がする。

まぁ、ボケは進んでいるようですが、仕方ないかな。でも顔色は良く食欲もあるようでした。車で送ってもらったので楽でした。半分寝てた。

　　 最果ての銀河船団
　　 http://amzn.asia/54pYPhx

は、施設にいる老人に人がやってきて星の見える丘に連れ出して「あれが、これから出発する船団です」ってやるんだよな。

超準解析

学部時代に存在を氏って、斉藤先生の本とか買っていたんですが、

　　肝腎のモデルの話がない

で、ロビンソン先生の元が読めるわけなので、そちらを読むわけですが、超フィルターとか出てきて良くわからなかった。

今回は、

　　https://math.berkeley.edu/~jhicks/links/SOTS/koneill030514.pdf

を読んでみました。何回か集合論勉強したので超フィルターだいぶましになってる。

　　If A, B ∈ F,then A∩B ∈ F
　　If A ∈ F and A⊆B⊆I,then B ∈ F

フィルタ自体は割と簡単。ある集合Iの部分集合の集まりFで、その要素の共通部分もF含まれていて、ある要素を含む集合も含まれているというもの。ブール代数のイデアルの双対みたいなものらしい。

超フィルターFってのは、Iの部分集合Aを取ると、AかAの補集合がFに含まれるもの。これを使ってIの部分集合を二つにわけて、いろんなモデルを構築するわけね。簡単な例は、あるIの要素aを撮って、それを含む集合とそうでない集合にわける。そうすると超フィルターになりまう。a がA入ってなければ、Aの補集合にはaは入っているから。これを Principal filter というらしい。

超実数は、実数が整数の無限列なのと同様に、実数の無限列として作ります。
四則演算は、実数列それぞれで行えばよい。
問題は、こいつに順序が入るかどうか。それぞれの列の実数を比較して、1と0を割り振ると、

　　1と0の無限列ができる

で、1が多い方が勝ちにするわけだけど、特定の列で決まってしまうと具合が悪い。1と0を逆転させると結果は逆転して欲しい。つまり、1,0の無限集合の部分の集合が non principal な超フィルターFに含まれるかどうかで勝ち負けを決めると良いらしい。

で、問題は、non principal な超フィルターFが存在するかどうか。non principla ってのは、

　　どんなIの要素aを取ってきても、それを含まないFの要素の集合がある

ってことね。フィルターの要素の共通部分はフィルターに含まれるので、

　　有限個のIの要素を取り除いた集合はすべてFに含まれる

ということ。有限集合はぜんぶ含まれない。問題は無限集合で無限個の要素を欠いたものだな。これを全部含むと超フィルターではなくなってしまう。そこで、

　　有限個のIの要素を取り除いた集合をすべて並べて、その共通集合を取っていく

そうしてできたものをFとすると。選択公理があるなら、これが可能。で、選択公理を仮定しないとないとしても良いらしい。

要は整数の部分集合の集まりであるnon principal 超フィルターを仮定すると、超実数に全順序が入るということらしい。

ここまで来るとあとは簡単で、

　　どんな小さい正の実数よりも小さい正の超実数を無限小とする
ある超実数は、ある実数と無限小分だけしか違わない

無限小だけの差しかないを、 ≃ とすると、これが同値類になり、実閉体で成り立つものは、= をこれで置き換えるだいたい成り立つというわけですね。

デルタ関数とかも普通に関数として定義できるらしい。便利。

　　http://planetmath.org/constructionofdiracdeltafunction

でも、超実数に対する直観は、やっぱりモデルの直観だと思うので、εδとかよりわかりやすいかどうかは。

超フィルターが存在するかどうかは選択公理に依存するので、そんなものあるのという疑問は正しい。なので、ちょっとやっっかいな感じ。でも、

　　超実数に全順序がある

ということ自体はわかりやすいかな。これを認めれば良いかもしれないですね。

ハクソーリッジ

見てきました。東京では午前中の上映しかなくて、なかなか見に行く根性が。日曜日のロサ会館だがガラ空きでした。

浦添ようどれの戦いですね。普天間から嘉数高台の激戦の直後なはずです。高台からはえ割と平坦で、そこから長く崖があるので、そこですね。 何故、米軍が裏からはさまなかったってのは議論があるらしいです。

銃を持たずに衛星兵と戦うわけですが、そこまでの話が面白いかな。扱いに困る廻りと、プライドのために戦う人という構図。彼女がとってもアメリカンでいい感じ。

戦争シーンは、もう少しという感じ。日本兵の歩兵戦略をもっと描いて欲しかったかも。まぁ、あれがハリウッドの期待しているものなんでしょう3ど。ようどれのてっぺん自体は広くないので、ちょっと違うんじゃないかな。そこにこだわる監督はもういないですかね。

嘉数高台にはトーチカ跡がありますが、ようどれはお墓が復元されただけで、戦闘の跡はあまりない。でも、艦砲射撃で地形は変わってしまってます。

今では眺めの良い Ingress 激戦区か。いや、ようど3れあたりは、割と平和で白ポがたまにあるかな。自分の守備範囲という認識ではあるんですが。

fj 同窓会

今回は新宿ルミネの中のベトナムアリス。良く、土曜のお昼に予約取れたな。

電子メールとネットニュースは初期のバケツリレーメカニズムでの実装はほぼ同じで、電子メールを繋げるとネットニュースも付いてくるという感じでした。

企業と学校、日本語と英語が入り混じっていて、独特な雰囲気だったかな。今のFacebookと、それほど差がない気もする。入れ物が変わっても中身は変わらないもの。

Know how が貯まらないってのは、ネットニュースでも2chでもSNSでも同じか。Wikiとかにしがみついている人たちも。Stackover flow も本質的な差はない気がする。

ということは、まだ、改良の予知はあるんでしょうね。

それと今回の集まりとは、まぁ、あまり関係なく。緩い昼ビールな食事会でした。また、呼んでください。

母との日々

実家で母とのんびり過ごしています。ヘルパーさんが来てくれる日と、デイサービスの日と交互に。

たくさん連れ出してくれるヘルパーさんとか、家事をいろいろやってくれるヘルパーさんとかいろいろいて面白い。

母もぼけは進んでいるようですが、にこやかに過ごしていただければうれしいかな。4人姉妹も、だいぶお年を召してきたわけですが、4人それぞれだな。

Ingressで洗濯物は多いのですが、洗濯機廻しておくと、ちゃんと干しておいてくれます。たたむのは、そろそろめんどくさいらしい。

今日は研究室の東京にいる卒業生たちと食事です。行ってきます。

東京のIngress

西8池袋は割と青いです。立教が夏休みだから、そういう影響もあるだろうな。

要町までにバス通りに8ポがたくさん。千早フラワー公園にはFF後が放置されていたり。そんなわけなので、補給には苦労しない感じ。というか、X8が300すぐに貯まって、あまり使えないんですが。まだ、本気で緑の所を荒らしてないからなんだけど。

ミッションはたくさんありますね。池袋西口ぶらり旅ってのを片付けたので、次は、

　　夏の大三角

という30連をやろうかと。池袋周辺なはずです。まぁ、のんびりと。元気な人は一日で終わらせるんだろうけど。

Ingress、ミッションの検索性の悪さはなんとかならんのかなぁ。

東京は暑い

そんなわけでしばらく東京にいます。(-8/30)

実家の一階のクーラーは壊れているっぽいな。二階が外よりも暑くて、

　　冷えるまで外で飲んでるか

で飲みに出て帰ってきたらクーラーは切られてました。まぁ、少しはましになっていた...

今回は、東京のIngressミッションを少し追求したい。

免許更新

もう、5年たったか。相変わらずのペーパードライバーですが、今後、運転する機会のないことを祈るだけだな。嫌いってわけでもないが、廻りが危ない。

で、バスで南風原までいくわけですが、宜野湾から1時間、大学まで2時間ってなところですね。

なんだが、

　　病気で気を失いましたか

とかいう問診票が。そういえば手術したし、麻酔中は意識なかったな、と思ったが、'もちろん、「いいえ」

だが、

　　日付が読めない

とか言う文句が。

　　くだらん意味ない書類か書かせて、さらに文句言うのか? 誰も見ないだろ!

日付が読めないぐらいで文句をつける方がおかしい。いや、下手だが読めるし。サインが読めないというぐらいおかしいだろ。

　　いや、サインが読めないって文句は海外でもあるらしい

んだけど。日本語のサインが良いという人もいるけど、そういうこともある。

といういわけで、免許更新はできたようです。次は更新するかどうかは謎です。鬼が笑うか。

X.v6 ARM を OS X のclangで作る

Linux 上のGCC ARM Cross compiler で作るのは普通にあって、それで作ったのを大学院の授業では読んでみたわけですが...

　　clang で作れるんじゃないか?

で、clang -arch arm で ARM をはいてくれるわけですが、OS X だからな。elf ではなく mach-o 。まぁ、いろいろいろ問題はあるが...

　　entry.S

が通らない。なんか命令がないとか言ってくる。


　　1:
　　　 CMP r1, r2
　　　 STLTMIA r1!, {r3}
　　　 BLT 1b

とか書いてあるんですが、しばらくわからなかったんだど、LT って、Predication か。アセンブラの命令に条件をつけられるあれですね。じゃぁ、

　　　 STMIALT r1!, {r3}

だろ? LTは後ろに付くはずだけど。これで通りました。なんだよ。

なんだが、問題は Linker か。開始アドレスを指定したり、segment の位置を指定したりしないといけないんだが、OS X の ld でどうやればいいのかがわからん。

できないってことはないんじゃないかなぁ。

まぁ、clang を elf をはくように作り直しても良いはずなんですが、mach-o でやっても面白いかな。

GCC版なCbCもあるんだが、最新版に合わせるのは大変なんだよな。

gcc なcross compilerはあるので、それでclangを作っても良いんだけど。

いろいろ方法があるだけに悩ましい。

Mendeley

論文管理サービスですね。いろいろ比較して、Papers.app を使っているわけですが...

　　お前、琉大だろ、メンバになれば容量増やしてやる

みたいなメールが来てたので、再度トライ。ばっちりパスワードなくしていたので再発行から。昔よりはだいぶ良いかも。昔のMendeley って妙に複雑でさっぱりわからなくって。

で、BibTex の読み込みってのがある。D論書いた時がLaTeXの出た翌年だったりするので、BibTeX使いです。なのだが、

　　さっぱり読み込まない

一つだけなら読み込む。じゃぁと、BibTeXのentoryを論文毎に切り分ける Perl script を書いて一括登録〜としたら、やっぱり蹴られる。やっぱり使えんな〜

でも、Desktop app があるな。で、そっちを使ってみると、

　　ちゃんと読み込めました

Webサービス側で手抜きしただけか。誰も使ってないんだろうな。読み込めたけど、それだけだな。

この手のものは、すぐにネット上に上げさせるけど、量的に無理なんだよな。2.3GBなのでたいしたことはないんですが。TB1万円台になっていて、それくらい出しても良いけど、

　　サービス毎に1万円出すのはバカすぎる

一方で、自サーバを使えば1万円で4TBぐらいのサーバを作れる。それが現状だよね。なので、やっぱり Papers かな。

Mendeley は学生との参考文献共有に向いているとかあったんだけど、どうなんだろう?

　　https://www.mendeley.com/

agda-vim

いろいろ動かなかった agda-vim ですが、なんとか動きました。

　　https://github.com/derekelkins/agda-vim

~/.vim/bundle の下に置けって書いてあるけど、それをするためには、pathogen ってのを使わないといけなかったらしい。

　　https://gist.github.com/romainl/9970697

まぁ、いろいろね。Get Pathoben と Configure Pathogen をやるらしい。

で、動いたんですが、

　　,l で reload すると、一旦、Terminal画面にvimから戻って、agdaのSkipping ... が大量にでる


これはちょっとなぁ。Emacs だと、別バッファ上でやるので、元のバッファは残ってる。消えるのはちょっとなぁ。

学生は「動画を見る限り使えるようですが」とか言ってましたが、動画でも同じ状況でした。作った人は「でっかいターミナル一つ」な人のようで、それだと気にならないんだろうな。

ちょっと、ソースを見ると、

　　def RestartAgda():
　　　global agda
　　　agda = subprocess.Popen(["agda", "--interaction"], bufsize = 1, stdin = subprocess.PIPE, stdout = subprocess.PIPE, universal_newlines = True)

ってことで、Python 2.7で実行しているらしい。　この辺でダサいことになっているんだろうな。プロセスの扱いは Emacs は最初から頑張っていた。

vim でもterminal modeとか作っている人がいるようですが...

自分で手直しするかどうかは気分次第だな。subprocess.Popen を追求するのは気が重いです。

まぁ、でも、その reload を我慢すれば、まぁ、使えます。Emacs の vipper と agda の相性の悪さと戦うよりは良いかも。

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

MBP setup

ほとんど終わりました。ほとんどは、brew/brew cask で。

ちょっと、はまったのは、Agda のlibraryの設定。blog に書き忘れたんですが、Agda に自分のlibraryを付け加えるには、

＊ ~/.agda/libraries
/usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
/Users/kono/src/public/category-agda/category-agda.agda-lib

＊ ~/.agda/defaults
standard-library
category-agda

というのを書く必要があるのでした。Emacs 側からできるのかも知れないけど、まぁ、いいや。

brew list
＊ agda cabal-install gdbm mercurial openssl python sqlite
＊ antiword emacs ghc nkf pkg-config readline

brew cask list
＊ emacs mactex pdftotext

ぐらいですね。

Papers3 も、~/Documents/Papers3 をcopyして、Paper.appをいれて、ライセンス指定して終わり。

mhは、どうも、nmh ではなく MH-JPを使っているっぽいな。なんだよ。

新しいMBP

EnPITの予算関係でもらえるらしく。EnPIT ありがとうございます。学部でやってくれっていうのも、通って嬉しいです。

今のMBP、結構、引き継ぎ引き継ぎで来たので、さすがに clean install でいこうかなと。ほとんどのファイルはサーバ上にあるので、無理に手元におかなくてもよいかな。

つうか、このまま移行すると、ラズパイのimageとかあるので、かなり時間かかるはず。670GBも使ってるな。

というわけで、つまり、あんまり移行できてません... Ansible とか Docker みたいなので minimum install したい...

iCould にデータを全部移すかみたいなのが出てくるけど、ちょっと高いのがな。1TBなくすとか、また、せこいわざを...

File Vault とかもデフォルトで入れようとするようですが、 もちろん拒否。

無意味なセキュリティのおかげで、OS X上のOSの課題がめんどくなっているのがいくつか... dtrace とか gdb とか。

Unix系は、だいたい brew で入れられるはず。

Xcode
X11
TeX
Agda (Emacs/Haskell)
X11のAgda用のfont
hg
perl/Tk
nmh
ラズパイ用のqemu
Virtual Box
VMWare fusion
Papers3
FreeMind
Omni Graffle
Google Photo Backup
QuickRes (なんか有料になっていた...
滅多に使わない LibreOffice

あとは自前のPerl script 群か。Dockerも入れたんだが、ほとんど使ってない。

Google Drive も、もっと積極的に使って良いのかも知れんが、あんまり、気が進まなくてなぁ。

フードフリー and 黒ガー

日曜日は、いつもの宜野湾のフードフリー。なんですが、

割とすいてました

なんでかな。宣伝不足? 良くあるのは宣伝担当者が変わったとかかな。

で、真夜中に Ingress Guardian が150日に。1月辺りにも139までいったのがあったんですが、屋富祖だったので、最近activeになった緑(gurukamaとかfound000とか)にやられました。

1月に青の作戦があったんですが、

http://seeker-s-eye.blogspot.jp/2017/01/okinawa-ingress-resistance-operation.html

その時の反転ポータルの処理のやつみたいです。真夜中にあんなところに取りに行ったのか。

この所、沖縄は緑優勢。宜野湾真栄原も「網羅的に焼く」人が何人か。いや、僕もいろんなところを網羅的に焼きにいくわけですが。なので、真栄原辺りだとガーポは厳しいかな。

もっとも、ご近所指向の僕が取れるくらいなので、沖縄のIngressのactivity自体が結構落ちているってことだろうな。

土砂降り

今日は土砂降りで酷い目にあいました。

沖縄だと台風以外だと珍しいんだけどな。周回道路が川になってました。

まぁ、僕の移動がすんだら止むんですけどね。

小澤の不確定性原理

昨日のOSCの飲み会でビール飲みまくっていたら「先生どこですか」的な呼び出しが研究室OBから。なんで沖縄戻ってきてるのと聞いたら、

＊ 科学基礎論学会/科学哲学/科学史
＊ http://phsc.jp/conference.html

ぐ、懐かしすぎる。ぜんぜんアンテナに引っかかってませんでしたが、琉大でやってるのか! で、プログラムを見ると、

＊　　出口弘
＊　　小澤正直

ぐ、懐かしすぎる。東工大の吉田夏彦先生配下な人たちではないですか。

なんですが、さすがに三日連チャンで早起きは無理でした。遅刻しつつ、小澤さんの発表を聞くことができました。

＊　　σ(P)σ(Q) + ε(P)σ(Q) +ε(P)ε(Q) > hoge

だったかな。Hiesenberg のドイツ語の論文のアブストラクトとかが出てるのが吉田研っぽくって面白かったです。不確定性は indeterminancy から来ているのだけど、元のドイツ語は inaccuracy に相当する言葉だったらしい。それを英語の共著者が inderminancy とまずい訳をしたと。それにEinsteinが引っかかって、あんな議論になったかと思うと、まぁ、そんなことはないと思いますが。あの議論は量子力学の定義の精密化には訳なったわけだし。

というわけで、懐かしい面子に会えて良かったです。

OSC Okinawa 2017

いつもの内輪の展示会ですね。そういえば、両親も業界の内輪の展示会では暇そうにしていたっけ。

展示はいつものなんですが、セミナーのネタがなくて。なので、

＊　2月にいじっていた cmake の入門をやろう

と思ったわけですが、聴衆は自分の学生以外は三人でした。ま、まぁ、地味な話だからな。

cmake は、mavenとかgradleとかに近いかな。make が、わりと魔境になってしまっているので、

add_target ( target_name source1.c source2.c )

だけで、いい感じにやってくれるのは便利。まぁ、そこからいろいろやろうとすると、どうせ魔境なんだけど。

今回は自治会館。コンベンションセンタ、あるいは、OISTよりは、はるかに便利なところ。特に今日は雨だったので、沖縄では珍しい「駅から濡れずにいける会場」なのはうれしい。

GPU VDM

https://groups.oist.jp/external-events/event/gpu-accelerated-vdi-international-conference-2017-asia

いや、まぁ、琉大にはGPUクラスタないし。システム更新でも「GPUは毎年新しいのが出るから」で見送られたりしたので、いや、だったら、毎年なんか買えよ〜

と言うわけで、少し場違いなわけですが、まぁ、全然関係ないわけでもないしなぁ。今年の2月ぐらいはMac ProのGPUと格闘してたし。というわけで、プレゼンもすることに...

OISTなので、学生に車で送ってもらうわけですが、

8時と言ったのに、ぜんぜん来ない

間に合わないよ、で、かなに「すみません、送ってください」と頼んで階段を降りたら、下から登ってくるうちの学生が。「道が混んでて8時に出たのに30分かかりました」って、いや、そこ「8時に迎えに来て」って言ったのが「8時に迎えに出る」になっているところが、沖縄なんだよな。

まぁ、僕も、そんな感じで、いまだに遅刻魔なわけですが。

そこそこお金取られたので、ちょっと厳しい。学生の分がな。

そして、明日は OSC Okinawa です。そっちも、よろしく。一応、うちの学生のcmakeのセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。

Prolog とシーケント代数

去年も今頃授業でやっていたみたいです。関数型言語と同じで、

＊　　プログラム中での変数の論理的関係が理解しやすいように記述する

ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。

Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。

でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。


Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'

これだけだものな。

実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。

Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。

アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。

メッセージ

観てきました。原題が Arrival で、元の小説のタイトルは「あなたの人生の物語」ですね。

元の短篇が割と何も起きないタイプの話で地味。で、その通りに極めて地味に始まって「どーすんのこれ」だったのですが、ハリウッド的な拡大解釈が入っていて、そこそこ盛り上がりました。よろしかったです。

こういう、どうしようもなく人類が変わってしまう話って割と好きかも知れないな。正解するカドとか。

異世界言語の学習という視点ではどうなんだろう。深層学習使うシーンとか欲しかった気もするけど。一応、データの視覚化はやってたか。
アメリカ人的には、異星人がテレビとかラジオから英語勉強して、いきなり流暢な英語を話すとかを期待してるのかな。この手の言語習得は18-19世紀にはたくさんあったはずなので、そのあたりの蓄積があるはずなんだけどね。今はもう需要はないのか。

Emacs 25 の続き

というわけで、Emacs 25 と Agda 2.5.2 は、xterm/Terminal.app 上では完全に壊れてしまって。C-C C-L するたびに→が増殖する始末。気持ちはわかる。Emacs は昔の端末流に描画の最適化ってのをやるわけ。この位置だけ書き換えればよい的な。それを、Unicode 上でやると、どうしても位置がずれる。Terminal 上での描画幅は正確には知り得ないから。でも、行頭から順に描画すれば良いはず。なので、vim とか Emacs 22 では問題ない。壊したのがいるってことね。

しょうがないので、GUI版を試してみようと思うわけですが、どうinstallするのかが謎。結論的には Mac OS X では、Homebrew で、

  brew tap caskroom/cask

  brew cask install emacs

とすれば良いらしい。また、Emacs 入れ替えか。

Agda 側は

brew install agda

で良いらしいです。Haskell は brew install ghc らしい。

で、GUIで立ち上がるわけですが、

Font が小さい

いや、 2880x1778 で k14 使っている僕が言うんだから、かなり小さい。文字幅1mmないだろ。でも、Agda は動いているっぽい。

で、Emacs の文字の大きさを変える旅に出るわけです。

C-X C-+

で一時的に大きくなるのはすぐにわかりました。そして、Option Menyu に Set Default Font... がある。大きくして、Set Default Font か。

もちろん、再起動で元に戻る

あ、あーん? で、見つけたページがこれ。

Emacs：一発で文字サイズを変更する方法
http://lioon.net/emacs-change-font-size-quickly

つまり。「GUIから文字サイズを変える手段はない」ということらしい。.emacs か! そこで、

Set Default Font... を押すと Font Menu は出てる

というのには気がつきました。でも意味はないらしい。 Set Default Font... ってのは嘘ってことね。Font Menu は閉じないと再起動でも開く。なんだよ。

なんですが、このページに書いてある通りにしても動かない。Twitter でぐちっていたら、

.emacs があると、.emacs.d/init.el は読まないよ

って、ばっちりそれでした。mv ~/.emacs ~/.emcas.d/init.el か。

それで動いたんですが、翌朝になるとまた動かない。なんだよ〜

そのうち、

fontset-standard undefined

とか言われて、New window もできないように。

で、init.el の中で frame の font を指定してみたら、

VL Gothinc not found

とか言ってる。そうか、

    (set-fontset-font "fontset-standard"
              'ascii
              (font-spec :family "VL Gothic" :size 20) nil 'prepend)  ;; ここでサイズを指定
    (set-fontset-font "fontset-standard"
          'japanese-jisx0213.2004-1
          (font-spec :family "VL Gothic") nil 'prepend)

    (setq default-frame-alist
          (append (list 
                   '(font . "fontset-standard"))
                  default-frame-alist))

そのままコピペしたのがだめなんだな。VL Gothinc を monaco に変えたら動きました。あ〜　疲れた。

vim 版の Agda を試してみるべきだな。

新しい Agda

Sets (集合を対象、写像を射とする圏)の Completeness としばらく格闘していたんですが... Compleness ってのは Limit があることで、Limit ってのは、与えられた関手で示された対象と射のグラフ上の可換関係を代表する対象みたいなものらしい。

直積とかは二つの要素の代表なんだけど、それがあれば、その二つの要素にできることは全部できるじゃないですか。そんな感じ。

なんだが、なかなかできなくて。結局、

  record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
       ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
     field
         snmap : ( i : OC ) → sobj i
          sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
     smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
     smap0 {i} {j} f x =  smap f x

という record を作れば Limit の uniquness 以外は簡単に示せました。なのだが、uniquness が堅い。要するに、field 二つが等しければ、record 自体が等しいという合同性の問題らしい。

でも、ググってたら、にたようなのを Stack Over Flow で見つけました。(良くある)

https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types

なのだが、こいつの例題が通らない。もしかして、Agda の version の問題か? 確かにちょっと古いんだよな。

で、update をかけたんですが... なんか、emacs も update。あ、てめーちょっと待て。

emacs 25 に上げられてしまったおかげで、xterm 上の色とかUTF8がずれまくる。vim は大丈夫なんだけど。くそ、unusable だ。しかも。Agda は 25 でないと動かない。

GUIでしか動かさないあほが手を入れて xterm 側を壊してるんだよな。

で、肝心の例題は Agda のupdate で通ったんですが、Sets completeness の方は通らず。くそ〜 どうも問題は Agda のrecord の合同性の扱いそのものにあるっぽい。僕のせいじゃないらしいです。

    snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
                 ( s t :  snat SObj SMap   )
             → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
             → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡  (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
             → s ≡ t
    snat-cong s t refl refl = refl

が通るはず。だけど、通らない。これはあきらめた方が良さそう。

なので、Agda 壊れちゃったので、ちょっと困ってます。vim で編集して emacs でチェックみたいな感じ。

iPhone 7

このあいだ、また、iPhone の画面を割ってしまって。ワイシャツのポケットがほつれれてでかいiPhoneだと落ちやすい。落ちどころが悪いとわれるらしいです。

で、5月で2年しばりが消えるので、ソフトバンクからは抜けようと思っていたのでちょうど良かったんですが、MNPとか面倒くさすぎる。かなのauの家族割に入るのがやすいらしいが...

まあ、格安SIM試してみるんじゃないの?

っことで、IIJ MIO に。めんどくさいけど、ソフトバンクにで電話して、うだうだ話してMNP予約番号をもらう。こんなのWebから一発発行でいいのに。IIJの方はWebから申込。で、iPhone 7 plus は Apple から買うと。はい終わり。

と思ったが、IIJの認証が通らない。免許証の写真を upload する方式なのだが、そもそも普段使いのクレカでは通らないとかわけわからん。で、サポートに電話したんですが、

コーノとコウノ

の違いだったらしい。いや、コーノで統一しているんだが、通らないあほシステムが若干あって、そこではコウノにするしかない。ローマ字側を kouno で強制するのとかも見たことがあります。もしかすると、免許証がそれだったかも。

免許証には漢字しかない

はずので、おかしな話ではあるな。

と言うわけで、ネックはIIJ側だったらしい。SIMがくれば、

iPhone を最新iOSでバックアップ
SIMをactivateして、新しいiPoneのOSを最新に
そこに restore

という手順で動いたみたいです。まぁ、しばらくいろいろあるだろうな。

中部商業の歩道

中部商業から琉大の山道ですが、昔の山道らしく曲がりくねっていて。琉大直行のバスに乗れば良いんだが、いつもあるわけじゃないからな。

で、ようやっと歩道のなかった部分に歩道が。久米島みそのあたりで、道路にはみ出てる建物とかあるし、一応、バスも通る道だしで、結構、危ない感じでした。

20年目にしてようやっとかぁ。

とはいえ、ここを歩くのは琉大では僕だけだと思われる。中商生は結構歩いてるみたいです。

中商経由でいくと、行程の1/3ぐらいしかバスに乗れない気がする。まぁ、そんなんなので ingress 向きに歩きなれていたわけですが。

今日は涼しかったかが、大学に着くと着替える季節だな。

読み会最終日

学校に来てみると、なんかホワイトボードに多層パーセプトロンの図が。なので、Chainerから読み始めたんですが、

＊ Python での処理がずーっと

なので、なかなかCudaに行き着かない。cuda.py の部分のソースは用意されてなかったりしたので、そこまでで。

TensorFlowの方は、さっさとCudaに処理が渡って、何をしているのか割とすぐにわかったんですが... もっとも、Chainerの方がわかりやすいっていう人もいて、人それぞれだな。

午後は x.v6 arm の方を。ところが、ARM 7 ってGameboy advance の頃とは結構違う、っていうか、

＊ TLBとかは、Coprocessor なMMU でやるわけ?

TLB flush とかはMRCとかの Coprocessor 命令じゃなくて、専用ニーモニック用意しろよと思いました。ニーモニックってのは、そういうものだよね? まぁ、ARMの仕様の外にあるってこともかも知れないけど、納得できないです。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/innparusu/xv6-rpi/

で、Docker で動かせば、x.v6 arm の gdb trace がいつでもできるらしい。(VMと違って、setup には結構時間がかかるらしい ... )

というわけなので、ちょっと、物足りない感じではあったかな。x.v6 に絞った方が良かったかも。

ソースコード読み会初日

最初は minetest ( C++ で書いたマインクラフト) なんですが、

＊　Mac OS X だとキー入力できん

ってことで「じゃぁ、そこ見るか」。irr とかいうGraphics framework を使っていて、OnEvent というcall back で key event が来るのはすぐにわかった。わかったんですが、

＊　Key Event 自体が来ない

ぐ、これは Graphics Framework 側の問題だな、で、あきらめ。なんか、release でない最新版ではなおっているらしいです。

で、次は、x.v6 on Raspberry Pi 。こっちは、

＊　OS X 上のDockerで、qemu-system-arm で x.v6 動かして、gdb で接続して読むというのが可能らしい。ARMのアセンブラの説明して、UART にメッセージを出すところまで読みました。(つまり、ぜんぜん読んでない)

さらに、Chainer も OS X 上のCuda で動くので、そっちも設定。Pythong の debugger で、ちょっと追う。Linear とかで1000x1000の配列切ってるわけね。

というわけで、初日は、まぁ、準備できたかな〜　ぐらいです。

明日は、ハリーズのカレー食べながらって話になるはずです。

今週末はソースコード読み会

なんですが、どうも、何を読むかで盛り上がらず。いや、自分が盛り上がってないだけかも。

オープンソースなマインクラフト

これは C++ らしい。割と普通な感じ。Unity のを読みたい気もするが、なんか、あんまり良いものが見つからず。

Chainer

前回は Tensor Flow 読んだんですが、安直に作ったタスクマネージャー的な側面が強くて、GPU載っけたマシンで読むしかないのだが、あまり綺麗に読めないみたいです。

X.v6

また、これかぁ。悪くはないんだが、少し時代遅れかなぁ。

TOPPERS の組込みOSというのも見てみたのですが、うーむという感じ。

というわけで迷走中です。

Ingress Event

先週は恩納村に三日続けていく羽目になっていたわけですが(風邪ひきなのにも関わらず)、IngressのEventも並行して走ってました。

ま、風邪ひきななので控えめに参加してました。Builderもローソンも、そこそこ貢献できたみたいです。3113は恩納村送りにも関わらずギリギリ取れました。

他の人がイベントに集中していたせいで、いつものご近所IngressのCFが多めに取れてちょっとうれしい。

風邪ですか? だるだるですが、少しずつ咳も収まってきてるようです。

風邪ひいた

いつもの定期便らしく... 土日に既におかしかったんですが... ひっくり返せない予定が、あったので、結局、こじらせてしまいました。

恩納村三連チャンは、ちょっと無理だったか。

まぁ、週末休めばなんとかなるかってところです。

OS研究会

毎年の研究会ですが、今年も恩納村ホテルモントレーです。いや、やっぱり同じ場所は楽。その方がホテルとの交渉もスムーズだし。去年は懇親会でお酒を出せないみたいな失態があったのですが、今年は配慮してもらえたので普通の飲み放題な懇親会になりました。

沖縄に赴任した直後から新城先生を引き継ぐ形でホテルムーンビーチで開催していたんですが、その後はいろんな場所を転々と。那覇市内は便利なんですが、リゾートホテルが沖縄っぽいかな。

来年も同じ場所でできると自分的はぐっと楽です。その方針で行こう。

研究発表も今年は割と面白い。VMで動かすならプロセス要らないじゃんということでLKMとしてアプリケーションを動かすと速いとか、信頼できないハイパーバイザー上でセキュアにVMを管理するとか、QEMUの命令エミュレーションのバグを回避するとか。

Applicative

Haskell のApplicativeってのを去年はいろいろやっていたらしいです。で、にこやかにソフトウェア工学の授業で、Haskell やるんですが、

Functorってのは、fmap で

ふんふん。自分で書いたものだから自分では良くわかる。

のだが、あれ、続きがあるぞ? Applicative だし。あれ、その続きも。これ、どこまで続くの? おっと、Monad までいくのか。それはやりすぎだろ(→去年の自分)

去年の授業の時に、それなりに行き詰まって、で、書きなおしたんだよな。その時に勢い余ったんだろうなぁ。

途中に、理解を助ける課題を入れればいいんじゃないかな。というわけで、突っ走ったのを修正する必要があるなぁ。

fmap とか <*> とかって、型さえ合ってれば、いろんな実装ができるんだけど、実は満たすべき性質がいくつかある。それが実装を制約するわけなんですが、その制約は圏論から来るから、いまいちピンと来ないんだよな。

授業のページも版管理しないとだめなんだよな。そういえば、生成scriptにバグがあって参照ファイルの存在をうまく検出できないっていうのがあった。

猫の投薬は、だいぶうまくなりました。

GPU-Accelerated VDI International Conference 2017 Asia

http://asia.gpuvdicon.fml.org/index.shtml

というのがあるらしく。

この辺、なんかイベントが立て込んでいて、

オープンソースカンファレンス
https://www.ospn.jp/osc2017-okinawa/

もあります。どっちも何か出すみたい。がんばります。OSCは cmake ネタにしようかと。

GPUVDIは、学科紹介みたいな感じかなぁ。GPGPUは使っている人はいるんですが、GPUクラスタはあんまり使われないかも。

問題は、

アイドルグループ「AKB48」のイベント（選抜総選挙）が、OSC沖縄の同日（6/17）に、豊見城市で開催される

ことらしいです。

その前に、OS研究会があるか。

猫のお薬

まぁ、うちのくそジジイな猫もお年だからなぁ。血管拡張剤的な薬らしいんですが、小さい錠剤です。これを飲ませるのが今回のお留守番ミッションらしい。

膝の上に仰向けに抱え込んで、顔を押さえて、口を開けさせたら、奥に落とし込めば良いらしい。のだが、

　　ペッと吐き出す

こ、こいつ〜　しばらく格闘していたら、フーッ! とかいう。その時に口を大きく開けてくれるので、ばっちりでした。しばらく上向きに押さえてれば、吐き出せないらしい。でしたが、

ああ、なんか股間から放物線が...

ぐ、おしっこもらすほど怖い思いさせたか、ごめんな。

なんか仰向けに押さえるのが良くないらしく、座らせて、顔を押さえて「フーッ!」を待ったら、楽勝でした。

あとで水飲ませると良いらしいんだが...

Ingress Operation

といっても青の作戦だからな〜

国際通り周辺を青くする

って、それだけですか? もちろん、それだけであるはずもなく、

昼飲みは控えるように

という指令が... そして、そんなものが守られるはずもないのが青なので...

国際通りをしばらく歩くだけで、がんがんX8が補給できる、そんなことになってました。

GWの肉なイベントとかビールなイベントとかも楽しかったです。

青くすること自体は、みんなでばらばらに、残っている緑を掃討するみたいな地味〜な作業なんだよな。

まぁ、この青の作戦のぬるさが青っぽいと思うし、それも良いと思うこの頃です。

プログラミングIII

っていう3年次の授業なんですが、

なんか作る

ってなものです。なんですが、

なんか、ちょっと違う

とかいう理由で、最初にいた学生たちがいなくなる。もしかすると、今年は受講者ゼロかも。

3年次にはEnPitもあって、そっちも「なんかプロジェクトやる」ってなものなので重なってるんだよな。そっちの方が「ちゃんとしてる」かも。

どんなものを作るにしても、今はネットと繋げないのはありえないから、Web Serviceの構築はやってねみたいな感じでやっていたんですが、それが嫌われたか? Web Serviceの構築でも Web Framework やら、git やら、ansible やら、Jenkins やらでやること多いからな。まぁ、OSの授業で全部やってもらってるんですが。

で、何やりたいのと聞くと機械学習と答える学生が多いです。流行だからな〜 いいよ、好きなこと、どんどんやれ〜 うちの学科は昔から人工知能の先生がいるので、得意な分野のはずです。

Boost

いつもの大学院のソフトウェアを読もうの授業ですが、

Boost

読みたいという学生が。なるほど。C++ のtemplate baseの現代的な Library ですね。

C++ は型変数を template という一種のマクロで導入していて、それとは別に、

Smart Pointer

つまり、GCのないC++でオブジェクトの寿命管理をポインタの種類で制御するということを始めます。それが、

RAII Resource Allocation is Initialization

とかいうものらしい。実体は参照計数なので、Objective C のARCと同じ。まぁ、Swift では見えなくなっているわけですが。

iPhoneでは、一旦、GCを導入して、やめてARCにしたみたいな経緯がある。AndroidはJava だからGC base。

じゃぁ、GCとRAII/ARCとどっちが良かったかということになると、

構文的には面倒のないJava/GC

だろうなぁ。そこで、

BoostやSwiftで、面倒な Smart Pointer 構文を隠す

という行為に出たのではないかと。でも、

GCの技術から見ると参照計数は手間がかかりすぎてダメ

まぁ、そうだよな。Smart Pointerですむようなのは GC のアルゴリズムで、ほとんど効率的にGCされてしまうってのが実際なんじゃないかなぁ。iPhone のアプリでのメモリ由来のプチフリーズを経験した人は多いはず。

僕は GC は予測が難しいので嫌いですが、だからといって、Stack base/参照計数だけみたいな原始的なアプローチはちょっといただけないですね。

で、そのBoostのソースですが、もちろん、template の塊で、見かけないC++の構文ばかり。これなんだろう? みたいなのが。コンパイルしてみると、

小さい例題でもコンパイラが黙り込む...

おお。さすがです。でも、また、Boost.filesystems をちょっとかじっただけ。きっと、Boost.Graph とかは、もっとすごいんだろうな。頭の良い人たちはすごいよ...

iTunes Match

結局、自動的に renew は嘘だったらしく、iTunes のstoreを探すのだが、renew のメニューはまったく出ず。Subscriptionは切れてしまいました。Apple の意地悪さというかやる気のなさというか。まぁ、iTunes Matchはやめたいんじゃないかなぁ。でも、DRM free down load はまだ終わってない。

なので、三台目のOS Xから、もう一度、入れてみると通りました。わけわからん。前のデータは残っているらしく問題なく、iPhone側から再生できるようになりました。

なのだが、iTunes Match分を Air Play できないな。Down load してもダメだな。AVアンプに接続はしているので、もしかすると、SC-LX87が256k AACをサポートしてないのかもなぁ。

まぁ、たかだか62GなのでQNAPに入れて、外からQNAPにアクセスで良いじゃんと思わなくもないです。BD-R 三枚分とか誤差だな。

家のネットワーク

うちから海炎祭の花火を見物している時に、void が「iPhoneから音楽流したい」というので、いつものAirMac に繋がっているアナログアンプでも良かったんですが、

そういえば、パイオニアのAVアンプが使えるんじゃないか?

と思って。SC-LX87 の取説を見ると、WifiはないがLANはあるらしい。で、ケーブルと持ってきてハブにつなげて、いろいろやるんだが、

ぜんぜんつながらん

DHCP取らないし。まぁ、その時は諦めたんですが...

今日、外からBDレコーダーに(Sonyのアプリ経由で)つなげようとするとつながらない。あれ? で、BDレコーダ側を見ると、やっぱりDHCP取れてないじゃん。

結局、ハブとルータをつなげるケーブルがいかれてた。なので、ハブに繋がってるもの同士では通信できるので気がつかなかったんだよな。

それで、AVアンプもLANにつながって、iPhoneからルータ経由で鳴らすことができたみたいです。

たぶん、ケーブルが急にだめになったわけではなくて、バッファローのGigabitなハブとの相性なんだろうな。今時のは自動的にクロスかどうかを判定するのだけど、それがうまくいってないとか、そんなのでしょう。

しかし、うちにはEthernetケーブル何本あるんだ? そして、そのうち生きてるのはどれ? この前、GBit 用にケーブル買ってきたはずなんだが... 機材が増えるのに追いついてない感じだな。

itojun の墓参り

これも10年かぁ。青山霊園。たまにしかお墓参りしないので、

場所がわからない

なんとかなると思ったのだが、けっこう広いし。

「itojunのお墓でGoogle mapで検索すると出る」

確かに出るんですが、そこについても、外人墓地の怪しいお花見している人たちしかいない... いや、itojun のお墓参りも、まぁ、怪しいお花見みたいなものなんですが...

Mapion の地図リンクも送ってもらったんですが、Goole mapと同じ場所っぽい。こいつら全然駄目だな。

で、「墓地の区画の番号」を聞くわけですが、ロの9ですか? 霊園の地図にないんですが... ロの8の次は10だぞ。そこで歌代さんからのMessageで、

霊園事務所を渋谷側へ

え、そっち? で、霊園の墓地の地図を見直すと、端っこにロの5,7,9 が。そこかぁ。そこでようやっと到着できました。

霊園事務所では人名入りの地図があって、そこで聞いても良かったようです。まぁ、迷っていたのは僕だけじゃなかったみたいだし。

桜は三分咲きかな。これぐらいが良いという話も。満開は人がたくさんだし。

お酒もおいしかったです。

母とIngress

いや、まぁ、母はIngressはしないわけですが...

朝、起きて、お散歩。
お昼の後に、お散歩。
夕食前に、お散歩。

らしいです。おかげで、要町から椎名町、立教までを制圧できてうれしいです。一回、35位に入りました。

一人で出ると、いろいろ怪しい買い物をしてしまうらしい。ジャンクなものが家にたくさん... 今川焼きとか、苺とか、大福とか...

まぁ、元気で出歩けるうちに自由にお散歩してください。

しばらく東京です

今回は特に何があるわけでもないので、のんびりしているはずです。少し、Ingress Mission でもやりたいところ。

呼び出されなければ4/7まで東京の予定。

思ったより寒くなかったが、夜は寒いのかな?

飲み会などは適当に呼び出してください。

カレーパーティ準備中

12月にやったばっかりですが... 年二回目標です。

今年は11時に学生4人に来てもらって。わりと順調です。やっぱり経験値上がってるからな。いや、学生が優秀だからか。

Google Spread Sheet に、材料とかスケジュールとかがまとめてあるんですが、

　　やっぱり、どんどん大きくなっていく

まぁ、記録ないよりは良いんだけど... レシピはあるんだけど、5倍量とかだと、比率も変わるので。

表を作るなら、Schema も作るべきで、コメントとかを表に入れてはいけないんだろうな。複数の表が同じコラムで制御されてしまうのも残念な感じ。

僕は、HTML直書き(あるいはTeX)で表を作るのが好きだけど、HTMLのは、ちょっと見づらいかな。

あなたの人生の物語

テッドチャンですね。なんか映画化されて「メッセージ」というタイトルで5月に公開されるそうです。

なのだが、

　　　　どんな話だったっけ?

さっぱり思い出せないです。なので、本棚から引っ張り出すわけですが、奥様に聞くと「それはこの段の奥」で、そこにある。どうも、ちゃんと著者名順に並べているらしい。えらい。

だいたい読んだ本は、ネットに書くのだけど、blog にない。そうか、ネットニュースの時代に読んだんだな。それを見てみる限り、非因果的な言語ってのは面白いけど使いこなせてないみたいなことしか書いてない。

で、読み直す気になったんですが、短篇なので瞬時に読めるんですが、

やってきた宇宙人とテレビ経由で話すだけの超地味な話

でした。こんなの良く映画化する気になったな。

しかも、そこで使っている手法って、スペイン人が最初にアメリカで現地人に会った時に使うような感じで..

まぁ、地球人は電波とかで自分たちの言語や情報を垂れ流しまくっているので、向こうは全部わかってるってのがありそうな感じ。

今だったら、とりあえず、DNNに流して見るくらいはするんじゃないかな。問題は「何を」だったりしますが。DNNは何を理解したかは教えてくれないし。でも、どこを見ればよいかぐらいは見つけくれるんじゃなかろうか。

まぁ、宇宙船でやってきてテレビ電話で通信するあたりで、人類との共通点はたくさんあるのでコミュニケーションに問題がでるとは考えづらいが...

もっとも、自分の赤ん坊でさえ何を要求しているのかわからなかったりするし、犬や猫とのコミュニケーションもできてないからなぁ。

昔のテレビの電波だったら解読は容易だろうけど、今のデジタル方式のはどうだろう? まして暗号化されていたら。

解読されやすくするコードとかの話も70年代に「宇宙と交信する」とかが流行っていた時にあったな。それも、向こうが交信する気があればの話だけど。

そんなわけでメッセージがどんなできたかは楽しみです。

http://www.ie.u-ryukyu.ac.jp/~kono/sf/194.html

Agda の圏論の証明

まぁ、やってるのが圏論だってのが特殊ではあるんですけどね。

　極めてパズル的

帰納法とかほとんど出てこない。なので、

　証明の穴に適当に推論を当てはめる

ということになりがち。そして、それで、結構通る。それで終わってしまうのが普通。

もともと圏論が General Abstract Nonsense だからってのもあるんだろうけど。

Monad も面白いんですが、一生懸命証明したものが、

　メタ計算も関数の結合法則に従う

というだけだと、ちょっとさびしいんじゃないかなぁ。

でも、一方で、

　プログラムはちゃんと型的に穴が埋まっていれば動くんじゃないの?

とも思います。

数学や物理の理論を理解するには、数式や論理式の裏にある

　モデル

を理解することだと思う。圏論はモデルと論理式が一体になっている特殊な例なのかな。

　視覚化できるモデルとかたいしたことない

とも思うのですが、視覚化には「気づき」みたいなところがあるからな。

久しぶりにAgda

なんか、沖縄とっても寒い〜

学生の方が一段落したので、いつものように Agda いじってるんですが。今回のお題は否定。有限の射を持つ圏、つまり、たんなるグラフがうまくできなくて、

＊　存在しない射に対する結合則とかは、矛盾⊥ から導くのが良いんじゃないか?

ってことで、否定について調べてたんですが、

　 Nope : (m n : ℕ) → Set
　 Nope (suc _) zero = ⊥
　 Nope _ _ = ⊤

　 nope : ∀ m n → m ≡ n → Nope m n
　 nope zero ._ refl = _
　 nope (suc m) ._ refl = _

　 peano : ∀ n → suc n ≡ zero → ⊥
　 peano _ p = nope _ _ p

　 http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda

とかあって、結構面白い。

なんですが、

　 even : ℕ -> Set
　 even zero = ⊤
　 even (suc zero) = ⊥
　 even (suc (suc n)) = even n

　 div : (n : ℕ) -> even n -> ℕ
　 div zero p = zero
　 div (suc (suc n)) p = suc (div n p)
　 div (suc zero) ()

とかいうのもあって。()ってなんだ?

　 ¬_ : Set → Set
　 ¬ A = A → ⊥

　 data Dec (P : Set) : Set where
　 yes : P → Dec P
　 no : ¬ P → Dec P

　 EvenDecidable : Set
　 EvenDecidable = ∀ n → Dec (even n)

　 isEven : EvenDecidable
　 isEven zero = yes _
　 isEven (suc zero) = no (λ ())
　 isEven (suc (suc n)) = isEven n

　 http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type

とかやるらしく。起き得ない入力の組合せみたいなものらしい。Agdaが、これは起きないと理解してくれれば使えるらしいです。

つまり、A x B x C -> D みたいな関数で、A/B/Cのすべての入力について関数を定義する必要はないらしい。そういえば、data で規定された範囲しかみたいなみたいなことはやっていたな。どうせ、矛盾を取れる部分は規定された範囲外なんだから、実は除外できるんじゃないか?

今までは存在しない部分は Maybe で nothing とかやっていたんですが、それがいけなかったかも。で、演算定義とか結合則とから、いろいろ抜いていくと、

あれ? なんかできるじゃん

どうも、Maybe とかで record の中に入れ込んだので、Agdaが理解してくれなかったっぽい。

というわけで、要素2の圏を記述はきれいになりました。

なのだが、その後の Limit から Equalizer の証明には、はまりました。でも、定義を二重に入れてしまって、それの同一性が取れなかっただけで、定義を一部外に出したらできた。

　 http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/fd79b6d9f350/discrete.agda

結構、苦労していたのができて、ちょっとうれしいです。

　 http://seeker-s-eye.blogspot.jp/2017/01/agda.html

iTunes match vs Google play music

そういえば、ちょうど11ケ月前に、 iTunes Match 試してみたんですが... そしてほぼ放置だったんですが... Matchの状況を iTunes から見れるらしい。

errorになってるのも多いんですが、CDは結構match、沖縄民謡は全滅、なみろむも全滅、なんですが、

＊　LPから取ったのが、ちらほらmatchしてる
＊　スカパーからエアチェックしたものも
＊　なんとモノラル音源にもmatchすることがある

ふーん。そして、MatchしたのをAACで取り出すには、

＊　他のデバイスから読む
＊　一度、消してダウンロード

するらしいです。ううう、めんどくさい。部分的にmatchしたのを読み込んじゃうと、そこだけ浮いてしまうらしい。ううう、めんどくさい。また、AppleScript 書くのか?

自分で取り込んだものは明示的に「iCloud Libarayにupload」してやると iPhone にも反映されるらしい。


なんですが、クラウドに上げるだけなら、Google play music が無料だという説が... また、Google? まぁ、使うだけ使うか。いや、iTunes Matchが生きている間はそれでいいか?

Apple Music とか Google play music の聴き放題の方はあんまり合わないかな。つうか、スカパー使っているので重なってるんだよな。

11ケ月まえのはこれか。

http://seeker-s-eye.blogspot.jp/2016/03/itunes-match-and-apple-music.html

久しぶりにWindows 7 を使ってみたら

なんか、update とかどうとかで。一度、しくって、VMware Fusionのsnapshotで戻してダメで、また、現在のに戻ってとかやったら、

＊　Mac OS X の方が虹色アイコン状態に...

で、そこから Safe であげて、また、もう一度 reboot して... それで、ようやっと Windows が上がったようです。

大変お疲れ様でした。やりたいことは、問題なくできました。いや、結構、紆余曲折したが。

で、まぁ、あのtweetにつながるわけだな。

A&W

最近の学生は酒飲まない。沖縄だと移動が車なのもあるらしいです。バスで行けバスで。なので、

＊　たまにある打ち上げは、A&W で

学生は自分の好きなコンボを頼んで。それに、チャビイチキンとカーリーフライを足す方向で。

まぁ、酒癖悪い学生もいるからなぁ。

A&W安いとか言ってた学生もいたが、そこそこ良い値段だと思うけど。居酒屋で飲むのと、それほど変わらない。でも、ルートビール飲み放題だしな。

シュガーレスルートビア出ないかな。

虐殺器官と温泉

この間、読み終わった虐殺器官ですが、アニメも見てきました。学生と一緒に。

サザンプレックスだったんだけど、

＊　壁のポスターとか、せめて塗りなおして欲しいです。ぼろぼろです。

そして、金曜日11時からだろうけど、

＊　がらがら

でした。

感想としては「小説とまったく同じ」。小説読みながら、なんとなくイメージはするんですが、

＊　それよりイケメン過ぎる

のを除けば、まあ、まったく同じ。出てくるガジェットも。同じので良いとは思うけど、なんか小説を越える部分が欲しかったかも。

もう少しスプラッタかなと思ったが、割とマイルドに作られてたかな。いや、アニメにしては頑張っていたか。

その後、学生と一緒に宜野湾の温泉に。結構、寒かったので温泉良かったです。

C#

今年は Jungle DBをC#に移植すると言うのをやってもらったんですが、

＊　　構成管理ツールは?

でググるんですが、出てきたのが rake と cmake。要するに、Visual studioかXamarin かってことらしい。いや、まぁ、ちゃんと、deployとtestができれば文句はないわけですが...

まぁねぇ。EclipseもInteliJも、その上で動かすのは簡単なんだけど、

＊　それ、サーバー上でもbuildできるの?

という問題が。jarなりなんなりで deploy できれば良いじゃんとは思うんだけど。いや、

＊　採点の都合

もあるな。いちいち、IDE立ち上げないとだめなわけ?

Javaの時代遅れさ加減にはうんざりですが、C#が先進的かというと、それほど差はないかなぁ。ただ、IDEを離れた構成管理だと Java の方が選択肢が広いかな。いや、

＊　IDEを離れた構成管理自体が時代遅れ

という主張もあるとは思うんだけど、じゃぁ、Jenkins どうするんだよ...

C#で .dll を作るのは良いんだけど、MONO_PATH とかで管理するのも残念な感じ。いろいろググってみると。。

＊ Global Assembly Cache (GAC)

おぉ、これはいったい。Globalて世界中全部? ちょっと、その辺りで挫折中です。

まあ、一応、rake で実行はできたかな。テストは nunit らしいんだが、その辺りも謎です。

cmake の方はうまく動きませんでした。

いろいろ楽しめそうだな。C#