isabelle: Admin/isatest/isatest-stats@97e81a8aa277 (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
44152 a07748619f53 somewhat more uniform THIS; wenzelm parents: 42461 diff changeset	7	THIS="$(cd "$(dirname "$0")"; pwd)"
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	8
44993 9a2d100dd3eb more isatest stats; wenzelm parents: 44152 diff changeset	9	PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 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="\
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	12	HOL-Auth \
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	13	HOL-Bali \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	14	HOL-Boogie-Examples \
30111 01a87bc13415 include HOL-Decision_Procs in stats; wenzelm parents: 29283 diff changeset	15	HOL-Decision_Procs \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	16	HOL-Hahn_Banach \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	17	HOL-Hoare \
33072 ae416aebbb75 updated session name; wenzelm parents: 33028 diff changeset	18	HOL-Hoare_Parallel \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	19	HOL-IMPP \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	20	HOL-IOA \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	21	HOL-Imperative_HOL \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	22	HOL-Import \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	23	HOL-Induct \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	24	HOL-Isar_Examples \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	25	HOL-Lattice \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	26	HOL-Library-Codegenerator_Test \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	27	HOL-Matrix \
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 32633 diff changeset	28	HOL-Metis_Examples \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	29	HOL-MicroJava \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	30	HOL-Mirabelle \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	31	HOL-Mutabelle \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	32	HOL-NanoJava \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	33	HOL-Nitpick_Examples \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	34	HOL-Nominal-Examples
32633 4ba4bfa08749 adjusted to new Number Theory scenario haftmann parents: 32421 diff changeset	35	HOL-Number_Theory \
4ba4bfa08749 adjusted to new Number Theory scenario haftmann parents: 32421 diff changeset	36	HOL-Old_Number_Theory \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	37	HOL-Predicate_Compile_Examples \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	38	HOL-Probability
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	39	HOL-Prolog \
34237 225daff4323b updated stats; wenzelm parents: 33264 diff changeset	40	HOL-Proofs-Extraction \
225daff4323b updated stats; wenzelm parents: 33264 diff changeset	41	HOL-Proofs-Lambda \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	42	HOL-Proofs-ex \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	43	HOL-Quotient_Examples \
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	44	HOL-SET_Protocol \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	45	HOL-SPARK-Examples \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	46	HOL-SPARK-Manual \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	47	HOL-Statespace \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	48	HOL-TPTP \
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	49	HOL-UNITY \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	50	HOL-Unix \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	51	HOL-Word-Examples \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	52	HOL-Word-SMT_Examples \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	53	HOL-ZF
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	54	HOL-ex \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	55	HOLCF-FOCUS \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	56	HOLCF-IMP \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	57	HOLCF-Library \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	58	HOLCF-Tutorial \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	59	HOLCF-ex \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	60	IOA-ABP \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	61	IOA-NTP \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	62	IOA-Storage \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	63	IOA-ex \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	64	TLA-Buffer \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	65	TLA-Inc \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	66	TLA-Memory"
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	67
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	68	AFP_SESSIONS="\
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	69	ArrowImpossibilityGS \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	70	Coinductive \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	71	CoreC++ \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	72	HOL-AVL-Trees \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	73	HOL-Abstract-Hoare-Logics \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	74	HOL-Abstract-Rewriting \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	75	HOL-BinarySearchTree \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	76	HOL-Binomial-Heaps \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	77	HOL-Binomial-Queues \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	78	HOL-BytecodeLogicJmlTypes \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	79	HOL-Category \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	80	HOL-Category2 \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	81	HOL-Cauchy \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	82	HOL-ClockSynchInst \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	83	HOL-CofGroups \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	84	HOL-Collections \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	85	HOL-Compiling-Exceptions-Correctly \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	86	HOL-Completeness \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	87	HOL-DPT-SAT-Solver \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	88	HOL-DataRefinementIBP \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	89	HOL-Depth-First-Search \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	90	HOL-DiskPaxos \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	91	HOL-Example-Submission \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	92	HOL-FFT \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	93	HOL-FOL-Fitting \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	94	HOL-FeatherweightJava \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	95	HOL-FileRefinement \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	96	HOL-FinFun \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	97	HOL-Finger-Trees \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	98	HOL-Flyspeck-Tame \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	99	HOL-Free-Boolean-Algebra \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	100	HOL-Free-Groups \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	101	HOL-FunWithFunctions \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	102	HOL-FunWithTilings \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	103	HOL-Functional-Automata \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	104	HOL-Gauss-Jordan-Elim-Fun \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	105	HOL-GenClock \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	106	HOL-General-Triangle \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	107	HOL-GraphMarkingIBP \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	108	HOL-HotelKeyCards \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	109	HOL-Huffman \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	110	HOL-Integration \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	111	HOL-JiveDataStoreModel \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	112	HOL-KBPs \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	113	HOL-Lazy-Lists-II \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	114	HOL-LightweightJava \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	115	HOL-List-Index \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	116	HOL-Locally-Nameless-Sigma \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	117	HOL-Marriage \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	118	HOL-Matrix \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	119	HOL-Max-Card-Matching \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	120	HOL-MiniML \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	121	HOL-MuchAdoAboutTwo \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	122	HOL-Multivariate_Analysis \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	123	HOL-Myhill-Nerode \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	124	HOL-Nominal \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	125	HOL-Nominal-Lam-ml-Normalization \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	126	HOL-Nominal-SequentInvertibility \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	127	HOL-Ordinal \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	128	HOL-Ordinals_and_Cardinals \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	129	HOL-POPLmark-deBruijn \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	130	HOL-Perfect-Number-Thm \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	131	HOL-Polynomials \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	132	HOL-Presburger-Automata \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	133	HOL-Program-Conflict-Analysis \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	134	HOL-Ramsey-Infinite \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	135	HOL-Recursion-Theory-I \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	136	HOL-Regular-Sets \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	137	HOL-Robbins-Conjecture \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	138	HOL-SATSolverVerification \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	139	HOL-SIFPL \
f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	140	HOL-SenSocialChoice \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	141	HOL-Statecharts \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	142	HOL-Topology \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	143	HOL-Transitive-Closure \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	144	HOL-Tree-Automata \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	145	HOL-Verified-Prover \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	146	HOL-Word \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	147	HOL-Word-RIPEMD-160-SPARK \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	148	HOLCF \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	149	HOLCF-Shivers-CFA \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	150	HOLCF-Stream-Fusion \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	151	HOLCF-WorkerWrapper \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	152	HRB-Slicing \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	153	HRB-Slicing-InformationFlowSlicing \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	154	Jinja \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	155	Jinja \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	156	LatticeProperties \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	157	LatticeProperties-MonoBoolTranAlgebra \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	158	LatticeProperties-PseudoHoops \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	159	Lower_Semicontinuous \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	160	NormByEval \
29283 f4743512b12d updated sessions; wenzelm parents: 28602 diff changeset	161	Simpl \
37976 ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	162	Simpl-BDD \
ce2ea240895c more precise stats; wenzelm parents: 37160 diff changeset	163	Slicing \
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	164	Slicing \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	165	Slicing-InformationFlowSlicing \
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	166	VolpanoSmith"
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	167
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	168
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	169	for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	170	do
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	171	if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	172	SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	173	else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	174	SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	175	fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	176
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	177	"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	178	cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	179	<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	180	<html>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	181	<head><title>Development Snapshot -- Performance Statistics</title></head>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	182
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	183	<body>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	184	<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	185	EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	186
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	187	for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	188	do
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	189	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	190	done
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	191
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	192	echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	193	echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	194
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	195	done

author	wenzelm
	Fri, 14 Oct 2011 11:34:30 +0200
changeset 45142	97e81a8aa277
parent 44993	9a2d100dd3eb
child 45194	d825a8f1d088
permissions	-rwxr-xr-x