`sage-logger`: Replace use of `/usr/bin/time` by bash keyword `time` #37840

mkoeppe · 2024-04-20T22:56:17Z

Follow-up after

... to make the display of package build times available on Linux too.

Fixes #37785 (comment), closes #37832.

📝 Checklist

The title is concise and informative.
The description explains in detail what this PR is about.
I have linked a relevant issue or discussion.
I have created tests covering the changes.
I have updated the documentation and checked the documentation preview.

⌛ Dependencies

Depends on sage-logger: Suppress "No such file or directory" messages #37785

github-actions · 2024-04-20T23:59:38Z

Documentation preview for this PR (built with commit ffa4f46; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

tornaria · 2024-04-21T17:06:12Z

Do we really need to have different functions for different systems? It seems this kind of case by case handling might lead to issues later.

May I suggest something like this, which depends only on $SECONDS (available on bash) and will use whatever the user has as time (usually bash builtin)

time_silent_if_less_than() { 
  local max=$(($SECONDS+$1))
  shift;
  exec 3>&1 4>&2
  local out=$((time 1>&3 2>&4 "$@") 2>&1)
  [ "$SECONDS" -lt "$max" ] || echo "$out" >&2
}

Usage:

$ time_silent_if_less_than 10 sh -c "sleep 5 ; echo stdout && echo stderr >&2" 
stdout
stderr
$ time_silent_if_less_than 10 sh -c "sleep 15 ; echo stdout && echo stderr >&2" 
stdout
stderr

real	0m15.006s
user	0m0.001s
sys	0m0.005s
$ time_silent_if_less_than 2 sh -c "sleep 65 ; echo stdout && echo stderr >&2" 
stdout
stderr

real	1m5.007s
user	0m0.001s
sys	0m0.006s

Variation:

time_silent_if_less_than() { 
  local max=$(($SECONDS+$1))
  shift;
  exec 3>&1 4>&2
  local out=$((time 1>&3 2>&4 "$@") 2>&1)
  [ "$SECONDS" -lt "$max" ] || echo $out >&2
}
$ time_silent_if_less_than 10 sh -c "sleep 15 ; echo stdout && echo stderr >&2" 
stdout
stderr
real 0m15.006s user 0m0.000s sys 0m0.006s

mkoeppe · 2024-04-21T17:22:47Z

It seems this kind of case by case handling might lead to issues later.

What "issues" could that possibly be?

tornaria · 2024-04-21T17:36:53Z

It seems this kind of case by case handling might lead to issues later.

What "issues" could that possibly be?

I don't know, someone wants to change something about this code, and has to be aware of the 3-4 different versions of the code. Just like #37391 was only tested on mac and seemed to work fine, having different implementations for different platforms is a risk. Since everything can e implemented with bash, we just defer to bash having the same behavior on the different platforms.

mkoeppe · 2024-04-22T22:54:57Z

having different implementations for different platforms is a risk

Based on my experience with portability work, let me just say that I don't find this believable.

mkoeppe · 2024-04-22T22:56:25Z

Since everything can be implemented with bash, we just defer to bash having the same behavior on the different platforms.

Let's check in with our most prominent antibashist (#29345, #29344, #30128) in our project. @orlitzky, any thoughts?

tornaria · 2024-04-22T23:30:15Z

Note that $SECONDS can be replaced by $(date +%s) if you are concerned about that.

orlitzky · 2024-04-22T23:51:56Z

Bash is fine so long as the shebang doesn't say #!/bin/sh. If bash makes this easy to fix, then I would use bash.

In case it helps, the comments to the effect that bash time can't redirect to a file aren't quite right. For example (in bash),

$ (time echo "hello world!") 2> derp
hello world!
$ cat derp

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

Problem is, this will redirect stderr for the inner command, too. I'm sure there's a way around it by juggling file descriptors.

tornaria · 2024-04-22T23:57:09Z

Bash is fine so long as the shebang doesn't say #!/bin/sh. If bash makes this easy to fix, then I would use bash.

In case it helps, the comments to the effect that bash time can't redirect to a file aren't quite right. For example (in bash),
$ (time echo "hello world!") 2> derp
hello world!
$ cat derp

real	0m0.000s
user	0m0.000s
sys	0m0.000s
Problem is, this will redirect stderr for the inner command, too. I'm sure there's a way around it by juggling file descriptors.

Here: #37840 (comment)

orlitzky · 2024-04-23T00:33:21Z

Here: #37840 (comment)

Mere inches above where I was typing, the perfect hiding place. It's not any more readable but I would bet that the bash version is more portable.

kwankyu · 2024-05-10T07:03:37Z

A compromise

time_cmd() {
    exec 3>&1 4>&2
    local time=$({ time sh -c "$@" 1>&3 2>&4; } 2>& 1 )
    echo "$time" > $timefile
}

report_time() {
    local time=$(echo $(cat $timefile 2>/dev/null))
    if [[ $time =~ real\ ([0-9]+)m([0-9]+)\.[0-9]+s ]]; then
        local minutes="${BASH_REMATCH[1]}"
        local seconds="${BASH_REMATCH[2]}"
        total_seconds=$((minutes * 60 + seconds))
        if (( total_seconds >= 10 )); then
            echo "$time"
        fi
    fi
}

Would this work?

tornaria · 2024-05-10T13:53:15Z

A compromise

time_cmd() {
    exec 3>&1 4>&2
    local time=$({ time sh -c "$@" 1>&3 2>&4; } 2>& 1 )
    echo "$time" > $timefile
}

report_time() {
    local time=$(echo $(cat $timefile 2>/dev/null))
    if [[ $time =~ real\ ([0-9]+)m([0-9]+)\.[0-9]+s ]]; then
        local minutes="${BASH_REMATCH[1]}"
        local seconds="${BASH_REMATCH[2]}"
        total_seconds=$((minutes * 60 + seconds))
        if (( total_seconds >= 10 )); then
            echo "$time"
        fi
    fi
}

Would this work?

LGTM. Two comments:

if we are using bash specifics anyway, using $SECONDS to detect whether 10 seconds have elapsed seems easier and cleaner (no parsing)
the reporting of time can be done inside time_cmd() itself, avoiding saving through a file, and the caller doesn't need to know about it. You just get a time_cmd which prints the time only if more than 10 seconds.

This is more or less what I proposed here:
#37840 (comment)

if you don't like the extra parameter, you can hardcode "10" there. Something like:

time_cmd() { 
    local start_seconds=$SECONDS
    exec 3>&1 4>&2
    local time=$({ time sh -c "$@" 1>&3 2>&4; } 2>& 1 )
    local total_seconds=$(($SECONDS - $start_seconds))
    if (( total_seconds >= 10 )); then
        echo "$time"
    fi
}

kwankyu · 2024-05-10T22:23:13Z

if we are using bash specifics anyway, using $SECONDS to detect whether 10 seconds have elapsed seems easier and cleaner (no parsing)

the reporting of time can be done inside time_cmd() itself, avoiding saving through a file, and the caller doesn't need to know about it. You just get a time_cmd which prints the time only if more than 10 seconds.

My variant is a compromise, in the sense that the suggested commands can be replaced with Matthias' time_cmd() and report_time().

Anyway, this PR is Matthias's. He is free to adopt whatever we suggest or not.

mkoeppe · 2024-05-16T20:50:04Z

Finally coming back to this PR. Thanks all for the suggestions. I'm preparing a version that adapts from the suggested solutions that use the bash keyword time and output redirection.

kwankyu

Works well. LGTM. Thanks.

mkoeppe · 2024-05-17T17:03:20Z

Thanks!

…sh keyword `time`       Follow-up after - sagemath#37391 - sagemath#37785 ... to make the display of package build times available on Linux too. Fixes sagemath#37785 (comment), closes sagemath#37832. ### 📝 Checklist  - [x] The title is concise and informative. - [x] The description explains in detail what this PR is about. - [x] I have linked a relevant issue or discussion. - [ ] I have created tests covering the changes. - [ ] I have updated the documentation and checked the documentation preview. ### ⌛ Dependencies    - Depends on sagemath#37785 URL: sagemath#37840 Reported by: Matthias Köppe Reviewer(s): Kwankyu Lee

tornaria · 2024-05-18T18:27:34Z

build/bin/sage-logger

+    local out
+    TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1)
+    local retstat=$?
+    [ "$SECONDS" -lt "$max" ] || echo "$TIME_OUTPUT" > "$timefile"


