Carry out a computation, returning (not just printing!) how long it took and (on supported Lisps) how many bytes were allocated.
In most cases, you don't really need to do this. Instead, see time$, which is built into ACL2 and allows you to print the runtime and allocation of a form as a logically invisible side-effect. Since time$ doesn't return the elapsed time or allocation, it is simpler and doesn't need access to state. It also has some nice features for controlling when timing information is printed.
On the other hand, if you want to do things like collect up tables that
describe how your functions perform on various inputs, then time$ won't
do what you want: it just prints the timing information to the terminal,
leaving you with no way to collect and compare the times and allocations. In
(oracle-time (fib 35)) ; Simple since it returns a single value --> (mv time ; Rational, number of seconds bytes ; Natural, bytes allocated ans ; Answer from (fib 35) state) ; Updated state
(oracle-time (random$ 100 state) ; Returns multiple values :ret (mv ans state)) ; Explains the return type --> (mv time ; Rational, number of seconds bytes ; Natural, bytes allocated ans ; The random number produced state) ; Updated state
See also the file
(oracle-time form [:ret retspec])
The return value of
(mv-let retspec form (b* (((mv & time state) (read-acl2-oracle state)) ((mv & bytes state) (read-acl2-oracle state))) (mv time bytes retspec [state])))
You can see here that the