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

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

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

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

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

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

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

下のようなエラーが出たとき <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 ‘stm-2.4.3:Main’ is defined in multiple files: ... みたいなエラーが出てコケたときは、 % cd stm-2.4.3 % ./Setup install % cd ../ % ./bootstrap.sh とやればよい。仕組みは不明。

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

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

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