iTunes match の続き

iTunes match は入れられたんだけど、これはLibrary全体をuploadにいくわけですが、

＊　昨日入れたのは、当然、停まっている

まぁ、そうだよなぁ。自動的に再開するので放っておけば良い説もあるらしい。

購入したもののいくつかはAACに変換できた(9/342)みたい。何故かなくしてた The Yes Album のdown load が可能になっていただけでも、良しとするかという感じ。

http://www.excite.co.jp/News/reviewapp/20140507/E1399403695656.html

ここがわかりやすいですね。

つまり、matchするとiCloud のマークが変化するので、それをクリックしてダウンロードしろということらしいです。そして、

upload が停まったら、sign out / sign in して、iCloud Library をon にしろと。なるほど、わかりやすい。

たぶん、これ、upload が終了するまでに数週間かかるんじゃないかなぁ。

そして、

＊　match しなかったら、mp3 をaacにしろ

とかいうありがたいコメントが。mp3 は4千曲あるんですが。Apple Script 使うにしても結構厳しいだろうな。どうせ、

＊　LPから取り込んだものや、沖縄民謡のCDはマッチしない

わけだし。

というわけで、iTunes match との戦いは、しばらく楽しめそうです。

El Capitan

というわけで、Mac Mini をMarvericks から El Capitan 　に上げてみました。install 入れて帰ったら、朝には音信不通。

＊　何故か、AIMのpasswdで引っかかっていった

学科の外部から見えるサーバは「DHCPしない」って技をシス管が出したので、手動で設定する羽目に。IPv6 は自動で良いらしい。と思ったら、

＊　fe80 だけやん。

IPv6 を手動で入れろてか。くそめんどくさいです。Akatsuki 死ね。

でも、El Captian 自体は特に問題ないらしい。Yosemite の時には結構苦労したんだけどな。あの時は、

＊　clean install でないとハマる

というのがあったので、clean install したからか。その時の clean install は HDD が飛んだのでなかったことに。

＊　まぁ、世の中、そんなものだよね。

あの時には、postfix のCAの設定とかもやったんだけど、それもなかったことに。どうせ、オレオレ証明書だし。そういえば、3年で切れる設定になってるな。

＊　ちょうど、修士が卒業して設定がわからなくなったところで切れる

なるほど、良くできてますね〜 もっとも自分で設定しても「3年前だと、ちとわからねぇな」となることは確実だ。

いや、それも Marvericks に戻ったのでなかったことに。

iTunes Match の方は入れてみました。でも、、おそらくは、これから、すったもんだするだろうと思いますね。時間かかるしエラーも出るらしい。

Match は期待してないので、m4p -> m4a の変換の方を優先するのかな。これは手動ならしい。本気?

iTunes Match and Apple Music

というわけで、ちょっと調べてみたわけですが、

＊　iTMS は、iTunes Match に入っていれば DRM Free (それ以外は洋楽でもm4p)
＊　iTunes Match から抜けても、DRM Free で落としたものは残る

なんだが、Yosemite 以降らしい。うちのDesktopは Marvericks だったりするので、OS上げるところかららしいです。

MBP で iTunes Match するわけにもいかないだろう...

Apple Music は抜けたら落としたものも再生不可。家族割あり。

ってことね。iTunes Match が、そんなに高いとは思わないですけどね。iTunes Match/Apple Music/iCloud Drive でセットにしろよ... iCloud Drive は家族割なしだからなぁ。

LPから落としたものとか、沖縄民謡とかあるので、どっちもあまり期待できないところがなぁ。なので iTunes Match は見送りだったのですが。

m4pなのは持ってる1万曲中の340曲程度らしいので、それをDRM Freeにするためだけに iTunes Match ってのもありかな。まぁ、そうすれば、iPhone のたこなMusic Playerは使わなくて良くなるな。

OS上げるなら春休み中だけど...

イヤホン

なくしたと思っていた ER-4S ですが、

＊　前のかばんの奥底に埋もれていたらしい

なんと、復活しました。

2011に買ったらしい。

http://seeker-s-eye.blogspot.jp/2011/12/blog-post_28.html

なくしたと思ったのがいつなのかはわからないん。

この手の話は2007にもあるな。

http://seeker-s-eye.blogspot.jp/2007/05/blog-post_495.html

