Thursday, 17 August 2017

母との日々

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

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

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

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

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

Saturday, 12 August 2017

東京のIngress

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

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

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

  夏の大三角

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

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

Thursday, 10 August 2017

東京は暑い

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

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

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

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

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

Monday, 7 August 2017

免許更新

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

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

なんだが、

  病気で気を失いましたか

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

だが、

  日付が読めない

とか言う文句が。

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

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

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

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

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

Saturday, 5 August 2017

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を作っても良いんだけど。

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

Thursday, 3 August 2017

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/

Wednesday, 2 August 2017

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 の相性の悪さと戦うよりは良いかも。

Monday, 31 July 2017

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 も作れるのか。えらいな。

Sunday, 30 July 2017

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置いても問題なくなると予想します。

Friday, 28 July 2017

着替え

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

  汗びっしょり

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

  パンツだけない

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

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

Thursday, 27 July 2017

GoodWill でお買い物

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

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

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

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

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

Monday, 24 July 2017

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に残すので僕は良いかな。

Saturday, 22 July 2017

iTunes Match

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

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

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

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

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

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

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

Friday, 21 July 2017

辞書

昔々、電子ブックという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 経由で使っていたらしいけど、さすがに、それは使わないな。動かそうと思えば動くのだろうけど。そこまでやるならググるよな。普通。

Thursday, 20 July 2017

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/

Wednesday, 19 July 2017

パイオニア AV アンプ

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

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

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

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

アンプの電源リセット

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

Sunday, 16 July 2017

 スカパーのアンテナ

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

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

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

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

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

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

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

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

Saturday, 15 July 2017

琉大 Open Campsu

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

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

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

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

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

Thursday, 13 July 2017

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 は、まだ足りない記号がかなりあるらしい...

Monday, 10 July 2017

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を調整するオプションが付いてる

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

Sunday, 9 July 2017

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 設定の話なはずです。

Friday, 7 July 2017

MBPの付属品

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

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

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

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

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

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

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

Thursday, 6 July 2017

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を保存するから明らか」と書いてあって、結局、仮定だったのか。証明できそう韃靼はなんだったんだ。

ここまで来ると、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

Friday, 30 June 2017

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を使っているっぽいな。なんだよ。

Wednesday, 28 June 2017

新しい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 も、もっと積極的に使って良いのかも知れんが、あんまり、気が進まなくてなぁ。

Monday, 26 June 2017

フードフリー 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自体が結構落ちているってことだろうな。

Tuesday, 20 June 2017

土砂降り

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

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

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

Sunday, 18 June 2017

小澤の不確定性原理

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

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

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

*  出口弘
*  小澤正直

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

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

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

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

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

Saturday, 17 June 2017

OSC Okinawa 2017

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

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

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

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

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

add_target ( target_name source1.c source2.c )

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

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

Friday, 16 June 2017

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のセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。

Tuesday, 13 June 2017

Prolog とシーケント代数

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

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

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

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

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


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

これだけだものな。

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

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

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

Sunday, 11 June 2017

メッセージ

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

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

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

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

Friday, 9 June 2017

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 を試してみるべきだな。

Thursday, 8 June 2017

新しい 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 でチェックみたいな感じ。

Friday, 2 June 2017

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

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

Monday, 29 May 2017

中部商業の歩道

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

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

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

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

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

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

Sunday, 28 May 2017

読み会最終日

学校に来てみると、なんかホワイトボードに多層パーセプトロンの図が。なので、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 に絞った方が良かったかも。

Saturday, 27 May 2017

ソースコード読み会初日

最初は 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の配列切ってるわけね。

というわけで、初日は、まぁ、準備できたかな〜 ぐらいです。

明日は、ハリーズのカレー食べながらって話になるはずです。

Tuesday, 23 May 2017

今週末はソースコード読み会

なんですが、どうも、何を読むかで盛り上がらず。いや、自分が盛り上がってないだけかも。

オープンソースなマインクラフト

これは C++ らしい。割と普通な感じ。Unity のを読みたい気もするが、なんか、あんまり良いものが見つからず。

Chainer

前回は Tensor Flow 読んだんですが、安直に作ったタスクマネージャー的な側面が強くて、GPU載っけたマシンで読むしかないのだが、あまり綺麗に読めないみたいです。

X.v6

また、これかぁ。悪くはないんだが、少し時代遅れかなぁ。

TOPPERS の組込みOSというのも見てみたのですが、うーむという感じ。

というわけで迷走中です。

Sunday, 21 May 2017

Ingress Event

先週は恩納村に三日続けていく羽目になっていたわけですが(風邪ひきなのにも関わらず)、IngressのEventも並行して走ってました。

ま、風邪ひきななので控えめに参加してました。Builderもローソンも、そこそこ貢献できたみたいです。3113は恩納村送りにも関わらずギリギリ取れました。

他の人がイベントに集中していたせいで、いつものご近所IngressのCFが多めに取れてちょっとうれしい。

風邪ですか? だるだるですが、少しずつ咳も収まってきてるようです。

Friday, 19 May 2017

風邪ひいた

いつもの定期便らしく... 土日に既におかしかったんですが... ひっくり返せない予定が、あったので、結局、こじらせてしまいました。

恩納村三連チャンは、ちょっと無理だったか。

まぁ、週末休めばなんとかなるかってところです。

Wednesday, 17 May 2017

OS研究会


毎年の研究会ですが、今年も恩納村ホテルモントレーです。いや、やっぱり同じ場所は楽。その方がホテルとの交渉もスムーズだし。去年は懇親会でお酒を出せないみたいな失態があったのですが、今年は配慮してもらえたので普通の飲み放題な懇親会になりました。

