最近、早起き

特にそういう決まった生活習慣ないので、たまたまです。

なので、夜、早めに眠くなってしまう。 飲みに出ても、 結構、寝ちゃって怒られてます。

明日も、ちょっと早起きかぁ。

キャプテンフューチャー

78年にNHKで放送されたSFアニメ。スターウォーズとほぼ同時期ですか。宇宙船は2001年の影響が出てます。ハミルトンの原作では涙滴型ですが、それに近いけど、ディスカバリー号みたい。

NHKは元のフィルムやビデオテープのなくしてしまったのですが、フランスに残っていたらしい。フランス偉い! 時をかける少女とかもないんだよな。見れるのはうれしいです。ブルレイ買うとは思わないけど。

原作がスペオペ、つまり、

＊　科学設定は適当でいいから宇宙を駆け巡って悪と戦うんだよ

というものなんですが、その科学設定が、まぁ、かっこいい魔術みたいなものなんだよね。太陽系の原初に戻って潮汐説による惑星誕生を目撃するとか。核燃料が足りないので過去に戻って、半減期で減る前の核物質を取ってくるとか。野田大元帥が監修しているので、結構、原作通り。

というわけなので、それなりに醒めた目で見ていたはずです。

似た設定だとキャプテンウルトラって特撮ものもあるのだけどさ。

https://www.amazon.co.jp/dp/B01CTXVYKK

Flight line fair

久しぶりに行ってみました。大山のゲートから。そこから基地内のシャトルバス。

＊　今回は滑走路上を通過

おお、そんなこと許されるのか。写真撮ってもいいけど、中身見るかもねとかいう警告が。駐機場には、

＊　F15戦闘機、オスプレイ、C17輸送機

などが。最近はジェットな輸送機も普天間にいるのか。乗せてもらえるものも。

防弾服着てみたり、野戦キャンプの中で、ラップトップな無線機使わせてくれたり。戦車はありませんでしたが、ミサイル発射機とかはあったな。

帰りは佐真下ゲートから。そこ開いてるんですか。珍しい。

食べ物はビールとかチキンとか。ピザハットとか。お腹一杯だ。

いろいろ災害があると時期がずらされてしまうので、地元でも気を付けてないと「あ、今日なんかやってる」みたいな感じになってしまいます。

http://www.kanji.okinawa.usmc.mil/Events/Events.html

とか見ると良いらしい。kanjiってなんだ。

OS補講

今年もやります。10人ぐらいか。それぐらいがちょうど良いかも。落とした人はもっとたくさんいると思いますが、夏の補講は、

＊　後期の授業と、卒研と重なるのが嫌な人向け

なので。

今年は割とやる気がある方? いや、もちろん、そうでなくては。

今年はOSの教科書は、

Modern Operating Systems (4th Edition)
by Herbert Bos by Andrew S. Tanenbaum
Link: https://amzn.com/B01JQ0XXL2

にしました。なんか安くなってる。

popup block

今のbrowserだとdefaultでonになっているらしいです。

学科のシラバスとかのシステムが変わったので、

＊　もちろん、後期のシラバスを登録できない

という技が。ボタン押しても反応しない。学科のMLに登録できないって書いて思いついた。

＊　もしかして、別Window開こうとしてる?

で、browserのpopup blockを切ったら出ましたよ。別Windowが。

今時、popup はないだろと思うんだけど。そもそも、

＊　popup を開きまくるbrowser crasherが流行った

のが原因じゃなかったっけ。

まぁ、書けたのはよろしいんですけど。

20日ぶりにコンパイラのバグが取れた

最適化すると動かないという問題だったので、そもそも、

＊　どの部分でバグってるのかがわからない

stackが絡んでいて、stackから取り出した値が変で落ちるみたいな感じなので、stackに入れる時には何も文句言わないし。しかも、

＊　stackに入れた値自体は正しい

おいおい。まったくわからないです。で、

＊　Code Segement の間全部に script で ldb の break point を書けた

これで、どこで最適化されたものとそうでないものとの動作の違いが出るかを trace の差で見つけるわけだ。Parallel Debug と自分で呼んでるんですか。

これで、ようやっとわかりました。局所変数の初期化のコードが出てない。不要なものだと思って削除されているわけね。最適化しなければ削除されないわけだ。

で、LLVM IRの方を見てみると、普通のfunction call の直前に call lifetime.end が出てる。いや、それは tail call な CbC goto の時にだけしかやっちゃいけないのだよ。それで使ってないと見なされたな。確かにチェックのコードがぬけてました。これで解決。

