To profile code in AKCL-based HOL:

  1) compile the file profile.lsp:

     #lisp `(compile-file "profile")`;;

  2) load it in:

     #lisp `(load "profile")`;;

  3) initialise the profiler:

     #set_up_profile();;

     "making new array" 
     Loaded c and other function addresses
     Using profile-array length 10000000 
     Use (si::prof 0 90) to start and (prof 0 0) to stop:
     This starts monitoring at address 0 
     thru byte (256/90)*(length *profile-array*)
     (si::display-prof) displays the results() : void

  4) turn on the profiler:

     #start_profile();;

  5) run your code. E.g:

     #funpow 1000 (\x.x+1) 0;;
     1000 : int

  6) display the profiling results:

     #display_profile();;

       6.25% (    1): _make_cons
       6.25% (    1): _funcall
      18.75% (    3): _eval
      12.50% (    2): _lambda_bind
       6.25% (    1): _bind_var
       6.25% (    1): _number_compare
       6.25% (    1): _listA
       6.25% (    1): CAR
       6.25% (    1): SYSTEM::BEST-ARRAY-ELEMENT-TYPE
       6.25% (    1): _sigsetjmp
       6.25% (    1): _write
       6.25% (    1): ASSQ1
       6.25% (    1): PARSE-LEVEL
     Total ticks 16() : void

     These results may be sorted using the GNUemacs command M-x sort-columns
     after marking the region in which the numbers appear.

  7) turn off the profiler:

     #end_profile();;

     NOTE: turning off the profiler causes display_profile to not give
     correct output.  Always display the results before turning off the
     profiler.

  8) The profiler may be re-initialised by the command:

     #clear_profile();;

  9) The results generated by display_profile may contain references to
     generic function names (FUN%xxxx%yyy).  These names represent the
     lisp function that an ML function was compiled to.  A mapping table
     from lisp to ML function names may be had by invoking the command:

     #make_map_table();;

     Entries of the form:

     FUN%7247%128 = save_top_thm

     will appear.  It may, however, be the case that a symbolic function
     name does not appear in the table.  Say, for instance, that 
     FUN%7247%127 appeared in the profiled results.  Odds are that it
     is a lambda-binding associated with save_top_thm.  Unfortunately,
     it is not possible to extract these lambdas as they are in compiled
     functions.  So, it is up to the user to interpolate the table
     entries a bit.