2014/06/10

Agda を 2.4.0 にする

2014/06/05 に Agda 2.4.0 が Release されたみたいです。

けれど、Standard Library 0.7 の Release Note を見ると
2013–01–29: Version 0.7. README. Tested with Agda 2.3.2, Agda 2.3.2.1 and Agda 2.3.2.2. 
とのこと。Agda2.4 に対応してない。
ということで Standard Library を使うコードを実行してみると途中でエラー吐かれました。

なのでとりあえず Repository を直接もってくる。
$ git clone https://github.com/agda/agda-stdlib.git
それで agda2-include-dirs が通ってるところに配置。

私は
(setq agda2-include-dirs (mapcar (lambda (path) (expand-file-name path)) (file-expand-wildcards "~/Library/Agda2/*")))
とか設定していて、 ~/Library/Agda2 の下を全部 import できるようにしてます。

なので
$ cd ~/Library/Agda2
$ ln -s $HOME/files/build/agda/agda-stdlib/src `pwd`/agda-stdlib
とかしておしまい。

そして Standard Library なコードを実行すると通りました。めでたしめでたし。

2014/05/24

Open Source Conference 2014 Okinawa に行ってきた

オープンソースカンファレンス に行ってきました。

今年は沖縄が10回目らしいのだったり、最近100回達成したり、10年目だったりの記念会だたっぽいです。

参加者的には、噂の Eject コマンドユーザ会 を見られたりとか、トートバッグが当たったりとかな感じでした。


ちなみにあんまり参加者側の印象が無いのはブースで参加していたりセミナーで発表していたりしたからで。

ブースでは研究室の成果物である TreeVNC と ie-virsh を展示。
TreeVNC は大量のユーザが繋がっても重くなりづらく、画面配信する画面切り替えを接続を切ることなくできる、というもの。
ie-virsh は学生が自分のアカウントのみで自分の VM を起動したり操作できる、という学科向けマルチユーザ virsh です。
詳しくはきっと中の人達がどこかにまとめてくれているでしょう。


セミナーでは Agda入門 ということで Agda という言語の入門をしてきました。
加法の交換法則の x + y == y + x を証明してきました。
入門というのには大変なレベルでいろいろな要素が入っていて

  • Curry-Howard Isomorphism
    • プログラムで証明を扱う上でこういう理論をベースにしてます、と言わなきゃ
  • Peano Arithmetic
    • 加法するから自然数定義しなきゃ
  • Equivalence
    • 等価性証明するから定義しなきゃ
  • Reasoning
    • 式変形に使うし説明しなきゃ
とかとかで割と聞いたこと無いようなもの大盛りでお送りしました。


発表の感想としては割と反応難しいよなー、といった感じ。というか私も難しいよなーとか思っていながら。

目に見えて分かるくらい貢献するようなこういうことができます、ってくらい言えた方がやっぱり見た目的にも分かりやすさ的にも良いはず。
ただそういうネタが見つかんなかったのとそれが書けるかなー、とかやってる流れでとりあえず 1 + 1 = 2 な路線で行ってみようか、という感じでした。
うーん。どうしていこうかなー。

2014/05/12

rbenv と readline でゴニョゴニョした話

Ruby 2.1.1 を rbenv で入れようとするとビルドがコケる。

brew な readline が 6.3.3 にいつの間にか上がってて、それだとマズいらしい

6.2.4 とかだと大丈夫らしいので、一旦  checkout してインストールして brew switch とか。
$ brew versions readline
$ pushd /usrl/local
$ git checkout 0181c8a Library/Formula/readline.rb
$ brew install readline
$ brew switch readline 6.2.4
$ git checkout master
$ RUBY_CONFIGURE_OPTS="--enable-shared" rbenv install 2.1.1
そうすれば2.1.1が入りました。

と思ったら brew 側の readline が 6.3.5 に上がってた。
のと、Rubyも2.1.2 が出てた
ということで試してみる
$ brew install readline
$ brew switch readline 6.3.5
$ RUBY_CONFIGURE_OPTS="--enable-shared" rbenv install 2.1.1
$ RUBY_CONFIGURE_OPTS="--enable-shared" rbenv install 2.1.2
なんか素直に2.1.1も2.1.2も入った。
brew な readline 入ってるとその辺気にしないといけなさそうなのかな。

とりあえず 6.3.5 だと何ら問題は無いらしい。