でも、iPhone で音楽聞くとか、ほとんどしなくなってるからなぁ。なので、なくして困ってなかったし。

でも、これを機会に少し聞くようにしても良いかも。

レンタルCDが扱いやすいが、わざわざ借りに行く面倒くささよ。エアチェックな手間も高校生じゃあるまいし。iTMS とかの m4p なのは、もう要らないです。

というわけで聞かなくなったってことね。まぁ、販売側も余り売りたくないみたいだし。自業自得だな。

ライブとかに行ったら、その録音/録画がもらえるぐらいでいいと思うんだよな。そういう値段になりつつあるし。

うちの大家さん

アパートでいろいろ壊れると不動産屋に電話するわけですが、

＊ まあ、あまりスムースには進まない

だけど、大家さんにつながると、

＊　大家さんが自分で直しに来てくれます

素晴らしいです。

まぁ、それが一番安上がりだし、信用できるんだろうな〜

日本人は「とにかく文句を言われないように」とかいいながら、結構、手を抜くからなぁ。自分のアパートを自分で直すようになるのは仕方ないのか。

かばん

まぁ、あのボロボロのが気に入っているわけですけどね。

見かねて奥様がいろいろ買ってきてくれるわけですが、

＊　キャンバス地

なものも結構長く使ったんですが、これはスーツの方が負けてしまう。鞄の部分の生地がだめになっちゃう。

で、Tumi のを買ってきたんですが、あの黒くてでかいのを、どうにも使う気がせず。

で、今回のは、BREEとか書いてあるな。まぁ、黒いんですが、今の鞄よりはだいぶ軽い。皮地も結構良い。

まぁ、しばらく使ってみるか。というところです。

皮の鞄や靴は雨の日とかは油塗ってから出ると良いんですけどね。割とサボった割には前のかばんは長持ちしたな。

Agda

この間からはまっていたのは、ようやっとできました。

＊　振動するんだよね

あっちやって行き詰まって、また別な方向やって、また、元に戻って。しまいには、

＊　やろうとすると、こういう風に行き詰まるというのを思い出すように。

今回は Maybe の使い方と、data を使った制約の書き方を学べました。

まぁ、圏論/Agdaは1個とか2個とかの具体的なことをやろうと思うと大変。証明の場合分けが爆発しちゃう。

入力の射の種類によって場合分けするんですが、

＊　起きないはずの場合わけが出てしまう

まぁねえ。それぞれの射にt0とt1があれば全部の組み合わせが出ちゃうよな。で、証明できない...

と思ったんですが、

＊　Maybeを扱っていると、just/nothingの組み合わせで出ないものがある

nothing と nothing　の等号はnothingになるわけなので、等号のところにはjustとは書けない。逆に等号がnothingだと、その両辺はnothing。

そうか、そうやって場合分けを制約することができるのか! 等号は data で実装されているので、data で場合分けの制約を書ける! とわかったので、なんとかなりました。

まぁ、あんまり綺麗な感じでないけどなぁ。

Agda の data は論理式としては排他的和で異なる型の組み合わせで、データ構造としてはタグ付きのUnion。

record は直積に相当して、用途としては「fieldに記述した論理式を満たす性質を持つもの」というように使うようです。

例えば、等号は、

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

こんな感じ。Prolog の f(X,X). ですね。同じ値で、refl a a みたいにしないと　a ≡ a を作れない。これを入力で受けると、

　　lemma1 : {a} ( x y : Set a ) ->　x ≡ y　-> ...
　　lemma1 {a} x y eq　= ...

で、x と y は同じ場合しか受け付けなくなるというわけ。なるほど。単一化、Unification という理屈だとはわかっていても、ちょっと気持ち悪いか。

二個の圏の対象は、

　　data　TwoObject {c₁ : Level}　: Set c₁ where
　　　 t0 : TwoObject
　　　 t1 : TwoObject

こんな感じ。t0 と t1 は constructor ですね。

それで、射を

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
data Arrow {c₁ c₂ : Level } ( a b :　TwoObject {c₁} ) : TwoObject {c₁}　
　　　-> TwoObject {c₁} -> Set c₂ where
　 id-a : Arrow a b a a
　 id-b : Arrow a b b b
　 arrow-f :　Arrow a b a b
　 arrow-g :　Arrow a b a b
　 inv-f :　Arrow a b b a

