QNAP 続き

結局、QNAP の安いのを買い足してしまったんですが.. ベイが壊れてるんじゃ意味ないし。設定していく時に判明したのは

　　2016 に買った 2台WD 6 TB は、両方とも壊れていた

じゃぁ、ベイは生きてるのかと思ったけど、そんなことはなく。まったく同じ音で壊れていたのでタイマーでも入ってるんでしょう。

qnap 用の binary package は、また場所が変わっていて、ちょっと苦労しました。つうか、nohup も disown も default でないってどういうこと?

まぁ、rsync 打たずに バックアップコマンドでやれってことなんだろうけど。

裸族とかラズパイのとか単なるUSBな箱とかいろいろ見ましたが、どれもいまいちかな。

台風は、まぁ、たいしたことないっぽいです。

豊島園

池袋生まれですからね。子供の頃は良く連れていってもらったようです。父の8mm フィルムとかあるな。

　　近所で手軽なハレの日

だったな。

でも、あの頃はかなり混んでましたよ。

最近は、

　　エルドラド

だったかな。レトロで豪華でゆっくりで。空いてるからずーっと乗ってられる。一緒に乗ってくれる女の子がいればな。　

カルーセルとか言うんだよね。

3時から6時までは無料だったので、ingress にはうれしかったです。

最近は、IMAXで寄るくらいでしたが。

Disk server + Ceph

続きです。

　　ansible で Ubuntu に curl で ceph-adm を入れる。

　　ceph-adm で Ceph を設定

これで Web UI が使えるように

　　ceph に全部のディスクを登録

で、osd で作るんだけど、大きさどうすれば良いのか検索不可能。最近のWeb検索の無能さは半端ない。

　　10TBの osd 作ったら全然終わらない

100GBは瞬時。どうも、HDDの大きさを越えて作ってはいけないらしい。一つのHDDに複数のosdもだめらしい。

ってことは、HDD一つに付き、対応する大きさの osd を作る感じか。最初からそう書いて。

で、その上に Linux のファイルシステムを作るのだが

　　ceph fs
　　ceph fuse
　　rbd

の三種類があるらしい。取りあえず、ceph fs　が激遅ってのはわかりました。まぁ、そうだよな。

いろいろ使いどころが難しそう。

重複排除しようと思うと、RADOSGW 使えとか書いてある。やるかどうかは謎です。

　　/mnt/cephfs# time rsync -a /usr/ test2

　　real　　1m50.538s
　　user　　0m17.315s
　　sys　　0m11.973s

　　/mnt/ie-rbd# time rsync -a /usr/ test

　　real　　0m8.452s
　　user　　0m9.135s
　　sys　　0m5.025s

「ディスクサーバにOS入れて」「え、ディスクサーバってOSいるんですか?」

いや、Pure Storage とか NetAPP とかQNAPとかと違うので...

PowerEdge R740、しばらく楽しめそうです。ハードウェアRAIDなしで使おうと思ってるんだけど、

　　RAID0 でも Virtual Disk を組まないと Ubuntu から認識しない

ってなわざが。いや、あんまりやらない構成か。でも、同じ筐体内で冗長化してもあんまり意味ないような。

でも、システムは筐体内で冗長化した方が良いか。

RAID 壊すの得意な人です。今までに殺したコントローラは数知れず。もっとも、データ失うところまではいってないのだが。

そういえば、QNAPも飛んでたしな。

数学の学び方

5次の対称群が分解群にならない、つまり交換子 [ h , g ] が単位元 e にならないってのは、Altin には

　　 [ aec , abc ] = abc

