isabelle: Admin/isatest/isatest-stats@c192ba6e6e5d (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
49938 1c06f8d244af ignore old stuff and thus speed up the script greatly; wenzelm parents: 49310 diff changeset	9	PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 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
46988 9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP; wenzelm parents: 46651 diff changeset	35	HOL-Matrix_LP
45194 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
46651 1258eab48270 updated stats according to src/HOL/IsaMakefile; wenzelm parents: 45888 diff changeset	55	HOL-Quickcheck_Examples
45194 d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	56	HOL-Quotient_Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	57	HOL-SET_Protocol
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	58	HOL-SPARK
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	59	HOL-SPARK-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	60	HOL-SPARK-Manual
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	61	HOL-Statespace
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	62	HOL-TPTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	63	HOL-UNITY
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	64	HOL-Unix
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	65	HOL-Word
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	66	HOL-Word-Examples
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	67	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	68	HOL-ZF
45194 d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	69	HOL-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	70	HOL4
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	71	HOLCF
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	72	HOLCF-FOCUS
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	73	HOLCF-IMP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	74	HOLCF-Library
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	75	HOLCF-Tutorial
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	76	HOLCF-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	77	IOA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	78	IOA-ABP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	79	IOA-NTP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	80	IOA-Storage
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	81	IOA-ex
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	82	TLA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	83	TLA-Buffer
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	84	TLA-Inc
45888 66b419de5f38 more stats; wenzelm parents: 45194 diff changeset	85	TLA-Memory
66b419de5f38 more stats; wenzelm parents: 45194 diff changeset	86	HOL-Datatype_Benchmark
66b419de5f38 more stats; wenzelm parents: 45194 diff changeset	87	HOL-Record_Benchmark"
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	88
45194 d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	89	AFP_SESSIONS="
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	90	ArrowImpossibilityGS
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	91	Coinductive
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	92	CoreC++
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	93	HOL-AVL-Trees
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	94	HOL-Abstract-Hoare-Logics
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	95	HOL-Abstract-Rewriting
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	96	HOL-BinarySearchTree
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	97	HOL-Binomial-Heaps
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	98	HOL-Binomial-Queues
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	99	HOL-BytecodeLogicJmlTypes
49310 6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals" blanchet parents: 47044 diff changeset	100	HOL-Cardinals
45194 d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	101	HOL-Category
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	102	HOL-Category2
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	103	HOL-Cauchy
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	104	HOL-ClockSynchInst
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	105	HOL-CofGroups
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	106	HOL-Collections
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	107	HOL-Compiling-Exceptions-Correctly
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	108	HOL-Completeness
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	109	HOL-DPT-SAT-Solver
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	110	HOL-DataRefinementIBP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	111	HOL-Depth-First-Search
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	112	HOL-DiskPaxos
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	113	HOL-Example-Submission
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	114	HOL-FFT
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	115	HOL-FOL-Fitting
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	116	HOL-FeatherweightJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	117	HOL-FileRefinement
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	118	HOL-FinFun
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	119	HOL-Finger-Trees
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	120	HOL-Flyspeck-Tame
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	121	HOL-Free-Boolean-Algebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	122	HOL-Free-Groups
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	123	HOL-FunWithFunctions
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	124	HOL-FunWithTilings
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	125	HOL-Functional-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	126	HOL-Gauss-Jordan-Elim-Fun
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	127	HOL-GenClock
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	128	HOL-General-Triangle
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	129	HOL-GraphMarkingIBP
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	130	HOL-HotelKeyCards
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	131	HOL-Huffman
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	132	HOL-Integration
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	133	HOL-JiveDataStoreModel
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	134	HOL-KBPs
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	135	HOL-Lazy-Lists-II
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	136	HOL-LightweightJava
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	137	HOL-List-Index
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	138	HOL-Locally-Nameless-Sigma
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	139	HOL-Marriage
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	140	HOL-Matrix
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	141	HOL-Max-Card-Matching
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	142	HOL-MiniML
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	143	HOL-MuchAdoAboutTwo
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	144	HOL-Multivariate_Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	145	HOL-Myhill-Nerode
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	146	HOL-Nominal
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	147	HOL-Nominal-Lam-ml-Normalization
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	148	HOL-Nominal-SequentInvertibility
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	149	HOL-Ordinal
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	150	HOL-POPLmark-deBruijn
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	151	HOL-Perfect-Number-Thm
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	152	HOL-Polynomials
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	153	HOL-Presburger-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	154	HOL-Program-Conflict-Analysis
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	155	HOL-Ramsey-Infinite
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	156	HOL-Recursion-Theory-I
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	157	HOL-Regular-Sets
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	158	HOL-Robbins-Conjecture
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	159	HOL-SATSolverVerification
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	160	HOL-SIFPL
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	161	HOL-SenSocialChoice
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	162	HOL-Statecharts
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	163	HOL-Topology
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	164	HOL-Transitive-Closure
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	165	HOL-Tree-Automata
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	166	HOL-Verified-Prover
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	167	HOL-Word
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	168	HOL-Word-RIPEMD-160-SPARK
47044 1ab41ea5b1c6 more stats; wenzelm parents: 46988 diff changeset	169	HOL-Word-JinjaThreads-Basic-JinjaThreads
45194 d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	170	HOLCF
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	171	HOLCF-Shivers-CFA
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	172	HOLCF-Stream-Fusion
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	173	HOLCF-WorkerWrapper
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	174	HRB-Slicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	175	HRB-Slicing-InformationFlowSlicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	176	Jinja
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	177	LatticeProperties
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	178	LatticeProperties-MonoBoolTranAlgebra
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	179	LatticeProperties-PseudoHoops
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	180	Lower_Semicontinuous
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	181	NormByEval
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	182	Simpl
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	183	Simpl-BDD
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	184	Slicing
d825a8f1d088 further cleanup of stats (cf. 97e81a8aa277); wenzelm parents: 45142 diff changeset	185	Slicing-InformationFlowSlicing
45142 97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	186	VolpanoSmith"
97e81a8aa277 more complete stats, including small sessions which provide some clues on main HOL baseline performance; wenzelm parents: 44993 diff changeset	187
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	188
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	189	for PLATFORM in $PLATFORMS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	190	do
24831 887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	191	if [ "$PLATFORM" = afp ]; then
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	192	SESSIONS="$AFP_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	193	else
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	194	SESSIONS="$ISABELLE_SESSIONS"
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	195	fi
887d1b32a1a5 cover AFP logs as well, using "afp" pseudo-platform; wenzelm parents: 24489 diff changeset	196
22410 da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	197	"$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	198	cat > "stats/$PLATFORM.html" <<EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	199	<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	200	<html>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	201	<head><title>Development Snapshot -- Performance Statistics</title></head>
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	<body>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	204	<h1>$PLATFORM</h1>
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	205	EOF
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	206
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	207	for SESSION in $SESSIONS
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	208	do
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	209	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	210	done
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	211
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	212	echo "</body>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	213	echo "</html>" >> "stats/$PLATFORM.html"
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	214
da313b67a04d moved all isatest/cron job related files to own directory kleing parents: diff changeset	215	done

author	wenzelm
	Sun, 02 Dec 2012 22:20:12 +0100
changeset 50314	c192ba6e6e5d
parent 49938	1c06f8d244af
child 51059	c6a74742f8fe
permissions	-rwxr-xr-x