安物ヘアピン

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

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

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

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 による証明

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