雷の後始末 1

どうも、建物直撃だったらしく、

　　1) ケーブルモデムはおしゃか(ランプ点灯せず)

なのだが、

　　2) それを交換してもらっても接続できない

Air Mac Extreme のWAN port がいったか? で、

　　3) QNAP側で受けて

と思ったんだが、接続までできたが、ip forward してくれない。あれ〜という感じで

　　4) Air Mac Express と交換

なんだがだめ。なので、サポートに電話してやってみると、

　　5) お、つながった

なのだが、またダメ。そこで iPhone からはつながるが、MBP からはだめ辺りでわかったんですが、
3の時に DHCP の gateway 設定を外のにしてた。いや、NATなアドレスを指定するんだよ、わかってないな〜

で、そこで QNAP のDHCPを止めてなかった。なので、

　　どっちを取るかで動いたい動かなかったりした

QNAPのDHCP 止めたら Express で接続できました。 Extreme と接続できなかったのは、どうも、

　　6) ルータ接続に使っている短かいLANケーブルがだめ

らしく。いや、昨日まで使っていたんだけど!? なので、もしかすると、Extreme も生きてる可能性があるな。

でも、怪しいケーブルがいくつかあるので、

　　7) ケーブル買いなおした方が良い

さらに、BDレコーダも動作はするが、面画でない。2台とも。というわけで続くようです。

かみなり

なんか、梅雨が長引いていて...

中部を中心にかみなり落ちまくり。

で、どうも、夜中の3時にうちの電柱に直撃したらしく。他のところはなおったのに、

　　うちの建物だけ復旧せず

もっとも3時くらいには復旧したんですけどね。

でも、

　　ケーブルテレビのインターネットモデムはお亡くなりになったようです

あらら... モデルが死んだのは5年ぶり2回目か? 他の被害は調査中だが、だいじょうぶっぽい。

SSDの価格の予測

もはや D がなんだったか意味不明ですが、

　　そろそろ大容量でも SSD が HDD を抜きつつある

というか、5千円以下じゃ、商売にならんよな。

なんか HDD で 50TB が出るとかいう予測もあるらしく。ただ、

　　SSDの方が長持ち

という話も。HDDは2-3万になるとそれにする的な使い方してますが、

　　M.2 x 4 で 3.5inch ベイにささる

とかにひかれてます。今年はやらんだろうけど。M.2 といっても、いろいろあるらしく、

　　またかよ

感もある。でも、1万円 x 4 をさすとか面白い。M.2 2TB 1万円とかになるのは来年か?

もっとも、最近はむしろ値上がり傾向?!

20年前に課題で「SSDはHDDを抜くか」的な課題を出したけど、割とゆっくりだった気もしますね。

New Orleans

普天間でいご通り、サンエー横。

　Ganbo

とか書いてあるので「ガンボ」って頼んだんですが、アメリカンなサイズとは言えんな。

カーペンターズのジャバラヤにも出てくる食べ物ですが、米国っぽい雑な食べ物でもあるかも。

ジャンバラヤもそうだけど、あの歌はいろんな食べ物が出てくるよな。

オーナーは「にへーでーびる」とか言い放つ黒人のお兄ちゃん。チキンプレートみたいなのがメインなのかも。

Wifi ありでした。

まつぼっくり公園

ここ一ヶ月の雨で崩れたらしく通行禁止に。まぁ、たいした崖でもないんだが...

公園は ingress の要衝なので、定期的に回るわけですが、巡回路の一つが閉鎖されるのは残念だな。

もっとも、この道、途中に板があって、そこで滑って転んだことが一度ある。

ここは、もう一人、active な青エージェントがいるので、割といじされてるので、そういう意味で要衝ですね。

ユークリッドの互除法

√2 が無理数な証明には n^2 | 2 なら n | 2 ってのを使うわけですが、2 で証明するのは、まぁ、難しくない。

2でなくて一般的な素数でやろうと思うと良くわからない。ぐぐったら素因数の一意性を使うとか出てくるんですが、

その一意性の証明ってやさしくないよね? と思ったら、

　　ユークリッドの定理 素数 p なら (n * m) | p → (n | p) ∨ (n | q)
　　ユークリッドの補題 a x + b y = gcd x y

ってのを使うらしい。これを証明するのに素因数の一意性を使ってはいけませんなわけね。