という感じで、id-a は aからa、id-b は bからb。arrow-f は a から b という風に制約してみました。これで、

aからbの射とbからbの射を入力しているのに、abからabへのあらゆる組合せが出てきてしまっていたのが、ちゃん整合しているのものしかでなくなっって、ばっちり。

なるほどね〜　いや、まぁ、あんまい綺麗な方法とも思えないが... とりあえずできてめでたい。

いや、これを使って、LimitからEqualizaerを出して、それを使って、Floyd Adjunction Functor Theorem を証明するはずなのだが、まぁ、それはおいおいだな....

モバイルサイト

あの

＊　字が大きくて一画面の情報が少ないサイト

ですね。いや、わかるよ。

＊　老眼専用

でしょ? 今までは、老眼な人はスマホとか使わなかったから、そういう人たちが判断してなかったんだと思うんだ。でも、

＊　そろそろPCとかスマホとか使い、企業判断する人が老眼な世代になった

ってことなんだろうなぁ。いや、まったく、

＊　超迷惑

だと思う。だって、スマホの売りは、

＊　PCサイトがそのまま見れる

だったはずだよね。でも、PCに戻せるサイトはまだまし。戻せないのもある。

NHKニュースWebのことなんですが、どうも Chrome の Request Desktop View も蹴られるらしい。まぁ、日経でいいか。あっちのloginがハズレるのもうっとうしいのだが。

今日もRetina MBPの画面を除かれて「超字が小さい!」とか言われましたが、やっぱり一画面の情報量が多くないとね。

沖縄県総合運動公園

泡瀬にあります。入口までは行ったことあるのだけど、中は広いので時間がなくて。でも、

＊　日曜日に 16:30 からIngress First Saturday という名前のBBQパーティ

があるということなので行ってきました。

＊　バス Ingress なので、当然バス

330を石平(いしんだ)で右に曲がって行くバスにのれば良い。結局、どちらもコザにいくらしい。52番と61番ですが、61番は一日六本だからな。

なのだが、58号線の方の森川公園に寄りたかったので、58号線からの乗り継ぎを考えるはめに。23番が石平にいくのでバッチリだ。

で、公園には時間通りついたのですが、

＊　みんなのいる場所はどこ?

どうも、オートキャンプ場らしく。公園のミッションこなしながら行ったら40分かかりました。

そして、そこからの終バスは19:48。那覇に行くのは遅くまであるらしいけど、西原側通られてもなぁ。

まぁ、でも、BBQなら、3時間もいれば十分でしょう。(食べるだけならば :-p )

少し自信なかったので早めにでたら「バスは10分遅れ」をくらって、バス停でしばらく待つ羽目になりましたが、無事帰れました。

キーマカレーで始まったり、野菜がたくさんあったり、肉の焼き場は別にあったりで、なかなか楽しかったです。

青の方は沖縄市のNovaもあって、そっちの方も面白かった。途中でキ0ーを拾えたので、一つだけリンクを貼れました。もっと早く知ってればキー取りに行ったかも。まぁ、こういうのは情報統制が問題だからな。

恐怖の頭脳改革

キースエマーソンが亡くなったのは、それなりのショックでしたが、

＊　DAMのカラオケには、Karn ♯9 が登場

したみたいです。

ELPはLPで結構あるわけなんですが、展覧会の絵とか恐怖の頭脳改革とか取り込まなかったんだよな。たぶん、CDから読み込もうと思ったのではないかと。別音源のは一応持ってるので。

LPからの取り込みに使っているのは、たぶん大学生の頃に買ったTechnics SL 1301 です。

昔のオーディオ
http://seeker-s-eye.blogspot.jp/2008/03/blog-post_9040.html

に一回書いてるな。フルオートなんですが、さすがに、オートリターンしか動かなくなってる。直すのは不可能ではないかも知れないけど、難しいだろうな。

カートリッジはDL103使っていたんですが、いつかのカレーパーティの時に壊しました。なので、AT-15EGで使ってます。

なんだが、

＊　SL 1200 の新しいのが出るとか!?
http://www.theverge.com/2016/1/5/10718234/technics-sl1200-sl1200g-sl1200gae-turntable-new-models-announced-release-date-ces-2016

