プロジェクタとPCの画面

授業用にノートPCをプロジェクタにつなげると、

＊　解像度が変わって、Spacesの各画面の位置が勝手に調整される

おっとと。ミラーリングにしなれば、そういうことは起きないんだけど... プロジェクタに向かって学生と同じ方向で授業すればとか思いつくけどね。

でも、新システムではプロジェクタに、備え付けのMac Miniが付くはずです。

＊　そこに向かって、Tree VNC で画面共有してやればばっちり

なはずですがね〜 クライアントノードは有線が望ましいが、VNCサーバ側は無線でも大丈夫なはず。

ただ、

＊ Retina のdisplayをVNCで表示することになる

ので、少し工夫は必要なはず。一応、拡大縮小もサポートされているのですが、

＊　非力なマシンでは遅い

というのがあるらしい。そこで、Java に「速度優先でRenderingする」というoptionがあるらしく、それを使うと、

＊　アンチエイリアシングはさぼる

という手法で高速化されるようです。なかなか面白い。

9月以降が楽しみではあるな。また、TreeVNC のハッキング大会でもやるか〜

来週は京都だ

なんだが、ワークショップとは言え、発表する学生と連絡が取れないという状況に。

＊　英語の発表、甘く見てんじゃないの?

まぁ、別に、今から英語勉強したって間に合いはしないわけだけど。

若い人が、人生甘く見るのは悪いとは思わないけどね。僕もいまだに甘く見ていることは、その通りだし。

Mr. Philip Tan from MIT Game Lab
http://seeker-s-eye.blogspot.jp/2012/11/mr-philip-tan-from-mit-game-lab.html

この時の学生なので甘く見ていること確実だな。

最近、研究室に来ない学生が結構いて、将来が楽しみです。まぁ、来ればなんとかするさ。

皆勤賞は嫌い

男の子ってのは、だいたいそうなんだけど、自分も小さい頃はたくさん病気してました。子供の頃の記憶と言うと家で寝ていた記憶が多い。専用だった水色の折りたたみベッドとかを思い出すな。

なので、皆勤賞とかには縁はない方です。小学校はもちろん中高でも。中高はそんなに休んだ記憶はないけど。

なので、風邪で一週間寝込むとか別に普通ではあるね。声以外はなんとかなった気もするが、まだ、少し熱が残ってるかな。

あぁ、でもなぜか、IngressのSojournaは切れてないみたい。なんでだろう。不思議だな〜　まぁ、近所にポータルたくさんできたし。去年みたいにバスにのらないとポータルがないなんていう状況では無理だったでしょうけど。家から届くのが望ましいが。

Agda の謎

今日もおとなしくしているわけですが。(つまり、酒は飲まないという意味です)

ちょっと前から行き詰まっている Agda を見直してみました。

＊　Floyd の Adjoint Functor Theorem

が目標なわけですが、その前に、

＊　Limit から Equalizer と Product を作る

というのがあって。これ自体は全然難しくないんですけどね。なんだが、そのためには、

＊　Agda 上に有限な射を持つ圏を作る

ちょっと試行錯誤して、List と memberp (ある要素がリストに含まれているかどうかを調べる述語)はできました。これを使って、

＊　Hom(射)とObj(対象)の集合

を作ってやれば良いわけだ。ある record で memberp x list = true になる x を要素すると定義すれば良いんじゃないかな。それで、対象と射はできました。

圏なので、edge の演算を定義するわけなんだけど、

_×_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C

ってな感じ。なんだけど、「ない arrow はどうするの?」って問題が。 Agda はどうも、この「ありません」ってのをどうあつかっていいのか良くわからない。

この A B C にあらゆる可能な Obj の要素が入ってしまうので、困ってしまう。Hom A C は集合なので、空集合でも良いはずなのだが。Hom A Aは必ず一つはあるけど、そうでない場合は空集合な可能性がある。でも、Agad って集合 A があると、

a : A

とかで、必ず要素が取れてしまう。こまったなぁ。

_×_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C

の矢印も「ならば」と思って良くて、BからCへの射と、AからBへの射があれば、AからCへの射があるっていう意味なはずなけどな。

でも証明を書いていくと、A,B,C のすべての組み合わせだが出てきてしまう。射がないところにぶちあたると、そこで矛盾。あだだ。うーむ。この方法ではだめなのか。

風邪のゆくえ

結局、ずーっと寝てました。まぁ、それしかないよな。今朝、ようやっと平熱。まだ咳は残っているけど。まぁ、咳はしばらく残るんだろうな。前みたいに咳3ケ月とかはやめてほしい。

