行列

東京は「意味なく行列ができる」都市なんですが、

　　どうも、うなぎのひつまぶし弁当

らしいってのを今日見つけました。パチンコなことが多いんだけどね。

あと、池袋は西口東口とも腐女子向けなお店が多く、そこにも行列が...

みんな並ぶの好きだね

JALの折鶴

こういう無駄なセンスが JALっぽいんだよな

誰もうれしくない Hospitality というか

ラウンジビールなしは残念

s/mime

要するに メアドに対応する CA に署名された鍵が手に入れば、それを KeyChain.app に登録するだけ。

それで使えます。

KeyChain から export して iPhone に Finder 経由で持っていくと (GoodReader -> File という分からん経路)
iPhone の Mail からも使えます。

で、送信する時にそれを使って署名をつければよいわけね。

署名が付いているメールが来ると、それに公開鍵がついているので、それを使って鍵マークで返信すると暗号化できます。

簡単ね。なのだが、

　　相手が署名された公開鍵を持ってない限りだめ

自分だけが持ってても意味ない。あらら。まぁ、やれよってことですな。マイナンバーに入れといてくれ。

GMail の Web mail は s/mime を有効にできるのだが、

　　Education License だと秘密鍵の upload ができない

いや、それやるべきかどうかは議論のあるところだよね。結果的に

　　GMailなWeb mailからだと電子署名/暗号化できない

ってことらしい。つまり s/mime を邪魔しているのは Google 様ってことね。

いや、だから、Mail.app で送ればよいわけ。で、CAに署名された鍵ですが、

　　Actalis

から手に入る。いや、署名するだけだからね? なんですが、

　　mac.com なメールのは手に入ったんだが
　　ie.u-ryukyu なメールのは、何かしくじった

何せ、なにかしくじったらリカバリ不可能。ま、べつにいいか。

学生は ie.u-ryukyu で送ってきてるので取れないことはないみたいです。actalis 以外に取れるところあるのかな。

東京

オリンピックの看板とか見かけないし、店頭での中継とかやってないので、ぜんぜん関係ない感じ。遠くのイベントですね。

全然、普通。平常営業。つぶれた飲食店も多いらしいが、まぁ、こうなるよね的な。

あったOBたちのワクチン接種率は結構高い感じ。東京は割と積極的だったからな。

自分も東京にいるうちになんとかしたい。

カレー配達人

というわけで、カレー10個運んできました。

　　土曜日に受け取って
　　大学と家に分散して保管
　　学生に空港に送ってもらって
　　OBに羽田まで迎えにきてもらう

という手順。移動にタクシーとか使ってるので

　　あんまり安くなってないかもな

今度は、箱を送りつけるパターンかな。結構、大きな冷凍庫持ってるのがわかったので。

グリーンチャンネル

カナがオリンピックの馬術を見たいというので。じゃぁ、一か月スカパー取るかと思ったんですが..

　グリーンチャンネルのオリンピック放送は無料

おお、太っ腹。

一か月とってもいいかなと思ったんですが、夏なのにろくなプログラムがない。さらに、

　BS4K/CS4Kは実は映らないのを発見(2Kは映ってる)

なんか偏波がどうこうのあれかな。一応、アンテナ的には大丈夫なはずなんだが。

でも、しばらく追求する気はないです。

台風

結局、連休はずーっと台風らしく。それでも、

　　大したことないからバスは動かすよ

なので、割と大学にいるのですが、何人か学生も来てるな。いつもの

　　バスから降りると大嵐

も食らいました。

で、なぜか月曜日から東京。しばらくいるはずです。別にオリンピックにでるわけでもないので、

　　どっかに閉じこもってプログラミング

でもしてると思われます。何書こうかな。

ingress の unique portal 稼ぎも可能だな。

OB用にカレーかついでいく予定。もっと、カレー引き渡しに便利な飛行機の時間にすれば良かった。

Packaging 続き

なんと fpm という ruby の package で一発で binary debian package が作れました。

便利。