2014/04/27

gcc-4.8 な感じで Agda を入れる

brew で haskell-platform を入れて、その cabal 経由で Agda を入れてたんですが、いつかの update で apple-gcc42 が formula から消えてしまった様子。

ghc は apple-gcc42 に依存してたみたいだけれど、いつの間にか依存が
mpfr libmpc isl cloog gcc
になってる。

なので apple-gcc42 を消して gcc とかを入れる。

ghcを入れて、 haskell-platform を入れようとすると怒られる。
解決法は
https://github.com/Homebrew/homebrew/issues/28654
らしい。

ってなわけで
$ brew install ghc
$ brew install haskell-platform --cc=/usr/local/bin/gcc-4.8
とかで haskell-platform が入りました。


あとは PATH に $HOME/.cabal を追加して
$ cabal update
$ cabal install cabal-install
$ cabal install agda
とかすれば素直に Agda まで入りました。

2014/04/26

新入生歓迎LT祭り 2014 へ行ってきた

新入生歓迎LT祭り 2014 へ行ってきました。

今回の発表者は26人とのことで結構多い感。とはいえ過去も20数人くらいは発表していた様子。
さすがに見知った顔が個人の趣味なりなんなりを発表するとなるとバリエーションも多いなー、とか。
知ってる身内だけー、みたいな雰囲気はあるかもしれないけれど、こういう学科なんだよー、ってことを感じとってもらえたのなら幸いかも?
逆に、既にある程度の人達がオーラ作っちゃってる感もあるので新入生側からは入りづらいとかになってないかは気になるんだけれど、その辺はどうだったのだろう。
まーお祭りだし良いか。


今回は たまにはどこかへ。 (リンク先pdf) ということでイベントや勉強会へのお誘いをLTで。

話で出した okrk01 とかはとても規模が大きくて、内容もさることながら、その後の打ち上げではruby会議を開催するような人達がでごろごろいたりしたのが印象的。
なんというかそういうところでも「学生が少ない」とかって言ってたりするので、きっと大歓迎されますよー、とか。

ともあれ、こういうイベントは沖縄にもあって、参加してみるのも良いんじゃないか、というお誘いでした。
近場だと ie-developers として勉強会とかやる予定ですし。次はVimかなー。
誰かの選択肢を増やすことになれば幸い。


んで、関連するLTと言えば Yutaka_Kinjyoさん意識の高い内容 でしょうか。
このLTを聞いてわくわくしてどこかへ行きたくなったらどっか行っちゃうのも手です。
んで、好きなことをしたい、勉強したい、って時にそういうことが言えたりとか聞けたりとかする場もあるんですよー、とかって流れでイベント行って欲しいかもですね。

さらに関連と言えば yotaさん のLT。
「いきなりどこか行けとかって酷じゃない?」というのは割と言いえて妙。
たしかに知らん者とか人ばかりのところに突っこんでいけ、ってのも鬼だよなー、とか。
そういう意味でも私の発表は、やりたいことの選択肢の1つにしてみたらどうだろう、くらいの主張が良いのかもしれない。
あーしろこうしろ、だと結構しんどいかもなので。

今日の沢山のLTを聞いて、あ、これ気になる、とかでやってみるくらいで良いんじゃないかと。

あと私のところに殴り込んでくるなら TaPL とかで殴り合えば良いのかな。別に Haskell とか Category とかでも良いですけれど。その辺まだ良く分かってませんし。
あと、これらの単語良く分かんなかったら Ruby なり Vim なり git なりを布教くらいはするかもしれません。

ちなみに、私にリプライを送ってきた
@masamasa_massa さん, @rumagishi さん, @mitsumitsu10 さん, @MOSSEA_Re さん, @EIJU1o1 さん, @rumagishi さん, @kie_Udongein さん, @zirmele さん, @_simanman さん, @nekonekomeiko さん, @japan12345 さん, @kemikaruB1 さん, @ONAGA_tattsu さん, @Momo060849 さん, @fgpglv0816ss さん, @OZmku さん, @jzmob4 さん, @e125710 さん, @yshtk_ さん, @innparusu さん, @yu12com さん, @utah_pcxgs さん, @_simanman さん, @sister_clown さん, @kkz_interface さん
はたぶんVim勉強会するときにメッセージぶん投げます。
これで人数20は確保かなー。


ともあれ入学おめでとうございます + 良い大学生活を、ということで。