qemu-system-m68k

なんで、そんなものをいじってるかっていうと、mc6809 に似てるからでさ

hw も作る必要があるが、それは m68k のやつそのまんまからでいいんじゃないか

で、armのsignularity build でサーバ吹っ飛ばしたわけですけどね

結局わかったのは、ChatGPTが作った例題のアセンブラはでたらめだったってこと。hw のソースを見ながらやってたら、

　　なんか、違うこと言い出した

まぁ、そうだよな。マイナーなハードは苦手なんだよ。あと、

　　m68kの -M virt は、作成中らしくバグっているらしい

そんなこんなで、hw のところも結構見たので、だいたい感じはわかりました。問題は

　　集中力に欠ける

ところだけだな。えーと、gdb 部分を外すところから?

singularity cross build and lima

qemu mc6809 をやってるんだが、m68k を元に書こうというわけね

ところが、MBAは aarch64で、学科のサーバは Xeon。で、その上で singularity で built するわけだが...
まぁ、普通に動く。でも、MBAで動かすか。で、

　Lima で動くのは Aarch64

いや、amd64 でも動くとはある

　singulalrity image を Aarch64 で built すれば良い

2023にできてて、そのimageも動く。しかし、

% singularity build --fakeroot m68k-arm.sif m68k-arm.def
INFO: Starting build...
FATAL: While performing build: conveyor failed to get: Error initializing source oci:/root/.singularity/cache/blob:639b1aee6821be62e6db147eb40cbd169d39c46a64fa1bbcbdb7d2a142733fc3: Error choosing an image from manifest list docker://arm64v8/ubuntu:22.04: no image found in image index for architecture amd64, variant "", OS linux

どういうこと? なんか変わったのか? docker://arm64v8/ubuntu:22.04 がないといってるので、podman で pull して、root で実行! で動いた!

　　/ に mount されて、server 死亡

をくらいました。いったい全体なんなんだ。いや、podman で pull してユーザで実行できないってどういうこと?

さすがに、もう一度試す気はせず、MBA上の lima で apptainer buildすることに

% apptainer.lima build --fakeroot m68k.sif m68k.def
INFO: Starting build...
Copying blob 71daa2c787b0 skipped: already exists
Copying config 368eb09313 done |
Writing manifest to image destination
2025/04/27 19:50:00 info unpack layer: sha256:71daa2c787b0984bbf3b93b60686fc9fe305d28e833914019b2745ab9f36730e
INFO: Running post scriptlet
FATAL: container creation failed: mount hook function failure: mount /Users/kono->/Users/kono error: while mounting /Users/kono: destination /Users/kono doesn't exist in container

これはわかる。/Users/kono が read only mount されてるわけね。apptainer.lima shell なら、問題なく動く。fakeroot の関係か

ところが
% limactl shell apptainer apptainer build --fakeroot m68k.sif m68k.def
なら、このエラーはでない。しかし、最後の .sif の書き出して失敗する。これも /Users/kono が read only mount されてるからだ

% limactl shell apptainer apptainer build --fakeroot /tmp/m68k.sif m68k.def

とすればできる。しかし、この /tmp は　VMの中だ

                                                               

                                                                                                                                              

   % limactl copy apptainer:/tmp/m68k.sif .                                                                   

                                                                                                                                              

として、取り出せば良い。これでできたんだが、Aarch64には m68k のgcc cross compilerと実行環境はないらしい                                       

          

花ぐるま、最終日

まぁ、いろいろあって閉めることに。ママもいい歳だからな

店で転んだりすると大騒ぎなので

47年やったらしいです。すごい

僕がいたのは、2009からだな

ママの歌だと「恋は神代の昔から」「津軽の花」「裏町人生」「情の唄」とかだったかな

お疲れ様でした

沖縄、急に暑くなって

なんか、体調こわしている人も...

まだ、汗かく感じでもないが

でも、もはや梅雨か。沖縄は、たまにスコールみたいな感じではあるんだけど

また、睡眠検査

今度は CPAP の圧力の調整らしい。また、電極つけまくって...

結構、かぶれるんだよな

と思ったが、前回よりはひどくなく

CPAPついてるので、夜中のおしっこも一回だけだった。その一回は途中鼻水でまくってたけど

沖縄は、もう暑くて、先週は寒かったのに。その温度差でやられている人もいるらしい

結果は5月ね。機材の調整もやるんだろうな。なんか remote でもできるらしい

