Edited at

GNU Time にある壮大なバグ (はもうありませんので安心してください)

More than 1 year has passed since last update.

とりあえず警告として拡散できればということで。

bash の time ではなく、 明示的に /usr/bin/time と書くことで呼び出せる

プログラムがあります。機能はtime と同じく、コマンドを引数に取り、

それを実行し、そして使用メモリ量、使用時間(user,sys)を出力します。

bashのtimeにくらべて、引数でフォーマットを自由に変更できるので便利です。

しかししかし、壮大なバグがあります。

それはすなわち、

使用メモリ量が4倍に表示される

ことです。BSDの実装をlinuxにそのまま持ってきたらこうなったそうです。

2010年ぐらいに見つかったバグですが、

ubuntu14.04の公式aptリポジトリでも time のバージョンは1.7のまま。

直っていません。直せよ・・・。

論文締め切り前なんですが、これで結構な時間を無駄にしました。ちくしょー

ソース

https://bugzilla.redhat.com/show_bug.cgi?id=702826

https://bugzilla.redhat.com/show_bug.cgi?id=783143