HDD 処分装置

うちのシステムは学生用だから、やばいものは置いてないので。でも、

　　使ってみますよね?

ってわけで、不要なものを持ってきて。昔のHDDってほんと溜まるよな。もしかすると G4 Cube 時代のかも。

あぁ、なるほど。二ヶ所に穴を開ける感じですか。それだと

　　粉々にはならいないな

まぁ、そんなものでいいならいいです。

GFS2の発掘

学生がないとか言ってたので。長いです。要するに GFS2 を cluster でなく single node で mount する方法。

1)　iSCSI の配線

単にdumb hubで全部繋げる良いわけですが、broadcast ping で生きてることを確認します。ping -b ... ね。

なのだが、Equalogic のは複数あるポートでダメな方があるらしい。ping が返ってこなかったのはそれだった。付け替えてok。

2) LAN 側の配線

サーバなら普通にもう一つ Ethernet あるでしょ。そっちをつなげて、DHCPなり直打ちなりで。

3)
　 iscsiadm -m discovery -t sendtargets -p 10.100.20.200
　 iscsiadm -m node --login

で login できるはず。できない時はなんかのaccess制限がかかってる。今回は volume の access record に IP address が書いてあった。

4) で、もう見えてるはずなので。

　　ls /dev/sd*

とか

　　pvscan ; pvs -a

とか。これで見えるなら苦労しない。

5) GFS2 だと cluster ので cluster を組まないと見えない。でも、

/etc/lvm/archive/vg_whisky_00010-793111190.vg とかの

　　　　status = ["RESIZEABLE", "READ", "WRITE", "CLUSTERED"]

を落とせば良いらしい。しかし...

　　vgcfgrestore vg_whisky -f　/etc/lvm/archive/vg_whisky_00017-1019350896.vg

で書き込めるなら苦労はない。 [ 7297.253396] blk_update_request: critical nexus error, dev sdc, sector 8
とか dmesg に出てる。

6) なんと、SCSIの reserve みたいな概念があるらしい。

　sg_persist --out --no-inquiry --register --param-sark=0xb8c90000 --device=/dev/sdb
　sg_persist --out --no-inquiry --clear --param-rk=0xb8c90000 --device=/dev/sdb
　sg_persist --in --no-inquiry --read-reservation --device=/dev/sdb

みたいにして、それをはずす。物理 volume 全部。

8) これで vg を書き込めるので、書き込んで

　 pvscan
　 vgscan
　 vgchange -na
　 lvchange -na

で logical volume が見えるはずです。でも、まだ、mount できない。GFS2: can't find protocol fsck_dlmと dmesg にでる。

7) 最後に lock protocol を使わずに mount すれば良いのだが、ググって出てくる

　 gfs2_tool sb /dev/mapper/nasVG2-nasdb proto lock_none

というのは、Redhat 7 からはないので、

　mount　-o lockproto=lock_nolock　/dev/mapper/vg_whisky-lv_whisky /mnt/whisky/

で mount の option で渡す。はい。見えた? え、でも、この volume じゃないの? 先に言ってよ。

中耳炎

なんか学生が zoom のやりすぎとかでくらったらしく

僕はさぼってるのでだいじょうぶなんですけどね。

まぁ、イヤホンなしでもZoom使えないことはない。

みなさんも気をつけて...

Sakura 側

というわけで、Sakura の方は問い合わせてみたんですが

　　あ、ごめん、理由は不明だけど、remote media のメニューありませんでした

でした。直してもらって、sftp で image 送ったら一発で Ubuntu が上がりました。楽勝じゃん。

学生にやってもらおうとしたんですが、

　　コンソールのボタンが出ません
　　Java が入ってません

とかいろいろ。コンソールボタン自体が JavaScript なのかな。popup block とかそんな関係らしい。

まぁ、ssh できてしまえば、関係ないところなので。

まぁ、でも、このクラスのを、この値段で使えるなら良いかなってところです。

VM あげるようなことはしないで、podman でがんばるらしい。

podman と k8s の関係がまだ不明なんだが、podman もだいぶなれてきた感じ。

発掘作業

システム更新、まだ難航していて、2015年ぶりのLDAPの設定なので、いろいろ変わっているらしい。sssd とか。

なんですが、

　　ネットニュースのVMを持ってくるのを忘れてるのが発覚

VMに二つ disk image が付いていたんだが「一つしか持ってきませんでした」だったらしい。ぐ。