火曜日の朝がピークで38.7℃で悪寒がひどくて。今回は寝汗もひどくて、一日二回は着替えてました。なんか、風呂に入って治したような感じ。

そんな感じで脱水気味で57.5kgまで体重落ちた。学部以降、このレベルはなかったんじゃないかな。

まぁ、お酒を抜く良い機会でもあったか。6月前半まで妙に忙しかったので、その後で良かったです。

来週末は Okinawa Open Source Conference(7/4) がありますが、京都と重なっていて出れません。しかし、

http://www.ospn.jp/osc2015-okinawa/

＊　並列研の展示(琉大IDGA/Global Game Jam)
＊　琉大シス管

の展示はあります。シス管の展示は、

＊　うちのM2の修論のポスター/スライド使えば良いんじゃない?

と言ったが、どうも、最終版をcommit/push してなかったらしい。くそ〜 そこまでチェックしろってか。チェックしてなかった僕があほでしたよ。

そんな新システムも部分的に入り始めているようです。「まずは、ラックだけな」あ、そうですか。

BD-REとOS X

熱も程よく上がってきて、おそらくは、月火まではだめでしょうね。火曜日は慰霊の日でお休みらしいです。普段はゼミはやるのだが。沖縄だと、午前中は平和祈念公園にいく家が多いみたいです。

風邪ひいた時には、録画の整理をするわけですが、前回は2014/6らしい。

＊ http://seeker-s-eye.blogspot.jp/2014/06/bd-r-dvd-r.html

特に風邪ひいていたようには見えないな。

で、OS X Yosemite で BD-RE を読み込もうとするわけですが、

＊　　なんか、ガーガーうるさい。eject時にいろいろやる。

BD-Rでは問題ないので、どうも何か書き込みにいっているらしい。なので、read only mount になる方法を探したんですが、いまいち、うまくいかない。

＊ mount -u -r /dev/disk2 だと、busy と言われる。そもそも手遅れ
＊ /System/Library/Filesystems/udf.fs/Contents/Info.plist に -r を追加しても見てくれない

そもそも、mount_udf 自体に -o rdonly がない疑惑が。

/var/log/hd.log とか見てたんですが、/var/log/system.log を見たら、

＊ /Volumes/SONY_BD_RECORDER_VOLUME/.Spotlight-V100/Store-V2/BEEE0798-CADB-484E-A758-F4F4CC4191F5/0.indexGroups

お前か! そういえば、Spotlight 停める方法あったよな。あと、fseventsd も .fsevets 作るらしい。これらを、


sudo launchctl unload -w /System/Library/LaunchDaemons/com.apple.metadata.mds.plist
sudo launchctl unload -w /System/Library/LaunchDaemons/com.apple.fseventsd.plist

で停めてやればOk。これで、BD-REでがーがー言わなくなりました。そもそも、書き込み可能光学メディアにそんなことする意味はないので、これは、

＊　バグ

でしょうね。そもそも、

＊　eject 時に Panic

を数回喰らったし。まぁ、BD-R/BD-RE読めるだけですごい。もう誰も使ってないかもしれないし。

これで録画したものがどこかを探すのは容易になったはずです。でも、普通の人は、

＊　外付けHDD録画

だろうなぁ。でも、HDDはいつかは壊れるものだから。いや、BD-R/BD-REでも、かなりの率で読めなくなるけどね。LTHの10%ぐらいがやられてました。最近はBD-RE onlyにしてます。十分安くなったので。相転移メディアは偉大。DVD-RAMはトラブルなかったからな。

そういえば、沖縄に来る時に持ってきたCD-Rって、まだ読めるのかな? 今度、探してみよう。

やっちゃったかも

喉痛い、だるい、熱っぽいで、風邪伝染されたかも。

週末とか休み前になるとやられるパターンだな。もっとも、明日は金曜日だけど。

家でおとなしくしてようと思ったら「源泉票もらってこい」だそうです。即日で出してくれれば良いのだが、いつものように「担当の人がいない」らしいです。トラックファクター1だな。いや、本当にそうかはわからない。適当にレイズすればできるのかも。まぁ、そういうのは「元気な時に」とっておこう。

というわけで週末はおとなしくしているつもりです。近所のポータルのぞくぐらいややるだろうけど。Sojourna medal ひどい。

少し、自分のPCの環境を整えないと。

Monoid

なんか唐突に授業で出てきて。自分で忘れているところがな。Monoid は、

＊　単位元があって結合法則が成り立つ

というぐらいなので特に難しくはなく。

なぜ出てきたかは、ちょっと先を見たら思い出した。

＊　Monad の例に使う

