パルコシティの回転寿司

「恵み」かな。 廻転はしてませんでした。

職人さんが手袋ってのは、ちょっと違うかなぁ。

お勘定は Pad から。音声入力させて欲しいかも。いや、目の前にいるわけなんですが... でお勘定ですが、

　　お皿数えて伝票でないものに書き込み

その伝票でないものを渡されてレジにいくと、

　　伝票でないものからレジに打ち込んで会計

はい? いや回転していた頃の名残りか... 回転しないなら Pad からお勘定したい感じ。

皿にチップが入っていてセンサでってのは見た気がする。

パルコシティは、開店からしばらくたったガラ空き度とあまり差がない感じでした。

録画整理の季節

Apple TV+ に Foundation 2021 とか書いてあって、ちょっとがっかり。政治的に正しいキャストなようでクソジジイなハリセルダンは出てこないっぽい...

それとは関係なく、円盤派なのでBDREにコピーするわけですが、もう、CMカットとかもさぼってるな。

いつまでたってもClosed Captionが改善せず、むしろ悪化したスカパーはやめてしまいました。CMなしアニメは便利だったんだけど。

今は BS11 あるから、アニメはそれでいいかな。録りはぐれがあるとリカバリできないですか。必要な時だけスカパー入れるとかでも。

Amazon Prime Video は残念すぎる感じ。わざわざ Closed Caption はずして配信するのが意味不明。画質も圧縮しすぎ。

　　まぁ、今の若い子は画質なんて気にしないですけどね

80inchくらいのテレビが欲しいと思わなくもないが、徐々に見なくなるものだな。

結局、今期のアニメは見ないまましまわれてしまうのか。サクラ大戦もちょっと違う感。神の塔は少しがんばるか?

ぴったりだ

まるであつらえたかのようだ

VSCode の続き

お昼に首里でラーメン食べた時に替え玉したら夕方まで祟りました。おっとっと。ラーメン自体はうまかったです。

結局、Agda は Market place から access できる Agda mode で「Vim の insert mode で C-C C-L」するで良いらしい。

Emacs での→とかの入力方法も使える。

ま、おっさんなのでTile baseのごちゃごちゃいろいろついてるのはなあ。InteliJ で慣れてるつもりなんだけど、

　　便利なはずの機能はAgdaでは、ほぼ意味なし。予測入力くらいか。

mini map もそうだけど、版管理の変更部分を左右に表示するとか、cursol上のwordを全部 hilight するとか馴染めないです...

行番号も消したい派だからなぁ。気が散る感じ。

Search も否定条件をいれようと思うと、正規表現のうんたらを使う必要があるらしい。あと、dot file もサーチするのやめて...

いや、一般的なプログラミング言語に対する一般的な編集とプログラミングなら良いんじゃないですかね。

ってな感じでお友達にはなれそうにないな〜 InteliJ は Java ならまぁ。

VSCode and agda

ZFの方できまづいバグを見つけたので微妙にやる気が... なんとかなるかどうかは謎だな。

なので、VSCode ためしてみようかなと。つまりは逃避ですけど。

なんか install は簡単なのだが Electron なんだよね。つまり、JavaScript でも ts つまり、TypeScript で書くらしい。

ですが、なんか右側に縮小表示、左側にExploer。なかなかお友達になれそうにないな。右側は

　 Setting で minimap を探して Editor > Miniap: Enabled のチェックをはずす

ので消える。で、Vim Key binding にするには、Vim の Extension を入れればよい。Extension Menu で Search して install するだけ。

で、問題は Agda だが... Higlight はあるんだけど、interactve mode は?

一応、agda-mode あるんだが、なんか動かない。

　　　　　https://github.com/konn/vscode-agda-interactive.git

を試してみるんですが、node.js がいるの?

　brew install node.js
　npm install -g yo generator-code
　npm install -g vsce
　npm install -g pegjs
　npm install --save-dev typescript
　mkdir out
　vsce package
　/Applications/Visual\ Studio\ Code.app/Contents/Resources/app/bin/code --install-extension agda-interactive-0.0.1.vsix

ぐらいで入ったんですが、まだ、動いてないです...