まぁ、歴史的な意味しかなくて「動態保存」的なものなんですけどね。まぁ、筑波にだけつながればよいとも思うんだが。

問題は、Google group につながるかどうかくらい。

なので、GFS2を再構成してみることに。dumb hub で ping すると

　　4台のうち3台が応答

微妙。もう一台は 「 still initializing ... 」だめかもな。もっとも、生きてる二台の方にあるはずなので復旧できるかも。

AWS educate

2018/11 に blog があって、AWSの人が来てくれて登録したはずです。でも、

　　審査で待たされる

的な感じで、その時は使えなかった。そのまま忘れ果ててたんですが、9月になんかで見かけて入ると、approve されてました。(遅い)

で、Sakura の学生用サーバはあんまり使ってもらえなかった(Sakura Cloud そのままとかいうわけにいかなかった)ので、今年から AWS educate に。

class 作ってから approve に3日かかったんですが、その後の学生の追加は即座に反映されるらしい。一人 $50 にしたけど、そんなものでいいのかな。

今までの課題だと ansible または image のupload で的なものなんですが、AWS だと

　　cloudformation

っていうテンプレートで Wordpress くらいはすぐ動く。はずですが、DB の接続が良くわからんな。でも、Apache の page はすぐに見れました。

好きに使ってもらって良いんですが、なんか面白い課題を緩募中。

がんがん使うなら学科のサーバに建てる方が良いね。

d3js

シス管の移行作業を横目で見ながら、OSの補講の様子を discord で見ながら...

　　そういえばOSの課題で使ってるPerl/Tkなんとかするか

malloc を繰り返して fragmentation を graphical に見るって奴なんですが、いまどき Perl/Tk 入れさせるのもな。X11 いるし。

　　HTML生成して、そっちで graph を拡大縮小スクロールできれば良い

ってので、いろいろ探すんですが、まぁ、

　　CSS + JavaScript って最低だよね

なにが最低って、何年か前に学んだものは今では「最低最悪、あれはやるな」ってことになってるのが普通。で、見つけたのが

　　d3js

なるほど。まぁまぁ、使えるみたい。

svgContainer = d3.select("body").append("svg")
.attr("width", 1200 * scale)
.attr("height", 300)
.attr("id", "halfpage");

svgContainer.selectAll("rects1").data(elements).enter().append("rect")
.attr("width", function(d,i) { return xydata[i*2+1] * scale;} )
.attr("height", 20)
.attr("y", 175)
.attr("x", function(d,i) { return xydata[i*2] * scale; })
.style("fill", color)
.style("stroke-width", 1)
.style("stroke", "black");

ってだけだな。なのだが、前のの消し方がわからん。exit().remove() じゃ消えんぞ? もう良いよ

　　 svgContainer.remove();


で。ってわけで svg を毎回消すという残念さ。でも、できたから良いか。

Ceph

予想通り苦労しているわけですが... Ceph は

　　osd  データを入れておくところ
　　mds メタデータを入れておくところ
　　mon どこに入れたかを決めるところ

みたいな感じなんですが、

　　mon を移行させることは考えてない

らしく。サーバ切り替えのIPアドレスで、それぞれの関係が切れてしまったらしく osd を接続できないってな状態に。

中身が見えないじゃん。

まぁ、サーバ移行して構築しなおせば良いのだが、旧ディスクサーバは外しちゃったしな。現物はあるんだが、

　　GFS2を再度構成しないと読み出せない

おーい。まぁ、やるかと思ってたんですが、

　　NetGear x 2 の方にバックアップがある

え? まだ旧機材はあるが残ってるかな。と思ったら

　　あった

なので、degrade している NetGear から復旧で乗り切るみたいです。Ceph いまいち信用できんな。

Discord で OS 補講

いつものOSの補講です。遠隔で良いと言ってるのだが...

　　遠隔授業を乗り切れるような人はOSを落とさない

なので、結構な人数が登校。まぁ、せいぜい換気してください。

授業と違って「みんながもくもくと課題をやる」なので、Zoom には向かない感じ。Zoom は break out でもばらばらどが足りない。

そういうのには Discord が向いてるらしい。画面配信とチャットが複数勝手に走る感じ。

　　課題やってる人は配信しながらやってね

で、そこを巡回する感じ。そうすると、

　　やっべ、先生が来た

とか言うことに。初日は「この課題がやさしいから、それを優先してやって」みたいな感じなので順調なようです。

bot が簡単に作れるのが良いな。

国勢調査

