2011-03-20

imapsync で gmail へメールを引越し

昨日の続き。

お題

imap サーバに溜まってた大量のメールを gmail に移動したい。地味にクライアントでドラッグアンドドロップで移動してもいいんだけど、絶対に効率よく出来てる気がしない。というか Thunderbird が固まりまくりで大変です。

gmail には POP で拾ってくれるとか Migration API なるものも用意してあるようですけど、前にも似たようなことがあってちょっとだけ触った imapsync を使いました。

debian ならもちろんパッケージあるし、 MacPorts でも入ります。基本は perl スクリプトのようです。

つかいかた

使い方はいたってシンプルで、以下のような感じ。

ichii386@elmo% imapsync \
> --host1 mail.example.net --port1 143 --user1 ichii386 \
> --passfile1 ./aho1 --authmech1 CRAM-MD5 \
> --host2 imap.gmail.com --port2 993 --ssl2 --user2 'ichii386@mail.example.com' \
> --passfile2 ./aho2 --authmech2 LOGIN \
> --folder INBOX.hoge.fuga --dry

この例では --dry ついてますが、実際に動かすときは外します。ミスるとけっこう大変なので、 --dry つきで少しずつ確認したほうがいいように思います。

aho1, aho2 にはパスワードを生で書いたファイルを用意しておきます
移行元の host1 で ssl が必要なら --port1 993 で --ssl1 つける
--authmech1 は PLAIN とか、まあいろいろ試せばどれか当たるでしょう (--authmech2 はそれで調べた)
- mew 使いなら (setq mew-debug t) しておけばわかると思います。
--folder は指定すればそのフォルダだけ、指定なければ全フォルダをコピーします
途中の画面で移行元、移行先にどういうフォルダがあるか、 host1 にあって host2 になりフォルダはなにか、が表示されます
- とりあえずフォルダ 1 つ指定してみて、デフォルトでフォルダ名がどういう対応で移動されるか見るとよさそう
--regextrans2 でフォルダ名を s/hoge/fuga/ することもできます
--delete2 とかほかにもオプション盛りだくさん

++++ Calculating sizes
Host1 folder [INBOX.hoge.fuga]                  Size:  12170183 Messages:  3162
Total size: 12170183
Total messages: 3162
Time: 3 s
++++ Calculating sizes
Host2 folder [hoge/fuga]                        does not exist yet
Total size: 0
Total messages: 0
Time: 0 s
++++ Listing folders
Host1 folders list:
[INBOX]
[INBOX.Archives]
...

Host2 folders list:
[INBOX]
[Notes]
...

Folders in host2 not in host1:
[[Gmail]/foo/bar]
...

++++ Looping on each folder
[INBOX.hoge.fuga]                   -> [hoge/fuga]
Host2 folder hoge/fuga does not exist
Creating folder [hoge/fuga]
...

このように INBOX.hoge.fuga は hoge/fuga に移動されるようでした。この場合、 "hoge/fuga" というラベルが付いたメールとして gmail に入ることになります。

もっとも、 gmail ではフォルダはラベルでしかなく、ラベルの張替えはとても早いので、すでにある namespace とかぶらないとこに一旦全部突っ込んで、あとで必要なところに振り分けるのもありかもしれないです。

注意点としては、昨日書いたとおり「同じ message-id をもつメールが 1 つに縮約される」ので、移行元のサーバに同じメールのコピーがたくさん転がっている場合は少しずつ試してからやりましょう。とくに INBOX.Sent に注意。

メモ

ちなみに、前に調べた時と比べると超絶遅かった。これは gmail 側が遅いようです。 gmail 側の負荷が厳しいとはとても思えないので、あるていど大きな folder について並列で走らせてあげるといいかもね。

2011-03-19

Google Apps と IMAP なメール生活

google apps gmail imap

地震を始めいろんな理由で、使っているメールサーバのいくつかが最近 Google Apps に移行しました。

いままでは cyrus なり courier の imapd にメールを溜め、 Thunderbird でメール読んで mew でメール書いていたんですが、これが Google Apps の IMAP サーバ (Gimap) に変わりました。プロトコルとしては IMAP で同じですが、ずいぶん前に調べたとおり、フォルダの概念とラベルの概念が微妙に違うんですよね。