Suggested change

[ "$SECONDS" -lt "$max" ] || echo "$TIME_OUTPUT" > "$timefile"

[ "$SECONDS" -lt "$max" ] || echo "$TIME_OUTPUT" >&2

you don't really need to go via "$timefile", do you?

It seems more natural if time_cmd has similar semantics/usage as regular time (except the time is only printed out if >= 10s).

Yes, I do. This thing runs in a subshell.

My point is: print to stderr instead of saving to a file. What's wrong with that? Saves a point of failure (communication via filesystem).

From my experience as the principal maintainer of the Sage distro build system, let me just say that this concern ("point of failure") is wildly beside the point.

tornaria · 2024-05-18T18:29:31Z

build/bin/sage-logger

@@ -94,8 +92,7 @@ if [ -n "$SAGE_SILENT_BUILD" -a ${use_prefix} = true ]; then
    # Silent build.
    # Similar to https://www.gnu.org/software/automake/manual/html_node/Automake-Silent-Rules.html#Automake-Silent-Rules
    echo "[$logname] installing. Log file: $logfile"
-    ( exec>> $logfile 2>&1 ; $TIME sh -c "$cmd"; status=$?;
-      [ -r $timefile ] && cat $timefile; exit $status )
+    ( exec>> $logfile 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status )


