GCD

冬休みのプログラミングです。Automaton の授業の例題に√2が無理数ってのをやろうとしていたらしいんだが...

　　gcd26 : (n m i : ℕ) → 1 < n → 1 < m　→ gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )

という簡単な部分で停まってます。割り算なんだけど、全部引き算で実装するわけなんだが、

　　gcd1 : ( i i0 j j0 : ℕ ) → ℕ
　　gcd1 zero i0 zero j0 with <-cmp i0 j0
　　... | tri< a ¬b ¬c = j0
　　... | tri≈ ¬a refl ¬c = i0
　　... | tri> ¬a ¬b c = i0
　　gcd1 zero i0 (suc zero) j0 = 1
　　gcd1 zero zero (suc (suc j)) j0 = j0
　　gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
　　gcd1 (suc zero) i0 zero j0 = 1
　　gcd1 (suc (suc i)) i0 zero zero = i0
　　gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))　j0 (suc j0)
　　gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0　

　　gcd : ( i j : ℕ ) → ℕ
　　gcd i j = gcd1 i i j j

と簡単なんだが、四つの引数の制約が足りないようだな。対称性とかは示せたんだが。

これができると、√2の他に素数が無限にあることとか、そんなのが証明できるはです。

そんなことをしながら大晦日か。

256番

ぴったり感のある番号のバスですが

　　意地でもゆいレールと北谷/沖縄市を結ぶ路線は出さない

という感じですかね。56番のてだこ浦添止まりなんだが、

　　既存路線を短くして自慢する

ってのは面白いな。

浦添前田の接続の56番の終バスは真栄原止まりとか、いろいろ面白い。

もっとも、最近は那覇にはあまりでないわけですけどね。

〆

特に区切り感ない人なのですが... 仕事納めは昨日だったらしい。でも、うちのゼミは火曜日。

ハリーズ開いてるのか説もあったんですが、ちょっと両方で様子見してしまったか。

　　ちゃんと予定を聞こうぜ

学生は人数頼まないととか言ってましたが、いや、10人分とか頼むのは前もって言っておかないと。

一応、お店は昨日までだったらしいです。また来年、よろしくお願いします。

ゼミもお休みではあるのだが、危なさそうなB4/M2には見ようかな。

久米のチャコ

今年のシス管はシステム更新で大変だったので、打ち上げは「チャコでステーキ食おうぜ」で。先月の話ですが。

なんか写真取る方式の検温計が。

　　やってる感が出てよろしい

レアで頼んだんですが、10oz じゃぁ、ミディアムにしかならんか。

まぁ、昔の味は思い出補正があるからな。BSE騒ぎで日本のステーキは割と残念になった気がする。

宜野湾も10時まで

さすがに、那覇浦添沖縄市には文句がついたか。いや、飲んでもバスがあるのは良いかも。意味あるのかとか言ってる人もいるけど、

　　確率だから、時間を短くすれば減る

ま、ゼロにはなりませんけどね。いや、本気度が足りないんだよな。中国や韓国みたいに「二週間封鎖」みたいにすれば解決なんですが。

武漢であれだけ猛威をふるっていたものが収まっていることは確かなので、まぁ、そうすれば良いだけのものらしい。

　　でも、できないもんだよね。いや、「やらない」ですか。

素粒子物理とか、ソフトウェアのバグとかと同じで

　　確率の低いところが問題になる

のは現代的な気がする。そういう時代なのだな。

個人に対してがんばれと言えばなんとかなると思ってるあたり、この国は戦時中と変わってないのだとも思う。

Agda apkg はだめ

結局、DivMod 通らないので apkg はあきらめ。とりあえず、Homebrew から入れなおし。

Solver とか面白いんだけど、

　open AlmostCommutativeRing ring
　-- The solver is flexible enough to work with ℕ (even though it asks
　-- for rings!)
　lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
　lemma₁ = solve-∀

こいつって、Data.Nat じゃないんだな。これを Data.Nat に引き戻す方法がわからない。

もっとも、もっと、ずっと簡単にできる方法がある気もする。

いや、~/.cabal が悪さをしていたらしい。削除で解決。

Google Cloud Directory Sync というそびえたつくそ

LDAP と Google のアカウントを同期するって奴なんですが...

なんか学生が苦労しているので... なんと、

　　Java 8 なアプリで、Browser 立ち上げて認証

で、Ubuntu で動かないとおっしゃる。今までは Windows なPCで動かしていたらしい。

どうせ xdg-open で開けてるのだろうと思ったんですが、そんなんでは動かないらしい。

　　Java 8 だからな

なので、

　　捨てるのが良いらしい

です。代わりは CSV でやれと? 本気?

対角線論法とHalting Problem

対角線論法は割と簡単に(やっと)書けたのだが、Halting 問題の方は良くわからない。

　　 Bijection TM (List Bool)

自体が矛盾するので、 TM = List Bool → Bool にしないで、そのうちの encode を持つものみたいに限定するのだろうな。
で、halt が encode を持つとすると矛盾くらいか。いや、そう書こうとしているんですが...

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

open Bijection

diagonal : ¬ Bijection　( ℕ → Bool ) ℕ
diagonal b = diagn1 (fun→ b diag) refl where
　　¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
　　¬t=f true ()
　　¬t=f false ()
　　diag :　ℕ → Bool
　　diag n = not (fun← b n n)
　　diagn1 : (n : ℕ ) → ¬ (fun→ b diag ≡ n )
　　diagn1 n dn = ¬t=f (diag n ) ( begin
　　　　　 not diag n
　　　　≡⟨⟩
　　　　　 not (not fun← b n n)
　　　　≡⟨ cong (λ k → not (k　n) ) (sym (fiso← b _)) ⟩
　　　　　 not (fun← b (fun→ b diag)　n)
　　　　≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
　　　　　 not (fun← b n n)
　　　　≡⟨⟩
　　　　　 diag n
　　　　∎ ) where open ≡-Reasoning

年内の授業は終わり

でも、あんまりめどのついてない修士のためにゼミはやるかとか考えてます。オンラインだしな。

OSの教科書は、今年は手に入りやすいものと考えて、

AN INTRODUCTION TO OPERATING SYSTEMS: CONCEPTS AND PRACTICE
https://www.amazon.co.jp/dp/B085B1W656

を使ってるんですが、微妙な感じ。問題が Review Question とかやさしいものが分離されてる。まぁ、それもいいか。

タネンバウム先生のも良いんだが、なにせ問題が「メインフレーム」だったりするからな。

いまどき、ハードウェアとかOSとか流行らないよ的な意見もあるかも知れない。でも、プログラミング技術的な興味もあるし。

キャンパスバス実証実験

まぁ、いろいろひどい。琉大からてだこ浦西を結ぶわけですが...

　1. そもそも遠隔授業で学生があんまりいない
　2. 終バスが18時前。修士で18時前に帰るなんてありえない。朝は来ないし。
　3. 北口からてだこ浦西までは高速バスで3分なので琉大には意味がない
　4. 真栄原までは98/広栄からは125とかぶり
　5. 北口までなので東口の文系や病院の人は使えない

そもそも需要がずれてる。足りないのは

　A. ゆいれーるからの遅い時間の接続

てだこ浦西のバスは21時にはもうない。ゆいれーるは0時着がある。浦添前田は22:39があるが真栄原止まり。

　B. ゆいれーるから330/58の接続

このバスは確実に宜野湾営業所から来る。なのに、58号線からは人は乗せない。

　C. 琉大から沖縄市への接続

長田の乗り換えは200m歩く。誰も乗り換えてない。

まぁ、沖国からは便利かも。本数の少ない125の代わりにはなる。真栄原から大学へのバスの本数が増えることにはなるな。

スタバから琉大に直接行ける。

琉大生はバスがあんまりに不便なので、だいたい車で通うから。

http://www.watta-bus.com/news/detail.php?news_id=156

西原

たまに ingress で廻るわけですが、西原サンエーまでバスで行って、お昼ご飯と思ったが、

　　予想通り、ベトナム料理屋さんは開いてない

どうせ、そうだろうと思ってたよ。どうしようかってところなんですが、サンエーまでも戻ってもたいしたものがあるわけでもなく。

そういえば、大典寺から登る手がある。ぐぐったら、48分。48分であの坂登るのか。あぁ、まぁ、上原からバスに乗る手があるか。

