Just Do Live このページをアンテナに追加 RSSフィード

2222-02-22 ブログ移転しました このエントリーを含むブックマーク このエントリーのブックマークコメント

2014-11-24

ヤフオクAPIラッパーを作ってgemに登録してみた

ここ最近

暇つぶしで、嫁のやってる事を楽にするための超嫁得Webサービスrailsで立ち上げて遊んでました。

yahooが提供しているヤフオクapiをごにょごにょしていい感じに表示させるWebサービス(ユーザーは嫁のみ)なんですが

http://developer.yahoo.co.jp/yconnect/

このyconnectを使ってoauthで認証する系のAPIの使い方が分からなくて手こずってました。

omniauthってので認証してaccess tokenをゲットするまではある程度すんなり出来たけど、その先のtokenを使ってどうやってAPI叩けばいいの?ってのに嵌りました。

認証が必要ない場合のAPIを叩くgemはあったんですが、認証が必要な場合のが無かったので自分で作ってついでにgemとして登録してみました。

https://rubygems.org/gems/yahoojp-auction-api

ただのラッパーなんだけど慣れてないとこんな情報あるだけで助かるんですよ。

2012-12-09 配列の逆順のユニーク性

[] 配列(リスト)の逆順に関する性質の証明

https://gist.github.com/4243787

最近、プログラマの採用面接で解かす問題集みたいな本が出て

その中に「ある配列がユニークであるかどうかを示すコードを書け」という問いがあり、Coqで書いてみました。

下記のようなコードになるんだけどついでに配列を逆にした場合も結果は同じであろうという直感を証明しようと思ったらすごく嵌りました。

Require Import Bool.
Require Import Lists.List.
Require Import String.
Require Import Ascii.

Definition eqc (x y : ascii) : bool :=
  if ascii_dec x y
    then true
    else false.

Fixpoint list_of_string (s : string) : list ascii :=
  match s with
  | EmptyString => nil
  | String c s => c :: (list_of_string s)
  end.

Fixpoint contain (c : ascii) (chars : list ascii) : bool :=
  match chars with
    | nil => false
    | x :: xs =>
      if eqc x c then
        true
      else
        contain c xs
  end.

Fixpoint snoc (l: list ascii) (v: ascii) : list ascii :=
  match l with
  | nil => v :: nil
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev (l: list ascii) : list ascii :=
  match l with
  | nil => nil
  | h :: t => snoc (rev t) h
  end.

Fixpoint uniq_i (chars : list ascii) : bool :=
  match chars with
    | nil => true
    | x :: xs => 
      if contain x xs
        then false
        else uniq_i xs
  end.

Definition uniq (str : string) : bool :=
  uniq_i (list_of_string str).

配列の先頭に付与する場合は帰納法で素直に解けるんですが、appendする場合は素直にいかない。

パターンマッチさせる場合 x::xsのように先頭でマッチさせるような関数を書いているのが原因だけど、配列の後尾から帰納的証明が行えるような機能が必要に思う。

証明は配列にappendした際の性質 in_app_or_congtain がキモ。

(* 配列に要素をappendした際の重要な補題 rev系の証明では必須 *)
Lemma in_app_or_contain:
  forall (l : list ascii) (a b : ascii),
    contain a (snoc l b) = (contain a l) || eqc b a.
Proof.
  intros l b a.
  induction l.
  simpl.
  case (eqc a b).
  reflexivity.
  reflexivity.
  simpl.
  rewrite -> IHl.
  case (eqc a0 b).
  reflexivity.
  reflexivity.
Qed.

証明の全容は

https://gist.github.com/4243787

にあります。

最後の定理が目的のものです。

2011-09-13 [Coq] 存在の証明 1 このエントリーを含むブックマーク このエントリーのブックマークコメント

Coqインストールしたので

http://d.hatena.ne.jp/qnighy/20101220/1292829222

この辺を参考に勉強中です。

ついでに自分で命題を考えて証明してみた。


命題は forall (x : nat), x > 1 -> x < x * x. というもの。


こんなもの直感的だろ!

といいたい所ですが、論理学の世界では公理系から演繹(証明)出来ないものは全て不定な存在です。


戦略的にはSearchPatternで (_ < _ * _) を調べ見つけた

mult_lt_compat_r: forall n m p : nat, n < m -> 0 < p -> n * p < m * p

の定理を使う方針で証明していきます。

pをx、nを1、mをxとすると仮定から p n mはnatであり、n < mとなるので定理より命題は成り立ちます。

が、 x < x * x と 1 * x < x * xが同値な命題かどうかを証明しなければなりません。

要は x = 1 * xを証明する必要があります。

