Text Replacement 続き

なんか、一部、動かないのがあって。で、

　ls -l ~/Library/KeyboardServices
　total 2956
　-rw-r--r-- 1 kono staff 892928 Aug 31 17:14 TextReplacements.db
　-rw-r--r-- 1 kono staff 32768 Aug 31 18:10 TextReplacements.db-shm
　-rw-r--r-- 1 kono staff 1536792 Aug 31 18:09 TextReplacements.db-wal

sqlite3 なんですが、 これが、System Setting のUIとずれてる。これが原因か。

なので、sqlite3 を

　UPDATE ZTEXTREPLACEMENTENTRY 　SET ZPHRASE = '⁸', ZSHORTCUT = '\^8' 　WHERE Z_PK = 245;

とかやって手でなおすと良いようです。なんだよそれ。

正規部分群、部分圏

最初に随伴関手定理をやった時に

　　いきなり部分圏が出てくる

ので結構困って。だってマクレーンもそうなんだけど集合論抜きでやってるわけでしょ? なので、

　　圏Aで、Functor A A があれば、その像は部分圏になる

ってのを使ってた。Obj A と、その条件 P : Obj A → Set から作るべきなんだと今ではわかるが。

正規部分群でも自己凖同型があってとかやってたんだが、部分群よりも強い条件なんだよな。なので

　　凖同型定理が自明になってしまう

らしい。で、

　　正規部分群から、自己凖同型を作る
　　部分圏から、自己関手を作る

ってのを考えてたんだけど、非構成的ならありそうな気がする。逆に選択公理が偽ならなくても良い。

実区間の圏や群から開区間の部分圏や部分群を作るとか考えてました。

まぁ、気が向いたら書き直すかも。でも、凖同型や関手があるってのでもわかりやすくて良いかも。

Cisco Wifi firmware udpate

いや、さぼってたので。controller から update できるんだが、http は Certificate がどうこういってくる。

なので、firm をもらって tftp で。ところが、

　　tftp のところに folder fw を掘る
　　そこにもらった firm　は tar なので、tar xxf で展開
　　ファイル名には foler 名 /fw/ を入れる

なんですが、失敗する。g2 と g3 が混在するのがだめらしい。しばらく悩んだんですが

　　g2 外しちゃえ!

物理的に外すのと、swirch から POE を切るのとで強制的に。

これでばっちり上がりました。

g2どうしようかな。めんどくさいから捨てるか。共存できないの?

基礎とかいちからとか

いや、ちょっと、そういうの違和感あってさ。教科書って

　　最初の方を見ても良くわからない

そういうものだよね?

　　最初の前提がわかりやすいとは限らない

例えば、ニュートン力学は、 f = ma から習ったりするが、それは実はかなり後付け。

　　ローラーコースターは、元の高さより高くなったりしない

それは、そんなことが起きれば、それを繰り返して発散したりするから。それが

　　エネルギー保存則の基礎

だってことね。同じ状況なら同じことが起きるとか、そういうことが基礎になってる。つまり、

　　基礎ってのは、普通の世界の状況を言葉で説明できること

であって、わけわからない魔法の法則や公理の集まりことじゃない。そういうのをやりたければ、

　　Agda みたいな記号論理、高階直観論理をやれ

ってこと。反科学を基礎がわかってないとかいうのは間違いで

　　日常の状況を言葉で共有できていることを確認すること

からなんじゃないかな。まぁ、結論ありきな人たちだが、認識の共有を諦めたら、そこで終わりなので。

お休み〜

沖縄の世間的にもお休み

自分のやる気的にもお休みな感じ

まぁ、そういうのも悪くないかな

寝るのも仕事のうち的な

Agda and gitub copilot

いや、まぁ、あんまり期待してなかったんですけどね。neovim plugin で使うわけですが、

Agda って大半は自分で定義したもので、それは見てくれない。なんだが、

　　List とか Maybe なら得意だぜ

あ、そうですか。なるほどね。ただ、