だからって簡単に書いてある。[ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h なので、それは計算すればわかる。

abc は「aをbに、bをcに、cをaに」という巡回置換。でも、こんな風に書いてあるだけましで、岩波の現代数学とか

　　練習問題

だから... 学部の時には阿部英一先生の代数学を使ってたらしいです。万年筆で赤がたくさん。

でも、余白で計算しているようではだめだな。甘い。甘すぎる。やっぱり、

　　自分独自のノートに自分独自の構成

をしないと。Agda はそういうツールには最適なようです。全部、証明しなくて、

　　命題を Agda で書くことによって、教科書のいい加減な構文とか型とか

を、ちゃんと理解できる。数式の構文解析がちゃんとできてなくてわからないってことは多いよ。

団子

バスの団子はなぁ。大謝名の坂を登るのは本数は結構あるんですが、三ついっぺんに来る割に、終バスが遅いのでがっかりですよ。

1時間に一本でもいいから登り下り12時まで運行して欲しいが。

今は、一番遅いのはゆいレールかも知れん。

ゆいレールは、まだ、終電は試してません。てだこ浦添は割と途方にくれる感じだからな。

まぁ、あと40分歩けば良いのだが、途中で何かに捕まってしまう可能性が高い...

Agda version up on macOS

バグレポのために開発版使ってたりするんですが... このところ上げるのさぼってて。

一般人は、brew install agda で十分です。

　　　　https://github.com/UlfNorell/agda-prelude.git
　　　　https://github.com/agda/agda-stdlib.git
　　　　https://github.com/agda/agda.git

このあたりから取ってきます。Haskell 必須なので

　　　　brew upgrade ghc
　　　　brew install make

macOS の make は gmake だが古すぎる。

agda に移動して、 なんか cabal に変更があったらしく

　　　　cabal user-config update

これで install diretory を指定する必要があるらしい。 さらに、

　　　　 cabal install text-icu --extra-lib-dirs=/usr/local/opt/icu4c/lib --extra-include-dirs=/usr/local/opt/icu4c/include\n

が必要。おそらくは何かの指定漏れ。

　　　　 cabal clean && cabal build && cabal install --overwrite-policy=always

とかする必要がある。

　　　　 gmake install CABAL_OPTS='--extra-lib-dirs=/usr/local/opt/icu4c/lib --extra-include-dirs=/usr/local/opt/icu4c/include'

でできますが、MBP で50分。さらに、

　　　　gmake test

これをしないと fix-whitespace が入らない。しかも、それを

　　　　path=($HOME/.cabal/bin　$path)

と path に入れる必要があります。でないと、stdlib の gmake でこける。

　　　　cd ../agda-stdlib ; gmake

でできたがりですが、std-lib の gmake は要らないかも。あとは、.emacs.d/init.el とかを修正して終わり。

　　　　Relation.Binary.Definitions

の追加とか、

　　　　fromℕ≤ was deprecated in v1.2.　Please use fromℕ<

とか。特に、どこが良くなかったとかわからんな。

なんか、git pull で勝手に merge に入るのやめて欲しいです。

ガロア理論

中学生の時にガロアの夢とか読まされたが、あやうく数学嫌いになるところだったような。アルティンの方が良いが、今は数学ガールがあるから。

順列やってたのは、このためなんだけど。割と話は簡単で、

xの多項式は

　 (x - α)(x - β)(x - γ)

の形だとαβγを置換しても同じ式になります。

なので多項式には順列の群である対称群が対応することになります。

　 f x => (x - α)(g x)

の変換は、f xの対称群からg xの対称群への変換になるわけ。具体的には三次の対称群から二次の対称群だな。

三次の対称群、つまり三つの数の入れ替えは、αβγはγ..と.γ.と..γからなるわけですが、

三次式を二次式に変換できるなら、αβγとβαγの二つの形にならないとおかしい。つまり、

　αγβ = αβγ

とγを移動できる必要がある。ということは、

　γβ=βγ

でないとダメ。逆元をかけて

　 β⁻¹ γ⁻¹ βγ= e

になれば良い。左辺が交換子というのだけど、これを繰り返し作って e になれば解ける。5次だと解けないってわけ。

すったもんだしたんですが、2次まではできた。でも、これ、ちょっと順列でやるにはきついな。

lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
lemma4 g h = begin
　　　 [ h , g ]　　　　　　　　　　　　　　　 ≈⟨ grefl ⟩
　　　 (h ⁻¹ ∙ g ⁻¹ ∙　 h ) ∙ g　　　　　　　　≈⟨ assoc _ _ _ ⟩
　　　 h ⁻¹ ∙ g ⁻¹ ∙　(h ∙ g)　　　　　　　　　≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6))　⟩
　　　 h ⁻¹ ∙　g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹)　≈⟨　∙-cong grefl (lemma5 _ _ )　⟩
　　　 h ⁻¹ ∙　g ⁻¹ ∙　(g ⁻¹ ∙ h ⁻¹) ⁻¹　　　　≈⟨ assoc _ _ _ ⟩
　　　 h ⁻¹ ∙ (g ⁻¹ ∙　(g ⁻¹ ∙ h ⁻¹) ⁻¹)　　　 ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
　　　 h ⁻¹ ∙ (g ⁻¹ ∙　 h ⁻¹ ∙ g) ⁻¹　　　　　 ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
　　　 (g ⁻¹ ∙ h ⁻¹ ∙　 g ∙ h) ⁻¹　　　　　　　≈⟨ grefl ⟩
　　　 [ g , h ]　⁻¹　　　　　　　　　
　　 ∎ where open EqReasoning (Algebra.Group.setoid G)