で、ローソンで適当にすませて、坂を登りました。

トポロジー

なんとなく来年はチコノフの定理やろうと思っていたのだが少し書いてみました。

record Toplogy　( L : HOD ) : Set (suc n) where
　 field
　　　 OS　　: HOD
　　　 OS⊆PL :　OS ⊆ Power L
　　　 o∪ : { P : HOD }　→　P　⊆ OS　　　　　 → OS ∋ Union P
　　　 o∩ : { p q : HOD } → OS ∋ p →　OS ∋ q　→ OS ∋ (p ∩ q)

これは filter に似てるな。

record Filter　( L : HOD　) : Set (suc n) where
　 field
　　　 filter : HOD　
　　　 f⊆PL :　filter ⊆ Power L
　　　 filter1 : { p q : HOD } →　q ⊆ L　→ filter ∋ p →　p ⊆ q　→ filter ∋ q
　　　 filter2 : { p q : HOD } → filter ∋ p →　filter ∋ q　→ filter ∋ (p ∩ q)

実際、コンパクトが超フィルターが集積点を持つことに対応するらしい。量は多いけどできそうな感じ。

別に集合でやらなくても良くて束上でやるとか自然数上でやるとかでも。ただ集合論も基数できてないし、トポスもやってないし。

群論も正規部分群とかやってないんだよな。いろいろ老後の楽しみがたまっていく感じ。

パイプライン伊祖近辺

パイプライン道路は、昔、米軍基地へのパイプラインがあった通りらしく、自分が来た頃は、まだ残骸が残ってました。

人が通るわけじゃないから、上下動お構いなしで、ジェットコースターみたいな感じ。それが好きで通る先生も。

なんですが、だいぶ整備されて割と普通な道に。ここも、だいぶできたきた。車線増やすのだろうな。まぁ、バイパスのさらにバイパス的な。

その先の低くなっている辺りは、雨が降ると水没するあたりですが、それはなんとかなったのか?

介そばとスタンプラリー

パイプラインの嘉数のところにあります。バスが遠いから、なかなかいけないが、

　　Ingress のついでなら

割と普通に美味しい。で、なんか、

　　沖縄そばスタンプラリー

なるものが。しかし、名護とかですか? バス派には、ちょっと厳しい感じだな。

でも、我如古のは行ったことがない。今度いってみよう。

これって公式サイトみたいなのはないのか。

GCC cross compiler on Homebrew

単に自分で拡張した GCC10 な arm cross compiler を作りたいだけなんですが...

問題は ARM tool chain と GCC 10 の pthread.h がずれているかららしく。いや、prefix と読むべき header の位置がずれてるとかも。

そんなわけで、libgcc のコンパイルを通すことはできないらしいので、

　　　File.open("make.sh", "w") { |f| f.write "\#!/bin/sh\nmake \"$@\"\nexit 0\n" }

と必ず成功する make の shell wrapper を通すことに。こんなんで良いらしい。tool chain 自体は brew install -s すれば良いだけだらしい。

そもそもの問題は作った gcc が system 側の as を参照してしまうことだったんですが、どうも hard coded されてるらしく、

　　　"--with-as=#{arm}/bin/arm-none-eabi-as","--with-ld=#{arm}/bin/arm-none-eabi-ld",

と、こちらも hard coded で対抗すればよろしいらしい。LLVM はこういうクソな問題ないので、LLVM だけにしてしまいたいです。

GCC側

単に cross compiler 作れば良いだけなんだけど。clang 側は割と簡単に片付いたんですが、

　　GCC側が libgcc.a 作るところでこける(pthread関係)

いや、そんなもの要らないので、他は make -k でできるので良いんですが、

　　brew install

が許してくれない。くそ〜 macOS 上で作ってる好き者はあんまりいないしな。そもそも install 先をこそこそ見たりするし。

ま、ふっとできるかも知れないです。

hgweb date of Mercurial

久しぶりに LLVM いじったら、brew update から始まって環境設定に2時間... 恒例の Mercurial の hgweb の date の表示の修正です。

なんで、2 weeks ago とか 2 month ago とかだすのか理解できないです。2年前以上は日付がでる。ぜんぶそうしろよ。計算できないのはアメリカ人だけだから。

hgweb.config で指定できるべきなんだろうけど。ちなみに、hg もやっと Python3 に対応したらしい。全部のファイルが10%ずつ変更なので、つらいのはわかる。
pycompat なんてのがあるのか。

