twitter archive / Perl / GPT

twilog が使えなくなっちゃって。まったく、不便にすることにはまめな人たちだからな。代わりのツールは一切でず。

なので、2020でとまってた twitter の archive を取ることに。ところが、

　　全開付いてた CSV はなくなってた

それを grep するツールを作ってたんだが。JSON が100MBずつ三つなんだよな。Web UIがあるんですが、なにせ

　　20万tweetもある

ので、実用的な速度で動かない。twilog は問題なかったんだよな。偉大だった。いや、

　　CSVのgrep で問題ない

わけですよ。なので、JSONからCSVを生成することに。昔、そういうscript作ってて発見はしたんだが動かない。

Anatouf は JSON::PP 使えとか言ってたんですが、こんな感じで問題なく動きました。

　　my %tw;
　　my $id;
　　while(<>) {
　　　　chop;
　　　　if (/\"id\" : \"(\d+)"/) { $id = $1; }
　　　　if (/\"created_at\" : \"(.*)\"/) { $tw{$id} .= $1 . " "; }
　　　　if (/\"full_text\" : \"(.*)\",$/) { $tw{$id} .= $1; }
　　}

　　for my $t ( sort {$a <=> $b}　(keys %tw) ) {
　　　　print $t," ",$tw{$t},"\n";
　　}

　　#　　　"id" : "1201579915",
　　#　　　"in_reply_to_status_id" : "1201560603",
　　#　　　"created_at" : "Thu Feb 12 04:22:35 +0000 2009",
　　#　　　"favorited" : false,
　　#　　　"full_text" : "@mizobuchi 自作です。TZを設定してdateを呼び出してるだけ。",
　　#　　　"lang" : "ja",

手抜きだ。本当は red black tree に読み込むのが良いのだが、これでも数秒で CSV に変換できる。

ついでに GPT4 で JSON:PP も使ってみたんですが、これが割とでたらめでな。まぁ、minor だから仕方ないんだが...

　　JSONの line alignment を無視する ( incl という incremental option がある)
　　いきなり全部のファイル(300MB)をメモリに読み込もうとする
　　上の script でもそうだが、読みながら sorted tree を作るのをさぼる
　　そもそも syntax error が...
　　無意味に CSV module を使おうとする

Has::Ordered を使えとかいうと使えたりする。存在しないAPIを発明したり。確かに、

　　TIE hash API から、Red Black Tree を呼ぶ

とか面白いことは面白いんですけどね。Modern::Perl なんていう module どこから探してきたんだ?

まぁ、その時その時の「さっさと作る scriptのアルゴリズムのさぼり方」は、無理だよな。

Safariのbookmark folder

よく使うのをまとめていた folder があったんですが、なんかの拍子に消してしまって

調べてみたら30日以内なら iCloud のbackupにあるらしい

ゴミ箱じゃないのか? そもそもなんであっさり消える

なので、そこから restore したんですが、100個のうち20個くらいしか戻らない

いや、割と Web service の途中のとか怪しいリンクが多かったことも確かなんですが...

残りはなんとかするか

昇華の塔

宜野湾は沖縄戦の激戦地だったので、そこここに塔があるわけですが、佐真下公園のは昇華の塔という名前。

なんか工事してると思ったら、なんかダサいことになってる。

別に多少崩れててもいいんじゃないかと思ったりしますけどね。でも工事されてるだけまし。

まつぼっくり公園の散歩道は崖が崩れて、そのまま通行禁止で放置。

山道なんだから、そういうリスク込みで歩けば良いわけで通行止めってのは残念だな。

運動公園展望台の道も橋が崩れて放置。

まぁ、徐々にインフラを維持できなくなってるってことか。

圏論と関数型プログラミング

2014くらいからやってるんですが、そんなに難しい離しでもない。要するに、

　　型を対象、関数を射と呼ぶと圏になる

というだけなので。

関手は型変数a を持つ data F a とaに対する fmap。自然変換はF
aからG bへのdataの変換で、f : a -> b に対して可換なもの。木
をリストに変換する flatten : tree a -> [ a ] とか。

自然変換がfmapに対して可換なdata構造の変換ってのはわかりやすいよね。

何の役に立つかというと、fmap とか可換性とかで、コードが満たしている性質、
要するに invariant が見やすくなるというだけ。

Monad は Maybe a で理解するのが良い。関手であることは fmap があるからすぐにわかる。
mu : Maybe (Maybe a) -> Maybe a
return : a -> Maybe a
は当たり前でしょ。

g : a -> Maybe b
f : b -> Maybe c

で、f (g x) とは書けないけど、mu (fmap f (g x)) で意味が通ると気がつけば良い。

fst x , snd x) が x に等しいっていうのが、pair の uniqueness だが、これがLimit とか普遍問題の解とか表現可能関手とかいろいろ言われてるだけではある。

　　c
　　|
　　v
a <- (a,b) -> b

で、h : c -> (a ,b) があれば、f : c -> a : h (fst x) を作れる。圏論の用語が煙幕なだけで本質は簡単。

Proofs and types には圏論は一切出てこない

Natural deductionとsequent calculus、system Tとsystem F

さらにsystem Fの強正規化、sequent calculusのcut eliminationが載ってる

しかも、薄い！素晴らしい本だ
http://paultaylor.eu/stable/prot.pdf

圏論だと少し勧めにくいけど、

Introduction to Higher-Order Categorical Logic
https://t.co/avsLk9iCjF

を使ってて、わからないところがあると、

Categories for the Working Mathematician
https://t.co/k2jDYFtixH

を使ってます。

血圧と薬

もうだいぶ長いですけどね。一日、一錠なので楽。なんですが、やっぱり忘れるんだよな。なので、

　　血圧測定と一緒に

で、iPhoneのShort cutで、server上に記録する方式。体重もそれが良いかも。なのだが、

　　やっぱり、忘れる。血圧の方の記録を。

薬は忘れないんだよな。飲んだら、ケースを出しておくようにしてる。

なので、血圧の方を忘れるのは本末転倒な感じ。

もっとも、父は自分の歳には脳梗塞でぼろぼろだったので、まぁ、

　　血圧の薬で保っているようなところがあります

stable diffusion と rails の続き

singularity で stable diffusion を動かすのは結局、

　　build する時の apt-get に -y を忘れた

というしょうもない問題だったらしい。なんだが、

ImportError: cannot import name 'SAFE_WEIGHTS_NAME' from 'transformers.utils'

の方がまだよくわからん...

rails の方は

　　apt-get で落ちる

つまり、

　　user mode podman では、そういう image は作れない

ってことらしい。なるほど? root で作った image を user mode podman で動かすことはできる。

そういうものなのか。じゃぁ、

　　rails7 も singularity でやってもらう

のがよ8いんですかね。user mode podman でなんでもできてしまうってのも変なんだけど。

じゃぁ、singularity ならいいのか?! apptainer がなんか singularity と挙動が違う...

いろいろわからんな。

造波水路

いや、20年も琉大にいるんだが、動いているのをみたのは初めて。

水道代がかかるので、年一回しか動かない噂を聞きました。

え、そこの池のを使えば?

あぁ、もうGWで、その次はOS研究会だ。

Winny

見に行ってきました。学生と一緒だが、学生はあんまりピンとは来てなかったみたい。

　　youtube, github な時代の学生に、当時の closed source な Windows binary の配布の話はどうなの?

とも思う。

まぁ、当時のCRTとか、ThinkPad、そして、Windows 2000 な画面、ぱかぱかガラケーは割と楽しめたかな。

　　シーンが暗すぎる

自分は特に割と明るくしてプログラムする方なので.. 当時のBlack on white だし。

あの歳で食べながらプログラムすると太る...

映画自体はテンポ悪いし地味だしで勧めづらいな。「まぁ、地裁だからな」で片付く話な気もしました。

懸垂

なんか学生が持ち込んでました。置いてくと捨てるのがめんどいのだが。

鍛えてるのとかそうでないのとかいろいろ。

iPhone の相談

まぁ、ママさんたちからそんなのを聞かれるわけですが

　　なんか password を聞かれる

ありがちと思ってみてみたら

　　聞かれてるのは iCloud password

それはやば過ぎる。reset には複数台必要なんだが、あるはずもなく。なんだが、

　　Apple support アプリってのがあって、それだと他の人から reset できる

ふーん。で、やってみるんですが、

　　reset したいiPhone上で、パスコードを聞かれる

解決と思ったんだが、

　　ママさん、それが通らないとおっしゃる

え〜　それは詰んだかな。いや、なんか「まて」とか言われるんですが、メールが送られるらしい。iCouldに。

いや、それは読めないです。読めないよ。ここで諦めた。キタムラかApple Storeでなんとかなるかも知れんけど、

　　なんともならなくて、full reset

って可能性がある。彼女たちは割と簡単に諦めるみたいではあるんですけどね。

　　全部消えちゃったから、電話して

とか言われる。

せめて二台持ち。あるいはPC使ってほしいかなぁ。特にLINEは消えやすいので...

サーバ室見学

シス管を三年次の実験でやる奴の一環なんですが、割と受けは良い。まぁ、そんなにすごいわけではないけど、

　　物理サーバ

が見れるのは良いよね。

レールで引き出せるのと、旧システムを買い取ったので引き出せないのとある。

最近は、AIの方が人気ではあるんだが、まぁ、学生はよろこんでいたみた。二回にわけてやるので来週もあるはず。

自分で組んでおいてなんなんだが、割と振る舞いがなぞで。今日も、Aerohive が30人越えると遅くなる現象ってのがあるらしくて。

実は321だけでなく322もAerohiveってらしく「322は遅いってのはなんだったんだ??」になってます。

NATのなんかのtableの関係かな。

apptainer と podman

既にかなり使いなれてるはずなのに...

　　apptainer で stable diffusion 動かす

ってだけなのに、anaconda がどうこうで、なんか作れない...

　　user mode podman　で rails 動かす

ってだけなのに、いろいろこけるのはなんでだ。bootsnap がどうとか、

　　gem update --system

例の肉

なんの肉かは忘れました

MBP16 重い...

いや、89年の3.4kgのDynabookから、ずーっと持ち歩いてるわけなんですけどね。17inch PowerBook も3kg。
それに比べればMBP16は軽い気もするんだが...

最初の頃は鞄が1年持たなくて。ぼろぼろの鞄でもずーっと使ってるのは、長く持つのがそれだけだったってのもある。

でも、最近、ちょっと右手がしびれる感じもたまにあって... で、

　　GPD3試す

とかやったんだが、やっぱりキーボードがつらい。いや、持ち歩いても良いんだが。それでも、

　　MBP16より全然軽い

普通に13inchでいいじゃんという気もするけど。とかいろいろ迷ってるが

　　結局 MBP16 に戻ってます

16MBPとMac Mini そして、持ち歩きはGPD3という風にしたい気もする...

ChatGPTと数学

いくつか聞いてみたんですが、Referenceがでたらめってのは、置いといて...

推論はしてくれないので、知ったかぶりレベルなんだよな。で、自分でもそうなんだけど、

　数学の本は、おれおれ定義と用語で突っ走ってるのが普通

その中では閉じてるわけ。それで合ってるのが、むしろ不思議なレベル。なので話が合わない。

数学は異なる視点があって、例えば線形代数は集合でもあるし群でもあるし圏でもある。そういうのがだめらしい。

話は合わせてくるんですが、その先にあるモデルがない感じ。まぁ、ないものねだりしてもしかたないが。

じゃぁ、Agda ではどうなのかというと、

　　字面の証明の後ろには、かなり複雑な証明のλ項がある
　　それは数ギガの大きさを持つことがある

つまり、モデルを表す巨大なデータ構造があるらしい。それは、LLMそのものだとも思うんですが、

　　AIがLLMそのものを扱えるのか
　　数学者はそもそも、その数ギガの記号モデルを扱っているのか

あたりが面白いかな。

質問の仕方が悪いと「意味がない」とか言ってきて面白いです。

Q 商群の定義は普遍問題だったりする?

A 商群の定義は、実際には余普遍性に関連する問題です。群 G とその正規部分群 N が与えられたとき、商群 G/N は、以下の余普遍性を満たすものとして定義できます。

π は G から G/N への射であり、N をその核にもつ準同型写像である（すなわち、π(n) = 1_G/N となる任意の n ∈ N）。
任意の群 H と G から H への準同型写像 f で、N を核にもつものが存在する場合、一意の射 g: G/N → H が存在して、f = g ◦ π となる。

カラオケとらぶる

なんか、フリーズさせちゃって。いや、だから、そういうの得意なんだよ。

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

で、フリーズで、ソフトリセットでも治らなくって。だから、そういうのが得意なんだって。

そこで「電源抜いたら?」で食らったのがこれ。

最近のDAMってハードディスク入ってるのか。fsckするのはださいだろ。log structured file system じゃないのか。

結局、担当の人が来るまで Boot しませんでした。Boot したら、なにごともなく動きました。

　　ありがち

ラッピングツール

当然もってます。学部3年の時に自作機作った時だな。なので、64Kbyte DRAMはそれで配線してます。

ピンにワイヤをむかずにくるくるってやる。それで導通。外すときには反対側を使う。

ただ、ピンがかなり長いのが気に入らなくて、結局、半田に戻ったんだよな。

　　そんなに半田付け上手くないくせに

でも、プロトタイプには向いてるよね。

ラッピングワイヤがかなり減ってるのはさすがかも。でも、半田付けの時はウレタン線使ってた。

実家からウレタン線を回収し損ねたのは痛恨。銅線だったのに。

ChatGPT使ってる?

今日は、TAや先生とその学生と少し話ができたので、聞いてみました。

　　ほとんど使ってない

聞いたことはある程度らしい。いや、今年からのレポートとか課題とかどうするんだよってところなんだけど。

肝心の学生が

　　一番保守的

だからな。まぁ、確かに、ChatGPT使ってると怒るようなダメ先生はいるだろうし。

自分の印象は

　　ChatGPTは鏡で、自分のできることと相関する感じ

「あぁ、まぁ、そういう解答だよね」ってのが多くて感心するのとは違うかな。ちまたで聞いた怖い話は

　　データをそのまま突っ込んで解析を聞く

いや、そういうツールは別なものであって、ChatGPT自体は計算は苦手ってのはよく言われているのに...

そういうのを含めて改良されていくとは思いますけどね。とにかく

　　ちゃんと質問できて、解答の真偽を判断できること

が必須なので、使い方で格差がでるのはそうだろうなぁ。

blog を三分で書く

ま、ちょっと難しいですね。無理に書く必要はないんだが。

今年はなんのソースを読むかな。ChatGPT役に立つのか?

プリンどら

沖縄のもんではないらしいです。これが、

　　中身が激硬い

そういうの流行りなのか? 300円は強気だが、パーキングエリアだとそんなものか。

外から入れるのは知っている人は多いかも。バス停あるし。

年度が変わると動がないプログラム

卒研登録のページなんですが、gitlab で「今年だけ取り出す」方式だったらしく、生成したら「全部消えました」

去年までは gitlab ci ではなかったらしいので、それで前の年のが残るので動いていたらしい。

gitlab ci だと毎回ゼロから生成だからな。まぁ、gitlab の元の方は残ってるから。

ありがちなばぐではあるな。

マイナンバー保険証

使ってみましたよ。なんか、

　　お前が自分でやれ

って言われる。やると、

　　顔認証

とかいってくる。当然、

　　認識しない

なに考えてんの? ぽっとでの技術で動くってか? でも、暗証番号でもいける。最初からそれにしろ。

で、そのあと、いろいろぐだぐだ聞いてくる。それはひどいんじゃないの?

　　頭の悪いセールスマン

としか思えないですが。まぁ、いつものように、

　　マイナンバーの悪いところは物理カード

なので、それがなければ、普通の保険証がマイナンバーに結びつけられて、アプリから履歴が見れる

で終わってたはず。そして、

　　それを絶対に修正できない

ところが、日本政府の終わっているところだな。物理カード廃止で、使用率100%なのにね。

プログラムと証明

昔書いた、Hoare Logic を見直してたんですが

　　メタで証明を切り分ける

ってやってたんだが、最近、証明ばっかりやってたので、

　　切り分けると書きづらい

となってきた。Agda だと命題だけ書いて証明後回しで良いので、無理に切り分けなくて良いのではとなってます。

という話をOS研究会でやるのか?!

Apptainer on Aarch64

前の続きなんですが、singularity の名前が apptainer に変わったわけで、

　　apptainer は macOS 上で lima で動く

なんですが、Intel のコンテナを ARM で動かすのはださい。なので、

　　Aarch な container image を作ればよいんでしょ

というわけで、Aarch64 な Ubuntuから作るかと思って、それは動いたんですが、

　　attainer 自体が、qemu-user-static を呼び出して、Docker image pull から動かせる

なるほど?

apt-get install qemu-user-static

してやって、

BootStrap: docker
From: arm64v8/ubuntu:22.04

と、.def に書けば良いだけらしい。もちろん、細かい差はあるんですけどね。

ってことは、もしかして、macOS 上で build するのも可能だったのか。

macOSの brew もだいぶボケてきてて、container base が良いかもしれない。

インストール大会

なぜか新入生はスーツ。なんで、って聞いたら、入学式があるから。

コンベンションセンターだから、気持ちはわかる。でも、うちはそういうところ
じゃないから。

相変わらずMacですが、SSD256Gかぁ。ぎりぎりかな。課題をサーバー上でやればまぁ。

学認

そんなものがあるのを発見したんですが...

　　当然ログインできない

なんでだ。cs のアカウントじゃないのか。教務情報は入れるんだが。

なんか、センタのアカウント管理が紙で送ってくる方法じゃなくなったみたいらしいので、

もちろん、締切りには間に合わなかったんですが、まぁ、一応、送ったはずなんだけど、

　　消されたかもれない

一回、母が倒れて東京に通ってた時に、やっぱり新年度で消されて、センターまで言って復活してもらった記憶がある。

また、聞きにいくかな。教務情報に入れないとかなりやられるんですが、学認はまぁ必須ではないから。

X68000Z

どっちかっていうと、思い入れがあるのは8bit のOS9の方ですけどね。OS9/68K も使ってなかったわけじゃないです。

その頃は、Vax 730にはまってた。でも、今から考えると、

　　もっとアセンブラいじるべきだった

とは思いますけどね。OKITAC4300とか、Z80の並列マシンなTopstar があった。

一応、linker / assembler も付いてる。

グラディウス動くのはすごいけど、ファミコンでも動いてはいたからな。

今年も登場してました

農学部まめだな

カレーパーティ

超久しぶり。人数は4年次限定な感じで、10人以下で。

でも、あやっぱり人数少ないと楽。多いといろいろ大変。

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

　タンドーリチキン、パニプリ、チャパティ、ラッシー、パパド

ですかね。リハビリ的な感じ。