証明の途中で仮定化したい補題が発生した場合はassert tacticsでがしがし仮定化し証明していきます。


では証明

Lemma square_is_big:
 forall (x:nat), x > 1 -> x < x*x.
Proof.
 intros.

 (* x = x * 1 の証明 *)
 assert (G: x = x * 1).
 assert (G1: x * O = O).
 apply (mult_0_r x).
 assert (G2: x = x + O).
 apply plus_n_O.
 rewrite G2 at 1.
 assert (G3: x + O = O + x).
 apply plus_comm.
 rewrite G3.
 rewrite <-G1 at 1.
 apply (mult_n_Sm x O).

 (* x < x * x を 1 * x < x * x に変換 *)
 rewrite G at 1.
 assert (G4: x * 1 = 1 * x).
 apply mult_comm.
 rewrite G4.

 (* x > 1 は仮定に存在しているので,後は仮定にx > 0が必要なので証明 *)
 assert (G5: x > 0).
 assert (G6: 1 > 0).
 apply neq_O_lt.
 apply O_S.
 apply (gt_trans x 1 O).
 exact H.
 exact G6.

 (* 条件が整ったので最後の仕上げ *)
 apply mult_lt_compat_r.
 exact H.
 exact G5.
Qed.

x = x * 1とか 1 > 0とかの証明が意外に難しかった。

まぁただ欲しい仮定はassertでどんどん証明していくという事を掴めればなんとかなる。

普通に数学の命題を証明する時と同じ思考回路を使うんだけど SearchPatternで公理、定理を検索出来るからかなり便利。

2011-03-24

VPSRailsでサービス開発

404 Not Found

 先週の3連休、私は家にひきこもって酒を飲みながらemacs誰得的な記事を書きつつVPSで遊んでいました。

そこで作ったtwitterを利用したサービスが出来るまでの流れをざっくり公開しようかと思います。

 作ったサービスは http://stkr.dip.jp/maps 上で公開してます。

twitter idを入力するとI'm atアプリ等でtweetした文書を取得し、だいたいの場所をGoogle map上にプロットします。

このくらいであれば1日もあれば一から作れます(酒があれば)


VPSの登録

世の中には様々なVPSサービスがありますが、今回使用したのはServersMan@VPSというサービスです。

このサービスは月額490円でメモリ256MB(MAX768MB)でHDDが10GBほどのリソースが使え、

root権限もあるのである程度遊ぶには十分な環境と言えます。

このサービスが出た直後は登録するのに1ヶ月待ちとかだったのですが、今なら登録直後に使用出来るのもいいですね。

http://dream.jp/vps/index.html

へ行きお好きなプランを選んで登録してみてください。

登録したメールアドレスに環境情報が送られてきます。

開発環境の設定

rootユーザーで作業するのは何かと危険なのでまずはユーザーを作りましょう。

 % ssh -P 3843 root@xx.xx.xx.xx

ログインし、useraddコマンドでユーザーを作成します。

作成したユーザーを以下「user」とします。

次にsshまわりの環境を整えます。

ServersManではsshのポートが標準の22から3843に変わっているので普通にログインしようとしたら上記のように打ち込む必要があるので非常に面倒です。

そこで ローカル(VPS上ではない)の~/.ssh/config ファイルに以下のような設定をします。

Host	vps
  HostName  xx.xx.xx.xx
  Port  3843
  User	user

HostNameはServerManから与えられた固定IPアドレス、Portがsshのポート番号で、UserがログインユーザーIDです。

この設定をしておくことで

 % ssh vps

と打つだけで済むようになります。

emacsを使っている方はtrampというリモートサーバのファイルを編集出来る機能を設定しておきましょう。

 % wget http://ftp.gnu.org/gnu/tramp/tramp-2.2.0.tar.gz
 % tar zxvf tramp-2.2.0.tar.gz
 % ./configure --with-contrib
 % make
 % sudo make install

.emacs.elに以下を追加