Suggested change

( exec>> $logfile 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status )

( exec>> $logfile 2>&1; time_cmd "$cmd" )

or even maybe

Suggested change

( exec>> $logfile 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status )

time cmd "$cmd" >> $logfile 2>&$1

Also, in L104 below, the time is reported again.

One goes to the logfile. One goes to the terminal.

tornaria · 2024-05-18T18:30:20Z

build/bin/sage-logger

-    ( exec 2>&1;
-      $TIME sh -c "$cmd"; status=$?; report_time;
-      exit $status ) | \
+    ( exec 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status ) | \


same here...

tornaria · 2024-05-18T18:44:57Z

build/bin/sage-logger

+time_cmd() {
+    local max=$(($SECONDS+10))
+    exec 3>&1 4>&2
+    local out


thanks, I'll clean this one up in a follow up.

This is done in #38026.

tornaria · 2024-05-18T18:45:33Z

build/bin/sage-logger

+    TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1)
+    local retstat=$?


Suggested change

TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1)

local retstat=$?

local TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1) retstat=$?

if you want't TIME_OUTPUT to be local, this is one way.

OTOH, if you keep TIME_OUTPUT global you can use it instead of timefile.

kwankyu · 2024-05-18T23:06:54Z

@tornaria Thanks for reviewing and for additional comments. But let me express my worries about certain attitude of reviewers that I am observing recently. First my apologies for making remarks toward fellow reviewers, which I usually don't.

From our doc on "reviewing", we see

“The perfect is the enemy of the good”

The point of the review is to ensure that the Sage code guidelines are followed and that the implementation is mathematically correct. Please refrain from additional feature requests or open-ended discussion about alternative implementations. If you want the code written differently, your suggestion should be a clear and actionable request.

We develop sage "incrementally". A PR should be good enough to be accepted, but it need not be "perfect" from one reviewer's point of view. If the reviewer has an idea to improve the code further, then he can open up his own PR building on the present PR, implementing the idea.

If I have mistaken your good intention, then my apologies again.

tornaria · 2024-05-19T21:21:35Z

If I have mistaken your good intention, then my apologies again.

I don't understand what you mean.

I'll make sure in the future to keep my 2c to myself.

@jhpalmieri

- Clean up after sagemath#37391, which used `sage-logger` for prefixing output; generating the log/time files was a side effect, which has not proven to be useful - Fixes sagemath#37887 @jhpalmieri ### 📝 Checklist  - [x] The title is concise and informative. - [x] The description explains in detail what this PR is about. - [x] I have linked a relevant issue or discussion. - [ ] I have created tests covering the changes. - [ ] I have updated the documentation and checked the documentation preview. ### ⌛ Dependencies    - Depends on sagemath#37840 (merged here) URL: sagemath#38026 Reported by: Matthias Köppe Reviewer(s): Kwankyu Lee, Matthias Köppe

@jhpalmieri

- Clean up after sagemath#37391, which used `sage-logger` for prefixing output; generating the log/time files was a side effect, which has not proven to be useful - Fixes sagemath#37887 @jhpalmieri ### 📝 Checklist  - [x] The title is concise and informative. - [x] The description explains in detail what this PR is about. - [x] I have linked a relevant issue or discussion. - [ ] I have created tests covering the changes. - [ ] I have updated the documentation and checked the documentation preview. ### ⌛ Dependencies    - Depends on sagemath#37840 (merged here) URL: sagemath#38026 Reported by: Matthias Köppe Reviewer(s): Kwankyu Lee, Matthias Köppe

mkoeppe added p: minor / 4 c: build labels Apr 20, 2024

