台風過ぎました

なんか土曜の朝8時には停電してしまって。復帰は今日の15時だったみたいです。13時から16時までは目の中にいました。

ベランダに奥様のプランターがたくさんあったんですが、全部、中に入れたのでベランダには何もなくて平和。前は折りたたみテーブルかなんかを
残してしまってうるさい目にあいましたが。

まだ、アンテナは確認してないけど、そんなわけなので割と無事だったようです。プランターも外に出したし。

まぁ、冷蔵庫の中は全滅ですけどね。火曜日にまとめて捨てるんだな。

台風の準備

久しぶりに風速70m直撃らしく... 2012/9以来かな? しかも、この手のってしばらく居座ったりするからな。でも、沖縄を過ぎれば高速になるらしいです。

というわけなので、ベランダのプランターをお片づけ。新聞取ってないから新聞紙がないのがな。蔦みたいなのもあったが、ぜんぶひっぺがし。ま、しかたないですね。

あとはインスタント食品シリーズか。停電するとやっかいですけどね。最近は停電は少ないが。でも、2012は停電したはず。

MBPの電源がないが、まぁ、切れたら、MacBook Air 使えば良いか。

Agda trouble

Agda version 2.5.4.1 にあげたわけだけど、なんか、いくつか通らない証明が... 前にもそういうのあったんですが、

　　その時には、証明の方がおかしかった

引っかかったのは、monad から applicative を導くと言う奴で、Sets が絡んでいるので、いろいろ大変な奴... あらら。

赤が出ると type conflict なので完全に失敗してしまうわけなんですが、さすがに、そうはならないけど、

　　黄色くなる

これは、微妙なんですが、型の衝突はないが、

　　項が等しいと判断するのに十分に変数の値が代入されてない

みたいな感じらしいです。でも、証明は繋がってないのでダメ。だいたい、変数の対応を推論しきてれないことが多いので、
暗黙の変数({x}みたいな)を明示してやると通ることが多い。

多いわけですが、一度証明が通っているので、それほど簡単ではなく...