なのだが、brew 側が mojave/catalina/BigSur/BigSur Arm とあるので難航中。

どうも brew は version が違うなら formula 別にしろってことらしい。まぁ、そうかな。

なんと、

　　M1 MacMini で clang 作る方が、2012 Mac Pro よりも速い

一つは packagの最後で ruby/fgrep が走るのだが、それが single thread なので core 数関係ないかららしい。

コンパイラ割とメモリネックだしなぁ。

2012 Mac Pro は Mojave までで、そのXCodeは 11.3 までらしい。Command Line Tool が上がらなくなると厳しい。

あと、BigSurもMBPで作るのはちょっとな。で、ゴミ箱な方を BigSur に。とかなんとか

　　時間かかる

学生ども手伝えよ〜

https://fpm.readthedocs.io/en/latest/intro.html

debian package

LLVM13はなんとかなったので、じゃぁ、

　　apt package

と思ったんですが、debian package って、結構厄介。ninja にも対応しているようなんですが、どうもうまくいかん。

sourceのtar ballがある前提なの?

じゃぁ、と思って brew for linux と思ったんだが、

　　singularity の sudoでしくじりまくる

つまり container とは相性がよろしくない。brew は Haskell とかも使ってるからなぁ。

単なる binary package でいいのにと思ったが、それでもいろいろやらないとだめらしい。

なんか簡単な方法ないのかな。

もっとも、singurarity の .sif でいいかなとも。でかいけど。

桃林堂の水羊羹

日暮里のお店に大学から自転車でいったかな。

沖縄からだと送料があれですが、みんなで頼めば怖くない。

甘いものがそんに好きなわけではないですけど。

楽しかった頃でもあるな。

いや、それなりに圧力あったか。

https://www.tourindou100.jp

リモコン

SKP75は大学に持っていったんですが

　　リモコンが使えないとなんにもできん

アンテナケーブルはさがしたら、すぐに4本でてくるのが大学っぽい。なんでもある。

で、リモコンも持っていったんですが動かない。なんで。まぁ、

　　10年ぶりに起動したリモコンに、すぐ動けといっても無理か?

また、持って帰って調べるしかないか。ってことは、

　　地上波は大学で録画

ですか。ま、いいけど。

かながオリンピックの馬術録画したいというので

　　NHKでは足りない

って話が。じゃ、スカパー取るかと思ったんですが

　　グリーンチャンネルはオリンピックは無料

そうなの? じゃぁ、それでいいか。今年は年初に一か月取ってるんだよな。

またとってもいいかなと思いましたが、まぁ、なくてもいいかな。

LLVM13/clang

先月もやってたんですけどね。

　　毎年のことだから、最新版に追従

ってことで、例年なら学生にやらせるくらい楽勝なはずなんですが...

なにか、妙にトラブる。やる気が低いってのが大きいんだが、

　　大半は、merge の時のミスだった

一行消えてるとか、 editor の操作ミス? ちょっと焼きが回ってるかも。で、残りは何かと言うと

　　初期のconv()とか正確に引数を指定してない場合にエラーが出るのを放置してたのを忘れてた

つまり、前回の仕様までは特に問題なくできてたのに気がつかなかったと。いや、

　　テストルーチンなおしておけよ〜　ちゃんとエラーメッセージだせよ

ってところです。あとは、

　　Linux用の apt package を作る

というのがあるのだが、singurality でどうするのかのイメージがまだつかめてない。

　　開発用のcontainerで debian package まで作って
　　仕様する側は別な container にする?

いや、途中からコンパイラのデバッグに入るっての良くあるんだよな。まぁ、

　　楽しい悩みかも知れないです

はびこるアロエ

子供の頃、おばさんが絞って飲んでたかな。

良くある光景ではあるね。

Programming 3

という名前の授業では既にないんですけどね。去年もそうだけど、学生もコロナ下でのプロジェクトは難しいらしく...

今年は、

1) Oculus Quest な魔法戦争もの

2) 学生向けフリマ

3) Unity での 3D 迷路ゲーム