ぐっと欲しくなるんですが... 幸いなことに、まだ出てないらしい。

新しい方は値段も不明ですが、SL 1200 は中古で良ければ4万円ぐらいで手に入るのか。その程度の値段だと良いな〜

Apple Photos.app and Cloud Storage

iPhone と連携させるわけですが、

＊　Photo Stream は偉大だった

なんだけど、Photos.app にしてから、どうも詰まるらしい。iCloud storage を使うという選択肢もあるわけですが、

＊　有料(1TB 年間15,600円)

昔の MobileMe とかだと、5人分払うみたいなことが可能だったんですが、どうも、

＊　iCloud は家族割みたいなものはない

ってことは、さらに、これの倍?! それは、ちょっとありえないな。

＊ 200GB/年間4,800円

っていう中途半端なのもあるが...

でも、まぁ、

写真とか音楽とかを除けば、無料の5GBで十分

なわけだよね。Google drive / Google Photos で良いし。(Bitcasa は解約しました)

なんですが、Photo Stream の調子がよろしくないし、定期的に iPhone から自宅サーバ側に写真を移すわけですが、

＊　写真をすべて取り込んで削除

が動かない。写真をバックアップからはずしたりしてたからかな。仕方ないので、

＊　手動で選択して削除

したんですが、

＊　サーバ側でほとんど重複したので、それをさらに手動で削除する羽目に

昔の iPhoto には重複検出と削除があったんだけどね。いや、そういうことをする AppleScript とかも持っていたりはするんですが...

＊　iTools の時には、もっとしょぼいサービスに年間1万円払ってた

わけなんですけど。

Google drive なら同じアカウントを使うとかも可能なはずだが...

Google Drive 側は、Academic なアカウントの方は結構容量を使えるらしいので、そっちに移行するのが正しいはずなんですが、そっちも、なんだかな状態です。

というわけで、結果的に Cloud Storage は、Bitcasa を解約しただけな状態です。あらまぁ。

SSDの価格下落も進むという予想もあるらしいけど、今後5年ぐらいはHDDの方が安いかな。

http://www.itmedia.co.jp/news/articles/1512/09/news103.html

昨日は飲みすぎだった...

まぁ、奥様がご機嫌だったので良かったです。

Agda は、

f
--->
・ ・
--->
g

というのをやっているだけなのだけど、これだとf の逆向きの射はは存在しないわけだよね。適当に辻褄合わせの射を入れれば良いというアプローチだったんですが、圏の結合則とかはともかく、Functor の分配則がだめで、この方針ではダメらしい。

なので、そもそも射がないという性質を持つ圏を作らないとダメなんだよなということに気がついたのが昨日の午後。Agda の Maybe と格闘してました。

＊　Maybe と整合性のある等式公理

があるだというのがわかりました。この辺も未定値⊥を持つプログラム理論とかで勉強していたはずなんですけどね。簡単だよね、ふんふん、とかですませていたが、

＊　自分で等式の反射律とか推移律とかを書くとなると面倒

それがData.Maybeに既に書いてある。やっぱりライブラリは偉大だ。

とはいえ、まだ、終わってないです。この証明「いけそうだ」「だめだ」を何回繰り返したことか。証明自体は簡単なんだがなぁ。

とかやっていて、遅刻しそうになってあわてて家を出たら、奥様が上がってくるところで、結局、そこからさらに遅れて出ましたが、車でいくことになったので、まぁ、なんとか間に合ったみたいです。

LINEは復活できました

しつこくメール送って、同じFAQを見されられてたんですが、

＊　今日試したら、E-Mail でCarry overの認証

というメニューが出て移行できました。

いや、今まで、そんなメニュー項目なかったと思うんだよな。多分、向こうでなんかやってくれたんでしょう。

でも、この対応って、LINEは毎日何百人とやっているんじゃなかろうか... ご苦労様なことです。

なんか、PC用のLINEアプリもあるらしいけど、

＊　前のをdeleteして移行

とかやっている限り、いろいろ事故は避けられないんじゃないかなぁ。まあ、余計な心配か。

脱出ゲーム

終わらない学級会からの脱出
アジトオブスクラップ
http://realdgame.jp/ajito/okinawa/