　　もっともらしいが、違うものを持ってくる

のがなぁ。ChatGTP とも重なりますけどね。で、

　　え、有料なの?!

まぁ、Agda 専用なのもできるような気はするけど...

シス管の勧誘

最初にやってた頃は翁長先生が

　　「全員にやらせろ」

とか、それは無理だろって思ったわけですが、なんとなく4,5人、多くても10人はいない感じ。

長田先生は院生中心に「仕事としてやらせる」ようにしたかったらしいんですが、

　　見合う給料を出せない

問題があってな。中途半端な金額は残念。まぁ、お金でなくてもメリットあるし面白いとは思うんですが...

まぁ、情報が多いクラウドがいいんだろうなとも思うんだけど、使ってみれば無料分はしょせん無料分なわけで...

ってわけで、毎年勧誘に苦労してます。ボドゲ大会でもするか?! ま、

　　毎年、廃部の危機!

的なやつね。結局は一本釣り的なところがあるんですが、コロナで難しいところも。

今日の Ingress

なんか、kabtou 氏が 首里城間大謝名を取ってて

　　うらやまし〜

とか思ってたんですが、落とされたので「おかわりするか」で出動。

いや、別に勝算なかったんだけど。大謝名を修復したら、城間が落とされてて

　　なんと首里のキーがそこに落ちてる

甘いぞ、甘すぎる Punix! で、ばっちり取れました。

ま、すぐに落とされたけどな。

微妙に最大取得Muを更新。2万4千。前はいくつだったんだろ。

running remote agda

学生のノートPCだと非力で Agda が動かないなので、

VSCode から remote で server 上の動かせば?

と思ったんだが

　　WindowsのPowerShell -> Bat -> ssh -> apptainer exec

なんだけど、apptainer が

　　 Message from stderr when validating the program:
　　INFO: underlay of /etc/localtime required more than 50 (116) bind mounts

とかいう余計な stderr を出す。これを避ける方法がないので諦めました。

まぁ、singurarity の中の emacs で使っとけ。

だから〜

その、どっかで見たようなものを持ってくるのはやめろ〜

ゲーム班でも、スーパーマリオのコピーを作られたことがあってな。

まぁ、練習ならいいんだけどさ。でも、それなら一週間な。

検診の結果

まぁ、いままでと良くなってるわけでも、悪くなってるわけでもないわけですが

いくつか引っかかってるのはあるんだが、そのまま、かかりつけの内科の先生に渡したら

　　何か頭ひねってる

これなんだけど、とか紙を示すんだが

　　え、それは単なるゴミでしょ
　　ゴミねぇ

なんか、要再検査な紙が入ってたらしく。最後のおじいちゃん先生ろくに問診もせず聴診器当てただけだったよな。

で、二人で数値見るんだが、どこを検査すれば良いのかさっぱりわからず。事務経由で問い合わせても意味不明。

　　やっぱり、ゴミなんじゃないの?

心電図取るとか言ってるが、それ高校生の時から引っかかってるブロックでしょ。

猫はレタスが好き

なんでかね〜　猫草も好きらしい。あれは大麦か。

虫がわくとかで猫草は見送らしい。残念ね。

pointer authentication

setjmp/longjmp やってるわけですが、見なれない AArch64 命令が

->　0x198c88b24 <+0>:　pacibsp
　　0x198c88b14 <+96>: retab　

　　pacibsp (Pointer Authentication Code for Instruction, using the Baseline Key, with data from the Stack Pointer):
　　retab (Return with Authentication):

まぁ、いろいろ考え出すよな。stack overflow とかで return oriented やられるのがいやってのはわかるんだけど。

Side channel 系の攻撃でも「侵入されて任意のコードが実行される前提」とかだしなぁ。

関所作るなら、そこじゃないんじゃないか? お前たち、

　　プログラムの正しさを証明する気ゼロだろ

ってわけですけどね。そういえば、

　　MD5 は速すぎるのが悪だから、もっと遅いの使え