いや、3D迷路は、80年代じゃないんだからやめろって言ったんですけどね。まぁ、Unity の練習くらいでもいいか。

Oculus Quest は魔方陣出してってやるんだが、HMDなUIどうするかで迷走中。がんばれ〜

フリマは、中国人な学生が主導しているらしく、Alibabaな micro service で作ってる。まぁ、これが良くできてるんだな。

GUIなWeb console で micro service を接続していくだけ的な。ただ、

　　Javaな Micro Service がメモリを食って、まともに動かない

らしい。無料サービスを使うとそうなるな。しかも、

　　Alibabaなframeworkで作ってしまったので、オンプレに簡単に移行する

というわけにもいかないらしい。やられましたね。データベースとか、そこそこ面白いんだが。

Javaのところだけ書き換えるという手もあるかな。ただ、技術的なところに気を取られてて肝心のサービスは微妙。

でも、それを含めて毎年いろいろ面白いです。

オンプレな環境に micro service framework を作ってあげるべきだと思うが....

今年は、まとめなWeb page をさぼってる(staticに移したとばっちり)もあったし、オープンキャンパスに出してもらうのも忘れたり。

いろいろ微妙。学生と一緒に迷走中です。

香港

牧港にあるお店ですね。割と軽い感じ。これでお粥とか亀ゼリーとかあれば。ないんですけど。

看板がちょっと面白かったので。チキンにしましたが量は日本人向きか。

この前から妙に役に立ってるケーブル

RD-Z1 片付けた時に、かなり捨てたんですが、

　　ま、一本ずつ取っておくか

で置いてあったケーブルが妙に役に立っている。まぁ、これが最後だろうけどな〜

テレビ側に端子があるのがすごいといえばすごい。

信号生成も楽なので、自作派にはうれしいものだったが。

いまはラズパイにもHDMI付いてるからな。

Sony BDZ FBT1000

そろそろ4K BDレコーダ欲しいかなと思っていたのでカタログは持ってたんですが、ソニーにこだわりはないが、移行は楽だから。

カタログは女性モデルの「お前は80年代から進歩してないだろ」的なもの。もっとも、80年代は、もっとメカとデザインを表に出してたか。

もはや、BDレコーダとかは世界的には衰退しててガラパゴスなものなんだよな。実際、

　　BSアンテナは生きていて、画面は映らないが録画は進んでいた

ってのを発見してなければやめてたかも。でも、なんかこう

　　録画整理する楽しみ

ってのあるじゃん。自分たちの世代には。

クロスバーはPS3からだったと思うけど、割と使いやすかったが大分前に廃止。でも微妙に残っているっぽいぞ。

リモコンの機能はほぼ同じ。SKP75は2011年なのに。ただ、

　　チャプター分割のボタンが廃止