最後の電話入力でばっちりバグ踏んで、最初に戻されました。こういうの得意。

いや、あのシールなハガキでURLとIDだけでも良いのに。パスワード同じ紙に載せるのは意味ないだろ?

自分的にはマイナンバー書くと終わり的なのを期待してたかも。

紙とWebとどういう比率になるんだろ?

理工系の女子学生の数

 

自分の時にも160人中13人とかそんな感じ。うちの学科でも60人中2-16人くらい。はっきり、

　　女子学生が多い方が活動度が上がる

一つは女子学生の方が能力が高いことが多いからかな。女子の方が語学能力が高いのでそうなるのかも。

普通にすると半々ぐらいになるらしいので、

　　理工系の才能の半分は見逃している

ことになる。残念です。日本特異な現象で、明らかに異常。

社会人でも、理系な発想の女性は良く見るし、理系の標準教育を受けてないのは残念な感じ。もっとも

　　自分で勉強すれば良い 

博士課程の時に結婚出産なんていう例も。そういう人生設計も割と良いと思うんだよな。理系男子ちょろいし。

でも、今は文系でも

　　微積、線形代数、確率統計、解析力学、量子力学、プログラミング

からは逃げられない感じですかね。

Sakura Internet の方

使い方難しくって。自分の意図としては

　　学生がお金を気にせずに心置きなく使えるサーバ

ってつもりだったんですけどね。ま、使う奴は AWS/GCP 使うし。結局、OSの演習用に。AWS/GCP 様は

　　無料分で使ってください

で終わり。まぁ、それでも良いのだが学生には敷居が高いかもな。クレジットカードとか。なので、Heroku とか使って

　　Heroku 、5分たっても上がりません

とかやってる。というわけで演習用は外してしまいました。

システム用は

　　専用サーバ + 44TB HDD
　　DELL R720xd 　CPU：Intel Xeon E5-2630 v2 (2.60GHz 6Core) ×2
Memory : 16 GB

って構成で、まぁ、クソ古くても動くなら許す。メモリ16GBはいまどきは無理ゲー。

なのだが、OSが Centos 7。それは許されないです。なんですが、
Ubutntu を入れる方法がわからない。Centos7 とか向こうが用意したものは

　　PXE経由で install される

ずるい。HTTP経由の仮想メディアでできると書いてあるのだが、接続した仮想コンソールにはそんなものはなく。

　　iDRAC7 の機能を使うんだが、それがサポートされてない感じ

Windows でもだめ。ここで諦めて Sakura にお手紙を出しました。

学生は Centos7 に Ubuntu を上書きして上げるという技を出したんですが、grub2 を吹っ飛ばして終了的な。

44TB RAIDで22TBですか。自動で mount されないのであれこれ探したが

　　root@localhost ~]# lspci -nn | grep -i raid 02:00.0 RAID bus controller [0104]: Broadcom / LSI MegaRAID SAS 2208 [Thunderbolt] [1000:005b] (rev 05)

と

　　dmesg | grep sd

で見つかりました。mount で -t してしない方が勝手にやってくれるのか。xfs が最近の標準?

Apple One ...

なんか、また、subscription させよう系ですが... うちは二人なので family は中途半端。Apple TV+ 微妙だし。

iCloud Stotage を50GBにしたら family が外れたらしく、その時に

　　怒りにまかせて自分は無料にした

らしい。なので5GB。でも、まぁ、写真の同期を手動でやれば問題ないらしい。まぁ、そうなるか。Photo Stream も切ってしまった。

なので、かなり Apple のしがらみを断ち切ったようです。

別に月千円が高いとは思わないけど、あっちもこっちもじゃな。iTunes Match 入れてるんだけど、なくなる予感。

なぜか、iOS のupdate/backup とかは iTunes 経由でやってたりするんですが... Catalina ではできるのか?

システム更新続き

いや、どれだけ続くか謎なんですが...

　　今までのシステムはVM base

20個はない。最初はそれくらいあったんですが。油断するとっていうか、最後の手段として

　　今のVMをそのまま移す

ってのがあるわけ。それが一番簡単。でも、それをやらなせないのが面白いわけですが。

2015に作ったAttonのAkatsuki、VM、PCのIP address管理システムは、あっちーのあれを元にしたアプリ。Ruby on Rails で、それなりに

　　うちの誇りかも

他のところはどうしてるんですかって聞いたら「買うんです」って言われるものだな。

