美栄橋のエリーカレー

11月から移転だったので冷やかしに。美栄橋とてんぶすの間くらいの場所かな。

そこにあった中華のお店はなんかしばらくお休みらしく。そこに昼間だけお店を出すという感じね。

メニューも少し変えたみたいですね。宜野湾からだとちょっといきづらいかな。

そういえば、普天間の「月を詠む」のカレーにも行ったのだった。

まぁ、そういう、ちょっと辺鄙な場所に、お昼だけのお姉さんのカレーのお店っていうパターンがあるのかな?!

コロナワクチン5回目

ワクチンは自分のためでなく社会のために打つものだからな

いつものように特に何もなし

今回もファイザーでした

インフルもやってたので頼めば同時に打ってくれたかも

CとPOSIX API

これも OS の課題なんだけど、system call なので、構造体を渡すわけですけどね。C は良いんだが、

　　Rust も go も、そこに距離がある

見れないわけじゃないんだが、memory dump みたいな感じ。いや、

　　そこは知らなくてよい

ってのはあるとは思うけど、OSの授業だとちょっとそれは通らないかな...

まぁ、Cを病的に避けても仕方ない。まだ、Linux kernel は C だし。

Perl とかは C の header からの converter とか持ってて任意のsystem callを呼べたりしたんですけどね。

Rust compiler 読み会完結編

今回は準備がほぼ完璧だったので、読むこと自体は簡単

ただ、trace はできるんだが、p で表示ができない。なんでだろ。

もっとも、そこら中に debug が埋め込まれていて、環境変数で制御できるっぽい

　　もはや、gdb とか誰もつかってない説

なんかすると読めるようになるのかも。Debug用の関数とか作るのかな。

fn とかをparseしてるところもわかった。