ということで違いを調べてみたいんですが、正直よくわからん。まあ中の実装がどうであれ、こう設定すればいいのね、というのはわかった気がします。もうちょい IMAP の RFC ちゃんと読まなきゃだね。

以下、 imap というのはよくあるふつうな imap サーバ、 gmail は Google Apps も GMail も含んだもの。

参考資料

フォルダとラベル

imap
- あるメールは unique な場所としてのフォルダという property をもつ。
- おなじ message-id をもつメールが複数存在しても良く、とうぜん複数のフォルダにあったりする
- フォルダはたとえば INBOX.foo.bar といった階層を持つ (という実装になってるって話だけど)

gmail
- フォルダという概念はなく、すべてのメールは「すべてのメール」に入ってる
- メールは複数のラベルを持つことができる
- おなじ message-id をもつメールは、実体として 1 つ

imap で見た gmail
- [Gmail]/foo/bar という形のラベルがフォルダのように見える
- cyrus imapd でいうところの duplicatesuppression: yes の状態で、おなじ message-id のメールを複数送っても1通しかこない。
- メールに複数のラベルが付いている場合、複数のフォルダに入っているように見える

送信済みメール

imap
- MUA が送信したメールのコピーを INBOX.Sent に置くことで、送信済みメールのフォルダを実装しています。

gmail
- gmail の smtp サーバは、送信したメールを gmail に保存した上で "[Gmail]/送信済みメール" のラベルをつけてくれるので、 MUA は何もしなくていい。というよりむしろ、してはいけない。

"Bcc: 自分" で暮らしていた人は、同じ message-id なので同じメール扱いで、受信フォルダと送信済みに同じメールが表示されます。つまりは同じメールに "[Gmail]/送信済みフォルダ" と inbox ラベルが付いた状態。これを削除してしまった場合、送信済みからも消えてしまうので注意です。

gmail のスレッド表示のおかげで、自分が送ったメールも含めてスレッドはちゃんと会話形式で表示されることになります。

メールの削除

imap
- ゴミ箱に移動する = INBOX.Trash フォルダに移動する
- 完全に削除する = \Deleted マークをつけて適当なタイミングで EXPUNGE する

gmail
- ゴミ箱に移動する = "[Gmail]/ゴミ箱" ラベルを付ける
  - ゴミ箱のメールは 30 日経つとかってに消える
- \Deleted マークつける = マークをつける対象のメールについて、そのフォルダに対応するラベルを消す??
  - ちょっとここの動作はわかんない。。。
  - 少なくとも、ふつうの IMAP クライアントでメールを消しても、ラベルが消える (= 全てのメールに残る) だけで、メール自体は消えません。

注意点として、送信済み同様にメール複数のラベルをもったメールを削除した場合、 imap で見るとフォルダ A に入ってるメールだけを消したつもりが B に入ってる同じメールも消えてしまう、ということがあります。

迷惑メール

imap
- 迷惑メールとしてマーク = これはクライアントがもつ機能でしかない
- 迷惑メールフォルダに移動 = INBOX.Junk フォルダに移動

gmail
- "[Gmail]/迷惑メール" ラベルが付いているもの。

メールの未読/既読

これは \Seen フラグで同じかな??

Thunderbird での設定

上の参考資料に書いてあるとおりですが、以下のように設定しました。最初の大まかな設定は自動設定に任せてて、特に書いてない項目はデフォルトのまま。 (英語版 Thunderbird 3.1.9 です)

Server Settings
- Server Settings
  - When I delete a message: Just mark it as deleted
- Advanced... (右下のボタン)
  - IMAP server directory: [Gmail]

Copies & Folders
- When sending messages, automatically:
  - Place a copy in: check off
  - Bcc these email addresses: いちおう自分自身を追加
- Drafts, Archives, and Templates
  - Keep message drafts in: Other: 下書き
  - Keep message archives in: Other: すべてのメール
  - keep templates in: "Templates" Folder on: (デフォルト), これは使わない限りフォルダできないので無視

Junk Settings
- Enable adptive junk mail control: check off
- Move new junk messages to: Other: 迷惑メール (これできっと学習してくれるはず)

Synchronization & Storage
- Message Synchronizing の Advanced...
  - すべてのメールのチェックは off にする