でも2005だから、Docker baseのテスト環境で作られる。でも、それをVM baseで移行されそうになる。

　　それはだめだから

で、うちのgitlabなソースと格闘するわけですが、OBが

　　先生、それ、僕が書いたもっと新しいのがあります

う。確かに、Rails 4 はおかしいとは思ったんだよ。ごめん。でも、

　　giblab のどの fork が新しいのか

くらいは明確にして。最新の reposotiry を見つけた後は瞬殺だったようです。いや、

　　LDAPとの戦闘がすんでいた

からだがな。

https://github.com/atton/akatsuki

システム更新

まだ、滞ってますが、今週中にはなんとかなるはずです... そういえば、

　　あっちーがいた頃、一週間でまったく設定が進まないのを見て、自分でその場でメールニュースまで設定した

が、長田先生に「あっちーにやらせてください」と怒られたのを思い出した。あの時からのCentosじゃないかな。

現行サーバは100Vに移しても特に問題なかったので、電源の問題は避けられたみたい。いや、まだ、

　　ラック移行して6台上げたら、死にました

ってのがありえるけどさ。

現行サーバは自分たちでリースバックを買い取って使いますが、どれくらい持つかは謎だな。

やることたくさんある割りには

　　逐次に一つ一つ片付けてる

気がする。まぁ、自分が把握できて良いけど。問題は

　　今やってくれてる学生は来年はいない

し、いま付き合ってくれてる来年いる学生はほとんどいないことだな。まぁ、でも、それも

　　サーバ班を立ち上げた辺り

は、そんなものだった気がする。だいたいの作業は Zoom で共有しながらやってるので、覗いてもらえると面白いと思います。

いや、ぜんぜんわからないかも知れない? だいたい僕がわかるまで突っ込むので大丈夫。基本を確認しないとね。

　　え、光差し替えたらストーム? なにやってんの!

Zoom で

とかいったけど、夕ご飯の直前だったし、

　　repository に入ってる卒研の中間発表

へのコメントを MatterMost に書き込んで終わり。Zoom でうだうだやるより、Chat tool の方が早い。

Wifi の設定も一悶着あったけど、

　　一つ一つ設定を確認していくしかない

でも、まぁ、それを一人でやるのは辛くて

　　みんなでわいわいやりたい

気持ちはちょっとわかる。

A&WからA&W

いつもの緑のエージェントに立派な多重を作られてしまって。まぁ、すぐに落としにいくような無粋なことはしないんですが。

といいつつ落としにいくわけですけどね。牧港のA&Wから、普天間、そして坂田の公民館か。というわで、普天間のA&Wまで。

なのだが、なんと閉店のお知らせが。あの辺、一休みできるところがあんまりないので、重宝してたんだけどな。

これもコロナの影響か。

ネットワーク入れ替え

ルームスイッチ、メインスイッチ、NAT用のUTMなどなどを入れ替え。

　　しかし、ループが結構でる

まぁ、そんなものかな。メイン側からみてループしてる現場にいってループを抜く。そんなものなのか。

ディスクサーバに光をつないでもらったので、25TBのコピーは一日で終わると期待したい。でも、Ceph だからなぁ。

　　「この緑の配線なんですか?」

とか、

　　2005年のF社製 1Gbit Ethernet hubが大量発掘されたり

とかいろいろ楽しいです。

システム構築

LDAP飛ばしたり、LDAPS で接続できなかったり苦労しているようですが、Ceph と KVM が構成できたらしく、久しぶりに学生の歓声をきいたような。

僕は、macOS のVisual Studioと格闘したりしてたんですけどね。二つ、zoom を上げているわけではなくて、遠くから歓声が入るみたいな感じ。

いや、まだまだ山はあると思うけどさ。まだ、Ceph にファイルコピーしてないし。ちなみに納入されたディスクサーバのディスクは既に一つ飛んでいるようです。

Catalina で 32bit バイナリが動かなくなったのは地味にきつい。別に VM なりコンテナなりで古いのが動いたって良いじゃん。まぁ、メンテが面倒ってのはわかるが。

いや、自分のMBPは Mojaveのままですけどね。

赤田風

blogによると 2008/3 以来らしい。メニューが12年前と同じ。

　　変わらないことが素晴らしい
　　変わらないことが難しい

瑞仙の43度が良かった。変わらず美味しいものをありがとうございます。

沖縄女子短大 / Ingress

きらきらビーチの方ですね。ポータル減衰率が元に戻ったらしく、そこら中が白ポに。なんので、おっきくCFが張れる。