mkoeppe self-assigned this Apr 20, 2024

mkoeppe added the s: needs review label Apr 20, 2024

mkoeppe requested a review from tornaria April 20, 2024 23:45

mkoeppe marked this pull request as ready for review April 20, 2024 23:45

mkoeppe added this to the sage-10.4 milestone May 14, 2024

mkoeppe changed the title ~~sage-logger: Handle more flavors of time, not just macOS/FreeBSD~~ sage-logger: Replace use of /usr/bin/time by bash keyword time May 16, 2024

build/bin/sage-logger: Replace use of /usr/bin/time by bash keyword time

ffa4f46

mkoeppe force-pushed the no_time_h branch from df0228c to ffa4f46 Compare May 16, 2024 21:08

github-actions bot added the v: minimal label May 16, 2024

kwankyu approved these changes May 17, 2024

View reviewed changes

kwankyu added s: positive review and removed s: needs review labels May 17, 2024

tornaria reviewed May 18, 2024

View reviewed changes

vbraun merged commit b13df98 into sagemath:develop May 25, 2024
21 of 22 checks passed

github-actions bot removed the s: positive review label May 25, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`sage-logger`: Replace use of `/usr/bin/time` by bash keyword `time` #37840

`sage-logger`: Replace use of `/usr/bin/time` by bash keyword `time` #37840

mkoeppe commented Apr 20, 2024

github-actions bot commented Apr 20, 2024 •

edited

Loading

tornaria commented Apr 21, 2024

mkoeppe commented Apr 21, 2024

tornaria commented Apr 21, 2024

mkoeppe commented Apr 22, 2024

mkoeppe commented Apr 22, 2024

tornaria commented Apr 22, 2024

orlitzky commented Apr 22, 2024

tornaria commented Apr 22, 2024

orlitzky commented Apr 23, 2024

kwankyu commented May 10, 2024

tornaria commented May 10, 2024

kwankyu commented May 10, 2024

mkoeppe commented May 16, 2024

kwankyu left a comment •

edited

Loading

mkoeppe commented May 17, 2024

tornaria May 18, 2024

mkoeppe May 18, 2024

tornaria May 18, 2024

mkoeppe May 18, 2024

tornaria May 18, 2024

mkoeppe May 18, 2024

tornaria May 18, 2024

tornaria May 18, 2024

mkoeppe May 18, 2024

mkoeppe May 18, 2024

tornaria May 18, 2024

kwankyu commented May 18, 2024

tornaria commented May 19, 2024

	[ "$SECONDS" -lt "$max" ] \|\| echo "$TIME_OUTPUT" > "$timefile"
	[ "$SECONDS" -lt "$max" ] \|\| echo "$TIME_OUTPUT" >&2

	( exec>> $logfile 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status )
	( exec>> $logfile 2>&1; time_cmd "$cmd" )

	( exec>> $logfile 2>&1; time_cmd "$cmd"; status=$?; report_time; exit $status )
	time cmd "$cmd" >> $logfile 2>&$1

		TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1)
		local retstat=$?

	TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1)
	local retstat=$?
	local TIME_OUTPUT=$((time 1>&3 2>&4 sh -c "$1") 2>&1) retstat=$?

sage-logger: Replace use of /usr/bin/time by bash keyword time #37840

sage-logger: Replace use of /usr/bin/time by bash keyword time #37840

Conversation

mkoeppe commented Apr 20, 2024

📝 Checklist

⌛ Dependencies

github-actions bot commented Apr 20, 2024 • edited Loading

tornaria commented Apr 21, 2024

mkoeppe commented Apr 21, 2024

tornaria commented Apr 21, 2024

mkoeppe commented Apr 22, 2024

mkoeppe commented Apr 22, 2024

tornaria commented Apr 22, 2024

orlitzky commented Apr 22, 2024

tornaria commented Apr 22, 2024

orlitzky commented Apr 23, 2024

kwankyu commented May 10, 2024

tornaria commented May 10, 2024

kwankyu commented May 10, 2024

mkoeppe commented May 16, 2024

kwankyu left a comment • edited Loading

Choose a reason for hiding this comment

mkoeppe commented May 17, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kwankyu commented May 18, 2024

tornaria commented May 19, 2024

`sage-logger`: Replace use of `/usr/bin/time` by bash keyword `time` #37840

`sage-logger`: Replace use of `/usr/bin/time` by bash keyword `time` #37840

github-actions bot commented Apr 20, 2024 •

edited

Loading

kwankyu left a comment •

edited

Loading