沖縄に赴任した直後から新城先生を引き継ぐ形でホテルムーンビーチで開催していたんですが、その後はいろんな場所を転々と。那覇市内は便利なんですが、リゾートホテルが沖縄っぽいかな。

来年も同じ場所でできると自分的はぐっと楽です。その方針で行こう。

研究発表も今年は割と面白い。VMで動かすならプロセス要らないじゃんということでLKMとしてアプリケーションを動かすと速いとか、信頼できないハイパーバイザー上でセキュアにVMを管理するとか、QEMUの命令エミュレーションのバグを回避するとか。

Wednesday, 10 May 2017

Applicative

Haskell のApplicativeってのを去年はいろいろやっていたらしいです。で、にこやかにソフトウェア工学の授業で、Haskell やるんですが、

Functorってのは、fmap で

ふんふん。自分で書いたものだから自分では良くわかる。

のだが、あれ、続きがあるぞ? Applicative だし。あれ、その続きも。これ、どこまで続くの? おっと、Monad までいくのか。それはやりすぎだろ(→去年の自分)

去年の授業の時に、それなりに行き詰まって、で、書きなおしたんだよな。その時に勢い余ったんだろうなぁ。

途中に、理解を助ける課題を入れればいいんじゃないかな。というわけで、突っ走ったのを修正する必要があるなぁ。

fmap とか <*> とかって、型さえ合ってれば、いろんな実装ができるんだけど、実は満たすべき性質がいくつかある。それが実装を制約するわけなんですが、その制約は圏論から来るから、いまいちピンと来ないんだよな。

授業のページも版管理しないとだめなんだよな。そういえば、生成scriptにバグがあって参照ファイルの存在をうまく検出できないっていうのがあった。

猫の投薬は、だいぶうまくなりました。

Sunday, 7 May 2017

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研究会があるか。

Saturday, 6 May 2017

猫のお薬

まぁ、うちのくそジジイな猫もお年だからなぁ。血管拡張剤的な薬らしいんですが、小さい錠剤です。これを飲ませるのが今回のお留守番ミッションらしい。

膝の上に仰向けに抱え込んで、顔を押さえて、口を開けさせたら、奥に落とし込めば良いらしい。のだが、

  ペッと吐き出す

こ、こいつ〜 しばらく格闘していたら、フーッ! とかいう。その時に口を大きく開けてくれるので、ばっちりでした。しばらく上向きに押さえてれば、吐き出せないらしい。でしたが、

ああ、なんか股間から放物線が...

ぐ、おしっこもらすほど怖い思いさせたか、ごめんな。

なんか仰向けに押さえるのが良くないらしく、座らせて、顔を押さえて「フーッ!」を待ったら、楽勝でした。

あとで水飲ませると良いらしいんだが...

Sunday, 30 April 2017

Ingress Operation

といっても青の作戦だからな〜

国際通り周辺を青くする

って、それだけですか? もちろん、それだけであるはずもなく、

昼飲みは控えるように

という指令が... そして、そんなものが守られるはずもないのが青なので...

国際通りをしばらく歩くだけで、がんがんX8が補給できる、そんなことになってました。

GWの肉なイベントとかビールなイベントとかも楽しかったです。

青くすること自体は、みんなでばらばらに、残っている緑を掃討するみたいな地味〜な作業なんだよな。

まぁ、この青の作戦のぬるさが青っぽいと思うし、それも良いと思うこの頃です。

Saturday, 22 April 2017

プログラミングIII

っていう3年次の授業なんですが、

なんか作る

ってなものです。なんですが、

なんか、ちょっと違う

とかいう理由で、最初にいた学生たちがいなくなる。もしかすると、今年は受講者ゼロかも。

3年次にはEnPitもあって、そっちも「なんかプロジェクトやる」ってなものなので重なってるんだよな。そっちの方が「ちゃんとしてる」かも。

どんなものを作るにしても、今はネットと繋げないのはありえないから、Web Serviceの構築はやってねみたいな感じでやっていたんですが、それが嫌われたか? Web Serviceの構築でも Web Framework やら、git やら、ansible やら、Jenkins やらでやること多いからな。まぁ、OSの授業で全部やってもらってるんですが。

で、何やりたいのと聞くと機械学習と答える学生が多いです。流行だからな〜 いいよ、好きなこと、どんどんやれ〜 うちの学科は昔から人工知能の先生がいるので、得意な分野のはずです。

Monday, 17 April 2017

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 とかは、もっとすごいんだろうな。頭の良い人たちはすごいよ...

Sunday, 16 April 2017

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 三枚分とか誤差だな。

Saturday, 15 April 2017

家のネットワーク

うちから海炎祭の花火を見物している時に、void が「iPhoneから音楽流したい」というので、いつものAirMac に繋がっているアナログアンプでも良かったんですが、

そういえば、パイオニアのAVアンプが使えるんじゃないか?

と思って。SC-LX87 の取説を見ると、WifiはないがLANはあるらしい。で、ケーブルと持ってきてハブにつなげて、いろいろやるんだが、

ぜんぜんつながらん

DHCP取らないし。まぁ、その時は諦めたんですが...

今日、外からBDレコーダーに(Sonyのアプリ経由で)つなげようとするとつながらない。あれ? で、BDレコーダ側を見ると、やっぱりDHCP取れてないじゃん。

結局、ハブとルータをつなげるケーブルがいかれてた。なので、ハブに繋がってるもの同士では通信できるので気がつかなかったんだよな。

それで、AVアンプもLANにつながって、iPhoneからルータ経由で鳴らすことができたみたいです。

たぶん、ケーブルが急にだめになったわけではなくて、バッファローのGigabitなハブとの相性なんだろうな。今時のは自動的にクロスかどうかを判定するのだけど、それがうまくいってないとか、そんなのでしょう。

