build/bin/sage-logger: Show build time if >= 10 seconds

Author: Matthias Koeppe

build/bin/sage-logger

@@ -61,6 +61,14 @@ else
     SED=cat
 fi
 
+timefile="$logdir/$logname.time"
+rm -f "$timefile"
+if /usr/bin/time -p -o /dev/null true; then
+    TIME="/usr/bin/time -p -o $timefile"
+else
+    TIME=""
+fi
+
 mkdir -p "$logdir"
 
 # Do all logging of child processes with V=1 to ensure that no
@@ -75,12 +83,15 @@ 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 ; eval "$cmd" )
+    ( exec>> $logfile 2>&1 ; $TIME sh -c "$cmd"; status=$?;
+      [ -r $timefile ] && cat $timefile; exit $status )
     status=$?
     if [[ $status != 0 ]]; then
         echo "  [$logname] error installing, exit status $status. End of log file:"
         tail -n 120 "$logfile" | sed "/Please email sage-devel/,$ d;s;^;  [$logname]   ;" >&2
         echo "  [$logname] Full log file: $logfile"
+    elif grep -q 'real [1-9][0-9]' $timefile 2>/dev/null; then  # at least 10 seconds
+        echo "  [$logname] successfully installed ($(echo $(cat $timefile)))."
     else
         echo "  [$logname] successfully installed."
     fi
@@ -90,7 +101,10 @@ else
     # We trap SIGINT such that SIGINT interrupts the main process being
     # run, not the logging.
 
-    ( exec 2>&1; eval "$cmd" ) | \
+    ( exec 2>&1;
+      $TIME sh -c "$cmd"; status=$?;
+      if grep -q 'real [1-9][0-9]' $timefile 2>/dev/null; then echo $(echo $(cat $timefile)); fi;
+      exit $status ) | \
         ( trap '' SIGINT; if [ -n "$GITHUB_ACTIONS" -a -n "$prefix" ]; then echo "::group::${logname}"; fi; tee -a "$logfile" | $SED; if [ -n "$GITHUB_ACTIONS" -a -n "$prefix" ]; then echo "::endgroup::"; fi )
 
     pipestatus=(${PIPESTATUS[*]})

build/make/install

@@ -103,7 +103,7 @@ EOF
 ###############################################################################
 # NOW do the actual build:
 ###############################################################################
-time $MAKE "$@"
+$MAKE "$@"
 if [ $? -ne 0 ]; then
     cat >&2 <<EOF
 ***************************************************************