isabelle: Admin/isatest/isatest-stats@83f3dc509068 (annotated)

22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	1	#!/usr/bin/env bash
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	2	#
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	3	# Author: Makarius
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	4	#
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	5	# DESCRIPTION: Standard statistics.
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	6
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	7	THIS=$(cd "$(dirname "$0")"; pwd -P)
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	8
41646 167a045fade4 more precise stats; wenzelm parents: 38561 diff changeset	9	PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	10
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	11	ISABELLE_SESSIONS="\
27448 28914fe628c8 moved HOL-Plain up; wenzelm parents: 27429 diff changeset	12	HOL-Plain \
28530 843b35caa8c4 added HOL-Main; wenzelm parents: 27478 diff changeset	13	HOL-Main \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	14	HOL \
34237 225daff4323b updated stats; wenzelm parents: 33264 diff changeset	15	HOL-Proofs \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	16	HOL-Library \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	17	HOL-Algebra \
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	18	HOL-Auth \
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	19	HOL-Bali \
30111 01a87bc13415 include HOL-Decision_Procs in stats; wenzelm parents: 29283 diff changeset	20	HOL-Decision_Procs \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	21	HOL-Hoare \
33072 ae416aebbb75 updated session name; wenzelm parents: 33028 diff changeset	22	HOL-Hoare_Parallel \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	23	HOL-Imperative_HOL \
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 32633 diff changeset	24	HOL-Metis_Examples \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	25	HOL-MicroJava \
34237 225daff4323b updated stats; wenzelm parents: 33264 diff changeset	26	HOL-Multivariate_Analysis \
27478 ac3b0f881d89 more sessions; wenzelm parents: 27448 diff changeset	27	HOL-NSA \
23443 fd8ffc8a5709 added HOL-Nominal-Examples; wenzelm parents: 22410 diff changeset	28	HOL-Nominal-Examples \
32633 4ba4bfa08749 adjusted to new Number Theory scenario haftmann parents: 32421 diff changeset	29	HOL-Number_Theory \
4ba4bfa08749 adjusted to new Number Theory scenario haftmann parents: 32421 diff changeset	30	HOL-Old_Number_Theory \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	31	HOL-Predicate_Compile_Examples \
34237 225daff4323b updated stats; wenzelm parents: 33264 diff changeset	32	HOL-Proofs-Extraction \
225daff4323b updated stats; wenzelm parents: 33264 diff changeset	33	HOL-Proofs-Lambda \
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	34	HOL-SET_Protocol \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	35	HOL-UNITY \
27478 ac3b0f881d89 more sessions; wenzelm parents: 27448 diff changeset	36	HOL-Word \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	37	HOL-Word-SMT_Examples \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	38	HOL-ex \
30616 ac79f1bb5db3 more stats; wenzelm parents: 30111 diff changeset	39	HOLCF \
ac79f1bb5db3 more stats; wenzelm parents: 30111 diff changeset	40	IOA \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	41	ZF \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	42	ZF-Constructible \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	43	ZF-UNITY"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	44
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	45	AFP_SESSIONS="\
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	46	Coinductive \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	47	CoreC++ \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	48	Group-Ring-Module \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	49	Group-Ring-Module-Valuation \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	50	HOL-BytecodeLogicJmlTypes \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	51	HOL-Collections \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	52	HOL-DiskPaxos \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	53	HOL-FeatherweightJava \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	54	HOL-Fermat3_4 \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	55	HOL-Flyspeck-Tame \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	56	HOL-Free-Groups \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	57	HOL-GraphMarkingIBP \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	58	HOL-JiveDataStoreModel \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	59	HOL-Locally-Nameless-Sigma \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	60	HOL-Ordinals_and_Cardinals \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	61	HOL-POPLmark-deBruijn \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	62	HOL-Presburger-Automata \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	63	HOL-Program-Conflict-Analysis \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	64	HOL-RSAPSS \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	65	HOL-Recursion-Theory-I \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	66	HOL-SATSolverVerification \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	67	HOL-SIFPL \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	68	HOL-SenSocialChoice \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	69	HOL-SumSquares \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	70	HOL-Topology \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	71	HOL-Tree-Automata \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	72	HOL-Word-JinjaThreads \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	73	HOLCF-WorkerWrapper \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	74	HRB-Slicing \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	75	Jinja \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	76	Jinja-Slicing \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	77	LinearQuantifierElim \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	78	Simpl \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	79	Simpl-BDD \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	80	Slicing \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	81	Slicing-InformationFlowSlicing"
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	82
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	83	for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	84	do
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	85	if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	86	SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	87	else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	88	SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	89	fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	90
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	91	"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	92	cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	93	<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	94	<html>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	95	<head><title>Development Snapshot -- Performance Statistics</title></head>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	96
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	97	<body>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	98	<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	99	EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	100
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	101	for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	102	do
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	103	echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	104	done
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	105
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	106	echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	107	echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	108
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	109	done

author	nipkow
	Tue, 22 Mar 2011 12:49:07 +0100
changeset 42059	83f3dc509068
parent 41646	167a045fade4
child 42461	56975de9e341
permissions	-rwxr-xr-x