というわけですね。Monad 則を満たすのにはMonoid との直積を使うのが楽らしい。もっと、一直線な授業の構成にするべきだな。

例としてはリストとか、関数の結合とかを挙げているのだけど、リストだけで十分かな?

Monoid を Haskell で定義するとかは入っていたけど、それだと単位元と結合演算だけで、結合法則が入れられない。

Monoid の定義を Agda で書いて、リストがそれを満たすことを示すとかが良いはずだが、それをいれなかった理由はなんかあるのかな? (単にさぼているだけか?!)

継承と移譲

まぁ、いつもの話なんだけど。Java だと他のクラスを継承することができて、

＊　継承したメソッドをちょっと修正

というのが可能。@Override とかいうannotationで、ちゃんと上書きしているかどうかを調べられます。

なのだが、

＊　まず、元のメソッドを全部コピペって、それを修正

ってのがあるらしく。だから、それやらずに、

＊　元のメソッドを呼び出せばよいだろ

ってことですね。同じコードを二度書いたら警告が出る IDE ってないのか?

なのだが、同じ通信路を圧縮ありなしで選択という場合で、

＊　圧縮なしを継承して圧縮ありを作る

というのをやってもらったんですが、

＊　通信路は一つなのにインスタンスは二つ

というのをやられてしまって。それは、動作がおかしくなるな。受信スレッド二つはダメだろ?

というわけで、そういう時には、継承ではなくて移譲を使う方が良い。つまり、

＊　ちょっと変更してから、元のインスタンスのメソッドを呼び出す

わけですね。これだと、元のインスタンスの動作を妨害しないのが良い。初期化時に元のインスタンスを渡してやる必要がありますが。

移譲の方がコードの依存性を下げられると言われているんですが、残念ながら Java には移譲に関する言語機能的なサポートはない。なので、

void hoge() { deleget.hoge(); }

みたいなのをたくさん書く羽目に。継承だと、こういうのは書かなくてすむのだが...

なんか、良い方法ないのかな。

腰の具合

忘れているぐらいには良くなったみたいです。でも座っていると「危ない感じ」がする。なので腰痛持ちな立ち振る舞いです。整体は効果あったということか。今年はぜんぜん泳いでないので、

＊　筋肉落ちまくり

で、その影響が出たのかもしれないです。体重は減ったけどね。まぁ、結局は、

＊　歳だから

ですね。体調自体は、

＊　泳いでいる時よりも良い

です。お正月に歯痛喰らってから、特に寝込んだりしてない。プールは、雑菌拾うからなあ。

かなは、風邪で寝込んでいるようです。お大事に〜 水分取って寝てるしかないさ。

だめなUI仕様とUML

消滅都市のデスパーティのプロトコルを見てそう思ったわけですが...

学生には、

＊　まず、ユースケース図書け

と言ってます。機能や、プログラミングから考えていくと、

＊　なんでもかんでも、command line option (そりゃ、それ楽だろう)

＊　いつも使う機能のメニューが遠い

とかなりがち。

＊　実際に作って動かしてみないとわからない

なら、まだ良いのだが、

＊　作っている人に取っては複雑な手順はうっとうしくない

らしい。だって、

＊　動く方優先
＊　やりたいこと優先

だからね。

＊　こうこう、こうしたい

と言うと、

＊　それは、お前が使い方をわかってないからだ

とか言われることも。

ユースケース図は、紙芝居に相当するわけだけど、それでも、いくつかの問題は洗い出せるようです。でも書き方にもよる。

＊　ユースケースの丸に極めて複雑なことが書いてる

＊　ユースケースのネストが複雑

とか。

UMLの入門書に、

＊　俺はユースケース図はわからん

とか書いてあるのがあって、いや、

＊　ユースケース図はトランザクションを書くんだよ

と言いたいが、

＊　UMLは所詮、道具であって、使い方は自分勝手で良い

とも言えるんだな。ステートチャートにいたっては、

＊　どんな図でも「それは間違った書き方だ」という人がいる

という状況じゃないかな〜

UI書く前に、ちょっとした紙芝居ぐらいやろうよ... というか、だめなUI手順を修正する手続きないの?

大型計算機センタ

という名称だったんじゃなかろうか。院生時代、研究室に Vax 730があり、それ経由をセンタと接続したり、ネットニュース読んだりで、計算機センタの故松方純さんのところに良く顔を出してました。さして意味がなくても遊びに行っていたと思う。

たぶん、その関係で村井先生と会ったんじゃないかな。当時、根津美術館の二階にあった茶店でお昼ご飯を食べていて、そこで会ったのだと思います。だいたい30年前です。第一印象は、