　　+firefly+one diff -c templatefilters.py　templatefilters.py.orig　
　　*** templatefilters.py　Mon Dec 14 19:40:36 2020
　　--- templatefilters.py.orig　　 Mon Dec 14 20:47:18 2020
　　***************
　　*** 86,93 ****
　　　　　　　　　return b'in the distant future'
　　　　　else:
　　　　　　　delta = max(1, int(now - then))
　　!　　　　 # if delta > agescales[0][1] * 2:
　　!　　　　 if delta > agescales[3][1] :
　　　　　　　　　return dateutil.shortdate(date)
　　　
　　　　　for t, s, a in agescales:
　　--- 86,92 ----
　　　　　　　　　return b'in the distant future'
　　　　　else:
　　　　　　　delta = max(1, int(now - then))
　　!　　　　 if delta > agescales[0][1] * 2:
　　　　　　　　　return dateutil.shortdate(date)
　　　
　　　　　for t, s, a in agescales:
　　+firefly+one diff -c templates/static/mercurial.js templates/static/mercurial.js.orig
　　*** templates/static/mercurial.js　　　 Mon Dec 14 18:31:49 2020
　　--- templates/static/mercurial.js.orig　Mon Dec 14 17:23:04 2020
　　***************
　　*** 293,301 ****
　　　　　　　　　　　　　　　　　　return "in the distant future";
　　　　　　　　　　　　　　}
　　　　　　　　　　}
　　-　　　　　　　　 if (delta > (scales.day)){
　　-　　　　　　　　　　 return shortdate(once);
　　-　　　　　　 　　}
　　　
　　　　　　　　　　if (delta > (2 * scales.year)){
　　　　　　　　　　　　　　return shortdate(once);
　　--- 293,298 ----

getArgs 解決

やっぱり「落ち着いてやればできるだろ」と思い直して。

Data.Text.Text とか言ってるので、getArgs が Text (おそらくutf8)を返しているんだろと思ったんだが、実は、

　　grep Text MAlonzo/**/*.hs | more

したら、

　　MAlonzo/Code/Agda/Builtin/String.hs:type T6 = Data.Text.Text

とかやってて、Compiler が Agda の String を Haskell の Data.Text.Text に変換してるわけね。そうといわかれば、

　　open import Codata.Musical.Notation
　　open import Data.Maybe hiding (_>>=_)
　　open import Data.List　
　　open import Data.Char　
　　open import IO.Primitive
　　open import Codata.Musical.Costring

　　postulate
　　　　getArgs : IO (List (List Char))
　　{-# FOREIGN GHC import qualified System.Environment #-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

　　main : IO ⊤
　　main = getArgs >>= (λ x →　putStrLn $ toCostring $ sym5solvable $ getNumArg1 x )

という感じで、 IO (List (List Char)) で受ければよいと。

Monomorphic な Agda では Monad の修飾構文はよろしくないらしく、直接、getArgs >>= (λ x → と書くのが残念な感じ。

Agda の getArgs

五次の交換子を計算すると終わらないってのに気がついたんですが、

　　なんと、Agda から Haskell にコンパイルすると瞬時に終わる

それだと計算結果を証明に使えないのだが... まぁ、いろいろあるな。

で、そうすると、引数渡したくなるわけですが、

　　postulate
　　　 getArgs : IO (List String)
　　{-# FOREIGN GHC import qualified System.Environment　　#-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

とかしろとあるわけですが、まったく動かないです。IO coString だったりとか、getArgs が Data.Text.Text になったりで
おいていかれているっぽい。github 上の getArgsの例題が軒並み動かない。

まぁ、コンパイルするような言語じゃないからなぁ。

Portal Scan

なんか、ポータルが点灯してるのでinsgessのNEWSみると Scout がどうたらと。ぜんぜんわかんないのでさらにぐぐったら、

　　Portal Scan しろ

と。え〜　あれ、周りの動画を撮るとかなんだよな。時間かかって面倒くさいだけ。気持ちはわかる。

　　Portal 周りの動画を集めて AR みたいなのをしたい

ってことでしょ? でも、携帯回線で動画の upload なんてしないです。しないよ。

まぁ、動画撮って、あとで Wifi のある所で送信とかなら。ただで仕事させるなら、もっと餌が良くないと。メダルだけではね。

ガロア理論一段落

一段落詐欺はいろいろあるわけですけどね。プロシンのネタので、締切前に終わっていたはずなんだが、まぁ、良くある。

残ってたのは順列の数え上げと交換子の数え上げがちゃんとできてるどうか調べるだけなので簡単だったはずなんだが....

順列の数え上げ自体は簡単で高校生でも書けるプログラムなわけなんですが、結構、難航。Fresh List の慣れもあるかな。

普通プログラムって何通りも書き方があって、まぁ、だいたいどれでも動くわけ。ところが、Agda だと

　　停止性とか、順序の正しさ、そして、全部入っていることを確認する方法

とかが全部つながってないとダメ。つまり、かなり特定の方法、再帰に特化した方法で書くことが必要らしい。

結局、三四回書き直す羽目に。でも、図書いて、ちゃんと再帰になるように書いたら、ぐっと短くなった。で、できあがり。長かった。

交換子の数え上げの方は任意のFresh List二つの組み合せに抽象化できるらしいんですが、ちょっと書き方がわからなくてやってません。

ガロア理論と言っても正規拡大体とかやってないけど、Agdaはむしろそっちの方が得意かもな。圏論に近いから。

来年は、チコノフの定理やろうかな。集合論あるし。Filter で圏論的にやるなんて言う手もあるらしい。

そんなわけで、詳細は、オンラインで開催されるプロシンで話します。

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

空中戦

なんか、緑の新人さんに刺激されたのか、連日、緑になったり青になったり...

まぁ、一応、緑の時は壊しにいきますがね。

それにしても元気だな。

Agda の演算子の構文によるエラー

中置演算子を定義できる言語はいろいろあって面白いんですが、Agda の自由度はかなり高い。

　　C [ f ≈ g ] = Category._≈_ C f g
　　infix　4 _[_≈_]

で圏Cでの等号定義できる。これを使うと複数の圏の演算を混ざるとか平気でできます。三項演算子だ。しかも二項演算子を三項に拡張してる。

この _ のところに変数が来るわけだな。 この記法は圏論でも使われてたりします。
さらに syntax というのがあるらしいが、まだ使ってません。

equality 自体も _≡_ という二項演算子で

　　data : Set } :　(x y : A) → Set　where
　　　refl　: {x : A} → x ≡ x

なんですが、これを x ≡_ みたいに使える。

　　x ≡_ = λ y → x ≡ y

(x ≡_) y が x ≡ y になるわけなので正しく curry 化されてるわけ。 なのだが、

　　_≡_ x　と _≡ x と x ≡_

と三種類書ける。どれも構文エラーにならない。 　　_≡_ x　と x ≡_ は同じ。

x ≡ y と　y ≡ x は同じなので、どれでも良いと思ったし、動いてたんですが、昨日、突然、

　　annot instantiate the metavariable _491 to solution section
　　since it contains the variable section
　　which is not in scope of the metavariable
　　when checking that the inferred type of an application

というわけわかエラーが。いやなにいってるんだかわらないんですが。でも、いろいろ削ってだめなところを抜き出したら

　　_≡ x と x ≡_ との違いだった

どっちかに統一すれば解決。なくなく 60 箇所くらい修正する羽目に。いや、Emacs の Keyboard macro でできるわけなんだが...

　　x ≡_ = λ y → x ≡ y
　　_≡ x = λ y → y ≡ x

なので、確かに違う。しかも通る場合がある。しかし、結局は通るはず。しかし、エラーは出る。なるほどわけわかりません。

いや、混ぜた自分が謎でもあるのだが...

健診

なんか延期になってたらしく。封筒が入ってたんですが、外注にだしただけらしく、

　　日付も場所も書いてない

で、ググってみたが保健センターのWebには何も書いてない。

メールを検索してみると日付は書いてあって来週らしい。しかし、

　　場所がわからない

中にあるリンクのpdfをクリックすると、巨大ファイルのダウンロードが...

そこに大学会館三階と書いてありました。

PDFのテキストだけ抜き出して表示するのを mh には組み込んであるのだが、URLのリンクを自動展開するようにしてないからな。

この

　　テキストに書くことができない障害者

たちをなんとかいて欲しいです... 罫線とか色の付いた四角とか幼稚園のお絵描きじゃないんだから、簡潔に文章で伝えて欲しいよ。

ほら、そこの学生、レポートをスクショでだすのはやめるんだ。

最近のコード検索

普通に検索すると、もうゴミばかりで... 間違ってるコードのページをコピーして大量に広告をはったページばかり。

忘れてた自分が馬鹿なんだが、サーバ側が IN_ADDRANY で待つのをすっかり忘れてて... サーバを gethostbyname で待つクソコードに引っかかってました。

https://www.example-code.com/csharp/ssl_server.asp

ここの方が少しましか。検索以前のInternetに戻ってしまったようだな...

github で動いているコードの中を検索した方がましかも。もっとも、C# で github ってのはそんなにないか。

通知

iPhone の通知はほとんど切ってるので平和なんですが、

　　シス管ミーティングをすっぽかす

という問題が。でも、入れるとかなりの量が... MatterMost の Channel 毎になんとかできるようんだが...

いちいち設定が面倒くさい。vi で設定させろって感じです。

まぁ、なんとかなるかな。

Facebook/TwitterのDMが確実か?

Calendar

iCloud のカレンダーが、まったく連携してくれなくて。まぁ、

　　あんまりスケジュール関係ない

人なんだが、割と不義理が... あと、遠隔授業な時代に推薦で休講日とか知らんし。いや学年歴のGoogle Calendar はあるんだが。

いろいろ見てみるんだが、やっぱり、Apple のが全然駄目だな。Goolge Calendar は諦めて、この前、入れたので、それから見えるらしい。

と思ったら、

　　Google Calendar から iCloud にloginできる

ぐ。それかあ。いやだから

　　最近、Goolge 嫌いなんだけど。

でも、まあ、仕方ないか。それで一応見れるみたい。でも、iPhone のCalendar はアイコン上の日付だけ便利なのでおいておこう。

ギガ

11/29まで 10GB 余ってるだったんですが、大学の帰りにポータルとろうとしたら、なんか落ちる。

　　iijmio の容量がゼロ

なんだよ。統計見るんですがresetさぼってたので良くわからない。しかし、

　　app store が 3.5 GB

とか。いや、そいつの Wifi は切ってるんだが。と思ったらばっちり on 。お前か。

この前の iOS update か、自分で何かの理由で入れたか。なんか Wifi から勝手に携帯に切り替える余計な機能とかあるらしいが。

11/30の夜だったので、12/1 になれば6GBにはなったので問題ないんだが「俺のギガを返せ〜」とは思いました。

使い切ると特に遅くなるらしく。まぁ、Twitter/MatterMost には影響ないので ingress 以外はどうってことありませんでした。

相対論関係

こんな感じ。この前にダメな本に結構引っかかってます。ブルーバックスとか、岩波新書のとか。

特殊の方は行列で不変直線ならったら「それ光速度不変じゃん」で計算するとローレンツ変換がでたのでうれしくて、なんか文章書いてたな。

そこまでわかってから他の本を読むと楽勝。

一般相対論はディラックの読み会があって、そこでだいたい。その後、復習もやった。

ただ、結局、どう計算するってところになると「作用でやれ」で、え〜な感じ。シュバルツシュルト解までだな。

結局、アインシュタインの本が良いんじゃないですかって思う。

マックスウェルの方程式を共変性が明らかな形に書き下すところからですね。

4次元運動量がエネルギーと運動量に射影されるとか感動だったな。

Rustc 読み会最終日

なんか立命館の学生も参加してくれたみたい。今日はastとcodegenで、かろうじて code 生成まで行き着いた感じです。

code 生成は Thread pool に投げてて、素直にトレースできない。で、しばらく迷走したんですが、

#0 <rustc_codegen_llvm::builder::Builder as rustc_target::abi::LayoutOf>::layout_of
() at compiler/rustc_codegen_llvm/src/builder.rs:92
#1 rustc_codegen_ssa::mir::operand::OperandRef<V>::from_const ()
at /rust/rust/compiler/rustc_codegen_ssa/src/mir/operand.rs:74
#2 0x00007fffefab11c0 in rustc_codegen_ssa::mir::constant::<impl rustc_codegen_ssa::mir::FunctionCx<Bx>>::eval_mir_constant_to_operand ()
at /rust/rust/compiler/rustc_codegen_ssa/src/mir/constant.rs:20
#3 rustc_codegen_ssa::mir::operand::<impl rustc_codegen_ssa::mir::FunctionCx<Bx>>::codegen_operand () at /rust/rust/compiler/rustc_codegen_ssa/src/mir/operand.rs:442

みたいに捕まえられました。ast -> hir -> mir -> llvm-ir みたいに生成するらしい。

40万ですが、今まで見たコンパイラのソースの方では良い感じ。特に smart pointer とかexceptionとかの処理が Rust はスムーズ。

ただ、Thread pool は微妙な感じね。Pthead だし。この辺は golang の方ができが良いかな。iterator が並列化されるみたいな方が自然で良いかも。

Rust 読み会続き

どうも、lldb だめらしく、gdb の方がまし。しかし、

　　break point が掛からない
　　p で表示できない

というつらさが... dynamic link されてるってのもあるが...

debugger は compiler が Dwarf という binary な debug 情報(関数名、コードと行番号の対応、構造体の名前と型)を使うのだが、

　　まぁ、それがでたらめ

っことね。おそらく、今の形の debugger はもうだめで、もっとコンパイラに関連した debugger を用意しないとだめだと思われる。

構造体の表示の仕方や関数のアドレスを知ってるのはコンパイラだけだから。

ただ、C++ な LLVM よりはだいぶ読みやすい。エラーが Option (エラーかどうかのフラグを含む構造体)なのは少し鬱陶しいけど。

徐々にいろいろなものがRustに移っていくかも知れないです。

結局、parse_fn_body くらいまでしかいかなかったが。

Rust compiler の trace 方法

まぁ、Haskell みたいにトレース不可能な感じではないんですが... 環境は二つ。明日、明後日で、読んでいきます。

環境は二つで

　　サーバの Singulariy 上の debug build した rustc
　　macOS上の rustc

下の方は LLVM なので gdb/lldb で。

Singulariy上の build いつもの python3 に引っかかって...

　　update-alternatives --install /usr/bin/python python /usr/bin/python3 10`

とかやらないと python が python3 にならないらしい。

Singulariyの作り方も 「--sandbox` と `--writable` を使って段階的にビルドするのがいいらしい」ことらしく...

最後にビルドした結果をsifに変換するとできるらしい。微妙。

　 singularity build --fakeroot debugging-rust-compiler.sif　rust-debug

これに

　 singularity shell /ie-ryukyu/singularity/rust-debug/debugging-rust-compiler.sif

として入って、中で trace します。sif は 5GB。VM並の大きさじゃん... 中に入ってみると 16GB。ふーん。

で、いけるかと思ったが.... break point がかからない。

　 l rustc_parse::expr::parse_expr

くらいでいけるべきなのだが。結局、

　 Singularity> nm /rust/rust/build/x86_64-unknown-linux-gnu/stage1/bin/../lib/librustc_driver-ce53599820ba664c.so | grep parse_expr

で mangling されたものに main で停めた後に

　 b _ZN11rustc_parse6parser4expr45_$LT$impl$u20$rustc_parse..parser..Parser$GT$27parse_expr_catch_underscore17h43010b29c3bbcd9bE

とすると捕まって、その後は　

　 l parse_expr

できるように。しかし、この方法は macOS ではだめでした。

source code debugger は C++ でもかなりだめでな〜　誰も debugger とか使ってないのかも知れん。

朝、10時からやるはずです。参加したい人は Facebook の DM くれれば Zoom の Link を送ります。

群論の続き

いや、プロシンのネタにしようと思って... ってことは、これから書くんですか? 8月くらいからやってるんですが...

こういうのって、やってると広がって、あれもこれもやりたいになるのだが...

　　Agda なので時間がかかる

かかる割に、システム更新とか授業とか他のもろもろとか... 事務は可能な限りさぼってるのに。

要は順列を数え上げて「全部数え上げたことを確認すれば良い」だけなんですが、割と迷走中。

でも、ある程度は形にはなったかな。Agdaの証明つまり型の整合を見るのに4分かかるのが10秒になるみたいな話らしいです。

え、そこ速度見るの?

余計なこと

授業前にうっかり「updateでreboot」をやってしまって、30minitesくらいましたが、少し遅れるくらいですみました。

Omnigaffle の update したら、

　　入力が必ず日本語に戻ってしまう

OmniGraffle どんどんくそになるな。もう学生9用ライセンスはやめてしまったんですけどね。ただ、Draw.io だって長続きするかどうか。

rust を compile するのに brew upgrade / update をかけてたら、うちでいれてる llvm のコンパイルに...

おかげでload avarageが大変なことに。年代物のMBPなのに。

Singurality でも Rust を入れてみたんですが、TZが設定されてないとかプロンプトを出されてしまうと、そこで終了。まっさからやりなおし。

buildを step by step でやる機能ぐらい欲しいけど。

量子力学の本

だいたい、こんな感じ。マンドルは学部時代に永嶋さんから借りっ放しです。すみません。

最初に吉田研の勉強会で読んだ奴が入ってないな。Poling のQuantum Chemistryも写ってないな。

面白かったのは、やっぱり Dirac かなぁ。でも、一番計算したのは Poling かも。

大学院の試験でも摂動法解いたし。フォンノイマンは微妙に相性が悪かった。一応、勉強会もしたんですけどね。

ファインマン先生のは延々スリットの問題をやるのがうっとうしかった。でも、また読み直す時が来るかも。

やっぱり計算しないとね。この辺も Agda で定式化する気になるかも。

大きな三角 ingress

元気な新人さんのせいで、割と刺激を受けたのか、古参たちが珍しく。

なかなか足がないと大きなのは難しいが、ガソリン代がかさむらしい。

そういえば、長距離リンクとかも引いてみたい気はするな。

光るグラス

だいぶ時間かかったが Lv8 に。大学で適当に CF 作って上げました。いや、木曜日にあと3時間がんばれば良かっただけなんだが。

L8使えないのは不便だった... Jarvis でお代わりが定番だとは思うんだけど、Hack数が足りなくて出ないんだよな。

こういうの好きなの人がいるらしく。これは大山のお店だな。

agda version manager

pyenv とかのたぐいですね。異なる版の共存は嫌いなんだけど、

　　agdaのbug reportには開発最新が必要で
　　授業用には brew の最新が必要

ってことなので切り替えが必要。

Haskell で書かれた agda そのものにはあんまり差はないのだが、standard-library がどんどん変わる。気持ちは分かるよ。

　　良くしようと思うと、directoryいじったり振動したりする

んだろ。取りあえず、整合性はとれたんですが、切り替え方は良くわからないです。


　　$ export AGDA_DIR=$HOME/.agda
　　Other way is to create a directory .agda in your directory and run agda-pkg from that directory. agda-pkg will prioritize the .agda directory in the current directory.

とか書いてあるが、ちゃんと動くのか?

directory毎に singulrarity / podman で固定された環境が動くとかが欲しいところ。hg/git clone で、その環境が自動的に設定されるとか。

https://pypi.org/project/agda-pkg/

シス管打ち上げ

まぁ、まだ、いろいろ残ってはいるが

　　新システムの構築終了

ということで打ち上げ。

でも、お披露目聞いてくれた人は14人? 半分シス管か?

しょうがないなぁ。授業の課題で出さないと使わないか。そんなものだよな。

いや、でも、まだ自分でも使い方良くわかってない。GCC/LLVM 使う時は Singularity 経由にするの?

https://ie.u-ryukyu.ac.jp/syskan/opening-introduction/

Recursion 2 回目

最近、緑が良く来てたからな、Lv16。まぁ、どこでも良かったんですが、泊でいいかという感じで

　　松山公園から泊まで焼いて、そこでRecurs and APEXで埋めながら戻る

ってのにしたんですが、

　　Lv5 以上は白ポ埋めでは足りなくて、CF作らないとあかん

ってのにいまさら気がついて。結局、地元の嘉数高台で多重作って Lv7 まで上げました。

明日からAP 2倍なので、そこでLv8にはなるでしょう。地元ではRecursion 4回の猛者も。

なんか最近の呼び込みって、こんなの持ってるのか。いや、入りませんでしたよ。

Rust コンパイラ読み会

例年のあれですが、今年は

　　Rust compiler

を読みます。Rust ってくらいなので、実は

　　極めて、C

な言語なんだよな。むしろ、C++ でないっていうところが重要か。

水曜日、と金曜日に環境そろえて、土日で読みます。Zoom 配信な予定。10:00-12:00 14:00-15:00 16:00-18:00 かな。

https://github.com/rust-lang/rust

Rust / InetliJ / Gitlab

というお題でした。Rust ほとんど触らないので、まったく忘れてる。

　　Reuslt を文末の ? で投げられる

というのを見つけました。assertOK ってないの?

InteliJ は Java には良いんだが、Rust はまだまだな感じ。VSCode で良いじゃん説もある。

で、(本当はhgを使いたいが) git 経由で gitlab に投げて CI するという仕組み。

gitlab 側に設定がないなと思ったら、自分でProject の下に .gitlab-ci.yml を書くだけか。

簡単でいいね。Jenkins いいけど、gitlab と二重よりは良いかな。

エラーでぼろぼろなまま、授業は終わりましたが、あとは学生が自分でやってくれるだろう。

　　# Setup a cache to cache job parts between jobs to ensure faster builds
　　cache:
　　　　key: "$CI_JOB_NAME"
　　　　untracked: true
　　　　paths:
　　　　- $HOME/.cargo/
　　　　- target/

　　# Define a yaml template for running a build and then running your tests
　　.cargo_test_template: &cargo_test
　　　script:
　　　- rustc --version && cargo --version
　　　- cargo build
　　　- cargo test --verbose

　　test:stable:
　　　image: "rustdocker/rust:stable"
　　　<<: *cargo_test

久しぶりに automaton

授業でやってるので。最初の年は List でやって「あんまり綺麗じゃない」、去年は Bool でやって「いろいろできたけど複雑」。

今年は、List Σ → Set で全部やるってのが降ってきて、確かに、わりと綺麗に。ただし、

　　簡単になったとは云いがたい

集合論の時にも Ordinal → Set でやるってのが降ってきて、いろいろ解決したわけですけどね。この

　　Set ってなんだよ

ってことだな。Agda 的には基本的な型でレベルがあるってくらいなんだが、何かの命題が入るという意味でもある。

言語、つまり、任意の入力文字のListの部分集合を List Σ → Set と書くわけですけど、その心は

　　Listの部分集合を識別する何かの述語がある

くらいだな。

　　is-a : List Σ → Set
　　is-a x = x ≡ (a ∷ [])

　　is-nil : List Σ → Set
　　is-nil x = x ≡ []

とやるわけですけどね。でも、Set は命題なので、それは証明しないと正しいとわからない。あるいは

　　is-nil? : (x : List Σ) → Dec ( x ≡ [] )

という x ≡ [] の証明があるかどうかを調べる述語を自分で実装するわけ。この場合なら

　　is-nil? [] = yes refl
　　is-nil? (_ ∷ _) = no (λ ())

とか。

だいぶ慣れたけど、いまでも、この Set 絡みは

　　まったくわかりません

となることがあります。

停電からの復帰

結局、Secondary の設定はしたんですが、上位の登録のと IP Address がずれているとのがあったらしく、

　　DNSが停まるとどうなるかという演習に

そもそも、年に数回計画停電があるってあたりが演習だけどな。復帰は順調なようですが、いくつかは立ち上がらないというもいつものこと。

この辺、全部クラウドにすれば、あんまり考えなくてすむわけだけど。

GMail も停まってたけど、復帰するとメールは遅れて届く感じ。

MatterMost は gitlab の認証で引っかかったらしく、つながりませんでした。

Slack は関係なく動くが、誰も使ってない。つまり Google アカウントはDNSに関係ない。

学科のWebも Sakura のは動いているけど、DNS がだめなので見れないわけね。

DNS

なんか、明日、計画停電らしく。いや、

　　停めないでできるでしょ

と思うんだけど。おそらく、定期点検的な役得なんだろうなぁ。

で学生がシステムの切り替え(いまだに手動)をやってるんですが、なんか嫌な予感が...

　　ちょっと DNS のセカンダリの設定見せてくれる?

と聞いたら

　　ありません

げ。Sakura の切り替えの時に、ドタバタして消えてたのは知ってたんだけど。まだ、立ち上げてなかったのか。

どうもキャッシュでなんとかなるとか Expire 延ばせばとか考えてたみたい。いまどきは、

　　Google 関係のサービスはDNSで接続している

ので、GMail が停まる可能性があるんだよな。

学科内は DB と連携させてたりで複雑なんですが、外向きは単純なので、まぁ、すぐに立ち上げられるとは思うんですが...

DNS はクラウドが良いとは聞きますけどね。

レモン麺

らぶメンがんばってるな。コロナでも閉めなかったお店の一つ。助かってます。

レモン麺、これほどはまるとは思ってなかったんだが。酸辣湯麺と似ていて酸味とラーメンって合うんだよな。

近所のわた琉も割と良い。

Marley

昔、そんな Ingres Agent がいてな〜 今頑張ってる新人みたいな。Punix とつるんで脅威でしたが...

普天間宮近くに移動してきたベトナム料理屋さん。ここは、実は

　　Ingress のポータルの要衝

といっても「自分の」だけどね。ここには花蓮もあるけど、こっち側に緩いランチができるのは素晴らしい。

なんか、隣にも怪しいオープンカフェみたいなのが。

普通に頼むとパクチー抜きになるらしいので「パクチー入れて」と頼むと良いらしいです。

緑の新人さん

なんか、けっこう頑張ってる ingress agent が... 何回かお代わりされてしまいました。

まぁ、こういう人がいないと、自分のところを染めた後、いろいろ出張にいくようなことになるので。

ただ、東海岸側はバスの便がな。那覇からいくか、護佐丸バスかになるので、なかなか厳しい。

昔の marley を思い出す感じ。

原神

一番高いところまではいきました。iPhone 7+ だとぎりぎりなので、原神のためだけに買い換え様かという気にもなるが...

このゲーム、初期の頃は墜落して良く死んでたんですが、グライディングと言って飛べる。で、

　　飛びすぎて、墜落して死ぬパターンが...

高いところまで登って、そこから飛ぶ。それが楽しいですね。テレポートあるけど、そういうの探すフェーズだからな。

遠景がかなり広く見える。そういう実装難しいんだが、もはや、それが標準技術か。しかもロード時間とかなくて。もっとも、

　　起動に時間がかかる

のは、そのまま。12とかにしてもあまり変わらないかもな。

もしかすると、一通りマップを開けて飽きて終わりかも。そういう人も多いみたい。

新町炎上

真栄原の怪しいところだったところですね。たまに写真展とかやってたらしいんですが、そこが燃えたらしく。

それでこんな看板らしいです。もっとも、わざわざ焼け跡見に行くほどでもなく。

この辺は普天間基地の緩衝帯であるべきところなので

　　立ち退きで公園にしちゃえ

って話があるらしい。花ぐるまとかサンエーがなくなると困るが、まぁ、それもいつになることやら。

JPHacks 2020

いろいろさぼっててすみません。

土曜日の午後で1分半の発表を20件くらいみたかな。この手のProject base な授業は前期でも見てて、後期もいろいろ。

なので、重複感がある。重要なのは

　　学生のグループがちゃんとサポート受けられること

なんですが、コロナの遠隔授業の影響で学生の負荷はむしろ上がっているらしく。Effort 30%とか無理的な。

テーマも心の健康とかオンライン授業対策とか「旬のものをもってきてる」感じがありました。

そこそこ頑張ってもってきてるけど、割とマンネリ化する宿命ではあるな。

人の心をいじるようなサービスは、少し、カウンセリングの経験が必要かも。そういうものをカリキュラムに入れる時代かも。

ファイナンシャルとかメンタルヘルス、あるいは労働法とか、そういう社会で生きていくためのカリキュラムかな。

まーさんパスポート浦添

なんか微妙な景品。結構、知らないお店もあるな。パルコシティできたし。しかし、今の時代にスタンプで投函ですかぁ?

　　ハリーズが入ってる

でも、判子もらうのは忘れました。

ラーメンフェスタも最初の一回は燃えたものだが...

こんなのよりも「また10万円」でしょう。

Twitter の mute と list

6400人フォローしてるんですが、油断してると

　　TLが肌色に...

エロ系を大量RTする人たちがいるんだよな。RTをいちいち停めるという手もあるんですが、

　　mute して list に入れる

すると、TLに出ないのは当然なんですが、list では見える。しかも

　　list では「RTは表示されない」

なので極めて健全な人に見えます。

ただ、この方法では

　　直接、エロ投稿している人には無力

なので、さらに別listへ。

いや、どんどん投稿してもらって構わないです。こっちで選択して読むからさ。

地図

いや、この職業、まだ生き残ってたとは。いや、ママさん、そこお金だすからでしょ。まぁ、助け合い的なところもあるんだろうな。

安いとも思いましたが、この地図が役に立つことはないよな。

昔の Google Earth は Google Map 以上にマイナーなお店が出て、かなり驚いたものだが... 今は、

　　どうでも良い店しか出てこない

検索エンジンで何かを発見する時代は終わってしまった感じ。深層学習とかで最適化された結果ってのは

　　90%の人には役に立つかも知れないが、0.1%を探している人には何のやくにもたたない

ってことね。

file を持ってくるスクリプト

こんな感じなんですけどね。rsync は --files-from=FILE ってのがあるので、もっと綺麗に書けるはずですが、
まぁ、動いているから良いか。バックスラッシュの数が笑える。.svn とかCVSとかが時代だな。

Dropbox は嫌いなので使ってません。source doe は hg/gitなので、こういうのは使わない。

このscriptは、もっぱら家と学校とノートPCでファイルを移動する時に使う。事務系のファイルが多いな。

事務は MS Team を使う羽目になってるはずだが、紙で抵抗しているようなのがいるという噂。

もっとも、MS Teamなんか使われると、こっちが迷惑説もあるかな。

量が少ないなら Home directory を rsync ですますんだが、まぁ、そうもいかず。

file event とって自動的に同期とかも面白そうではあるが...

#!/bin/zsh
host=insigna
test=
flag="-zavE"
for file in $*; do
　　case $file in
　　/*)
　　　　dest="$file:h"
　　　　file=`echo $file| sed -e 's/ /\\\\\\\\\\\\ /'`
　　　　dest=`echo $dest| sed -e 's/ /\\\\\\\\ /'`
　　　　( cd / ; $test rsync $flag --progress "$host":"$file" "$dest" --exclude .svn --exclude　CVS --exclude .cvs ) ;;
　　*)
　　　　here=`pwd`
　　　　dest="$here"/"$file"
　　　　dest="$dest:h"
　　　　file=`echo $file| sed -e 's/ /\\\\\\\\\\\\ /'`
　　　　dest=`echo $dest| sed -e 's/ /\\\\\\\\ /'`
　　　　$test rsync $flag --progress "$host":"$file" "$dest" --exclude .svn --exclude CVS　--exclude .cvs ;;
　　esac
done

無限列車

乗ってきました。まぁ、

　　ジャンプだからさ

という感じ。この系列、アストロ球団からの流れか? いや、聖闘士星矢か。

でも、終わったら「お父さん、もう一度みたい」って小さい女の子の声が。

面白かったかと言われると、テレビアニメの方が良かったかな。映画自体のできは微妙。とかいうと

　　あやまれ、煉獄さんにあやまれ!

と某女史に言われそう。

知ってることとできることの差

量子力学学んだのは、やっぱり吉田研での勉強会からだったけど、三日くらいで片付けていたはず。

でも、それは読んだだけ。その後、量子化学の授業で摂動法をやって、さらに院試の勉強で問題を解く。

それでやっと計算できるようになった。単に知っているだけではだめで

　　手を動かさないと

そのためにいろいろ課題を出すわけだけど、学生はいろいろ手を抜くわけだな。手を抜いても

　　結局は、大学院で必要なものをやり直す羽目になる

つまり

　　そこそこの厚みの(だいたい英語の)教科書の問題を全部やることになる

それにいつ気づくのかは人によって違うけど、学部で卒業してしまうと気がつかないままってのある。

先輩とか先生とかと一緒にやっても良いのだが、それは助走みたいなものだな。

Apple TVは一度に一つのネットしか接続できない

まぁ、こいつは1教室で60人に画面配信みたいなのには向かないわけですが、それでもHDMI/DVIでの接続よりはましなので大教室用に。

で、設置してわかったんですが

　　ネットワークは一つ

有線ポートあるくせに有線で設定すると無線の設定が出なくて、無線を設定すると有線でつながらない。

全部同時につなげられることを知らないわけはないので

　　わざといじわるでそうしている

らしい。まぁ、無線側も guest 用とenterprise用の両方に接続して欲しいわけですが、せめて切り替えと思うわけですが...

　　有線から無線の切り替えは有線を抜かないとダメ

らしい。なんだそれ。Air Port の開発者を切るような頭の悪いことするからだろ。

Aerohive のLDAP認証がちょっと微妙でWindowsからはつながらない的なのを出しているのでguest用のを使っている人が結構いるらしく...

もっとも、大教室の稼働状況はかなり低いので特に問題はないんですけどね。

Podman / Pytorch

まぁ、使いたいって人はいるけど、

　　自分で環境設定する能力はない

まぁ、やらないってだけなんだろうけど。シス管と一緒にやると面白いと思うんだけど。まぁ、卒業した後は

　　クラウド環境しか使わない

ってのはありそうな話ですが。だからこそ、今しか触れないと思うんだけどな。

もっとも、asible で server に Cuda を入れて、podmain で起動するだけ。

ansible も pdoman の Dockerfile も拾ってくるだけですが。

FROM docker.io/pytorch/pytorch:latest
WORKDIR /pytorch
RUN apt-get update && apt-get install -y git && git clone https://github.com/pytorch/examples.git
WORKDIR /app
CMD ["./entrypoint.sh"]

これだけ? これだけでも、できないって言う人いるよね。でも、それは割と嘘で、細かい試行錯誤がいろいろあるんだよな。その辺はシス管のKnowHow。

なんですが、

　　Ceph 上で podmain build すると 4分
　　SSD 上だと 3秒

という問題が。計算が始まれば問題ないんだけど。あと、rootless だとユーザ間ではファイルが共有されない。

うーむ。そうすると、投入されたtaskを固定ユーザで実行する感じが良いのかな。ほんとメインフレームかお前は。

まぁ、環境制御はいろいろ方法があるのでコンテナでなくても良いのだが。

Docker よりも Podman が遅いってだけでなく、Cephが細かいファイルを処理するのが遅いんでしょう。まぁ、なんか方法あるかも。

　　BRD FS使うとか、Fuse 使うとか

いろいろ楽しめそうです。

クレジットカードの認証

なんか Mou で夕ご飯だったんですがカードで払おうとしたら

　　「かざせば暗証番号は要りません」

はい? そういうものなの? まぁ、カードの裏の三桁とかもそんなものなので、そんなものかなとも思うわけですが。

暗証番号なしってのは小額だと結構普通かも。

一方で iPhone は指紋認証します的な。まぁ、指紋だって別にすごく安全というか、本人の意志が確実にわかると言うわけでもなく。

セキュリティというのは、0.何パーセントかを無視すると利便性はぐっと上がるんだよなと思いました。

保険とかと組み合せてそういうものが良いかな。

ドラム缶

いまどき、こんなもの使うと近所から警察に通報されるかも。

昔は、工場の終業時にはだいたいなんか燃やしてた気がする。

OSの授業

新しいシステムになってからの三回目の授業なわけですが、

　　今まで動いていたものが全然動かない。動かないです。

docker やめて podman とか、ie-virsh というwarpperやめて、sudo virt-install とかなんだが、書かないといけないことがいっぱい。

自業自得とはいえ...

ただ、discord のサポートがあるので、例年よりはスムーズならしい。だったら去年から使えばよかったな。いや、去年も slack はあったんだが。

discord は学生はゲームで慣れてるからかな?

てだこ浦添駅の工事

なんか、穴は貫通したらしい。ゆいレールと高速バスの乗り換えに良く使うので工事が邪魔。

工事のあと、どうなるのかは良くわからないです。あんまり期待できないな。

那覇よりにインターができるらしいので、もしかするとバスが降りるのか? それだと時間のロスがな。

まぁ、インターができるのはだいぶ先なので、それまでは今のバス停のままかな。ということはしばらくは

　　今のまま、高速バスの乗り換えには山越えが必要

ってことになるのかな。

パルコシティ向けバス

61番にのったらパルコシティ向けとおっしゃる。いったいいつから?

　　ちなみに一日6往復

でも、中北部から行く方法が存在しなかったのに比べれば無限大に良いわけで...

安谷屋、中部商業経由なので、自分には便利。

43のもか。でも、北谷と那覇バスターミナル間で経路が全然違うのに同じ番号はだめだろ...

あ、でも、43は一日一本?! 使えなさすぎる。

いや、まったく知りませんでした。

Ingress Kinetic Capsule

なんか、8km あるくと Ultra Link が合成できるってものなんですが

　　素材が Link amp 3 つ

まぁ、要らない時はどんどん貯まって捨ててるLink ampなんだが、

　　必要な時にはない

この前、「Link amp bundleとか売って誰が買うんだよ」と言ってましたが、

　　Link amp bundle はもう売ってない

その代わり、余計な物が入って高いものを売ってる。商売上手だな。買わないけど。

いや、買って応援しないと危ないかな。

自分のペースだと週三つくらいは(素材があれば)できる感じだけど、

　　最初に合成した一つは間違って差して終了

合成したものが最初に選択されるって技があるのか...

HPVDI 2020

OIST に行ってきました。まぁ、Online でも良かったんですが。実は水曜日からだったんだけどさぼって金曜日だけ。

なんだかんだ毎年発表してるわけですが「ネタがないんだよ」。いや、ネタ切れからが本番だから。

今回は Ceph でシステム構築したので、その話をしてきました。

オンラインの人が多くて会場はスカスカ。こういう方がいいかな。Zoom は機器に接続すれば勝手にやってくれる方式。

オンラインからの質問も割と聞き取りやすかったです。Slack 併用。

なのだが

　　OISTのカフェ/コンビニが使えない

飯が食えないので車で載せてもらって恩納そば。なつかし。割と味が落ちたイメージがあったんだけど、割と良かった。

ジューシーをラップで包んで、おやつにしました。

https://www.highperformancevdi.com/ja/meetings/2020/index.html

Axiom 公理

これって複数形どうするってな問題があって。

　　data と datum

なので、data は複数形なんだが、既に datas は良く見る...

axiom もそういう系列らしくて、axioma, axiomata となる可能性もあったらしい。

https://twitter.com/na4zagin3/status/1319108047009009665?s=20

Letter Head

あの透かしの入った便箋と封筒なわけですが... 確か、10年前には琉大にもあったはずなんだが...

　　総務と学務に聞いてもないと

まぁ、そういう権威がどうのってよりは一種の証明書的な扱いだったはずなんだけど。

なんか、どうも「ここにPDFあるから、それ使え」ってことらしい。

自分が修士の時には、それで海外の先生に手紙だしまくってアポとったものだが。

名前が○○とかあって、結局、いろいろ細工する羽目になるので、とっても捏造している気分。

無駄な文化だったような気もするが、まだ残ってる大学もあるみたい。

筋トレ

なんかコロナ太り気味なのでなんかしようかなと。60kg 目標ぐらいなのだが、65kg 現状。でも、1-3月は63kgくらいだった。そういえば

　　そのあたり割と体調悪かったような

昔の記録を見てみると、Ingress やりまくってた頃が60kgくらいで、その後は64kgが普通だったらしい。

腕立て伏せと腹筋くらいなんですが、腹筋を三種類くらいにしたら

　　2 sets やると気持ち悪くなる

なんか、そういうのあるらしい。まぁ、あんまり無理しない方向で。

お腹の運動

原神

いや、別に暇ってわけでもないんですが... iPhone のゲームにしてはそこそこでかい。が

　　縦で起動すると落ちる
　　横で起動すると真っ白な画面

で、だめかなと思ったんですが、

　　白画面で数分放置したら down load に入った。4GB

で、まぁ、始まったんですが「英語」。iOS英語モードにしてるからな。まぁ、問題はないんですが...

　　ムービーがぼろぼろ

くそ、iPhone 7+ で無理なのか。でもフィールドだとそこそこ動く。ただ、あっちっちになるけど。やっぱりだめかな。

オープンワールドなのでなにして良いかわからん。泳いで溺れたりとか、なんか使えとかメッセージが出てる敵にやられるとか

　　落ちて死ぬとか

で死にまくり。HP回復アイテムの集め方がわからんな。

黒の砂漠はゲームの方がぬるくて事務作業になってしまうのでやめてしまったので、これくらいの難易度の方が良いかも。

しかし、この重さだとやめちゃうかも。再接続に1分くらいかかる。

https://genshin.mihoyo.com

靴のかかと

なんか修理してもらいました。減ると、足ひねりやすくなるし、

　　石が入ってぴこぴこサンダル化する

って問題があるんだよな。

今日は、港川から伊祖に抜けるコースだったけど、おわりごろに ingress のサーバが不調に。

昔は浦添も青のエージェント何人かいたんですけどね。最近は好き勝手にやられてるな。

サムズアンカーインのお弁当

どこもいろいろ大変だよな。にんにくが利いてるスーパーウェルダンでした。

これをもって、森川公園のポータルを落として、そこでお昼。もっとも日曜日の話ですが。

ご飯半分残し。

大勝軒にしようかと思ったんだけど、結構、混んでたのでパス。

戻ってきた頃には森川公園は取り返されてました。

アカウント拒否な一日

なんか、久しぶりに Windows 10 を上げたら、ばちがあたったのか

　　アカウントが変

とか言われる。取りあえず、ie なアカウントで通ったんだが、大学のアカウントは cs なはずなので、365が通らない。別にそれは良いのだが(良くない)

　　どうも、cs のアカウントはないっぽい

パスワードが違うとかそういうレベルじゃないってことね。前にも母が倒れた時に書類出せなくてアカウント消された時があったっけ。なので問合せ中。

大学のLDAPアカウントは別なので問題ないです。そういえば、cs なアカウントってメール一度とも読んだことないな。あんまり良くないよね。

GMail ではないので統合はできないです。

もう一つは、github と Visual studio の連携。Plugin 入れるまでは良くて、github のloginまで順調なんだが、

　　Vistual studio を authorize できない
　　緑の authorize button が有効にならない

くそ〜 VirtualBox の中からだからかな。redirect 先が localhost なせいかも。少しネットワーク設定いじってみたが良くわからん。

神の塔

アニメです。女の子を追いかけて、選抜試験が待つ神の塔に登る的な話なんですが...

　　試練が理不尽すぎる

管理している人たちが酷いわけ。諦めることはできるっぽいので、そんなのさっさと諦めろと思うわけですけどね。

しかも、突破できるのは「生まれつきの資質」だけに寄るっぽい。そして、

　　女の子の性格が悪い

まぁ、世の中の男子よ、世の中はそういうものなので諦めてください。というような話らしいです。

自分が出してる課題も、そんな風に思われているかも...

続きは見ないかも。

Rust

C の代わりに良さそうなので。でも、OSの講義で使うに

　　C / Java

も適度に古くさくって良い気もする。自分で新しいもの探せるし。

去年は golang 使ったんですが、自分がなんかはまらなかった。

InteliJ でやってみるんですが動かない。

　　rustup

ってのがいるらしい。これで Cargo.toml があればいけるようです。

VSCode 側はまだわからん。「couldn't start Rust language server」ですか?

今年はだいぶ変わるわけなんだが、補講でも落としているのが何人か。いや

　　OSの授業好きすぎて何回も受けたい

のはわかるんだが... そこそこ大変な作業だとは思うけど。Rust の環境設定で苦労しているのとかの連続だからな。

マクドのモバイルオーダー

なんかテーブルに数字が... ってことはアプリから注文すると、ここに持ってきてくれるってこと?

これだとカウンターに並ぶ必要ないのか。でも、オーダー確認しないのね。なんとなく

　　テーブルのどっかが光る

的な工夫はあっても良かったかも。受け取り時にアプリ提示とかもなくて。でも、

　　注文聞きに来て、品物が来てから伝票が来る

的なプロトコルだったんだから、それでも良いんじゃないのって気もする。

結構便利。

でも、この辺の社会的プロトコルは紆余曲折ありそうな予感。

コヒーだけじゃなくてアイスティーもお代わりありにして欲しいかな。

MacはビックMac派です。

Re:ゼロ 2期

　　中途半端に続く

でした。

以下はねたばれ気味に。

ソシャゲの方も少しやって「これだったら見直した方が早い」と思ったんですが、

　　予想以上に覚えてない

これって主人公の覚えゲーなんだよな? まぁ、セーブ細かいとは言え...

エキドナの話しか出てこない気もするし、その伏線も先送りなんですかとも思うわけなんだけど、

　　人でないものたち

がたくさん出てくる。特に魔女か。人から人でないものに変わる過程を書くつもりなら面白いかも。

マドカマギカもそいういう話だったな。

既に主人公は人ではないわけなんだけど、まだ自覚してないのか? 周りを見ろ。というわけなので、

エキドナの契約を断った理由がさっぱりわからないです。まぁ、契約したら最後

　　選択肢を全探索させられる

ことは確かだとは思う。でも、結局は、そうするなら知識を持つものと一緒に探索するべきだと思うんだが...

まぁ、でも、この設定だから結局は契約するのかな。

お気に入りの場所

着替えとタオルが猫毛になってしまうので、カバーをかけてます。

そろそろ、お腹に乗ってくる季節だな。

再起動試験

だいぶ新システムもできてきたので。前回は

　　Cephを吹っ飛ばした

って実績が既にあるのでね。今回は iDRAC つまり IMPI 経由で全部のサーバとスイッチを落として上げるテストでず。

ついでに iDRAC / BIOSの version up もしました。で順調に上がったんですが。

　　二ヶ所に cephfs が mount できない

error=13 = permission denied ふーん。なんですが、

　　/var/log/syslog に親切な error message が

mount の commad miss で一件落着。他にも VM が上がらないとかそんなの。まぁ、いろいろでるよね。

とりあえず、試験成功おめでとうございます。まだ、GPU の設定その他があるけど、山は越えた感じかな。

千円

なんか、これも GOTO 関係なのか。使えるところが限られてるらしく。

　　豊見城だと水族館くらいしか使えない

まぁ、わかりやすいと言えばそうかも。

ホテルのは裏から水族館はいい感じの散歩道でした。三線弾いてる人とかいました。

かりゆし水族館

先週の土曜日の話だけど、アシビナーのそばに泊まったので、朝、水族館に寄ってきました。

　　空いてる水族館って良いよね

ここは

　　クラゲが売りだってのを発見しました

2400円なので高めだが、なんか、地域振興券みたいなのをホテルでくれたので千円引き。

Ingress Battle Beacon

Ubuntu は20ではなく16を使ったら簡単に上がりました。driver が足りないんだな。旧サーバはLDAPとCephをansibleで設定すれば終わり。

　　が、なんかやる気が出ないな

それとは関係なく金曜日の夜に Ingress の Battle Beacon お試し会に行ってきました。瀬長島夜11時。

　　帰れないだろうが〜

時間が emrin とか言われてた。まぁ、来る人に送ってもらえば良いんですが、長時間往復はな。というわけで道の駅のそばのホテルに泊まりました。

1分ぐらいの反転を繰り返しながら一つのポータルを取り合う感じ。複数のポータルを点灯させても良いので、複数もOk。

まぁ、なにやってもよいですが...

　　攻撃、レゾ差し、MOD

そばのポータルに低レゾさしてAP稼ぎもありだな。結構長く感じる。バスターあんまり持ってかなかったんですが、1つに百くらいあった方が良いかな。

最後に花火でご褒美ポータルに変わるので、8人いた方が良いですね。でも、今のIngressだと青緑8人ずつは少しきついか? FSとからめれば。

自分的には ingress はお遍路みたいなものなので、一人廻るもの的なところがあるかな。戦い苦手だし。緑はがちで勝ちに来るしな。

PowerEdge firemware update 解決

UEFI から実行する bios update ってのもあったんですが、実行すると

　　BIOSのfirmwは上がるが、Lifecycle controller は消える

で、そこから先は行き止まりだそうです。結局、

　　Lifecycle controller が古すぎて ftp とか言ってるのだがだめ

らしい。そこで Fedora あげるかみたいなことやってたんですが、Bootable USB からでは上がらない。あっそ。

そこで、めんどくさくなってきたので

　　動いてる Centos 7 と disk 3 台を入れ替える

という暴挙に。RAIDのconfigを読み込めば一応上がる。そこから ./suu -u で上げました。できました。ちゃんちゃん。

で、HTML5 の virtual media で Ubuntu を入れるのですが、どうも UEFI でも BIOS でも立ち上がった後の HTML5 の virtual media を認識しないようだな。

おそらくは Fedora 32が上がらない理由と同じだな。

というわけで、3日間苦労したけど、virtual media からは起動できないってことで終わりみたいです。メディア焼いてみるか?

学生は入れてたのでなんか方法があるんでしょう。

Firmware version up 続き

やっぱり、Lifecycle Manager が古すぎるらしく、ftp とかいってるのでダメらしい。iDRACからのも上がらないのは同じ理由っぽいです。

なのだが、SUU の方が bash suu -u で動作するのがわかったので、なんとか上げられました。一度、Lifecycle Manager があがれば、そこから上げられます。

これで、HMTL5 で動くように。

　　2台は

一台は Ubuntu なので suu が途中でこける。suu も Java だが、/dev が違うんだろうな。なので、

　　OSを一旦、Live CDなどで変えてなんとかするしかない

らしいです。Centos 7 入れ直しか。まぁ、それも良い。やっぱり PXE 用意しようかな。あと、

　　もう BIOS にするのはやめて。UEFI でお願いします。

UEFI から bios update もできるらしいが、iDRAC はできないみたい。Lifecycle Manager はどっちなんだろう?

Dell PowerEdge firm update 続き

まだ完了してないです。おいおい。問題は、

　　iDRAC8 から Java の仮想コンソールを開けない

おそらくは Javaのversion checkが走ってる。Java 自体は動いてるから。Sakuraの jlnp をコピったりしたんですがだめ。

なので、仮想メディアを接続できない。それができないとOSのinstallを含むほとんどのメンテが遠隔でできない。もちろん、

　　firmware version up もできない

で、いろいろ調べるわけですが、bootable media があって、それを USB Memory に入れるってのがる。あの

　　FAT32 に MBR (Master Book Record )書く

ってやつですよ。DiskUtitilty でできる。なのだが、それで立ち上がるのは Linux なんだが sdほげないとか文句いってくる。ぐぐると

　　それは仮想メディアでないからだ

てーめー、それじゃ意味ないし! その仮想メディアがでないから苦労してるんだろ。IPMI tool からできたりしないのかな。

それで Windows / Linux からやる SUU というのがあるらしい。Linux だと X11 だな。いやな予感がしたんですが、

　　画面は出て認識までするんだが、ボタンが押せない

キーボードショートカットを打つと、起動した xterm 上に出る。おーいー。CUI あるにはあるんだが、やり方が不明。

じゃぁ、ってんで、サーバ機にX11 server入れたんですが「glamor がSEGV」くそ、どこまでも....

というわけで敗れさり中です。Live CDか、あるいは、SUUのCUIか、あるいは Windows 経由か。

古いサーバ

Centos7 から Ubuntu に変えるだけの楽勝な仕事なわけですが...

iDRAC 経由で上げるよね?

で、IMPI の接続から確認するわけですが、iDRAC のアドレスを設定すると...

　「え? 直につながるの?」

ま、良いか。そのうちにまずいものは分離するがいまのうちは。

ところが、仮想コンソールが上がらない。Sakura のは一発で上がったのに。もしかして、Firm が古いから?

で上げるのだが、全然上がらん。ぐぐったら、

　古い奴から一つ一つ上げていけ

え? 2015年から放っておいた奴を? 本気ですか? うーん、やっぱり

　PXE で上げる?

その方が iDRAC と格闘するよりはましかな?

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が張れる。

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

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

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

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