Twitter CLI

いや、Perl で書いたのがむかしからあったんですけどね。

　　当然のように動かない

最近は、Perl の module は cpm で入れるんだが、こける。

　　openssl header がない

なるほど。brew install openssl が良いらしい。Net::Twitter は少し API が変わってましたが、動きました。

でも、まぁ、使わないよね。なんのために入れてるんだか。

では、よいお年を。

○○ Bar

いや、別にいいんですけどね。こういう開き直りは嫌いじゃない。

年末進行

といっても、呼び出されて飲みまくってるだけですが。

今年はzornの補題な年だった。できてよかったが。チコノフの定理とか可算モデルとかもできそうな。

それはゆっくりでいいかな。OSの採点とかしてるはずです。(つうか、それをやれ

カレンダー

あんまりスケジュールとか関係ない人なんですが、この前からカレンダーの管理が死んでて。

いや、Google Calendar でいいだろとも思うんですけどね。

　Web上の main.ics を生成して読み込ませる方式で、それをみて cron でメールを送る

みたいな方式で、30年前からそれだったりするんだよな。

Perl script で重複を消すように調整して、/usr/bin/mail を mhmail にしてとかやってたら動いたので、まぁ、いいかな。

　grep -l new ~/Library/Calendars/*.caldav/*/Info.plist

とかすると、Calendar.app の new という予定を取れるらしい。割と変わってない。

可算モデル

Zornの補題終わったので集合論みなおしてたんですが、01の可算無限列の順序を選択公理を使ったZornの補題で極大フィルターを作ってで証明するんだが、選択公理は整列定理と同値だから、それは仮定そのものだなと思ったり。

で、Power/Unionを見直して、もっと簡単な形で良いことを発見したりしたんですが、

　　可算順序数と Power ωは両立しないよな

とか考えて困ってたんですが、そもそも集合論の可算モデルって何? ってことに。レーベンハイムスコーレムで可算集合に落とすんですが...

Mが可算モデルってのは、集合論のモデル、つまり公理を満たすことを証明する時に使う値に番号を付けるみたいなものだなと。

対角線論法でも、確かに Power ωから可算個対応させて、ほら別にもう一個あるでしょで、Power ωの中の可算個しか使ってない。

Mが含まれてるZF全体の集合のごく一部がMに入っていて、Mがモデルみたいな面をしているだけなのね。

Mは可算だから、Mの中の順序数に対応するものは可算順序数になっていて、その中で Power ωは、やせほそった可算集合でしかない。

でも、それはその中のωよりは大きい。そういうことか。

現場猫案件

まぁ、実害ないならいいんですけどね。

前は、連絡橋の下部の一部が落下したことがあった。

Ingress の裏道

まぁ、歩くためにやってるわけなので。

ここから階段の下の三角を抜けて。昔の太陽市場のところに。

まぁ、危ないところは攻めないようにはしてます。

学生の装備

Fortigate/Yamaya/NEC/Cisco と楽しそう

プロシンのあと、少し東京にいる予定です(1/9-11)

ChatGPT で OS 教科書のの問題を解く

英語の問題なので英語で解答されてしまいますが、日本語でといえば日本語になるはず。

問題は、ABIとAPIの特徴的な違いはっていうShilversharzらしい問題ですが、

　　OSの教科書の問題ってのを知らないから一般的に解かれてしまう

まぁねぇ。要求しているのは

　　プログラマはAPIは探すがABIは探さない
　　コンパイラとかライブラリを作ってる奴はABIを見る

みたいなのだと思うんですよ。まぁ、先生の要求している解答とか教科書が要求している解答を当てるのは難しいよな。

キャベチャー

宜野湾330沿いのラブめんですが、

　　キャベチャー

が登場。200円は高いが、まぁ、このご時世だからな。でも、

　　そうじゃなくて、キャベツを増やしてほしい

というか、キャベツだけで良いんだが。今度はキャベツ多めでと頼んでみよう。

Zorn の補題の Agda での証明完了

いや、3月くらいからやってて、かなり難航したんですができました。詳細はプロシンで話すので興味のある方はどうぞ。

　　record SUP ( A B : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　sup : HOD
　　　　　ax : odef A x
　　　　　x≤sup　 : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -- B is Total, use positive

　　record Maximal ( A : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　maximal : HOD
　　　　　as : A ∋ maximal
　　　　　¬maximal<x : {x : HOD} → A ∋ x　→ ¬ maximal < x　　　 -- A is Partial, use negative

　　Zorn-lemma : { A : HOD }
　　　　→ o∅ o< & A
　　　　→ ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B　 ) -- SUP condition
　　　　→ Maximal A

定理自体はこれだけ。HODってのが、今回使ってる Agda で実装した ZF 集合論の集合。遺伝的順序数定義可能集合(Heritic Ordinal Definable Set)ですね。

Kunen と田中先生の本には載ってるけど、ちょっとずれてる。ってことは、別な集合論の公理をAgda用に作ったわけ。

A上の単調増加関数 f x と、その閉包 FClosure A f x を与える上界関数列 supf x 、そして、それが定義するAの全順序部分集合列 UnionCF A f supf x
と、それらの性質を表す record である ZChain で、

　　全部で 1800行

nvim 上でチェックにかかる時間は5分。agda command だと6秒。なんなの。メモリは7GB。なんだが、ソースコードを工夫したら3GBに。

時間がかかった理由はいろいろあるが、最小上界でなくてもできると思ったのが間違いで、さらに、≤ な関数で fixpoint を示せると
思ったのが間違いで、まぁ、それではだめなのに気づくのに試行錯誤しまくったのがだめだったみたい。

その辺の証明を正確に追うことも可能なんですが、あんまり Agda っぽくないしな。整列集合の切片とかのあれですね。

でも、まぁ、証明自体は岩波現代数学概説に沿っているはずです。

これで、Generic Filter の存在とか、チコノフの定理とかが示せるはずです。

ブラウン管でのプログラミング

なんか学生が研究室にブラウン管持ち込んでなにやら。

　　PALとNTSCってなに?

とかやってる。楽しそうだな。

最初にプログラミングしたのは PC8001 をテレビにつなげてで、目が死にました。

自作のもテレビにつなげてて。父の工場の払い下げのを使ってたっけ。これはビデオ端子なので、それほでも。

でも、大文字小文字は反転で区別してた。そんなんで C とか良く書いてたよな。

安物モニタの方がましだったので、そっちの方を使っていたはずです。

今の 4K でのプログラミングも目が厳しい。

OIXの話

長田先生の置き土産の OIX が、Okit 経由で存在していて、琉大ももちろん接続されてます。

この辺は県が割り込んだりして、残念なことになっているらしい。

　　ネットワークの第ゼロ層の政治層の構築に失敗した

ってところですか。別に波風立てたいわけではないですが、仲良くやって欲しいところですけどね。

プログレ

最近、ヘンリー8世と六人の妻の冒頭だけ練習してるんですが、学生になんの曲ですかと聞かれたので、

　　ラウンドアバウトと、太陽と戦慄 part 2

も一緒に教えました。

冒頭はいいんだが、途中が楽譜が正しくないっぽい。いや、読めてないだけかも。

楽譜読み解って認識するアプリとかないのかな。

4回目

3回目打った後にコロナを食らったので、しばらくおとなしくしてたんですが。既に先週木曜日の話。

宜野湾体育館でがらがらでした。

効果のほどは期待してませんが。ただだしな。コロナは血管系、心不全とかにも関係する話もある。どっちかというと

　　それって長く残るの?

あたりが気になりますが、まぁ、それはこれからわかる感じか。

珍しく、少し注射跡が痛かったし、微熱な感じだった。まぁ、それでも飲みには出るんですけどね。

だから、打つ的なところもあるか。

かばんの修理

雨が降ってたし、少し重かったしな。久しぶりに、カバンの紐の金具を引きちぎってしまいました。

　　少し位置をずらして、ねじを締めなおして修理完了

まぁ、時間の問題だが、代わりのが見つからなくてな。

すずめの戸締り

観てきました。天気の子の別解みたいな感じですね。

東京の風景が懐かしい。お茶の水あたりとか。

予想外に面白かった。あの頃から、みんな成長してるはずだが...

https://suzume-tojimari-movie.jp

RAM

80年代初頭の、

　　ASCII/RAM/IO/Interface

が情報源だったわけですね。それと、Bit Inn に通ってた。

いやさ、

　　命令セットが載ってるだけで、かなりのことがわかる

わけ。RAMは、この他に Micro C が載ってるのも持ってたんですが、なくしてしまいました。

ROM Writer を当時の東工大の助手だった久慈さんが持ってたので

　　いきなり、ビデオとキーボードが付いているコンピュータを作れる

それも、たぶん、売ってるものの半額くらいで。しかも、最新のCPUとRAMで。そういう時代ですね。

それが

　　雑誌を読むだけで、可能だと分かった

今の学生には、また、違った地平線が見えてるだろうとは思いますけどね。

最近の原神

ナヒーダでて、80まで上げたんですが、90にしてから使おうと思ってたが、最後のつめでめんどくなって。

と思ったら、Wwanderer でるのか。育成楽しいといえば楽しいんだけど。

でも、TCG は嫌いなんだよ。勝手に決められたルールの adhoc さがな〜　なので、そっちはさぼる予定。また怒られるか。

FF8の変なミニゲームを思い出すな。

DNSのお話

PowerDNSは設定したんですが、まだ、運用してません。別に怖いわけじゃないんだが。

Akatsuki との設定に少し苦労したんだが、DHCP6 / KEA DHCP との接続とかもやらんとだめならしい。うーん。

ところが、

　　なんか、8.8.8.8 から見える時と見えない時がある

とか言ってるのが。え〜? ちょっと見せてみ。

　　え、なんで、Sakura 上のサーバに対して検索してんの? そんなの聞いてない

で、調べてみたら

　　BIND9の Master で NS で指定されていて、設定ファイルが9月

どういうこと? なんで、Slave じゃないんだよ。で、Slave 設定して終わりなんですが...

　　Master が死んだら Slave のキャッシュはどれくらいもつ?

とかの話が。Slave なのであって Cache ではないんですけどね。SOA Expire ってのがあって二週間くらいらしいです。

こっちの Master/Slave の用語は purge しないのか?

義母との食事

竜宮通りの店を使いました。最近は、東京の妹の家と沖縄の家で、二人で交互に一緒に住んでるらしい。

元気なのは素晴らしい。一緒にいる時間を大切にしたいです。

Roland SC55

どっかで手に入れたんだが、どこで手に入れたかは覚えてないです。たぶん、秋葉原のジャンク屋。

2000年の写真に88Proが写ってる。今のは、やっぱりジャンク屋で買ったSC55。

ガレバンとかでいいんだが、

　　切れてて再起動とかめんどくさい

なんとなく、ふっと手慰みに弾きたい感じだからな。

ちょうど、ハラカミ・レイの話をNHKでやってたみたいですね。道具は使い方だからな。

SC88というとカラオケなわけですが、その安っぽさが、むしろ、

　　バブルのはじけたあとのゴールデンリセッションな時代

に合ってたと思う。

いまだと箱な音源はもう使わないのかも。

開かれた大学

まぁ、動物園なので「危ないのを外に出さない」的な意味もあるんですけどね。鉄条網はどうなの?

立教大学は徒歩の通り道でもあるので、かなり自由に通れる。琉大も車は抜け道に使ってるな。

イギリスのケンブリッジ大は、街中にばらばらにいろんなところを借りてるので、キャンパスって感じと違う。

東工大は幼稚園の散歩場所になっていた印象がある。

東大は終電だと弥生門の横を乗り越えてたな。

建物の入り口でカードとか、あるいは、部屋ごとにとか、いろいろあるけど、

　　大学はむしろ治安を良くするので、敷地はオープン

なのが良いんじゃないかな。

PC8001の思い出

実家から回収したので、どっかにあるはずです。拡張ボードも持ってくるべきったか。

大学二年の時に友人(青柳氏)と半々で買いました。16万円。既にプロ電(fx502p)でプログラミングはいろいろ知ってた。
メモリ32KB。

買って、テレビにつなげて一晩でBASICでブロック崩し書いて「目が死ぬ」知ぬことがわかりました。
で、秋葉原でジャンクなモニタ(裸)を一万円で買ってきてつなげました。友人は嫌がってたが。

この頃はJISキーで特に問題なく。それまでBASICは店頭で動かすくらいだったはず。

で、MS20かなんかのシンセにつなげる DA x 4 + Z80 CTC + Z80 PIO + GPIB な拡張ボードを作りました。
なんだが、MS20って f/v で oct/v じゃないんだよね。なので、シンセの制御はぜんぜんだめだった。がっかり。
リズム出すくらいなら。GPIB は卒論で活躍したらしい。

CTCはROM Writer を back で動かすなんてのに使ってた。で、この上で GAME80 で 6809 のアセンブラを動かして
マイクロマウスを作ったわけだな。 32KB RAMで十分楽しかった。

もっとも、大学三年の時には自作6809の方を触ってたので、PC8001 は実はあんまり使ってない。
なので、 PC8001 の30万円のFDとか、PC8801/PC6001 あるいは MSX には縁はありませんでした。

まぁ、楽しい時代だったかな。自作が安上がりで性能が良かった時代ですね。

PC8001 ミニですか? もう十分遊んだから要らないです。

安物ヘアピン

まぁ、必須なんですが、コンビニ以外だと探しにくくて、適当に買ったら、これですよ。

日本の髪ゴムが異常にもつとかの過剰品質はあるけど、このヘアピンは使い物にならんだろ。

(といいながら、使ってますが

Agdaの証明と論文

まぁ、論文ってほどでもなかったりするんだが、なんと3月からはまっている Zorn の補題の証明をプロシンに出すんですが、

　　まだ、Agdaの方が終わってない

まぁ、間に合うはずなんですが。良くあることなんだが、

　　論文書き始めると整理されるので見通しが良くなる

なので、もっと早く書けば良かった。いろいろ原因はあるんだが、

　　色々細かい選択肢があるが、それのどこがだめだったか忘れて振動する
　　Agda は「とにかく、そこにある記号で穴を埋める」ってのがあって、それに引きづられる

ってのがあるのだけど、文章にするとそれが整理されるらしい。

でも、まぁ、証明は一応つながって「実はあれもこれも不要で小さくなりそう」みたいな段階ではある。

ところが、そこから「やっぱりうまくいかん」ってのを繰り返してたりするんだよな。まぁ、数学者なら

　　Zorn の補題? あんなの簡単じゃん

であろうとは思います。

LuaLaTeX なんだが、STIX font で ⟪ ⟫ がでなくてちょっと困ってます。なんでだ。

最近の ingress

特にがんばってません。自分のまわりの守備範囲だけって感じ。

宜野湾の青のエージェントが元気なので、助かってます。

だめな電子メニュー

和風亭がそんなことに、某N社のですけどね。マクドのとか良くできるのに、どうして、ここまで最低にできるのか。

もちろんん、

　　メニューから支払い不可

そんなものに引っかかるサンエーの経営者が残念すぎる。そして、

　　メニュー番号がないと注文できないが、メニューは給仕に取り上げられてしまう

電子メニューからは追加注文させない仕様らしいです。しかも、紙メニューは死守するらしい。

この手のものを作る会社が全部潰れれば日本も少しは良くなるんじゃないかな。だいぶ潰れたけどね。

長田のそば屋のもひどいんだよな。おなじN社かも知れん。iアプリの標準的なものとかありそうなもんなんですけどね。

テーブルにQRコードがあってメニューはそれだけってお店もあったが、それはそれでさびしいものだな。

もう少しZ80の話

GAME80のdisassembleくらいかけるかと思ったんですが、githubには良いのがなくて。

と思ったら、

　　Typescript base の何かすごいのが

いや、そんなのが欲しいわけじゃないんですけどね。

Z80はPC8001とif800をさんざん触って、ROM witer つけたりしてました。拡張ボードも現存してたが、まぁ、意味はない。

DA converter 4ch で、Z80 PIO/CTC/SIOと乗せてました。

if800はCP/Mで使ってて、EDIT80使いまくってました。でも、GAME80のエディタの方が便利でな。

Z80はLDIRとかが好きだったわけですが、IXとかが遅いのが残念。

6809も日立が勝手な拡張をだいぶ入れたんですが、まぁ、役に立たない。むしろMMU内蔵とかが欲しかったな。

Z80ではアセンブラばかり書いてましたが、残ってない。特におしいとも思わないけど。

6809側はたくさんあって、面白かった。

https://github.com/maziac/DeZog

GAME80

なんか twitter で

　　Z80なBASICを理解したい

みたいな話が。だったら、GAME80がいいよね。Parse が簡単で実行もソース直接だし。

ASCII Ency Vol 3 があるので、HEX DUMP 取り込んでみました。

実行して見る気はないが...


https://github.com/shinji-kono/GAME80.git

cp -al

いや、rsnapshot が、そんなもん使ってるってのは初めて知ったんですが...

-l Create hard links to regular files in a hierarchy instead of copying.

本気ですか。NFS上でも動くんだが、すごく時間がかかる。こういうのってNAS上で動かすもんだよな。

で、問題は

　　それで作った directory をどうやって消すの?

だって、daily.0 とかを rotate するわけでしょ。

　　regular file を remove して、空になったら削除

だろうけど、やってんの? と思ったら、

　　rsnapshot は Perl script で実際にやってるらしい

普通に rm -rf したら負けってのがなぁ....

停電あとのトラブルの続き

停電から復帰して、自分のサーバに入れたから「停電対応、お疲れ様」と返したら、
実は「freeradius が postgress に接続できない」という技を出していたらしく。

　諦めて帰ります

ってのなのが MatterMost に。で、夜中の10時から入って。で、旧 LDAP VM 止めてなおったと思ったら

　朝には「動いてません」

というありがたい御宣託が。で、朝もう一度 Zoom で接続しながら。

　freeradius と postgress の podman に podman exec /bin/bash して確認

なんですが、両方 ping は通るんだが、

　postgress から ping しておきながら freeradius を手動で上げると立ち上がる

はい? route が片方しか通ってない時の症状ではあるだが。そういえば、

　postgress は PowerDNS の時に podman pod にしたんだった
　PowerDNS側は問題ない

なので、freeradius も pod にしたら、

　しばらくしたら動くようになった

うーん。まぁ、freeradius のversion 上げたり、podman を 4系まで上げたりしてたからなぁ。

　動いたから良いか、ってとこです

学生の一人は k8s にすればって言ってますが、その方が IBM が書いてるからましかも知れん。

entrypoint.sh を間違えていた話は、また、次の blog ネタにしよう。

なんかまた停電でトラブってるよ

どういうことなんですかね

大謝名の歩道橋

ほとんど、トマソン化してますが、左から回り込んで登れます。右側はバリケード組まれてる。 別に歩行者のために作ってるわけじゃないからこれでいいんだろうな。 この歩道橋は、二輪の事故の原因にされて、半分撤去されたんですが、58の拡幅でこうなった。 横断歩道もあるのでかなり中途半端。 また、ここから下り側のバス停が遠い。

UbuntuのLDAP認証解決篇

いや、ぜんぜん LDAP と関係なかったんですよ...

1台だけLDAP認証が動かないサーバで、じゃぁ、sssdを podman で動かすかで、

　　git clone で Dockerfile を取ってこようとしたら...

/usr/lib/git-core/git-remote-https: symbol lookup error: /lib/x86_64-linux-gnu/libhogweed.so.6: undefined symbol: __gmpn_cnd_swap

おいおいおいおい。で、ldd で犯人探し。もちろん、/usr/local/lib に、だめな libgmp.so が...

その辺全部消して、sudo ldconfig 、apt-get upgrade して

　　reboot したら、あら不思議、ばっちり動く

だから、

　　怪しいサービスとかアプリとか入れるなら
　　singurarity とかのコンテナの中でやれと

その方が逆に system 側を update してアプリが動かなくなるとかもないしね。

でも、Singularity も身売りしちゃったのか。apptainer とかなんかださい。いや、

　　singularity って名前が無駄に格好良すぎるんだよな

ネギ食べすぎた

野菜がおいしい
ビールと合うし

hugo の tmp dir

hugo 動かないみたいな話があって

　　/tmp/hugo_cache/

を決め打ちしているあほが。もはや multi user は死語か。

すでに、github の issue には載ってるんだが

　　mktempdir 呼び出せよ

というわけですけどね。まぁ、workd aroundで環境変数設定しろと。

最近は、XDG とかいう brain damanged　なのもあるが、その辺含めて、mkditempdir で解決して欲しい。

セブンイレブンのあれ

これはたしかにあかんかもしれん。

ちなみに、パンの耳は不要派。

コンパイラ読み会2日目 Agda

LLVM clang のコード生成部も読んでたんですが、最終的なアセンブラ生成は

　　IRを指定Archのコードに変換するだけ

だったので、割とつまらなかった。いや、Arch毎の命令記述はかなり謎なんですけどね。それはGCCも同じではあるが。

こういう部分ってCPUが自分で用意しろと思わなくもない。アセンブラの多様性とかいるのか?

Agdaの方は、やっぱり

　　Haskell code の読み方がわからない

って問題が。割と苦労して、Agdaの最新コードを singularity の中に構築するのはできたんですが、

　　Traceの方法がわからん

gdb で trace するっていう手もあるらしいが...

ghci で、Agdaの Main.hsを読み込むってのもやってみましたが、できないことはないっぽいが、

　　構文定義の問題があるらしく、いろいろ見ながら作る必要があるらしい。

結局、ソースコードみながら、ここから TypeCheck みたいなのは見つけたんですが、

　　そこが実行されるかどうかは良く分からない

いや、そこここに、liftIO 使った print 文がコメントアウトされてるので、そういうものなのかも。

if [[ -f /singularity ]]; then
prompt="%S+%s%m%S+%s$SINGULARITY_NAME:r%S+%s%n "
tty= $SINGULARITY_NAME:r
fi

みたいなコードを入れると singularity とそうでないのを区別できてよいらしい。

コンパイラ読み会

LLVM clang をなぜか debug flag を忘れてて。良くある。

Agda の方も、lua 入れたり、.agdai 生成したりで、まぁ、苦労してます。

読む方は、Stacktrace を down しながら。ちょっと安易かな。

まぁ、でもこんなもんか。明日は agda 読む予定です。

Agda の compile

compiler の読み会で使おうかなと。

singurality でやるんですが、LLVM/clang は楽勝だったのが... (CbC merge はまだ)

agda が全然できない

　　そもそも Ubuntu の ghc / cabal が古すぎる (GHC 8.8 / cabal 3.0)

いろいろ試したんだが、

　　結局、https://downloads.haskell.org から tar ball を持ってくるのが早い
　　ghc-9.2.4 cabal 3.8.1

という身も蓋もない話らしいです。

いや、Agdaの ghc build が 1.5Gもメモリ食ってるんだが...

できんのかこれ。

Ubuntu の LDAP認証

まぁ、鬼門なんだよな。radius使えよって話もあるみたい。今日のお題は

　　旧サーバ3台(Ubuntu 22.04)のうち一台だけが LDAPのユーザを認識しない

lastを見ると、22.04 にあげた9月以降 login できてないらしい。どうも、

　　その一台だけが nslcd (ldapのキャッシュ)が設定されている
　　その他は pam_ldap.so だけ(sssd なし)

らしい。さらに、

　　apt-get update がこける (これは、apt purge fish で解決)
　　pam_ldap.so がないといってくる ( /usr/lib/security と /usr/lib/x86/securityの違い

ここまでだと、他の二つが動いている方が不思議なんですが。

たぶん、ldap関連で nslcd とかがハードコードされている package とかの問題なんじゃないかと。つまり

　　nslcd とか、もはやメンテされてない

まぁ、そうだろうなぁ。sssd 設定するしかないか。それで動く保証はないんですが。

　　じゃぁ、他のが動いているのはなんで?!

個別に slapd 動かした方がよいという説もあるらしい。そうでないと起動時にこけたりするので。

久しぶりに LLVM clang update / コンパイラ読み会

まぁ、毎年やってるんですけどね。git でやってもいいんだが、git -> hg で。

　　hg add

したあと、移動または消されたファイルを hg から削除するんだが

　　hg status から　! なのを抜き出して
　　cat /tmp/aho | xargs -L 100 hg rm

なるほど。一つ一つだと結構遅い(7千くらいある)ので、-L 100 で100個ずつ。

あと、

　　hg merge -r 237 --tool internal:other

ってのがあるのね。便利便利。

vim の three way merge を勉強するべきかとも思うが、

　　その程度の patch なら、それでもいいが

それでは全然手に負えないわけで... 修正は明日明後日かな

ってなのを、コンパイラ読み会で、

　　土日、10:00-12:00 14:00-17:00

でやってるはずです。今回は

　　LLVM clang
　　agda

のはずです。

またバックアップが〜

どうも、9月に手動でバックアップしたあと放置でいままで...

　　rsnapshot.conf

いて、cron 入れるだけなんだが。油断するとこれだよ。

さらに、貸出VMのDisk容量が危ないらしい。

いろいろゴミを消して 500GB くらい確保したけど時間の問題だな。どうも、

　　古いのは消していた

らしい。まあ、学生のだからそんなものだよな。

ハペ学会

爬虫両生類学会らしいです。琉大っぽいな。

球陽池にはいろいろいそう。

Herpetological だからか。

琉大周辺の道

これが、こうなって、こうなる

ちなみに、途中には Ingress のポータルが...

いしぐすくのあたり

GothicMade

FSS おたくではないんですが、そこそこは読んでます。2012 は東京に行く機会はあったが見れなかったんだよな。

沖縄の桜坂で十日間特別再上映。沖縄が入るのは珍しい。

　　IMAXとかだと逆に上映できない

という不思議な映画だからなぁ。

　　しかし、桜坂のBホールのスクリーンは小さすぎる

でも、

　　あの雨がデジタルじゃないとか本当?

遠景に巨大戦艦とかだと、3Dだと良いのにとか少し思いました。

話が単純なのは良いね。第三皇子いい奴すぎる。 暗殺部隊があっさり引き下がったのは納得できん。焼き払うとか言ってたくせに。

あの話の断片の一つ一つにこういうのがあるのだろうな。

それほど思い入れないので、エンドロールが重要なのはわかるけど、あんまり良く分からず。
ターボ音とかがクレジットに入ってた。

まぁ、でも、楽しめました。

https://gothicmade.com

Perl Homebrew cpm

Homebrew で Perl を update したら、また、Tk が。そろそろ Tk やめろよとも思うんだが。

　 cpm install -g Tk

とするらしい。-g が思い出せないんだよ。NKF.pm が cpan にないのは誰かのせいなんだが、いつも手で入れてる。

　cd ~/src/nkf/nkf
　git pull
　cd NKF.mod
　perl Makefile.PL
　make
　make install

マクドで

いつもサラダにしているので、ドレッシング(玉ねぎ)をかけて、

　　ビッグマック食べてからサラダ

ってしたら、ドレッシングがかかってない。あ〜ん?

　　どうも、アイスティーのふたをあけてミルク入れる時にやらかしたらしい

まぁ、混ざらないのでかき混ぜなければ問題ないみいたです。

ストローとスプーンが紙と木になってました。別に問題無し。

でも、子供の頃は

　　紙パックの牛乳はぺって吐き出す

やつだったらしいです。あの四面体のやつだな。

数式処理

Mathematca に憧れた頃もあったけど。Markdown で数式を扱うのは Markdown+Math が簡単。

VSCode で preview もできます。でも、

　　チェックとか変形はしてくれないです

まぁ、綺麗で楽しいのだが

　　速いかというと、そうでもない

コピペを駆使するわけだが、それでも時間はかかる。

Agda でいいじゃんというところもある。でも、

　　わざわざ数式にするか? プログラムでいいでしょ

的なところもある。証明しないで

　　清書するだけでも良いかな

遅いのは

　　いちいち詳細まで記述しないとダメ

ってなところがあるので、AI補完みたいなのと組み合わせると速いかも。

本の余白に書いたり、LaTeX で清書とかもやったけど、やっぱり

　　Agda による証明

が納得するためには一番かな。ただ、時間を無限に食う感じ。

雨なので学生が来ない

まぁ、ゼミはオンラインなのでいいんですけどね。

西原運動公園

ミッションデーの関係だと思うけど、かなりポータルが増えてて、取りに行ってきました。

緑のNovaの余波で落とされたけどな。御苦労様です。

この裏に階段があって、キリ短に抜けられます。

この雑な感じのステージはなんなんだ。琉大の池のそばにもあるが。

Ingress Mission Day

ミッション苦手で。うっかり首里から始めて、識名園往復したので、坂がきつくて。

ゆいレールからで、県庁周辺が楽だったろうとは思いますけど。

緑はこのタイミングで Nova ですか。割とお掃除されてよいかも。

那覇周辺は緑のリンク切るの大変だったんじゃないかな。

バスが二台続けて

と思ったら一台は48分遅れ。沖縄のバスあるある。

そんなバスでも工夫して使ってますが、なかなかありがとうという気持ちにはなれない。

バスの運転手の個々の技量もあるけど、上の方が

　　乗る人のことを考えて運用してない

それは残念な感じだな。

　　ゆいレールの終着に連絡した沖縄市/うるま市までのバス

とかあるとだいぶ変わる気がする。

　　北側から琉大に乗り換えなしのバス

もないから、どんだけ沖縄市/うるま市冷遇するつもりなのか。

るんば君のおうち

なんか作られてました

新しくなったので、地図とか見れるらしい。前のは

　　ランダムウォークだろお前

ってな感じだったからな。

相変わらずケーブルは天敵らしい

Agda memory exhusted 解決

どうも、

　　値のまま、直接書くとだめ
　　一度、変数で受けて、その関数内で簡単にしてやると良い

らしい。これはちょっと不思議で、

　　Haskellの実装は、値は一度変数で受けるように変換される

はずなんですけどね。Agda では違うのか。こそくな変換で通ったり通らなかったり。

うまく例題が抜き出せれば、issue 出すんだが...

ペットボトルのキャップ

なんか、一杯なんですが

　　ゴミのコストは回収のコスト

どうするんでしょうね。21世紀に夢を持つのは小学生までで、実際に21世紀になったら

　　21世紀は馬鹿の時代

だなと。戦争始めるのは馬鹿しかいない。でも、本当は

　　21世紀はエントロピーとの戦いの時代

だと思う。Heを大気から抽出とかもやるようになるのかも。

来週はミッションデー

Ingress も10年かぁ。自分はもう少し短いですけどね。iOS版からだから。

Android を使っている米軍関係の人から始まったので、沖縄は割と早くかもりあがったみたい。

ミッションは

　　参加者が作るポータルを巡回する

もので、それをいくつか用意してイベントというわけですね。メダルがもらえるはず。

https://note.com/md2022_naha/

Agda のメモリ超過

別に Agda の限界を試しているつもりはないのだが

　　Agda interaction error: agda: Heap exhausted;
　　agda: Current maximum heap size is 3758096384 bytes (3584 MB).

3.5GBくらいごみだが、増やしてもおそらくは意味がない。なんかループしてるんだな。

この前、Model Checking 書いた時にも、別な無限ループくらってた。

型検査は基本的には Unification なんだけど、

　　NP Hard

だっていう論文を昔みたっけ。とりあえず、

　　なだめすかしながら

みたいな感じでやり過ごす予定です。結果は、プロシンで発表するはず。

Ingress の Kinetic Capsule

ポケモンのあれと同じで

　　歩くとアイテムがもらえる

やつなんですが、なんか、大量に出るようになっちゃって。

空きカプセルとあわせてが27個? 27個横スクロールかよ。

　　そのUIでいいと思った責任者でてこい

的な。まぁ、でも

　　Power Cubeは10個を、Hyper 5個に変換して使う

ってのが良いようですね。他は変換材料がそろったらみたいな感じか。

ctest

コンパイラの例題、書き直し始めたんだが

　　cmake で書くだろ?

こったことしなければ簡単。CMakeList.txt に

　　cmake_minimum_required(VERSION 3.24)
　　add_definitions("-Wall -g")
　　set(CMAKE_C_FLAGS_DEBUG "-O")
　　set(COMPILER　s-compile.c s-token.c)
　　add_executable(s-aarch　${COMPILER}　s-code-arm-mac.c　)

と書けば良いだけ。test がよくわからなかったんだが

　　enable_testing()
　　add_test( NAME test-aarch COMMAND sh test.sh ${CMAKE_C_COMPILER} s-aarch )

で良いらしい。

　　ctest

が、add_test した COMMAND を順に実行するだけ。そうそう、そういうので良いんだよ。凝ったことするな。

cmake いろいろ問題があって、特に CMakeList.txt の構文のだめさは半端じゃないけど、動作の割り切りは良いんだよな。

くろしお

いらぶー使った沖縄そばのお店。愛知の裏、長田先生がいつも行ってた飲み屋さんのそばです。

　　だがしかし、このやる気のないのはなんなの?!

いや、味は、いらぶーらしく「ど、あっさり」で良かったですよ。

　　それでは足りない人のために塩が置いてあるくらい

ここは歩きは無理なんだよな。

iCloud Photos

ちょっと多すぎて切ってるんだが

　　勝手に入れる奴がいる

そういうところなんじゃないの? Photo stream がトラブりまくるのもあったし。

Cloud storage は「人質にする」戦略があって、

　　勝手に昔のを消す Slack

とか。それで

　　自分は敬遠してる

感じ。将来的にはどうなんだろうな。自分は fj 的な

　　オンプレ / 個人ストレージとの連携

を考えてしまうが、それを妨害しにくるのか、連携しにくるのか。

思ったより値段下がってないし。動画でなければたいして持ってるわけでもない。

182G Photos
61G iTunes

マイバックからパンツ

コンビニで「これに入れてください」で出したら...

　　「あ、洗ってあるから大丈夫です」

って、そういう問題ではないか。着替えを持ってきた時に中に残ってしまったんだな。

原神のイベント

最近、さぼりぎみで。デイリーくらいで放置してたんですが、なんか、アンケートで、

　　お前は、なんで、このイベントやらないのか

と怒られた。なんとか祭りなんだが、あと7時間? そういえば、

　　レザーの産みの親がなんとか

ってのを見たような。あれって、そんな大きなイベントだったのか。いやさ、

　　なんで、新マップと重ねるんだよ
　　そもそも、レザーってくそがきにそんなに興味が...

いや、確かに、そんな理由でベネット全然育ててなかったとかあったわけですが。

どっちかというと、モンドの懐かしいキャラ紹介イベントみたいな感じなんだな。

　　リサおばさん、久しぶりです

的な。これって、あと7時間で終るのか?

こた

12歳くらいだっけ。おじいちゃんだけどね。

7色のTシャツ

なんか学生が

　　曜日毎に違う色のTシャツを着ているらしく

いや、別に停めませんよ。

自分は学部4年の時にはスーツ着てたな。アルバイト先とかでも、その方が。

コンパイラの例題がさびついてて

まぁ、動かない。簡単な式のtokenize/parse/code生成までですけどね。

もういいかなとか思って、さっさと、gcc/llvm だと思ったら、

　　学生が ARM のところがわからないんですが

とやってくる。わかったわかった。来週なんとかするから。

code 生成部分の printf を書き直すだけだけど。

byte code のも書いてみたいかも。

https://gitlab.ie.u-ryukyu.ac.jp/teacher/kono/compiler-examples
-

blog は毎日書くからblog

mixi はカレンダーで書いた日が見えてたので、毎日書くというモチベがあった。

で、0時の前後に二つ書くとかやってました。タイマー使った時限投稿とか。

本末転倒感はあるかな。

ネタを Evernote に書いておくとか。

ネタになる写真を撮っておくとか。

まぁ、ネタにつまってからが本番であることは間違いない。

OSの補講の採点

Q. Why is it that having multiple resources does not necessarily prevent
the occurrence of a deadlock?

Why で始まっているが、例示が必要。なぜと聞いてはいけない例にもなってる。うちの学生には難しすぎるか。

dead lockの条件を列挙するところまではできるのだが、その条件を絶対に満たさない例がないと「ロックの必要はない」にはならない。
複数ファイルを順に読むだけならロックは不要とか書けば良いんだが...

英語ができるかどうかってよりは読まずに答えている感じかな。

国際通りのブラウン管

Back to the future やってるな。そして、

　　ばっちり映り込んでる

気をつけてはいるんだけど、やっちゃうね。

Tap Water

水道水のこと。学生時代に米国に言った時にお店で愛用してた。今はやらないですよ。

　　お店に、ちゃんと水物で儲けてもらうのが良いお客さん

で、良いお客の方が歓迎されるからな。なんだが、

tab water だと思ってた。だって、そう聞こえたし、それで通じてたし。日本人だしな。

現地のお兄ちゃんに聞いたからだが、辞書引けと。

こう集まってると、落としたくなる

そんなものだよね

QUNOG

この手のイベントは長田先生だったんだが... IXとか懐かしすぎる。

珍しく話を聞きにいってきました。

物理層の話は楽しいが、プロに任せるべきだと思うぞ。

質問は Slack だったんですが、少ない感じ。プロシンと比べてはいけないか。

健康は野菜から

なんか、サンドイッチに付いてるパセリ

　　それでも取れば野菜だから

え〜、そんなものなの? ナッツ食えとかうるさいですけどね。やっぱり、

　　もつ鍋

じゃないですか? 野菜が多いのは楽しい。

英語を学ばない子供たち

まぁ、日本でのIT技術職の給料の話とかして、

　　自分の授業では英語の教科書を使う
　　そこから問題を解かせる

とかやってますけどね。まぁ、やらないですね。20代前半なんだから、

　　半年も英語に commit すればかなっりのところまでいく

20代後半からやっても、到底無理なところまで楽勝なのだが、その黄金期を逃してしまう。

それは残念なことだな。いや、

　　カリキュラムとして、実用レベル(TOEIC 900とか)まで要求

すれば大半クリアできることはわかってるんだよな。もちろん、それで落ちこぼれるのが無能というわけじゃないですが。

今の日本だと中国語か英語あるいは両方は必須だと思うんだけど、思ってるだけでは学生には伝わらないな。

　　東大の博士が日本語で博士論文書く

とか驚いたのもずいぶん昔だが。

任意の比率の柿ピー

ダメじゃん

リコリコ

ちょっと話題になったあれですが、なぜか第2話だけ録れてなかった。が、まぁ、それほど影響はなく。

というか、やっと盛り上がってきたと思ったら、もう終わりなのか。

　　弾よけと言えばエイトマン

まぁ、たきなは可愛かったし、シンジ君も出てたしな。

優秀な才能ってのはあるけど、まず、居場所を確保して、あとは好きにすれば良いといえば良い。

そんな感じ?

ヘンリー8世と

Rick Wakeman のあれですが、最近、練習してたりする。最初の方だけですが。

　　いや、やっぱり、暗譜して繰り返し練習すればいけるだろ?

院生時代に買った楽譜で。当時は、まったく弾けなかったんですが。で、まぁ、

　　一応、なんとかなる

なんだが、

　　Wakeman のお飾り高速トレモロ

は、無理っぽい。それも練習すればいけるのか?

昔も下手だったが、練習さぼると、そこまでもいけないのだよな。音階からやる根性はないですが...

てだこ浦西周辺のお店

ゆいレール終点まで乗って「何もない駅」なわけですが、いくつかあります。

ご存知ハリーズ。うちの研究室御用達のスープカレー屋さん。石嶺方面に7分くらいか。日曜休み。

よなラボラトリー。イタリアン。水曜日休みだが、最近根性ないみたい。結婚式の二次会に使えるくらい広い。

トルコ料理ケレベッキ。當間先生御用達。

良いお店はいかないと無くなってしまうので、応援したい。

Disk server Ubuntu update 22.04

それ以外は全部 22.04 + podman 4 まで無事上がったので。で、Disk server を 22.04 に上げるのは楽勝〜

　　なはずもなく

ばっちり、ネットワークがつながらない。iDRAC は動くんだが。どういうこと。

Firm update してみたんですが、

　　dmesg | grep bmx

でみると、Broadcom 10G は、ちゃんといる。いろいろすったもんだしたんですが、

　　/etc/netplan と ip a の ehternet device 名が違う

で、目のこでなおしたら動きました。そういうことか。/etc/netplan/*install* そのまま変更してるからかな。

device name 変更は趣味ですか? 他のは問題なかったのに...

必ずトラブルあるのどういうことなの?

podman で複数ネットワーク

cni でやるわけですが、

　　今まで動いたのが、どんどん動かなくなる

という感じ。

　　-network pod350,pod48

で複数指定して動いていたんがだめ。

　　-network pod350:ip=xxx:xx -network pod48:ip=xxx:xx

とすると、ip a で正しく見えるが、

　　ping でぼろぼろ落ちる (おいおい

ちょっと諦めモードなので、pod ではネットワーク一つにして NAT でなんとかするか。

Intel MacMini, Monteley の Time Machine

この間から backup 取れてなかったやつですが、

　　やっぱり、取れてない

ディスクを選択できるが、そこに backup が始まると落ちる。ぐぐると、

　　同じことが起きている人たちがわらわら
　　しかし、Apple は知らん顔

って感じらしい。なんか、

　　接続しているブルレイドライブもだめ

なのだが、MBPにつなげば問題なし。ってことは、USBのドライバの問題か。

おくたびれ

昔は、あーくたびれた。で、じゃぁ、飲みにいくかだったんだが、

最近は、おとなしく帰ります。

IPv6 なおったっぽい

どうも、センタ側の「新しく入れたA10」が悪さしていたらしく。ところが、

　　 curl --ipv6 -v https://gf.line.naver.jp が通る時と通らない時がある

そういえば、NATの外向け Pool が妙に小さかったような。で、

　　え? IPv6 でNAT?

という突っ込みが入るわけですが、自分が設定する前から入ってたので尊重してただけ。ま、IPv6 のNATは切るよね。

で、動いているみたい。自分のを除いて。CUIで設定さがすの面倒なので、明日にするか。

というわけなので、片付いたみたいです。めでたい。

NAT64 は動きました

VLANを全部、Fortigate に集めて、Fortigate で分配するという方式らしく、さらに、

　　DNS46(IPv4をIPv6にmapする)

も Fortigate にやらせてるのだが、

　　gateway と DNS は異なると思ったらしく、gatewayがずれてた

だけでした。典型的な

　　一方からの ping は通るが、反対側からは通らない

って症状だったのに気がつかなかった。あと、

　　VLANの数の二乗の分の、policy6 と policy46

を書けば良いだけ。でも、FortiOS 7 になると動かない説とかも。

センタ側のIPv6の問題はもめるかもしれないが、SINETからのIPv6を通してくれればよいだけなので、

　　むこうがごねなければ

問題ないはずです。でも、いきなり切る人たちだからな。

あとは、PowerDNSの設定は終ってるので切り替えだな。Kea DHCPとかも。

IPv6 な問題

gitlab は NAT46 運用なんですが、apt-get できないって問題があって。どうも、NAT64 がうまくいってないっっぽい。

しばらく Fortigate と格闘してたんですが、

　　そもそも、IPv6 が外に出てない

どうも、二ヶ月前に

　　LINEがIPv6だとつながらないから、DNSのIPv4切った

とか書いてある。それでは気がつけないです。その時は ping6 は通っていたっぽい。今は ping6 も通らない。

こっちの IPv6 gateway までは届くし、IPv4 ば抜けてるので、おそらくはセンタ側の問題なんじゃないかと。

そもそも、琉大の本家のWebは ipv6 ないし。

gitlab 側

中から外に出てれなくて、ci が動かなくなってる gitlab なんですが、

　　ipv6 は外にはつながってる
　　DNS46 は動いていて 64:: を返してる

しかし、

　　NAT64 は動作してない
　　学内から ipv6 で gitlab に接続するのもきてない

そもそも、

　　学科の bind9 が AAAAを返してない

なるほど。誰だよ壊したの。まぁ、たぶん自分だが。

ipv6の接続性をなおさずにDNSをなおすと、だめなはずなので、ipv6 からだな。

Main Switch のroutingか、Fortigate 。たぶん、Fortigateだと思うんですが...

git のトラブル

Hugo が簡単に使えるように、いろいろ画策してたんですが、

　　できた! で、git commit -a ; git push!!!

で、「使ってね〜」で、

　　自分で試してみたら、動かない

なんだよ〜

　　submodule を入れるところに、空の directory が入ってて動かない

で、git で 空のdireotyは git rm -rf では消えない。

　　git clean -fd

しろと。だから、git に付き合うのはいやなんだって。

どうも、hg-git っという、hg から git repository にアクセスする plugin があるらしいですが... (だめだろうな)

こんなことも知らないのか攻撃

僕もたまにやりますけどね。

　　知らなくてすみません、それはどこの教科書に載ってるんでしょう

と返すと良いと思います。

　　教科書に載ってるのなら、まぁ、そんなんもん
　　教科書を示せないなら、文句を言った人の残念

という感じじゃないかな。知ってて当然なら、どっかに書いてあるべきだよね。

KVM の vm で IPv4 が通らない問題をやっと解決しました

OSの補講をシステムのチェックにつかってるわけですが、

　　あっとんの遺作な Akatsuki を修正しているうちに

gitlab の ci が、IPv4 が通らないせいで動かないのを思い出して、その辺を調べることに。

IPv4 が通らないのは VM なので、おかしいのは KVM だろってことで、旧サーバのUbuntu 22.04 なKVMを調べる。

で、やっぱり、旧サーバでも Fedora の IPv4 なDHCPが通らないことが判明。ちなみに、

　　Fedoraの static ip の設定はくそめんどくさい

のね。で、どうも、

　　iptable6 改め、netfilter の問題らしい

で、以下の blog にある

　　/etc/sysctl.d/bridge.conf
　　net.bridge.bridge-nf-call-ip6tables=0
　　net.bridge.bridge-nf-call-iptables=0
　　net.bridge.bridge-nf-call-arptables=0

　　/etc/udev/rules.d/99-bridge.rules
　　ACTION=="add", SUBSYSTEM=="module", KERNEL=="br_netfilter", \
　　　　　　　 RUN+="/sbin/sysctl -p /etc/sysctl.d/bridge.conf"

で、netfilter を外して、

　　virsh net-undefine default
　　virsh net-destroy default

として、reboot すれば良いってことがわかりました。

いや、去年すぐにわかってしかるべきだったが、最近のネット検索はごみが多くて。githubのissueとかが引っかかるんだが...

https://levelup.gitconnected.com/how-to-setup-bridge-networking-with-kvm-on-ubuntu-20-04-9c560b3e3991

Ubutsu 22.04 続き

podman 3.4 は、/etc/cni の構文が変わっただけみたい。ただ、コマンドラインから

　　--ip は一つだけ
　　複数 ip はだめ
　　ipv6 もだめ

なんだよ〜 podman 4 にすれば --ip6 と書けるらしいけど、あんまり期待できないな。

/etc/cni の方の構文 (json)に関しては no information 。

podman4 を入れようと思うと、source code からってことらしい。まぁ、Unix文化っぽいけどさ。

ちょっとはまってます。いつものことか。

咲樹の骨汁

まあ、1/3は食べれない骨なんですけどね。

1/3は残したかな。これでもご飯少なめ。

Ubuntu 22.04 / podman 3.4

いろいろ先送りしてたのをやってたんですが、

　　また、PowerDNS用に posgress のデータベースをコピー

するだけなんだが、4月にやったのに「やりかたをすべて忘れてる」。うっかり、-d db をつけ忘れて、変なところにコピーしてしまった。

それはなんとかなったんだが、

　　そもそも、podman の pod のネットワークがまったくつながってない

え〜　どうも、

　　macvlan は廃止

え、そうなの。じゃぁ、どうするの〜

いや、その

　　サーバを含むあらゆるところに、VLAN で全部の LANを持ってくる

っていう発想が間違っているんじゃないのか?

企業からの訪問

いまは、学生いないからな〜

なんか、海上自衛隊の保守関係の会社らしく、いろいろ聞けて面白かったです。

　　船とかに送り込まれると、ネットがつながらないから人気がない

えぇ、いまどき? 飛行機でもつながるでしょ。しかし、

　　潜水艦は無理

まぁ、それはそうだな。この手の官公庁絡みの会社は安定といえば安定。成長するかどうかは知らないですが、

　　大手が撤退している分、中小の仕事が増えている

という逆説があるらしい。

Time Machine HDD

いや、そういえばあれはとかあるじゃないですか、自宅の MacMini で、じゃぁ、TMみて

　　と思ったら動作してない

外付けHDDのランプは点いてるが。外して、MBPにつないでもだめ。どうも、2.5inch HDD の音がしてない。(Seagate)

うーむ。チェンジニアリングの結果、HDDが逝ってるという結論に。

MBPは今は micro SSD に取ってるので、その前のHDDを使うことに。え、前のbackupは 2021/4? まったく気がつかなかった。

で、一つのHDDに二つのTMがあると文句いうのね。でもなんかとりあえずは取れてるみたい。

最初のちょっと見てみるって方は、自分の blog の検索ですませました。

atcoder

いや、プログラミングコンテストは、あんまり好きじゃないんだが。

ちょっと問題見てみたんですが、

　　2時間だが、まる一日かかる

まぁ、そうだよね。問題自体は、C/C++ 向きに作られてる感じ。時間とメモリ限定だし。でも、

　　計算量的に無理な感じに作られてる

つまり、

　　普通に全数検索するめるとだいたい死ぬ
　　配列の大きさが10^5なので、二乗で厳しくなるように作られてる

なので、

　　時間がかかりそうなら、適当に答えをなげる

というコードを入れてる人がいる。点数にはならないけど。

なので、やっぱり C++ でやってる人が多いな。C++の lower_bound とか使ったことないな。

まぁ、実際にやるかどうかは。

https://atcoder.jp/home

おおコウモリ

琉大名物です

ばっさばっさと飛ぶ

BD-REDL

いや、どうせほとんど見ないんだけど。昔はHDDに入れたりしてたんですが、

　　光学メディアだけで良くね?

ネトフリアマプラDzyを一月ごとに廻すでも良いんだが、まぁ、カセットに録っていた頃の惰性です。

で、BD-REDL 50GBも安くなってきたし、録画の手間が減るかなと思って。なんだが、

　　安物を買うくせが...

そんなにかわなんないんですけどね。で、

　　ばっちり不良

三回くらい出し入れすると、初期化が成功する場合がある。ダメな時もある。しかし、

　　BDZ-FBT1000 だとだめ
　　BDZ-RX50 だと初期化書き込み問題ない

はぁ? で、RX50で初期化して FBTで書き込めば良いと思うが、

　　FBTでの書き込みは失敗する

あっそ。レーザーの出力とか、書き込みアルゴリズムとかいろいろあるんだろうな。

BD-RE でも昔のに書き込んだりすると「いきなりメディアが死ぬ」とかあるので、

　　光学メディアの信頼性はそんなもん

らしい。まぁ、惰性なので、その程度でいいかな。この「だめなメディア」ってのも楽しいといえば楽しいし。

Ingress Lv10

まぁ、6/27 Recursion からだが、そんなペースです。

最近は、そんなにがんばってるわけでもないが。宜野湾通ったときには、応援なり撃滅なりしてください。

前田のスープカレー、ハリーズの入り口

並列信頼研御用達です。

座布団みたいだが、なんか、名前があるであろう飾り。

うちは、ここのカレーで廻っているようなもんです。

最近は、もっぱらテイクアウト。コロナだからというよりは、前のオーナーの健康状態に配慮した感じ。

insta は、あんまりupdateされてないな。LINEもあるはずだが。

https://www.instagram.com/hallyscafe5232/

facebook の写真だけ見れない

ってわざを、学科のWifiのiPhoneが出してて。MBP では問題ないんだよな。

まぁ、Wifi 外せば見れるんで害はないんですが。

この手のわけわからんのを、さっと調べることはできんのか。

MTU か NAT の関係だろうなとは思うんだけど...

iPhone の容量

いや、全然仕事してないので、メインに食ってるのは

　　原神

Photos は基本削除ですが、Google Photos で一通りは見れる。

音楽も最近は聞かないが、Apple Music でない、iTnues Match 。

なので、そんなに容量要らないわけね。でも、

　　128GBか256GBは迷った

が、まぁ、足りない時はその時だから。まあでも、

　　去年、13 ProMax にしたのは正解だった

ってところですね。

USBメモリ

ずーっと昔から使ってるやつ。USB-B/C で普通に便利。最近は、

　　コピー機にこれで持っていって、印刷

が多いかも。事務はいい加減、紙止めろよとも思うけど。まぁ、そういう頻度ってことね。

16GBで、micro SD　の128GBの方が容量が多いんだが、そっちはあんまり使わない。

たまに学生に自慢して「欲しいなら買うよ」というが、その程度では釣られないのが最近の学生か。

キーボード

割とこだわらない方です。システム管理でキーボードにこだわるのは二流だろ。

若い頃は

　　Sony NEWSのJISと、東芝DynabookのUSを交互に打って腱鞘炎

とかやってましたけどね。その時には、

　　JISは止める
　　遠い Enter key は、手首全体を動かして押す

ようにしたら改善しました。今の MacBook の

　　超浅いストローク

も結構好きかも。ただ、この前の MBP15 のはさすがにいただけなかったが。かなり壊れたし。

なので、例の超速タイプなJKの打ち方も割と違和感ない感じ。その方が

　　指の腱に負担がかからない

のだと思います。

Gundam Seed

浦添パルコのガンダム展は結局入らなかったんですが、

　　例のポスターには、Gundam Seed 版もあった

ということがわかりました。

Gundam Seed は 1st をrespectするとかいって始めて、まぁ、あんまりよろしくなかったんだが、

　　Gundam Seed Destity は、そんなものじゃなかった

でも、

　　色んな曲が入っていて、カラオケは面白い

まぁ、もう忘れかけてるけどな。

クリームパスタ

いつもの、West Field Cafe なんですが、

　　豆乳仕立て

なるほど、クリームでは女性にアピールしないか。

昔(1970年代)、世界の料理ショーというイギリス人の料理番組があって、これが、

　　とんでもカロリー

だったんですが、1990年にグラハムカーが再度登場して、新世界の料理ショーってのが、

　　クリームをヨーグルトに入れ替えて、カロリー表示

というわざを出していた。

自分も博士課程で結構太ったので、割と共感しながら見てた記憶。でも、

　　イギリスで1年自炊してたら、激痩せしました

カルボナーラとか、卵入り袋麺とか良く作ってたんだけどな。ま、いまは普通。

台風

まぁ、9月っぽい 今回は学生達は、サーバは停めないみたいだな。まぁ、だいじょうぶでしょう 昔は、台風だと、西原町は必ず停電したものなんだけどね いや、微妙になんかとまってる?

ループの続き

Server と Fortigate の設定いじりまくってたんですが、どうにもならず。

　　VM停止、vlan 停止
　　Fortigate から conflict してるVLAN停める

で、めんどくなって、

　　Fortigate とサーバーをメインスイッチからケーブルごとはずす

ってのをやってみたんですが、ランプの状況が変わらない。

なので、何か違うかも。Switch のログみながら、ケーブル外すってのをやってみるか。

単に全部のランプが点滅だけじゃね。

ループの続き

どうも、サーバ側と loop してるらしく... Switch やケーブルの問題ではないらしい。

で、サーバ4台には

　　Fortigate へのリンク (F)
　　Main SW へのリンク (M)

が二つあり、それぞれ、20個くらいの vlan の trunk... なんで、そんなことになってるかは歴史的なもの。

loop してるのは、そのうちの2台 (a と c)

で、めんどくさくなって、

　　F を a と c で落とす

ってやったんだが、影響なし。そうだよな、Main SW 経由でつながるから。loop も止まらない。

　　M を a と c で落とす

ってやったら、a は影響なかったんだが、c の接続が切れた。c は大域アドレス持ってないからな。

iDRAC から login しようとしたら、

　　パスワードが入らない!

キーボードが日本語になってるからだ。しかたなく、物理コンソールつないでみたらわかりました。

やっぱり、Fortigate 側の問題なんじゃないかなぁ。サーバ側の設定が git で管理されてないって問題も。

学生のプロジェクト

M1 だと好き勝手なことできるからな。 なんか、ヤフオクで、Cisco のスイッチとか、Fortigate とか買って遊んでるらしい。 いや、もっと高いのがそこあるだろ?

サーバメモリ増強

ディスクサーバ2台ですが32GBは無理でしょ。というわけで、旧サーバから256GB (32GB x 8) 引っこ抜いて、128GBずつ増強。

　　Different type of DIMM detected

なるほど。前の16GB x 2 を抜かないとだめなのか。

ところが、一台が Intializing で iDRAC にも接続できない。ググると

　　ハード不良でそうなる

え〜 しばらくメモリ入れなおしたり格闘したんですが、

　　サーバのACケーブルを抜いて入れたら復帰

おいおい... まぁ、良くある話ではあるが。

これで、Ceph のOSD Buffer を推奨どおり 4GB にできて、残りのHDDもOSDにできるはず。
-

Shivershatz の続き

Wiley の site が、学科の無線LANからだとぜんぜん動かなくて...

wiley.com で購入

するが、そこから epub が落とせない。メールでコードを送ってくる。

VitalSource Bookshelf というクソアプリを down load して

　　wiley の account とは別にあたらしく account を作る

　　電子メールで確認

そして、iPhone 側では Redeem code prompt は出ないので、mac 側の Bookkshelf から redeem

すると、iPhone 側でも読めるようになる

という流れらしい。で、*.vdk とかいうクソバイナリが epub らしいです。

ePub Reader 自体は、そんなにだめじゃない感じ。でも、これは絶対に読めなくなるパターンだな。

いや、

　　電子書籍を不便にして高く売る馬鹿ものたち

というわけですが... いや、古くてもただの方がいいかも。

なんだが、メジャーな教科書なので、Web にも落ちてるな。買いたくないわけじゃないんだが、これじゃぁなぁ。

辞書

2019に世界大百科が読めるようになったとか書いてたが、

-rw-r--r-- 40M Apr 3 2001 dict/AE.TXT
-rw-r--r-- 2.9M Oct 25 1999 dict/DAILYEJ.EUC
-rw-r--r-- 2.6M Oct 25 1999 dict/DAILYJE.EUC
-rw-r--r-- 6.4M Oct 25 1999 dict/IWANAMI.EUC
-rw-r--r-- 9.9M Jan 28 2019 dict/chujiten.txt
-rw-r--r-- 37M Jan 28 2019 dict/kojien.txt
-rw-r--r-- 218M Jan 27 2019 dict/sedai.txt

ってのが手元に。全部、平文で sort 済み。これを Perl script で二分法で検索する仕組み。

Viewer アプリ使ってたときもあったんだけど、やめちゃった。

思ったより小さい。AE はCDROMがでたばっかりの頃に買った英語の Multimedia Encyclopedia です。

広辞苑は eBook だな。daily はなんだったかな。雑誌の付録だったような気もする。中辞典は研究社の英和。

普通に、macOS についてくるので困らないとは思うけど、歴史的経緯で持ってるだけです。

command line から検索できるのは便利

!! iwanami べんり
Searching ベンリ....
ベンリ 【便利】〔名・ナノ〕都合がよく重宝なこと。また、うまく役に立つこと。「通勤に—な所」;〔派生〕 -さ -がる〔関連〕便・便益・便宜・簡便・軽便・至便・利便・実用・重宝・徳用・好都合
ベンリ 【弁理】物事を判別して処理すること。取り扱うこと。
ベンリ・コウシ 【—公使】外交使節の階級の一つ。特命全権公使の下、代理公使の上。
ベンリ・シ 【—士】特許・実用新案・意匠・商標について、特許庁に対する申請・出願などの事柄を代理して行う職業の人。
ベンリ・ヤ 【—屋】物品の配達とか伝言とかの雑用を足すことを職業とする人。

片仮名に変換してるんだな。

use Search::Dict;
$word = nkf('-e',$word);
$word =~ s/\244(.)/\245$1/g; # Make it kata-kana
open($DICT,"<$dictionary");
&look($DICT,$word,$dict,$case);

かんたん。

Zybook

OSの教科書、Silvershatz 探してたら

https://www.wiley.com/en-us/Operating+System+Concepts%2C+10th+Edition-p-9781119320913

が引っかかるわけですが、2018 でも、既に古い気がするが、まぁ、いいか。大学の教科書でレンタル?

　　あんたは、大学で得る知識もレンタルで、1年で忘却する契約か?

ま、そうかもな。

なんだが、Zybook ってのが引っかかる。どうも Web base な interactive なものらしいが、

　　値段がわからん。

Zybook どうなの?

課題は、Rust やめて golang にするつもりなんですが、C やらないのもちょっとなぁ。

Rust を C++ の package manegment に使うと良いなんて話も聞きますが、race condition を書くのに苦労するのだとちょっとね。

Mou で blog 書こうとしたら

MBP の電池が 1% 。どういうこと。

　iPhone 充電しようとしたら、充電しない
　で、MBP 経由にしたら iPhone は充電した

ってことで、

　おそらく、ACタップがだめで、そもそもMBPに電源がつながってなかった

ってことだろうなぁ。

学生と遊ぶ

学生が「昔のアップルのハードウェアの展示をやってる」というので見にいくかとなったんですが、

　　うるま市ではなくて、東村
　　しかも、水曜日は休み

ってことなので、パルコでうだうだと。

　　Raido Eva

ってのがあるのね。公式グッズですか。あんまり、ものにはひかれないですが...

東村は 8/28 までらしいんですが、再度挑戦するかどうかはなぞです。

https://www.okinawatimes.co.jp/articles/-/1006936

マイバッグ

割ともらうことが多いので、普通に持ち歩いてます。箸と同じだな。

まぁ、いろいろ便利。たまに洗う。箸と同じでいろいろ議論されるが、

　　昔は持ち歩くのが普通だった

そんなもんだよね。

LESS の option

なんか、この前から mhl / less 振る舞いが変だと思ってたんだけど。

export LESS=rMecmndh10

を歴史的な理由で使ってきたんだが、これを

export LESS=eR

にしたら、まぁ、復活。もはや、どれがどれだかわからんけど。

e は、EOF で抜けるってやつで、さすがにこれはないとうっとうしい。
R は、Esc をそのまま通す。これがないと、git/hg の diff の色付けが化けてしまう。

xlsx を送ってくるのは無視してます。

neovim and nvim-agda

ほぼ実用というか、自分で使えるくらいまでなおしたんですが、

　　ある状況になると、ex command line にわけわからんメッセージを表示して死ぬ

という状況が。Lua かなにかのError message なんだが、読めないのでどうしようもない。

Emacs 側で修正してとかやってたんですが、再現性はある。どうも、

　　neovim 8 から Lua の stack trace が入ったらしい git log がある

なので、neovim 8 の build へ go! cmake なのね。

　　cmake　-GNinja CMAKE_BUILD_TYPE=RelWithDebInfo　../neovim

とかやるらしい。ところが、Lua-5.1 の library がやはり引っかかる。やはり、

　　cp ~/.luarocks/lib/lua/5.1/lpeg.so /usr/local/lib/lua/5.1/

みたいに手動でコピる必要があるらしい。まぁ、気持ちはわかる。で build は、まぁ、通った。

なんですが、結果的には neovim 7 と同じで役に立たず。

lldb で b emsg_multiline　とかもやってみたんですが、なんか、DLOG とかがソースにある。なるほど?!

　　 nvim -V99/tmp/aho zorn.agda

とかすると、Debug log が取れるのか。(-V15 とかではだめ)

　　...kono/.vim/pack/plugins/start/nvim-agda/lua/agda/init.lua:917: invalid UTF-8 code
　　stack traceback:
　　^I[C]: in function 'gsub'
　　^I...kono/.vim/pack/plugins/start/nvim-agda/lua/agda/init.lua:917: in function <...kono/.vim/pack/plugins/start/nvim-agda/lua/agda/init.lua:910>

やっと捕まえましたよ。Luaの utf8 lib の utf8.gsub が invalid UTF-8 code で死んでる。良く見ると

　local v =　utf8.gsub(vv, "^JSON> ", "")

で、JSON> を落としているだけなので、string.gsub に置き換えたら通りました。

で、そのまま pull req したら、「ばらばらじゃなくて、まとめろよ」とか言われたので、squash とかして出しなおしたところです。

https://github.com/shinji-kono/nvim-agda

ISSと月とのホーマン軌道

ISSは、ほとんど地をはう感じだからな。月の方は1km/sくらいで動いているわけですが、ホーマン軌道もそんな感じ。

　　ISS側4km/s
　　月側0.8km/s

120時間で着くらしい。月側は良いんだが、ISS側はそこそこ加速しないとだめだな。

で、この軌道にそこそこ大きな質量を置いて、質量加速器を付けると面白いと思う。

人間が乗れるような加速度にはならないとは思うけど、巨大な

　　メリーゴラウンド

みたいな奴。降りる方もそれを使うような感じで。あるいはスペースフック的な。

いや、4km/s の速度差があるものに乗り換えるってのは、どうなのって気もするが、

　　5G 80秒

なら、実用的な感じもする。

問題は、間違えて地球にそれを落とした時に大惨事ってやつだな。

4TBの使い道

なんか、バックアップ用にNAS買ってもらったんですが、

　　4TB x 4 で 16TB

なにけっちってんだよって感じで全然足りないので、

　　16TB x 4 に換装

したわけですが、

　　余った 4TB x 4 の使い道がない

もしかして、4TBってもはやゴミ? そうなのか?

すれ違い

たぶん、高度差はかなりあるんでしょうけどね

りはびり中

たいして熱もなかったし、しばらく閉じこもっていただけなんですが、

　　少し気力に影響してるな

というわけで、りはびり中です。でも、

　　プログラミングには支障ないらしい

nvim-agda の Lua の debug 手法がわからん。neovim 8 まで上げると stack trace が見れるらしいが...

neovim の search hilight

VSCode だと良くあるけど、neovim も

　　search すると、探したものを　hilight する

まぁ、それは良いんだが

　　ずーっと残る

これは、うっとうしい。で、

　　:nohl

とすれば消えるんですが、かなりの回数打ってることに気がついた。

まぁ、VSCode ユーザは気にしないんじゃないかと思うけど。


　　function DisableHL()
　　　nohl
　　　redraw
　　endfunction

　　autocmd InsertEnter * :call DisableHL()

とすると insert mode で消える。でも、微妙に復活するな。

search register を空にした方が良いってのもみましたが、それはどうかな。

ブラウン管

池袋の地下では、まだ、現役らしい。動画にするべきだったな。

その先はビデオなんだろうけど、確認はしませんでした。

だから若者がいくようなところは

まぁ、感染しないことが目標ではないので... でも、このタイミングはな。

これ食べてる面子で自分含めて三人なので、まぁ、そういうことらしいです。

結局、熱らしい熱もでなかった。悪寒があったのは一日だけ。三回打った成果か。

でも、三回目は3月だったから、感染予防というには前すぎたか。

この時期の東京にきた時点でかなり負けてるからな。沖縄ならいいのかってのもあるけど。

まだ、しばらくはおとなしくしている予定。