＊　この人は、なんて太っているんだ!

です。既にWIDEな人たちが周りにいて、自分でもサーバ管理に関わっていたので、村井先生の周りは面白かったな。sendmail.cf やらDNSやら。

村井先生には優秀な秘書さんが付いていて、なんと、

＊　ダイエット成功

な時期もあったはずです。4月に会った時には「割と普通」な体型でした。(そこしか見ないのか?)

スパゲティが好き

ですね。沖縄に来たばかりな頃、久茂地にあったイタリア食堂で、

＊　スパゲティ二種類とワイン一本

という頼み方をしてました。今もパスタで昼夜とか多いな〜

TreeVNC

うちで作った授業/ゼミ用の画面配信システム、

http://www.cr.ie.u-ryukyu.ac.jp/software/TreeVNC_en.html

なんですが、最近、至極、快適です。プログラミング3で学生に作ってもらったものですが、ようやっと使い物になるようになった感じ。

＊　授業の先生の画面を学生に「先生のPCを重くすることなく」配信可能

＊　発表する学生の画面をネット上で切り替えて表示するDisplay mode

の二つで動きます。

ただし、有線でないとだめです。無線でもつながりますが、最初の二つ三つが限界ですね。

プログラミング3の授業でプロジェクト毎に順々に発表してもらうわけですが「コネクタ切り替えて」とかやらなくてすみます。あと、

＊　コネクタを占有しないでプレゼンできる

ってのも素晴らしいです。

どうも最後当たりにいろいろ入れた機能が悪さをしていたらしく、その辺を卒研発表後に削ってくれたので調子良くなったらしい。

Java なので、なんでも動くはずですが、Windows とかでどう動くのかはテストしてないんだけどさ。

でも、ちゃんと使い方書いてないな。もっといろいろ書かないとだめかも。最近の動画か。

学生旅費

7月の京都のLICSに学生と一緒に参加しようかと。発表はワークショップだけですけどね。今は校費から普通に出せるらい。昔はダメだった。ま、どうせ、いつもの事務の

＊　特に根拠はないが勝手な内規で許可しなかった

だったのでしょうけど。なぜできるのようになったのか知りません。

＊　学外予算を取ってこい

というインセンティブだったかもね。なのだが、

＊　日程とかうるさいい

これは昔の方が楽だった。行き先と日程でだけで定額支給。別にそれで良いんじゃないかと思うけど、半券出せとか。

僕はどうせ東京の母のところに寄ってくので飛行機代はでないはずです。うだうだいうのも面倒なので自費です。最近はマイレージ以外で飛行機のるは稀だしな。それでも、

＊　学生と一緒の日程にしろ

とか言ってくるわけですが、まぁ、言ってくるだけらしい。学部生は先生の子供扱いか?!

自費研修扱いにすれば、一応、仕事していることにはなるらしいです。

そういえば、バス代は回数券廃止のあとどうするつもりなんだろう? 回数券の表紙はたくさんあるので当分困らないが...

x.v6 読み会最終日

いや、まぁ、

＊　短いソースって良いなぁ

と思いました。

午前中は昨日の復習から。real mode/protected mode/64bit mode へ。 segment の初期化で、また、LDT/GDTを読んで。

初期化を読むのは退屈なので、次は、wait system call。おそらく一番簡単だろうと言うことで。そしたら、

＊　process table をfor文で、先頭からなめて子供を探す

え〜　そんなのあり? と思ったら、process table は64 entriesしかないらしい。でも、

＊　そのfor文を、そこいら中にばらまく

ってのは、どうなのかぁ。

そして、なぜか、

＊　ptable をlock/unlock しまくる

しかも、lock release 時にも、

＊ lock xchg

するのだが、そこには、

＊ INTEL64では、普通の代入で良い

とかいう謎のコメントが。返り値チェックしないのに lock xchg してどうするの? まぁ、もしかするとわざとかも。lock時は、もちろん、CASしているわけですけどね。

system callや割り込みで trap に来て、そこから普通にreturnで戻って、iretq するわけですが、kernel の中で、

＊ swtch

とかで、context を切り替えてしまう。iretq してるプロセスがたくさんあって、それをschedulerが切り替えている感じですか。

読まなかったけど、最初のinit processのところで割り込みスタックを作るようなことをしているんでしょうね。なので、

＊　fork 書く方が spawn より楽だ

とは思いました。

V6のソース読むよりは、x.v6の方が良いかなとは思いましたが、ちょっと玩具な感じはしかたないかな。コメントもあまりなくて、マジックナンバーも多くて。