しかし、うちにはEthernetケーブル何本あるんだ? そして、そのうち生きてるのはどれ? この前、GBit 用にケーブル買ってきたはずなんだが... 機材が増えるのに追いついてない感じだな。

Sunday, 2 April 2017

itojun の墓参り

これも10年かぁ。青山霊園。たまにしかお墓参りしないので、

場所がわからない

なんとかなると思ったのだが、けっこう広いし。

「itojunのお墓でGoogle mapで検索すると出る」

確かに出るんですが、そこについても、外人墓地の怪しいお花見している人たちしかいない... いや、itojun のお墓参りも、まぁ、怪しいお花見みたいなものなんですが...

Mapion の地図リンクも送ってもらったんですが、Goole mapと同じ場所っぽい。こいつら全然駄目だな。

で、「墓地の区画の番号」を聞くわけですが、ロの9ですか? 霊園の地図にないんですが... ロの8の次は10だぞ。そこで歌代さんからのMessageで、

霊園事務所を渋谷側へ

え、そっち? で、霊園の墓地の地図を見直すと、端っこにロの5,7,9 が。そこかぁ。そこでようやっと到着できました。

霊園事務所では人名入りの地図があって、そこで聞いても良かったようです。まぁ、迷っていたのは僕だけじゃなかったみたいだし。

桜は三分咲きかな。これぐらいが良いという話も。満開は人がたくさんだし。

お酒もおいしかったです。

Wednesday, 29 March 2017

母とIngress

いや、まぁ、母はIngressはしないわけですが...

朝、起きて、お散歩。
お昼の後に、お散歩。
夕食前に、お散歩。

らしいです。おかげで、要町から椎名町、立教までを制圧できてうれしいです。一回、35位に入りました。

一人で出ると、いろいろ怪しい買い物をしてしまうらしい。ジャンクなものが家にたくさん... 今川焼きとか、苺とか、大福とか...

まぁ、元気で出歩けるうちに自由にお散歩してください。

Thursday, 23 March 2017

しばらく東京です

今回は特に何があるわけでもないので、のんびりしているはずです。少し、Ingress Mission でもやりたいところ。

呼び出されなければ4/7まで東京の予定。

思ったより寒くなかったが、夜は寒いのかな?

飲み会などは適当に呼び出してください。

Saturday, 18 March 2017

カレーパーティ準備中

12月にやったばっかりですが... 年二回目標です。

今年は11時に学生4人に来てもらって。わりと順調です。やっぱり経験値上がってるからな。いや、学生が優秀だからか。

Google Spread Sheet に、材料とかスケジュールとかがまとめてあるんですが、

  やっぱり、どんどん大きくなっていく

まぁ、記録ないよりは良いんだけど... レシピはあるんだけど、5倍量とかだと、比率も変わるので。

表を作るなら、Schema も作るべきで、コメントとかを表に入れてはいけないんだろうな。複数の表が同じコラムで制御されてしまうのも残念な感じ。

僕は、HTML直書き(あるいはTeX)で表を作るのが好きだけど、HTMLのは、ちょっと見づらいかな。

Monday, 13 March 2017

あなたの人生の物語

テッドチャンですね。なんか映画化されて「メッセージ」というタイトルで5月に公開されるそうです。

なのだが、

    どんな話だったっけ?

さっぱり思い出せないです。なので、本棚から引っ張り出すわけですが、奥様に聞くと「それはこの段の奥」で、そこにある。どうも、ちゃんと著者名順に並べているらしい。えらい。

だいたい読んだ本は、ネットに書くのだけど、blog にない。そうか、ネットニュースの時代に読んだんだな。それを見てみる限り、非因果的な言語ってのは面白いけど使いこなせてないみたいなことしか書いてない。

で、読み直す気になったんですが、短篇なので瞬時に読めるんですが、

やってきた宇宙人とテレビ経由で話すだけの超地味な話

でした。こんなの良く映画化する気になったな。

しかも、そこで使っている手法って、スペイン人が最初にアメリカで現地人に会った時に使うような感じで..

まぁ、地球人は電波とかで自分たちの言語や情報を垂れ流しまくっているので、向こうは全部わかってるってのがありそうな感じ。

今だったら、とりあえず、DNNに流して見るくらいはするんじゃないかな。問題は「何を」だったりしますが。DNNは何を理解したかは教えてくれないし。でも、どこを見ればよいかぐらいは見つけくれるんじゃなかろうか。

まぁ、宇宙船でやってきてテレビ電話で通信するあたりで、人類との共通点はたくさんあるのでコミュニケーションに問題がでるとは考えづらいが...

もっとも、自分の赤ん坊でさえ何を要求しているのかわからなかったりするし、犬や猫とのコミュニケーションもできてないからなぁ。

昔のテレビの電波だったら解読は容易だろうけど、今のデジタル方式のはどうだろう? まして暗号化されていたら。

解読されやすくするコードとかの話も70年代に「宇宙と交信する」とかが流行っていた時にあったな。それも、向こうが交信する気があればの話だけど。

そんなわけでメッセージがどんなできたかは楽しみです。

http://www.ie.u-ryukyu.ac.jp/~kono/sf/194.html

Friday, 3 March 2017

Agda の圏論の証明

まぁ、やってるのが圏論だってのが特殊ではあるんですけどね。

 極めてパズル的

帰納法とかほとんど出てこない。なので、

 証明の穴に適当に推論を当てはめる

ということになりがち。そして、それで、結構通る。それで終わってしまうのが普通。

もともと圏論が General Abstract Nonsense だからってのもあるんだろうけど。

Monad も面白いんですが、一生懸命証明したものが、

 メタ計算も関数の結合法則に従う

というだけだと、ちょっとさびしいんじゃないかなぁ。

でも、一方で、

 プログラムはちゃんと型的に穴が埋まっていれば動くんじゃないの?

とも思います。

