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年前だった。でも去年も年末は体調崩しているらしい。毎年の行事だな。実家の家のせいなんんじゃないか説も。ハウスダストとか。