regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
#!/usr/bin/env perl
#
# Author: Makarius
#
# DESCRIPTION: Simple report generator for Poly/ML profiling output.
use strict;
my %log = ();
my @output = ();
while (<ARGV>) {
if (m,^([ 0-9]{10}) (\S+$|GARBAGE COLLECTION.*$),) {
my $count = $1;
my $fun = $2;
$fun =~ s,-?\(\d+\).*$,,g;
$fun =~ s,/\d+$,,g;
if ($count =~ m,^\s*(\d)+$,) {
if (defined($log{$fun})) {
$log{$fun} += $count;
} else {
$log{$fun} = $count;
}
}
}
}
foreach my $fun (keys %log) {
push @output, (sprintf "%14u %s\n", $log{$fun}, $fun);
}
print (sort @output);