『マルレク第七回テーマ：「型の理論」と証明支援システム -- COQの世界 』に行ってきました

お勉強

ひさしぶりに頭がグルグルする講演(勉強会)に行ってきました。

講演の概要はここ の講演概要を読んで下さい。資料は ここ からダウンロードできます。

感想

  • 万年Haskell弱者である私には、なぜHaskellerが 型 型 型 型 いうのかが理解出来なかったのですが、今回学んだ(ちゃんと理解は出来てませんが・・・) "Propositions as Types"、 "Proofs as Terms" (PAT) から来ているのだということで、腑に落ちた気がします(まだ気がしますレベルですが)
  • Homotopy Type Theoryという最新の型の論理の証明は、なんと GitHub に Coqで書かれた証明がアップされていて検証・討議できるようになっています！ プログラマーのみなさんの大好きな Pull Requestも出せます(現在0ですが、Issueはたくさん出てますね)
  • Coq は自動的に証明してくれるようなソフトではなくて、証明を手伝ってくれるソフトです。証明のやり方などは人間が指示、ようするにプログラムのような物でを書く事で、ソフトが後の単純作業をやってくれるものです。
    • また、いくつもの 演繹や定理(tactic)のデータベースを持っていて、それを検索し利用できます。
    • ちなみに通常のプログラミング言語のような使い方も出来ますが、いろいろな部分が公理からの演繹で行われるので、速度とかは実用的ではないです。1 + 10000 を計算させると Stack overflow Warningが出ます(10000 + 1 では出ません)
    • ダウンロードやチュートリアルは http://coq.inria.fr 。日本語の入門が ここ にありました、ありがたや、ありがたや。
    • 日々の仕事に嫌気がさした時に、Coqで遊ぶと仙人の気分に浸れるかもしれません :-)

安全にクリーンインストールでMac OSのアップデートを行う方法

Mac

OSのアップデートを行うには、従来のデータやプログラムを残したままアップデートする方法と、ディスクを消去して新規にインストールするクリーンインストールがあります。私はクリーンインストールが好きです、理由は

  • アプリやOSが使っていたテンポラリーなファイル等がリセットされる
  • 不要なプログラムやデータを掃除できる
  • OSが安定に動作する(かも)

ただし、クリーンインストールではディスクを消去してしまうのでバックアップから情報を戻しますが、まれにファイル単位では復旧できな情報もあったりするので注意が必要です。
そこで、私が行ってる安全にクリーンインストールでMac OSのアップデートを行う方法を書きます。


用意するもの

  • USBメモリー： Mavericksの場合は 8Gbyte以上の容量が必要です
  • 現在使っているMacの内蔵SSD/HDDと同等の大きさの外部HDD： ブート可能な内蔵SSD/HDDのコピーを作ります。容量は正確には内蔵SSD/HDDの使用領域の容量より少し大きい外付けのHDD(SSD)です。USB接続で良いです(もちろんThunderboltなら作業が早く済むと思います)。

注： 外部ディスクに2つのパーティションを作って、Mavericksインストルー用とコピー用に使うことも出来ます。

手順

1. 新OSのインストールUSBを作る

ダウンロードした、Mavericksはそのままではクリーンインストール出来ないので、ここの手順を参考にMavericksをインストール出来るUSBメモリーを作ってください。

2. TimeMatchin等のバックアップ

外付けHDDにコピーを作りますが、そこで間違うことも考えられるので、TimeMatchin等でバックアップを作っておいてください。

3. 外部HDDへのフルコピー
  1. Macをshutdownします
  2. Mavericksインストール用USB、 外付けHDDを接続
  3. option(alt)キーを押しながら電源ON、ブートデバイスとしてインストール用USBを選択
  4. インストール画面が起動されたらUnilitiesメニューからTerminalを選択
  5. ターミナル上で各ディスクのデバイス名を確認し、asrコマンドでディスクをコピー
$ df

# dfの表示から、sourceになる内蔵SSD/HDDのFilesystem名 (/dev/diskNNN)と外付けHDDのFilesystem名 (/dev/diskMMM) 
# を調べる

$ asr restore --source /dev/diskNNN --target /dev/diskMMM --erase --noverify

ディスク容量によってはかなり時間がかかります。私のMac(SSD 512Gbyte)をUSB2の外部ディスクにコピーした時には 6時間かかりました。

4. 外部HDDからのブート確認
  1. Macをshutdownします
  2. option(alt)キーを押しながら電源ON、外付けHDDを選択
  3. 旧OSのMacが起動される事を確認
  4. Macをshutdown
  5. 外付けHDDを外します