Thunderbird の mark it as deleted はなにやってるんだ...? \Deleted じゃないの??

mew での設定

気をつけなければならないのは以下:

fcc: %Sent は勝手にやってくれるので不要
メールの削除は \Deleted ラベルじゃなく「[Gmail]/ゴミ箱」に移動しないといけないので、 imap-trash-folder の設定が必須
- mew の実装では COPY してからもとのメールを \Deleted つけて EXPUNGE するので、ただし mew の
というかフォルダ名が日本語とかありえないので、gmail の表示言語は英語にしておく。
- いや、どうかな...

(setq mew-name              "ICHII Takashi")
(setq mew-user              "ichii")
(setq mew-mail-domain       "example.net") ; 名乗るメールアドレスは ichii@example.net
(setq mew-imap-user         "ichii386@mail.example.com") ; apps のアカウント
(setq mew-imap-server       "imap.googlemail.com")
(setq mew-imap-ssl          t)
(setq mew-imap-trash-folder "%[Gmail]/Trash")
(setq mew-imap-delete       nil) ; imap サーバから削除しない
(setq mew-smtp-user         "ichii386@mail.example.com")
(setq mew-smtp-server       "smtp.googlemail.com")
(setq mew-smtp-ssl          t)
(setq mew-fcc               nil) ; 不要
(setq mew-dcc              nil) ; 必要なら入れる

iPhone (iOS4)

ちょいおまけですが、 http://support.apple.com/kb/HT4207 という話があります。

ようするに削除はうまく動かない (全てのフォルダに残ってしまう) ので、削除ボタンをアーカイブボタンに変えてしまえばいいじゃん、ということでした。

まとめ

とまあ、ようするに gmail の IMAP はあくまで「それっぽく動く」だけで、根本的に思想が違うんです。なので gmail をその思想通り使うにはやっぱり web の gmail を使う必要があって、 MUA に趣味が現れる時代じゃないんだな...。

思想が違うものが同じようなアプリで同じように扱えてしまうと、却って混乱のもとなのかもしれません。これを機に、 gmail になってないのも全部移行してしまおうか悩んでます。

2011-01-13

Re: Renumbering SCSI controllers under Solaris

solaris devfsadm

http://www.lbl.gov/ITSD/CIS/faqs/UNIX_Faq/9.html をインストール時にやってみよう的な話。

某コントローラが 6 つあるマシンに Solaris 11 Express をインストールしようとしたら、コントローラが c7, c8, c10, c11, c12, c13 とナゾな認識のされ方をしてしまった。欠番の c9 は ILOM で飛ばしている Virtual CDROM ドライブ。

Solaris 11 Express Live CD から起動し、先のサイトに書いてあるとおり、思い切って rm /dev/{dsk,rdsk,cfg}/c* をしてしまう。どうせ再インストールで一度全部消すし。この状態で iostat -En してみると、 iostat -E と同じく sd0, sd1, ... になってるんですね。

この Virtual CDROM ドライブは /var/adm/messages によると scsa2usb0 と認識されているので

# devfsadm -v -i scsa2usb

とすれば、 CDROM ドライブだけが c0t0d0 に割り振られました。

つづけて引数なしの

# devfsadm -v

すると、残りのコントローラが c1 - c6 に割り振らました。

先のサイトでは、

6)
Boot with "-srv" option.

と書いてあるんですけど、 devfsadm したおかげでちゃんとディスクはみえているようです。そのままデスクトップの "Install Oracle Solaris" のアイコンをダブルクリックしたら、ちゃんとインストールが進んでいます。(まだ途中)

けっきょくなんで c7 から始まったのかというと、きっとディスクに「すでにこのディスクは cXtY で運用されてるよ」みたいなことが書いてあるんでしょうね。で、インストーラが起動時にそれを読んでしまい、再インストールしてもそれを継続してしまう。今回インストール前とズレたのは、ふだん繋いでいない Virtual CDROM をつなげたからでした。

text installer だとどうやるんだろ。 Debian とかだったら、 Ctrl+Alt+Fn で裏の端末から作業するとこだけど...。

うん、とりあえず連番っていいですね。

2010-12-23

ILOM から /SP/console でサーバにログインしたい

sun solaris x86