market place 側の agda-mode ってのもあるらしい。そっちもなんかだめ。agda command が呼ばれてるかどうかくらいわからんのか?

VSCode 本体は... あんまり馴染めないかもな〜

Remote Pair Programming

学生がやってくれてるのに、こっちから口出しする感じで。学生は優秀だし集中力あるけど、経験はないからな。

うちの独自言語なのでIDEとかはなく vim で。自分の趣味だけど

　　black on white (あるいはそれに準ずる色で)
　　ssh/terminal は tab ではなくて working directory が違う分、別Windowで開く
　　grep しまくる

みたいな感じでやってます。

取りあえず書いてみて、いや、こういう風に書くと良いだろ「おお〜」とかになると面白い。

ただ、

　　昼飯直後は眠くなる

のが欠点だな。観客一人いたので三人でした。「ぜんぜんわかりません」とか言ってたな。

こういうのが、うちのゼミっぽいので、参加して欲しいとは思うけど、

　　学生の遠隔授業疲れ

が出てきてるかも。水曜日の三連チャンZoomは、僕もすこしつらいです。まぁ、自分は暇な方です。(そのために沖縄にいるようなものだ...

JALのカレンダー

来年から美女ではなく風景になるらしく。なんか妙に地味な服装にしたりとか抵抗してたらしいんですが陥落したか。Beauty ってところで政治的にだめな感じ?

男女混ぜれば?

変えろという指令がしつこく来るので、別にdefaultで良いじゃんと思ってたんですが、

変更のリンクを踏むと、JAL Card 側に入れられて、Card 側の暗証番号を入れさせられる羽目に。微妙にマイレージのとの違う。それは乗り切ったんですが...

　　さらにパスワードの変更を強制

おいおい。いや、まぁ、Web上で4桁の暗証番号使ってた人たちだからな。ところが、

　　パスワードに意味ない制限が...

その大文字とか記号とか時代遅れなのやめろよ... つうか、公開キー登録させてさせて欲しいんですが。まぁ、もう、そんなものなんだけどね。

無意味に疲れさせるのやめて。桁数多ければ、そういう制限は不要って知らんのか。それよりは強度評価しろとは思います。

default は卓上カレンダーになってました。なので、おおきなのが欲しい人は変更した方が良いみたいです。

ハリーズのしあわせ

去年はいろいろあったからなぁ。ハリーズのカレーが食べれるだけで十分幸せです。

去年の今頃は、インド人たちとカレーパーティしてたらしい。

ピロティ構造

沖縄、こういうの多いけど、地震に耐えそうにない。自分のアパートも結構下が空いてて。

大抵鉄筋だしな。

まぁ、ダメな時はダメだけどね〜

Ceph 読み会最終日

分散ファイルシステムは、やっぱり難しいよね。

昨日はDocument読んだんですが、今日は、mon/osdの C++ Header から。なのだが、

　　C++17 勉強会みたいな感じに。

いろいろあるな。LLVM もそうだったけど。

　　std::forward std::move && 値渡し関係の効率化的な
　　lambda (captureってなんだよ) [&] とか [=] とか
　　std::optional Maybe 今頃?
　　std::deque 差分リスト的な
　　std::set std::map の値のないやつ
　　std::lock_guard RAII的な lock
　　explict constructor compilerに勝手に使われない
　　std::variant Unionの頭の良い奴(動的なの?)
　　boost::intrusive 意味不明

でも、最後には gdb で mount したところに書き込んだところからのeventを捕まえられました。

しかし、その直後に heart beatで見つけられて殺された。ひどい。

なんか、本があるのか。そっちを読んでからかも。

Ceph: Designing and Implementing Scalable Storage Systems
https://www.amazon.com/dp/B07NC5NM5Q

Ceph 読み会続き

割と難航中。どうも、

　　crimson-osd という次世代 OSD

があるらしく、それが、seastart という continuation / future base の非同期ライブラリで書かれているらしい。なんですが、

　　それは build されてないので読めない

build の仕方はあまり自明でないらしく... もしかすると、 developper commit からでないとダメかも。

　　bin/ceph osd pool create rbd
　　bin/rbd create foo1 --size 1000
　　bin/rbd device map rbd/foo --id admin
　　mkfs.xfs /dev/rbd0
　　mount /dev/rbd0 /mnt/ceph1

とすると、mount できるのはわかりましたが、osd/mon/mds のどこをどう通るのかが、まったくわからない感じ。

明日で終わりですが、どこまでできるかは謎です。

Ceph

というわけで読み始めたんですが、C++ なのはともかく、これって分散ファイルシステムの

　　全部入り

っぽいものだな。巨大。

　　Object Store ods
　　Meta Data Store mds
　　Messageing msg
　　Block device blk
　　Monitor/Paxos mon

xfs interface は Legacy とか書いてあるけど、Ceph のAPIがすっばらしいものとも思えず...

実際、Ceph上のアプリってあるんだろうか?

結局、Centos 7 上では build できなくて、Ubuntu 上で読んでます。ま、Centos 7 は、もう捨てるので。

ドキュメント読むところからですが、一応、gdb で ceph-osd に接続するのはできたみたい。

どっから読むんだろう?

https://docs.ceph.com/docs/master/cephfs/

帯状疱疹のワクチン

なんか奥様が目覚めたらしく受けてきました。ちょっと高いな。

なんか10年前くらいに夜中に歯も悪くないのに激痛食らったことことあってな。水疱瘡みたいなものだが、外に出ないこともあるらしい。

最近は子供がワクチンでかからないので、大人の免疫が維持されないってのがあるらしい。もうこどもに触ったりとかないし。

まぁ、なんでこのタイミングなのかとも思うけど、

　　ワクチンある病気なんだから受けとけ

とは思うよね。本当は、ピロリ菌とかも見てもらった方が良いのだが。

この手のワクチンの情報とかはマイナンバーみたいなもので管理して欲しいよね。いちいち問診票書くとかだるい。

Zoomの画面切り替え

爆撃よけにもなるので画面共有入れてしまうのが良いわけですが、

　　Webの資料とコード実行のターミナルの行き来がめんどくさい

とTwitterに書いたら画面の部分共有を使うと良いと教えてもらいました。

そこに Safari と xterm (?!) とかを置いといて、あるいは必要なものをその場所に放り込めばよい。

そこ以外の部分で準備とか twitter とかもできるので調子が良いです。

前画面だと解像度が細かすぎてぼけちゃうしな。

学生が Twitter 中継とかすると面白いけど、あんまりやってくれないみたい。

明日からは、ソースコード読み会で、今年は Ceph なはずです。Rust な ls の続きも少しやるか。

超電磁ヨーヨー

フィリピーナにはボルテスVが受けるとかいうような話があったが、まぁ、かなりの年配の人のお話ね。

でも、こういうの好きでしょ?

Filter

数学の概念、Ideal の双対だってのを割と最近知ったのは残念。集合論の選択公理連続体仮説が成立しないモデルを作る時に使います。

超実数を定義するのにも使うな。

集合論を手に入れたので楽勝で書けると思ったんですが、

　　本によって書き方が違う

Kunen とか二ヶ所に書いてあって、ちょっと違う。∃を使うか∀を使うかと、集合でやるか順序構造でやるかの違いらしい。

Agda だと ∃ は扱いにくいので、∀ を使う方が良いみたい。ultra filter なら prime filter ってのを証明できたのでそれっぽくできたみたい。

去年の10月に書いたのがだいたい正しかったようだな。本読んでる時には「はいはい」みたいに理解してたが、いざ証明してみると時間がかかる。

だいぶ馬鹿になってるかもね。ZFSet でやらずに OD でやってるが、原理的にはZFでできるはずです。

どこまでやるかは割と謎です。練習な感じ。

　　record Filter　( L : OD　) : Set (suc n) where
　　　 field
　　　　　 filter : OD　
　　　　　 f⊆PL :　filter ⊆ Power L
　　　　　 filter1 : { p q : OD } →　q ⊆ L　→ filter ∋ p →　p ⊆ q　→ filter ∋ q
　　　　　 filter2 : { p q : OD } → filter ∋ p →　filter ∋ q　→ filter ∋ (p ∩ q)

　　record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
　　　 field
　　　　　 proper　: ¬ (filter P ∋ od∅)
　　　　　 prime　 : {p q : OD } →　filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

　　record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
　　　 field
　　　　　 proper　: ¬ (filter P ∋ od∅)
　　　　　 ultra　 : {p : OD } → p ⊆ L →　( filter P ∋ p ) ∨ (　filter P ∋ ( L ＼ p) )

　　record Ideal　( L : OD　) : Set (suc n) where
　　　 field
　　　　　 ideal : OD　
　　　　　 i⊆PL :　ideal ⊆ Power L
　　　　　 ideal1 : { p q : OD } →　q ⊆ L　→ ideal ∋ p →　q ⊆ p　→ ideal ∋ q
　　　　　 ideal2 : { p q : OD } → ideal ∋ p →　ideal ∋ q　→ ideal ∋ (p ∪ q)

New Normal

事務の人たちはマスクすれば今までのままで良いってことで、まったく同じ作業に戻ってしまいました。

まぁ、そういう人たちだよな。

授業はうちは前期は遠隔なんじゃないかな〜　でも、やっぱり自宅の環境に問題がある学生が、たまに来てます。

それも、また問題なし。

何も言わないと何もしない学生もいるが、毎週のゼミも遠隔で別に問題ない感じ。

遠隔授業だと、課題をたくさん出す先生がいるらしく、プロジェクト系の演習が多いうちは、そっちに皺寄せが来てるらしい。

課題は自分の理解の確認のためにやるものだが、先生の安心のためのものでもあるのだろうな。

母への電話

せめて週一回ぐらいはと思うわけですが... ネットでも使えば顔も見れるが、まぁ、電話も良いよね。

ヘルパーさんがでる場合は、問題ない。母とも話せるし、いろいろ話も聞ける。

母が出てヘルパーさんがいないと、話は聞けないが、まぁ、良いかな。

妹が出て母が出かけてると、何にも聞けずに終わる。

ま、いいけどね。向こうからはかけてはくれないみたい。今度、ヘルパーさんに頼んでおこうかな。

Ceph build on Centos7

やっぱり、Cetos7 なので苦労しているのですが、

　　そもそも C++17 なのでコンパイラが新しくないとだめ
　　leveldb の version が合わない

みたいなのがあって、yum で入れても 1.0.7 かなんかで古すぎる。

rpm も stdc++ のversion が合わなくて、そんなものあげたら、いろいろ動かなくなる恐れが。

なのであんまり Linux っぽくないのだが、leveldbb も source から build することに。

で、だいたい動いたんですが...

../lib/libkv.a(LevelDBStore.cc.o):(.data.rel.ro._ZTI17CephLevelDBLogger[_ZTI17CephLevelDBLogger]+0x10): undefined reference to `typeinfo for leveldb::Logger'
collect2: error: ld returned 1 exit status

なにこれ。どうも C++ の RTTI の関係らしい。Runtime type information ですか。leveldb 側が no-rtti で Ceph 側が rtti 。どうする?

あと、

[ 41%] Linking CXX shared library ../../lib/librados.so
collect2: fatal error: ld terminated with signal 11 [Segmentation fault]

SegV はひどいでしょ。

% /usr/bin/ld.bfd --version
GNU ld version 2.27-34.base.el7
Copyright (C) 2016 Free Software Foundation, Inc.

なにそれ。それは古すぎる。とはいえ、落ちるか普通。

というわけで、まだ、しばらく楽しめそうです。来週、読み会なはずです。

静的HTML

なんか、WordPress 追放したい的な説出てて。DB関連の接続がよろしくないのが理由らしいんだが... まぁ、キャッシュ挟めば感もありますが...

この前、WordPressのDBを見た時に Page 毎に table を作成しているのを見かけたので「あぁ、こいつはだめだな」ってのには賛成です。

PHP + SQL 生成って残念さといい加減な Plugin のせいで、2,3年前になんかやられたしな。

で、代わりに名前が上がってるのが、nuxt.js ですか。git push から trigger してHTMLを生成する方式。

まぁ、自分も WebObject + Apache を見て「Emacs outline から Perl scrtipt でHTML生成の方がまし」と思って24年なわけですけど。

静的HTML生成は劇的に軽いからな。

とはいえ、WordPress の特徴である複数ユーザによる協調編集はどうするの? ie-news みたいな掲示板とか卒研ページはどうするんだよ。

gitlab に push する script 書くってか? まぁ、トランザクション的にはたいしたことないけど...

そういうところは CMS の安直さが良いんだけどね。どうするんですかね。

https://nuxtjs.org

黒猫 in クロネコ

ちょうど良い箱らしい

沖倉利津子

実家から回収してきたものの一つ。少女マンガを読むのは男子学生の教養だからね。別マだったらしい。

90年のケンカ友だちが実質的な最後なのかな。家なき子のコミカライズがあるのか。

ケンカ友だちは完成度高いなという感想を持った記憶がある。

お隣のお兄ちゃんに育てられるセッチシリーズなのだが、高校以降の消息は不明。

一冊、欠けてるのを発見しました。おそらくは実家の本棚の裏に落ちてるんだろうな。

最近、このサイズだと目がつらいな。

雨の中を投票所に

県議員で、落ちるのは一人だけ。まぁ、でも勘定に入るのは重要だから。

投票所にいる人たちは、マスクとフェイスシールドで防御。しかし、それ以外は

　　人の配置とか手順とか、まったく変わらず

変わらないために頑張る人たちって感じですね。いいから、近寄るな! って感じでした。

なんで、わざわざ投票券を手で取りに来るのか理解できん。そういえば、投票ブースに鉛筆がなく使い捨てを手渡ししてたみたいです。

いいから、近寄るなってば。

LLVMの続き

去年からの懸案の clang 対応。Paeser 部分では CompoundStatement 、つまり、Cの {} が

　　RAII を使うようになった

のが問題を引き起こしていて。RAII とは

　　Resouece Allocation is Initialization

というもので、malloc/smart pointer を宣言で片付けようって奴。ARCもその仲間。Rust もそうかな。

関数の中で関数を定義するので環境切り替えが入るのだけど、そことRAIIの境界がずれて死ぬ感じ。余計にpopしてる感じ。

結果的には

　　{ RAII; ... }

というように {} で scope を追加してやると良いらしい。微妙な感じ。動けば正義か。

もう一つは tail call が出なくて死ぬいつものやつ。Parse時とcall生成時がずれるのでCallIsntのconsructorにcounterは挟んだ。

これで、生成時からParse時を追跡。でも、見つけてみたら、そこは普通の関数と同じ扱いをするべきところだった。はぁ?

で、hg blame してみると、5/30に、ばっちり自分で処理を削ってる。お前な〜 酔っ払いながらやってたろ〜

まぁ、protptypeがあわないとえげつないメッセージを出して死ぬっていうおまけはあるんですが、できたみたいです。

brewはcompileに1時間、bottleにするのに1時間40分。3GBあるみたい。LLVMのdebug binary でかすぎる。

LLDB + くそ Python

clang と格闘しているわけですが、

　　p Actions.getCurFunction()->CompoundScopes.size()
　　n

ってのを繰り返し実行したいんだけど。gdb の define みたいなのあるんじゃないの?

　　p Actions.getCurFunction()->CompoundScopes.size(); n

で良いんですが。ですが、できません。help command とかやってみるのだが。そこで、

　　そういうことしたければ python 書け、この馬鹿

と書いてある web page を発見。はぁ? python ってのは indent な言語なので

　　1行でいろいろ簡単にやる

ってのには絶望的に向かない言語なんだよ。なんでよりによって Python。

実際、この二つのコマンドを実行するってだけでも、

　　別ファイルに書き出した数十行の python class を作る

ってのが必要らしい。頭の良い人たちの考えることは理解できませんですよ。

https://stackoverflow.com/questions/14637074/lldb-alias-for-multiple-commands-as-one

Rust の exa

単なる ls なんですけどね。Rust で書いてあると言うだけ。

結果が Sum type で返ってくる(HaskellのMaybeみたいなの)のは良いかな。

lldb で trace するんですが、library が結構追えない感じ。なんとなく、

　　もっと、low level まで追いたい

感じはあるんだけど。RustのLibraryのソースコードを読まないとだめか。

でも、コード的には所詮、ls だよな。

& とか出てくるので、中途半端にCっぽいのが残念な感じかな。

mut とか clone とか、そこどうしてそうするの的な疑問が残る感じです。

＊ ＊ ＊ ＊

なんか Zoom で Browser上のページと、コ0ードを実際に動かす画面の切り替え方法で、

　　PCの画面の一部を共有にして、そこ切り替えるWindowを放り込む

というのをTwitterで教えてもらったんですが、FocusがZoomに取られてしまう。

なので、Window の一部を共有部分から外にはみ出させて、そこにFocusするっていう技を発明しました。

見てる方はどうだったんだろう?

5月で収まる説

3月頃にそんなのがあって。インフルエンザからの類推だったんですけどね。いや、コロナは夏風邪だから違うってな話だったが、

結果的には猛威を奮ったイタリア、NYでさえ収まってきたので正しかったらしい。もちろん、ブラジルとかロシアとかインドとか真っ最中なところもあるわけですが。

収まるメカニズムが不思議。インフルエンザの場合は湿気とか言われてるんですけどね。

まぁ、だとすると、また季節的に流行る感じかなのかな。

大学の使い方

徐々に院生は研究室に戻りつつあって、まぁ、時間わけて混まないように使えばってな感じ。

対面授業は別に僕はなくても良い派で、そもそも出席取ってなかったりしたからな。Webみて課題出せば良いよ的な。

そんなわけで誰もいなくて快適な大学もこれまでか。

遠隔授業で、自宅の環境が残念なのが明らかになった人たちもいるらしい。まぁ、

　　大学生にもなると親のいる時には家にはいたくない

ものだし。そういう時の避難場所としての大学の役割もあったと思う。

学生だけでなく、自宅から遠隔授業する羽目になった先生方の方の問題も。大して給料もらってるわけでもないから、

　　仕事部屋が取れない

ってのもあるらしく。いや別に

　　大学すかすかなんだから、大学に来てもらって、そこから遠隔授業すれば良いじゃん

と思うんですけどね。そう考えない非常識な人たちがいるらしく。

僕は動画な授業は意味ないと考える方で、自分が学生の頃のことを思い出せば、そんなの誰も見ないことはすぐにわかる。

それに放送大学のあれに勝つとかシロートに可能なわけもなく...

でも、ラジオ講座みたいなものだと思えば。

そんなわけでなので、自宅の環境が残念な人は学生でも先生でも大学に相談すると良いと思います。

あと、うちは MatterMost だが、Chat tool 積極的に使って欲しいかな。

LLVM/clang

build できるようになったので debug中。いや、あんまり言いたくないけど、

　　学生がいないのではかどる

というところがあるかも知れない。

LLVMは C++ で書かれていて、clang はC++のobjectを作っていくわけですが、中身がみれないって問題が。しかし、ぐぐってたら

　　std::string get_string(const Expr *expr, const ASTContext &Context) {
　　　PrintingPolicy print_policy(Context.getLangOpts());
　　　print_policy.FullyQualifiedName = 1;
　　　print_policy.SuppressScope = 0;
　　　print_policy.SuppressUnwrittenScope = 0;
　　　std::string expr_string;
　　　llvm::raw_string_ostream stream(expr_string);
　　　expr->printPretty(stream, nullptr, print_policy);
　　　stream.flush();
　　　return expr_string;
　　}

とすれば良いと。お、ばっちり。

　　(lldb) p get_string(E.get(),Actions.getASTContext())
　　(std::__1::string) $2 = "__builtin_longjmp"

どうも、tok::annot_non_type ってのが builtin とか用に追加されたらしく、それは扱いを変えないとだめらしい。

　Sema::NameClassification Classification = Actions.ClassifyName(getCurScope(), SS, II, Loc, Next, &CCCValidator);
　setExprAnnotation(IITok, Classification.getExpression());

ではなくて

　Sema::NameClassification Classification = Actions.ClassifyName(getCurScope(), SS, II, Loc, Next, &CCCValidator);
　setNonTypeAnnotation(IITok, Classification.getNonTypeDecl());
　setExprAnnotation(IITok, Actions.ActOnNameClassifiedAsNonType(getCurScope(), SS, ND, Loc, IITok));

とかするらしい。いろいろ謎だ。