に有人に誘われたので行ってきました。初体験。

制限時間一時間で、結構、高密度ですね。みんなで考えるという形式で、なかなか面白かったです。午後2時から始まって4時には終わるという感じですね。

脱出成功にはなりませんでしたが、結構、良いところまでいって90点でした。いや、結構、ヒントもらってたかな。ヒントで難易度調節みたいな感じなのかな。時間的に厳しい感じなので、結構、飛ばしていかないとだめですね。

まぁ、あまり貢献できませんでしたけど、力仕事系には役に立ったかも。。

常設ものらしいですが、イベントものも面白いらしい。

基地内ポータルの続き

ひさしぶりに、がっつり Ingress 。いつもの普天間一周コースでした。森川公園(普天間の西)と市民のいこいパーク(普天間の東)の両方は、やりすぎなんだが...

基地内ポータルからのリンクが、いくつか外周に届いていたので、それを利用して。ここしばらく、基地内のが邪魔でCF作れない状況だったからなぁ。

＊　基地内のエージェントもレベルが上がってきた

ということですかね。

西側引いてる間に、東側落とされるとか良くある。それもまた楽しい。Command Channel Open の時に more を打つと言うのを学習したので、ちょっと楽でした。

初代PS3のギガビットのトラブル

結局、ケーブル変えたくらいではだめで、100Mに戻したら動いたので、

＊　初代PS3とGBハブとの相性

の問題らしいです。で、PS3をTime Capsuleに直結してやったら動いた。本当に相性の問題らしい。

大きなパケットだと詰まるみたいな症状だな。MTU調整にしくじってるか。

ハブは、BUFFALO LSW5-GT8NP/BK でした。

まぁ、NASとの接続は、ちょっとは速くなった、かな?

QNAPの続き

4TB x 4 なのでコピーに2/23から3/7までかかりました。先にGBitなハブにかえてからやるべきだったかも。

QNAPは単なるLinuxなので、package managerで好きなものを入れられるらしい。ほとんどのものは QNAPのmanager toolから入れられるわけですけど、

zsh とかは無理

まぁ、そうだよね。ググって見つかる情報が古くて(2015で既に古い...)はまったんですが、

QNAPware(Entware)
http://apps.qnap.community/11-community/10-qnapware

のURLを手動でInstallしてやれば

opkg install zsh

で一発でした。

最初の頃に ssh に key で入るってのができなかったんですが、どうも RSA ではなくDSAを使っていたのがダメだったみたい。といっても、ssh 必要な作業はほとんどないですね。

DLNAサーバもいくつか試しましたが、m2tsようだとTownKey が良いみたいです。opkg 抜きで簡単に動きます。単なるWeb serverとして動いてくれれ良いのだけど再エンコードしたりするのが多いらしい。

なんですが、Gigabit なhubにしたらPS3からの動作が変。でも別なPS3からはアクセスできた。なので、PS3の足回りが変ならしい。UTPケーブルかなぁ。

4TB x 4 で、ほぼフルに使っていたのでRAID構成にはできず。まぁ、いつか6TB x 4構成にしたいところだな。6TB大分安くなったが結構良い値段。

TS431より新しい機種だと、直接、HDMIが出てたりするようですが、DLNAサーバの調子を見ると、ちゃんと動くかどうかは微妙かな。

iPhone復活とLINE終了

最初、Rycom 行ったんですが、在庫がないということで北谷のキタムラに。どうも、

＊　同じ機種、同じ色、同じ容量

でないとだめらしいです。なるほどね。世の中、いろんなことする人いるからな。

で、特に問題なく交換してもらって7,800円。ちょうど1年ですが、だいぶボロくなっていたからなぁ。

iTunesから restore で終わりなはずですが、

＊　restoreしたにも関わらず、アプリは再ダウンロード?

どういうこと?! まあ、それは良いが、

＊　LINEのアカウントは引き継げない

らしいです。

＊　LINEのアカウントの移行を許可してないと、前の電話番号認証かLINEのアカウントにPINを投げて認証する

ということをするらしい。LINEのアカウントの移行の許可は2段階認証メニューで行うらしい。

もちろん、LINEのアカウントとかアクセスできないし。いま、インストールしている最中なんだから。

