Makefile: Detect if we are using gnu time

[jmprusi]

Due to differences between bsd time and gnu time command,
the current makefile files to run under Darwin.

This commit disables writing "bench.txt" for non linux systems.

[unleashed]

There are non-linux OSes running GNU time. How about using time --version and looking for the string GNU time? Also there might be workarounds to have this information (alone, not including anything else but timing info) in a bench text file, although not sure it is really worth exploring.

[mikz]

@unleashed then those users can contribute that feature, right? :) This is improving it significantly for macOS users. gnutime is not even part of coreutils on brew (that some people install to get stuff like readline). And time is provided by shell anyway in some cases (like zsh).

[mikz]

👍

[unleashed]

It's not a feature, but doing this right: you want to avoid using GNU time's features if you don't have GNU time. We'd also be better off providing a similar behaviour if possible/easy instead of disabling it.

Here we want to store the timing data to be shown at the end of the process - so if time does not have -o on BSDs/Darwin it might still be possible to dup stderr for time and redirect stdout/stderr to the original streams for the executed processes, getting the same desired result (although probably a different output format from time).

Something like \command time 3>&2 4> bench.txt 2>&4 sh -c "$@ 2>&3" might work everywhere and then the only thing needed would be to check which of the other arguments are supported on BSDs/Darwin userland. IIRC some BSDs also supported formatting the output.

[mikz]

@unleashed but no one cares about this feature on Darwin. First person that comes and cares can do that.
Right now it does not work and this is a fix to make it work.

[jmprusi]

@unleashed @mikz Updated the PR, please review, now we check if the time command supports --version (gnu) and choose between two different strategies.

[mikz]

Unfortunately this does not work in zsh.

$ command time --version
time: illegal option -- -
usage: time [-lp] command.

I'm for dropping this feature altogether and let people opt in by setting on SHELL instead of this being in the Makefile:

apisonator/Makefile

Line 3 in 2aef665

SHELL = $(PROJECT_PATH)/script/make_report_time.sh

[jmprusi]

@mikz this should be interpreted by /bin/sh not zsh, working fine for me, with zsh.

[mikz]

I see! 👍

[unleashed]

bors r+

[bors]

Build succeeded

• ci/circleci