とかも見かけたな。まったく... 普通に12文字なパスワード使ってください。いや、パスワードもうやめて。

勉強会のやり方

いろいろやってたな。高校時代も読書会とかいって、本を指定して集まって議論するとかやってた。

学部時代も読書会はいろいろ。文系の本が多かった。クワインもそれ。

でも、割と薄い教科書を複数人で問題含めて3日で片付けるってのが面白かった。相対論とか量子力学とか。

ノーベル賞受賞論文とかもいくつか読んだような。

院生時代になると本職なので、分厚いのをやる。これも楽しかった。

自分の研究室だと自分の知ってるものをやろうかという気になかなかならなかったかも。

でも、コード読んだり、Proofs and types 読んだり。

そういう地道に読んでいくしかないという感じではある。

次は何読もうかな。

gpgsm again

いや、先々週に使ったばかりなのに、なんで動かん...

　　% gpgsm --debug-ignore-expiration --recipient 'xxxx@ie.u-ryukyu.ac.jp' -a -e ~/src/CA/tmp-os/1342.tmp
　　gpgsm: checking the CRL failed: End of file
　　gpgsm: can't encrypt to 'xxxx@ie.u-ryukyu.ac.jp': End of file

良くあることなんで、githubから　build しようとしたら、libassuan がだめ。

libassuan ってのは gnupg だけが使っている IPC library らしい。そういうのは一緒にして欲しいところ。

なんだけど、

　　Options controlling the security:
　　　　 --disable-crl-checks　　　　　　　 never consult a CRL

ってのが付いていた。

　　% gpgsm --disable-crl-checks --debug-ignore-expiration --recipient 'xxxx@ie.u-ryukyu.ac.jp' -a -e ~/src/CA/tmp-os/1342.tmp
　　gpgsm: CRLs not checked due to --disable-crl-checks option
　　-----BEGIN ENCRYPTED MESSAGE-----

ばっちりだ。Revoke 関係らしい。無視でいいかな。

LLVM CbC の続き

builtin setjmp は書いてみたんだが、そこそこ大変そう。

一方で、当然なんだが、CbC の例題を setjmp/longjmp で書き直すのは楽勝。で、

　　問題なく LLVM16 で動いてる

環境付き goto を落とせば実装は小さくなるので、そうする方が正気かも...

もう少し考えてみるかな。

原神の心海

神里綾香と相性良いらしく。水が少し足りないってのもあって。いや、モナも行秋もいるんだけど。

久しぶりに Lv90 まで育てるのが楽しい。最近、ちょっと飽きてたからなぁ。

といいながら、一週間はかからないのか。

そういえば、雷電将軍の人形を見かけました。ちょっと欲しくもないこともなかったが...

Aarch64 の builtin_setjmp

CbC側からCに復帰する部分なんですが、まぁ、setjmp/longjmp で良いわけで、要らないという意見も。

理論的には、たんにreturnするので良いはずだったり。まぁ、つじつま合わせではある。

GCCでは nested function 使ってるんですが、LLVMにはそれはない。sp/fp をいじれば良いだけなんだが、

GCC/LLVMとも「frame pointerなし」ってのをやりたかったらしく、直接 fp に触れない。なので、

　　LLVMでは諦めて、setjmp 呼び出した

んですが、setjmp.h を読み込むのはあれなので、builtin_setjmp にしたという流れ。そこで、

　　Aarch64 の builtin_setjmp は実装されてない

ってのはあんまりだと思うんですけどね。たぶん、既に実装はされてるんだが、なんかの問題があるんだろうな。

いろいろ選択肢はあって、

　　1) Aarch64 の builtin_setjmp を実装する
　　2) setjmp.h 使えば良いので、仕様から落とす

まぁ、後者が楽ではあるんだが...

いつもの LLVM / clang

自分の道具だからな。LLVM13からLLVM16。一気に最新まで上げたい気もするか、まぁ、ゆっくり。

でも、mergeする時に間違えて take other してしまったので、