数学や物理の理論を理解するには、数式や論理式の裏にある

 モデル

を理解することだと思う。圏論はモデルと論理式が一体になっている特殊な例なのかな。

 視覚化できるモデルとかたいしたことない

とも思うのですが、視覚化には「気づき」みたいなところがあるからな。

Thursday, 2 March 2017

久しぶりに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

Monday, 27 February 2017

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

Sunday, 26 February 2017

久しぶりにWindows 7 を使ってみたら

なんか、update とかどうとかで。一度、しくって、VMware Fusionのsnapshotで戻してダメで、また、現在のに戻ってとかやったら、

* Mac OS X の方が虹色アイコン状態に...

で、そこから Safe であげて、また、もう一度 reboot して... それで、ようやっと Windows が上がったようです。

大変お疲れ様でした。やりたいことは、問題なくできました。いや、結構、紆余曲折したが。

で、まぁ、あのtweetにつながるわけだな。

Saturday, 25 February 2017

A&W


最近の学生は酒飲まない。沖縄だと移動が車なのもあるらしいです。バスで行けバスで。なので、

* たまにある打ち上げは、A&W で

学生は自分の好きなコンボを頼んで。それに、チャビイチキンとカーリーフライを足す方向で。

まぁ、酒癖悪い学生もいるからなぁ。

A&W安いとか言ってた学生もいたが、そこそこ良い値段だと思うけど。居酒屋で飲むのと、それほど変わらない。でも、ルートビール飲み放題だしな。

シュガーレスルートビア出ないかな。

Friday, 24 February 2017

虐殺器官と温泉

この間、読み終わった虐殺器官ですが、アニメも見てきました。学生と一緒に。

サザンプレックスだったんだけど、

* 壁のポスターとか、せめて塗りなおして欲しいです。ぼろぼろです。

そして、金曜日11時からだろうけど、

* がらがら

でした。

感想としては「小説とまったく同じ」。小説読みながら、なんとなくイメージはするんですが、

* それよりイケメン過ぎる

のを除けば、まあ、まったく同じ。出てくるガジェットも。同じので良いとは思うけど、なんか小説を越える部分が欲しかったかも。

もう少しスプラッタかなと思ったが、割とマイルドに作られてたかな。いや、アニメにしては頑張っていたか。

その後、学生と一緒に宜野湾の温泉に。結構、寒かったので温泉良かったです。

Thursday, 23 February 2017

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#

Wednesday, 22 February 2017

採点終了

去年は結構落としまくったのと、今年の学生が真面目だったのとで、例年よりも量は多かったんですが、

* 真面目に採点したので、割と追いついていた

みたい。

今年はタネンバウムの教科書を使ったんですが、課題の難易度のばらつきが大きい。でも、

* プログラム書けとか書いてあってもたいしたことないんだからやれよ

とは思うわけですが、一方で、device independent とは何かとかいう問題があったり。少し多めに出して選択して、易しいのはこちらで却下するのがいいかな。

教科書の問題は「英語の問いを写して、それに日本語なり英語なりで解答しろ」と言ってるんですが、

* どうしても訳を付けてるのが...

まぁ、今のGoogle翻訳は昔よりはかなりまともなんだけど、それでも、やっぱり邪魔。それに、

* 大学生が英語を訳して読むのか? 英語で読めよ!

同じものを二度読まされるのが苦痛なのと、英語と日本語の考えの差があるのと...

この辺、ちゃんと英語で理解しているかどうかを入試でテストすることはできないのかな? 英語の綴りの怪しいプログラミングは結構厳しいので、基本単語ぐらいはクリアしていて欲しいのだが...

Friday, 17 February 2017

学生インタビュー

卒論修論の審査関係はほとんど終わって、あとは修士のポスター発表かな。その前にあるのが、学生インタビュー。

導入されたのは去年からかな。学生が大学の教育をどう思っているかを聞き出すわけですが、まぁ、難しいかな。

* 先生ではなくて第三者がインタビューする方が良いんじゃないか?

それでもアンケートよりは、こっちの聞きたいことを直接聞けるのが良いです。学生が統計の授業の一貫として行う授業アンケートもあるんですが、項目をこちらでコントロールできなくて、聞きたいことが聞けない。単にレベルの高い授業を難しいとか言っているだけのアンケートとか参考にはならないし、そんなのをまともに扱っていたら、どんどんん授業のレベルが下がってしまう... まぁ、落ちこぼれている学生は結構いるんですが...

去年聞いたのと同じような答えが返ってくるのは、やっぱり、情報を引き出せてない感じかなぁ。この手のインタビューの専門家とかいないのかな。もっとも、卒論と修論で80人ぐらいいるので結構大変なんですが。

学生には大学で自信をつけて卒業していって欲しいが、自己評価の低い学生が結構。それは大学教育が失敗しているということなので、教える側の問題点なんだよな。でも、それはゆとりっぽいかなとも思います。そのゆとり世代も今年が最後か?

Thursday, 16 February 2017

卒研発表終わり〜

昔は、学生の徹夜に付き合ったりしましたが、今はそんなことはなく。

でも、今年はちょっと疲れたかも〜 いや、昨日のプログラミングが一番疲れた気がする。学生といろいろプログラミングできて面白かったです。

いちごの研究をしている先生がいるので、今年もいちごを食べられました。沖縄でいちごを作るのは難しいらしい。

これで修士も卒論もかた付きましたが、イベント的には、まだ少しあるらしい。うちは割と遅い方ですね。

今年は、3月にもう一回カレーパーティ(3/19 Sun )する予定です〜

Wednesday, 15 February 2017

CUDA と pthread

別に普通に動くはずなんだよな。実際に簡単なプログラムも作って pthread と両立したし。

なんだけど、どうも、

pthread_create された側から cuInit(0) すると何もいわずに落ちる