ならしい。これは残念だな。いや、最近は、CM切りもめんどくてあんまりやってないんですけどね。(少しはやってる

でもレスポンスは良いです。10年差があるからな。　

自動録画は SKP よりはまし。SKP は「アニメギルド」とかあると、それに引っ張られてしまうっていう欠点があって...

画質は、まぁ、あんまり関係ないよね。4Kはまだ見てません。HDMIはAVアンプの方が4KはOkなんだが、なんかの新しい規格に追随してなくて

　　HDMI三本つかって平行配線しろ

とかあるが、やんないよね。やらないだろ?

何回もしつこく書いてるが、スカパーが字幕焼き込みしなければ、まだ取っていたと思うんですよ。そして、

　　Amazon Prime は字幕焼き込み

ってのを発見したしな。なんかそういうのを強制している人たちがいるの? Netflix は、まだがんばってるが、そのうち字幕焼き込みになるの?

やっぱり、米国アカウント欲しいかなぁ。

オープンキャンパス

ごたぶんにもれず、オンラインで。いやさ、

　　オンラインだと、リアルタイムでは観ないだろ?

自分だったらそうだからな。なので、動画も作っておこうとシス管には言ったのですが

　　オンラインの時に動画流すだけ

にしろと言ったつもりはなかったのだが。最近の学生は合成音声ですまして、それで良いと思うのだろうけど、

　　それだとライブ感に欠ける

と思うんだよな。オンラインで見るなら、その面白さみたいなものがあった方が。

二回目は動画にコメント入れてもらいましたが、そっちの方が良かったかな。

ゲーム班の方は、毎年学生に準備してもらうんですが、今年は油断してて忘れてました。

何となくやらんでよいだろと思ってた。ま、そういうわけにもいかんか。なので自分でやることに。

　　それもいいかな

午前午後で20人20人ですが、録画を見てくれる人がいれば、まぁ、いいかなくらいです。

例年だと結構人が来てたが...

雷の後始末の続き

結局、SonyのFBT1000を足したんですが、

　　まさかと思った、ビデオ端子から画面が見れた

ので、BD経由で録画の取り出しは可能。いや、手間が増えただけな気もするが...

新しいのは例のクロスバーUIをやめたやつね。中身は Andoroid?

D端子とHDMIで画面が出ないってことは、著作権関係の回路が飛んだってことかもな。

ちなみに新しい機材はビデオ端子なんかないんで、そういうわざは使えないみたいです。

お引越しダビングなるものがあるらしいが、2014以降か。SKP75は2011だからな。

超準解析を Agda で

うっかり書き始めてしまったわけですが、わりと順調。

超自然数は

　　HyperNat = ℕ → ℕ

整数は差を取れば良い。

　　data HyperZ : Set where
　　　 hz : HyperNat → HyperNat → HyperZ

で分数と。

　　data HyperR : Set where
　　　 hr :　HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR

等号とか不等号の決定はTrichotomous は排中律な仮定になるわけですけどね。

　　record _n≤_　(i j : HyperNat ) :　Set where
　　　 field
　　　　　≤-map : Bijection ℕ ℕ
　　　　　≤-m : ℕ
　　　　　is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map　k)

ってな感じか。これで、できそうなんですが、

Transfer principle ってのがあって「実数で証明できる性質は、超実数でも証明される」ってのがあるらしい。

確かに、自然数から上の方法で分数まで作って体になるので、そうなるんだが、それ自体をどう Agda で書くのかわからん。

　　transferN : ( p : ℕ → Set ) → HyperNat → Set
　　transferN p n = (k : ℕ ) → p (n k)

　　transfer : {R H : Set} → ( p : R ∨ H → Set )
　　　　 → ((x : R ) →　p (case1 x) )
　　　　 → ((x : H ) →　p (case2 x))
　　transfer {R} {h} p rp x = ?

ってなのを思いついたが、それで通るのかは謎だな。

David Byrne's American Utopia

沖縄では二週間だったらしく。油断してたら最終日。がらがらってほどではないくらい。

Talking heads は90年代に良く聞いたわけですが、NYダダイズムとか呼ばれてた時代ですね。

今回のライブ映像は

　　裸足なグレースーツで、ちんどんやっぽいステージ回し

で、面白かった。裸足だと結構怪我するが、サポーターみたいなのをつけてた人も。

予習はしなかったんですが、知ってる曲の方が多かったな。ってことは

　　40年間同じことやってたのか

ま、おじいちゃんがんばってるねと、自分に言いたい感じなものだったかな。

70年代の Stop making sense も良かったが、録画持ってるだろと思ったが持ってなかった。

手に入れても良いかな。

https://americanutopia-jpn.com

大学の無線LAN

システム更新前のアクセスポイントが確保してあるので、それを各部屋に配れば改善するはずですが、

　　まぁ、シス管の人手不足とか、自分のやる気とか

いろいろ。でも、

　　PoE なんだよな

今のスイッチで動くんだったっけ? と思ったが動くらしいです。

もっとも、

　　遠隔授業は、基本、有線派

家でもそうしたいが、配線がなかなかな。

Bijection と invariant

