Admin/profiling_reports
author hoelzl
Wed, 01 Dec 2010 19:20:30 +0100
changeset 40859 de0b30e6c2d2
parent 36859 51af1657263b
child 44152 a07748619f53
permissions -rwxr-xr-x
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
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