Bullet+OpenGLに入門した
levelfour君の記事を読んで物理演算エンジンに興味を持ったのでBulletを学んでみることにした。
OSはUbuntu 13.04
Bulletのインストール
https://code.google.com/p/bullet/downloads/listからbullet-2.82-r2704.tgzをダウンロードして展開し、そのディレクトリに移動して
mkdir bullet-build cd bullet-build cmake ../ -G "Unix Makefiles" make #pacoで管理するため sudo paco -lp 'bullet-2.82-r2704' 'make install'
OpenGL入門
物理演算エンジンは初めて触るけど、Bulletで計算した結果をOpenGLで描画すればいいのだろうと思って、まずOpenGLに入門することにした。
自分はhttp://www.wakayama-u.ac.jp/~tokoi/opengl/libglut.htmlのサンプルプログラムを動かしながらOpenGLを学んだ。
記事自体は古いがWisdomSoft(旧)のOpenGLのページもたぶん参考になると思う。
Bullet
物理エンジンはまったくの初心者なので
物理エンジンの流れ - 雑念プログラマーの日記
で流れを理解した。
Bulletの初期化からシミュレーションまでのもう少し詳しい説明は
myb design :: blog :: cocos3d+Bulletで物理シミュレーション (実装編) #cocos2d_2011_adcal
がわかりやすかった。
HelloWorld
まず手始めにHelloWorldを動かしてみた。
このプログラムは球を自由落下させて高さ(y座標)を標準出力に表示するだけだが、Bulletの基本的なところが分かる(たぶん)。
ヘッダやライブラリのパスの指定にはpkg-configを使うといいらしい(pkg-configとか知らなかった)。
Makefile
hello: hello.cpp g++ `pkg-config --cflags bullet` $^ `pkg-config --libs bullet` -o $@
HelloWorld+OpenGL
次にHelloWorldに書き足して自由落下する球をOpenGLに描画させてみた。
OpenGLのライブラリを使うのでコンパイル時のオプションには-lglut -lGL -lGLUが必要になる。
反発係数の設定
元のプログラムは地面についた後に跳ね返ることなく、止まったままになるので、反発係数を設定することにした。
void btCollisionObject::setRestitution(btScalar rest)
初速度の設定
初速度もつけてみたいと思ったので調べた。
void btRigidBody::setLinearVelocity(const btVector3 &lin_vel)で速度ベクトルのset
void btRigidBody::setAngularVelocity(const btVector3 &ang_vel)で角速度のset
この他に、練習のため球を二つに増やし、高さを変えて鉛直に並べ、球同士をぶつけるプログラムに書き換えてみたりもした。
振り子
落下以外も作りたいので、次は振り子のようなものを作ることにした。
球の動きに制約条件を追加する。
HelloWorldから地面を取り除き、btHingeConstraintを作成してbtDynamicsWorld::addConstraintでDynamicsWorldに追加した。
Coq関係で最近やったこと
期末試験での現実逃避のため最近改めてCoqに触ってみた。ここでは、その内容と自分の理解について簡単にまとめて書き残すが、不正確な内容が含まれているかもしれない。
関数の連続性、数列の収束
微積分の証明をCoqで扱ってみたいなと思ったので、関係しそうなところを調べてみた。
Coqで実数を扱うには
Require Import Coq.Reals.Reals.
をすれば大丈夫だと思われる。
実数に対して四則演算、大小関係などがNotationとして定義されているが、これらは自然数でのものとしっかり区別しなくてはならないし、Scopeに気をつけなくてはならない。その辺についてはたぶんhttp://coq.inria.fr/refman/Reference-Manual014.htmlに書いてある。
例えば
Require Import Coq.Reals.Reals. Goal forall n:nat, INR n < INR (n+1). (*INR:nat->Rは自然数から実数への包含写像*)
としても
Error: In environment n : nat The term "INR n" has type "R" while it is expected to have type "nat".
というエラーが出る。
これは"<"が自然数natにおける不等号と解釈されているせいである。実数Rにおける不等号と解釈させるにはOpen Scopeして
Require Import Coq.Reals.Reals. Open Scope R_scope. Goal forall n:nat, INR n < INR (n+1).
または%Rを後ろにつけて
Require Import Coq.Reals.Reals. Goal forall n:nat, (INR n < INR (n+1))%R.
とする。
逆にOpen Scope R_scopeしているときに
Require Import Coq.Reals.Reals. Open Scope R_scope. Goal forall n:nat, n < n+1.
とnatの不等式を書いてもエラーになるので、%natをつけるなどして対処する。
調べた標準ライブラリ
http://coq.inria.fr/library/Coq.Reals.Raxioms.html
公理的に実数を定義している。
自然数から実数への包含写像INRなどもここで定義されている。
http://coq.inria.fr/stdlib/Coq.Reals.Rdefinitions.html
四則演算、不等号、NotationやInfixなど
http://coq.inria.fr/library/Coq.Reals.Ranalysis1.html
には関数の連続性や微分可能性に関する定義があるようで、
continuity_ptが一点での連続性、continuityが実数全体での連続性、と言う具合に_ptがつくものは点での性質を表す。
http://coq.inria.fr/library/Coq.Reals.Rseries.html
数列の収束Un_cv、単調増加性Un_growingなどが定義されている。
http://coq.inria.fr/library/Coq.Reals.Rfunctions.html
R_dist 距離 絶対値をとるだけ
infinite_sum
sum_f_R0 Nまでのf_nの和
sum_f sからnまでのfの和?
sum_nat_f_O natの数列の和
powerRZ x^n
http://coq.inria.fr/stdlib/Coq.Reals.RIneq.html
実数の不等式
Record posreal
http://coq.inria.fr/library/Coq.Reals.Rbasic_fun.html
Rabs
Rmax
Rmin
タクティック
最近知ったタクティックを簡単にまとめ
Variable
Un_cvの定義においてUnが暗黙のうちに使われているように見えるが、よく見るとSectionの最初にVariable Un : nat -> R.とかかれている。リファレンスマニュアルを読んだ感じだとどうやらSectionの中ではVariableで宣言したUnはUn_cvの定義などにおいて暗黙に使えるようになるが、外からUn_cvを利用するときは明示的に与えなくてはならないらしい。
数列{1/n}が0に収束する事を書きたければ
Goal Un_cv (fun (n:nat) => / (INR n)) 0.
のようにUn_cvにUn:nat->Rに当たるものを与える。
Record
正の実数posrealは次のように定義されている。
Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
これを使うと
Goal forall r:posreal, r > 0.
のように書ける。
Recordの定義のcond_pos : 0 < posは仮定として用いることができる。
Goal forall r:posreal, r > 0. intro. apply cond_pos. Qed.
destruct r.
とかもできるみたい。
{A}+{B}
Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
のように、{A}+{B}が成り立つときに、AかBかで場合分けしてDefinitionを書きたいときがある。
二つの実数のうち小さい方を返すRminを参考にした。
(*Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.*) Definition Rmin (x y:R) : R := match Rle_dec x y with | left _ => x | right _ => y end.
left, rightでパターンマッチさせればいいらしい。
infix
中置記法にする。
http://coq.inria.fr/library/Coq.Reals.Rdefinitions.html
を見れば分かると思う。
NotationもInfixと似たようなことに使われているようだが、たぶんInfix以上のこと、例えば三項演算子のようなものを定義したり、左結合、右結合を指定したり、異なる演算子の間での結合の強さを指定したりできるものだと思う。
info_auto
autoの中で実際何をしているかを表示する。
auto with Hintdb
ヒントデータベースHintdbを利用してautoする。
Hintdbとしては実数関係のヒントデータベースrealなんかがある。
Print HintDb Hintdbで表示できる。
ltac
タクティックをいくつか組み合わせて新しくタクティックを定義するようなものととりあえず理解している。http://coq.inria.fr/refman/Reference-Manual011.htmlに説明されていると思うが、しっかりと読んではいない。
Require Import Coq.Reals.RealsをするとRComputeやRegなどが使えるようになる。
http://coq.inria.fr/refman/Reference-Manual011.htmlに書いてあるタクティックについて
idtac:何もしない/文字列や数字を表示
repeat: 繰り返せるだけ繰り返す
try: error levelを1引く
fail: errorを出す
など
実際に動作を見ればわかりやすいと思う。
Goal forall (P Q:Prop), P/\Q -> Q /\ P. intros. destruct H. split; [apply H0 | apply H]. (*splitでできた二つのゴールの一つ目にapply H0、二つ目にapply H*) Qed. Goal forall (P Q:Prop), P/\Q -> Q /\ P. idtac "message". idtac 1. (*メッセージを表示*) idtac. (*何もしない*) repeat intro. (*繰り返し*) first [apply H | idtac]. first [apply H | split]. (*[]の中のtacticを前から順に適用できるか試し、どれかが適用できれば成功してそこで終了、どれもできなければ失敗*) fail || idtac. try(try (fail 1)). fail 2 || idtac. (*tryや||が一つあるごとにlevelが1ずつ引かれていく?*) (*ただのfailはlevel 0?*) progress idtac. (*進歩があれば成功*) solve [idtac | intuition]. (*証明が完了するまで進めば成功?*)
Ocamlでtacticを書く
qnighyさんの記事CoqのtacticをOCamlで書く話 - 簡潔なQを見て少しやってみようかと
環境はUbuntu 13.04
ocaml-native-compilers libcoq-ocamlをインストール
Make
-R . evar_match evar_match.ml
evar_match.ml
open Pp open Term open Refiner TACTIC EXTEND evar_match | [ "evar_match" constr(x) ] -> [ match kind_of_term x with | Evar _ -> tclIDTAC | _ -> tclFAIL 0 (str "not an evar") ] END
この二つのファイルを作ってから
$ coq_makefile -f Make -o Makefile $ make
を実行。
これでevar_matchというtacticが使えるようになる。
evar_match.v
Declare ML Module "evar_match". Goal forall (x y z : nat), x = y -> y = z -> x = z. intros; eapply trans_eq; match goal with | |- ?a = ?b => evar_match a; idtac a | |- ?a = ?b => evar_match b; idtac b end.
感想
記事が長くなって、途中から書くのが面倒になってしまった。次からは長い記事は分割して書くようにする。
リファレンスマニュアルをあまり読んでいないが、読むべきだなと思った。
mod_rewriteとCGIでServer Side Includesする
mod_rewriteとCGIが使えるけどSSIが(たぶん)使えないサーバーで作業しててふと思いついた
こんなのやりたがる人いるかは怪しいし、くだらないかなと思いつつも書いておく
やったことは単純
.htaccessに、名前が.shtmlで終わるファイルへのアクセスがあった時に、ファイルパスをパラメータにしてCGIを呼び出すように設定する
CGIでSSIの処理を行う
以上
以下に自分が試してみた.htaccessとプログラムを載せる
このプログラムは非常に雑なので、.shtmlファイルに書いてあることならどんなコマンドもexecするし、どのファイルもincludeする
RewriteEngine on RewriteRule ^(.*\.shtml)$ ssi.cgi?path=$1 [L]
ssi.cgi
#!/usr/bin/ruby require 'cgi' def handle_ssi(direc, param, value) case direc when 'include' if param == 'file' #valueのチェックをしていない open(value){|f| f.read } else raise NotImplementedError end when 'exec' if param == 'cmd' #任意のコマンドを実行 IO.popen(value){|io| io.read } else raise NotImplementedError end else raise NotImplementedError end end cgi = CGI.new path = cgi['path'] begin #pathのチェックをしていない file = open(path) output = file.read.gsub(/<!--#(.*?) (.*?)="(.*?)"-->/){|matched| handle_ssi($1, $2, $3) } rescue => e print "Status: 404 Not Found\n" print "Content-Type:text/plain\n\n" p e exit ensure file.close end print "Content-Type:text/html\n\n" print output
最近はrubyで書いてること多いな
Twitter Gem使ってみた
Twitterでオバマ大統領(@BarackObama)があかり大好きbot(@akari_daisuki)をフォローしているとかいう画像を目にした
少し前からRubyのTwitter Gemを使ってみたかったので、Twitter Gemで検証してみた
Twitter Gemのインストール
Twitter Gem使ったことないのでインストールから
>gem install twitter
すると
Please update your PATH to include build tools or download the DevKit
from 'http://rubyinstaller.org/downloads' and follow the instructions
at 'http://github.com/oneclick/rubyinstaller/wiki/Development-Kit'
とエラーが出るので
http://github.com/oneclick/rubyinstaller/wiki/Development-Kit
にしたがってDevKitをインストールする
行ったことは
>cd (Devkitを展開したパス) >ruby dk.rb init (config.ymlの確認をする) >ruby dk.rb install
うまくいったようなので再度
>gem install twitter
インストール終了
require 'twitter'
でtrueが返ってくることを確認
dev.twitter.comに登録
次にconsumer_key, consumer_secret, access_token, access_token_secretを取得する
https://dev.twitter.com/
へ行って、自分のアカウントで適当に登録する
この辺の説明は省略
検証プログラム
require 'twitter' #各自取得したものに書き換える client = Twitter::REST::Client.new do |config| config.consumer_key = "YOUR_CONSUMER_KEY" config.consumer_secret = "YOUR_CONSUMER_SECRET" config.access_token = "YOUR_ACCESS_TOKEN" config.access_token_secret = "YOUR_ACCESS_TOKEN_SECRET" end obama = client.user("BarackObama") akari = client.user("akari_daisuki") p client.friendship?(obama, akari)
実行してみるとclient.user("BarackObama")を実行したときに
Twitter::Error: SSL_connect returned=1 errno=0 state=SSLv3 read server certificate B: certificate verify failed
というエラーが出た
SSLはよくわからないが、環境変数SSL_CERT_FILEに証明書へのパスを設定するとエラーが出なくなった
http://curl.haxx.se/ca/cacert.pem
から証明書をダウンロードして
>set SSL_CERT_FILE=(cacert.pemへのパス)
とする
先ほどのプログラムを実行すると
false
その他
最近Twitter Gemの仕様変更があったようで、調べているときに自分の環境では動かないコードがとても多くて大変だった
client = Twitter::REST::Client.new do |config|
が
Twitter.configure do |config|
となっているところがあったり、
config.oauth_token = ...
では警告が出るので
config.access_token = ...
と書き換えたりした
最初からRubyDoc.infoを参照すればよかった