で、これを証明するには互除法を追っていくことになるらしい。

すると、やはり、Hoare Logic 的に不変条件を持ち歩くということになる。

結局、プログラムの正しさの証明に戻ってくるわけね。

Agda で書いてみたんですが、整数使わないとだめだな。整数の利点は a - b で a > b を確認しなくて良いところだな。

まぁ、既にライブラリにはあるので、練習あるいは証明法の確認みたいな感じです。

VS Code

まぁ、あんまりなじまないエディタだがな。遅いし。普段使いは、emacs + viper だったりするので、いろいろおかしい。

Mardkown で数式書いてもらうんですが

　　New File だと markdown preview mode にならない

ぐぐっても良くわからなったんですが、

　　command palette というコマンド検索があり、そこで探せと

いや、New File した時に聞いてくることもあるんですよ。聞いてこないこともある。

学生が使ってるのを見てると

　　マウス/パッドで

まぁ、そうなるよね。なので、遅い。まるでスローモーションを見ているようだ。ま、自分もそんなに速いわけではないが。

元のキーバインドを見ても、ろくなものないのね。その辺は学習コストたかいので仕方ないのかもしれないが、IT系だとちょっとな。

この辺のショートカットとかTipsとかコマンドとか


　　覚えるのがめんどくさい

みたいな人がいるのは残念感じ。

https://vscode.readthedocs.io/en/latest/getstarted/keybindings/

どなん

昨日はお客さんがゼミの後で来てくれたので、お客さんは車できたので飲めないにも関わらず

　　どなんを開けました

まぁ、大学でお酒を飲むなというルールはないらしいのだが、

　　監査の時に表に出しておくのはやめてくれ

まぁ、そうだよな。自分はあんまり気にしてないんですが。どなん60度は自分が好きなのをしっている学生がいるので、

　　たまに卒業する時にくれる

うんうん。わかってるよね。沖縄で買う分には、そんなに高いお酒でもないし。で研究室にはあるのだが

　　学生と飲むより、シラフでなんか作業した方が楽しい

からな。

一時期は、これをキープで置いていたんですが、最近は、キープはもっぱら菊の露ブラウン。それも、

　　このご時世なので

でも、さすがに家飲みに菊の露ブラウンは残念か。

暇なので夜、缶ビール(恵比寿派)開けちゃうのが、少し残念な感じであるな。晩酌すると夜が早くて。

まぁ、でも、どなんは楽しいな。

検診

不真面目なので、かなりさぼってます。なんか Google Drive で予約とる方式になってる。が取れなくて放置してたら

　　開いてるから取れと

バグってたか、まだ、開けてなったかどっちかだな。

前回より3kgほど体重が減ってますが、それだけだな。検尿と心電図と血液検査くらいか。あと視力と聴力とレントゲン。

これくらいの手抜きなのが良いかも。がんがん検査して見つけるのが良いかというとそういうわけでもないらしい。

レントゲンの人にコロナとか見つかりますかとか聞いたら「たまにね」。大騒ぎしてるほどの比率ではないんだよな。

West Field Cafe 復活

めでたいが、がらがら。

お酒出さないだけで、そんなにがらがらになるですか。自分的には

　　一律に根拠のない基準を全国に当てはめるより
　　いろいろばらばらにやって、うまくいったところのを使えば良い

と思うわけですけどね。Teal 的な自律性が多様性と可塑性を広げる的な。

僕は、お酒なくても平気。そもそも悪酔いしなければ、普段とかわらんし。

　　普段から酔っ払っているような奴だからな

飛行機雲

夕方だったから、光って見えるのだな。動画で取るべきだったが、少し急いでいたので。

普天間からはジェット機はあんまり飛ばないです。オスプレイもヘリモードでなければ、それほどは。

嘉手納はジェット機がうるさいのだが、基本、海に向かって飛ぶので、まぁ。普天間は、なぜか、市街地に向いてるので。

Agdaの証明法

素数が無限にあること証明はゲンツェンの最初の記号論理的な証明の例なので由緒あるものなんですが、ちょっとやってみてるけど

割とめんどい。ちなみにWikipedeiaはまともなんだが、それがいがいのは割といい加減なのが多いみたいです。

　　n と n + 1 は互いに素