という技が。なので、main thread と CUDA thread を入れ替えてみた。で、結果的には動いたんですが...

thread を入れ替えると、データの初期化順序が狂うので、待ち合わせを行う必要がある。もちろん、

semaphore 使うのが正当ですが...

面倒くさいので、大域変数の spin lock で... ってのが裏目に。良くあるパターンなんだけど。spin lock の位置によって、dead lock したり、データ壊れたり、どっちかが先に終わってしまったり...

まぁ、楽しい時間だったともいうかな。

thread localとかのコンパイラの問題かと思って、CUDA部分だけ clang 使ったんですが、それでもだめだった。まあ、良くわからん。C++ でなく C なのがいけないのか。

Tuesday, 14 February 2017

夜桜食事会

近所のコートドールの夜桜見物というイベントです。

https://tabelog.com/okinawa/A4703/A470404/47005320/

2/12までとか書いてあるけど、桜は5分咲きぐらいだったかな。まあ、ソメイヨシノではないし、夜桜は少し早いくらいの方が良いかも。

花見の日程設定は難しい。去年(2/16)は割とベストタイミングだったんですが...

http://seeker-s-eye.blogspot.jp/2016/02/blog-post_16.html

食事は鹿肉がメイン。チーズフォンデュとかもあって、とても美味しかったです。

毎年のイベントになるといいかな〜

Sunday, 12 February 2017

cmake の realclean

卒論修論が真っ最中ですが...

やっぱり cmake いじっていたり。普通とちょっと違うことしているので、rm -rf CMakeFiles とかしないと、うまく動かないことがあって... realclean ないのか? とググったんですが...

http://stackoverflow.com/questions/9680420/looking-for-a-cmake-clean-command-to-clear-up-cmake-output

とかを見ると、

out-of-source で使え

って書いてある。つまり、

hoge-source があったら、working direcotry から cmake hoge-source しろ

と。cmake . するなと。うん、LLVMとかGCCとかがそうなのは知ってました。つまり、dist-clean したれば、

rm -rf working-directory

しろと。なので、

add_custom_target(clean-all COMMAND rm -rf * )

しろと。ちょっと、待て。それは自殺行為だろ。でも、

  make rebuild_cache

というのがあるみたい。あ、欲しいのはそっちだな。きっと。

cmake 総じて見ると、悪くはないかな。Cuda も

find_package(CUDA REQUIRED)
cuda_add_executable(Cudasample_gpu Cudasample_gpu.cu)

とかで動くし。ま、もちろん、自分のプロジェクトでは、それは使えないわけなんですが...

Thursday, 9 February 2017

cmake

最近は cmake と格闘しているんですが、

add_executable(hoge hoge.c fuga.cc )

とかでできるのは良いのだが、そこから先何かしようとすると、結構、厳しい。

ソースコードを生成してからコンパイルするには、

add_custom_command

というのを使うんだけど、それを動的に生成しないといけないらしい。それには、macro が使えるんですが、かなりのクソです。

まぁ、世の中のマクロ処理系でクソでないものって存在しないんじゃないか説。Cのあれとか、Lispのあれとか、C++のあれとか、TeXのあれとか...

で、今度は CbC compiler と Cuda を両立させようとするわけですが...

cmake はそのもそも複数のcompilerを取り扱うようにできてない

らしい。external project でできるという説もあるらしいですが、どちらかのcompilerを add_custom_command するしかないみたい。その部分は闇になると。

まぁ、とりあえず、なんとかする方法はわかったので良いか...

Saturday, 4 February 2017

てだこウォーク2017


なんか、キャンプキンザーの設定が20km/42kmに。42Kmはなぁ。

と言いながら42km行ってきたんですが、全部歩きだと17時までに到着できない。まぁ、そうだよな。4km/hペースだと10時間だし。走れるところは走れば良いんだろうけど、そいうトレーニングしてないからな。

というわけで、帰りの宜野湾広栄あたりで戻ってきました。普段廻れない、Ingressのportalが取れたのが良かったです。

Wednesday, 1 February 2017

Java PathFinder

JavaのModel Checkerですね。thread の並行実行の可能な実行をすべて列挙してくれるという優れものです。aとbとcを表示する三つのthreadを実行すると、abcからcbaまで全部出ます。OSの課題です。

なんだが、

「せんせー、うごきません」

な学生が。直接僕に聞かずに先輩に聞けって言ってるだろ。なんだが、研究室には僕しかいない....

で、見てみると、

class JPF not found

あれ? jar の中に JPF ないし。ant が壊れてるのかな。ant buid はできてるので、.class はできてる。なので、

java -cp hoge -cp hoge1

で、どんどん足していくと、お、HelloWorld は動いた。が、RacerとかDiningPhilとかが native code Illeagal access とか言ってる。なんだこれ?

学生にOS聞いたら「El Capitan」と、最新使えと言ってるだろうが、というか、そのために自分のを最新にする羽目になってるのに...

で、自分の環境では、実は最後にbuildしたのは、2015だったので、作り直してみる。

動く

ぐ。なんだ? java とか ant のversionとか Java Pathfinderのversionでも合わせて見るが、問題なし。

で、自分のbuildを tar で固めて学科のserverにあげて落としてもらったら、動きました。

結局、

おま環

だったようです。何が原因かはなぞだが。build の時に壊れてるからな〜

OSの採点は珍しく順調です。怒ったり笑ったりしてます。

Tuesday, 31 January 2017

東大

沖縄にいろんな人が来てくれるのはうれしいことです。まぁ、

一緒に飲みに行くだけなんですが

最初の頃は、良く、首里城に行ったものだが、今は、そんなことはなく。

先週は、東大の焼きてびちを食べに行きました。栄町にあるおでんやさん。名前の由来はしりません。滅多に行きません。一度、呼ばれていったぐらい。