前回

LINEの電話番号認証をスキップする
http://seeker-s-eye.blogspot.jp/2014/08/line.html

ってのをやったので、前の電話番号認証ってのは存在しないらしい。

というわけで、LINEのアカウントに関しては詰んだみたいです。まぁ、どうしてもLINEとか言い張った人の分だけなので、どうでもいいか。

と思って新規にアカウント(引き継がずに前のアカウントを使うと言うのもないらしい))作ったら、

＊　電話番号で登録が通知される

ってのをやられた。あぁ、それが嫌だったから電話番号認証をスキップしたのに。やっぱりLINEは、ちょっとだめ。

風邪はだいぶ良くなった

なんですが、血圧の薬をもらいにいった帰りに浅野浦のバス停の階段でこけて、

＊　iPhone すっ飛ばして割りました

くそ〜　しばらく家でうだうだしてたので、身体がなまってたか。まぁ、階段でこけるのは良くあるのだが...

AppleCare+ には入っているのだが...

あとは、QNAPにzshいれたりとか、LLVMいじったりとかしてました。

家にいるのも飽きたが...

Ahgda は、

＊　あ、できた
＊　やっぱりダメだ

のループをやってるみたい。でも、少しは進んだかな〜　Agda は証明を自分の頭で考えると言うのとちょっと違うので、風邪ひきの時とかに良いようですね。

まぁ、あんまりがんばらない方針で。

今までの経験だと、鼻水は当面抜けないので、どっかで見切りだな。

一日、家にいました

Ingressにはまってからは珍しい。皆勤賞とか子供の頃から縁がないものだったけど、一応、Sojourna Medal は取りましたけどね。

鼻水とくしゃみで、咳ではないので、それほど、きつくはないんだが、外に出ても社会の迷惑なだけだからなぁ。プロシンにティッシュを箱ごともっていったこともあったっけ。

久しぶりに Agdaも触りましたが、あんまり成果はなく。

＊　Limit から Equalizer を導く

という比較的簡単なお題なのだが(そして、それがFlyod Adjoint Functor Theoremに必要なわけなんだけど)、何か、うまくいきませんです。

Equalizerの要件(fe=geとか)を、自然変換の可換性で表してやればよいのだけど、

＊　関手の行き先が f : a->b

みたいなことができないらしい。関手の FMap の行き先の型は Hom A a b ではなくて、Hom A (FObj F x) (FObj F y) だからなぁ。a = (FObj F x) なのでつじつまは合ってるわけなんだけど、型がその場で一致してないとだめなので「値は同じなんだよ」と主張しても、Agda は許してくれないわけね。cast みたいなことをすれば逃げられるようではあるが。

まぁ、それでも、2(要素が2個しかない圏)とかの圏の書き方はなんとなくわかりました。Sum type との同型写像で場合分けしまくる感じ。そのままがんばればできそうな気もしたが、あまりに汚くなったので、諦めました。

きっとAgda的に画期的な解決方法があるんじゃないかな〜

風邪ひいた

忙しいのが片付くと風邪ひくという、いつものパターンですね。

鼻水だけで熱はあまりないらしい。去年は6月ぐらいにやらかしているらしいです。

http://seeker-s-eye.blogspot.jp/2015/06/bd-reos-x.html

Ingress のSojournaも明けたので、さぼってもいいんだよな。

火星の人

Starwars 7 は東京で見ました。そっちをもう一回見ても良かったのですが、時間の都合が良いのがオデッセイだったので、そちらに。

なぜ、オデッセイという邦題にしたのかは映画を見てもさっぱりわからず。The Martian が火星の人になってオデッセイになったらしい。ここまで関係ないタイトルは珍しいかも。

ISSがそのまま火星に行くみたいな感じの宇宙船で、それはそれで面白いかな。

＊　人工重力用の回転船室がある

SF映画では2001年宇宙の旅(あっちは原題がオデッセイだな)からの伝統なんですが、ISSには存在せず。実際に作ろうとすると、いろいろ難しいらしいです。まぁ、映画的な都合かな。全部、無重力で撮るのはつらいってことか。

火星の有人探査は政治的な意義はあるのかも知れないけど、成果とリスクと費用を考えるとあまり意味はないかなぁ。