大晦日

日曜日と重なっているので、飲み屋さんで開いてるところも少なく

家飲みですね

今年は、良く飲んだかな

まわりには、飲みすぎで fade out した人もいるので、気をつけよう

カレンダー

よりどりみどり。

年賀状とおなじですたれいく習慣とは思うんですけど、

　　家や職場、研究室に、文化的なものが置いてある

ってのはよいと思う。街にも、ingressのportalになるような、意味不明のものをたくさん置いてほしい

カレンダーは寄付とかできるみたいな話も聞いたな。

Dune

なんか学生達の何人かが最近の映画のを観たらしく。まぁ、

なんの知識もなくあれを観てわかるのかと言われると... でも、

　　なんかすごい

とは思うらしく。自分も二部は楽しみなんですけどね

もちろん、日本語と英語と、あと making book と、Dune Encyclopedia までもってるわけですが

拡大再生産で残念になったところもあるけど、救世主、子供たちまでは読むものかな

神皇帝の完結感がいまいちなのが残念

とか考えると第一部だけでいいのか。それでも充分量多いからな

Marantz NR1200

まぁ、レシーバだが、居間で使う汎用だからしかたないか

なんだけど、かな設置してくれたんだが、

　　レコードの方が、まだ調子悪い

ネットのはわりとちゃんとしてる。ってことは、Accuphaseのアンプのせいではなかったのか

なんか、特定のところでビビッたりするんだよな。たぶん、

　　レコードプレイヤーが鳴ってるのでは?

おそらくは、なんか低周波とかそんなの。あるいは配線不良。Techniqs 1200欲しいような気もするしな

設置方法良くないしな。

というわけで、いろいろやる楽しみがあるようです

Okitの人と meeting

いや、向こうはぼくのこと良く知ってるらしいんだけど。ぜんぜん思い出せないです。

基本ネットの人だからな。イベントかあるいは、オンラインだけのつながりか。

Facebook ではつながってるんですけどね。

でも、いきなり

　　Abaddon って話が。まさかの ingress つながり?

また、なんか那覇で ingress のeventあるらしい。そういえばサーバとめてしまったのだった。

なにか連携できればよいんですけどね。

とりあえず、これらしい。

https://ricc.itrc.net

まだまだ続くかけ算の話

なんと算数の教科書では

「1あたりの数」×「いくつ分」＝「全体の数」

で「定義」されているらしく、累加じゃないらしい。いや、これでは計算できないと思うんだが、

アレイ図と分配法則と九九で、無理やり筆算。なるほど。

確かに、これではかけ算の定義を答えられない人は多いかも。複雑すぎる。なので「計算すれば分かる量」
くらいの認識なんだな。

「日本では、遠山啓の数教協の影響で、伝統的な、同数累加の定義が批判され、教科書でも1980年代に、同数累加の定義が駆逐され、同数グループがメインになりました」

おぉ、そこかぁ。僕はかなり古いので、累加で習ったかも。

この時期、割と集合論が流行ってて、代数系の先生が累加でなくてもいけるってのを流行らせて、それが教科書になったらしい。

なので、かけ算の定義を「足し算の繰り返し」と言えなくなったというわけね。

まぁ、おまけ的には書いてあるらしく、自力で発見するとは思うんですけどね。

でも、その定義でも対称ではないので、かけ算の式の順序を問う問題は可能。それがまだ議論を呼ぶってわけ。

単位のサンドイッチ、左分配則右分配則にも同じ問題があるらしく... 対称じゃないからな。

プログラミングあるいは直観主義論理からの算数教育の見直しはあるんじゃないですかね。

かけ算の順序 禁則事項編

その後、「かけ算には順序はない」派の人たちと話てて、驚きの事実が。

かけ算から順序を落とすには、一度、累加でかけ算を定義した後、定義を忘れて
一階述語論理的な二項関数として扱うってのがあるんですが、それを実行している人がいる
いや、僕も信じられないんですが... つまり、反順序には禁則事項がある。

いや、むりむり。こんなの守って算数/数学なんてできないです

# 禁止事項1 かけ算の定義