店が開くのが9時半。でも、9時から並んでいるので、その頃にはいかないと。でも、ついうっかり歩いて行ってしまって。

お店には入れたんですが、

「焼きてびちは1時間半かかります」

まぁ、いいか。で二人で菊の露一本取って、おでん盛り合わせで、ゆっくり待つ。

東大の焼きてびちって、他のところでは出ないんだよな。なんでだろ。

大を二人で楽勝で食べられることはわかりました。

(が菊の露のボトルを二人で空けたのは飲みすぎだった...)

Friday, 27 January 2017

虐殺器官

まだ、読んでませんでした。なんで10年も寝かしていたのか。いや、買ったのは2010年か。話題だったのでへそ曲がりで読んでなかっただけでしょう。

映画は2/3からですか。かろうじて間に合ったか。音楽だと予習した方が良くて、映画だと予習しない方が良いものだが...

面白かったな。でも結構ゆっくり読んだ。普通、一日で読むだろと思うんですが、最近はゆっくりが多い。入院中は結構読んだが。10日ぐらいで書かれた作品だそうですが、それをゆっくり読むのも良いか。

戦争は劇的に減って、テロは増えている、そんな今の時代のSFだな。文法自体にそれほど深入りしてないのは、物足りない気もしますが、その部分はSciFiな部分だから、それで良いのかな。Startrekのwarpみたいなものだ。

解説にあった参考文献は、ほとんど読んでないので、その辺りも読んでみるか... え、なに、デネット、ピンカー、ガザニガ、デイリー&ウィルソン?

Thursday, 26 January 2017

Okinawa Ingress Resistance Operation

もう先週の日曜日だったんですけどね。やっぱり、卒論だ何だかんだで何も手伝えなかったんですが...

「作戦のために宜野湾のポータル反転します」

あぁ、どうぞどうぞ。だったんですが...

ですが...

どうも、宜野湾の縦断するリンクを通してCFを作る作戦だった(のを後から知った..)。で、そここに、

拠点ポータルの反転緑ポータル

が... あだだだだ。そこ反転されると... というわけで、宜野湾は結構やられていたようです。

運悪く、作戦実行日と、active ENL (328とMarrey)の活動日が重なったらしく、結構な多重CFを作られてました。あららら。

今週前半は、その反転ポータルの処理をしていたみたいです。宜野湾RES、ご苦労様です。

作戦は半分成功みたいな感じだったみたい。宜野湾縦断は無理だったようですが。

こういう作戦があると、青も緑も刺激を受けるようで、いろいろ変化があって面白いです。

卒論生もいろいろやらかしてくれているがな!

Thursday, 19 January 2017

JavaFX Gantt Chart

なんか、そういうの学生に課題で出したんですが、自分でやってみようかなと。Java FXのexampleを見れば簡単なはずなんですが...

BarChart

というのはある。あるんだけど、Year は理解できるのだが、Series? どうも、Series に年毎のデータを入れると棒グラフにしてくれるらしい。

なんですが、もっと自由にデータを入れたいんだけど。しばらく、いじって、どうにもできそうにないので、ググったら、

  既に Bubble Chart から Gantt Chart を作った人がいた
http://stackoverflow.com/questions/27975898/gantt-chart-from-scratch

おお。それを使うか。なんですが、

cpu が逆順にならんでしまう

え、なんで。逆順にadd()すれば良いんだろうと思ったが、それでも順序は変わらない。

調べてみると、

XYChart.Series という FXCollections は ObservableListで、それは SortedList

え? 任意の順序にデータを入れられないのか。そういうモデルに制約を入れるようなことされちゃうと汎用性がなくなるんだけど。しかも、どのタイミングで sort されるのかがわからない。setData() しても、あとで順序を変えられてしまう... ひどい。

結局、Series に入れるデータの名前で sort されているみたいなので、それを適当に決めてやれば良いらしい。それと Y軸に表示されるラベルとは*関係ない*。え、そうなの。まぁ、いいか、表示できたから。

ssh://yomitan.ie.u-ryukyu.ac.jp//net/home/hg/teacher/kono/os/OSQueue

というわけで、Java FXの XYChart は割とクソでした。Tk だと、この辺は極めて自由で、表示したグラフをマウスで操作するとかも簡単なんですけどね。sort されてる状況だと任意に動かすのは無理だな。

あと、どうも、Java 1.2とかの時代って「とりあえずObject型で扱って、instanceOf で切り分ける」みたいなプログラミングだったのだけど、Java FXは、それを引き継いでるみたいだな。そういうのどうなの?

Tuesday, 17 January 2017

Photos.app

なんか、また、DB変えたのか... と思ったら、

Database/apdb/Library.apdb

ってのが、

database/photos.db

ってのに名前が変わっただけらしい。いや、なんか細かく変わっているみたい。編集を加えた場合の扱いとかくそだったからなぁ。でも、まぁ、いい少しぐらい間違っててもいいや。

これだけなら、まぁ、まだいいんだけど、

Photos.app を終了しても、sqlite3 の lock がかかったまま

え、なんだそれ。なんかの daemon が握っているのか。前はさすがに、app を終了すれば lock は外れていたんですが。

といっても、その .db 自体をコピーしてしまえば、sqlite3 で開けることはできるし、そうしていたので、あまり影響はないらしい。

検索したりするのは Google Photos にしてしまったので、Photos は local な保存用という感じですね。

いや、もちろん、iCloud の値段が劇的に下がるなら、iCloud base にしても良いんですが。

50 GB:¥130
200 GB:¥400
1 TB:¥1300
2 TB:¥2500

月額じゃなくて年額で、それなら考えても良いかな。

Monday, 16 January 2017

センター試験