でも、Linux の方が爆発してるので、OSの授業で x.v6 使うのも悪くはないかな。boot プロセス面白かったようなので。

x.v6 読み会二日目

午前中は、Intel64 のマニュアルと格闘。

＊　Segment Register
＊　GDT/LDT
＊　CR3
＊　PD/PTE

Real mode (8086)からProtected mode(ia32)への切り替えは「こうやれ、余計なことするな」とマニュアルに書いてある。まぁ、要するに、

＊　マニュアルに書いてある通りにすれば良い

わけですね。Protected mode から64bit mode への切り替えは、

＊　PTEのフラグを設定した Code segment へ Jump

という方法だそうです。なので、午後一からは、

＊　アセンブラで GDT と Page table を作る部分

を読みまくりました。しかし、

＊　コメント皆無

ですね。まぁ、読みづらくはないんだけど。普通のアセンブラとCだから。最近の Linux は、

＊　コードを読みにくくするのを生きがい

にしているみたいなところがあって、それに比べればいさぎよい。

物理メモりはシングルリンクで簡単につなげるだけですか。良いね。その後、いろいろやるのでしょうが。

acpi でCPUの数を調べるところまで読んだので、明日は、system callっぽいところが読めるはずです。

http://www.cr.ie.u-ryukyu.ac.jp/~game/pukiwiki/index.php?xv6

この辺に、Vagrand box があります。でも、kernel gdbが成功するのは稀らしい。原因不明。通る人と通らない人とがいるらしい。

x.v6 読み会

golang で書いた Docker は、あまり良くは読めなかったけど、一応、終わったのかな?

明日から、x.v6 のコードを読みます。64bit 版という条件を出したのですが、結構、錯綜したらしい。

＊　16bit -> 32bit -> 64bit

と移行するので、それを

＊ 同時に一つのgdbでは追うことはできない

gdb がSEGVするらしいです。あらら。なので、それぞれで違う gdb をattachするらしい。

で、gdb で QEMU 上の x.v6 をtraceできる Vagrand Box を作ったそうです。そうですが、見つからんな。

読み会を UST するかどうかは明日の根性によるでしょう。今日は、準備で、gdb で追えることは確認しました。

　＊　＊　＊

整体は行ってきました。「良くなりましたか?」「いや、あんまり」「上体そらしてみてください」「あ、痛くない」「良くなってるじゃないですか」良くなってるみたいです。明日も行くか〜　

基本方針は、

＊　腰痛は Ingress で治す

です。

整体

腰痛というわけで、整体に行ってみたのですが、

＊　これは、マッサージと同じもの

だな。マッサージなんかだめなんだよな。触られるのあんまり好きじゃない。この手の痛みは、

＊　腱鞘炎と40肩

でくらったことがあります。まぁ、マッサージとかで楽にはなるのだが、

＊　対症療法

だよな〜　今回の腰痛は40肩と同じ単なる老化現象なんじゃなかろうか。まぁ、そろそろ「ゆっくりすれば?」という身体のサインなんでしょう。なので、Ingress で歩いて治す方針で(お)。

整体の先生には「腎臓のツボが」とか言われましたが、人間ドックではだいたいタンパク出てると文句言われるし、時たま、痛むので、腎臓は何かダメなんでしょう。超音波とかでは何も出ないんだけど。

明日も来てくださいと言われましたが、根性があれば。いつもの内科の先生にも腰痛の話をしてみるか。座ってる時に、脈絡なく激痛ってのはかんべんしてもらいたい。

腰痛 Ingress

というわけで、昨日から腰が痛いんですが、やることは、いつもと変わらず。まぁ、たいしたことないってことなんだけど。酒飲んで、Ingress してます。

＊　バンテリンは悪化

したので冷やすのはダメっぽい。歩いている方が良いみたいです。なので、

＊　普通に Ingress は可能

らしいです。

まぁ、内臓系か老化だろうなぁ。明日も痛いようなら病院いくか。

添付ファイル

もともと MIME が adhoc かつダメな規格で... でも、Mac OS X が

＊　UTF8をMIME encodingして送る

というわざを出したので、したかなく、Perl で書いたdecoderを使ってます。PDFやMS Wordも less で見れるすぐれものです。antiword とかpdftotextを呼び出しているだけだけど。

昔はファイルを複数のメールに分割して送ったりとかあって、もっとひどかったが、今はさすがにそれはないか。

OS Xには、メールの添付ファイルを実行するという文化はないのだが... それで困ったことはありません。

今日は腰が痛い。なんだろうな。結石じゃないのとか言われたこともあるんだけど、そんな激痛ではないので、ちょっと我慢ですます。