Sunday, 22 October 2017

歯医者さん

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

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

  詰め物にポッチがある'

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

  ポッチ

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

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

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

Wednesday, 18 October 2017

学生のやりたいこと

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

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

まぁ、そうだよなぁ。

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

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

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

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

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

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

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

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

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

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

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

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

Tuesday, 17 October 2017

クラウドの課題

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

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

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

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

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

  Web service の tuning contest

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

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

Sunday, 15 October 2017

円の描画

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

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

  DDA Algorithm http://tinyurl.com/qa48sjv

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

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

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

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

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

  円をアフィン変換する

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

  ベジェ曲線で近似する

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

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

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

Friday, 13 October 2017

Kindle 本

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

  学生がなんか買えない

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

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

  コピペができない

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

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

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

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

  Kindle / Amazon くそすぎる

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

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

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

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

Wednesday, 11 October 2017

目医者さんと歯医者さん

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

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

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

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

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

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


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

Monday, 9 October 2017

iOS, OS X upgrade

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

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

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

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

  iCloud drive のファミリー共有

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

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

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

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

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

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

-

Sunday, 8 October 2017

OSを上げないと...

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

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

Wednesday, 4 October 2017

Ingress CF challenge

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

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

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

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

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

Saturday, 30 September 2017

コードギアス

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

  全然観ず

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

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

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

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

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

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

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

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

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

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

Wednesday, 27 September 2017

2000 CF

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

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

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

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

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

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

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

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

Tuesday, 26 September 2017

Javaのpackage名

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

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

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

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

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

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

で、

  hg mv Hoge hoge

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

  hg rename Hoge tmp
  hg rename tmp hoge

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

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

Friday, 22 September 2017

VHS発掘

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

  もっとも古いのがない

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

  実家にあったのはVHS x 3

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

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

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

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

  みんな結構もってる

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

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

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

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

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

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

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

Wednesday, 20 September 2017

Ansible

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

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

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

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

結局、

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

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

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

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

Tuesday, 19 September 2017

OS補講

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

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

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

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

  解けない問題がある

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

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

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

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

  やればできる

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

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

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

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

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

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

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

Saturday, 16 September 2017

動いた...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Friday, 15 September 2017

たかね

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

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

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

Thursday, 14 September 2017

台風18号

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

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

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

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

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

Wednesday, 13 September 2017

Ingress の補給

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

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

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

なんだが、

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

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

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

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

Tuesday, 12 September 2017

blog は 2005年から

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

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

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

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

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

Monday, 11 September 2017

目の注射

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

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

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

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

Saturday, 9 September 2017

Twonkey Media 復活

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

  Twonkey Media を本家からinstall

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

  http://twonkyforum.com/downloads/

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

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

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

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

Wednesday, 6 September 2017

DLNAサーバ

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

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

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

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

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

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

Tuesday, 5 September 2017

洗濯機のUI

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

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

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

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

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

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

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

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

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

  What you see is what you get

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

Sunday, 3 September 2017

東京のIngress


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

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

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

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

Saturday, 2 September 2017

目医者さん

沖縄に戻ってきました。

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

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

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

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

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

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

Sunday, 27 August 2017

打ち上げ花火

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

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

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

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

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

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

Friday, 25 August 2017

Ingress Mission

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

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

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

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

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

Thursday, 24 August 2017

いつものお見舞い


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

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

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

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

Monday, 21 August 2017

超準解析

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

  肝腎のモデルの話がない

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

今回は、

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

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

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

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

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

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

  1と0の無限列ができる

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

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

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

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

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

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

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

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

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

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

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

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

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

  http://planetmath.org/constructionofdiracdeltafunction

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

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

  超実数に全順序がある

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

Sunday, 20 August 2017

ハクソーリッジ

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

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

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

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

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

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

Saturday, 19 August 2017

fj 同窓会

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

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

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

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

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

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

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