なんか、いきなりマークシートを解いた問題から塗っていく人が大半。ということは、そういう指導がされているってことか。もっと見直せとは思いますけど。センター試験は満点を目指す試験だから...

国語は先祖返りみたいな古くさい問題。科学文明を論理もなく批判する大衆という一元的なとらえ方ってどうなのという文章。理系を目指している学生は読んでうんざりだったろうな。漢文にレ点を打たせるとか、まだやってるのか。漢詩は日本語的な文脈ではなくて、四声とか中国語の文法とかと一緒に教えるべきものなんじゃないのかなぁ。私小説的な随筆とか、ほんわか系の古文とかも、

大学に来る学生は論理的な文章の理解と作成ができて欲しい

という要求からはかけ離れていてがっかりでした。作家を目指しているわけじゃないんだからさぁ...

英語と数学は量は多いんだけど、ちょっと易しすぎるんじゃないかなあ。

ラノベレベルの英語ではなく大学の1年次は英語の教科書で勉強する準備ができている

とか、

因数分解とか三角関数の加法定理の技術ではなく、微積分と線形代数の重要性を理解している

とかではないのかな。 スキージャンプの分布図から情報を読み取る問題とかは良かった。

物理は、

静的な力の釣り合いばかりで、エネルギーや運動量保存が出てこない

それだと解析力学に繋がらないんですが... いやエネルギーの単位を問う問題とかあったな。なんだそれ。

というわけなので、とってもずれを感じました。まぁ、センター試験だから難しいのはダメってことなんだろうけど...

Wednesday, 11 January 2017

英語で授業

なんか、そんなのがあるらしくて。授業一コマだけですが、やってきました。まぁ、そもそも留学生向けの大学院の授業とかもあるので、大学院だと英語の授業は普通。でも、

日本人が日本人に英語で授業して面白いのか?

まぁ、なんか練習にはなるか。英語の質疑応答とかをもっと入れればよかったかも。

もっとも、自分の学部時代に歴史が嫌いな奴なのにユダヤ文学とか超つまらないのを読まされてつらかったので、そういうのよりは良いかも。ラバイがどうとかどうでもいいです...

学部時代から博士にいこうと思っていたし、博士論文は英語で書くものと思っていたので(実は東大でも日本語の工学博士論文はありだったのだが)、英語は結構勉強しました。

SFのペーパーバック。最初は短編集から。ルグィンとかは文学よリで難しすぎる。クラークとかハインラインとかアシモフとか。挫折したものも。ベアのQueen of Anglesだな。邦訳も読みましたが、まぁ、難しい。邦訳が出てないシリーズものとかを読めるのはうれしい。BaxterのManifold trilogyとか。

W.V.O.Quine の From a Logical Point of View 。吉田夏彦先生のところで読みました。論文集というかエッセイ集というかそんなもの。これ、邦訳もあるのだが、訳を読んでもさっぱりわからないというシロモノ。結構、苦労しながら読んだ記憶が。でも、卒業する頃にはするする読めるように。そんなものだよね。吉田先生に「なんだ、君たち、こんなものもわからないのか」と言われたのが記憶に残ってます。

DiracのQuantum Mechanics。これも邦訳があるんですが、訳を読んでもさっぱりわからない。まぁ、数式も結構面倒くさいんですが、最初の方は割とやさしい。朝永振一郎の方も読んだのですが、ディラックの方がアプリオリに確率ベースの力学を導入するので僕にはわかりやすかった。英語で読んだ方が良い本ですね。

Z80のマニュアル。ザイログシンタックスのアセンブラのマニュアルですね。これは繰り返し読んだな。やさしい英語。あとで邦訳も出た。そういえばCP/M 80のBIOSマニュアルとかも英語だった。CP/MはOSが何か知らない頃に読んだので「BIOS呼び出せばなんでもできるから、他のものはいらない」とか思っていた感じが。そういえば、BASICで他社のCP/Mのファイルを読むプログラムとか書いていたような。

大学院に行ったら、元岡田中研はCACM/JACM/BYTEが全部研究室の図書室にあるという素晴らしい研究室で、日々、図書室に埋もれてました。なんだが、先輩の博士課程の学生に渡されたのは、StandfordのD論。これらが読みやすくて面白かった。

他にも Database とか Mathematical logicとか、まあ、大学院時代は英語の輪読を良くやりました。学部時代は日本語の本の読書会を良くやってたな。

大学にマンナ先生が来た時に英語で質問したら、同期の学生が英語はなせるんですねと少し驚いたのが、むしろ驚き。

英語の先生に講義してもらうのが英語の勉強になるんじゃないか?

やっぱり使う機会がないと。英語の本に慣れないとね。

Sunday, 8 January 2017

プロシン2日目

自分たちの発表は朝一。Jungle DBの話だけど、まあ、あんまり伝わってない感じ。いろいろ反省。

発表で図がでないという技を出してました。

プロジェクタにHDMIがない
ノートPCを入れ替えてファイルを転送
HTMLスライドが参照している図が絶対パス
図が全滅

という流れだったようです。あらまあ。

新屋が前回の発表でも賞をもらったので良かったです。卒業生が活躍するのは素晴らしい。

結論としては、温泉はすばらしい。

Saturday, 7 January 2017

Raspbian on QEMU and fuse-ext2

実機でのLLVM compileはlinkがメモリを要求するので256MBでは無理ならしい。なので、QEMU上でメモリ増やしてやればよいんじゃないかと。

qemu 自体は brew install qemu で簡単。で、raspberrypi のkernelとboot imageを取ってくればよい。

そのあとは、結局、

http://www.linux-mitterteich.de/fileadmin/datafile/papers/2013/qemu_raspiemu_lug_18_sep_2013.pdf

これがわかりやすいみたい。initの代わりに sh を指定して、いくつかファイルを修正して boot と。