(require 'tramp)
(setq tramp-shell-prompt-pattern "^.*[#$%>] *")
(setq tramp-default-method "ssh")

設定終了後はemacs上で

 C-x C-f /vps:

と入力しましょう。パスワードの入力をするとVPS上のファイルを編集出来るようになります。

Ruby on Railsインストール&設定

ServerManでRailsが動くようになるまで以下のアプリ群をインストールしてください。

以下の作業はすべてrootで行います。

コンパイラ関連
 # yum install gcc glibc gcc-c++
Ruby関連
 # yum install readline-devel openssl-devel zlib-devel 
 # wget ftp://ftp.ruby-lang.org/pub/ruby/1.8/ruby-1.8.7-p299.tar.gz
 # tar xvzf ruby-1.8.7-p299.tar.gz
 # cd ruby-1.8.7-p299
 # ./configure --prefix=/opt/ruby-1.8.7-p299
 # make
 # make install 
 # ln -snf /opt/ruby-1.8.7-p299/bin/ruby /usr/local/bin/ruby
 # ln -snf /opt/ruby-1.8.7-p299/bin/rake /usr/local/bin/rake
 # ln -snf /opt/ruby-1.8.7-p299/bin/irb /usr/local/bin/irb
mysql関連
 # yum install mysql-server
 # yum install mysql-devel 
RubyGems関連
 # wget http://rubyforge.org/frs/download.php/70696/rubygems-1.3.7.tgz
 # tar xvzf rubygems-1.3.7.tgz 
 # cd rubygems-1.3.7
 # ruby setup.rb
 # ln -snf /opt/ruby-1.8.7-p299/bin/gem /usr/local/bin/gem
Rails関連
 # gem install rails
 # ln -snf /opt/ruby-1.8.7-p299/bin/rails /usr/local/bin/rails
sqlite関連
 # wget http://www.sqlite.org/sqlite-autoconf-3070500.tar.gz
 # tar xvzf sqlite-autoconf-3070500.tar.gz
 # cd sqlite-autoconf-3070500
 # ./configure
 # make
 # make install
 # gem install sqlite3-ruby mysql dbi dbd-mysql
passenger関連 (railsapache経由で使用するため)
 # gem install passenger
 # /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5/bin/passenger-install-apache2-module
railsでプロジェクトを作成する
 # cd /var/www/html
 # rails new stokker
 # cd stokker
 # rails generate scaffold maps
 # rake db:migrate
rails ルーティングの定義 (stokker/config/routes.rb)
  match 'maps/hoge' => 'maps#hoge'
  match 'maps/hoge/:twitter_id' => 'maps#hoge'

scaffoldで作ったmapsコントローラに新しいメソッドを定義した場合、ルーティングが通って無いのでそのメソッドを使用したリンク等をクリックするとエラーとなります。

上記のように適宜ルーティング定義を追加します。


apacheの設定

ServerManはデフォルトApacheが入っているのでconfの設定だけをします。

/etc/httpd/conf/httpd.conf の以下の行のコメントアウトを外します。

NameVirtualHost *:80

起動ユーザーとグループはデフォルトだとdaemonですが、適切なユーザーに変えておきます。

User user
Group user

/etc/httpd/conf.d/stokker.confファイルを以下のように作成します。

<VirtualHost *:80>
  DocumentRoot /var/www/html/stokker/public
  ServerName stkr.dip.jp
  RailsEnv development
  <Directory /var/www/html/stokker/public>
     AllowOverride none
     Options -MultiViews
     Order allow,deny
     Allow from all
  </Directory>
</VirtualHost>

DocumentRootはrailsでプロジェクトを作った際に出来るpublicディレクトリを指定します。


/etc/httpd/conf.d/passenger.confファイルを以下のように作成します。

LoadModule passenger_module /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5/ext/apache2/mod_passenger.so
PassengerRoot /opt/ruby-1.8.7-p299/lib/ruby/gems/1.8/gems/passenger-3.0.5
PassengerRuby /opt/ruby-1.8.7-p299/bin/ruby

apache再起動します。

http://xx.xx.xx.xx/

railsが生成した画面が表示されている事を確認してください。


Google maps api

http://code.google.com/intl/ja/apis/maps/signup.html

ここでgoogle maps apiを使用するドメインを登録しKEYを取得します。

取得したKEYは以下のように使用します。

<script src="http://maps.google.com/maps?file=api&amp;v=2&amp;
 sensor=true&amp;key=XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX"
 type="text/javascript">
</script> 

マップは

 <div id="map_canvas" style="width: 728px; height: 400px"></div>

というdiv要素上に表示されます。


twitter4r

twitterの発言を取得するのにtwitter4rを使用しました。

 % sudo gem install twitter4r

twitter4rをインストールしたら使用するrubyのファイルで以下のように宣言しておきます。

require "rubygems"
gem "twitter4r"
require "twitter"

公開発言を取得するだけであれば以下のような簡易なコードで取得出来ます。

    @MAX_COUNT = 500
    @twitterid = ...
    last_month = Time.now - 60*60*24*30
    tw_client = Twitter::Client.new
    tw_client.timeline_for(:user, :id => @twitterid, :count => @MAX_COUNT).each do |status|
      created = status.created_at
      if created > last_month then
        ...
      end
    end

その他

ロゴ

twitter風のロゴは http://www.twitlogo.com/ で作成しました。

Connection: close