Re: suggestion: timer format

[Bill Allombert <Bill.Allombert@math.u-bordeaux.fr>]

On Fri, Oct 21, 2022 at 04:40:07PM +0200, Markus Grassl wrote:
> Dear Ruud,
> 
> Thanks for the detailed explanation.
> 
> My question was to some extent triggered by laziness.
> 
> In my code, I just enable the built-in timing information using
> 
>   default(timer,1)
> 
> which will reported both the total CPU time and the wall clock (real time)
> spent on commands, e.g.,
> 
>   cpu time = 73h, 13min, 28,457 ms, real time = 2h, 12,222 ms.

Note that you can use %# to get the timing as a number of milli-second instead.

If we want to allow the display to be changed that, we should probably use
strftime.

Cheers,
Bill.