diff -r a7b3ab44d993 -r 887d1b32a1a5 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Thu Oct 04 14:42:47 2007 +0200 +++ b/Admin/isatest/isatest-stats Thu Oct 04 16:21:31 2007 +0200 @@ -7,8 +7,9 @@ THIS=$(cd "$(dirname "$0")"; pwd -P) -PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e at-poly-5.1-para-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e" -SESSIONS="\ +PLATFORMS="at-poly at-sml-dev at64-poly-e at64-poly-5.1-para-e at-mac-poly-5.1-para-e afp" + +ISABELLE_SESSIONS="\ HOL \ HOL-Algebra \ HOL-Auth \ @@ -30,8 +31,27 @@ ZF-Constructible\ ZF-UNITY" +AFP_SESSIONS="\ + CoreC++\ + HOL-DiskPaxos\ + HOL-Fermat3_4\ + HOL-Flyspeck-Tame\ + HOL-Group-Ring-Module\ + HOL-Jinja\ + HOL-JiveDataStoreModel\ + HOL-POPLmark-deBruijn\ + HOL-RSAPSS\ + HOL-SumSquares\ + HOL-Valuation" + for PLATFORM in $PLATFORMS do + if [ "$PLATFORM" = afp ]; then + SESSIONS="$AFP_SESSIONS" + else + SESSIONS="$ISABELLE_SESSIONS" + fi + "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS cat > "stats/$PLATFORM.html" <