だいたいの Sun のサーバには ILOM (Integrated Lights Out Manager, ALOM とか ELOM とかも同じようなもの?) ってのが付いています。いわゆる管理用のワンボードマシンのようなものです。

ILOM の特徴

本体が落ちていても通電さえしていれば ILOM は動いていて、 ssh で ILOM CLI にログインして本体の電源を入れたり、http 経由で ILOM Web にログインしてブラウザから操作することもできます。さらには KVM をまるごとリダイレクトできる jnlp も用意されています。知ってる限りでは RJ45 ポートが 2 つ付いていて、シリアル (SER MGT) とイーサネット (NET MGT) の両方で ILOM に接続できるようになっています。

たとえば、まだ OS をインストールしていないマシンでも、イーサネット経由で ILOM さえつながれば、POST 画面から BIOS に入るのもリモートで作業できます (x86 前提ぽくて恐縮ですが...)。 PXE boot できればそこからインストールすればいいわけですね。

Dell や HP のサーバを使っている人には IPMI (Intelligent Platform Management Interface) と言ったほうが分かりやすいかもしれません。 Solaris なら /dev/bmc も用意されているし、基本 IPMI 互換ですが、もうちょいリッチなもの、というかんじです。

シリアルとか端末とかコンソールとか

Sun のサーバの1つである Sun Fire X4540 (もう EOL; 前身の X4500 は TSUBAME 1.0 で使われてたやつ) には、 ttya (COM1), ttyb (COM2) が OS から見えるものの物理的にはポートは存在せず、ILOM のシリアルポートを ILOM の /dev/console として使うか、本体のシリアルポート (/dev/ttyb?) として使うかが BIOS で選べるようになっているようです。また ILOM CLI からは "start /SP/console" というコマンドで本体の /dev/ttya にシリアル接続できるようです。

...とか言ってもよく分かんないですよね。正直シリアルコンソールなんてほとんど使わないし、自分くらいの "プレゆとり" な世代は pty とか pts しか知らないですよ。

感覚としては以下のようなことは分かっているんですが、それぞれの関係がどうなっているのか分からない。

本体にモニタとキーボードつなぐと "ホスト名 login:" というプロンプトが出てログインできる
ILOM に /SP/console という機能があって、コンソールにつながると説明書に書いてある (ログインできるような期待がある)
OS からは /dev/console と /dev/ttya と /dev/ttyb が見える
eeprom もしくは grub の multiboot に渡すブートオプション (-B) で、 console=[text|ttya|ttyb] が選べる

/SP/console が動かない

とまあ、ここまでは前フリで、話としては ILOM から start /SP/console してもログインプロンプトが出なくて困ってました。例えば OS の sshd が死んでしまったときにリモートからログインしたいんだけど、Java アプリだと GUI でも操作できる代わりにコピペできないので、ILOM に ssh して作業したいのです。

ひたすらググってるうちに http://oshiete.goo.ne.jp/qa/4012162.html を見たら、あーこんなかんじかな? と繋がったような気がするのでメモです。間違ってても知りません。

ログインプロンプトは /usr/lib/saf/ttymon -d の引数で渡したデバイスに出る
- デフォルトでは /dev/console
/dev/console は仮想的なデバイスっぽい?
- 実体は eeprom もしくは multiboot のオプションで決める。変更するときは再起動が必要。
console=text の実体
- 本体につないだモニタ = ILOM Web の jnlp でいう "ILOM Remote Console"
console=ttya の実体
- BIOS で SER MGT ポートを ILOM に渡してる設定の時は /SP/console
- SER MGT ポートを本体に渡してる時は未確認 (/HOST/console なのかな?)
デフォルトでは console=text かつ ttymon は /dev/console を向いている
- なので /SP/console ではログインプロンプトが出ない

ttymon の先を変える

BIOS の機能として console=text の実体に /SP/console に繋げられるとありがたいんですが、そうもいかないようでした。再起動などせずにサクっと切り替えるには、ttymon でつなぐ先を変えばいいじゃん!

さいしょ

ichii386% ssh ILOMのIPアドレス
Password:

Oracle(R) Integrated Lights Out Manager

Version 3.0.10.13 r56460

Copyright (c) 2010, Oracle and/or its affiliates. All rights reserved.

-> start /SP/console
Are you sure you want to start /SP/console (y/n)? y