結論から言うと、だめでした。Emergeny shell mode まではいくが、systemd の load module でこけてしまう。

さらに、

raspbian のメモリ256MBは hard coded で変えられない
https://bugs.launchpad.net/ubuntu/+source/rootstock/+bug/570588

らしい。つまり、この方向で LLVM をコンパイルすることはできないらしいです。

なので、残った方法はcross compile だな。

上の方法を試す前に、fuse で boot image を OS X で mount するってのもやりました。brew で fuse-ext2 はないので、自分で作る必要があるのだが、結構、複雑。

http://apple.stackexchange.com/questions/226981/how-do-i-install-fuse-ext2-to-use-with-osxfuse

ここかな。結論的には、

CFLAGS="-idirafter/usr/local/Cellar/e2fsprogs/1.42.13/include -idirafter/usr/local/include/osxfuse/" LDFLAGS="-L/usr/local/lib -L/usr/local/Cellar/e2fsp rogs/1.42.13/lib" ./configure --sbindir=/usr/local/sbin\n

で config できるみたいです。

fuse-ext2 -o force boot.img /mnt

すれば良いのかと思うとそうはいかなくて、いちど boot.img を DiskUtility で開けます。そうすると、vfat な boot partition が開きます。partitoin 2は、

% diskutil list
/dev/disk2 (disk image):
#: TYPE NAME SIZE IDENTIFIER
0: FDisk_partition_scheme +4.4 GB disk2
1: Windows_FAT_32 boot 66.1 MB disk2s1
2: Linux 4.3 GB disk2s2

ここにあるので、

# fuse-ext2 -o force /dev/disk2s2 /mnt

で mount できます。これで書き換え可能になります。SD card でも可能なはず。

ここまで、できたので、これを cross compileの環境に使えるはずだな。

Friday, 6 January 2017

プロシン58

今年も伊東の同じ場所です。そういう方が幹事さんが楽。宿の方も助かるし。

踊り子号に乗るつもりだったんですが、新宿ではなく横浜乗り換えだったのに、間違えて池袋で埼京線に乗ってしまって新宿で降ろされてしまいました。そこで、湘南ライナーに乗り換えられるはずだったんですが、降ろされたのが大宮行きのホームで、湘南ライナーの乗り場を探しているうちに乗り過ごしました。なので、こだま号で行く羽目に。

踊り子号は自販機では買えないっぽくて、熱海でも踊り子号の指定券を買う方法が良くわからない。どうも改札の外に出るとか書いてあるが、まぁ、いいかで、結局、熱海から普通で。

伊東は結構青いな。ingress的に。

Thursday, 5 January 2017

母の洗濯

実家に帰ると洗濯は母がやってくれるわけですが、ありがたいことです。

室内に干すのだが、階段の上で割とやりやすいらしい。なのだが、

最近洗濯機の使い方が怪しいらしい

洗濯機の前で悩んでいるのは去年見かけたが... 洗濯物入れて、洗剤入れて、電源入れて、スタートを押すだけなのだが、いろいろ怪しい。洗剤を入れたまま放置されていたり、ボタンが良くわからないらしい。余計なボタンを隠すと良いかも。なので、廻しておくと干すのはやってくれるので良いようです。いろんなことができなくなってくるのは、つらいだろうとは思うけど、そのためのヘルパーさんなので、うまくやってもらえると良いと思います。

女の人は年取ってもいろいろやることがあって良いのかも。年末に、母の妹のお見舞いにいった時にも洗濯物をたたんでいる人がいたな。脳の機能の大半は手を制御するために使われているらしいので、手を動かすのは良いみたい。

古い着替えは若干カビているのがあるみたい。円形の脱色が。まあ、無害なんだけど。

Tuesday, 3 January 2017

初詣

母が熊野神社に行こうと言うので。風邪もだいぶ良くなったし、昼ご飯時だし、いいか。なんだけど、お母さん、そっちの方ではありませんが。反対側のバス停なんですが。といったら、長崎神社と。あぁ、それは椎名町だから、そっちだね。Ingressもできるし、どっちでも良いです。

なのですが、お母様、それは長崎神社ではなくて金剛院なのですが。ま、別にいいか隣だし。あんまり言いたくないけど、金剛院の方がお金があるっぽい。なんと、

AR金剛院

なるものが! スマホのアプリでスキャンすると御利益があるらしいです。しかも、そばには、

素晴らしいカフェができてる

金剛院素晴らしすぎる。ちなみにカフェからはIngressのポータルが4つ届きます。

ちなみに、帰った後、また、長崎神社に行こうと言われましたが、今日はもういいです。またね。

Monday, 2 January 2017

お留守番 Agda

少し良くなったので、Agdaをいじってます。

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()

ってのがあるらしい。矛盾からはなんでも出てくるってやつね。

否定もあるんだが、

contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
P → ¬ P → Whatever
contradiction p ¬p = ⊥-elim (¬p p)

¬が、どこで定義されてるのかわかんないんだけど。

なんか、うまく使えん。Agdaのネット上の情報のなさは笑える。空集合をなんとかしたいだけなんだが...

Sunday, 1 January 2017

明けましておめでとうございます

といっても実家で風邪で寝てるだけですが。だいぶ良くなったような気がする。が、出歩くのはやめておこう。おせちがありがたい。

実家に来たら、布団が夏布団。めんどくさいのそのまま使ったのだが、

寒い

と思ったら、クーラーが冷房設定のままだった。冷房の24度と暖房の24度は違うのか?

布団をもう一枚出して使っていますが、下にもう一枚ひきたいところ。

1年前も頭痛かったんだよなと思ってblogを見たら2年前だった。でも去年も年末は体調崩しているらしい。毎年の行事だな。実家の家のせいなんんじゃないか説も。ハウスダストとか。