zshのtimeと/usr/bin/timeが別物ってことに気づかずハマったので、メモ。
使い方としてはどちらも引数にコマンドを渡すと、そのコマンドの実行時間を出力してくれるというもの。
zsh
zshでtimeコマンドをそのまま使うとzshの提供するtimeが発動する。
$ which time
time: shell reserved word
で、このtime使うとこんな出力がされる
$ time sleep 1;
sleep 1 0.00s user 0.01s system 1% cpu 1.017 total
このフォーマットは環境変数TIMEFMTに従う。
$ echo $TIMEFMT
%J %U user %S system %P cpu %*E total
これの意味はman zshparamのTIMEFMTの項目で見れる。
timeコマンド自体の説明はman zshmiscに載っている。man timeで見れるのは/usr/bin/timeの使い方であって別物。/usr/bin/timeで使えるようなオプションはない。
ちなみにREPORTTIMEという環境変数設定しておくと一定時間以上かかったコマンドの時間を出力してくれるが、このzshのtimeで出力される。
http://qiita.com/items/b72373f7e4bc79b13568
/usr/bin/time
こちらを使うと以下の様な出力になる。
$ /usr/bin/time sleep 1;
0.00user 0.00system 0:01.02elapsed 1%CPU (0avgtext+0avgdata 2080maxresident)k
0inputs+0outputs (0major+172minor)pagefaults 0swaps
こいつのフォーマットは環境変数TIMEに従う。TIMEが設定されてなかったら以下のフォーマットになる。
%Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k
%Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps
使い方やフォーマットの意味はman timeで見れる。多分大体zshのtimeと同じ。オプションが使える分高機能？
蛇足
「time コマンド」とかでぐぐって出てくるのは/usr/bin/timeの方ばっかりだし、man timeして出てくるのも/usr/bin/timeの使い方なのに、timeとコマンドを打つと思ったとおりに動いてくれなくて困ってた。
オプションは使えないし環境変数TIMEをいじっても出力変わらないし。
ほんと時間無駄にした(´・ω・｀)