I was told that people using bash will have to differentiate between the shell-builtin time and /usr/bin/time ( time(1) ). I had to time a program and also had to find ways to automate input, using echo and string redirection <<<. These are the results,

$ time python3 -c "a=input("");print(a)" <<< "12"

real    0m0.023s
user    0m0.020s
sys 0m0.000s

The shell-built-in is called in this ^ case.

$ echo "12" | time python3 -c "a=input("");print(a)"
0.01user 0.00system 0:00.02elapsed 100%CPU (0avgtext+0avgdata 6524maxresident)k
0inputs+0outputs (0major+593minor)pagefaults 0swaps

time(1) is being called in this case.

Why is this happening ? Are they different environments ?

Using Ubuntu 14.04 x86_64

  • Your second example did not use /usr/bin/time but intrinsic code from the shell. The format in use is typically controlled via the shell variable TIMEFORMAT and as your output contains more than just the times, I woould guess that you use csh, zsh or a recent Bourne Shell.
    – schily
    Aug 31 '15 at 9:32
  • @schily: No, it used external time in second case. Try echo | time and /usr/bin/time to see the same output. It's sound like a bug, echo | time work well in zsh, ksh. Also echo |<literal newline>time yield error in bash.
    – cuonglm
    Aug 31 '15 at 9:42
  • No, as you mentioned that you use zsh, "time" refers to the reserved word "time" in zsh. If you like to call /usr/bin/time, call /usr/bin/time.
    – schily
    Aug 31 '15 at 9:51
  • @schily: What do you mean? You said that our second example did not use /usr/bin/time but intrinsic code from the shell, I gave the example to demonstrated that echo | time in bash use the external time instead of reserved word time.
    – cuonglm
    Aug 31 '15 at 9:55
  • You used a shell intrinsic, call type timeto understand your mistake. If you like to use the external command, you cannot just type time but need to use /usr/bin/time
    – schily
    Aug 31 '15 at 9:58

The structure of a pipeline doesn't allow time in the middle, only at the start of the pipeline.

Also, time is a "shell keyword", as shown by type time.

But nothing forbids the use of compound commands (and time each):

time comm1 | ( time comm2 )

So, you could workaround using a sub-shell, like this:

echo "12" | ( time python3 -c "a=input("");print(a)" )

Or also like this:

echo "12" | { time python3 -c "a=input("");print(a)"; }
  • Correct, time was introduced as a shell keyword by ksh88 and other shells copied this idea.
    – schily
    Aug 31 '15 at 9:53

There is two types of time commands. One is shell built-in, belongs to bash. That's the one you see in your first example. Second one , is /usr/bin/time, that's the second one you saw. As for why it's different output, it's because you cannot pipe output to shell builtins. More on that here


If you like to time commands for performance reasons, I recommend not to use /usr/bin/time but either ptime(1) if this available on your platform - ptime gives a nanosecond resolution - or to use a recent Bourne Shell, as the Bourne Shell allows to automatically time all foreground commands (including shell builtins) with a microsecond resolution on all modern operating systems. To time all foreground commands in the Bourne Shell, call: set -o time and set TIMEFORMAT to a useful content to get a higher resolution, e.g.: %6:E real %6U user %6S sys %P%% cpu %I+%Oio %Fpf+%Ww

/usr/bin/time typically has a fixed resolution of 10ms or 1ms.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.