みたいなのを使う方法もあるらしい。でも階乗使う普通の方法で。

その中で、n! は n 以下のすべての数で割きれるっていう簡単なのがあるのだが....

　　すべての数で割きれるってので再帰する必要がある

「n<mのすべてのnで割きれる」という関数を再帰で作る的な方法を最初に思いつくわけですが、

　　何で割り切れるかを返す関数
　　それで割きれる証明を返す関数

と二つ作る必要がある。良くあるパターンなのだが、

　　二つの関数を同時に展開して、展開した形になって欲しい

わけですが、ならないことが良くある。場合分けが重複してたりするとか、with での仕分けとか。これはλ計算の理論の範囲外ではあるけどね。

まぁ、何か研究があるとは思うんだが、Agda にはそれを制御する方法ないらしい。

割きれるという record を作って、それを再帰的に作っていくという方法がある。それだと割と簡単。 一種の分割統治かとも思うけど。

平行展開みたいな方法はだめな方法らしい。自然ではあるんだけど。

あと、もう少しだが GCD 側でやり残したものがあるっぽいな。
　　

ひとなべ

行ってきました。レジは無人だが、注文とかは人がいるわけね。

でも、ここ一月は、珍しく梅雨の大雨で、入り口にバリアが。

まぁ、狭いが、MBP を広げるくらいはできます。

基本はしゃぶしゃぶなんだな。1200円から〜

となりは 88Jr 。最近は肉は余ってる感じなのか質は良い。

母の車

母が倒れた時に、シーマ(初代じゃない奴)は車検だと部品作るんで何十万とか言われたので処分してしまったんですが、

最近ちょっと、シーマのリストアの話が出てたな。バブル車で「父に買ってもらった」みたいなのが点数高かったのかも。

確かに良い車だったかも。母とのLINE面談の時に車の写真の検索して楽しかったです。

　スバル360

後ろに乗せられて富士山に登ったことがある。車が嫌いな原因の一つだろうな。

　 コロナ
　 マークII

この頃はトヨタだったらしい。

　　ケンメリ

これも、また、後ろに乗せられるには最低の車でな。でも当人達は楽しかったらしい。

母が免許取ったのはこの頃なんじゃないかな。その後は日産が続いて、グロリアとか。最期がシーマだったわけですね。

シーマは94-09だから、15年も乗ったのか。

もっぱら、ゴルフ場までの送り迎えに便りに使われていたようです。

おうちでオリンピック

遊びじゃなくて仕事でやってるんだから、やれよってな立場です。

大学だって遠隔で対応しているわけで、オリンピックだって可能。そこで不要不急だからやめろよというの?

観客動員したい人たちもいるようだが、IT技術あるんだから使えよってなところですね。

もはや、大都市への集中、人が集まること自体が、リスクだということだな。

世界選手権のいくつかにオリンピックという冠を付けるくらいでも。

昔は発展途上国のインフラ整備の口実的な役割があったかも知れないけど、今は集中開催自体がださい感じだな。

夕食〜

まぁ、別にお酒飲めないのは良いんですが、

　　19時ラストオーダー

ってのが生活パターンに全然合わなくて。一人飯が割と好きだったりするので

　　West field Cafe

を使っていたんですが、先週から閉店。お酒だせないと開けてても仕方ないですか。

沖縄は予定だと6/20が緊縮明けだが、

　　開けたら、みんなで飲みに繰り出して、また、感染が増える

というわかりやすい展開だな。もっとも6/7月は気温の関係か減るものなので、それに期待したい。

ワクチンもあるしね。僕は反ワクチンみたいな反社ではないので、打てるようになったら打つ予定です。

東京の母は6/20とか言ってたかな。施設だとそんなものなのかも。

自分は10月以降かもな〜

中庭の置物

そこ? 台風来たら落ちて割れるだけかな。

誰だよ置いたの。

BigSur の Photos.app 解決篇

いつもの Photos.app の内蔵DBの変更ですが、

Pictures/Photos Library.photoslibrary/database/Photos.sqlite

をなんとかすれば良くて、