　　ほぼ手動で merge する羽目に

まぁ、でも見直しできたから良いか。M2の学生と一緒にやってるんですが、

　　ちまちま、mergeを修正

していくわけですが、

　　「これって、無限に続くんですか?」

いや、それはないんだが.. と言ったその場で link まで通りました。そんなもん。

一昨年あたりに Preprosessor あたりをいじったんだが、そこがばっちり修正入ってて少しはまりました。

コンパイラの中から直接文字列なCのコードを使えるようにしたので、それを使って全体に簡単にしたいんだが、

　　なかなか難しい

感じ。Intel compilerがLLVM baseになったとかの話も聞きましたが、どうなんでしょうね。

窓の続き

いや、なんで、6Fの窓が割れるんだよ。割れた部分を取りさって、あとで修理ってことね。

プロ3の発表もなんとか。いろいろ文句はあるが、まぁ、完成品を持ってくるところはすごい。あえてページは貼らないが。

修士の方は、前のでできたと思ったが、GPUを呼び出してないことがはっかく。どういうこと? pytorchの build で Cuda を認識してないのか。

まぁ、C++までは到達しているので、あと一歩だな。

いろいろあったが、前期の授業は終わり。

　　久しぶりに青空を見ました

6階の窓

工学部1号館の6階の窓が台風で割れたらしく、そこだけ5-7階階段閉鎖。

いや、屋上に怪しいものが置いてあるので、そのとばっちりか? あるいは開けっ放しでやられたか。

とはいえ、珍しく台風で停電しなかった。どうも送電線が地下になったからとかいう説を出している人がいるみたい。

台風のコースは気圧配置で決まるので、今年は、まだ、いくつかくるかもな。

Github Copilot and ChatGPT 4

Copilot は neovim の plugin ですね。両方共、金取るのかってのあるが、広告入れるわけにもいかんしな。

まぁ、税金と思うか説もあるが、両方は重複してる感じがある。

Agda はなんも出ないだろって思ってたんですが、

　　Hoge : ?

に対して、Hoge = ? ぐらいは出す。なんだが、

　　外れの再帰を出してくるのはやめろよ

Agda だと、一致しているかどうかの判断がかなり重いので邪魔感がある。

OSの授業なら、かなり役に立つんじゃないですかね。Copilot は切っちゃうかもな。

台風でお休み中

東京には、また、そのうち。うちでゆっくりするのも悪くはないし。

最初ほどではないですが、出歩くほどでもなく。ただ、

　　スーパーに食材が戻るのは少しかかりそう

CSSと格闘

だいたい、Webのmarkdownへの移行はすんだんですが、いろいろ細かい問題が。例えば、

　　上部の部分の画像がPCの時だけ両端が空く
　　下部のおしゃれなメニューが崩れる
　　日本語から英語に移行したあと、日本語に戻ってこれない

いや、そもそも裸のHTML/CSSはいじらんだろって思うが、WordPressで生成したHTMLを
reverse enginieering して、Hugo Theme にしてるのでそうなる。

まぁ、なおったんだけど、要するに

　　生成用に分割した html / css / javascript のファイルの順序

の問題。なので、いくつかの css 定義を移動したらなおりました。

Browser の開発モードから、この値はどのファイルに書いてあるってのを探せるから、それほど難しくない。

なんか、container とかの名前が微妙に再利用されててな。

まぁ、一度、Markdown 化してしまえば、AstroでもNext.jsでも移行は簡単なはず。

でも、昔の学生の作ったものとはいえ、今のはそこそこ良くできていて、今の学生には難しいなと思いました。

それだけに、あっさり捨てられてださいのになるのはな。いや、既に一部やられてるし。実用的には問題ないが、

　　デザインの悪さを気にしない

のは日本人の悪いところだと思う。

Bleach 千年血戦編

いや、既に第二クールなはずなんですが。なんか、いまいち気がすすまなくて。

少しお休みしてたんですが、やっとみました。