ってな感じ。

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

Portal Ghost

なんか、たまに出る。Scanner のバグなのか、わざとだしてるのか。

邪魔だった、キャンプフォスターのリンクは消してもらいました。が、

　　今日は一日、Agda で Permuation いじってた

そろそろ Agda は封印だな。

変える気のない人たちと、変わらされてしまう人たち

嘉数中学も、なんか既に学生がたくさん。大学事務は、マスクとかフェンスとかで、まったく同じ。店舗も

　　検温すれば、いつも通りで良い

ということになったらしく。まったく変える気ない感じ。

でも、大学はな、天羽も書いてたが、

　　20代を大量に授業でシャッフル

となると結果は見えてるわけで、実際、やらかしている大学も。うちは、

　　IT系で、学生は MBP を入学時から持ってる

状況なので、特に問題なく遠隔授業環境に突入。先生方も、特に文句ないらしく。いや、玉城先生には負荷だったかも。

彼らは、もうしようしもなく変わらされてしまう。寂しいとか言ってる人もいるけど、もう

　　慣れるしかない

そう、

　　ネットだけで友人を作っていくしかない

僕のようにな。Facebook の友人でも実際に会ったことがない人の方が多いです。ソニーでも社内IRCが楽しくて、

　　会ってないのに、既に、知り合い

みたいな感じだった。

　　こちらの世界へ、ようこそ。

Permutation

ここ二三日、順列と格闘してました。Agda の定義は Bijection がどうとかで高尚でなぁ。

やりたいのは数え上げなので

　　 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
　　 1 ∷ 0 ∷ 2 ∷ 3 ∷ []
　　 1 ∷ 2 ∷ 0 ∷ 3 ∷ []
　　 1 ∷ 2 ∷ 3 ∷ 0 ∷ []

ってな置換パターンを生成して、再帰的に組み合せてやればよい。

いきなり作ると Data.Fin とか Bijection で死んでしまうので、

refl : ∀ {xs} → xs ↭ xs
prep : ∀ {xs ys} x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
swap : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
trans : ∀ {xs ys zs} → xs ↭ ys → ys ↭ zs → xs ↭ zs

で inductive に作ってやると良いらしい。prep と swap は直接書けたので。ところが、

　Agda のプログラムの引数がまったく合わない

誰だよ、関数型言語はバグがないとか言ったのは... まぁ、できてしまえば、どうってことない。

これで、順列の交換子を数え上げれば終わりなはずです。

スーツ

珍しく新調したんですが、

　　足が少しきつい。膝っ小僧の辺り

ウエストは問題ないんだが... これで Ingress 歩きまくると、結構、ズボンをやっちゃうような気がする...

論理的に考えること

学部生が論理的な考え方や話し方ができてないから中高で教えるべきだ的な話をみかけたんですが... それって

　　どんな論理を想定してるの?

高校時代に島内先生の数学の基礎に引っかかって、

　　A → B は A が偽ならば真

にまったく納得できなかったことを思い出すな。前原先生の「Don't move or I'll kill you」と「If you move, I'll kill you」を読んで割と納得。