　　my $sql = $mdb->prepare('select * from ZASSET , ZADDITIONALASSETATTRIBUTES where　ZASSET.Z_PK=ZADDITIONALASSETATTRIBUTES.ZASSET and ZDATECREATED >= '.$after." order by ZDATECREATED");
　　$sql->execute or die("db error $sql->errstr");
　　while (my $photo =　$sql->fetchrow_hashref ) {
　　　　 my $filename = $photo->{'ZORIGINALFILENAME'} ;
　　　　 my $imagePath = "originals/".$photo->{'ZDIRECTORY'}."/".$photo->{'ZFILENAME'} ;

これだけでした。Z_PK ってのは表のキーに全部同じ属性名付けてるのか。まぁ、IDとかつける人いるしな。Primary Key のこと?

で、他の表のキーには表の名前をそのまま付けてるのか。普通 attr_id とかすると思うんだが。

なんか名前の重複を処理しないなと思ってデバッグしてたら、本当に同じファイルが複数DBに入ってた。

さすが、クソアプリ。写真の重複判定しないのね。もはや読み込みにしか使ってないです。

オートミール

イギリスにいる間はあんまり食べなかったんですけどね。どちらかというとシリアル派。それも最近はあんまり。

カップなオートミールは戻る時間は早いらしい。そのままでも十分早いとは思うが...

中身がとっても少ないらしい。

　　お茶漬けの素を入れると日本人には良いらしいです

マトリックスのネブカド号でネオを食べてました。ま、何も入れないと無味無臭だからな。

呪術廻戦

アニメの方だけ。なんかエンジンかかるの遅い話ですが、回り始めるとパターンになってしまう...

まぁ、こういうのもたまには良い。

ブリーチっぽい感じではあるかな。

そういえば、ブリーチは、途中で落ちたままだな。366話もあるんだよな。いつか観るかもしれないです。

シドニア

アニメの映画です。今回もサザンプレックスですが、車に乗せてもらえたので楽勝。

原作は終わってて、もともと、ぬるいハードSFよりなスペオペ的なもの。映画も甘い仕上がりでした。

で、

　　あのフォント欲しいな

と思ったんですが二万二千円。え〜。7700文字TrueTypeかぁ。NEXTSTEPもりさわフォント付きよりは安いが...

最近だとAIで自動生成と思うが、そういう研究はやまほどあるらしい。が、

　　お金がかかるのはチェックの方

だろうしなぁ。Unicode encoding に変換するのか?

https://iwatafont.co.jp/toa/

Hombrew / LLVM12 / GCC

brew に詰めるってのをやってましたが、なんとなく

　　mojave/catalina/BigSur/BigSurM1

と用意して build したけど、もしかして、xcode のselectでBigSurだけでできるのかな?

　　==> Detecting if cbclang--llvm10.big_sur.bottle.1.tar.gz is relocatable...

に妙に時間がかかる。そういうの ruby でやるのやめて。やんなくて良いんじゃないの?

なのだが、LLVM10からLLVM12もついでにやるかと思ったら

　　github の位置がずれてる

LLVMはSVNだったんだが迷走の結果 github になってみたいね。ま、仕方ないか。とかいいながら

　　hg に焼き直して使う方式

です。少し引っかかってるが、コード生成系をこの前のでほぼスキップできるはずだが...

GCC側も上げるんじゃないかと想像します(他人事)。去年の今ごろも同じことやってたらしい。

ただ、Ubuntu の apt の作り方がわからない。rpm じゃあかんのか。

ディスクキャディ

リースバックで買い取った Dell R630 にディスクを追加しようと...

が、しかし、適当に買ったら

　　R740用を間違えて買ってました

形ちがうのか。なんか縦線が余計で入らん。なのだが、

　　キャディなくても刺せることは刺せる

ひどい。なんか、ここでくださいといえばもらえるような気もするが...

たいした値段でないんですけどね。

なんか結果的にがっつり ingreess

普天間の反対側のキーを取るわけですが、そこから、2/3回ってさらに反対側に。

そしたら、那覇に出ることになり、ゆいレールの終電で前田から

　　貸し自転車

なのだが、そういうことをすると

　　あそこによって、ここによって

雨も降ってきてるのに。しかも、

　　下手なので壁にすったり、立ち転び

とかで上着がぼろぼろに。少し高くついてるな。

まぁ、広く取れたから。いや、まぁ、いろいろあったわけですけど、あえて書かないことにします。

LLVM Clang compile from string

ちょっと苦労しましたが動きました。CurLexer と CurTokenLexer とあって、

　　Lex して MacroInfo にためたToken stream を CurTokenLexer が提供する

感じ。なのだが unique_ptr で、CurLexer が消されてしまう。なので、新しく作った TokenLexer と sawp 方式で。

まぁ、C++ 一つ一つの仕様は必然性があって便利に作られているんでしょうけど、

　　あとから全体を見ると狂気にしか見えない

そんなものだな。でも、

　　 CompileFromString("int env_buf[64];",CompoundStmts);

とかできる。これで全体を書き直すと、かなり短かくなりますが、

　　まぁ、そこまでやらなくても良いかな

少し盛り上がりに欠けるけど。

この部分は優秀な学生が書いてくれたんですが、優秀な学生にありがちなんだが、

　　書き過ぎ

なんだよね。書き過ぎたら「他の方法があるはず」と思った方が良いらしい。そのOBに見せて自慢したい気もします。

玉城先生そろそろ一周忌

学生部屋通りかかったら、玉城研の博士な学生が。遺影ありますよとか。

そういえば、死因聞いてないんだよといったら、

　　もともと肝臓悪かったんだけど、転んで打って...

う、やっぱりそれかぁ。自分も言えた義理じゃないんだが。やっぱり、

　　ほどほどに長く飲もうよ

と思いました。昔ほど強くないしな。もっとも、自分をお酒弱いと思っているようなのが周りにはたくさん。

板書な先生だったのでオンライン授業はストレスだったかもな...

お酒だせないと閉めてしまうお店が多いんですが、いや、

　　おいしい水でも良いんですけど

お酒が悪いわけじゃないにとは思いますが、酒飲んで騒いでいる人たちが多かったのはその通り。

それでも開けてるお店はありがたい。

夕方は激眠かった

llvm/clang のをZoomで続きやってたんですが、なんか眠くて。

　　話しながら、寝ちゃうのね

なので、少しお休みしてました。別に前日、遅くまでやってたわけでもないのだが。

圏論は2013から

なんか灘高の圏論入門みたいなのを見かけて。そういえば途中だったなで始めたみたい。

最初に触れたのは吉田研の出口さん関係の勉強会だったはずです。層圏トポスで米田関手までだったかな。

最初は本の余白(と言ってもA4にコピーしたので割と広い)でやってたんですが、全然足りない。

今でもそうですが twitter で書きながらなので教えてくれる人とかいて面白い。

で、TeXのtikzとかでやってたんですが、そういえば証明支援系あるよなで、Coq から Agda という流れ。

最近は結構見かける感じ。証明の視認性はCoqよりはAgdaが良いかも。論文とか整理されたAgdaのsiteとか。

ただ、Topos までやってるのは見かけないかな。特に Sets との関連はかなり面倒なのだから。

圏論は集合論の直観で展開している本が多くて、竹内先生のもそうですが、Lambek/Scott は圏論のみにしたいらしい。

けど、それでも一部集合論が出てくる感じ。その辺も寄り道したのでだいぶわかってきたかな。

　2013 クライスリ圏
2017 随伴関手定理
2018 CCC
2019 ZF
2020 Galois
2021 Topos

学生時代にこういう読み方ができると良かったなとも思うけど、今の復習も楽しい。

LLVM clang

今年もそんな季節か。今回のお題は buitin_longjmp の inlcude file を消すことですが...

　　string を C のソースとして見てコンパイルする関数をつくれば良いんじゃないか?

ってことで、いろいろやってるんですが...

　　Macro として扱えば。EnerMacro っていうのあるし。

なのだが、判明したのは Macro は既に Tokenize されてる。そういう実装なのか。なので、

　　Macro に突っ込む前に自分で Lexer を通す必要がある

というところまでわかりました。

GCC側も同じことやるか? いや、まだ、LLVM側ができるかどうかわからんのだが。

サザンプレックスまでの道のり

車でいくと西原インターから南風原インターまでなので16分なんですけどね。

　　そこに高速バスはない

なので、那覇インターで乗り換え可能らしい。そこから20分あるく人もいるらしいですけど。

191馬天行きってのが一日7本。それで南部保険センターで降りると、AEONを通り抜けていけるみたいです。

33とかで真玉橋経由もあるらしい。