琉大と儀保駅でつなぐわけですが、琉大儀保間は、まぁ、バスとゆいレールでなんとかなります。

なのだが、西原のサンエーくらいまでなら、まぁ、バスでなんとかなるんですが、(いや、沖縄でそんなことするのはめったにいない)

きらきらビーチは厳しい。なので、車で連れていってもらいました。車なら割とすぐ。

こういうのを三ヶ所から青の面子で代わりばんこに張る的なのが楽でよろしい。

Data.List.Fresh

Agda で昨日発見しました。sort された List を宣言できるという超素晴らしい。

　　ins : ISortedList
　　ins = 0 ∷# 1 ∷# 3 ∷# 10 ∷# []

いや、なにが素晴らしいか全然伝わらないと思うんですが、順序を間違えるとエラーになる。

いや、そこじゃなくて「順序が正しいことを実行や証明で使える」ってところ。

ところが、

　　module _ {a} (A : Set a) (R : Rel A r) where
　　　data List# : Set (a ⊔ r)
　　　fresh : (a : A) (as : List#) → Set r
　　　data List# where
　　　　[]　 : List#
　　　　cons : (a : A) (as : List#) → fresh a as → List#
　　　infixr 5 _∷#_
　　　pattern _∷#_ x xs = cons x xs _
　　　fresh a []　　　　= ⊤
　　　fresh a (x ∷# xs) = R a x × fresh a xs

簡単な定義のわりにさっぱりわからない。fresh ってなんだ? いや、

　　単に insert したいだけなんですが...

で、見つけたのがここ。なるほど、total つまり、≦ か ≧ どっちかってのを使うのか。そもそも

　　　fresh : (a : A) (as : List#) → Set r

Set を返す関数ってのは普通のプログラミングには出てこないし、単なる型とも違うので難しい。

　 ttf : (a : FL (suc n)) → (y : FList {suc n}) →　fresh (FL (suc n)) ⌊ _f<?_ ⌋　a y　→ fresh (FL (suc n)) ⌊ _f<?_ ⌋　x y
　 ttf a [] fr = Level.lift tt

こんな風に、関数で定義された型で受けるらしいです。いや、Agda、まだまだ、新鮮だな。

https://gist.github.com/aristidb/1684202

サーバの電源

BIOSレベルで Exceed Power Limit といわれるらしく。1.6Kw x 2 のが4台、Disk Server 2台なんですが...

　　結局、現場にいかないとわからんだろ?

で行ったんですが、

　　配電盤には200Vはきていて、二つ配線されている
　　現行サーバは100Vで動いている
　　UPSは200V対応

さらに、

　　床の適当な100Vを使うと Exceed Power Limit
　　UPS側から取ると動く

なのだが、6台動かすとUPSが文句をいうらしい。おそらく、現行サーバは200Vで動いているんじゃないの? テスタではわからんかったけどさ。

非接触な電流計もあるはずなで、それで見てみるか。

　　じゃぁ、2台 + Disk Server 2台で取りあえず良いだろ?

で4台で動かしてます。これで順番に設定していけば良い。

台風で結構停められたので、ぜんぜん、設定が進んでない。間に合うのか〜　サクラ側は Ubuntsu 入らんとか言ってるし。

まぁ、順番に見ていくしかないな。

Zoom 同窓会

大学院のですけどね。なんか在籍時の domain MTL がそのまま。でも、田中先生が教授になってからのOB/OGの面子の方が中心。なので知らない人ばっかりだ。向こうから見てもそうだよな。

でも、まぁ、自慢話大会にはなるので、そんなに居心地は良くないです。ですが、先生に顔見せるのは大切。

沖縄からだと普通はさぼるのですが、オンラインならまぁ。最近はそういうの多いだろうな。

その自己紹介廻すの日本的だからやめようよ。そこはチャットでスルー的な感じにして欲しいです。

台風は、かなり、それたのでちょっと雨風あったくらい。ゆいれーる停めたみたいだが、必要なかったか。

まーた、台風

 そうそうに学科のサーバを停められてしまったので、大学にはいかずに。有線が生きてればいっていたかも。

　　なぜか、メインスイッチは停めない

方針らしいので。メインスイッチ停めないならサーバも止める必要はないのではないか? まぁ、

　　この前の計画停電でメインスイッチの電源を飛ばした

ってのをリアルに思い出すわけですが... MRAM base なシステムが普通になると、サーバの電源を停めるという発想はなくなるかもな。

電源異常に間に合うように保護してくれれば問題ないわけなんですが... 

なんか PowerEdge の1.6Kw電源がぶーたれてて、200V必要なんじゃないか説が。文句いってるだけなら無視して良いが...

システム更新いろいろ

なんか、今日はいきなり「センタの新LDAPのテストは明日まで」とかいうのが降ってきて。おいおい。ちょっとまって、

　　Centos 7 で戦うのはやめて...

TLSでつながらんとかやってますが、まぁ、なんとかなるはずです。岡崎先生も忙しいのにご苦労様です。

QNAP の方も一つコピーが終わって、二つ目をコピー中。6TB x 2 を吹っ飛ばした割には被害はなかったらしい。

　　6TB x 2 はバックアップ側に使っていたから

まぁ、光学メディアもあるので最悪でも全部なくなるわけではないから。

ガロア理論の続き

いろいろ面白かった。大半は Agda の流儀に苦労してただけだけど。

　　単純に順列を数え上げてリストにしても全部数え上げたことにはならない

まぁ、そうですよね。結局、concrete な数列表現との bijection (一対一対応)を作らないと。

　　data　FL : (n : ℕ )→ Set where
　　　 f0 :　FL 0
　　　 _::_ :　{ n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

Data.Fin の降順列にしてやると良いらしい。bijection では書きにくいので iso と書いてしまうが、isomorphism は演算の保存も含むので少し違うか。

順列は結局は具体的な数列なので、それが等しければ順列置換としても等しい。つまり、

　　FL-inject : {n : ℕ }　→ {g h : Permutation n n }　→ perm→FL g ≡　perm→FL h → g =p= h

変換した先が等しいなら元が等しいってのは、injection というらしい。これは圏の言葉だと equalizer だな。

もともと圏論はガロア理論から作られたらしいので、同じようなものが出てくるのでわかりやすい。

　　数学は一つ理解すると、他の物も理解しやすくなる

ってやつですね。

5次の対称群が可解でないのいのは、3次の対称群を含むから abc を含むのが反例という風に書けば良いらしい。

　　 counter-example :　¬ (abc 0<3 0<4　=p= pid )
　　 counter-example eq with ←pleq _ _ eq
　　 ...　| ()

　　 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →　x =p= pid　
　　 end5 x der = end sol x der

abc あると、全部 pid になるという end5 の反例になるってわけ。

　　¬sym5solvable : ¬ ( solvable (Symmetric 5) )
　　¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) )

solvable ならend5 が成立するのだが、それには反例があるみたいにやるわけね。abc は以下の二つで作ります。

　　 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }　→ (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
　　　　　→ deriving n (abc i<3 j<4 )
　　 dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ }　→ (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
　　　　　→ deriving n (dba i<3 j<4 )

右向きと左向きがある。deriving は「その対称群が含む部分群の要素を判定する述語」だな。それは data Commutor で書かれていて

P g → P h　→ Commutator P [ g , h ]　この部分が、[ g　, h ] のかっこをしたものという制限になってます。


　　[_,_] :　Carrier　 → Carrier　 → Carrier　
　　[ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h

　　data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
　　　uni　 : Commutator P ε
　　　comm　: {g h : Carrier} → P g → P h　→ Commutator P [ g , h ]
　　　gen　 : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙　g　)
　　　ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g

　　deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
　　deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
　　deriving (suc i) x = Commutator (deriving i) x

uni は不要らしい。gen も交換子の積が必ず交換子になるなら不要だな。

三次の対称群は数え上げて record で書き下しました。20 x 2 。でも、そうすると Agda が死にやすい。停まらない。

いろいろ、bug っぽい挙動も見かけたが、正確に型を書くのが基本らしい。

　　https://github.com/shinji-kono/Galois

予定通り J Key が

F key が壊れた時にキタムラのお兄ちゃんに「次は J ですね」と言った通りに J のキートップが壊れたのでなおしに行ってきました。

今度は、部品があるからすぐだった。

台風はたいしたことなかったんですが、

　　コンビニがからっぽ
　　しかし、まるよしは開いている

ってなところですね。まだ、9月だからな。

Ingress の drone

stay home 対策らしく。 最初、南へ飛ばしたんですが、激戦区なのでポータルが落とされて戻される。

北部は平和なんですが、ポータルの間隔が広いので届かない。

なんか、行けたのに戻ってこれなかったり。届くかどうかは気分次第? 距離じゃないのか。