(λ r →

とか書いてるところを

(λ (r : ((b → c) → _ ) * (b → c) ) →

と書いたらなおったところが。う、うーん。

もう一ヶ所は、読みやすくするために、同値な項だけど形が違うものを書いていたりするんですが、

　　それを取り除いたら黄色が消えた

なるほど? 余計なことするなと。

最後のが苦労したんですが、

　　Product が builtin になったらしい

なんかλかなんかで定義されていたのに。それで、

　　normalized term の形がずれた

具体的には、項をまたがった Product の reduciton をやってくれなくなったみたい。変形して、そばに合わせてみたいな感じで逃げられました。

この手の微妙なのが Agda はなぁ。まぁ、学生が扱うにはそんなものは出てこないはずなんですけどね。

いやいや、今頃は、もっと他にやることあるだろ〜

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/rev/06388660995b

JPHacks 説明会

沖縄は10/27-28だそうです。

割となんでもありな感じな　Hackathon かな?

村上さんには、割と好き勝手をいいましたが、いつものことなので、気にせずにお願いします。

https://2018.jphacks.com

(今日は、Excel とか書かされたので、ちょっと逃避して圏論の例題解いてました...)

お休みな日

ラーメン食って、大学にいたら、飲みに来いメールが来ていたので、琉大のそばの行きつけの店がいいといったんですが、

　到着のメッセージを見落として1時間放置でごめんなさい

でした。いろんな話が聞けて楽しかったです。

明日も飲みに行くことは決定なみたい。よろしくお願いします。

今日のIngress

あと30分頑張れば閉じられたが、また、明日〜

今日のハイライトは、どちらかというと北上原公民館を取りにいったことかな。

サンダーバード秘密基地

買いませんでしたが。祖母に言えば買ってくれたとは思うけど。替わりに、

　　0-X 号

は買ってもらいました。映画見ると「たる〜い」話でな〜

下面に車輪が付けられるようになっていてゼンマイで動くのだったかな? それ用の穴が子供心に「これなんとかならないの?!」

今だったらパテなりで埋めるわけですけどね。さっさと壊して捨てられてしまったはずですが、先頭の着陸船部分はだいぶ残っていたはずです。

ジェットモグラ号が砂場で役に立たないと言う経験が工学者には大切だと思います。

OSで使う言語 Java 10

まぁ、C はやるんですけどね。

すでに Java 10 という話。なんか、最新のしかサポートしなくなったらしく、しかも、

　　Java 9 から微妙

という感じなので、ついていくのにしんどくなってるところです。それに、

　　古くさい

ってのもあるね。こういう

Hoge hoge = new Hoge();

みたいに同じことを何回も書く言語はダサい気もするし。

golang もいいかなと思うんですが、

　　OSのAPIを学ぶには、少しずれてないか?

ってあたりがな。速度的にはJavaの方が上なみたいです。速度が重要なわけでもないですが。

C#にすると、Unity と連結するので便利ではあるんですけどね。

Haskell/Prolog 辺りは別な授業でやってるし、OSとの相性はよろしくない。

OSでメモリ管理やる一方で、GC base の言語ってのもずれてる感覚あるんだよな。Apacheのpoolみたいなのが良いとは思わないんだけど。

ま、とりあずは、今年は Java 10 な予定です。

High Performance VDI Conference 2018

補講は学生に任せて行ってきました。学生が来ればタダ飯食えるのに。もっともOISTは遠いけど。

VDIと言いつつ、なんかストレージの話ばっかり。

＊　　Pure Storage

NAND Flash のコントローラをFPGAで独自実装して高速なSAN node。重複検出してくれるが'売りらしい。
SANの先に繋げるだけなので検証容易。でも、これ次世代不揮発メモリが出たらどうするの?

＊　　Datrium

SSDを仮想ディスクとして使うLAN baseなstorage node。プレゼンではなんなのかさっぱりわからず。
ブースに聞きにいってようやっとわかりました。これはくせがありそう。CentOSでまともに動くかどうか。
でも、SAN無しですむのは良い。

Pure Storageの人と「SANなしでNASだけで構成する手もあるよね」みたいな話もしてました。

いずれにせよ、検証機もらって動かしてみてからだな。Datrium はSSD手に入れないと評価できないらしい。

https://www.highperformancevdi.com/ja/

ペアプロ

OSの授業は課題37個ぐらいで、最近の標準からすると多いのかも知れないけど、OSのインストールとかDockerでの実験とかなので、

　　まぁ、やればできるでしょ

的なものですが、適性はあると思うんだ。

　　Javaのtestをgradleに記述して、Jenkins でチェック

とか、やってみると、間違える可能性が無限にあって、結構ハマる。これを乗り越える根性が.... そういうところを避けるように課題を
作ることは可能ですけど、

　　実際のプログラミングとかは、そんなものの塊

だったりするので、避けるのは少し違う気がする。

でも、いかんせん補講受けに来るぐらいの学生なので、そういうレベルともまた違う。

　　1時間たっても最初の課題を出さない

ちなみに最初の課題は「教科書から10個、英英辞書を使って単語を引く」ってやつなんですけどね。何故出さない。それは不思議なことなんだけど。

ADHDとかいろいろ言い訳はあるし、やる気の問題と切り捨てても良いんだけど... 今回は、

　　じゃぁ、二人一組にするから、そことここと一緒にやって!

ってのをやってみました。10人ぐらいしかいないんだけど、一人一人ぽつんと座っていたりするんだよ。TAが全員に付くわけにもいかないし。

既に10個とか提出している人も何人かいるので、そういう人に付いて提出すれば楽勝なはずです。

聞いてみると「助かりました」みたいなことを言ってる人が何人か。それでも、結局、別々にやっている人たちが何組か。いろいろ面白いな。

あさってまでですが、なんとか乗り越えて欲しいです。

OSの補講

補講と言っても「出席してれば単位はもらえる」とかではないので、

　　課題の手伝いをしてくれるTAがいる4日間

っていうだけですけどね。

でも、この時期だと、10月から始まるOSの授業の課題のチェックに使えるので便利。さっそく、

　　Fedora 28 では去年の ansible script は動かない

と言う技を出していたようです。どうも、firewalld と mysql-python が Python3 に変わったらしい。

https://ie.u-ryukyu.ac.jp/hg/y17/index.cgi/home/hg/y17/k178572/ansible/

20年たっても迷惑をかける Python 3 ってわけですな。これからしばらくそういうのが続くかも。

トップを狙え2

こっちもなんとか。「努力と根性とかじゃないから」はいはい。別物であることはわかりました。

が、盛り上げ方はそんな感じですね。

2003年なので15年前か。手元の録画は2014のだな。ずいぶん寝かせたもんだ。

カフェユニゾン

普天間でいご通りのカフェですが、

　　なんか、途中から隣でうるさいバンドの演奏が...

100円割引してもらいました。

多少うるさいのは平気だが、低音の漏れがな〜

シュタインズゲート

アニメのゼロの方もようやっと盛り上がってきた感じですが、元の方をようやっとクリア。達成度75%ぐらいだけど、これくらいでいいや。

16時間ぐらいだったかな。それなりに楽しめました。アニメの方が飛ばしモードだったからなあ。ゲームの方が達成感あるし。

タイムマシンものですが、三種類くらい出てきます。

　　携帯メールで38byteの通信
　　記憶を転送
　　人間を転送できるもの

最初のだけで押し通せよと思わなくもなかった。もちろん、J.P.ホーガンのパクりなわけですが、特許とかと違うからな。芸術と言うのは模倣し模倣されながら進歩していくものだからさ。

SciFi なのだから科学設定に突っ込むよりは、指定されたルールの整合性を楽しめば良い。なんだが、それができない人もいるでしょう。絶対音感と相対音感とかとにてるかも。

設定で面白いのは「12TBの人間の記憶データをブラックホールで38byteに圧縮して送る」ってところだな。12TBのエントロピーはどこにいったというわけだけど、

　　圧縮というよりtiny URLみたいなもんじゃね?

実際の12TBのデータは未来の可能性の中に埋もれているので、そこから発掘するためのキーみたいなものなのかも。ファインマンラジオの一種か? ま、設定だし〜

平行宇宙であって平行宇宙でない的な話だけど、この辺の処理はタイムスケープがやっぱり秀でてるかなぁ。それも一つの設定でしかないんですけどね。

やっぱり、物理ループだったらしい

やっぱり cisco の log の見方を復習しないとだめだな〜

flapping しているlogが「別なスイッチ」あ、そうですか。

spannning tree がうまく動いてないってこともあるんだけど、これくらいだと今は「調子が悪い」くらいですんでしまうのか...

いろいろ勉強になります。

スイッチトラブル

一応、CCNP の途中までは勉強したんですけどね。高須さんの講演のあと、上に行ったら、

　　スイッチがおかしいです

え〜 なんか、

　　フロアスイッチが次々に落ちる

という症状らしい。なので、停まっているのに接続に行ったんですが...

　　もう動いてます

え? Cisco のSwitchの脆弱性が出ていて、それ関連かと思ったんですが、Virus関係だったら復活するのは変。

で、メインスイッチの show logging を見てもらったら、

　　flapping between port 22 and port 23

とか言ってる。で、それがいろんなポートで起きてるらしく。それが原因らしい。なんだ? メインスイッチのポートのランプは

　　全部同時に点滅

なので、ループかなと思いました。なので、

　　順番にポートを落として、停まったらそこなんじゃね?

Spannning tree 動かしてないのは良くある話だからなぁ。なんですが、

　　全部落としても、停まらない

残りは、数十パケット/秒くらい。うーん、これくらいだとスイッチの管理パケット程度だな。

show span-tree 見てみると、一応、なんか動いているっぽい。

で、ポートを元に戻してみると、ランプは相変わらず同時点滅なんですが、

　　なんか、快適に動いているんですが...

なんだぁ? show logging には fapping は現れず。

これだと、ちょっと僕の手には追えないかもぁ。スイッチの問題な可能性もなくはないです。3850 x 3 stack っていう構成だからなぁ。

IOSのupdateもした方がいいから、いずれにせよ、サポートに連絡かな。

高須さんの深のお話

深圳の熱気が伝わってくる感じで面白かったです。

ハードウェアを作るのに、日本だと一億円、深圳だと500万円的な。

中国の中では良いが、世界に売ろうとすると「特許たくさん取ってクロスライセンス」とかやり始めるらしい。

大衆創業万衆創新というのを中国政府が推進してる

などなど〜

参加した学生が少ないのが残念だな。深圳にハードウェアを発注する授業とかやりたい気がする。

https://www.facebook.com/events/2206294419606775/

Agda と格闘中

同じ所廻っているような気がする〜

やっぱりドキュメント読まないと。

https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html

と思ったら、今使っているのは2.5.2なので既に古いらしく。2.5.3 からとか書いてあって。

まぁでも、

　　brew update
　　brew upgrade agda

ですむから簡単ですよね。と思ったら、

　　illegal byte code

はぁ? ちょっと困りましたが、

　　~/.agda/libraries

に library の場所が、そのまま書いてあるのか。これを

　　/usr/local/Cellar/agda/2.5.4.1/lib/agda/standard-library.agda-lib

に修正しろと。そう、brew upgrade agda が表示してました。

ω automaton で n 番目みたいなのを証明しにいくわけなんだけど、こっちは n, n-1, n-2 ... 1, 0 と推論するんだが、
ω automaton の計算の方は 0, 1, 2 と進んでいく。その辺が、うまく揃わなくって。

まぁ、そのうち、なんとかなるでしょう...

Java Kuche Agile 勉強会

土曜日の話ですけどね。Agile は

　　理解はできるが習得は難しい

というものらしく。何回か講演もあったし本読んだりもしましたが、なかなか。

大学の研究室だと学生のテーマは一人一人別々だったりするから、少し状況が違う感じ。

でも、アプリやフレームワーク作ったり、あるいはGCC/LLVMをいじる時には意識してはいます。

今回は、ゲーム二つ

　　紙飛行機をたくさん作る
　　コインの操作のタスクの粒度を変える

みたいなのがあって楽しかった。自分でやってみて数字がでるので説得力がある。

この数字で評価するというのもAgileの一つの柱なわけですが、プロジェクト全体を単一の数字で計ってしまうとダメな方向にいってしまうらしい。

最近流行りのTEAL組織の話もちょっとだけ出てきました。まだ、本読んでる最中ですが、この手の本の通例で、うさんくさく始まるんだよな... 読みきれるのか?

飲み会の方でもいろんな話が聞けて楽しかった。専門用語よりも、もう少しざっくばらんな感じでお願いします。

プログラミング能力の基準として「三ヶ月三千行ちゃんと動く」みたいなのを使っているんですが、行数は古いんじゃないかとか言われました。じゃぁ、これに変わるものは何かな。何かいいものあります?

トップを狙え

なんか、3やるって話があるんですね。2、まだ観てない。なので、1から復習しました。2はまだ(しつこい)。

いや、面白いほど、

　　まったく憶えてない

最後のシーンは、いろなところで引用されるので憶えているわけなんですが。こんな話だったけ。つうか、こんなに乳首でるアニメだったっけ?

シャトルはサンダーバード型なデザインで、ワープエンジンはヤマト型と。三角形なのはスターウォーズの影響と。わかりやすい。

話の広げ方とか父の使い方とか王道だしな。

憶えてないのは前回観たのが20年前だからではないかと。何回か録画しなおしてるはずだけど、毎回観るようなことはしなかったみたいだな。

インターステラーでもブラックホールネタを使ってましたが、まぁ、そういう設定だってだけでさ。Sci-fi のSciは「お約束な科学」なので。

背景のポスターネタが面白いので、見直す人はそこを中心に見ると良いかも。借金返すためのOVAだったみたいだけど、作る方が楽しんでるのが良いね。

https://amzn.to/2QhAbee

Casio FX602P

学生の頃、良く使っていたプログラム電卓FX502Pの後継機ですね。iAppにエミュレータがあります。

エミュレータのプログラムのsave/loadが良くわからなかったんですが、本来はdropbox経由でなんとかするものだったらしい。
mode 3 にして、save とか load とかのボタンはあるんですけどね。
でも、dropboxのAPI変更で動かなくなった。なるほど。

なんですが、

　　液晶の部分をタップするとSettingにいけて、
　　そこのFilesにプログラムがある

なんだ、そこかぁ。で、そこの i ボタンから、

　　メールで自分に送れる

おお、なるほど? そうすると、

　　*.pf

というバイナリストリームと、HTMLなListが得られるという方式らしいです。

で、それをメールでiPhoneに送りつけると、エミュレータで開けることができる。はいはい。

というわけで、プログラムのやりとりができるようになったみたい。

バイナリストリームは割と簡単な構造なはず。アセンブラ書くのも難しくないはずです。昔、Prologで途中まで書いたような記憶があるが。

FX806Pは232Cが付いていたので、そこからプログラムを抜き出していたはず。それで書いたものも、どっかにあるはずだが...

PROGRAM LIST
*** P0
x=0
MAC
LBL9
AC
5
MinF

% xd.pl 20235.2.octet-stream
file size 000000f8
00000000 400e0000 00000000 006c8e29 fa1bf10c
00000010 b7674361 8a5c4362 5a0b0a0a 5e688a8a
00000020 43b18a5c 43b25a0b 0a0a5eb8 8a20785d

バスと Java Kuche イベント

台風の次は地震ですか... 沖縄は平常運転です。

9/8に イベントあるんだ。見落としてました。えーと、この場所は... 宜野湾バイパスのあっち側ですか。28のバスの数本が通るかな。タクシーかな。

道はいろいろできるんですが、バスの路線が追いついてなくて。今年できた海上道路にバスが通るようになるのはいつだろう?

琉大も90が何本か琉大経由になってくれると良いんですけどね。中部商業はバスのすれ違いは厳しいが。

日本酒試飲会

日本酒強いん会、日本酒死因会? まぁ、間違ってはないない気もするが...

那覇のサンパレス球陽館でした。サンかぶってるんだけど。酒造さんがだいたい二つずつ持ってきているが、

　　二千円で10回分のチケット

なので、全部は飲めないわけですけどね。カナとだいたい「これどう?」みたいな感じだったので二倍は試せたはずです。つうか、

　　試飲会なんだから、いっぱい注ぐのはやめて

でも楽しかったです。黒龍、〆張鶴、貴とかの有名所から、「埼玉のローカルな米の銘柄なので知らないと思うんですけど」みたいなものまで。

お酒強い女性は独特なオーラがあって面白いな。

復旧作業続き〜

やっぱり、朝、9:20ぐらいに再度書き換えられてました。どうも、

　　theme/*/functions.php

に実行すると、theme/*/functions.phpをすべて書き換えるコードが入っていて。scan-dir とかする極悪さ。

それは一応落としたんだけど、

　　theme/*/functions.php

のmodeが 666 。いろいろやられているっぽいです。

また、明日まで様子見だな。

また、少しイベントがあるようなので、少しアナウンスしないと。もっとも、

　　学生は夏休みで大学はすかすか

なんですけどね。

復旧作業

昨日は三人でワイン4本空けたらしく。飲みすぎで気持ち悪かったけど二日酔いはないみたいです。

学科のWebサーバは、まだ、点検中。

　　yum update してない

ダメじゃん。

　　maria db が10.1 ( 最新は10.3)

ダメじゃん。

worcpress plug in の方は authenticity check でチェックしましたが、

　　そもそも、admin check をskipするコードがかなり昔から入っていた

って、ダメじゃん。

で、vuls でcheckするわけですが、

　　vuls のCVE指摘が減らない

ってダメじゃん。

というわけで、もう少し時間がかかりそうです...