finch-0.9.2 の body と bodyOption のバグ

finagle の finch を触っています。 現時点での最新版は0.9.2なのですが、0.9.2には RequestReaders.bodyOption: RequestReader[Option[String]] とこれを使っている RequestReaders.body: RequestReader[String] にバグがあります。0.9.3-SNAPSHOT では直っ…

dotfiles をアップデートした

前回 dotfiles を大幅にアップデートしたのがちょうど2013年の10月だったので、約2年ぶりの更新です。 以下変えた部分。 Emacs el-get をアップデートした init-loader を使うようにしたい el-get-lock を使うようにした 新しいマシンに .emacs.d を持ってく…

crates.io のパッケージページで Reverse Dependencies を表示する Chrome 拡張

最近 Rust に再入門しています。 言語初心者によくある問題として、良い (信頼できる) ライブラリがどれかわからないというものがあります。 Rust の中央パッケージリポジトリである crates.io は各パッケージのダウンロード数が書かれていて、 良さそうなラ…

mbed で PS2 を操作するやつを作った

表題のとおり、mbed という自分のような初心者にも優しいマイコンで PS2 を操作するなにかを、研究室の同期3人で作りました。 これは個人の日記ですのであとで3人でもう少し詳しい解説記事を書くかもしれませんが、とりあえず簡単に言うと、 こんなので、 こ…

ITSP PBL で作ったもの・使った技術やツール

PBLというチーム開発の授業でうちのチームはこんなの作ったり使ったりしたよという記事です。 成果発表会や展覧会では技術的なことの説明はほとんどしなかったように思うので、せっかくなので公開しておきます。 来年以降この授業を取る人の参考になればと思…

(第二回)更新を楽しみにしているWeb漫画10

個人的に更新を楽しみにしているWeb漫画10の2回目です。前回と被っているものもあります。 Web漫画とは言えないものもありますが、とりあえず2015年2月3日現在Webで読めればよしとします。 (順不同) NOBELU-演- 一番楽しみにしてる 宇宙大恋愛 マイアニマル …

Keycastr と Gifzo が便利だった

utop のバグっぽいものを見つけたので、それを issue に書くために GIF のツールを使ってみた。 keycastr/keycastr · GitHub Gifzo - 宇宙一簡単なスクリーンキャスト共有 Keycastr はキーストロークを画面に表示してくれるツールで、Gifzo はスクリーンショ…

Frama-C のインストールメモ

環境: OSX Yosemite パッケージマネージャ: homebrew, homebrew-cask, opam コンパイラ: ocaml4.01.0+clang-fix brew cask install xquartz これを入れないと pkg-config でコケる (X が入ってないというエラーはでない) 普通に XQuartz.dmg を入れた状態だ…

CodinGame をやってみた

プログラミングの勉強を本気でWebゲーム化した「CodinGame」が時間泥棒確定! 面白そうなのでやってみました。 いくつか解いてみた感想 ただのプログラミングコンテストの問題 標準入力から情報を受け取って、なんらかの計算をして標準出力に計算結果を出力…

チャットでも証明が書きたい

チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。 こんなかんじ。 導入方法 (hubot 自体の導入方法については他の記事に任せます) 適当なサーバに Coq 8.4 以上をインストールします。 …

なつやすみのにっき

夏休みです。 Coq Summer School 8月の終わりに NII Shonan School on Coq に行ってきました。 一週間みっちりCoq漬けでした。楽しかった。でも英語ができればもっと……。 夏ゼミ Coq合宿が終わった3日後から2泊3日の研究室合宿がありました。千葉の館山に行…

homebrew で MathComp を入れる

追記 2015/11/11 今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。 opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 …

coqtop -emacs のプロンプト

プロンプトについて ProofGeneral や、coqtop-vim は裏で coqtop -emacs というコマンドを実行して、そこと通信しています。 coqtop -emacs を実行すると、標準エラー出力に <prompt>Coq < 1 || 0 < </prompt> というのが出てきます。ここを見ると現在の coqtop の状態がわか…

can't load .so/.DLL for: というエラー

下のようなエラーが出たとき <command line>: can't load .so/.DLL for: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib (dlopen(/Users/amutake/work/jype/jype-doc/. cabal-sandbox/lib/x86_64-</command>…

cabal-install の bootstrap.sh で module ‘foobar-0.0.0:Main’ is defined in multiple files ...

cabal-install の bootstrap.sh で module ‘stm-2.4.3:Main’ is defined in multiple files: ... みたいなエラーが出てコケたときは、 % cd stm-2.4.3 % ./Setup install % cd ../ % ./bootstrap.sh とやればよい。仕組みは不明。

$GOPATH

golang の GOPATH について。 昨日まで GOPATH で指定したディレクトリは、Haskell の .cabal ディレクトリみたいにパッケージがインストールされるだけの場所だと思ってたけど、自分でコードを書くときもこの中で作業をするということを知った。 研究室の先…

更新を楽しみにしているWeb漫画10

個人的に更新を楽しみにしているWeb漫画10選です。順不同。 パペラキュウ All You Need Is Kill 市場クロガネは稼ぎたい はるこ少女期 徒然チルドレン 働かないふたり 俺とヒーローと魔法少女 T.Yめもり~ず アクアの魔法 裏ジャック

Why3 で遊んでみた

Why3 で遊んでみたのでメモ.インストールで手間取った.環境は Mac OS X 10.9.1 です. Why3 のインストール ※この方法は Mac OS X かつ Homebrew 専用です.Linux や MacPorts でのインストールはわかりません. ソースからは面倒なので,OCaml のパッケー…

Idris 0.9.10

idris-0.9.10 がリリースされたのでちょっと触ってみた。http://www.idris-lang.org/idris-0-9-10-released/ 証明付き型クラス 以前の idris では下のツイートのようなことはできなかったのですが、できるようになっていました。 型クラスを実装するときに、…

idris-mode for Vim/Emacs

最近巷で話題の Idris (依存型を持つ純粋関数型言語)ですが、この Idris にも vim と emacs のプラグインがあります。 idris-vim vim の idris-mode です。Idris のメイン開発者である Edwin Brady さんも開発に加わっています。 リポジトリ Edwin Brady さ…

OS X Mavericks にしたら gcc を使う Haskell パッケージがビルドできなくなった件

参照: http://cp.reddit.com/r/haskell/comments/1ozukp/anyone_running_ghc_763_on_osx_mavericks/ Xcode 5 が clang を使っていて gcc4.2 を提供しなくなったせいらしい。 clang に対応している GHC7.8 が出るまで待つか GHC HEAD を使えばいいらしいけど…