というくらいエンジンかからない話ですが、ちゃんと盛り上がりました。

このために復習したわけだしな。まぁ、なんか漫画は全部揃ってるらしいんですが。

父親とかが出てくるのはワイドスクリーンバロックの定番だしな。

でも、先は長いらしい。

Bleach は歌も良いね。エンディング。

pytorch gdb debug

なんか、やっとできました。要するに、

　　libtorch*.so

を LD_LIBRARY_PATH で切り替えることを防ぐ仕組みがあって、install してからでないと gdb できないわけね。

あと、

　　apptainer 1.1.7 の --fakeroot --writable がバグってて動かない

ってのもわかりました。singularity でやったら動いた。時間の問題だとは思うけど。　

　　cd /opt
　　# build pytorh
　　git clone --recursive https://github.com/pytorch/pytorch
　　cd pytorch
　　git submodule sync
　　git submodule update --init --recursive
　　pip install mkl mkl-include
　　# pip install magma-cuda110
　　pip install -r requirements.txt
　　mkdir -p /opt/pytorch/build
　　cd /opt/pytorch/build
　　cmake .. -GNinja -DCMAKE_INSTALL_PREFIX=/opt/pytorch/torch -DPYTHON_EXECUTABLE:FILEPATH=/usr/bin/python3 -DPYTHON_INCLUDE_DIR=/usr/include/python3.10 -DCMAKE_BUILD_TYPE=Debug
　　ninja
　　ninja install
　　cd /opt/pytorch
　　python3 setup.py develop

できてみれば、どうってことない。なんで、こんな苦労したんだか。

　　singularity shell　--nv --shell /bin/zsh pytorch.sif
　　gdb --args python3 ~kono/src/pytorch-test/ttest.py
　　Thread 1 "python3" received signal SIGINT, Interrupt.
　　[Switching to Thread 0x7f703d224280 (LWP 2849215)]
　　c10::TensorOptions::pinned_memory (this=0x7ffeb2bf44c8, pinned_memory=...) at /opt/pytorch/c10/core/TensorOptions.h:261
　　261　　　 }
　　(gdb) l
　　256　　　 C10_NODISCARD TensorOptions
　　257　　　 pinned_memory(c10::optional<bool> pinned_memory) const noexcept {
　　258　　　　 TensorOptions r = *this;
　　259　　　　 r.set_pinned_memory(pinned_memory);
　　260　　　　 return r;
　　261　　　 }
　　262
　　263　　　 /// Sets the `memory_format` property on `TensorOptions`.
　　264　　　 C10_NODISCARD TensorOptions
　　265　　　 memory_format(c10::optional<MemoryFormat> memory_format) const noexcept {
　　(gdb) bt
　　#0　c10::TensorOptions::pinned_memory (this=0x7ffeb2bf44c8, pinned_memory=...) at /opt/pytorch/c10/core/TensorOptions.h:261
　　#1　0x00007f7033f85bab in torch::autograd::THPVariable_ones_like (self_=0x0, args=0x7f6eae15ee00, kwargs=0x7f703cfaa580)
　　　　at /opt/pytorch/torch/csrc/autograd/generated/python_torch_functions_1.cpp:4836
　　#2　0x0000559eece47c9e in ?? ()
　　#3　0x0000559eece3e72b in _PyObject_MakeTpCall ()

風邪で死んでたので、Web pageの続き

でも、まぁ、熱はだいぶ引いたので。

学生が作ったトップページので、巨大なバナーがあって、その「中に」なんか配置されてるらしい。

そういうのはなぁ。なので、その大きさに引きずられて中のいろんものが下に落ちてるらしく。

それで、下に filler を挟むかと思ったんだが、grid とか flex とかでわけわかでした。

まぁ、できたんだけど。

　　iPhoneと MBP をケーブルでつなげて、iPhone側のSafariをMBP側のSafariの開発モードで開ける

なんてことができるのか。知りませんでしたよ。(知らない方が良かった...