ネットにつなぐとかは出てないので SIM 内蔵ってことなんですかね

qemu and Microwre OS9

前にいじったのは 2018くらいかな。その時に MMU を emulationすると、かなり遅くて。で、

　qemu の TCG生成/softmmu を使えば良いんじゃないか

とは考えたんだが、そこまでやる気はせず。でも、最近は暇なのでやっても良いかなと

m68k のをそのまま使って、code だけ書き直せばいいかな。page size は...

　　8kbyte

え? 6829 は 2kbyteだよな。と思ったんだが、どうも CoCo のMMUが8kbyteらしい。Nitros9 がそれで書いてある

問題は TLB flush に相当する命令がないってことね。MMU registerをアクセスしたら flush でもいいんだが

　　Nitors9 のコードもあるので、TLB flush 命令を入れることも可能

その方が簡単かな

いや、のんびり実装するので、いつできるのかは謎です

Okica trouble

なんか、ゆいレールでチャージしようとしたら食われました

駅員さんが、なんかわけわかんないこといって「改札口でチャージできます」でできたんだが...

1) Okicaのカードには裏表を判定するマークがる
2) 長年の使用で消えた
3) 消えるとゆいレールの券売機では使えない(裏表の判定があるから)
4) 判定のない機種なら問題ない

までは良いんだが...

5) 書類を書けば新品に交換する
6) しかし一日かかる

はい? デポジット返してくれれば新しく買うって言ったんだが「それはだめ」

まぁ、ゆいレールでは「改札でチャージしろ」ってことか

定期券だと印刷があるので裏表検出があるのはわかるんだが...

13年くらい使ってるからなぁ

Queen 来日50周年

なんか、NHK FMとかYoutubeとかでいろいろイベントが。NHK FMは最後の方だけリアルタイムで

あとは「聞き逃しサービス」で。今の人たちは「留守録」とかないんだよな。便利なんだが

いや、90歳のおじいちゃんカメラマンとか出てくるので、まぁ、あれなんですけどね

当時は、なんかアリーナのいい席を並んで取りにいって、それは妹に売って二階席で見るというパターン

楽しかったけ。Queenの面子もそうなんだけど、日本のファンも「日本のファンがQueenを育てた」という感じ

まぁ、でも僕自身は1st,2ndのプログレっぽい雰囲気が好きだったので、自転車あたりからは離れてしまったんですが

日本での人気はむしろ、その後の方がすごかったらしい

ラジオ番組では、その後のライブの話とかが出てて、その辺は少し距離ある感じだったな

hg and git

やっぱり、削除書くかと思って、RedBlackTree のrepository を見直してたら

　hg 側の uncommit change がある
　しかも、.git/hoge...

log を見ると、2023なB4がやらかしたらしい。まぁ、そうか

　hg rm -rf .git

なんだが、git 側が消えるのはよろしくないので、rsync で backup してから

なんだが、やっぱり触られてしまうらしい

開発用は hg で、github への commit は git という使いわけですけどね

肝心の削除の方は手つかず。めんどくさいんだよ

https://github.com/shinji-kono/gearsAgda/blob/main/BTree.agda
-

タワレコ

久しぶりに那覇のリュウボウにいったんですが、

　8Fにタワーレコードがある

LP/ビニール盤が1/4くらい。値段が2500円。8千円ってのもあったが3枚組かなんかかな

でも置いてあるものが、すげーふるい。デレクアンドドミノス? 横の映画館では「エリッククラプトンのライブ映画」やってるし

まぁ、若い人は使わないってことなんだろうな

いや、CDプレイヤー欲しいかなと思わなくもないんですけどね km5　のCP2 とか?

いきなり取り込んで、ネットで再生でいいわけなんだが

　　聞こうとすると接続が切れてる
　　そして、音質のダメなアマプラでかけられてしまう

いろいろ残念な時代でもある

シンセサイザーを踏む猫

なんか、音がするので。そっちをみたら、

　お前か!

善林堂

沖縄の文具屋さんですけどね

大謝名にできたので、ついよってみたのだが

「ぜんりんどう♪」という音楽が流れている

そして、消しゴムとか鉛筆削り、そして電卓。なんか、懐かしいものばかり

いや、昔は、そういうものに燃えた時期もあったんだけどさ

ちょっと高めのボールペンとか万年筆とか

で、極めつけがこれ

　　小切手タイプライター

おぉ? まだ売る気か?