5. 新OSのクリーンインストール
  1. option(alt)キーを押しながら電源ON、インストール用USBを選択
  2. インストール画面が起動されたらDisk Unilityを使い、内蔵SSD/HDDを消去(Format)
  3. Disk Unilityを終了
  4. インストール画面からMavericksのインストールを実行
6. 外部HDDから必要なファイルのコピー
  1. 外付けHDDを接続し、必要なファイル・フォルダー等をコピー
万が一の時は、外部HDDから旧OSをブート

一部の情報は、アプリを起動しないと書き出せないものもあります。新OSになってからそのような情報に気がついた場合には、外付けHDDからブートし必要な情報を内蔵SSD/HDDに書き出します。
また、新OSでは上手く動作しないソフトがあった場合にも、旧OSが使えるので安心です :-)

私も今回のアップデートで、iOS開発用の秘密キーをファイルに書き出すのを忘れていたのですが、外部HDDからブートし無事に秘密キーを書き出せました(キーチェインのファイルをコピーすればだいじょうぶという説もありますが)。

Mavericks(Mac OS X 10.9)にRuby1.8.7をインストールする方法

Ruby

今さら最新のMac OS に Ruby 1.8.7 をインストールする人は少ないかもしれませんが、もろもろの理由でRuby 1.8.7が必要なのでインストールしてみました。

特に新しい情報はありませんが、brew, rbenv を使ってインストールしました。

% brew install apple-gcc42
% CC=/usr/local/bin/gcc-4.2 RUBY_CONFIGURE_OPTS="--without-tcl --without-tk" rbenv install 1.8.7-p374
% rbenv shell 1.8.7-p374

RubyWorld Conference 2013 に参加しました

イベント

RubyWorld Conference 2013に参加し、教育関連の発表してきました。発表の方は 会社Blog を見て下さい。

http://www.rubyworld-conf.org/images/masthead.jpg

初めて RubyWorld Conference に参加した感想を書いてみます。

Matzは松江生まれでないという衝撃の事実を知る！

Rubyの作者、まつもとゆきひろさん は島根県・松江市に生まれ育ち、そしてUターンし松江市に住んでいるんだと勝手に思っていました。だからこそ松江市、島根県が Ruby に 大幅にコミットしているのだと。

初めて行った松江市の風景、宍道湖へと流れる穏やかな川が流れや広々とした風景が Ruby言語に与えた影響があるのかなぁ〜 と思いながら控え室で まつもとさんに 聞いたところ、母方の家系は島根の人だけど、まつもとさん自身はNaCl(株式会社ネットワーク応用通信研究所)にジョインするまでは、まったく松江と関係が無かったそうです！
ちなみに、その時ちかくにいた方も私同様に衝撃を受けていました :-)

市長、県知事、国のお役人が参加するカンファレンス

オープニングセレモニーは

前日のウェルカムパティーも由緒ありそうな料亭・・・ 1日目レセプションには大きなお魚の活き作り・・・ まつもとさんの偉さを実感しました。

島根、松江の お・も・て・な・し

会場のくにびきメッセには、抹茶のサービスコーナー、島根県、松江市の観光案内ブースがありました。またスタッフは市役所だけでなく、一畑電気鉄道などの地元企業の方も。

スピーカーには、ウェルカムパティー以外にも 美味しいお弁当、広い控え室、コーヒー・・・ 等々のサービス。 RubyWorld Conference 参加は スピーカーが断然お得です :-)

さらに、井上(NaCl)社長の 脅威の ホスピタリティー !! で、とても楽しいカンファレンスの日々をすごせました。

だんだん

S3へのアップロード速度を上げる方法

サーバー管理

以前、S3への転送が遅い件について に書いたように、自宅 Mac mini からS3へのバックアップファイル転送ですが、単純に aws-sdk(Ruby版)を使うより2倍程度になったので書いておきます。


aws-sdk でのアップロードプログラム

次のようなコードで、ローカルにある PATH_TO_FILE ファイルを S3 の BUCKET_NAME にコピー出来ます(もちろん、access_key_idやsecret_access_keyにはあなたのキーを設定して下さい)。

#!/usr/bin/env ruby
require 'rubygems'
require 'aws-sdk'

AWS.config(
  :access_key_id     => 'XXXXXXXXXXXXXXX',
  :secret_access_key => 'YYYYYYYYYYYYYYY',
  :s3_endpoint       => 's3.amazonaws.com'
)
s3 = AWS::S3.new
bucket = s3.buckets['BUCKET_NAME']
path = 'PATH_TO_FILE'
obj = bucket.objects[File.basename(path)]
obj.write(:file => path)

writeメソッドのオプションを指定しよう

AWS::S3::S3Objectのwriteメソッドのドキュメントを見ると、いくつかオプションがあります。ここで転送速度と関係しそうなものには

  • : single_request 転送を一回で行うか、分割して行うか。デフォルトは分割(false)
  • :multipart_threshold 小さいファイルの場合は分割しない、しきい値。デフォルト 16Mbye
  • : multipart_min_part_size 分割する際の大きさ。デフォルト 5Mbye