Serial console started.  To stop, type ESC (
(このまま固まる)

ttymon のデバイスを変える

ichii386% pfexec svccfg -s console-login editprop
("# setprop ttymon/device = astring: (/dev/console)" の行で、先頭の # を削りつつ以下に編集して保存、終了)
setprop ttymon/device = /dev/ttya
ichii386% pfexec svcadm restart console-login

固まってた /SP/console からログインプロンプトが出る!
- めでたしめでたし

このあたりで、そういや Linux だと Ctrl+Alt+Fn とかで tty 切り替えてたよなー、と思い出すんですよね。 Solaris の流儀だと1つしか使わないものなのかな??

おまけ

某パートナー企業のサポートに聞いてもまったく埒があかず、しかたないから真面目に調べたら、あっさりできた。お金とってあそこはいったいなにやってんだ...。

そうそう、これを調べてる間に http://www.sun.com/opensourcecode/ なんてのがあったのを知りました。もうすごいね、自分で make できる気がしないです。

2010-11-18

Oracle Solaris 11 Express がキタ

solaris virtualbox

とうとう来ましたよ! SPARC 版は OpenSolaris や OpenIndiana 含めて Solaris10 u9 で (まともなリリースが) 止まってたので、ほんと待ちわびてました。

http://www.oracle.com/us/products/servers-storage/solaris/index.html

ということで、さっそく家のサーバを入れなおしました。 image-update してもいいけど、せっかく rpool とは別に zpool を用意してあるので、zpool export して新規にインストールです。

インストール

...うーん、すごいすんなり行きました。すんなりすぎて書くことがありません。

ichii386@oscar% uname -a
SunOS oscar 5.11 snv_151a i86pc i386 i86pc Solaris
ichii386@oscar% cat /etc/release
                      Oracle Solaris 11 Express snv_151a X86
     Copyright (c) 2010, Oracle and/or its affiliates.  All rights reserved.
                           Assembled 04 November 2010

気づいたことをメモ。

使ったのはテキストインストーラで、OpenSolaris のときみたく GUI が動く環境は不要
- gdm はそもそもインストールされない。 svcs -a | grep graphical も空っぽ
rpool が rpool1 になった
インストール時に作ったユーザは sudoers に入るが Primary Administrator ではない
time-slider 依存の zfs-auto-snapshot が~~動かない~~動きました
- dbus かなんかのエラー。GNOME 入れる気はしないしなぁ。

dbus.exceptions.DBusException: org.freedesktop.DBus.Error.AccessDenied: Connection ":1.4" is not allowed
to own the service "org.opensolaris.TimeSlider" due to security policies in the configuration file

- 追記: svcadm refresh dbus; svcadm restart dbus したらエラー出なくなりました
  - ふとちゃんと見直したら /etc/dbus-1/system.d/time-slider.conf があるので動きそうなもんだよな、と。

VirtualBox もバッチリ

host os との組み合わせで不安な仮想マシン周りですが、 VirtualBox はさっき拾ってきた 3.2.10 で問題なく動きました。

ただし、 gdm などの GUI はインストールされてないので、 vm の起動は VBoxManage などを使わないといけません。でも設定項目とかどういう選択肢があるのか調べるのめんどいですよね。そういうのはやっぱり GUI で誰かが頑張ってるのを使いたいところ。

そこで、ぜんぜん使ってなかった virtualbox webservice を使ってみることにしました。

phpVirtualBox

virtualbox webservice 自体は soap のサービスでしか無いので、これのクライアントが必要です。なんと php で出来てるクライアント web アプリがあるそうで、 virtualbox.org のトップに動線貼ってあって感動した。

http://code.google.com/p/phpvirtualbox/

以下に使えるようにするまでの手順を書きます。

virtualbox を誰で起動してたのか調べる
- 以下が正しい調べ方な気はしないですが、とりあえず自分のアカウントで vm 作ってたんだろうな、という気はする

ichii386@oscar% VBoxManage list --long systemproperties|grep folder
Default machine folder:          /export/home/vbox/Machines
Default hard disk folder:        /export/home/vbox/HardDisks
ichii386@oscar% ls -la /export/home/vbox/Machines/
total 6
drwxr-xr-x 3 ichii386 staff 3 Jul 15 11:34 .
drwxr-xr-x 4 ichii386 staff 4 Jul 15 11:34 ..
drwxr-xr-x 3 ichii386 staff 5 Nov 17 23:18 win7

webservice の起動ユーザをいじる
- "# setprop config/user = astring: root" のところを自分のアカウント名に変えた

ichii386@oscar% pfexec svccfg -s svc:/application/virtualbox/webservice:default editprop

webservice を有効にする

ichii386@oscar% pfexec svcadm refresh virtualbox/webservice
ichii386@oscar% pfexec svcadm enable virtualbox/webservice

確認

ichii386@oscar% netstat -an -f inet -P tcp | grep 18083
127.0.0.1.18083            *.*                0      0 65928      0 LISTEN
ichii386@oscar% ps -ef|grep vboxweb
ichii386  4642  4567   0 01:11:05 pts/1       0:00 grep vboxweb
ichii386  4478     9   0 00:16:52 ?           0:02 /opt/VirtualBox/vboxwebsrv --host localhost --port
ichii386@oscar% telnet localhost 18083
Trying ::1...telnet: connect to address ::1: Connection refused
Trying 127.0.0.1...
Connected to oscar.
Escape character is '^]'.
GET / HTTP/1.0

HTTP/1.1 500 Internal Server Error
Server: gSOAP/2.7
Content-Type: text/xml; charset=utf-8
Content-Length: 495
Connection: close

<?xml version="1.0" encoding="UTF-8"?>
<SOAP-ENV:Envelope xmlns:SOAP-ENV="http://schemas.xmlsoap.org/soap/envelope/" xmlns:SOAP-ENC="http://
schemas.xmlsoap.org/soap/encoding/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="
http://www.w3.org/2001/XMLSchema" xmlns:vbox="http://www.virtualbox.org/"><SOAP-ENV:Body><SOAP-ENV:Fa
ult><faultcode>SOAP-ENV:Client</faultcode><faultstring>HTTP GET method not implemented</faultstring><
/SOAP-ENV:Fault></SOAP-ENV:Body></SOAP-ENV:Envelope>Connection to oscar closed by foreign host.

これで webservice は動いてるようです。

apache, php が動く環境を用意

ichii386@oscar% pfexec pkg install web/php-52 web/server/apache-22/module/apache-php5 web/server/apache-22

/etc/apache2/2.2/conf.d と php.ini を適当にいじる
- とりあえず DocumentRoot を /home/apache/htdocs とかにしておきます
phpVirtualBox をダウンロード

ichii386@oscar% cd /home/apache/src
ichii386@oscar% wget http://phpvirtualbox.googlecode.com/files/phpvirtualbox-0.5.zip
ichii386@oscar% unzip phpvirtualbox-0.5.zip
ichii386@oscar% vim phpvirtualbox-0.5/.htaccess
(なんか適当に)
ichii386@oscar% cd ../htdocs
ichii386@oscar% pfexec ln -s ../src/phpvirtualbox-0.5 vbox

ドキドキしながら http://oscar.local/vbox/ を叩く。

が、エラー。どうも認証でこけてるっぽい??
- http://code.google.com/p/phpvirtualbox/issues/detail?id=35 とおなじメッセージ
./phpvirtualbox-0.5/config.php にパスワード設定するところがある
- 超絶気持ち悪いけど、自分だったり root だったりの生パスワード書いてもうまくいかない
VRDPAuth がどうこうしてるみたいなので、めんどいから null にしてしまおう
- このへん Solaris 版の情報って少ないですよね

ichii386@oscar% VBoxManage setproperty websrvauthlibrary null

もいちどやってみたら、動いたようです。最初の画面が表示されるまでちょっと時間かかるかも。

見たとおりですが、VirtualBox 上では Windows7 が動いています。ホストは zfs で i/o 性能がいいので、 vm の起動もサクサクです。手元の iMac で VMWare Fusion を使っていたときは、起動するたびに i/o wait で死んでたから超快適。今はいつも動かしっぱなしになっています。

ちなみに Windows7 への接続は、 VirtualBox のではなく windows 自体のリモートデスクトップサーバに接続するようにしてます。さらに windows 版の iTunes いれて、ついでに入ってくる Bonjour サービスのおかげで DHCP 環境でも oscar-win7.local でアクセスできて超快適です。

2010-11-01

ports install

memo

ただのメモ

bonniexx
coreutils +with_default_names
findutils
git-core
iperf
lv
mercurial
nmap
proctools
rsync
#screen
stunnel
subversion
vim
w3m
wget
zsh-devel +mp_completion

proctools は /opt/local/bin/tsort をいったん退避して /usr/bin/tsort を使わせる

2010-10-09

Coq 入門

coq

@kikx さんと @lyrical_logical さんに教えてもらってます。

ichii386@count% coqtop                                                                                  [..ecture/functional/coq]
Welcome to Coq 8.2pl2 (July 2010)

Coq < Goal forall (P Q: Prop), (P -> Q) -> P -> Q.
1 subgoal

  ============================
   forall P Q : Prop, (P -> Q) -> P -> Q

Unnamed_thm < intros.
1 subgoal

  P : Prop
  Q : Prop
  H : P -> Q
  H0 : P
  ============================
   Q

Unnamed_thm < apply H.
1 subgoal

  P : Prop
  Q : Prop
  H : P -> Q
  H0 : P
  ============================
   P

Unnamed_thm < exact H0.
Proof completed.

Unnamed_thm < Qed.
intros.
apply H.
exact H0.

Unnamed_thm is defined

Coq < Goal forall (P Q R: Prop), (P->Q->R)->(P->Q)->P->R.
1 subgoal

  ============================
   forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R

Unnamed_thm0 < intors.
Toplevel input, characters 0-6:
> intors.
> ^^^^^^
Error: The reference intors was not found in the current environment.

Unnamed_thm0 < intros.
1 subgoal

  P : Prop
  Q : Prop
  R : Prop
  H : P -> Q -> R
  H0 : P -> Q
  H1 : P
  ============================
   R

Unnamed_thm0 < apply H.
2 subgoals

  P : Prop
  Q : Prop
  R : Prop
  H : P -> Q -> R
  H0 : P -> Q
  H1 : P
  ============================
   P

subgoal 2 is:
 Q

Unnamed_thm0 < exact H1.
1 subgoal

  P : Prop
  Q : Prop
  R : Prop
  H : P -> Q -> R
  H0 : P -> Q
  H1 : P
  ============================
   Q

Unnamed_thm0 < apply H0.
1 subgoal

  P : Prop
  Q : Prop
  R : Prop
  H : P -> Q -> R
  H0 : P -> Q
  H1 : P
  ============================
   P

Unnamed_thm0 < exact H1.
Proof completed.

Unnamed_thm0 < Qed.
intros.
apply H.
 exact H1.

 apply H0.
 exact H1.

Unnamed_thm0 is defined

Coq < Goal forall (P Q R: Prop), (P->Q->R)->(P->Q)->P->R.
1 subgoal

  ============================
   forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R

Unnamed_thm1 < auto.
Proof completed.

Unnamed_thm1 < undo
Unnamed_thm1 < .
Error: No such subgoal

Unnamed_thm1 < Undo.
1 subgoal

  ============================
   forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R

Unnamed_thm1 < info auto.
 == intro P; intro Q; intro R; intro H; intro H0; intro H1;
       simple apply H.
    exact H1.

    simple apply H0; exact H1.

Proof completed.

Unnamed_thm1 < Qed.
info auto.

Unnamed_thm1 is defined

Coq < Print Unnamed_thm1.
Unnamed_thm1 =
fun (P Q R : Prop) (H : P -> Q -> R) (H0 : P -> Q) (H1 : P) => H H1 (H0 H1)
     : forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R

Argument scopes are [type_scope type_scope type_scope _ _ _]

Coq <

Coq < Goal forall (P: Prop), P -> P.
1 subgoal

  ============================
   forall P : Prop, P -> P

Unnamed_thm2 < intro.
1 subgoal
  
  P : Prop
  ============================
   P -> P

Unnamed_thm2 < intro.
1 subgoal
  
  P : Prop
  H : P
  ============================
   P

Unnamed_thm2 < intro.
Toplevel input, characters 0-5:
> intro.
> ^^^^^
Error: No product even after head-reduction.

Unnamed_thm2 < apply H.
Proof completed.

Unnamed_thm2 < Qed.
intro.
intro.
apply H.

Unnamed_thm2 is defined