On Thu, Aug 08, 2024 at 08:31:10 +0200, Thomas Schmitt wrote: > Greg Wooledge wrote: > > * TIMEFORMAT=... time foo will invoke /usr/bin/time, but > > TIMEFORMAT=... eval time foo will use the builtin.
(Yeah, oops, time is a "shell keyword", not a "builtin".) > I wonder about the formal reason for this. > > Is it because "time" is not listed in the man page under > SHELL BUILTIN COMMANDS but mentioned as "reserved word" under Pipelines ? > Does the variable assignment before "time" cause the rest of the line > to be regarded as Simple Command rather than as Pipeline ? There are some mysteries in bash that I'm content simply to write off as "here be magic". I note that such mysteries exist, I try to find the best workarounds that I can, and I document them if I feel other users are likely to find my workarounds helpful. Honestly, I don't fully know. You could ask on the help-bash mailing list, if you really want to find out. Or go source-diving in bash yourself. But I suspect it's simply that the grammar for "time" was never extended to allow temporary variable assignments. Shell keywords (such as "time", and also "if", "while", "case", "[[" and several others) have special grammar/parsing rules. If one of these keywords is involved, you're no longer looking at a Simple Command. You've got something different. In the specific case of "time", the syntax is time [-p] pipeline If your code says time echo hi | sleep 2 then you aren't simply timing the echo command. You're timing the whole *pipeline*, including the sleep command. This wouldn't be possible without "time" flexing its keyword powers and bending the parsing rules. You can't do that with /usr/bin/time, unless you invoke a whole new shell: /usr/bin/time sh -c 'echo hi | sleep 2' which of course distorts your timing. (Also note that "time echo" runs the shell's builtin echo, while "/usr/bin/time echo" would be forced to run /usr/bin/echo, since /usr/bin/time doesn't have access to the shell's builtins.)