前原先生の授業はNatural deductionだったし、層圏トポスも読んでたし、様相論理の本も吉田先生からがめていたので論理にはなれていたはずだが...

でも、Prolog 学んで Foundation of Logic Programming でモデルの考え方を知った時には

　　記号論理の意味がぐっと具体的な感じがした

かな。もっとも、それが数学の本を読む時のとはあまり一致してなくて。むしろ、

　　現実の世界はモデルであって、記号論理は、その上での構文

という科学的なイメージに近い。

数学の論理はやっぱり証明なので、直観主義論理的な Natural Deductionに合う感じ。

もっとも、→ の意味は記号論的なもの以外にもいろいろあって、因果関係とか予測とか様相とか。

科学者や数学者はもちろん厳密な直観主義論理を使うだろうけど、それと論理的な話し方とは差があるだろうな。結局は、

　　論理的に考えて話す人と、どれだけ話すかによる

気がする。「できてないから教える」というのは学校に期待しすぎ。社会自体が論理的にならないと、学生は論理的に話すようにはならないと思う。

プチッと

楽しく、zoom のゼミやってったら、

　　いきなり画面が暗転

あれ? 一階上の研究室には学生が三人。そっちに移動して。「声聞こえてる?」「小さいけど、聞こえてます」

終わって、USB C cable をたどってみたら、さきっぽんは何もつながってない lightning だった...

ありがちだな。気をつけよう...

逆方向のリスト

普通はリストは、

　　・ → ・ → ・ → ・ → []
　　↓　　↓　　↓　　↓

見たいに作るわけなんですが、これだと、1 - ( 2 - ( 3 - ... ) みたいになるので、人の直観とは合わないかも。

　　　 ← ・ ← ・ ← ・ ←
　　 　　↓　　↓　　↓

みたいにすると、((( 1 - 2) - 3 ) - 4 ) ... になります。引き算がまともになる。

で、Tree から list に変換する時に、順方向と逆方向が可能。 なのだが、逆方向がなかなか書けない。なんか一時間以上かかったぞ。

だいぶ焼きが廻ってるな。

これで、パターンを作って Agda の群論の式を整形する方式は割と便利。

　　data MP　: Carrier → Set (Level.suc n) where
　　　　am　: (x : Carrier )　 →　MP　x
　　　　_o_ : {x y : Carrier } →　MP　x →　MP　y → MP　( x ∙ y )

　　mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
　　mpf (am x) y = x ∙ y
　　mpf (m o m₁) y = mpf m ( mpf m₁ y )

　　mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
　　mp-flatten　m = mpf m ε

　　mpl1 : Carrier → {x : Carrier } → MP x → Carrier
　　mpl1 x (am y) = x ∙ y
　　mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1

　　mpl : {x z : Carrier } → MP x → MP z　→ Carrier
　　mpl (am x)　m = mpl1 x m
　　mpl (m o m1) m2 = mpl m (m1 o m2)

　　mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier
　　mp-flattenl m = mpl m (am ε)

　　test1 : ( f g : Carrier ) → Carrier
　　test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

　　test2 : ( f g : Carrier ) → test1 f g ≡　g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙　(f ∙ g) ⁻¹　∙ ε
　　test2 f g = _≡_.refl

　　test3 : ( f g : Carrier ) → Carrier
　　test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

　　test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))
　　test4 f g = _≡_.refl

マイナポイント

まあ、いろいろ残念なんですが、

　　マイナポータルからは案内がない

そんなものか。え、アプリ落とすの? なのだが、選択肢があんまりない。クレカもQuic Payもだめなのか。

結局、諦めて、Pay Pay のチャージに。でも、今チャージしちゃだめなのね。9月からか。

その何回もカード見るのやめて欲しいなぁ。接続不安定なんだから。

Pay Pay はハリーズ専用に使っているので、まぁ、それでいいかな。

いや、

　　諦めて、毎月、10万円配るんだ
　　でもしか公務員増やすんだ

リーマンショックの数倍の不況なのだから、通常の方法でだめだよ...

一階述語論理

Prolog に一コマ取ってるので、定義と説明があるのだが