赤ポ消滅

ingress は、赤ポをかき分けて、field 取るみたいな感じだったんだが、いきなり消滅

ライカムまで余裕で届く感じ。でも、

　　また、復活する噂も

まぁ、いいけどさ

階段

ingress やってると良くとおる

割と好きかもな

工事中でも人は通るようにして欲しいとは思ってます

さて、どこでしょう?

Seqouia

少し前に入れたんですが、特に期待はしてなかったんだが

　iPhone をMBAの画面に表示できる

で、いろいろやるんだが、だめ。ところが MBA を reboot したら接続しました

なんだけど、

　すぐそばにないとだめ。部屋が違うとだめらしい

単なる画面転送だろ? なんでだめなわけ? あと、画面操作が違う。それは致命的なんですけど。原神できないじゃん

というわけで、割とがっかりでした

あと、また、Calendar のDBが変わったらしい。放置中です

体重

まぁ、下げ止まってはいるんだが

腎臓関係の薬のせいらしく。でも、標準体重だからいいんじゃないというのがお医者さんの解釈らしく

まぁ、お酒抜いているのも原因かも

仕方ないので、もう一着、スーツを作りました

Lv12

ちょっと、ingress やりすぎ

歩くから、中毒性があるんだよな。ちょっと足がぼろぼろだ

赤ポを落とすと、武器が落ちるので少し便利

文字列同士のかけ算

文字列の長さの分、かけられる文字列を結合するってだけですけどね

　　% perl -le 'print "abc" x length("de");'
　　abcabc
　　% perl -le 'print "de" x length("abc");'
　　dedede

と非対称な演算になる。長さをみれば、普通のかけ算なので 6 で同じ

Perl では x という演算子で計算できる。文字列のかけ算という認識なわけだな

何の問題もない普通の文字列のかけ算だよね。数学的にはモノイド上の乗算で、非可換ってだけ

これが反順序たちにとっては阿鼻叫喚らしい

　こんなのかけ算じゃない!

みたいな話ね。なにやってるんだかね

リストを使ったかけ算は非可換になるってのは、2024の最初辺りには書いてるんだが、

　反順序たちはわからない

っていう問題があるらしい。目で見える掛順の非対称性ってわけですが、これに拒否反応を出してしまうのがだめなところなわけね

算数の教科書の最初の「かけ算の絵」自体も、これと同じ構造を持っているわけだが、見えない人たちには見えない

もっとも、PV=nRTの瓶三本

　　PV=nRT → P(3V)=(3n)RT

にも文句をつけるのが反順序。P(3V)=(3P)Vだが、瓶三本で圧力3倍にはならないだろ? これで掛順を理解しない人たちとの話なのでね〜

ガンダム Gqux

そういえばブックレットを配っているから、もう一回観にいくんだと思ってたら最終日に

ブックレット豪華と思ったら、中はスクリプトが大半でした

券を買うときに席をみたら「自分一人」

最後に特典映像がついていた

また、魔女なのか

新しいバッテリー

なんか、1600mAhと数値は上がっている

なんだが、磁石が弱いな。ポケットに入れると外れてしまう

まぁ、膨らんでないからいいか

Graph から CCC の普遍問題

Graph から CCC を作るのはできたので、普遍問題をやってるんだが

　　直積やCurry化の構造は、グラフ/公理の外にある

なので、その部分は「単にコピーするだけ」になるらしい

確かに、元の圏 A と、そのCCC である CCC A は別なので、まぁ、そうなんだけど

なので、CCC functor が単なる普通の関手でいいことに。なんだそれ? それでいいのか?

モバイルバッテリ

2022から非接触のを使ったんですが、なんか膨らんできた

また、新しいのを買ってもらえるみたい

iPhone 13PM 自体の電池もへばっているので、17が出たら買い換えの予定です

Graph からCCC

昔、Graph から圏はできたんだが、CCCをPostive logic経由で作るっ4てのができなくて、
Sets への関手を作って終わらすって技を出してたんですが、

　それだと、Setsの部分圏がCCCになってるかどうかわからない

なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた

Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん

f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)

という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は

　fmap (g ∙ f) z ≡ fmap g (fmap f z)

という分配則があって、それを使うと証明できた。そういうことなのか

それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、

e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]

が、うまくいかない。でもじっとみてると

　関数外延性を仮定するといける

らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです

で、まぁ、Graph から CCC はできた。

https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda

このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは

で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる