Friday, 20 April 2018

不織布とBDメディア

なんか、去年あたり Goodwill でいつも使っているElecomの48枚箱が売ってなくて。と思ったら、

  BD用のを新しく売ってる

どうも「不織布が細かくなりました」みたいに書いてあります。

ググってみると、

  不織布の模様がBDメディアに転写されて読めなくなった

なんて話が。2009年あたりから使ってるわけなんだけど、この前もチェックしたが得に不都合はないんだけど。そもそも、縦置きの箱で転写するほどの圧力がかかるはずないし。

というと別に不織布でも大丈夫みたいな話も。どうも、

  溶剤が残ってる不織布だとだめ

とかいう情報もあったり。

新しい不織布は,まぁ、確かに少し凸凹は少ない気がするが、

  そんなに差があるとは思えず〜

なので、昔から使ってるのはそのままでいいか。全部箱を買い換えたりするとメーカの思うツボ的な。

check と言うのはたまに重複したもの取り除いたりしてると順番が狂うので、箱に入ってるのをplaylistだけ読み出して html な目次にするってのをやってたりするからですね。

そもそもコピ1とかでバックアップを制限するから問題になるんだろとも思います。

あぁでも場所食ってきたんだよな。そろそろテラバイトなメディアでないの?

エレコム BD ファイルケース http://amzn.asia/cDv3rzo

Thursday, 19 April 2018

Open Source Conference のネタ

まぁ、毎年、ネタがないなか出してるんですけどね。

年末からLLVM/GCCやってたので、それでも出そうかなあ。それは x.v6 用にやってたので、それでもいいかな。

Agda やったり、TreeVNCやったり、去年は、

  cmake で聴衆一人をやらかしたり

ふむふむ。そういえば、

  Java9 の jigsaw と格闘

ってのもやったな。やぶれさりましたが。

締切り 4/23 らしいので、もう少し考えます。

Wednesday, 18 April 2018

Prolog

去年もblogで書いてるんですが、授業で教えた方が良いよなってことで1講義使ってるんですが、

  去年真面目に書きすぎた

らしく、ちょっと難しすぎたんじゃないのか? と反省気味です。まぁ、時間内には収まるんだが...

たぶん、節形式は命題論理の範囲内で扱って、面倒くさい部分はリンクで外に出して、

  シーケント代数部分の例題

を入れるようにすると良いかな。

Tuesday, 17 April 2018

Blog の勧め

自衛隊の日報が話題になってますが、

  Blog は読み返すと面白い

学生とかだと、そもそも書く練習をあまりしてない。なので、とにかく書けと。Twitter で意味不明なことをたくさん書くのも良いが、

読者は未来の自分

なんだよね。他人のブログは検索してみるくらい。なので、自分に向けて書く。

例えば、MBPの新規installした時に、

 あのソフトはどうやってinstallした? 設定どうした?

とかは、blog に書いておけば一発です。

自分が面白いと思ったことを書き留めるわけなので、自分がもっとも面白いと思うらしいです。自衛隊の日報でもそうですが、

 毎日ネタ探しするようになる

ということは、今日は何か面白いことあった? と考える。 あるいは、今日はなんか面白いことしよう(そしてblogに書こう)ということになります。これが結構いいと思う。

問題は Facebook は検索が実用的ではないということね。自分でサーバ建てて、そこで運用も良いけど、メンテも自分でするの? いや、やるけどさ。

 自分は Blogger (Blogspot)

使ってます。Google のサービスだな。なので、Ingress 関係は Blogger から G+ に publish してます。

Facebook とBloggerへのMHからのscriptによる同時投稿なので、人に勧められる方法でない所が残念。でも、Blogger からの連携方法はいくつかあるらしい。 Facebook からはzipで引き上げて、bloggerにAtomでuploadするというのが可能なはずです。(二度とやりたいとは思わないが...)

まぁ、Facebook の検索性がくそなので、Blog としては役に立たないってことではあるんですけどね。むしろ、その検索性の低さに安心する人もいるのかも知れないけど...