　　Agda でやるよね?

で data で構文定義していく方式で。割とすぐに書けたんですが、やっぱり構文ださいよねで、parser 書いたら思いっきり複雑に。

特に証明しているわけでもないのでHaskellでいいんだど。paeser は諦めて、

　　ex1 : Statement
　　ex1 = All X => All Y => (( Exist Z =>
　　　 ( ( predx father ( var X , var Z ) ∧　predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )

これくらいで妥協か。で、Star Wars のねたばれ例題をやるわけですが。

　　brother ( const leia , const leia) = true

あぁ、この定義ではそうなるか。ま、いいよね。

　　data Var : Set where
　　　　　X : Var
　　　　　Y : Var
　　　　　Z : Var

　　data Func : Set where

　　data Pred : Set where
　　　　　father : Pred
　　　　　brother : Pred

　　data Expr　: Set　where
　　　 var　 : Var　 → Expr
　　　 func　: Func　→ Expr → Expr
　　　 const : Const → Expr
　　　 _,_　 : Expr　→ Expr → Expr

　　data Statement : Set where
　　　 pred　　　 : Pred　　　→ Statement
　　　 predx　　　: Pred　　　→ Expr　　　→ Statement
　　　 _∧_　　　　: Statement → Statement → Statement
　　　 _∨_　　　　: Statement → Statement → Statement
　　　 ¬_　　　　 : Statement → Statement
　　　 All_=>_　　: Var　　　 → Statement → Statement
　　　 Exist_=>_　: Var　　　 → Statement → Statement


　　_⇒_ : Statement → Statement → Statement
　　x ⇒ y = ( ¬ x ) ∨ y

Interpretationと節形式への変換までできたのでいろいろインチキはあるが問題ない感じ。Eqaulity 入れるとぐっと難易度が上がるらしい。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/FirstOrder

Zoomでのペアプロ

特に問題ないっていうか、

　　寝っ転がりながらできる

という素晴らしさ。しかも、

　　学生にやらせてる間、内職も可能(メール読みとか)

言わないと何もしない学生に、back ground job を割り振ることも可能。なんか、

　　いいことずくめだ

ちなみに、関係ないと思った学生は

　　BGM にしてるから大丈夫です

ということだそうです。

自分の影響だから仕方ないのだが、vim / emacs 派が多いな。一部、Unity 。

HDD分解

OSの授業で分解したものを見せたりしてます。HDDも、もうすぐなくなってしまうかも。


この間、何もしてないのに壊れたHDDですが開けてみると、

　　昔のと、それほど変わってないかも

枚数が多いな。ヘッドが動きにくい感じ。

- * - * - * -

サーバ構築中ですが、いろいろ苦労してる感じ。いざとなれば今動いているVMそのままなんていう手もあるが。

ダイニングキッチン幸福

いや、名前からしてなぁ。門構えもこれでしょ? マチナトボウルの向かい、エンダーの裏だが... しかし、

　　ランチやってる

というので入ってみました。居酒屋ランチは当たりなことが多い。

なんか、松花堂ランチがある。それって、和風亭のと同じなんですが。

　　で、結局、ほぼ同じようなものが。1100円

これは割と優秀かも。いや、和風亭と同じなんだけど。もしかすると、和風亭と提携? まさか。

LLVM clang

なんか、まだ、バグが... まぁ、自分たちのせいなんだけど。

　　最適化フラグを付けないと SEGV

うーん、なんか通ってないパスがあるとか。で、調べると、

　　clang -cc1 -mllvm -debug-pass=Executions

とすると、どれを通るか教えてくれるらしい。で、研究室のGrowi に書こうとしたら、

既に書いてあるじゃん。やるな清水。Executions ではなかったが。

でも、なんか良くわからないので、とりあえず対症療法で。

台風 チャンミー

できたと思ったらいきなり襲来といういつものパターン。

　　沖縄だと、ちょっと風邪強い日だな

くらいです。でも、バスの乗り換えの時に土砂降り食らった。その時だけなんだよな。なんなんだ。

真栄原の緑はゆっくり片付けます。

HDD の音

QNAPに入れてた WDの6TBも飛んでたんですが、がっかりな音だな。保証は2018/11までだったらしい。

もう少し買い足す予定だが、6TBと8TBどうしようかな。

Main Switch Failure 第二幕

壊れた3850の代替が来たので入れ替えて終わりなはずだったんですが...

　　設置しただけで上の二台が飛ぶ

という症状が... Revenge ですか。原因不明で、

　　持ってきた一台を使って再構成

ってな感じだったんですが、実はだめだったのは

　　Stack Power

Stack した Switch の電源を融通する的なものらしく、冗長モードと強調モードがあるらしい。

いや、3台に電源は二つずつ6個もついてるわけですよ。で、

　　そのStack Power Calbe に触れるだけで落ちる

解決方法は

　　そのケーブルを外す

そんなものでいいんですか。再構成の途中でループがあったり、iSCSIの channel group の問題があったりで午前中に終わるはずが15時くらいまで。

まぁ、でもなおって良かったです。このシステムも今月一杯で更新なのに、最後の最後でやらかしてくれるよな。

これも前回の停電の影響だろうなぁ。施設部には問い合わせてるんですが、応答なし。

成績付け

試験嫌いなんだよ。で、試験しない人です。成績は課題とレポートだけで付けてます。ゆっくり人のを見ながら解いていいよ。

　　その方が難しい課題をたくさん出せる

やっぱり数だと思うんだ。そして、エビデンスが残る。先生と学生との両方に。それが自信になると良いんですけどね。

なので、そんなに一生懸命採点してません。メールのレポートをscriptで集計。あんまりなものにはコメント的な。

今年は、WordPress のpageとか MatterMost とかも使ったんだが、やっぱりメール集計scriptが便利だな。

LMS もいいんだけど、Web page でごそごそやるのはダサくて。Browser ってその上で文章を書くには最悪。

　　編集機能が低い

　　途中セーブとかの機能がWeb page依存

　　なので消えやすい

　　書いたものが手元に残らない

ってなわけで、しばらくはメールベースかな。メール自体がレガシーなのはそうなんですが、ネットベースのツールのできが悪すぎる。

いや、もっとも、メールが便利なのは MH 使ってるからかも。

Goole App Script とかは、まぁ、その辺をなんとかしようという意図は見えるが、

　　囲い込みくささがくさ過ぎる

F Key

良くあることらしいんですけど、MBP 15 の F のキーがはずれました。3年目だし。

簡単になおるだろうと思って予約してキタムラに行ったのですが「取り寄せになります」。お。

ま、しかたないか。ネットに出てるのを買った方が早い気もするが...

QNAP recovery

すったもんだしましたが、まぁ、なんとか復旧。無意味に Linux Software RAID / LVM に詳しくなってしまった。

どうも抜き差しした時に入れ替えてしまったのがだめだったらしい。

まず、

　　# md_chechker
　　# cat /proc/mdstat

というcommandがあり、それで md (multi device) つまり Software RAID の状態をチェックできる。なかったら作る。
QNAP は partition 3 に作るので、いったいどういうRAIDだったのか

　　# mdadm --examine /dev/sdd3

とかで状況を見れる。Disk が生きてないとだめですが。今回ははずしてしまって md3 とかないので作る。

　　# mdadm --create --assume-clean -l1 -force -n1 /dev/md3 /dev/sdb3

1台はおかしいだろと文句いわれるので -force 。--assume-clean なら問題ないらしい。

これで、/dev/md3 ができるので、

　　# dd if=/dev/md3 bs=512 count=255 skip=1 of=/tmp/aho3
　　# vi /tmp/aho3

すると、LVM の config が見れる。これは、

　　# ls /etc/config/lvm/backup
　　# ls /etc/config/lvm/archive

とかにある奴と同じはず。QNAPを初期化したりしなければ。あるいは、他からもってきたHDDでなければ。

違っていたら、HDDの方が正しいので、それを元に新しく作る。それを

　　# vgcfgrestore --force -f /tmp/vg3 vg3

で restore する。その前に、vg congig の backup はQNAPの外にとっておく方が良い。(でないと後悔することが

　　# vgccan ; pvscan ;　vgchange vg3 -a y

とすれば、/dev/mapper になんかできるはず。そこで、

　　# /etc/init.d/init_lvm.sh

すれば、Web UIの storage manager に表れるはずです。表れない時は、

　　# mount -t ext4 /dev/mapper/cachedev6 /mnt/sdc_root/

とかで手動 mount を試みる。で、見えることもあるくらい。だめだったら? vg config をなおしてく感じか?

HDD上の vg config が生きてればなんとかなる感じみたいです。

いや、RAIDなんて使いたくなくて、BDの代わりみたいに使いたい。なので、自分で mke2fs してしまう方が良いらしい。

それで普通に認識してくれるようです。

https://www.linuxjournal.com/article/8874




-

Main Switch Failure

だいたい年二回くらい嫌がらせのような計画停電があるんですが、

その後、研究室のサーバにアクセスできない

で、夜、気が付いたんですが、MatterMost に「スイッチに赤いランプが点いてる」あだだだ。

担当SEさん(みんなも知ってるうちのOB)と一緒に朝一で...

　　Console calbe どこ?

そこからですか。3850 の三台 Stack なんですが、一番下のが電源二つ赤いランプ。「じゃぁ、一台他のと交換して」

　　やっぱり、だめですね。本体故障確定です。

だだだーん。代替が来るまで放っておいてもいいかと思ったんですが(ぬるい)、

　　ポート空いているので、差し替えて再構成します

本気ですか? 結構大変だと思うけど。結局、GBIC を二つを上の方に。なんですが、

他のフロアスイッチ、ルームスイッチも気絶しているっぽい

一体全体どうやれば、そんなに機材を巻き込むような停電が可能なの? 学生によると

　　そろそろかと思ったら、既に落ちていた

的な話なので、まぁ、なんかやらかしたんでしょう。サージか瞬電か。

まぁ、でも午後三時には復旧していたので良かったです。

10年前なら自分でやってたかもな。いや、自分でやりたかった気もするが... でも、頼もしいOBが頼もしい仕事をしてくれるのは素晴らしい。

ぐ、NAS をすっとぱした

いや、RAID 信用してないので使ってないつもりだったのだが... QNAP だしなぁ。 Disk 毎に 1 volume にしてたし、それでつながっていたので大丈夫だと思ってたんですが、 　1台目が Bay が二ついかれて、さらに一台HDDが飛んでるらしい なので、HDDを2台足してなんとかってことだったんですが、 　動いている方のHDDを引き抜いた いや、1台だったら別に大丈夫だったはずなのだが、これ、うっかり差すと、そっちに上書き始めるんだよな。 そういう設定にしてないはずだったんだが... まぁ、4台のうち半分はなんとかなったんだけど、残りの2台がなぞです。 まぁ、どうせアニメ録画とかだし、光学メディアの方にもあるので、時間かければだいたいはリカバリできるはず。 QNAP のGUIからではなく、手で、e2mkfs するべきだった。 https://gist.github.com/nvpnathan/827aac9e972f22233ca63d17e2fbea04

Emacs / Viper / Unicode Parenthises

Agda ではUnicodeな括弧を良く使うわけなんだけど、show match して欲しいよね?

　　( [ { ⁅ ⁽ ₍ 〈 ⎴ ⟅ ⟦ ⟨ ⟪ ⦃ 〈 《 「 『 【 〔 〖 〚 ︵ ︷ ︹ ︻ ︽ ︿ ﹁ ﹃ ﹙ ﹛ ﹝ （ ［ ｛ ｢
　　) ] } ⁆ ⁾ ₎ 〉 ⎵ ⟆ ⟧ ⟩ ⟫ ⦄ 〉 》 」 』 】 〕 〗 〛 ︶ ︸ ︺ ︼ ︾ ﹀ ﹂ ﹄ ﹚ ﹜ ﹞ ） ］ ｝ ｣

このあたり。evil.el は dot (command の repeat ) が馬鹿過ぎて諦めました。たぶん、agda-mode との干渉もあるんでしょう。

結論的には以下のコードを ~/.emacs.d/init.el に入れればよい。まぁ、少し動作はおかしいが、良しとする。
(space は全角間隔にしてるのでコピペでは動きません)

;; extend parenthises match
;; "\u0028 " "\u005b " "\u007b " "\u2045 " "\u207d " "\u208d " "\u2329 " "\u23b4 " "\u27c5 " "\u27e6 " "\u27e8 " "\u27ea " "\u2983 "
;; "\u0029 " "\u005d " "\u007d " "\u2046 " "\u207e " "\u208e " "\u232a " "\u23b5 " "\u27c6 " "\u27e7 " "\u27e9 " "\u27eb " "\u2984 "
;;
(eval-after-load "viper"
　'(defun viper-paren-match (arg)
　"Go to the matching parenthesis."
　(interactive "P")
　(viper-leave-region-active)
　(let ((com (viper-getcom arg))
　　　　(parse-sexp-ignore-comments viper-parse-sexp-ignore-comments)
　　　　anchor-point)
　　(if (integerp arg)
　　　　(if (or (> arg 99) (< arg 1))
　　　　　　(error "Prefix must be between 1 and 99")
　　　　　(goto-char
　　　　　 (if (> (point-max) 80000)
　　　　　　　 (* (/ (point-max) 100) arg)
　　　　　　 (/ (* (point-max) arg) 100)))
　　　　　(back-to-indentation))
　　　(let (beg-lim end-lim)
　　　　(if (and (eolp) (not (bolp))) (forward-char -1))
　　　　(if ( not( looking-at "[][(){}\u2045\u207d\u208d\u2329\u23b4\u27c5\u27e6\u27e8\u27ea\u2983\u2046\u207e\u209e\u232a\u23b5\u27c6\u27e7\u27e9\u27eb\u2984]"))
　　　　　　(setq anchor-point (point)))
　　　　(save-excursion
　　　　　(beginning-of-line)
　　　　　(setq beg-lim (point))
　　　　　(end-of-line)
　　　　　(setq end-lim (point)))
　　　　(cond ((re-search-forward "[][(){}\u2045\u207d\u208d\u2329\u23b4\u27c5\u27e6\u27e8\u27ea\u2983\u2046\u207e\u209e\u232a\u23b5\u27c6\u27e7\u27e9\u27eb\u2984]" end-lim t)
　　　　　　　 (backward-char) )
　　　　　　 ((re-search-backward "[][(){}\u2045\u207d\u208d\u2329\u23b4\u27c5\u27e6\u27e8\u27ea\u2983\u2046\u207e\u209e\u232a\u23b5\u27c6\u27e7\u27e9\u27eb\u2984]" beg-lim t))
　　　　　　　(t
　　　　　　　 (error "No matching character on line"))))
　　　(cond ((looking-at "[\(\[{\u2045\u207d\u208d\u2329\u23b4\u27c5\u27e6\u27e8\u27ea\u2983]")
　　　　　　 (if com (viper-move-marker-locally 'viper-com-point (point)))
　　　　　　 (forward-sexp 1)
　　　　　　 (if com
　　　　　　　　 (viper-execute-com 'viper-paren-match nil com)
　　　　　　　 (backward-char)))
　　　　　　(anchor-point
　　　　　　 (if com
　　　　　　　　 (progn
　　　　　　　　　 (viper-move-marker-locally 'viper-com-point anchor-point)
　　　　　　　　　 (forward-char 1)
　　　　　　　　　 (viper-execute-com 'viper-paren-match nil com)
　　　　　　　　　 )))
　　　　　　((looking-at "[])}\u2046\u207e\u209e\u232a\u23b5\u27c6\u27e7\u27e9\u27eb\u2984]")
　　　　　　 (forward-char)
　　　　　　 (if com (viper-move-marker-locally 'viper-com-point (point)))
　　　　　　 (backward-sexp 1)
　　　　　　 (if com (viper-execute-com 'viper-paren-match nil com)))
　　　　　　(t (error "")))))))

https://stackoverflow.com/questions/15717103/preferred-method-of-overriding-an-emacs-lisp-function