今回はバックアップなので転送するファイルは 数100Mbye〜数Gbyte です。 デフォルトだと5Mbyeのファイルに分割して送っています。試しに multipart_min_part_size を大きくしたところ、転送時間が多少改善しました。

:single_request => true にして試したところ、デフォルトの半分程度の転送時間になりました！

single_requestで送るとということは一旦ファイルをメモリーに全部取り込んでからS3へ転送されます、したがってメモリーを大量に消費します。バックアップを行っている時に Mac mini は他には何も行っていないので今回は問題ないですが、使用環境によっては multipart_min_part_size を調整する方が良い場合もあると思います。

「はじめてのiPhone/iPadアプリ開発」の iOS7/Xcode5対応サンプルコードとサポートページを公開しました

本

今年3月に出版されたiPhone/iPadアプリ開発の書籍 はじめてのiPhone/iPadアプリ開発―iOS6/Xcode4対応版 (TECHNICAL MASTER) のiOS7/Xcode5に対応したサンプルコード と サポートページ を公開しました！

はじめてのiPhone/iPadアプリ開発―iOS6/Xcode4対応版 (TECHNICAL MASTER)

はじめてのiPhone/iPadアプリ開発―iOS6/Xcode4対応版 (TECHNICAL MASTER)

サンプルコード

「はじめてのiPhone/iPadアプリ開発」で取り上げているサンプルコードは大部分はそのままでも iOS7/Xcode5 で動作しますが、

  • ビデオ再生アプリが iOS-SDKの仕様が変わったようで早送り等が出来なくなりました
  • 一部のアプリでは、表示の一部が欠けます

を修正しました。秀和システムのサポートページ からダウンロードできます。

サポートページ

サポートページ では iOS7/Xcode5 で本書内容と関連する、

  • iOS7のフラットデザインとコンテンツ中心の考え方で表示の一部が欠る件の対応方法
  • Xcode5で変わった Constraint(AutoLayout)の配置方法の簡単な解説

を書きましたので、参考にして頂けると良いかと思います。

ssh ログインで ~/.ssh/id_ras が優先されるのを防ぐには

サーバー管理

GitLab を開発用サーバーに入れて運用し始めたのですが ~/.ssh/config に接続用の秘密キーを指定しても ~/.ssh/id_ras を使って接続しょうとしエラーになり困っていました。

実用SSH 第2版―セキュアシェル徹底活用ガイド

GitHub風システム、GitLab は ssh 接続のgitコマンドからのアクセス時には、sshのキーを使いユーザーを管理しています。

もし1人のUnix(Mac)アカウントがGitLabに複数のユーザーを登録していて、ユーザーAの公開キーが ~/.ssh/id_ras に対応するもので、ユーザーBの 公開キーが ~/.ssh/id_ras_git の場合を考えてみましょう(各ユーザーのリポジトリーはユーザーだけがアクセス出来ます)。ユーザーBに対応するリポジトリーをアクセスする際に ~/.ssh/config に

Host user-b-repo
  Hostname gitlab.xxxx.com
  User git
  IdentityFile ~/.ssh/id_ras_git

と書き git clone git@user-b-repo:user-b/zzzz.git の様にアクセスすると認証エラーになってしまいます。
ssh に -v オプションを付けて user-b-repo をアクセスしてみると

% ssh -v user-b-repo
OpenSSH_5.9p1, OpenSSL 0.9.8y 5 Feb 2013
debug1: Reading configuration data /Users/aaaaaa/.ssh/config
debug1: Reading configuration data /etc/ssh_config
   ....
debug1: Connection established.
debug1: identity file /Users/aaaaaa/.ssh/id_ras_git type 1    ← ~/.ssh/id_ras_git が使われています
  ...
debug1: Authentications that can continue: publickey,password
debug1: Next authentication method: publickey
debug1: Offering RSA public key: /Users/aaaaaa/.ssh/id_rsa       ← ここに注目
   ...

なぜか ~/.ssh/id_ras を使って接続しています。この際に GitLab は ユーザーA がアクセスしてきたと解釈し、ユーザーBのリポジトリーにはアクセス権がないのでエラーを返します。

ここ数日悩んでいたのですが、今日判りました。 ~/.ssh/config に IdentitiesOnly yesを追加すれば、指定した秘密キーのみが使われるのでした！


ということで ~/.ssh/config は以下の様に書きましょう

Host user-b-repo
  Hostname gitlab.xxxx.com
  User git
  IdentityFile ~/.ssh/id_ras_git
  IdentitiesOnly yes