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

author	wenzelm
	Wed, 19 Oct 2011 14:40:49 +0200
changeset 45194	d825a8f1d088
parent 45142	97e81a8aa277
child 45888	66b419de5f38
permissions	-rwxr-xr-x