つまりかけ算の計算を諦める。これでも半環の性質は使えるので、ある程度はいけます
15x3=20 に反論してって言ってもできない。(ほんと、聞いたけど答えられない

# 禁止事項2

かけ算の性質を持つ対象のグループ分けに注目する

これは「かけ算の順序を問う問題」には正誤はないことの要請に対応してる。「どっちでもいい」ね

これで累加が禁止されて禁止事項1が出てくる

# 禁止事項3(2の別形式)

累加の定義は順序があり、回数をどちらにするかでLR二種類ある。累加だと違いがある

その二つは違いがあるとすることは禁止事項

# 禁止事項4(2の別形式)

この時にL⋁Rを使ってLやRを直接は使わないという逃げ道がある。あるいは「いったん」使って良いとすると少し強くなるが累加よりは弱い

なるべく半環として扱うみたいな感じ

# 禁止事項5

単位があるかけ算は単位のある定数に無次元数をかける形式に変形できる(単位のサンドイッチ)

変形までは許される。それを足し算の繰り返しと見るのが禁止

これは単位のサンドイッチに関する問題に正誤はないことからの要請

さらに、分配則に制限があって、

# 禁止事項6

右分配則や左分配則からは、累加の定義が出てくるので使用禁止

つまり、スローガンのできがわるいわけね

OSの教科書の問題

いつものSilberschatzなんですが、去年と違って Kindle もある。なんだが、

　　Kindle 版の方が若干削られてる

そういうのどうなのよ。どうも、Windows 7 関係の問題が削られているらしい。

いや、あの問題、ちょっと問題有だったからなぁ。

　　Windowsの defered procecure call

いや、そんなのどうでもいいよ感。まぁ、本文には書いてあるので、読めば解けるんだが...

ChatGPT で fork / posix_spwan の例題とか瞬時に書いてくれて、一発で動く

自分のOSの課題を解かせても、そこそこいく。学生の学習も捗ることだろう〜

自分の解答をChatGPTで採点してから出せという感じにしました。

　　ChatGPTの解答をChatGTPに採点させて、その採点が妥当かどうか判断しろ

的な話だな

　　

年末プログラミング、なにしようかな〜

別名、年越しプログラミングですけどね

去年は、Zornの補題の証明が12/18までかかって、そこそこ面白かった

いや、そんな悠長なこといってないで、いろいろやることはあるんですけど

ってなことを書いてるってことは、ちょっとやる気に欠けるか

忘年会 at Son of Sun

学生たちと。時間すぎてるのに、二人しか来てないぞ

ここは、最近、気にいって使ってます

https://www.instagram.com/son_of_the_sun_kitchen

農林中金前のバス停の表示

なんか、新しいのが登場してました

いや、結局、古いバスロケのが一番使いやすいんだけど

これがいろんなバス停にあるなら、ともかく、ここだけってのがなぁ

自動運転バスとか出て欲しい

沖縄 Avac

ってわけで、見てきたわけですが、Aura がかっこい。25万円。リモコンなし。飾るためのものだな。

Marantz 悪くない感じ。

Avacの親父も、Acuphase修理できるみたいなことは言ってました。

Audio Amp

Accuphase のがどうもだめで、どうしようか考え中

なおすってのもなくはないらしい

何か買ってもいいかな。マランツの何か。PM7000Nか、PM6007 か...

サクラの聖夜

沖縄事務所の開設ですか。行ってきました。

学生その他4人と一緒。学内のアナウンスには流したが、

　　最近の学生は反応悪い...

お前ら、就活しろよってところですけどね。

AWSやGCPは学校の都合とか聞いてくれないので、国内クラウドは使いやすいところはあるかな

農林中金のバス停のまん前だ

read / copy / update

OSの授業で、Linux kernel 読んでたんですが、最近は syscall dispatch 部分は C なので。

いや、あれは C っていうのかは微妙ではあるか。

Fedoraのdebug build な kernel な VMと、gdb で読む環境が singularity で用意してあるのでばっちりです。

で、fd_get から読んでくわけですが、記憶とかなり違う。いや、昔は syscall table は C のマクロとかじゃなかった。

で、

　635 * read-side critical sections may be preempted and they may also block, but
　636 * only when acquiring spinlocks that are subject to priority inheritance.
　637 */
　638 static __always_inline void rcu_read_lock(void)
　639 {
　640 __rcu_read_lock();
　641 __acquire(RCU);
　642 rcu_lock_acquire(&rcu_lock_map);
　643 RCU_LOCKDEP_WARN(!rcu_is_watching(),
　644 "rcu_read_lock() used illegally while idle");
　 what is rcu?

　ChatGPT
　RCU, which stands for "Read-Copy-Update," is a synchronization mechanism used in computer programming, particularly in operating

あぁ、copy on write みたいなのが file write にもあって、それを rcu って呼んでるのか。

意外だけど、教科書にはないな。

what is rcu

年末進行

なんか、飲み会の予定を増やしてるだけなような...

来週は学生と忘年会の予定です

かけ算に順序がないって言う主張は無理があるし、かけ算の理解を妨害する雑な議論だから、やめとけ

足し算の繰り返しとしてのかけ算の 定義を理解していることを確認する

かけ算の問いに関して「何を何回足したのかを確認する」。問題の意図と、そこでの規則を確認する。回数を右に書くと決めてるなら、それも良い

かけ算の順序はそのまま積分や群の作用につながる

かけ算の対称的な定義は存在しない。なので無理に「かけ算には順序はない」と主張すると、累加の定義を拒否することになる。それではかけ算を理解することはできない

普通に累加でかけ算を定義して交換法則があると考える方が正統だし柔軟。面積などの積で表される物理量をそれで理解できる

＊ 右かけ算と左かけ算

回数を右に取るか左に取るかで、右かけ算と左かけ算を回数で交換則と同時に帰納法的に定義していく方法でかけ算を対称的に定義したい

しかし、それは右かけ算と左かけ算が同じであることを意味しない。それを無理に同じとすると矛盾が生じる

右かけ算とかは右作用とかに対応するから無意味とまでは言わないが、交換則があるなら二つ使うのは無駄ではある。片方で良い

右かけ算と左かけ算は以下のように定義できる

lmul : ℕ → ℕ → ℕ
lmul zero x = zero
lmul (suc x) y = lmul x y + y

rmul : ℕ → ℕ → ℕ
rmul x zero = zero
rmul x (suc y) = rmul x y + y

ね。rmul x y ≡ lmul y x でも良い(この方が簡単)

rmul x y ≡ lmul x y が交換則

＊　関数外延性

rmul x y ≡ lmul x y から
rmul ≡ lmul を導くのが関数外延性

関数外延性を仮定すると、実装の違う関数を定義することが禁止されてしまう。それは制約が大きい。それを無視すると矛盾する

世の中に乗算器は一つの回路しかないみたいな感じ。詳細に立ち入れない。同じだから

rmul x y ≡ lmul x y
と
rmul ≡ lmul
を区別するのは高階直観論理でも一階述語論理でもそう

LISPで関数同士をeqで比較するような話ね。あるいはCの関数のアドレスの比較

* 面積を使う

面積で縦横変えて自明に交換則が成立すると主張したい

その形が違う点の集合は違うものなので単純に同じとは言えない

まず、それが個数として同じことを確認する。そして、それが足し算の繰り返しになってることを確認する

回転は実数が必要なので大変。止めないけど

Sonoma + iOS 17

やっと、両方あげたんですが、なんか差は良くわからず。(uim+anthyはくらったが...)

iPhoneのappのタイトル表示消してたんだけど、また出るようになってがっかり。なおせないです。

Journal は、もしかしてネット対応ではないのか? なんでいまさらそんなものを...

どっちかっていうと、Evernoteをなんとかして欲しいんですけど。何回か課金したが、今は無料ユーザ。

Notes はどうなのっていう説もあるが...

あとは、パスキーか。

イヤホンなくした日

なんか、寝室で使ってた 2011 な MacMini の電源が入らなくなってました。いや、治すようなものでもないしなぁ。

さらに、上着のポケットに入れておいたイヤホンが紛失。まあ、前にもなくしてるしなぁ。

で、イヤホン発掘の旅に。最初に見つけたのはなんか延長ケーブル付きのソニーの。これが音がだめだめ。

あんまりなので、もう一回発掘。なんと、なくした奴と同じものを発掘。いや、別物なはずです。

なんで、二つもあるんだ? そもそも何についてきたんだろ? いや、iPhone付属のスイッチ付きイヤホンも、まだたくさん。

uim-xim + anthy 解決編

anthy は無罪なので、uim-xim を debug することに。engin=anthy-utf8 ってのあがるのを発見したんですが、

configure.ac が対応してない。誰も使ってないな。でも、それを乗り込えてもだめ。

で、debug build することに。これが、また、難航。

　brew install -d --build-from-source --git --debug-symbols --keep-tmp uim

という感じにして、uim.rb の途中に

　 system "false"

と挟むと、そこで止まるので、そこでいろいろできる。で、install しないと動かない。

OnTheSpot の幅がゼロなのを発見して、

　　 (lldb) x/20x str
　　 0x600001720070: 0x0000b3a4
　　 368 convstr = uim_iconv->convert(iconv_cd_e2u, str);
　　 -> 369 utf8_ = MAKE_STR(convstr);
　　 (lldb) x/20x convstr
　　 0x600001724140: 0x00000000

これが原因。やっぱりiconv。なんで EUC-JP が来てるかというと、

　　 scm/japanese.scm
((("k" "a"). ())("か" "カ" "カ"))

これが EUC-JP だから。uimは sigscheme で書かれてるんだけど、schemeでローマ字変換してる。

で、anthy-utf8.scm で、

　　 ac (anthy-utf8-lib-eucjp-to-utf8 (anthy-utf8-make-whole-string ac #t (anthy-utf8-context-kana-mode ac))))))

とhard codedされてる。なので、ローマ字表を UTF8 になおして、そこをなおして終了。

　　uim-xim --engine=anthy-utf8

これでばっちりでした。お疲れ様でした。

https://github.com/shinji-kono/uim/tree/develop

まだまだ、uim-xim + anthy

iconv のbugだろ思ってるんですけどね。uim-xim のiconv は macOSのなので、OSをsonomaに上げて死ぬのはそれっぽい。

最初は anthy を疑ってたんですが、今時は最初からutf8なのね。anthy-agent でローマ字変換までは見れたのでこっちではないらしい。

で、uim-xim なんだが、こっちは割とbuildできる。schmeme付きなのに! そう、uim ってのは scheme で書いてある。

まぁ、でも scheme 部分ではないだろってことで、uim を debug build なんだが、これが

　　autoconf を script で wrap

なわけで、ぜんぜん動かない。uim-xim --engine=anthy-utf8 にすればiconvは通らないと思ったんだが、確かに通らないんだが動かず。

で、もう brew の uim.rb を書き直して debug build 。こいつ、xtermないでないうごかないくせに、変なところで止めると xterm 全部が止まる。

ちょっと楽しすぎるんですが。結局原因は不明。uim-xim が文字を受け取ってるのはわかったが、xtermに表示されないし、

anthy_set_string にも空文字が渡ってる。見かけは scheme 側の問題に見えるが...

uim + anthyの続き

どうせなら fcitx + mozc にしようかと思ったんですが、mozc ってくそPython なのな。なんか、python を決め打ちで
呼び出してたりして、pythonが 3.9から 3.12まであったり。で、dmzって呼び出してもなんか、コンパネにでない。

なので、Mozc は諦め。

で、anthy-agent を調べたんですが、こいつ、

　　agent といいつつ、daemon じゃない

なにそれ。要するに command として呼び出すものなのね。で、割と動いているっぽい。ってことは、

　　だめなのは、uim-xim

か。一応、xim protocol は見てるから、anthy を呼び出している scheme か。なんか、load が動かないぞ...

というわけで、まだ、格闘中です。いや、X11 やめろよ。

macOS sonoma と X11

いや、ばっちり、

　　uim-xim が動かない

ってのをくらって困ってます。xterm も接続にいってて、uim-xim も受け取ってる。

<-: XIM_SYNC_REPLY.
<-: XIM_FORWARD_EVENT.
->: XIM_SYNC_REPLY.
<-: XIM_GET_IC_VALUES.
->: XIM_GET_IC_VALUES_REPLY.

でも、xterm には表示がない。xterm に値が戻ってない感じだな。

もうやめても良いはずなんだけどさ。

白金カイロ

カイロってのは懐炉か。沖縄最近寒いからな。そう、

　　いつぞやのブラウン管の学生です

ホカロンが禁止な学校とか、そんな話をしました

hgweb and podman play kube

なんか動かなくなってて。まあ、放っておいんたんですが...

どうも、なんか、hgwebの分割を割と力技でやっていやらしく。でも、hgweb が動かないのは

　　podman play kube --network web-ip pods/ie-web.yml

は、Dockerfile の [CMD] を無視して、yml に書いてあるものを実行するからだった。

いや、それはわからんだろ。まさかとは思うけど、podman exec で後から実行してたりとか...

分割の方法は良くわからず。まぁ、directory 指定すれば良いだけだから。

podman は Docker にも k8s にもへつらってるからそうなる。

　 docker-compose と podman-compose
　 pod による実行と、systemd の生成
　 play-kube

といろいろあって、まぁ、残念。k8s に絞った方が良い気もするが、yml があまりにひどくて...

いや、ちょっと前なら perl で yml 生成するのを書いてただろうな。

とりあえず動いたからよしとする。

OS9 trace

LISP09 なんか色々動かなくて、で、OS9の debug 法を思い出すはめに。Emulator に step trace とか
break point を仕込んでるわけなんだが、

OS9の sbc09 emulator を立ち上げてから、そのemulatorの中でLISP09を load してから止める必要がある。
os9 のshellが上がってから、

DA69: 10 3F 2C OS9 F$APROC

まず。ここで止める。すると、sbc09 の起動直前に止められる。そこから、OS9 kernelからUser taskに戻る rti
で捕まえる。

とかやってた。OS9のdebugつかっても良いんだが、ちょっとうまく動く自信がないし遅いだろうし。

なんだが、もしかして、Emulatorのstep traceを呼び出す命令を用意すれば良いんじゃないかと。で、ばっちりだった。

なんで、こういうのさっさと思いつかないのかな。そういえば、IOもEmulatorからメモリアドレス監視とかやってるんだが、

IOを triggerする命令を用意すれば良いのか。そういえば、Cellには sync みたいなのあったな。

qemu に 6809 + MMU を仕込むってのもやってみたいと思ってるんですけどね。もうあるかもな。

LISP09

なんか動いたっぽい。

OS9 の上の SBC09 emulator を使って実行してます。つまり、56Kbyteなメモリエリアに SRECORD から loadして実行。これだと絶対アドレスで実行できる。 Relocatableな OS9 module にするには少し工夫がいるみたい。

といっても、メモリマップを工夫してATOM領域をコピーするくらいでできるが。

GAME09もそうなんだけど、Uを User stack に使ってる。それは良くある間違いなんだよな。

レジスタが減るだけ。なおしたい気もするけど、考古学的なプロジェクトだからな。

% make lv2
src/v09c -rom os9/os9v2.rom -v os9/level2 -0 os9/OS9.dsk -1 os9/WORK.dsk
NitrOS-9/6809 Level 2 V1.0.1
Unknown Machine
(C) 2014 The NitrOS-9 Project

http://www.nitros9.org


Shell

OS9:sbc09 lisp09/lisp09.s

---------------------------------------------
LISP-09 Interpreter version 2.08 1983.10.07
Copyright (C) 1982 by Kogakuin University
---------------------------------------------
# of free cells : 7424
atom area, used : 1907
User stack area : 6285
System stack area: 3492

:(SETQ X '( 1 2 3))
(1 2 3)
:X
(1 2 3)
:(CAR X)
1
:(CDR X)
(2 3)
:

ゲゲゲの鬼太郎誕生編

学生と一緒に見てきました。沖縄ではテレビ放送がないので、猫娘が見れないのは残念だったが、
映画でもチョイ役

鬼太郎のオヤジの活躍の話ですが、そこそこ強い。奥さんが美人設定に。

閉鎖された田舎の村の殺人事件みたいな感じでもあるけど、最初のゆっくりとした展開と

後半の怒涛のリズムは割と良い。そこで「待たせたな」は違うだろと思うし、最後どうなったかも割と分からない。

まぁ、色々問題はあるんだが...

でも、漫画の方の誕生編とつながるわけね。それは割と良いかな。でも、学生達にはあまりわからなかったかも。

https://www.kitaro-tanjo.com

美栄橋のエリーカレー

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ヶ月、いや半年に一回でもクリーニングしろとか言ってたので、確かに暇なのかも。

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

研究室の web server

2011ものの Mac Pro かなんか使ってて、明日死んでもおかしくない。

なので、学科のサーバに収納してしまおうかと。

でも、なんかいろいろやることがあるのね。

k8s のymlがひどすぎて、設定ファイルを読めない。なので nginx の podman の rebuildがいる。

Scrapbox に Nginx のコンテナの作り方が書いてあるのだが、「どれが最新の記述か」問題があって。

　　build script くらい書いておいて

で、cert は、学科サーバ経由で取れたので、あと、もう少しかな。

hgweb うごいてないのなんとかして。

エリーカレーで英語

もう、明日で美栄橋に引越しちゃうんですけどね。

なんか、いくと英語放す人たちと一緒になることがある。

この前は、米国人おばさんと日本人夫婦みたいな感じだったんだけど、妙に流暢で。

英語教室的な感じじゃなかったし。見かけだけで三人とも米国人だったかも。

この前は、おばーと娘みたいな感じだったですが、おばーが日本語英語まじりで、なんかあれ。

で、携帯で電話し始めて、それがポルトガル語。あぁ、なるほど。沖縄ブラジル移民の二世か三世ね。

二世でも日本語維持するのは大変なんだよな。シアトルで聞いた変な日本語を思い出しました。

NYも、既に米語が第一な人は少ないらしく、日本でもそうなるんじゃないかな。

gitlab ci and submodule

なんか、どうしても submodule を新しくしてくれなくて。

　　Skipping object checkout, Git LFS is not installed.

がだめだろとか ChatGPT はいうんだが、関係ないと思ったんだが、それでした。

　　RUN apt-get -y install git-lfs

を追加したら動きました。

　　From gitlab/gitlab-runner:latest

こいつがあてになんないんだな。これだから Docker hub は...

The Creator

映画ですね。AIとの戦いみたいな話だったので学生と観てきました。予告でネタバレするの良くない作品だな。

まぁ、それは仕方ないか。インドネシア、カンボジアの風景が出てくるので少しベトナム戦争っぽい。

AIの最近の話題は皆無でむしろ、

　　P.K.Dick や J.P.Hogan 的な正統的なSF

でした。佳作。空中要塞 NOMAD かっこよい。

何もしてないのに壊れました

10/25にいきなりネットワークが止まった件なんですが、Sakura の方で調べてもらったんですが

　　機材の異常はない

え〜? あぁ、まあ、Unbuntu 22.04 on Dell PowerEdge だからなぁ。いろいろ前科あるし。

卒研中間発表のあとで matayu と、もう一度、コンパネから接続。

　　もしかすると、netplan apply でなおるかもな

ってのが、ばっちりで、開通。なんなんですか。uptime 150 days タイマーでも入ってるのか?

demsg/syslog/ip a とかでも異常は見つからず。原因不明。気のせいか。

　　一応、reboot はしました

(gitlab-runner 側は dead だったら、再起動するcronを入れてみました)

Sakura / mattermost のtrouble

なんか夜中0時に止まったらしく。学生が2時に止まったとか書いてるのを朝5時にみたんですが、

ssh がつながらなくて、コンパネに入れない。

で、そうそうに見切って、オンプレ側の mattermost を動かしにいったんですが (外から見えるメインのサービスはそれだけ

　　なんか、9月に用意した痕跡が...

でも、podman は動くが、mysql に接続できん。

で、しばらくお休みしてたら、M2のmatayuがなんかやりはじめたんで、一緒にZoomで。

彼はコンパネ開いたので、見てみると Sakura のサーバは生きてる。でも、

　　gatewayのpingが通らない

これは自分たちのせいじゃない。だいたい、0時ぴったりだから、向こうがなんかしたんでしょう。

で、やっぱり、オンプレで mattermost を上げる方向で。9月のやつがかなり不完全で難航しましたが、11時にはあがりました。

まぁ、matayuと自分なら不可能なことは存在しない。なんだけど、

　　学内側はなぜか動かず

で、やっと PowerDNS recursor の cache reset が必要なことに気がついて復旧したのが17時。いろいろすみません。

Hot swap はめんどうなんだよ。backup は 10/21 なので少し古いな。mattermost だけもう少し細かくすれば良かった。

あれ、gitlab-runner が落ちてるな。なんなの〜

vim で :q できない

何言ってるんだお前は的な質問なんですが、

　　virsh で Fedora OSをinstallするんだが
　　日本語モードで install したらしく、
　　Fedora OSは日本語キーボードのつもりで
　　VNCは、英語キーボードを日本語キーボードに変換しているつもり

な感じで、: が ; に。そして、少し探したくらいでは : は見つからないという羽目に。

いや、ssh か virsh console ができれば良いわけなんですが、両方ダメらしい。

だから、

　　ここで日本語を選んじゃだめ

って言ったじゃん... まぁ、いまどき install は数分だから。

virsh console するためには、visrh で serial をたしておくと良いらしいが...

いや、まぁ、いまどき、qemu image も持ってこれるし、docker image でもいいじゃんとも思いますけどね。

一回はやっておくのが礼儀みたいな感じ?

ひさしぶりのハリーズ

なんか、ハリーズの月曜日に臨時休業が二回。あいだは、工学部の計画停電。

一か月ぶりかぁ...

永遠の終わり

アシモフの古いSF。アシモフには珍しい時間もの。銀河帝国誕生の裏話的なものでもあるな。

この本、中学生の時に、池袋の旭屋であらかた読んじゃって。で、やっぱり欲しくなって買った銀背です。

タイムトンネルを持つ官僚機構みたいな話。それをぶっ壊す話ですね。

だいたい、話は覚えていたが、細かいところは忘れてたので割と楽しめました。アシモフが若いので話も若い。

色恋ものでもあるんだが、そっちの方が全然書いてないのも、アシモフっぽいかな。一方で年代測定の話とか細かくてさ。

今読むと、ハーラン馬鹿すぎと思わなくもないです。官僚機構に限らず男はそんなものなのかも。

この手のものって、今の学生にはどうなんだろ。携帯とか出てこないわけなんだけど。自分は違和感ないが...

いや、漫画でも、その手の時代錯誤感はかなりあるからなぁ。

https://amzn.asia/d/fRrWB0Z

さっぽろ一番みそラーメン

得に思い入れがあるわけではないですが、実家で一人でいる時は袋麺で作ってたかも。

西池袋の幸楽の、さしておいしいわけでもなかったみそラーメンとか。

その頃の残念な感じでもあるかな。当時もキャベツがあれば入れてたかも。

Agda で Red Black Tree

CbC on LLVM は片付いたので(多少問題はあるが)、今度は Agda の方かなと思って。

一日かけたけど、あんまり進んでないです。つまり、二進木よりめんどいってことね。

もっと、ずっと簡単な方法もあるのかも。でも、

　　エンジンはかかってきたかな

プロシンは、これじゃなくて、Automaton の方を出すつもりです。

　　非有限 Automaton

みたいな話。

よならぼ閉店

結婚式の二次会とか良かったんだけど、コロナの直撃だったかなあ

パスタのお店というのが自分の認識でしたけど

学生連れていったり楽しかったな

最近のingress

近所の agent が二人も緑に変わったり、なんか新しい緑が来たりで割と劣勢です

でも、最初も「劣勢な方が面白いか」と思って青にしたので、実際割と楽しいかも。まぁ、

　　沖縄全体だと、青が強い

わけなんですけどね。緑のagentが那覇に偏ってるせいなんだが。

まぁ、暇な奴が勝つゲームなので、それほど勝ちを目指さない方針です。

歩くための持ちべだからな。

sysroot の問題らしい

llvm のbuild ですが、

-syslibroot /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.3.sdk
-syslibroot /Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk

この差でトラブルらしい。

ls -l /Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk
ls: /Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk: No such file or directory

これではだめです。何回かはまった気がする。いったん、Xcode を削除するのだったかも。

ジベタリアン

なんで、床でやってるん。椅子が足りない説?

cbclang package 作り

できたので、brew と debian package にするわけですが

sw_vers -productVersion 10.14.6
sw_vers -productVersion 13.2.1
sw_vers -productVersion 13.5.2

いろいろあるね。2012のロートルマシンとか。fat binary にはしないのが最近の流行りか。

debian は、fpm でやるんですが

　　なんで、前の command line をとっておかないんだよ...

Ventura で setjmp がかわって、Aarch64 で動かなくなったんだな。gcc はしばらく放置か。

うっかり、ロートルの brew upgrade したら、make install 始めてしまって、待ち状態。

あと、brew llvm は、なんか壊れてる。もともと入ってるので build できたので、まぁ、いいか。

まとめてくるバス

おかげで30分待ちとか良くあって。タクシーも減ってるしなぁ。バスの本数も減る方向こうかも。

将来的には自動運転になるとは思いますけどね。そうすると、本数増やすほど儲かるということになるのか?

この4台のバスは琉大向けじゃないやつ。

llvm / clang CbC fixed

なおったっぽい。

setjmp が二回出てるのはご愛嬌ですぐになおったんですが、問題は

　　__code carg4(struct arg args0,struct arg args1,int i, int j,int k,int l)
　　{
　　　　goto carg5(args1,args0,j,k,l,i);
　　}

この構造体の入れ替えね。

!　 call void @llvm.memcpy.p0.p0.i64(ptr align 4 %byval-temp, ptr align 4 %args0, i64 20, i1 false)
!　 call void @llvm.memcpy.p0.p0.i64(ptr align 4 %byval-temp14, ptr align 4 %args1, i64 20, i1 false)

ばっちり memcopy で壊されてる。tail call でなければ問題ないわけ。でも tail call を強制しているからな。

で、なぜか、x86_64 ではこうならない。Aarch64 で問題になる。なんで。なんと clang CodeGen 　に、こんなコードが。

　　clang/lib/CodeGen/CGCall.cpp
　　　　case ABIArgInfo::InAlloca: {
　　　　　assert(getTarget().getTriple().getArch() == llvm::Triple::x86);

ちょっと。これひどすぎないですか? clang level で Triple 見てチート?

そういうことなら、こっちも

　　#ifndef noCbC
　　　　　　if (this->FnRetTy.getTypePtr()->is__CodeType() && CallInfo.getReturnType().getTypePtr()->is__CodeType()) {
　　　　　　　　NeedCopy = false;
　　　　　　}
　　

レポートは ChatGPT で自己採点してから

なんか、やりかた間違えて、学生のChatGPTコピペを採点するはめになっている先生がいたようですが...

　　学生にChatGPTで自己採点させて80点以上

にするとわりと良いんじゃないか説。誰かの書いたダメなのをコピペするよりはましになるらしい。

教科書の該当部分と一緒に問題を食わせるとかなりましなんですけどね。

　　そもそも、教科書読まずに、教科書の問題解く

とか十年早くね? もっとも、Silbershatz もかなり時代錯誤でテープドライブとか出てきちゃうんですけどね。

いや、最近、テープドライブ見直されてるし?!

ハッカーずチャンプルーでも「Step by step」と入れると良いとかあった。今の学生は

　　ChatGPTと比べられてしまうので大変だよな

学生が自分で便利と思うのは、まだ先か...

Atlas Probe

何かメール見落としててすみませんでした。が、城間さんとサーバ班で設置完了。

ネットワーク観測器みたいなものですが、まぁ、地味なもの

　　もう少し、見栄えのよい視覚化かなんかないんですか?

Akamai のディスプレイはかっこよかったな。あんな感じのがいいな。

https://atlas.ripe.net

計画停電

まぁ、迷惑な話なんですけどね。実は17時には復旧していたらしい。

たまたま大学にいたので(偶然なわけではもちろんない...

ブレーカー切ってたのを入れていく。で、していされた順に iDrac で power on。

で、ceph 起動して終わり。

なはずなんだが、いろいろトラブる。主に podman の systemd への登録忘れですが...

　　mount -a

はださいだろ。

この手作業あるのなんとかならんの?

センター試験7割説

  

既にセンタ試験でも共通一次でもないわけですが。

まぁ、割とセンシティブな話ではあるんだが、人に教える職業なら、それくらいあるべきだろっていう説ね。

学校でダメな先生に当たることは、ままあって、それがいいかなとも思う。実際、そうでなと、                    

　　優秀な学生の話についていけない

感じではあるかも。フランスだとバカロレアでばっちり切られてしまってなれる職種が決るってなところがある。

でも、じゃぁ、だからフランスの教師の質が良いとか、役人の質が良いかというと、それも妙。

大半の学生はそういうレベルじゃない(そもそもセンター試験受ける層が限られてるし、7割とるのは、その3-4割)だという

話があって、それで中学高校あるいは大学受験をクリアするには

　　　暗記しかない

という話を真面目にする人たちがいるわけね。はじきとかそういう話。実際は、

　　　暗記でセンタ試験7割は不可能

なので割とつじつまはあう。そういう人たちがそういう話をしてる。でも、これは割と怖いで 

　　　理解して問題を解くという経験のない人たちが多数派

であるってことね。一方で、反ワクチンとか反原発は、むしろ高学歴にもいるわけなので、一概には言えないかんじ。 

まぁ、あんまり結論のない話なんだけど、

　　　センタ試験7割なら、時間さえ掛ければ誰でも取れる

とは思うんだ。それは自分の傲慢な考えだとも思うけど。もしそうでないなら、そういう器的な差があるってことだけど、そんな感じはしないので。

なので、そういう「時間無制限なカリキュラム」みたいなのが欲しいかなとは思います。

ハッカーずチャンプルー

会議100人、懇親会60人らしく。

このカンファレンスは、うちのOBの桃原が関与してて、割と関係があるかな。

OBがたくさん来てるし、発表も。そして、

　　B4の発表「DBMSのRustによる実装」!

一月で書いたのは偉いかな。もちろん、8割くらいで、残りが大変なわけですけどね。

でも、佐野はうちの研究室らしいとか言われてた。まぁ、そうかも。

他の発表ではNewSQL の話とか面白かったが、

　　mysql や postgress 互換

え〜、そうなの。

また、Hugo

OSの授業で Hugo の demo したら、

　　top page に一つしか表示されない

もう、この手のわけわんない動作やめて。いろいろいじったら、

　　postの下に置いて、config.toml の言語設定とかは消す

で出るようにはなったんだが... いや、これ普通、学生がいろいろ見つけるところなんだと思うんだが...

どうりで、補講の提出のpageが変なはずだよ。

対面授業

いや、もうあんまりやりたくなくて。でも、学生が教室にきてがっかりするのもあれなので、最初は出ようかと。

321教室久しぶりなので AVコンソールがなぞ。LANケーブルどこだ? Apple TV置いてあるので、それで接続でいいんですけどね。

なんか login とか言ってるが、Apple TVってloginしなくても Share screen できるのか。

とかいいながら、接続はHDMIで。それで、

　　Zoomも接続

割とめんどいのが音声と質問。いや、さ。

　　質問は Chat 限定でいいですか? Discord 使えよ

って感じ。

自分は録画はしてないんですが、欲しいという学生が。

　　どうせ見ないだろ

つうか、そんなもの見る時間あるなら、授業の内容は全部Webに置いてるんだから

　　課題やれ

と思うわけですけどね。再来週からは online only にしよう。

CbC llvm

いや、夏休みの間、やるやる詐欺で全然やらなかったんですが、

学生と一緒に x86_64側を見てたら

　　例題の方が間違ってて、なおしたらぜんぜん動く

いや、AArch64 側は setjmp が二回出てたりしてだめなんですが。でも、ってことは

　　割と簡単になおる気がしてきた

魔法はイメージが大切だからな! できる気がしないとな。

サーバ班

サーバ班は、もともと

　　システムメンテは面白いけど、修士がやることじゃない

ので、学部3年にやらせようと思ったもので、もちろん、

　　3年次に手に負えるわけもなく

自分たち(自分と当時の助手の白土先生と)でやることに。なんだけど、

　　なぜか、それとは関係なく参加してがんがんやってくれる学生がいる

学年に一人いるかいないかくらいですけどね。なんでだろ? まぁ、自分もそのひとりではあったかも。

シス管は、それでは使えないと思った長田先生が修士/博士に金出してやらせようと思ったもの。

　　ひとそれぞれの考え方があるな

まぁ、いろいろ変えていってください。

ハリーずお休み

だったので、エリーカレーに頼んでみました。(いや、ゆでたまご苦手だって言ったのに...

国連旗

フライトラインフェスタには、自衛隊も来てたんですが、国連旗もあがってるのね。

黒いのはなんだろ。

自衛隊はパトリオット展示してました。

大学で教えるべきこと

OBに聞くようにしてるんですけどね。まぁ、いま自分が必要としていることを答える人が多い。

　　データベースとかコミュニケーション能力とか

それは残念なことかなと思うけど。取締役クラスだと

　　分析力とか論理的思考能力

とか。なるほどとは思うけど。具体的な授業とかカリキュラムにはつながりにくいかな。

いや、別に回答を批判しているわけではなくて、大学が提供するものの難しさとかがわかる感じ。

学生には、

　　大学で学んだものが役に立ったという実感がる

よりは、

　　大学で学んだものは何もないが、そこで学んで得るものがあった

方がうれしいかな。

　　新しいものを学ぶためのメタ知識

みたいなものを教えたいと思ってます。

書類の続き

欲しいのは戸籍謄本なんですが、自分のカードでは「このカードで使えるサービスはありません」で郵送してもらうってことだったですが、

妻のマイナンバーカードでは問題なくコンビニで印刷できた。いや、筆頭は僕なんだけど。

　　なんでやねん

コロナ世代

物理的に大学にきてないので、どうも学生間のつながりが浅いらしく。連携が取れてない感じ。

OSの課題だとむしろ、まわりや先輩に聞いてやって欲しいんだが、それができない。

いや、Discord でやってとはいってるんですけどね。難しいみたいね。

イギリスの鉄道の話

90年頃はBritish Railは、まだまともで、InterCityもきれいだったんですが、
保線と営業を別にしておかしくなって、00年代にはぼろぼろ。

This train has been cancelled を結構くらって超残念だった。

そのあといろいろ修正されたらしいんですが、この一連の tweet のがひどくて、

(1)4PMにロンドン-エンジンバラに乗ったら
(2)スマホに This train has been cancelled
(3)運転手にそれが乗客から伝えられて Preston で止まる
(4)乗り換えの電車は満杯
(5)次の電車は cancel でもう電車はない
(6)約百人の乗客は鉄道会社持ちのタクシーで3時間
(7)道知らないイギリスのタクシーの迷走
(8)着いたけど、タクシーの運ちゃんは無事帰れるのか?!

失われたインフラを取り戻すのは難しいってことね

あるいは公務員が誇りを持って働けることの重要性か...

Preston は西側だが、マンチェスターの近く。せめて、その駅ならねぇ。

https://x.com/JamesNokise/status/1706433356186161479?s=20

ldap-server

何か最近は、ldap server / slave と呼ばず、provider / consumer らしく。

懸案だった、ldap -server を container にするってのを小川が片付けたらしい。えらい。

なんだが、いろいろトラブルが。

1) gitlab に login できない。

なんと、gitlab の ldap 設定がIPv6 address直打ち。あぁ、IPv4つながらないとか、そんなトラブルあったっけ。その時のだな。

まぁ、IPv6も割り振れよって気もしますが。

2) ldaps で接続できない

あぁ、昔からそうなんだよ。なんだけど、

cert がないとかいってる

昔と違って、Wildcard Cert を持ってるから、いれれば良いんじゃない? でアクセスできたんだが、

3) sssd からはだめ

いや、sssd 要らないとも思うんですけどね。実際、入ってるのは 4台のうち1台だけなんだよな。

ところがなぜか sssd が切れない。

sssd が古いのかも。結局、sssd の設定は ldap: のままか。残念な話だ。

いろいろなぞなままだな。

いや、でも ldap server は podmain になったし、ldaps は動いたし。進捗はしてる。えらい。

アナログメーター

なんかいいよね〜

上島珈琲のだったかな

agda の version up はだいたい終わり

一部、激ムズくらいましたが。

　　ライブラリの引数を変更されるとムカつくよね?!

Data.Fin の suc だけじゃなくて、inspect が新しい構文になったんだが、どうも一部の機能が低いまたはバグがあるらしく。

その部分を、case文の中で再証明すれば workaround できるのに気がつくのに少し時間がかかりました。

後は細かい問題だった。postulate / functional-extensinality があると、--safe は付けられない。

まぁ、少し分離したけど、虚しい気もする。module の入力にすれば形式的には逃げられる。

Agda の std-lib 2.0

一応、群論の方はなおせんたんだが、いろいろ判明。

　　--cubical-compatible では、case 文と Termination check に問題がある

なので、case文の方は

　--warning=noUnsupportedIndexedMatch

で警告を消す。Termination check は　cubical-compatible 諦めるしかないっぽい。

まぁ、cubical-compatible のありがたみは特にないわけなんですが。

--safe の方は、ほとんど問題無し。なんなんでしょうね。


問題は、

　　Data.Fin の 関数の zero / suc への展開が全滅

with f x とかやるだけで、

　 Function.Bundles.Inverse.from perm (suc x) != w of type Fin (suc n)

意味不明らしい。

いや、もともと Data.Fin (有限な自然数)怪しくてな。workaroundはできたんですが、大変だった...

finiteSet とかでもとらぶる予感。でも、無理になおさなくてもいいとも思うんですが。まぁ、ちまちまなおすか。

OSの補講と ChatGPT

いや、火曜日から4日間しかやらなかったんですけどね。課題出してもらえればよい。後期の授業は10月からなので、

　　後期の授業のチェック

みたいなところもある。なので、いろいろ修理しているわけですが...

課題の採点もやってるんだけど、

　　ChatGPTなだめなレポートが

いや、別に中身あってれば問題ないわけですよ。ところが、正解にならない。もともとコピペ対策で、

　　gitlabのciの失敗したやつのリンク
　　作成したVM imageの ls -l

とか提出されているので、チェックされてしまうので、そもそもChatGPTでは歯がたたないわけなんだが、

教科書の問題とかも、

　　dead lockの問題なのに snapshot という言葉に引きずられて snapshot について語ってしまう

ChatGPTおしゃべりだからな。問題解けよ! 語るな! いや、それでも、そういうのは少しは点数は出してたんだが、

　　もはや、問題を理解してないなら再提出しかありえない

なので、ChatGTP下だと採点が辛くなるのは仕方ないかなぁ。

教科書の対応する章を全部食わせて、問題解かせると良いんだが、API経由でそんなことすると10万円コースらしい...

gitlab-runner

OSの補講をやってるんですが、gitlab ci の課題が動いてない。まったく、こう次から次へと...

gitlab-runner で ci のテストが動くわけね。vmから、container / podman にしたのか。

　 podman exec -it gitlab-runner /bin/bash

で接続できて、go version も動く。何が不満なんだよ。と思って、.gitlab-ci.yml に full path で書いたら動く。

/usr/local/bin に symlink でいいか。ついでに Rust も設定。こっちは、.gitlab-ci.yml　を

　　variables:
　　　CARGO_HOME: "./cargo"

　　before_script:
　　　- export CARGO_HOME=$CI_PROJECT_DIR/cargo

とすると良いらしい。

singurarity　 も

　%environment
　　 export PATH="/opt/rust/bin:/opt/go/bin:$PATH"
　　 export CARGO_HOME=$HOME/.cargo
　　 export RUSTUP_HOME=/opt/rust

という感じで動きました。Rust 完璧に忘れてるな。

singularity / apptainer と Rust

pyenv / cabal とかもそうなんだけど、rustup が

　　$HOME/.rustup

にいろいろ作る。これが singularity / apptainer container と絶望的に相性が悪い。なぜかというと

　　$HOMEが default でbindされるから

これ、PC (一人一台) な文化なんだよね。それでいいならいいんですが、

　　個々のノートPCの能力が低すぎる (VMや Agdaに足りない)

なので、Server 側に singularity で整備してやろうってわけなんですが、

　　学生一人一人が、$HOME/.rustupに rustc とかを持つのかよ、馬鹿すぎるだろ

ってわけなんですが、一応、

　　export RUSTUP_HOME=/opt/rust
　　export CARGO_HOME=/opt/rust

で切り替えられる。それでも、そこが固定されてしまうので後から module 追加とか困るだろうけど。

まぁ、とりあえず、これでいいかな。メインフレーム/TSSっぽい話。ただ、

　　コンテナ用の package 管理もでるんじゃないかな

とも思います。

1円玉の処理

なんか350枚くらいたまってて... 学生のやるやる詐欺はもういいので、ingressのついでにコンビニに。

最近は銀行で引き取ってくれないのね。有料ってなんだよ。硬貨なんて廃止しろ！

ローソンで、何枚いいですかって聞いたら、200枚。十分十分。学生二人とちまちま格納。

で、次はファミマ。なんか計数器みたいのがある。ざざざざ。あ、拒否された。

　　もう一度やればよい。日本人は絶対やらないけどね。

最近はネパール人が多いかな。ありがとうございます。

蔵前工業会

なんかメール発掘してたら、会費無料とあったので10年ぶりくらいに。

そしたら、なんか学長さんが来てて... まぁ、数人しかいなかったし、首里の普通の居酒屋だったんですけどね。

久しぶりな面子にも会えたので良かったです。

学長は女子枠推進派らしく「理論武装は完璧」みたいなことをいってました。僕も女子枠賛成です。

医科歯科との統合もあって大変らしい。

たまには、行ってみるか〜

Agda の version up

なんか、一日たっても終わらないので、without-k やるかってことなんですが、そもそも、--safe にすると、Decの例題が通らない。

server側とのずれも気になるので「versionあげるか」なんですが、

　　name: standard-library-2.0

ちょっとお〜 なんかいろいろ変わってる。inspect が deprecated?! あれはひどかったからなぁ。

without-k も、< や Decの展開とかできないし、Heterogenous は文句いうしで、割と

　　　最初から勉強しなおし?!

な気分。まぁ、なんでもそんなものですけどね。

Agda の option

なんか、library が --without-k ってのを使ってるのは知ってたんですが、なんか最近、without-k 使ってないと文句言われたことがあって。

群論(S₅がS₃を含む)ってのも見直してたんですが、

　 [ dba , aec ] = (abd)(cea)(dba)(aec) = abc

が Altin に書いてあるやつなんだけど、作ってるのは abc だけど、元は dba とかで違うものじゃん。adb = dba⁻¹ だから、半分はわかる。

で、プロシンで発表した時は「全部の存在を示す」みたいな感じでやってたんですが、群でやれば良いんじゃないか? と思ったんですが、

　　交換子自体は積に閉じてない、なので、有限生成して群にする
　　なので、S₃から要素を取り出しても、交換子とは限らない

あだだ。でも、q が交換子なら、共役元 p ∙ q ∙ p⁻¹ は交換子になるってのを交換子群が正規部分群なことを示すのに使ってた。なので、
dba とか、abc の共役元で良いじゃん。で、次の一行で良いらしい。

　　 abc ≡ [ (dc)(abc ⁻¹　)(dc ⁻¹　)　, (eb)(abc) (eb ⁻¹　) ]

これで、abc の逆元と共役元から abc が作れるので、これが可解群 (いつか交換子群列は{ε}になる)の反例になる。簡単!

なんですが、

　　　チェックが全然終わらない。しかも、全部つながってるのだが、つなげると時間がかかる

　　% time agda　sym5h.agda
　　Checking sym5h (/home/teacher/kono/src/galois/src/sym5h.agda).
　　agda: Heap exhausted;
　　agda: Current maximum heap size is 3758096384 bytes (3584 MB).
　　agda sym5h.agda　1429.15s user 19.74s system 99% cpu 24:09.22 total

なので、もしかして、--without-k 使うと良いかと思って。なんだが、最近は、

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

と書くらしい。なんか、1 < x とかを展開するところで文句言われるので、かなりなおさないとだめらしい。で、

　　Dec p の展開で yes / no でも文句をいう

なので、何回いろいろ問題があるっぽい。たぶん、version 不整合とかかなぁ。

特にねたのない日

ま、無理して書く必要はないんだけどね。

BD-RE を買いにいったんだけど、ケースの方がない。48枚入りを使ってるんですが。そういえば前は通販した気がする。

でもさ、メディアとケースは組で売るものな気がするんだけど? 注文すれば買えるみたいではあるが。

Well-defined

数学だといろんなところで聞く用語なわけですけどね。Agda だと、

　　f-cong : {A B : Set} → {f : A → B} → → A < x ≈ y > → B < f x ≈ f y >

こんな感じ。数学だと型書かなかったりするから、x = y → f x = f y とか書いてある。

自明なのになんでと思うわけですが、≈ が関係だと自明にならない。ところが ≡ だと自明になる。後者は

　　data _≡_ {A : Set} (a b : A) → Set where
　　　 refl : x ≡ x

なので、Agdaの項として等しいという意味ね。

　 _≈_ : {A : Set} (a b : A) → Set
　 a ≈ b = ?

で自分で勝手に定義する。剰余群だと、mod 2 で等しいとかそんなの。なので自明じゃないので証明する必要がある。

なんで、Well-defined っていうかっていうと、関数の定義が集合論だと二つの集合の関係で well-defined なものだから。

　 F : {A : Set} (a b : A) → Set
　 well-defined-F : {A B : Set} {a b : B} {c d : A} → A < c ≈ d > → F c a → F d b → B < a ≈ b >

まぁ、にてるっちゃにてるけど、別なものだよな。

Agda / 直観主義論理だと関数が先だから、それは必要ない。

凖同型写像 f : A → B は群の構造を保存するわけで、それは A < a ≈ b > が保存する、つまり、B < f a ≈ f b > だってこと。
同値関係を保存するっていう方が明確な用語だよね。

面白いのは、圏論でもこの問題はあるのだが、大体省略されてる。圏の性質を保存する関手の定義には実は cong が必要。

剰余群 G / K は、Gの要素を a ∙ b ⁻¹ ∈ K という同値関係を持つ群に読み替えただけなので、f : G → H はそのまま f : G / K → H
になる。違いは

　　G < a ≈ b > → H < f a ≈ f b >

と

　　G/K < a ≈ b > → H < f a ≈ f b >

だけってことね。 GK < a ≈ b > は a ∙ b ⁻¹ ∈ K なので、x ∈ K → f x ≈ ε が凖同型定理の仮定なので、

　　f x ≈ f x ∙ f y ⁻¹ ∙ f y　≈ f (x ∙ y ⁻¹ ) ∙ f y ≈ ε ∙ f y ≈ f y

ってだけ。 これが凖同型定理だった。G / Ker f ≈ Im f も問題はそれだけでした。

剰余群の GK < a ≈ b > → GK < c ≈ d > → GK < a ∙ c ≈ b ∙ d > も、

　　a ∙ c ∙ (b ∙ d) ⁻¹ ≈ a ∙ c ∙ d ⁻¹ ∙ b ⁻¹ ≈ (a ∙ b ⁻¹) ∙ (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹)

で、(a ∙ b ⁻¹) ∈ K , (c ∙ d ⁻¹) ∈ K そして、共役元 (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹) ∈ から出る。

こうすると、共役元が K に属するのが剰余群の条件だってのが良く見える。

残りは自明だってのを納得するのに時間がかかった感じ。

BDレコーダー故障の続き

いや、まあ、もう録画止めてよいんですけどね。Amazon Primeの画質とか字幕の扱いは最低だが、それは地デジ/BSもにたようなもん。

でも、最後なような気もするし。惰性な趣味でもある。

BDZ-FBT1000 の光学ドライブがいかれただけなので、ソニーの一台買ってきて dubbing でいいかってわけですが、

　　接続がめんどい。AV AMPがどうこうで、学習リモコンがほげほげで。

元のをハンカチで目隠して、リモコンモードを変更。接続ポートを学習リモコンに登録。

なんか製品登録がソニーのアカウントと統一とか言われてる。まぁ、それはいいけど。

あぁ、前回のBDZ-FBT1000は登録されてないのか。ヤマダ電機で見つけたのは

　　BDZ-FBT3000

う、同じ時期の製品か。ま、いいか。ところが、

　　肝心の引越しダビングが開始できない

Firmware update (USB経由)とかもやったんだがだめ。でも、TVサイドビューはつながるのか。もしかして...

　　Wifi station ではなく、LAN Switchに二台ともつないだら認識した

最近のWifi stationって、broadcast 通さないのか?

ところが、

　　99個ずつ?!

まぁ、せこせこやれば終わるかな。メディアはBDZ-FBT3000の方では認識しました。

Ruby on Rails / Akatsuki

Free Radious は DHCP6 に対応しないようなので、Kea DHCP なんですが、それに合わせて Akatsuki をなおす必要がある。

まぁ、atton の置き土産だが、この前、PowerDNS対応したので楽勝なはずですが...

Ruby on Rails の package system って Gemfile に頼っているところがあるらしく、

　　Gemfileを用意しないとどうしようもない

いや、そこにソースあるんだから、そこから Gemfile を生成しろよと思うんだけど。まぁ、それは今あるのを使うんだが...

pddmanの Dockerfile が、まず、

　　COPY . /app

する。で、config だけ -v で map する。わけわんないんですけど。ファイル変更する度に podman build するのか?!

まぁ、debug する時だけ、そこを -v するっていう手もあるが... まさか、中から git する方式?!

この辺は、sigularity の方が開発向きではあるよな。

Readable Code

Twitter (自称 𝕏 )で、 話題になってたので学生部屋に置いておきました。

短いのは良いね。コードコンプリートはでかすぎる。

変数や関数名の付け方とかは英単語の話が多くてさ。get じゃわからんとか。同義語辞典使えとか。

コメントには、そのコードでないと起きる良くないことを書けとか。インデント深くするなとか。

まぁ、書いてあることは浅いんですけどね。後書きで須藤さんが

　　とにかくコード読め、読む文化を作れ

って書いてて良い感じ。

最近は証明にはまってるから

　　プログラムは正しさがわかるように書け
　　型は正しさを部分的にしか保証しない

ってな感じですね。

https://amzn.asia/d/351ioUJ

家系ラーメン

なんか大平の昇家の後が武蔵家になってたのでいってきました。ガテン系兄ちゃん二人。なんだが、

　　激アンモニア臭い

おまえらなぁ... でもめげずに注文したんだが、激しょっぱい。家系割とありありなんだが。東五反田のもそうだった。

でも、それを除けば。まあ家系でした。だた、なんか麺少なめだな。もしかしてご飯込み? 半ライスくらいつけるといいかも。

味薄めにできるらしい。いや、もう一回いく気にになるかどうかは。

はるやもやってるみたい。

コンビニで戸籍謄本

いや、とれるって話は聞いてたんですが、そもそもなん戸籍謄本が要求されるのか理解不能。しかも、郵送。

そんな手続き全廃するべきだろ。ネットでいいじゃん。そのためのマイナンバーなんじゃないの?

なんだが、なんか拒否される。

　　なんか、申請ボタンがあるぞ? なんだこれ? 馬鹿の仕業か?!

しかも、

　　5日待て

とかいってる。まさか

　　仕事なくされるのが嫌だから手作業残したのか? 馬鹿すぎるだろ...

例外処理なら、まだ理解できるが...

凖同型定理

学部の時の阿部先生の代数学の本を見直してたら唐突にできました。

　 Given two groups G and H and a group homomorphism f : G → H,
　 let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
　 (where G/K is the quotient group of G by K).
　 If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
　　　 https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
　
　　　　 f
　　　G --→ H
　　　|　 /
　　φ |　/ h
　　　↓ /
　　　G/K

ってだけだが、剰余群 G / K は要するにG要素の分類なので、Gと等号だけが違う群に過ぎない。

なので、 h は結局 f そのものでよい。φ も id でよい。なので、凖同型定理のほとんどは自明。

問題は、hの凖同型写像の条件の一つの

　　aN ≈ bN → f a ≈ f b

だけで、それ以外は f が凖同型写像なことからでる。これは、

　　GK < a ≈ b > → a ∙ b ⁻¹ ∈ N

なので、f (a ∙ b ⁻¹)　≈ ε から、f a ≈ f b だけだった。

代表元がどうこうとか、φ の逆射があるとか、いろいろ寄り道したが、それらはまったく関係なかった。

G / Ker f ≈ H まではやるかも。

カフェの灯り

まあ、いいんだけど。燃えるんじゃないかと少し心配。

紙っぽかったけど。

猫の結界

何か、新しい猫グッズが登場してるんですが、

　　そこにおじいちゃん猫が寝ると、お嬢ちゃん猫が手を出せない結界

になるらしく。原理は不明。単になれてないだけかも。

Alexa と Switch Bot

ホームオートメーションの基本みたいな感じですが、ラジオとしてでもいいかなと。

なんだが、

　　共有して使おうとするとめんどい

なので、自分は設定する気にならず。奥様の方は主にクーラー制御に使ってるみたいです。

HAL研のリモコンとか、USB赤外線とかもいろいろやったが、

　　いろいろ不都合がでるのに対処するのがめんどい

それに、

　　無線や赤外線の信頼性の低さとか

まぁ、一時期がんばったから、もういいかな。

lldb と Rust

Rust は LLVM base なので、普通に lldb / gdb が使えるわけですが、

　　使い方がわからないから printf debug

とか言ってるのがいたので..

　　cargo build
rust-lldb target/debug/rust-dbms

で普通に動く。

　　b main

だと、C側にかかるらしく、いきなり ARMのassemlerがでるけど、普通に Rust の関数に break point を掛けられる。

ChatGPT は質問している方がわかってるところまでしか聞けないところがあるので、ソースコードデバッグを
知らなければ、まぁ、質問しようがない。

もっとも、最近は、debugger 使わずに log base で debug するのが普通ならしい。Haskell とか break point の意味ないし。

水星の魔女

こっちも終わりまでみました。まーた、超能力エンドかよ。Vガンも逆シャアもそうだったし、進歩ないな。

お母さんが何したかったのかも良くはわかんないんです。でも、まぁ、

　　普通にしてれば、普通にハッピーエンドになる

そういう力はみんな持ってるはずなんだよな。そういう話だったかも。

まぁ、SFというよりは感性で進むみたいなものだからな。

BDレコーダーとか、Wifi経由のDLNAとかが割と不調。ご機嫌とるのも飽きたので、もう録画はやめてしまうかも。

宇宙兄弟

ちょっと絵があんまり好きな感じじゃなくて。敬遠してたんですが、ジャイアントキリングのあと読むものがなくて。

読み始めたら、六太が良い感じでした。時代背景はばかプーチンのおかげでだいなしですが...

この手の宇宙物って大故障大会なのが多くて。まぁ、宇宙兄弟もそうなんですが、実際のシステムだと細かいトラブルはあるからなぁ。

ISSも廃棄は確定だし。一方で月は、まだ有人は再開せず。

もっと自分は、ISS廃止賛成だし、月は無人でやった方が良いみたいな考えですけどね。

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の開発モードで開ける

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

WordPress から Hugo への移行のまとめ

WordPressのDBから *.md を拾ってくるのが正解な気もするけど、*.html から、直接 *.md 生成する方針で

で、theme も元の WordPress のを、そのままコピる。

*.md はPerl で find file しながら適当に。変換するファイルを list.txt に入れておく方式です。

ファイルの日付は、*.html に合わせて、それを保存します。

https://github.com/ie-developers/wp-to-md

これで、*/_index.md などができるので、これを content に入れて、hugo を設定すれば良い。

この時に、

　　content/ja content/en

とすると多言語対応が可能。

なのだが、元の WordPress の html file から、css / js を抜き出して、そのまま hugo theme にしまし√た。

抜き出した css / js は static の下。前後を header.html / footer.html で抜き出して layouts/partials に置く。

    ie-hugo-theme
    ├── LICENSE
    ├── README.md
    ├── archetypes
    │   └── default.md
    ├── layouts
    │   ├── 404.html
    │   ├── _default
    │   │   ├── baseof.html
    │   │   ├── list.html
    │   │   ├── section.html
    │   │   ├── single.html
    │   │   ├── staff.html
    │   │   └── top.html
    │   └── partials
    │       ├── footer.html
    │       ├── header.html
    │       ├── ie-jquery.html
    │       └── top-jquery.html
    ├── static
    │   ├── before.css
    │   ├── profile.css
    │   └── top.css
    └── theme.toml

https://github.com/ie-developers/ie-hugo-theme.git

config.toml は以下のような感じです (hugo v0.112.0)

    hasCJKLanguage = true
    baseurl = "https://ie.u-ryukyu.ac.jp/"  # Include trailing slash
    title = "home"
    copyright = "Copyright © 2021-2023"
    # canonifyurls = true
    paginate = 10
    theme = "ie-hugo-theme"
    drafts = false
    enableRobotsTXT = true
    [languages]
      [languages.en]
        title = "Your Website Title in English"
        languageName = "English"
        contentDir = "content/en"
        weight = 1
      [languages.ja]
        title = "Your Website Title in Japanese"
        languageName = "日本語"
        contentDir = "content/ja"
    [params]
      description = "This is a multilingual Hugo site"
      author = "Author Name"
    [[menu.main]]
        identifier = "home"
        name = "Home"
        url = "/"
        weight = 10
    [[menu.main]]
        identifier = "hugo"
        name = "Hugo"
        url = "/"
        weight = 20
    [permalinks]
        section = "/:sections/:title/"
    [frontmatter]
       date                       = [ "date", ":filename", ":default"]
       publishDate                = [ "publishDate", "date"]
       lastmod                    = [ "lastmod", ":fileModTime", "publishDate"]
       expiryDate                 = [ "expiryDate"]

LLVM clang merge

去年、LLVM16 やってた時に

　　merge を間違えた

らしく、ぜんぜん、merge されてない。おかげで、

　　全部手動で merge するはめに

まぁ、おかげで要らないコードをだいぶ減らせた。

Code Segment か普通のCの関数かを区別するために __code という型を入れて、void と同じ扱いにしてるんだけど、

その辺のコードが多い。本当は関数の属性で良いんだが... そうすれば変更は少し減る。

tail call forcing は LLVM でもだいぶ追加されてるんですが、まだ、足りない感じ。

正規言語とPumping Lemma

Pumping Lemma 自体は、Agda でだいぶ昔に証明したんですけどね、

　　0{n}1{n}

つまり、n 個の0とn個の1ってのは、正規言語じゃない、正規表現で書けないってのがなんか難しくって。

カッコの対応なので stack 使えば良いだけだが。授業中に書き始めて、これは難しいとなった記憶がある。

その残骸が残ってたわけですが、それは書き方が悪いな。生成器と検査器を書くんだが、

　　それが並行するように書くんだよ

片方再帰で片方ループとかだめだろ。ってわけでうっかり書き始めて一応書けたんだが複雑すぎる。

0と1の個数が同じってのが x ++ y ++ z と x ++ y ++ y ++ z とで両方成立するからとかやってる。

でも、書き終わったあとに簡単なのを思いつくのはよくある。

　　だから、検査を通るなら、unique に生成器と同じ

ってのを示せば、いろいろ証明しないで、x ++ y ++ z と x ++ y ++ y ++ z とを生成器と一緒に走らせればいいじゃん。

でも、そこそこ面倒で本質的には変わらないらしい。uniquenessを使うのは圏論っぽくっていいかな。

pumpling lemma は Berstein と似てるところもある。この辺の復習は面白い。

君は...

2回目みてきました。

そんなにねたばれがだめな映画ってわけでもないけど、さっさと見た方が。

やっぱり、子供が見にきてしまうんだけど、場違い感はあるかもしれないか。

でも、背伸びして、こういうのを見る子供ってのもいいよね。

最初は構えて見てしまうけど、二回目は落ち着いていろいろ見れるのが良い。

インディージョーンズ

引退する教授という設定ですが、80まで授業するの? 元気だな。

話はマンネリだが、マトリックス4みたいに変なメタなもの入れるよりはいいかも。

Hugo で表

学科の staff の page が表構造になってて。まあ、あとでもいいかと思ったんですが、

　　練習にちょうど良いかな

と思って。ChatGPT に

　　こういうHTML を hugo 出したいんだけど

というと、staff.yml を作って、template で生成できるらしい。なるほど。

<h2>教員</h2>
　　<div class="profile-list">
　{{ range .Site.Data.staff.staff }} <!-- staff.ymlのstaff要素を参照 -->
　　　<div class="profile">
　　　　<div class="profile-img">
　　　　　<img class="aligncenter size-full" src="{{ .image }}" alt="" width="250">
　　　　　<h3>{{ .name }}</h3>
　　　　　<p>{{ .nameKana }}</p>
　　　　</div>

まではいいんだが、その他はいろいろいろでたらめでな。

また、Hugo の Manual page が

　　　絶対に例題は書きません主義

らしくて。まったく、エラーメッセージは出さないは、くそな仕様にはするわで割とひどい。

issei にそういったら astra はどうですかとかいうのが、

　　　今更、また新しいのと格闘するのか?!

いや、この程度は学生はやってくれるはずなんですが、コロナ世代は自分からはまったく動かない感じだなぁ。

でも、ちょっと時間はかかったが、問題なくできました。

来週は学生に、英語のページを全部作ってもらおう。