　record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)　where
　 field
　　　 fun←　:　S → R
　　　 fun→　:　R → S
　　　 fiso← : (x : R)　→ fun← ( fun→ x )　≡ x
　　　 fiso→ : (x : S ) → fun→ ( fun← x )　≡ x

ですね。割と当たり前なんだが、

　　Bijection ℕ (ℕ ∧ ℕ) と Bijection ℕ ( List Bool )

後者は今年のお正月にやって、敗れさっていたらしい。ぜんぜん簡単なんですが、Agda で書くのはな。

なんですが、やっと invariant を書くのになれたみたい。

fun← ( fun→ x )　≡ x　を直接証明しようとすると、関数の引数を調整しながら

　 定義と同じように項 fun← ( fun→ x ) が展開されるようにする

というのが必要になるんですが、これがだいたいうまくいかない。なんだけど、

　record Invariant (i : S)　: Set
　 field
　　 j : R
　　 k1 : fun← i ≡ j
　　 k0 : fun→ j ≡ i

というように書いてやると、k1/k0 個別に調整できるので楽になるというわけ。induction で、Invariant を作れば完成と。

ま、証明の細かい面倒さは避けられないけど。

この Bijection は超準解析や集合の濃度でも使うからな。

これで、Agda の練習用の問題は一通りできた感じ。

　　素数が無限にある
　　素数の平方根が無理数

https://github.com/shinji-kono/automaton-in-agda

原神

まだ、やってたりするんですけどね。このゲーム、課金のポイントと必要性がわからんのだよな。

問題は英語モードでやってるので、検索が良くわからん。人の名前が英語だし。つまらん台詞読む根性が...

金の林檎諸島は半分位まわりました。(と数値には出てる

Daily Mission は退屈だし、効率も良くないのでやめました。武器とか進化とかめんどくさい。

でも、夏のイベントでだいぶ成長させたので、雪山の頂上まではいけました。

Golden House が終わってないんだが、越えられそうではある。

うっかり、World level を上げてしまうと、いろいろ倒せなくなる。(きまった mission をクリアしなければ上がらない

World Levev 4 / Adeventure Lank 45 です。

なのだが、また、いろいろ倒せるようになってるな。Electro Hypostasis とかは、まだ、だめ。

もっとも、そこを目標にしなくても、ちんたら、お使いするのでも良いんだよな。

ノンアルコールビール

なんか、こう飯屋が早く閉まるのがなぁ。酒飲まないので、やせた人も多いんじゃないかな。

カフェで早めに夕ご飯でも、なんかノリがな

　　で、気分的に

ま、ちょっと癒される気もするかな。

割と酒強い方なので、そんなに変わらないから、アルコール入ってても入ってなくても差がない的な?!

わけわかんないもの

板にガラス玉がはめてあるオブジェっぽいもの

これも北上原の販売所にある

光とか当てるとどうにかなるとか

とうがん

どしゃぶり続きですが、

　　ingress は、やってます

北中城の販売所のとうがん。

カフェクッチェのとうがん入りのグリーンカレーを思い出すな。

テレビっ子

と呼ばれた世代なんですけどね。もちろん死語ですが。

結局、BDレコーダーだけでなくアンテナ全滅らしい。BDレコーダ SKP 75 x 2 は割と気に入ってた機械ですが、

　　D端子とかでも映らず

ただ、DLNA経由なら観れます。取り出す方法はないな。メニュー打てればいいんだけど、視覚に頼ったUIだからな。

東芝RDだったがWebリモコンに画面が映ったんだが。中身、Linuxなんだから ssh よこせとも思うけどね。

修理すると2万5千円飛ぶので、2台だから新品かった方が良いな。それでも、いくつか選択肢が

1) そのままアンテナ修理してもらう

2) CATVに乗り換える (月2千円

3) 録画はやめ、Netfliex とかで良い

まぁ、fj と同じで「テレビ視聴」ってのを動態保存したい気はする。テレビっ子ですからね。

録画整理も無意味な楽しみではあるからなぁ。この前も2015なベストヒットUSAとか発掘してました。

-