Admin/profiling_reports
author boehmes
Wed, 12 May 2010 23:54:00 +0200
changeset 36896 c030819254d3
parent 36859 51af1657263b
child 44152 a07748619f53
permissions -rwxr-xr-x
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23604
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     2
#
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     3
# Author: Makarius
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     4
#
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: Cumulative reports for Poly/ML profiling output.
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     6
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     7
THIS=$(cd $(dirname "$0"); echo "$PWD")
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     8
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
     9
SRC="$1"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    10
DST="$2"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    11
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    12
mkdir -p "$DST"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    13
24856
f06829479407 cover only .gz files;
wenzelm
parents: 23604
diff changeset
    14
for FILE in "$SRC"/*.gz
23604
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    15
do
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    16
  echo "$FILE"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    17
  NAME="$(basename "$FILE" .gz)"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    18
  gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
56f945f1ed50 Cumulative reports for Poly/ML profiling output.
wenzelm
parents:
diff changeset
    19
done