　　extern "C" LLVMValueRef LLVMRustBuildCall(LLVMBuilderRef B, LLVMTypeRef Ty, LLVMValueRef Fn,

とかで LLVM を呼び出してるらしい。

　 b rustc_interface::passes::parse
　 b rustc_codegen_llvm::builder::Builder::call_intrinsic

とか簡単にできるのは良いかな。

まぁ、メタ部分どうするかとか先は長そうだけどな。

Rust compiler 読み会

結局、(ほぼ)一人でやってるんですが、

なんか、サーバから抜ける時に、Ceph が文句を言うんだよな。file system full で file が remove できない的な。

ぐぐったら、どうも mds_bal_fragment_size_max があふれるらしい。なんと、このパラメータは、

　　個々の mds にあるらしく、そのサーバの cephadm からでしかアクセスできない

あっそ。このパラメータいじるんですか? まぁ、あとにしておくか。どうも、

　　pythonとか rust とかが作る、$HOME下のきょだいなんとかがよろしくないらしい

あーいうの、共有環境を考えてないからなぁ。いや、がんばっていろいろ指定するんですけどね...

今日は、Rust の復習だった。あしたもやるけど、まぁ、趣味だな。

Rust compiler debug 用の singularity

なんかやっとできた。2020に一回やってるんですけどね。忘れはててる。

どうも、そのときに、.def をちゃん書かずにやったらしく、いろいろ失われた情報が...

config.toml を修正する sed は間違ってたりとか。あと、

　　なぜか、stage1 しか、source code debug できない

とか。stage0 はだめなのはなんで?!

5.4Gかぁ。まぁ、大学でコピーするなら、まぁ。stage2 まででも20分くらいで build できるらしい。

LLVMは入れてないから。LLVMどこからもってきてるんだろ?

まぁ、あとはあしたね

明日から...

プロシンの論文書いてるんだが、なんか進まず...

とかいいながら、明日からRustのコンパイラ読むのか? まぁ、明日は準備なだけなんですけどね。

たぶん、singularity で Rust compiler の debug 環境を作るはずです。3時からとかだと思う。

土日でどこまで読めるかはなぞだな。録画して編集しても良いが、自分で編集する気ははなぁ。そういうの

　　AIがやってくれないの?

すっころんでズボン破きました

またかよ〜 (今回は録画なし

琉大周辺、山道だからなぁ。うっかり膝ついちゃって。

原神のフリーナ

フリーナの話は割と良かったかな。フォンテーヌの裁判の話はかなりかったるかったし、リオの監獄の話も唐突で。

まぁ、でも、そういう風に落としますか。フリーナの評価が前半と後半でまったく変わるのは面白い。

英語でやってたりするんで、かなり読み飛ばしてるので話はあんまり観てないんだが、珍しくちゃんと読む気が出た感じ。

いや、これが日本語だとわざとら感があって微妙なんだよな。

まぁ、どっかで見たような話ではあるんだけど。シュタゲとか蟲師とか。神様の本質的の物語でもあるな。

iPhone で見てると、Youtubeのまとめの方が綺麗って問題があるな。

フリーナはガチャでもすり抜けなかったので、育成中。水のあれと、くじらに割とやられてます。

カヌチャリゾート

まぁ、普通の東南アジアのリゾートをそれなりに。今では「安い」というメリットがあるかも。

空いてるときを狙って11月にしたんだが、空いてて気持ち良かったです。

まぁ、どこにいってもやること同じ説はあるのだが。

夕飯は、ノスタルジックな感じが良かったな。

名護市のスタンプ

なんか、名護市のせこい旅行キャンペーン用のスタンプらしく。500円払うと1500円もらえるらしい。

(1) 名護の道の駅のおばさんに話しかける

(2) めんどくさいWebから、くれかの情報を入れる

(3) 名護のキャンペーン対応のレジで携帯のWeb pageを表示した状態でスタンプを押してもらう

(4) ひとりにつき、1500円割引

このWeb page がくせもので「一度表示を消すと二度と探せない」 (2)で tab で取っておく。

面白いのは(3)のスタンプ。物理的なものなのね。無線チップだろうと思うんですけど。

いや、そのおばさんに現金配らせた方が良いんじゃないの? クーポン券でもいいけどさ。

　　原神で話しかけると、なんかもらえるNPC

みたいなもんでしょ。

これで1万円とかならともかく、千円? しかも、

　　わけわかんない物理デバイス?!

(1)のイベントが必要な理由もよくわからん。付き合ってるおばさんも偉いような気もする。

年末進行中

11月はいろいろイベントがあって、そこそこ忙しい。

いろんなイベントがある扉。普天間のキンタコ。

全然、開けられません

どーなんてんの〜
-

ARG_MAX

OSの課題なんだけど、「自分の書いたプログラムファイルを全部 wc する」ってな課題ね。

　　wc $(find src -name '*.pl')

は不可にしたりするんですけどね。昔は ARG_MAX が 99 だったりとかしたりするので。なんだが

　　% getconf ARG_MAX
　　1048576
　　% getconf ARG_MAX
　　2097152
　　% getconf ARG_MAX
　　262144

だったりするわけですよ。まぁ、じゃぁ、正解でもいいかなと思うじゃないですか。ところが、

　　数が大きくなると遅い

え〜 いまさらそれ? いや、これは単純にappendすると O(n²) な問題がちょっとある。allocate しないとだめだから。

xargs で良いわけだったりするんですが、まぁ、ちょっと遅いくらいだからいいじゃんとか、測れよとかあるにはあるが...

ps agx の g みたいな無意味な手癖になりつつあるのかも。

Ingress Recursion

4回目。AP 倍と Apex で。楽勝で Lv8 ですね。

どっちかっていうと、Level が上がる時の item が邪魔。

ずーっと、Level 16 でやってるよりはいいかなくらい。

Apex 100貯まってるんですが。

掛け算の順序

なんか、昔にも blogに書いたことがある。良くある順序が違うとバツを食らうってやつなんですが…

なんか、どうも

　　掛け算に順序はない

ってな標語になっているらしく。それは変なんだよね。というのも

　　掛け算の定義は、足し算の繰り返し

で非対称なわけで。いくつか対称な掛け算の定義を agda で書いてみたんですが、どうも

　　交換則の証明抜きには無理

らしい。それほど難しくもないが、小学2年には厳しい感じ。まぁ、掛け算の順序を問いたいなら

　　何を何回足したのか

と聞けば良いだけなんですが。x * y でどっちが回数かは日米で差がありそう。ところが

　　累加は掛け算の定義じゃない、ペアノの公理は的外れ、ab と ba は同じ

とかが降ってくる。なんなの?

まぁ、累加は読み替え可能。例えば、

　　鶴の右足を数えてから、左足を数える

みたいなやつね。生徒が逆に書くのは、だいたいそれ。

ところが、その読み替えでも結果が同じになるのには交換則が必要。なんだが小2ではそれはまだない。まぁ、

　　交換則は経験則でも良い

ってのを言う人たちもいるんですが、それって九九の延長ってこと? もしかして

　　掛け算は天から降ってきたものなのか?

読み替えはプログラムの二重ループを入れ替えるみたいな話なんだが、メタ計算で順序は外から見えてしまう。

　　3m/s² で 5sec 加速と、5m/s² で 3sec 加速

は違う現象で可換にはならない。到達位置が違う。でも到達速度は+15m/sなので普通の掛け算なんだが…　と言ったら、

　　それは掛け算じゃない、次元が違う、単位が分かってない

この場合は、時間の方が回数っぽいよね。読み替えで順序を交換できるかというと、できなくはないんだが

　　激複雑な操作になる。それで、到達速度が一致するのはむしろ不思議

いや、それは交換則で保証されてるわけだけど(相対論では、ずれる)。で、どうも

　　掛け算は九九で無理やり覚えるという状態になる生徒がある程度いるらしい

確かにそれだと天から降ってくる感じ。いや、一階述語論理の関数の意味は実際そういうものだし。＊＊＊ そこか?! ＊＊＊

それだと文章題に掛け算を対応させるのはChatGPT的な確率マッピングになる気がするので、やっぱり、それなのかなぁ

つまり、掛け算を実在論的/イデア論的な「人の外にあるもの」で、その意味は神のみが知っているってな立場の人がいるらしい。実際、

　　ペアノ流の掛け算の定義を押し付けるのか?!

とか言ってくるわけですよ。いや。交換則押し付けてるのそっちだろ。証明しろよ。

直観主義論理は唯名論的なので、人間が知る記号ゲームが人の限界みたいなところがある。そこではペアノ流の構成になる。

ま、ネットで炎上する議論は、存在論の争いなことが多い。シロートが参加しやすいし、実在論は声が大きい方が勝つ的なところがあるからな。


　

カレーパーティ

611にいる学生達が来てくれて、そこそこ。

前日の手伝いが来てくれなくて、またゆ〜一人だったのは厳しかったが。

まぁ、一人いれば20人分くらいはなんとか。

　　チキンカレー
　　キーマカレー
　　カシューナッツとエビのカレー
　　マトンビリヤニ
　　チャツネ
　　タンドーリチキン
　　パパド
　　パニプリ
　　ラッシー
　　チャパティー

カレーの準備

キーマカレー、チキンカレー、エビとカシューナッツのカレー

まで作りました

明日はお昼からかな

別世界への扉

首里あたりにあるらしいです

agda safe mode

{-# OPTIONS --cubical-compatible --safe #-}

をつけると良いと言われているらしく、せこせこなおしてるんですけどね。

postulate はだめとか、functional-extensionality はだめとか。

それを拒否するわけでもないけど、分離できるならそれがいいかな。

fiso← : (f : R → Bool ) → ffun← ( ffun→ f ) ≡ f

と書きたいわけですが、これだと、functional-extensionality が必要。なので、

ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x

こんな風に「関数が等しいのは、すべての要素で値が等しい時」みたいに書き直すらしい。

これでも対角線論法は書けるのか。

麻雀

学生が研究室でテレビゲームしたりボドゲしたりするのは大目に見てるんですが(国田先生は良く思ってないらしい)

でも、

　　麻雀は禁止

ま、当然かな。別に理屈じゃなくてだめ。前にも取り上げたことがある。うるさいんだよね。寮とかでやれよってなところです。

むかし、東風荘が学生の間に流行ったことがあって、授業中にやってるのとかがいたな。

gitlab ci and git submoudule

gitlab ci で、submodule として使ってるもの(例えば、hugo theme とか)が古いのを参照してしまうのではまって。

　diff -r ie-hugo/.git/modules/themes/ie-hugo-theme/FETCH_HEAD ie-hugo-bad/.git/modules/themes/ie-hugo-theme/FETCH_HEAD
　1c1
　< 87f2c9104beede26b830162de860ffa99085d3bb branch 'main' of gitlab.ie.u-ryukyu.ac.jp:ie-syskan/ie-hugo-theme
　---
　> 0f21c8e7c80a63256094e41f4e07572945a94cb8 not-for-merge branch 'main' of https://gitlab.ie.u-ryukyu.ac.jp/ie-syskan/ie-hugo-theme
　diff -r ie-hugo/.git/modules/themes/ie-hugo-theme/HEAD ie-hugo-bad/.git/modules/themes/ie-hugo-theme/HEAD
　1c1
　< 87f2c9104beede26b830162de860ffa99085d3bb
　---
　> 273a8492477c556f070431440289596ea7cc4fb3

あたりで、おかしくなる。

　git submodule sync
　git submodule update --init --recursive
　git commit -a
　git push

あたりでいいはずなんだが、どうも、前のを gitlab-runner が覚えているらしく...

いや、submodule で、こういうの覚えるのどうなのかなぁ。気持ちはわかんなくはないが、固定したいなら、むしろ指定するとかの方が。

まぁ、しばらく格闘したらなおったわけですが。たぶん、なんか間違ったコマンド打ったな。

LISP09

8bit 時代のLISPですね。Microware OS9 で動かそうと。

なんだが、手元の a09 が macro support なし。なんだよ。os9 上のアセンブラでも良いんだが...

Perl で展開しちゃえ。で、アセンブルは通ったんだが、

　　メモリマップが変

TL/1 でもそうだったんだけど、初期定義(NULとかTとか)をなんとかしないとだめなのか。

元のソースはFLEXだし、そのままのmemory map で動かしても別に問題はないんですけどね。OS9 Lv2 だし。

まぁ、動くとは思うけど、あんまり意味はないかな。Scheme 構文になおしたい。

GAME09もそうなんだが、U stack と S stack 両方使うのは良くない。Sだけでやるべき。でも、それをやるのはむなしい。

最近の ingress

Discoverier の 30 Kinetic はやっと取れました。買わなくても余裕。

Liberator 黒がだいぶ前に取れていたらしい。気がつかなかった。次は Engineer かな。

Mod 入れは sheild 一つくらいだが、年内には取れるかも。

Lv16 も年内かな。いつものパターンで、即 Recursion だと思います。

沖縄は最近は緑が弱すぎ問題がある。いや、青が頑張りすぎなのか。

老人介護的なところもあるけど、まぁ、見かけたら落とすようにはしてます。

モンハンはポケモンと同じで自分は世代じゃないんだよな。Ingress は問題あるところもあるけど、

　　歩くモチべ

なので、なるべく歩く方向で。そういえば、はちれんも復活したので、佐覚下公園にいく理由があってよい。

ぼろぼろな背広

いや、ぼろぼろの方が着心地が良いって問題があってさ。パジャマとかは

　　穴が開いてるくらいが良い

のだが、スーツはそういうわけにもなぁ。ズボンは二本作ることも多いのだけど、上はね。

でも、MBP16持ち歩くから、まぁ、もたないですよね。

コンパイラ読み会

今年は、11/25-26 (10:00-12:00, 14:00-17:00) でやります。

　　LLVM / Rust と Agda

の予定。全部は無理なんだが、必要なさわりだけ。

いまどき、C でもないだろって感じで、CbC を Rust に入れられるかどうかを考える感じですね。

簡単にできそうなら、やっちゃいますが...

一応、授業なんですが公開でやるつもり。もしかすると、一人 Zoom かも。

π calculus

なんが学生が話題に出してて。どこで見つけてきた? 自分が手元にもってるのは、

　　Communication and Concurrency

ですけどね。自分は Clocked な Temporal logic やってきてて、その頃は λ calculus はやってはいたけど、

　　CCS 何もの?

ってのは結構あってな。慶應の人たちとお勉強したのは懐かしい。今、見直してみると、

　　並行動作するλ項の操作的意味論
　　仕様記述の時相論理

別に普通っちゃ普通。bisimulation よりは language containment ってのは用語の違いだけか。

Temporal logic of actions ってのもあって、みんないろいろ発明するものでもあるらしい。

ただ、なんか画期的な定理が示せたでもないんだよな。やさしくないってことか。

今扱ってるのでも、Agda で途中まで書いたんだが、どうも

　　途中で、検証ループに落ちる

ところがあって放置してるんだけど、もしかすると停止性の問題かも知れない。

ω automaton は、ℕ → Set みたいな形で書いてはみたが、まだ、あんまりうまくいってないかな。

まぁ、そのうち、なんか降ってくるかも。

歯医者さん

なんか、まわりで歯医者にいく人が何人か。そういえばパスしてたなと思って、クリーニングの予約したら

　　15分後が開いてます

あぁ、いや、それは無理(少し考えた)。で翌日にしたんですが、

　　もしかして歯医者さん暇なの?

クリーニングは1時間。割と疲れました。でも、

　　確かに、歯の色が白くなった

ホワイトニングしてもらったわけでもないんだが、最近、割といろが付くようになったかも。年か。

3ヶ月、いや半年に一回でもクリーニングしろとか言ってたので、確かに暇なのかも。

歯自体は、歯茎を含めて絶好調な感じ。なんでかな。