agentultra/lean-4-hackers

lean-4-hackers's Issues

Measuring lean overhead?

The Lean4 version is about 10x slower than BSD wc on Apple Silicon. I will have to dig in tomorrow but I am guessing it is a combination of buffer size (5 seems small), and overhead in converting the buffer to a list before passing.

% /usr/bin/time -l cat mobydick.txt | ./build/bin/WordCount-lean
        0.08 real         0.00 user         0.00 sys
             1605632  maximum resident set size
                   0  average shared memory size
                   0  average unshared data size
                   0  average unshared stack size
                 180  page reclaims
                   2  page faults
                   0  swaps
                   0  block input operations
                   0  block output operations
                   0  messages sent
                   0  messages received
                   0  signals received
                  34  voluntary context switches
                  13  involuntary context switches
             7072637  instructions retired
             3438399  cycles elapsed
             1131264  peak memory footprint
Characters: 1276235 / Words: 218951 / Lines: 22317
% /usr/bin/time -l cat mobydick.txt | wc                        
        0.00 real         0.00 user         0.00 sys
             1605632  maximum resident set size
                   0  average shared memory size
                   0  average unshared data size
                   0  average unshared stack size
                 176  page reclaims
                   0  page faults
                   0  swaps
                   0  block input operations
                   0  block output operations
                   0  messages sent
                   0  messages received
                   0  signals received
                 130  voluntary context switches
                   2  involuntary context switches
             6196961  instructions retired
             3683665  cycles elapsed
             1114816  peak memory footprint
   22316  215864 1276235