Sunday, 15 April 2018

Docker and Kubernates

いろいろあって久しぶりにいじってますが。といっても、去年のOSの課題でもトラブってるので、そんな昔でもないか。

Dockerは何故か、

  DBとWeb Serverを別コンテナで上げる

とかの信条があるらしく、細かいコンテナが沢山上がる。別に一緒にしても良いんですけどね。で、結局、

  細かいコンテナをまとめて管理する

ってのが必要で、それが Kubernetes らしいです。複数のサーバ上のコンテナを管理できるらしい。

便利そうだけど、なんかいろいろめんどくさい。Ansible script ないの?

一昨年の Docker container をいじったら、

  Failed to get D-Bus connection: No connection to service manager

とか言われる問題と少し格闘してました。/etc/rd 以下のscriptを起動すると勝手に sytemd が動くらしく、systemdが文句を言うらしい。

  systemd また、お前か?!

という感じ。docker --privledged /sbin./init とかすれば回避できるのだそうです。ふーん。他にもいろいろ疑問はあるが... ここまでかな。

Saturday, 14 April 2018

新歓LT

いや、さぼったんですけどね。結構、賑やかだったようです。なんと去年は1年次が10人しか来なかったらしい。今年は、

  ポスター貼りまくった
  當間先生が紹介してくれた

とかがあって、30人参加だったそうです。良かったね。ちゃんとすれば来てくれるものさ。

新B4の一人は研究室の居心地が良いらしく割と来てくれてます(本当は4人だけど)。別にB4でなくても研究室くれば良いのにと思うが。 LTでも、

  研究室の様子がわからない -> 行け!

なんてのがあったらしい。自分の研究に興味を持ってくれる人を歓迎しない先生はいないからさ。

自分も学部1年の頃から哲学の研究室に顔出してて楽しかったです。酒飲みな先生だったな〜

Agda の否定

前にもやったことあるんですが、また、勉強中です。

  http://seeker-s-eye.blogspot.jp/2017/03/agda.html

<,=,> の場合分けで、その計算型goto文を使うわけですが、

 data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
      Set (a ⊔ b ⊔ c) where
  tri< : ( a :  A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :  B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :  C) → Tri A B C

なので、ばっちり否定が入っていて。こいつで、場合分けしたら、tri≈ なら、それ以外の場合は出てこないはずなんですが、場合分けは出てきてしまう。

  checkEQ ( x y : ℕ ) -> ( eq : x ≡ y ) -> compare x y ≡ tri≈ _ _ _
  checkEQ x y refl with compare x y
  ... | tri≈ _ refl _ = refl
  ... | tri> _ neq gt = ?
  ... | tri< lt neq _ = ?

みたいにしたいわけだけど。いや、 x ≡ y なんだから、tri> とかは出てこないはずだろ?

Agda での否定は、

  ¬ A = A -> ⊥

みたいに定義されていて、対偶 ( ¬ B -> ¬ A ) は、

   ( B -> ⊥ ) -> ( A -> ⊥ )

ならしい。つまり、 B -> ⊥ と A の二つの入力がある。A -> B があれば、B -> ⊥ から、三段論法で、A -> ⊥ がでる。つまり、

   contraposition : (A -> B) -> ( B -> ⊥ ) -> ( A -> ⊥ )
   contraposition f g x = g ( f x )

というわけ。この逆方向( ( ¬ B -> ¬ A ) -> ( A -> B ) ) は直観主義論理では証明できないらしいです。

そういえば、否定からはなんでも出てくるのあったなと思い出した。

  ⊥-elim : ⊥ -> _

あ、そうか。

  ... | tri> _ neq gt = ?

の neq の型は、( x ≡ y -> ⊥ ) なので、neq ( refl ) は ⊥ になる。そこから、これで生成してやればよいのか。

    ... | tri> _ neq gt = ⊥-elim (neq refl)

う、うーん。なんか、かっこわるいんだけど。こんなものかな。if 文みたいにできないのかな。