生成されたコードの不具合を見つけるのに19日で、コンパイラをなおすのは1日だった。まぁ、だいたい、そんなものだよな。

twitter 6000 following

特に深い意味はないんですが、あと、30人だったので、増やしてみました。followers 5740 なので、6300ぐらいまでは増やせるらしい。

＊　意外につらい

昔は public time line から拾ってたりしたんですけどね。30増やすのでも面倒なもんだ。

＊　まず、自分のfollowerから

なんだが「いろんな意味で危ないのではずしている人」も、いるので気を付けないと。そういう人はlistに入れて再フォローしないようにしてます。うっかりすると、TLがエロ画像だらけに。

＊　次は、LIKESから

これは定番の方法らしい。自分が気に入ったマークを付けた人をフォローするわけですね。

というわけで、自分のTLはカオスです。ほとんど public time line だな。

特に見たい人はリストに入れてます。

研究室のOBとかメンバとかもリストにしてますが、たまに邪魔なのがなぁ...

＊　自分のグチ用と広報用と分けてくれない?

まぁ、害はないんだけど。つまらんよね。

Twitter accountは結構あっさり特定されるので(イベントのことを書いたりすると一発...)、それなりに気を遣うべきだろうな〜

と言いながら、僕も好き勝手に使ってますよ。

ガルパンのテレビアニメ

こっちの方も見てまみました。録画はしたが見てなかった。そんなのばっかりだ。

当然なんだけど、

＊　劇場版と基本同じ

アンツィオ戦はまああれだったけど。そっちはOVAなのか。

戦争ごっこを女子にやってもらうという極めて男の子向けな企画なわけですけど、楽しめれば良いよとも思うな。

おっさんどもを除いて徹底的に男子が排除されてるのもそれっぽい。

今季は録画しているものを一つも見てないんですが、なんか見るべきものあるのかな。

君の名は。

ライカムで見てきました。人気あるみたいだけど、ゴジラに比べれば「普通の佳作」でした。

ゴジラの予告は見せない予告だったけど、「君の名は。」の方は見せる予告で、普通に見たいと思いました。その分、見たかったものしか見れなかったかも。

新海誠は秒速5cmとかで、だいたい感触はわかっていたので、いきなり音楽が流れ出しても「やっぱり、そうくるか」ぐらいですみました。

アニメの時をかける少女の恥ずかしさみたいなものは結構あったので、そういうのが好きな人には良いんじゃないかな。

超常現象がダメな人には、まぁ、ダメでしょうね。

居酒屋week

でした。

鶴千 http://r.gnavi.co.jp/k6c5mt160000/
割とこじんまりとした串焼きと魚のお店
大同病院の裏かな? こういうお店は割と好きかも

のむりえ http://r.gnavi.co.jp/g3dwathd0000/
いつもの。ちょっと混んでた。

加藤食堂 http://tabelog.com/okinawa/A4703/A470404/47002382/
いつもの。フレンチだけど、ピッツァのお店という認識です。ちょっと飲みすぎたみたい。ワインは水に感じる。

絆屋 http://r.gnavi.co.jp/rerpt1dc0000/
新都心はあまり使わないか。普通な感じでした。結構、静かだった。

阜 (ゆたか) https://www.hotpepper.jp/strJ000659996/
前はお昼に良く使っていたんですが、お昼なくなったのでご無沙汰。夜に定食を頼むことも可能。まぁ、ビールぐらい頼むのは礼儀だが。
普通はお店だが、さすがに混んでた。

絆ってのは3.11以来流行ったが、自分的には共感しない言葉だな。絆よりは、対処と備えだろ?

居酒屋ご飯よりは、ご飯は酒抜きで、それから飲みに出る方が好みではあります。

久しぶりに圏論

なんか休みになると Agda に触っている感じ。コンパイラのバグが厄介そうなので、ちょっと逃避ですね。

今回のお題は、

Complete Category が initinal object を持つ iff Preinitial Full Subcategory

ですね。フロイトの随伴関手定理の補題らしい。いつもの Higher order categorical logic の0章。

相変わらず、そっけない証明が記述されているだけなんですが、

Subcategory は A から A への関手があれば良い
Full は射が全部あるってことなので、関手の逆射があれば良い

というのを3月の辺りに書いていて、それがばっちりだったので、割とすぐにできました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/61550782be4a/freyd.agda