Console Output

14:37:16 Started by upstream project "isabelle-repo" build number 858
14:37:16 originally caused by:
14:37:16  Started by an SCM change
14:37:16 [EnvInject] - Loading node environment variables.
14:37:16 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp
14:37:16 [isabelle-repo-afp] $ hg showconfig paths.default
14:37:16 [isabelle-repo-afp] $ hg pull --rev 10f4a17e5928b117654045afcba51782878adf5f
14:37:17 pulling from http://isabelle.in.tum.de/repos/isabelle/
14:37:17 searching for changes
14:37:17 adding changesets
14:37:17 adding manifests
14:37:17 adding file changes
14:37:17 added 4 changesets with 11 changes to 9 files
14:37:17 (run 'hg update' to get a working copy)
14:37:17 [isabelle-repo-afp] $ hg update --clean --rev 10f4a17e5928b117654045afcba51782878adf5f
14:37:17 9 files updated, 0 files merged, 1 files removed, 0 files unresolved
14:37:17 [isabelle-repo-afp] $ hg log --rev . --template {node}
14:37:17 [isabelle-repo-afp] $ hg log --rev . --template {rev}
14:37:17 [isabelle-repo-afp] $ hg id --branch
14:37:17 [afp] $ hg showconfig paths.default
14:37:17 [afp] $ hg pull --rev default
14:37:18 pulling from https://bitbucket.org/isa-afp/afp-devel/
14:37:18 searching for changes
14:37:18 adding changesets
14:37:18 adding manifests
14:37:18 adding file changes
14:37:18 added 4 changesets with 6 changes to 5 files
14:37:18 (run 'hg update' to get a working copy)
14:37:18 [afp] $ hg update --clean --rev default
14:37:19 354 files updated, 0 files merged, 0 files removed, 0 files unresolved
14:37:19 [afp] $ hg --config extensions.purge= clean --all
14:37:19 [afp] $ hg log --rev . --template {node}
14:37:19 [afp] $ hg log --rev . --template {rev}
14:37:19 No emails were triggered.
14:37:19 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson3944388363702434103.sh
14:37:19 + Admin/jenkins/run_build afp
14:37:19 + set -e
14:37:19 + PROFILE=afp
14:37:19 + shift
14:37:19 + bin/isabelle components -a
14:37:19 + bin/isabelle jedit -bf
14:37:19 ### Building Isabelle/Scala ...
14:37:48 ### Building Isabelle/jEdit ...
14:38:04 + bin/isabelle ci_build_afp
14:38:10 
14:38:10 === CONFIGURATION ===
14:38:10 
14:38:10 ISABELLE_BUILD_OPTIONS=""
14:38:10 
14:38:10 ML_PLATFORM="x86_64-linux"
14:38:10 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
14:38:10 ML_SYSTEM="polyml-5.6"
14:38:10 ML_OPTIONS="-H 4000 --maxheap 8G"
14:38:10 
14:38:10 === BUILD ===
14:38:10 
14:38:10 Build started at Mon, 24 Apr 2017 12:38:10 GMT
14:38:10 Isabelle id 10f4a17e5928
14:38:10 AFP id e95b688ce643
14:38:10 
14:38:10 === LOG ===
14:38:10 
14:38:11 Session Pure/Pure
14:38:12 Session HOL/HOL (main)
14:38:12 Session AFP/AVL-Trees (AFP)
14:38:12 Session AFP/AWN (AFP)
14:38:12 Session AFP/Abortable_Linearizable_Modules (AFP)
14:38:12 Session AFP/Abstract-Hoare-Logics (AFP)
14:38:12 Session AFP/Abstract-Rewriting (AFP)
14:38:12 Session AFP/Decreasing-Diagrams (AFP)
14:38:13 Session AFP/Decreasing-Diagrams-II (AFP)
14:38:13 Session AFP/Matrix (AFP)
14:38:13 Session AFP/Matrix_Tensor (AFP)
14:38:13 Session AFP/Knot_Theory (AFP)
14:38:13 Session AFP/Polynomials (AFP)
14:38:13 Session AFP/Groebner_Bases (AFP)
14:38:13 Session AFP/Allen_Calculus (AFP)
14:38:13 Session AFP/Automatic_Refinement (AFP)
14:38:13 Session AFP/Refine_Monadic (AFP)
14:38:14 Session AFP/Collections (AFP)
14:38:14 Session AFP/CAVA_Base (AFP)
14:38:14 Session AFP/CAVA_Automata (AFP)
14:38:14 Session AFP/DFS_Framework (AFP)
14:38:14 Session AFP/Gabow_SCC (AFP)
14:38:14 Session AFP/LTL_to_GBA (AFP)
14:38:14 Session AFP/CAVA_buildchain1 (AFP)
14:38:14 Session AFP/CAVA_buildchain3 (AFP)
14:38:14 Session AFP/CAVA_LTL_Modelchecker (AFP)
14:38:15 Session AFP/Promela (AFP)
14:38:15 Session AFP/Collections_Examples (AFP)
14:38:15 Session AFP/Dijkstra_Shortest_Path (AFP)
14:38:15 Session AFP/Formal_SSA (AFP)
14:38:15 Session AFP/Minimal_SSA (AFP)
14:38:15 Session AFP/Sepref_Prereq (AFP)
14:38:15 Session AFP/Refine_Imperative_HOL (AFP)
14:38:15 Session AFP/Sepref_Basic (AFP)
14:38:15 Session AFP/Sepref_IICF (AFP)
14:38:15 Session AFP/EdmondsKarp_Base (AFP)
14:38:15 Session AFP/EdmondsKarp_Maxflow (AFP)
14:38:15 Session AFP/Transitive-Closure (AFP)
14:38:15 Session AFP/Tree-Automata (AFP)
14:38:16 Session AFP/BinarySearchTree (AFP)
14:38:16 Session AFP/Binomial-Queues (AFP)
14:38:16 Session AFP/Bondy (AFP)
14:38:16 Session AFP/Bounded_Deducibility_Security (AFP)
14:38:16 Session AFP/BytecodeLogicJmlTypes (AFP)
14:38:16 Session AFP/CISC-Kernel (AFP)
14:38:16 Session AFP/CYK (AFP)
14:38:16 Session AFP/Card_Number_Partitions (AFP)
14:38:16 Session AFP/Case_Labeling (AFP)
14:38:16 Session AFP/Cauchy (AFP)
14:38:16 Session AFP/Sqrt_Babylonian (AFP)
14:38:16 Session AFP/Real_Impl (AFP)
14:38:16 Session AFP/Certification_Monads (AFP)
14:38:16 Session AFP/ClockSynchInst (AFP)
14:38:16 Session AFP/Coinductive_Languages (AFP)
14:38:16 Session AFP/Compiling-Exceptions-Correctly (AFP)
14:38:16 Session AFP/Completeness (AFP)
14:38:16 Session AFP/ComponentDependencies (AFP)
14:38:17 Session AFP/Concurrent_Ref_Alg (AFP)
14:38:17 Session AFP/Consensus_Refined (AFP)
14:38:17 Session AFP/Constructor_Funs (AFP)
14:38:17 Session AFP/CryptoBasedCompositionalProperties (AFP)
14:38:17 Session AFP/DPT-SAT-Solver (AFP)
14:38:17 Session AFP/DataRefinementIBP (AFP)
14:38:17 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
14:38:17 Session AFP/Dependent_SIFUM_Refinement (AFP)
14:38:17 Session AFP/Depth-First-Search (AFP)
14:38:17 Session AFP/Discrete_Summation (AFP)
14:38:17 Session AFP/Card_Partitions (AFP)
14:38:17 Session AFP/DiskPaxos (AFP)
14:38:17 Session AFP/Encodability_Process_Calculi (AFP)
14:38:17 Session AFP/Euler_Partition (AFP)
14:38:17 Session AFP/Example-Submission (AFP)
14:38:17 Session AFP/FFT (AFP)
14:38:17 Session AFP/FLP (AFP)
14:38:17 Session AFP/FOL_Harrison (AFP)
14:38:17 Session AFP/FeatherweightJava (AFP)
14:38:17 Session AFP/Featherweight_OCL (AFP)
14:38:17 Session AFP/FileRefinement (AFP)
14:38:17 Session AFP/FinFun (AFP)
14:38:17 Session AFP/Finite_Automata_HF (AFP)
14:38:17 Session AFP/FocusStreamsCaseStudies (AFP)
14:38:17 Session AFP/Free-Groups (AFP)
14:38:18 Session AFP/FunWithFunctions (AFP)
14:38:18 Session AFP/FunWithTilings (AFP)
14:38:18 Session AFP/GPU_Kernel_PL (AFP)
14:38:18 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
14:38:18 Session AFP/GenClock (AFP)
14:38:18 Session AFP/General-Triangle (AFP)
14:38:18 Session AFP/GoedelGod (AFP)
14:38:18 Session AFP/GraphMarkingIBP (AFP)
14:38:18 Session HOL/HOL-Library (main timing)
14:38:18 Session AFP/Abs_Int_ITP2012 (AFP)
14:38:18 Session AFP/Abstract_Completeness (AFP)
14:38:18 Session AFP/Abstract_Soundness (AFP)
14:38:18 Session AFP/Amortized_Complexity (AFP)
14:38:18 Session AFP/Dynamic_Tables (AFP)
14:38:18 Session AFP/ArrowImpossibilityGS (AFP)
14:38:18 Session AFP/Bell_Numbers_Spivey (AFP)
14:38:18 Session AFP/Card_Equiv_Relations (AFP)
14:38:18 Session AFP/Bernoulli (AFP)
14:38:18 Session AFP/Binomial-Heaps (AFP)
14:38:18 Session AFP/Boolean_Expression_Checkers (AFP)
14:38:18 Session AFP/Buildings (AFP)
14:38:19 Session AFP/Card_Multisets (AFP)
14:38:19 Session AFP/Category (AFP)
14:38:19 Session AFP/Category2 (AFP)
14:38:19 Session AFP/Category3 (AFP)
14:38:19 Session AFP/CofGroups (AFP)
14:38:19 Session AFP/ConcurrentIMP (AFP)
14:38:19 Session AFP/CoreC++ (AFP)
14:38:19 Session AFP/Datatype_Order_Generator (AFP)
14:38:19 Session AFP/Old_Datatype_Show (AFP)
14:38:19 Session AFP/Derangements (AFP)
14:38:19 Session AFP/Deriving (AFP)
14:38:20 Session AFP/Containers (AFP)
14:38:20 Session AFP/Containers-Benchmarks (AFP)
14:38:20 Session AFP/Show (AFP)
14:38:20 Session AFP/Efficient-Mergesort (AFP)
14:38:20 Session AFP/FOL-Fitting (AFP)
14:38:20 Session AFP/Finger-Trees (AFP)
14:38:20 Session AFP/Formula_Derivatives (AFP)
14:38:20 Session AFP/Formula_Derivatives-Examples (AFP)
14:38:20 Session AFP/Free-Boolean-Algebra (AFP)
14:38:20 Session AFP/Functional-Automata (AFP)
14:38:20 Session AFP/Graph_Theory (AFP)
14:38:20 Session AFP/ShortestPath (AFP)
14:38:21 Session AFP/Group-Ring-Module (AFP)
14:38:21 Session AFP/Valuation (AFP)
14:38:21 Session HOL/HOL-Cardinals (timing)
14:38:21 Session AFP/Ordinals_and_Cardinals (AFP)
14:38:21 Session AFP/Sort_Encodings (AFP)
14:38:21 Session HOL/HOL-Computational_Algebra
14:38:21 Session AFP/Coinductive (AFP)
14:38:21 Session AFP/Lazy-Lists-II (AFP)
14:38:21 Session AFP/Topology (AFP)
14:38:21 Session AFP/Stream_Fusion_Code (AFP)
14:38:21 Session AFP/Descartes_Sign_Rule (AFP)
14:38:21 Session HOL/HOL-Algebra (main timing)
14:38:21 Session AFP/JNF-HOL-Lib (AFP)
14:38:21 Session AFP/JNF-AFP-Lib (AFP)
14:38:22 Session AFP/Jordan_Normal_Form (AFP)
14:38:22 Session AFP/Pre_Perron_Frobenius (AFP)
14:38:22 Session AFP/Perron_Frobenius (AFP)
14:38:22 Session AFP/Subresultants (AFP)
14:38:22 Session AFP/Pre_BZ (AFP)
14:38:22 Session AFP/Berlekamp_Zassenhaus (AFP)
14:38:22 Session AFP/Pre_Algebraic_Numbers (AFP)
14:38:23 Session AFP/Algebraic_Numbers (AFP)
14:38:23 Session AFP/Algebraic_Numbers_Lib (AFP)
14:38:23 Session AFP/Pre_Polynomial_Factorization (AFP)
14:38:23 Session AFP/Polynomial_Factorization (AFP)
14:38:23 Session AFP/Jordan_Hoelder (AFP)
14:38:23 Session AFP/Perfect-Number-Thm (AFP)
14:38:23 Session AFP/Secondary_Sylow (AFP)
14:38:23 Session AFP/VectorSpace (AFP)
14:38:23 Session HOL/HOL-Analysis (main timing)
14:38:23 Session AFP/Affine_Arithmetic (AFP)
14:38:23 Session AFP/Cartan_FP (AFP)
14:38:23 Session AFP/Cayley_Hamilton (AFP)
14:38:23 Session AFP/Chord_Segments (AFP)
14:38:24 Session AFP/Echelon_Form (AFP)
14:38:24 Session AFP/Hermite (AFP)
14:38:24 Session AFP/Gauss_Jordan (AFP)
14:38:24 Session HOL/HOL-Probability (main timing)
14:38:24 Session AFP/Applicative_Lifting (AFP)
14:38:24 Session AFP/Stern_Brocot (AFP)
14:38:24 Session AFP/Deep_Learning_Lib (AFP)
14:38:24 Session AFP/Deep_Learning (AFP)
14:38:24 Session AFP/Density_Compiler (AFP)
14:38:24 Session AFP/Ergodic_Theory (AFP)
14:38:24 Session AFP/Fisher_Yates (AFP)
14:38:24 Session AFP/Girth_Chromatic (AFP)
14:38:25 Session AFP/List_Update (AFP)
14:38:25 Session AFP/Lp (AFP)
14:38:25 Session AFP/MFMC_Countable (AFP)
14:38:25 Session AFP/Markov_Models (AFP)
14:38:25 Session AFP/Probabilistic_Noninterference (AFP)
14:38:25 Session AFP/Probabilistic_System_Zoo (AFP)
14:38:25 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
14:38:25 Session AFP/Quick_Sort_Cost (AFP)
14:38:26 Session AFP/Random_BSTs (AFP)
14:38:26 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
14:38:26 Session AFP/Randomised_Social_Choice (AFP)
14:38:26 Session AFP/SDS_Impossibility (AFP)
14:38:26 Session AFP/Source_Coding_Theorem (AFP)
14:38:26 Session AFP/UpDown_Scheme (AFP)
14:38:26 Session AFP/Landau_Analysis (AFP)
14:38:26 Session AFP/Akra_Bazzi (AFP)
14:38:26 Session AFP/Catalan_Numbers (AFP)
14:38:27 Session AFP/Euler_MacLaurin (AFP)
14:38:27 Session AFP/Stirling_Formula (AFP)
14:38:27 Session AFP/Comparison_Sort_Lower_Bound (AFP)
14:38:27 Session AFP/Lower_Semicontinuous (AFP)
14:38:27 Session AFP/Ordinary_Differential_Equations (AFP)
14:38:27 Session AFP/HOL-ODE (AFP)
14:38:27 Session AFP/Differential_Dynamic_Logic (AFP)
14:38:27 Session AFP/HOL-ODE-Refinement (AFP)
14:38:28 Session AFP/HOL-ODE-Numerics (AFP)
14:38:28 Session AFP/Prime_Harmonic_Series (AFP)
14:38:28 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
14:38:28 Session AFP/Ptolemys_Theorem (AFP)
14:38:28 Session AFP/QR_Decomposition (AFP)
14:38:28 Session AFP/Rank_Nullity_Theorem (AFP)
14:38:28 Session AFP/Tarskis_Geometry (AFP)
14:38:28 Session AFP/Triangle (AFP)
14:38:28 Session AFP/pGCL (AFP)
14:38:28 Session HOL/HOL-Number_Theory (timing)
14:38:28 Session AFP/Bertrands_Postulate (AFP)
14:38:29 Session AFP/E_Transcendental (AFP)
14:38:29 Session AFP/Elliptic_Curves_Group_Law (AFP)
14:38:29 Session AFP/Fermat3_4 (AFP)
14:38:29 Session AFP/Koenigsberg_Friendship_Base (AFP)
14:38:29 Session AFP/Koenigsberg_Friendship (AFP)
14:38:29 Session AFP/Lehmer (AFP)
14:38:29 Session AFP/Pratt_Certificate (AFP)
14:38:29 Session AFP/SumSquares (AFP)
14:38:29 Session AFP/Liouville_Numbers (AFP)
14:38:29 Session AFP/Polynomial_Interpolation (AFP)
14:38:29 Session AFP/RSAPSS (AFP)
14:38:29 Session AFP/Rep_Fin_Groups (AFP)
14:38:29 Session AFP/Sturm_Sequences (AFP)
14:38:29 Session AFP/Special_Function_Bounds (AFP)
14:38:29 Session AFP/Sturm_Tarski (AFP)
14:38:29 Session HOL/HOL-Imperative_HOL
14:38:29 Session AFP/Imperative_Insertion_Sort (AFP)
14:38:29 Session AFP/HereditarilyFinite (AFP)
14:38:30 Session AFP/Incompleteness (AFP)
14:38:30 Session AFP/Surprise_Paradox (AFP)
14:38:30 Session AFP/HyperCTL (AFP)
14:38:30 Session AFP/Incredible_Proof_Machine (AFP)
14:38:30 Session AFP/Isabelle_Meta_Model (AFP)
14:38:30 Session AFP/Jinja (AFP)
14:38:30 Session AFP/HRB-Slicing (AFP)
14:38:30 Session AFP/InformationFlowSlicing_Inter (AFP)
14:38:30 Session AFP/Slicing (AFP)
14:38:30 Session AFP/InformationFlowSlicing (AFP)
14:38:30 Session AFP/KBPs (AFP)
14:38:30 Session AFP/LTL (AFP)
14:38:30 Session AFP/LTL_to_DRA (AFP)
14:38:30 Session AFP/Stuttering_Equivalence (AFP)
14:38:30 Session AFP/Lambda_Free_RPOs (AFP)
14:38:31 Session AFP/Landau_Symbols (AFP)
14:38:31 Session AFP/LinearQuantifierElim (AFP)
14:38:31 Session AFP/List-Infinite (AFP)
14:38:31 Session AFP/Nat-Interval-Logic (AFP)
14:38:31 Session AFP/AutoFocus-Stream (AFP)
14:38:31 Session AFP/MSO_Regex_Equivalence (AFP)
14:38:31 Session AFP/MSO_Examples (AFP)
14:38:31 Session AFP/MuchAdoAboutTwo (AFP)
14:38:31 Session AFP/Myhill-Nerode (AFP)
14:38:31 Session AFP/POPLmark-deBruijn (AFP)
14:38:31 Session AFP/Pairing_Heap (AFP)
14:38:31 Session AFP/Password_Authentication_Protocol (AFP)
14:38:31 Session AFP/Presburger-Automata (AFP)
14:38:31 Session AFP/Priority_Queue_Braun (AFP)
14:38:31 Session AFP/Program-Conflict-Analysis (AFP)
14:38:31 Session AFP/Regex_Equivalence (AFP)
14:38:31 Session AFP/Regex_Equivalence_Examples (AFP)
14:38:31 Session AFP/Regular-Sets (AFP)
14:38:31 Session AFP/Posix-Lexing (AFP)
14:38:31 Session AFP/Ribbon_Proofs (AFP)
14:38:31 Session AFP/SATSolverVerification (AFP)
14:38:31 Session AFP/Selection_Heap_Sort (AFP)
14:38:32 Session AFP/Separata (AFP)
14:38:32 Session AFP/Separation_Logic_Imperative_HOL (AFP)
14:38:32 Session AFP/Skew_Heap (AFP)
14:38:32 Session AFP/Splay_Tree (AFP)
14:38:32 Session AFP/Stable_Matching (AFP)
14:38:32 Session AFP/SuperCalc (AFP)
14:38:32 Session AFP/Tail_Recursive_Functions (AFP)
14:38:32 Session AFP/TortoiseHare (AFP)
14:38:32 Session AFP/Twelvefold_Way (AFP)
14:38:32 Session AFP/Vickrey_Clarke_Groves (AFP)
14:38:32 Session AFP/Well_Quasi_Orders (AFP)
14:38:32 Session AFP/XML (AFP)
14:38:32 Session HOL/HOL-Nominal
14:38:32 Session AFP/CCS (AFP)
14:38:33 Session AFP/Lam-ml-Normalization (AFP)
14:38:33 Session AFP/Pi_Calculus (AFP)
14:38:33 Session AFP/Psi_Calculi (AFP)
14:38:33 Session AFP/SequentInvertibility (AFP)
14:38:33 Session HOL/HOL-Word (main timing)
14:38:33 Session HOL/HOL-SPARK (main)
14:38:33 Session HOL/HOL-SPARK-Examples
14:38:33 Session AFP/RIPEMD-160-SPARK (AFP)
14:38:33 Session AFP/Kleene_Algebra (AFP)
14:38:34 Session AFP/KAT_and_DRA (AFP)
14:38:34 Session AFP/Algebraic_VCs (AFP)
14:38:34 Session AFP/Multirelations (AFP)
14:38:34 Session AFP/Regular_Algebras (AFP)
14:38:34 Session AFP/Relation_Algebra (AFP)
14:38:34 Session AFP/Residuated_Lattices (AFP)
14:38:34 Session AFP/Native_Word (AFP)
14:38:34 Session AFP/SPARCv8 (AFP)
14:38:34 Session AFP/Separation_Algebra (AFP)
14:38:34 Session AFP/Word_Lib (AFP)
14:38:34 Session AFP/Complx (AFP)
14:38:34 Session AFP/IP_Addresses (AFP)
14:38:34 Session AFP/Simple_Firewall (AFP)
14:38:34 Session AFP/Routing (AFP)
14:38:34 Session AFP/Iptables_Semantics (AFP)
14:38:35 Session AFP/LOFT (AFP)
14:38:35 Session HOL/HOLCF (main timing)
14:38:35 Session AFP/Circus (AFP)
14:38:35 Session AFP/HOLCF-HOL-Library (AFP)
14:38:35 Session AFP/HOLCF-Nominal2 (AFP)
14:38:35 Session AFP/Launchbury (AFP)
14:38:35 Session AFP/Call_Arity (AFP)
14:38:35 Session AFP/PCF (AFP)
14:38:35 Session AFP/Shivers-CFA (AFP)
14:38:35 Session AFP/Stream-Fusion (AFP)
14:38:35 Session AFP/Tycon (AFP)
14:38:35 Session AFP/WorkerWrapper (AFP)
14:38:35 Session AFP/Heard_Of (AFP)
14:38:35 Session AFP/HotelKeyCards (AFP)
14:38:36 Session AFP/Huffman (AFP)
14:38:36 Session AFP/IEEE_Floating_Point (AFP)
14:38:36 Session AFP/Impossible_Geometry (AFP)
14:38:36 Session AFP/Inductive_Confidentiality (AFP)
14:38:36 Session AFP/InfPathElimination (AFP)
14:38:36 Session AFP/Integration (AFP)
14:38:36 Session AFP/JiveDataStoreModel (AFP)
14:38:36 Session AFP/KAD (AFP)
14:38:36 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
14:38:36 Session AFP/LatticeProperties (AFP)
14:38:36 Session AFP/MonoBoolTranAlgebra (AFP)
14:38:36 Session AFP/PseudoHoops (AFP)
14:38:36 Session AFP/Lazy_Case (AFP)
14:38:36 Session AFP/Lifting_Definition_Option (AFP)
14:38:36 Session AFP/LightweightJava (AFP)
14:38:36 Session AFP/List-Index (AFP)
14:38:36 Session AFP/List_Interleaving (AFP)
14:38:36 Session AFP/Locally-Nameless-Sigma (AFP)
14:38:36 Session AFP/Marriage (AFP)
14:38:36 Session AFP/Latin_Square (AFP)
14:38:36 Session AFP/Max-Card-Matching (AFP)
14:38:36 Session AFP/Menger (AFP)
14:38:36 Session AFP/MiniML (AFP)
14:38:36 Session AFP/Network_Security_Policy_Verification (AFP)
14:38:36 Session AFP/No_FTL_observers (AFP)
14:38:36 Session AFP/Nominal2 (AFP)
14:38:37 Session AFP/Modal_Logics_for_NTS (AFP)
14:38:37 Session AFP/Rewriting_Z (AFP)
14:38:37 Session AFP/Noninterference_CSP (AFP)
14:38:37 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
14:38:37 Session AFP/Noninterference_Generic_Unwinding (AFP)
14:38:37 Session AFP/Noninterference_Inductive_Unwinding (AFP)
14:38:37 Session AFP/Noninterference_Sequential_Composition (AFP)
14:38:37 Session AFP/Noninterference_Concurrent_Composition (AFP)
14:38:37 Session AFP/NormByEval (AFP)
14:38:37 Session AFP/Open_Induction (AFP)
14:38:37 Session AFP/Ordinal (AFP)
14:38:37 Session AFP/Nested_Multisets_Ordinals (AFP)
14:38:37 Session AFP/Lambda_Free_KBOs (AFP)
14:38:37 Session AFP/Paraconsistency (AFP)
14:38:37 Session AFP/Parity_Game (AFP)
14:38:38 Session AFP/Partial_Function_MR (AFP)
14:38:38 Session AFP/Pop_Refinement (AFP)
14:38:38 Session AFP/Possibilistic_Noninterference (AFP)
14:38:38 Session AFP/Proof_Strategy_Language (AFP)
14:38:38 Session AFP/PropResPI (AFP)
14:38:38 Session AFP/ROBDD (AFP)
14:38:38 Session AFP/Ramsey-Infinite (AFP)
14:38:38 Session AFP/Recursion-Theory-I (AFP)
14:38:38 Session AFP/RefinementReactive (AFP)
14:38:38 Session AFP/Resolution_FOL (AFP)
14:38:38 Session AFP/Robbins-Conjecture (AFP)
14:38:38 Session AFP/Roy_Floyd_Warshall (AFP)
14:38:38 Session AFP/SIFPL (AFP)
14:38:38 Session AFP/SIFUM_Type_Systems (AFP)
14:38:38 Session AFP/SenSocialChoice (AFP)
14:38:38 Session AFP/Simpl (AFP)
14:38:39 Session AFP/BDD (AFP)
14:38:39 Session AFP/Planarity_Certificates (AFP)
14:38:39 Session AFP/Statecharts (AFP)
14:38:39 Session AFP/Stone_Algebras (AFP)
14:38:39 Session AFP/Stone_Relation_Algebras (AFP)
14:38:39 Session AFP/Strong_Security (AFP)
14:38:39 Session AFP/TLA (AFP)
14:38:39 Session AFP/Timed_Automata (AFP)
14:38:39 Session AFP/Transitive-Closure-II (AFP)
14:38:39 Session AFP/Tree_Decomposition (AFP)
14:38:39 Session AFP/Trie (AFP)
14:38:39 Session AFP/UPF (AFP)
14:38:39 Session AFP/UPF_Firewall (AFP)
14:38:39 Session AFP/Verified-Prover (AFP)
14:38:39 Session AFP/VolpanoSmith (AFP)
14:38:39 Session AFP/WHATandWHERE_Security (AFP)
14:38:42 Building HOL-Probability ...
14:38:42 Building HOLCF ...
14:38:42 Building HOL-Number_Theory ...
14:38:42 Building HOL-Word ...
14:38:42 Building HOL-Algebra ...
14:38:42 Building HOL-Nominal ...
14:38:43 Building HOL-Cardinals ...
14:38:43 Building HOL-Imperative_HOL ...
14:38:44 HOLCF: theory HOLCF.Nat_Bijection
14:38:44 HOLCF: theory HOLCF.Old_Datatype
14:38:44 HOL-Nominal: theory HOL-Nominal.Old_Datatype
14:38:44 HOL-Nominal: theory HOL-Nominal.Infinite_Set
14:38:44 HOL-Word: theory HOL-Word.Bit
14:38:44 HOL-Word: theory HOL-Word.Bits
14:38:45 HOL-Word: theory HOL-Word.Boolean_Algebra
14:38:45 HOL-Word: theory HOL-Word.Bits_Bit
14:38:45 HOL-Word: theory HOL-Word.Misc_Numeric
14:38:45 HOL-Word: theory HOL-Word.Bit_Representation
14:38:45 HOL-Word: theory HOL-Word.Word_Miscellaneous
14:38:46 HOLCF: theory HOLCF.Countable
14:38:46 HOL-Word: theory HOL-Word.Misc_Typedef
14:38:46 HOL-Word: theory HOL-Word.Bits_Int
14:38:46 HOL-Nominal: theory HOL-Nominal.Nominal
14:38:46 HOL-Word: theory HOL-Word.Phantom_Type
14:38:47 HOL-Word: theory HOL-Word.Cardinality
14:38:47 HOLCF: theory HOLCF.Porder
14:38:47 HOL-Word: theory HOL-Word.Bool_List_Representation
14:38:48 HOLCF: theory HOLCF.Pcpo
14:38:48 HOL-Word: theory HOL-Word.Numeral_Type
14:38:48 HOL-Cardinals: theory HOL-Cardinals.Order_Union
14:38:48 HOL-Cardinals: theory HOL-Cardinals.Fun_More
14:38:48 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List
14:38:48 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist
14:38:48 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More
14:38:48 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension
14:38:48 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap
14:38:49 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More
14:38:49 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation
14:38:49 HOL-Number_Theory: theory HOL-Number_Theory.Congruence
14:38:49 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding
14:38:49 HOL-Algebra: theory HOL-Algebra.Congruence
14:38:49 HOL-Algebra: theory HOL-Algebra.Exponent
14:38:49 HOL-Word: theory HOL-Word.Type_Length
14:38:49 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions
14:38:49 HOL-Word: theory HOL-Word.Word
14:38:49 HOLCF: theory HOLCF.Cont
14:38:50 HOLCF: theory HOLCF.Adm
14:38:50 HOLCF: theory HOLCF.Discrete
14:38:50 HOLCF: theory HOLCF.Cpodef
14:38:50 HOL-Number_Theory: theory HOL-Number_Theory.Order
14:38:50 HOL-Algebra: theory HOL-Algebra.Order
14:38:50 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
14:38:50 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation
14:38:50 HOLCF: theory HOLCF.Fun_Cpo
14:38:51 HOLCF: theory HOLCF.Product_Cpo
14:38:51 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic
14:38:51 HOLCF: theory HOLCF.Cfun
14:38:52 HOL-Number_Theory: theory HOL-Number_Theory.Lattice
14:38:52 HOL-Algebra: theory HOL-Algebra.Lattice
14:38:52 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic
14:38:52 HOLCF: theory HOLCF.Completion
14:38:52 HOLCF: theory HOLCF.Cprod
14:38:52 HOL-Cardinals: theory HOL-Cardinals.Cardinals
14:38:52 HOLCF: theory HOLCF.Deflation
14:38:52 HOLCF: theory HOLCF.Fix
14:38:52 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set
14:38:52 HOLCF: theory HOLCF.Sfun
14:38:52 HOLCF: theory HOLCF.Sprod
14:38:53 HOLCF: theory HOLCF.Up
14:38:53 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array
14:38:53 HOL-Number_Theory: theory HOL-Number_Theory.Complete_Lattice
14:38:53 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
14:38:53 HOL-Probability: theory HOL-Probability.Fin_Map
14:38:53 HOL-Probability: theory HOL-Probability.Discrete_Topology
14:38:53 HOLCF: theory HOLCF.Lift
14:38:53 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref
14:38:54 HOL-Probability: theory HOL-Probability.Essential_Supremum
14:38:54 HOLCF: theory HOLCF.One
14:38:54 HOLCF: theory HOLCF.Tr
14:38:54 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
14:38:54 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists
14:38:54 HOL-Probability: theory HOL-Probability.Probability_Measure
14:38:54 HOLCF: theory HOLCF.Ssum
14:38:54 HOL-Algebra: theory HOL-Algebra.Galois_Connection
14:38:54 HOL-Number_Theory: theory HOL-Number_Theory.Group
14:38:54 HOLCF: theory HOLCF.Fixrec
14:38:54 HOLCF: theory HOLCF.Map_Functions
14:38:55 HOL-Algebra: theory HOL-Algebra.Group
14:38:55 HOLCF: theory HOLCF.Bifinite
14:38:55 HOL-Probability: theory HOL-Probability.Stopping_Time
14:38:56 HOL-Number_Theory: theory HOL-Number_Theory.FiniteProduct
14:38:56 HOLCF: theory HOLCF.Domain_Aux
14:38:56 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview
14:38:56 HOL-Algebra: theory HOL-Algebra.Bij
14:38:56 HOL-Probability: theory HOL-Probability.Conditional_Expectation
14:38:56 HOL-Algebra: theory HOL-Algebra.Coset
14:38:56 HOL-Number_Theory: theory HOL-Number_Theory.Ring
14:38:56 HOL-Probability: theory HOL-Probability.Distribution_Functions
14:38:57 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker
14:38:57 HOLCF: theory HOLCF.Universal
14:38:57 HOL-Probability: theory HOL-Probability.Weak_Convergence
14:38:57 HOL-Algebra: theory HOL-Algebra.FiniteProduct
14:38:57 HOL-Probability: theory HOL-Probability.Giry_Monad
14:38:58 HOL-Algebra: theory HOL-Algebra.Sylow
14:38:58 HOL-Probability: theory HOL-Probability.Helly_Selection
14:38:58 HOL-Algebra: theory HOL-Algebra.Divisibility
14:38:58 HOLCF: theory HOLCF.Algebraic
14:38:58 HOLCF: theory HOLCF.Compact_Basis
14:38:58 HOL-Algebra: theory HOL-Algebra.Ring
14:38:59 HOLCF: theory HOLCF.LowerPD
14:38:59 HOLCF: theory HOLCF.UpperPD
14:38:59 HOLCF: theory HOLCF.Representable
14:39:00 HOLCF: theory HOLCF.ConvexPD
14:39:00 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
14:39:00 HOL-Probability: theory HOL-Probability.Projective_Family
14:39:02 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
14:39:03 HOLCF: theory HOLCF.Domain
14:39:04 HOL-Probability: theory HOL-Probability.PMF_Impl
14:39:04 HOL-Probability: theory HOL-Probability.Random_Permutations
14:39:04 HOL-Algebra: theory HOL-Algebra.AbelCoset
14:39:05 HOL-Probability: theory HOL-Probability.SPMF
14:39:05 HOLCF: theory HOLCF.Powerdomains
14:39:06 HOL-Probability: theory HOL-Probability.Independent_Family
14:39:06 HOLCF: theory HOLCF
14:39:06 HOL-Algebra: theory HOL-Algebra.Module
14:39:08 HOL-Probability: theory HOL-Probability.Convolution
14:39:09 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray
14:39:09 HOL-Probability: theory HOL-Probability.Information
14:39:09 HOL-Algebra: theory HOL-Algebra.More_Group
14:39:09 HOL-Algebra: theory HOL-Algebra.More_Finite_Product
14:39:09 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort
14:39:09 HOL-Probability: theory HOL-Probability.Projective_Limit
14:39:10 HOL-Algebra: theory HOL-Algebra.More_Ring
14:39:10 Timing HOL-Nominal (2 threads, 8.235s elapsed time, 16.256s cpu time, 0.776s GC time, factor 1.97)
14:39:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Nominal
14:39:10 Finished HOL-Nominal (0:00:26 elapsed time, 0:00:41 cpu time, factor 1.54)
14:39:10 Building Nested_Multisets_Ordinals ...
14:39:12 HOL-Algebra: theory HOL-Algebra.Ideal
14:39:12 HOL-Probability: theory HOL-Probability.Stream_Space
14:39:12 HOL-Probability: theory HOL-Probability.Distributions
14:39:12 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cancellation
14:39:12 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cardinal_Notations
14:39:13 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.FSet
14:39:13 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset
14:39:15 HOL-Probability: theory HOL-Probability.Characteristic_Functions
14:39:16 HOL-Probability: theory HOL-Probability.Sinc_Integral
14:39:16 HOL-Probability: theory HOL-Probability.Levy
14:39:17 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse
14:39:17 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
14:39:17 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Infinite_Set
14:39:18 HOL-Algebra: theory HOL-Algebra.RingHom
14:39:18 HOL-Probability: theory Probability
14:39:18 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.List_Index
14:39:19 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nat_Bijection
14:39:20 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Old_Datatype
14:39:20 HOL-Algebra: theory HOL-Algebra.QuotRing
14:39:20 HOL-Algebra: theory HOL-Algebra.UnivPoly
14:39:20 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_Order
14:39:21 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Plus
14:39:21 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable
14:39:21 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Order
14:39:21 HOL-Algebra: theory HOL-Algebra.IntRing
14:39:22 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Sublist
14:39:23 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set
14:39:24 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Complete_Lattices
14:39:24 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set_Type
14:39:29 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Order_Continuity
14:39:29 HOL-Number_Theory: theory HOL-Number_Theory.Cong
14:39:29 HOL-Number_Theory: theory HOL-Number_Theory.Totient
14:39:29 HOL-Number_Theory: theory HOL-Number_Theory.Coset
14:39:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Extended_Nat
14:39:30 HOL-Number_Theory: theory HOL-Number_Theory.Module
14:39:31 HOL-Number_Theory: theory HOL-Number_Theory.AbelCoset
14:39:33 HOL-Number_Theory: theory HOL-Number_Theory.More_Group
14:39:33 HOL-Number_Theory: theory HOL-Number_Theory.More_Finite_Product
14:39:34 HOL-Number_Theory: theory HOL-Number_Theory.More_Ring
14:39:34 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
14:39:35 Timing HOL-Word (2 threads, 22.816s elapsed time, 42.880s cpu time, 1.784s GC time, factor 1.88)
14:39:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word
14:39:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/document.pdf
14:39:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/outline.pdf
14:39:35 Finished HOL-Word (0:00:51 elapsed time, 0:01:18 cpu time, factor 1.52)
14:39:35 Building Kleene_Algebra ...
14:39:35 HOL-Number_Theory: theory HOL-Number_Theory.Fib
14:39:36 Timing HOLCF (2 threads, 21.989s elapsed time, 38.872s cpu time, 1.976s GC time, factor 1.77)
14:39:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF
14:39:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/document.pdf
14:39:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/outline.pdf
14:39:36 Finished HOLCF (0:00:53 elapsed time, 0:01:17 cpu time, factor 1.47)
14:39:36 Building Word_Lib ...
14:39:37 Kleene_Algebra: theory Kleene_Algebra.Signatures
14:39:38 Kleene_Algebra: theory Kleene_Algebra.Dioid
14:39:39 Word_Lib: theory Word_Lib.Sublist
14:39:39 Word_Lib: theory Word_Lib.WordBitwise
14:39:39 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
14:39:39 HOL-Number_Theory: theory HOL-Number_Theory.Ideal
14:39:40 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex
14:39:40 Word_Lib: theory Word_Lib.Prefix_Order
14:39:40 Timing HOL-Cardinals (2 threads, 24.175s elapsed time, 42.656s cpu time, 1.616s GC time, factor 1.76)
14:39:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Cardinals
14:39:40 Finished HOL-Cardinals (0:00:57 elapsed time, 0:01:23 cpu time, factor 1.45)
14:39:40 Building HOLCF-HOL-Library ...
14:39:43 Word_Lib: theory Word_Lib.Hex_Words
14:39:43 Word_Lib: theory Word_Lib.Signed_Words
14:39:43 Word_Lib: theory Word_Lib.Enumeration
14:39:43 Word_Lib: theory Word_Lib.Norm_Words
14:39:43 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Cancellation
14:39:43 HOLCF-HOL-Library: theory HOLCF-HOL-Library.AList
14:39:43 Word_Lib: theory Word_Lib.WordBitwise_Signed
14:39:43 Word_Lib: theory Word_Lib.Word_Syntax
14:39:44 Word_Lib: theory Word_Lib.HOL_Lemmas
14:39:44 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Multiset
14:39:44 Word_Lib: theory Word_Lib.Word_Lib
14:39:44 Word_Lib: theory Word_Lib.More_Divides
14:39:45 Word_Lib: theory Word_Lib.Word_Enum
14:39:45 Word_Lib: theory Word_Lib.Aligned
14:39:45 HOL-Number_Theory: theory HOL-Number_Theory.RingHom
14:39:45 HOLCF-HOL-Library: theory HOLCF-HOL-Library.FuncSet
14:39:45 Word_Lib: theory Word_Lib.Word_Setup_32
14:39:46 Word_Lib: theory Word_Lib.Word_Setup_64
14:39:46 Word_Lib: theory Word_Lib.Word_Lemmas
14:39:46 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Infinite_Set
14:39:46 HOLCF-HOL-Library: theory HOLCF-HOL-Library.LaTeXsugar
14:39:46 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Syntax
14:39:46 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Option
14:39:48 HOL-Number_Theory: theory HOL-Number_Theory.UnivPoly
14:39:51 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Permutation
14:39:52 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_More
14:39:52 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.McCarthy_91
14:39:53 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nested_Multiset
14:39:53 Word_Lib: theory Word_Lib.Word_Lemmas_32
14:39:54 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Multiset
14:39:54 Word_Lib: theory Word_Lib.Word_Lemmas_64
14:39:54 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hereditary_Multiset
14:39:54 Kleene_Algebra: theory Kleene_Algebra.Conway
14:39:54 Kleene_Algebra: theory Kleene_Algebra.Dioid_Models
14:39:55 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset
14:39:55 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Unary_PCF
14:39:56 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal
14:39:58 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Goodstein_Sequence
14:39:59 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hydra_Battle
14:40:00 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal
14:40:02 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge
14:40:03 Kleene_Algebra: theory Kleene_Algebra.Finite_Suprema
14:40:04 Kleene_Algebra: theory Kleene_Algebra.Inf_Matrix
14:40:04 Kleene_Algebra: theory Kleene_Algebra.Matrix
14:40:07 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra
14:40:07 HOL-Number_Theory: theory HOL-Number_Theory.Multiplicative_Group
14:40:12 HOL-Number_Theory: theory HOL-Number_Theory.Residues
14:40:16 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
14:40:16 Kleene_Algebra: theory Kleene_Algebra.DRA
14:40:16 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
14:40:17 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
14:40:17 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
14:40:17 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
14:40:18 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra
14:40:19 Kleene_Algebra: theory Kleene_Algebra.PHL_KA
14:40:20 Kleene_Algebra: theory Kleene_Algebra.PHL_DRA
14:40:21 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra_Models
14:40:22 Kleene_Algebra: theory Kleene_Algebra.Formal_Power_Series
14:40:26 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra_Models
14:40:27 Timing HOLCF-HOL-Library (2 threads, 21.311s elapsed time, 35.700s cpu time, 1.596s GC time, factor 1.68)
14:40:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-HOL-Library
14:40:27 Finished HOLCF-HOL-Library (0:00:46 elapsed time, 0:01:13 cpu time, factor 1.57)
14:40:28 Building HOLCF-Nominal2 ...
14:40:31 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Set
14:40:31 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Product
14:40:31 HOLCF-Nominal2: theory HOLCF-Nominal2.FSet
14:40:31 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_List
14:40:32 HOLCF-Nominal2: theory HOLCF-Nominal2.Phantom_Type
14:40:33 HOLCF-Nominal2: theory HOLCF-Nominal2.Cardinality
14:40:34 HOLCF-Nominal2: theory HOLCF-Nominal2.FinFun
14:40:37 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Base
14:40:43 HOLCF-Nominal2: theory HOLCF-Nominal2.Atoms
14:40:43 HOLCF-Nominal2: theory HOLCF-Nominal2.Eqvt
14:40:43 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Abs
14:40:46 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_FCB
14:40:46 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2
14:40:53 Timing HOL-Imperative_HOL (2 threads, 85.732s elapsed time, 84.660s cpu time, 2.504s GC time, factor 0.99)
14:40:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Imperative_HOL
14:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Imperative_HOL/document.pdf
14:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Imperative_HOL/outline.pdf
14:40:53 Finished HOL-Imperative_HOL (0:02:10 elapsed time, 0:06:52 cpu time, factor 3.17)
14:40:54 Building HOL-SPARK ...
14:40:56 HOL-SPARK: theory HOL-SPARK.Bit_Comparison
14:40:56 HOL-SPARK: theory HOL-SPARK.SPARK_Setup
14:40:58 HOL-SPARK: theory SPARK
14:41:09 Timing Nested_Multisets_Ordinals (2 threads, 83.203s elapsed time, 140.824s cpu time, 5.364s GC time, factor 1.69)
14:41:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals
14:41:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/document.pdf
14:41:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/outline.pdf
14:41:09 Finished Nested_Multisets_Ordinals (0:01:58 elapsed time, 0:03:15 cpu time, factor 1.65)
14:41:09 Running Psi_Calculi ...
14:41:11 Timing Kleene_Algebra (2 threads, 61.590s elapsed time, 103.236s cpu time, 4.620s GC time, factor 1.68)
14:41:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra
14:41:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/document.pdf
14:41:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/outline.pdf
14:41:11 Finished Kleene_Algebra (0:01:35 elapsed time, 0:02:35 cpu time, factor 1.63)
14:41:11 Building KAT_and_DRA ...
14:41:12 Psi_Calculi: theory Psi_Calculi.Chain
14:41:13 Timing HOL-SPARK (2 threads, 2.553s elapsed time, 4.188s cpu time, 0.112s GC time, factor 1.64)
14:41:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK
14:41:13 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.47)
14:41:13 Building Relation_Algebra ...
14:41:13 Psi_Calculi: theory Psi_Calculi.Subst_Term
14:41:13 Psi_Calculi: theory Psi_Calculi.Agent
14:41:14 Timing Word_Lib (2 threads, 76.320s elapsed time, 146.812s cpu time, 3.024s GC time, factor 1.92)
14:41:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Word_Lib
14:41:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Word_Lib/document.pdf
14:41:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Word_Lib/outline.pdf
14:41:14 Finished Word_Lib (0:01:37 elapsed time, 0:02:58 cpu time, factor 1.83)
14:41:14 Building IP_Addresses ...
14:41:15 KAT_and_DRA: theory KAT_and_DRA.KAT2
14:41:15 KAT_and_DRA: theory KAT_and_DRA.Test_Dioid
14:41:15 KAT_and_DRA: theory KAT_and_DRA.DRAT2
14:41:16 Relation_Algebra: theory Relation_Algebra.More_Boolean_Algebra
14:41:17 Relation_Algebra: theory Relation_Algebra.Relation_Algebra
14:41:17 IP_Addresses: theory IP_Addresses.Cancellation
14:41:17 IP_Addresses: theory IP_Addresses.Char_ord
14:41:17 Timing HOLCF-Nominal2 (2 threads, 24.930s elapsed time, 48.868s cpu time, 2.440s GC time, factor 1.96)
14:41:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Nominal2
14:41:17 Finished HOLCF-Nominal2 (0:00:49 elapsed time, 0:01:25 cpu time, factor 1.72)
14:41:17 IP_Addresses: theory IP_Addresses.Code_Abstract_Nat
14:41:18 IP_Addresses: theory IP_Addresses.Code_Target_Nat
14:41:18 Building Launchbury ...
14:41:18 IP_Addresses: theory IP_Addresses.Multiset
14:41:18 IP_Addresses: theory IP_Addresses.Code_Char
14:41:18 IP_Addresses: theory IP_Addresses.Code_Target_Int
14:41:18 IP_Addresses: theory IP_Addresses.Infinite_Set
14:41:19 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
14:41:19 IP_Addresses: theory IP_Addresses.Option_ord
14:41:19 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
14:41:20 IP_Addresses: theory IP_Addresses.Word_More
14:41:20 Timing HOL-Algebra (2 threads, 103.837s elapsed time, 182.880s cpu time, 9.360s GC time, factor 1.76)
14:41:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra
14:41:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf
14:41:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf
14:41:20 Finished HOL-Algebra (0:02:37 elapsed time, 0:04:24 cpu time, factor 1.68)
14:41:21 Building HOL-SPARK-Examples ...
14:41:21 Launchbury: theory Launchbury.Mono-Nat-Fun
14:41:21 Launchbury: theory Launchbury.Nominal-Utils
14:41:21 Launchbury: theory Launchbury.Vars
14:41:22 Launchbury: theory Launchbury.C
14:41:22 KAT_and_DRA: theory KAT_and_DRA.Conway_Tests
14:41:22 Launchbury: theory Launchbury.HOLCF-Join
14:41:22 Launchbury: theory Launchbury.HOLCF-Join-Classes
14:41:22 Launchbury: theory Launchbury.CValue
14:41:23 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Models
14:41:23 IP_Addresses: theory IP_Addresses.Quicksort
14:41:23 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD
14:41:23 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas
14:41:23 Launchbury: theory Launchbury.HOLCF-Meet
14:41:23 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor
14:41:23 Launchbury: theory Launchbury.Value
14:41:24 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence
14:41:24 IP_Addresses: theory IP_Addresses.Misc
14:41:24 KAT_and_DRA: theory KAT_and_DRA.KAT
14:41:24 Launchbury: theory Launchbury.C-Meet
14:41:24 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification
14:41:25 Launchbury: theory Launchbury.AList-Utils
14:41:25 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_RTC
14:41:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F
14:41:25 Launchbury: theory Launchbury.Env
14:41:25 Launchbury: theory Launchbury.AList-Utils-Nominal
14:41:25 Launchbury: theory Launchbury.Pointwise
14:41:25 Launchbury: theory Launchbury.HOLCF-Utils
14:41:26 Launchbury: theory Launchbury.Terms
14:41:26 Launchbury: theory Launchbury.C-restr
14:41:26 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Tests
14:41:27 Launchbury: theory Launchbury.Env-HOLCF
14:41:27 Launchbury: theory Launchbury.Iterative
14:41:27 Launchbury: theory Launchbury.EvalHeap
14:41:28 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash
14:41:28 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Vectors
14:41:28 KAT_and_DRA: theory KAT_and_DRA.DRAT
14:41:29 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Functions
14:41:29 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L
14:41:29 KAT_and_DRA: theory KAT_and_DRA.PHL_KAT
14:41:30 Launchbury: theory Launchbury.Nominal-HOLCF
14:41:30 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R
14:41:31 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L
14:41:31 KAT_and_DRA: theory KAT_and_DRA.DRA_Models
14:41:31 KAT_and_DRA: theory KAT_and_DRA.FolkTheorem
14:41:31 Launchbury: theory Launchbury.CValue-Nominal
14:41:32 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R
14:41:32 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round
14:41:32 Psi_Calculi: theory Psi_Calculi.Close_Subst
14:41:32 Psi_Calculi: theory Psi_Calculi.Frame
14:41:32 Psi_Calculi: theory Psi_Calculi.Structural_Congruence
14:41:32 Launchbury: theory Launchbury.Env-Nominal
14:41:33 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L
14:41:33 KAT_and_DRA: theory KAT_and_DRA.KAT_Models
14:41:33 Launchbury: theory Launchbury.HasESem
14:41:33 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R
14:41:34 Launchbury: theory Launchbury.HeapSemantics
14:41:34 KAT_and_DRA: theory KAT_and_DRA.PHL_DRAT
14:41:34 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Direct_Products
14:41:34 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt
14:41:34 Launchbury: theory Launchbury.Substitution
14:41:35 Launchbury: theory Launchbury.AbstractDenotational
14:41:35 Launchbury: theory Launchbury.Launchbury
14:41:35 Psi_Calculi: theory Psi_Calculi.Semantics
14:41:37 Launchbury: theory Launchbury.Abstract-Denotational-Props
14:41:37 Launchbury: theory Launchbury.ResourcedDenotational
14:41:38 Launchbury: theory Launchbury.Value-Nominal
14:41:39 Launchbury: theory Launchbury.CorrectnessResourced
14:41:39 Timing HOL-Number_Theory (2 threads, 124.447s elapsed time, 226.380s cpu time, 9.384s GC time, factor 1.82)
14:41:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Number_Theory
14:41:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Number_Theory/document.pdf
14:41:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Number_Theory/outline.pdf
14:41:39 Finished HOL-Number_Theory (0:02:55 elapsed time, 0:05:03 cpu time, factor 1.72)
14:41:39 Launchbury: theory Launchbury.Denotational
14:41:39 Launchbury: theory Launchbury.ResourcedAdequacy
14:41:39 Building Lehmer ...
14:41:39 Launchbury: theory Launchbury.ValueSimilarity
14:41:40 Launchbury: theory Launchbury.CorrectnessOriginal
14:41:41 Launchbury: theory Launchbury.Denotational-Related
14:41:41 Launchbury: theory Launchbury.Adequacy
14:41:42 Launchbury: theory Launchbury.EverythingAdequacy
14:41:48 Lehmer: theory Lehmer.Lehmer
14:41:50 Psi_Calculi: theory Psi_Calculi.Simulation
14:41:50 Psi_Calculi: theory Psi_Calculi.Bisimulation
14:41:52 Psi_Calculi: theory Psi_Calculi.Sim_Pres
14:41:53 Psi_Calculi: theory Psi_Calculi.Sim_Struct_Cong
14:41:53 Psi_Calculi: theory Psi_Calculi.Bisim_Pres
14:41:54 Psi_Calculi: theory Psi_Calculi.Sum
14:41:54 Psi_Calculi: theory Psi_Calculi.Tau_Chain
14:41:56 Psi_Calculi: theory Psi_Calculi.Bisim_Struct_Cong
14:41:56 Psi_Calculi: theory Psi_Calculi.Weak_Simulation
14:41:57 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp
14:41:58 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Simulation
14:41:58 Psi_Calculi: theory Psi_Calculi.Weak_Sim_Pres
14:41:59 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp_Pres
14:41:59 Psi_Calculi: theory Psi_Calculi.Bisim_Subst
14:42:01 Timing HOL-SPARK-Examples (2 threads, 19.143s elapsed time, 33.772s cpu time, 0.808s GC time, factor 1.76)
14:42:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK-Examples
14:42:01 Finished HOL-SPARK-Examples (0:00:40 elapsed time, 0:01:04 cpu time, factor 1.60)
14:42:01 Building JNF-HOL-Lib ...
14:42:02 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Sim_Pres
14:42:02 Psi_Calculi: theory Psi_Calculi.Weak_Bisimulation
14:42:06 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Pres
14:42:06 Timing Relation_Algebra (2 threads, 26.048s elapsed time, 51.260s cpu time, 1.720s GC time, factor 1.97)
14:42:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra
14:42:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra/document.pdf
14:42:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra/outline.pdf
14:42:06 Finished Relation_Algebra (0:00:53 elapsed time, 0:01:30 cpu time, factor 1.71)
14:42:06 Building Koenigsberg_Friendship_Base ...
14:42:07 Psi_Calculi: theory Psi_Calculi.Weak_Psi_Congruence
14:42:08 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Struct_Cong
14:42:09 JNF-HOL-Lib: theory JNF-HOL-Lib.Order_Union
14:42:09 JNF-HOL-Lib: theory JNF-HOL-Lib.Wellorder_Extension
14:42:10 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Pres
14:42:10 Psi_Calculi: theory Psi_Calculi.Weakening
14:42:13 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Struct_Cong
14:42:14 Psi_Calculi: theory Psi_Calculi.Weaken_Transition
14:42:14 Koenigsberg_Friendship_Base: theory Koenigsberg_Friendship_Base.Graph
14:42:15 Timing Lehmer (2 threads, 1.946s elapsed time, 3.508s cpu time, 0.000s GC time, factor 1.80)
14:42:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer
14:42:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer/document.pdf
14:42:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer/outline.pdf
14:42:15 Finished Lehmer (0:00:35 elapsed time, 0:00:50 cpu time, factor 1.42)
14:42:15 Running Complx ...
14:42:16 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
14:42:16 IP_Addresses: theory IP_Addresses.Hs_Compat
14:42:16 Psi_Calculi: theory Psi_Calculi.Weaken_Stat_Imp
14:42:16 IP_Addresses: theory IP_Addresses.Product_Lexorder
14:42:16 IP_Addresses: theory IP_Addresses.Lib_List_toString
14:42:16 IP_Addresses: theory IP_Addresses.Lib_Word_toString
14:42:16 IP_Addresses: theory IP_Addresses.Word_Next
14:42:16 Psi_Calculi: theory Psi_Calculi.Weak_Congruence
14:42:16 IP_Addresses: theory IP_Addresses.WordInterval
14:42:18 Complx: theory Complx.Language
14:42:18 Complx: theory Complx.Cache_Tactics
14:42:18 Psi_Calculi: theory Psi_Calculi.Weaken_Simulation
14:42:20 Timing KAT_and_DRA (2 threads, 43.968s elapsed time, 82.980s cpu time, 2.732s GC time, factor 1.89)
14:42:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA
14:42:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/document.pdf
14:42:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/outline.pdf
14:42:20 Finished KAT_and_DRA (0:01:08 elapsed time, 0:02:15 cpu time, factor 1.97)
14:42:20 Running SPARCv8 ...
14:42:21 Psi_Calculi: theory Psi_Calculi.Weaken_Bisimulation
14:42:21 IP_Addresses: theory IP_Addresses.IP_Address
14:42:21 Timing HOL-Probability (2 threads, 158.219s elapsed time, 282.404s cpu time, 8.704s GC time, factor 1.78)
14:42:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Probability
14:42:21 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Probability/document.pdf
14:42:21 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Probability/outline.pdf
14:42:21 Finished HOL-Probability (0:03:38 elapsed time, 0:06:08 cpu time, factor 1.69)
14:42:21 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
14:42:21 Building Deep_Learning_Lib ...
14:42:21 Complx: theory Complx.SmallStep
14:42:22 SPARCv8: theory SPARCv8.Adhoc_Overloading
14:42:22 SPARCv8: theory SPARCv8.WordDecl
14:42:23 Psi_Calculi: theory Psi_Calculi.Tau
14:42:23 SPARCv8: theory SPARCv8.Lib
14:42:23 SPARCv8: theory SPARCv8.RegistersOps
14:42:24 SPARCv8: theory SPARCv8.Sparc_Types
14:42:24 SPARCv8: theory SPARCv8.DetMonad
14:42:25 SPARCv8: theory SPARCv8.DetMonadLemmas
14:42:25 IP_Addresses: theory IP_Addresses.IPv4
14:42:25 SPARCv8: theory SPARCv8.Eisbach
14:42:25 SPARCv8: theory SPARCv8.Eisbach_Tools
14:42:26 IP_Addresses: theory IP_Addresses.IPv6
14:42:28 IP_Addresses: theory IP_Addresses.Prefix_Match
14:42:29 Complx: theory Complx.OG_Annotations
14:42:29 Complx: theory Complx.SeqCatch_decomp
14:42:29 IP_Addresses: theory IP_Addresses.CIDR_Split
14:42:32 Complx: theory Complx.OG_Hoare
14:42:33 Complx: theory Complx.OG_Soundness
14:42:34 Deep_Learning_Lib: theory Deep_Learning_Lib.Congruence
14:42:34 Deep_Learning_Lib: theory Deep_Learning_Lib.FunctionLemmas
14:42:34 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Unsorted
14:42:35 Complx: theory Complx.OG_Tactics
14:42:35 Deep_Learning_Lib: theory Deep_Learning_Lib.Order
14:42:35 Timing JNF-HOL-Lib (2 threads, 1.431s elapsed time, 2.740s cpu time, 0.000s GC time, factor 1.92)
14:42:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/JNF-HOL-Lib
14:42:35 Finished JNF-HOL-Lib (0:00:34 elapsed time, 0:00:48 cpu time, factor 1.42)
14:42:36 Building JNF-AFP-Lib ...
14:42:36 Complx: theory Complx.OG_Syntax
14:42:36 Deep_Learning_Lib: theory Deep_Learning_Lib.Ring_Hom
14:42:36 Deep_Learning_Lib: theory Deep_Learning_Lib.Lattice
14:42:37 Complx: theory Complx.Examples
14:42:37 Complx: theory Complx.SumArr
14:42:38 Deep_Learning_Lib: theory Deep_Learning_Lib.Complete_Lattice
14:42:38 Psi_Calculi: theory Psi_Calculi.Tau_Sim
14:42:39 Deep_Learning_Lib: theory Deep_Learning_Lib.Group
14:42:40 Timing Koenigsberg_Friendship_Base (2 threads, 1.099s elapsed time, 1.736s cpu time, 0.000s GC time, factor 1.58)
14:42:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship_Base
14:42:40 Finished Koenigsberg_Friendship_Base (0:00:33 elapsed time, 0:00:47 cpu time, factor 1.41)
14:42:40 Building Applicative_Lifting ...
14:42:41 Deep_Learning_Lib: theory Deep_Learning_Lib.Coset
14:42:42 Deep_Learning_Lib: theory Deep_Learning_Lib.FiniteProduct
14:42:43 Deep_Learning_Lib: theory Deep_Learning_Lib.Ring
14:42:44 JNF-AFP-Lib: theory JNF-AFP-Lib.IArray_Addenda
14:42:44 JNF-AFP-Lib: theory JNF-AFP-Lib.Containers_Auxiliary
14:42:45 JNF-AFP-Lib: theory JNF-AFP-Lib.IArray_Haskell
14:42:45 JNF-AFP-Lib: theory JNF-AFP-Lib.Missing_Unsorted
14:42:45 JNF-AFP-Lib: theory JNF-AFP-Lib.Comparator
14:42:46 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare
14:42:47 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Ring
14:42:47 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Comparator_Impl
14:42:47 JNF-AFP-Lib: theory JNF-AFP-Lib.Missing_Polynomial
14:42:47 Timing Launchbury (2 threads, 51.401s elapsed time, 94.108s cpu time, 3.576s GC time, factor 1.83)
14:42:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury
14:42:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/document.pdf
14:42:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/outline.pdf
14:42:47 Finished Launchbury (0:01:29 elapsed time, 0:02:31 cpu time, factor 1.70)
14:42:47 Deep_Learning_Lib: theory Deep_Learning_Lib.Module
14:42:47 Building Quick_Sort_Cost ...
14:42:48 JNF-AFP-Lib: theory JNF-AFP-Lib.Derive_Manager
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.Equal
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.Closure_Set
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.Extend_Partial_Order
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.FunctionLemmas
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.Generator_Aux
14:42:49 JNF-AFP-Lib: theory JNF-AFP-Lib.Comparator_Generator
14:42:50 Deep_Learning_Lib: theory Deep_Learning_Lib.RingModuleFacts
14:42:51 SPARCv8: theory SPARCv8.MMU
14:42:51 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare_Generator
14:42:51 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare_Instances
14:42:52 Deep_Learning_Lib: theory Deep_Learning_Lib.MonoidSums
14:42:52 JNF-AFP-Lib: theory JNF-AFP-Lib.Containers_Generator
14:42:52 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Permutations
14:42:52 SPARCv8: theory SPARCv8.Sparc_State
14:42:52 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Enum
14:42:52 Deep_Learning_Lib: theory Deep_Learning_Lib.LinearCombinations
14:42:53 JNF-AFP-Lib: theory JNF-AFP-Lib.Equality_Generator
14:42:53 Applicative_Lifting: theory Applicative_Lifting.Lambda
14:42:53 Applicative_Lifting: theory Applicative_Lifting.Commutation
14:42:53 Deep_Learning_Lib: theory Deep_Learning_Lib.Matrix
14:42:53 JNF-AFP-Lib: theory JNF-AFP-Lib.Equality_Instances
14:42:53 JNF-AFP-Lib: theory JNF-AFP-Lib.List_Fusion
14:42:53 Applicative_Lifting: theory Applicative_Lifting.Free_Ultrafilter
14:42:53 Applicative_Lifting: theory Applicative_Lifting.StarDef
14:42:53 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Eq
14:42:54 Applicative_Lifting: theory Applicative_Lifting.ParRed
14:42:54 JNF-AFP-Lib: theory JNF-AFP-Lib.DList_Set
14:42:54 Applicative_Lifting: theory Applicative_Lifting.Eta
14:42:55 JNF-AFP-Lib: theory JNF-AFP-Lib.Lexicographic_Order
14:42:55 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_ext
14:42:55 JNF-AFP-Lib: theory JNF-AFP-Lib.Set_Linorder
14:42:56 SPARCv8: theory SPARCv8.Sparc_Instruction
14:42:58 JNF-AFP-Lib: theory JNF-AFP-Lib.Regular_Set
14:42:58 Deep_Learning_Lib: theory Deep_Learning_Lib.Gauss_Jordan_Elimination
14:43:00 JNF-AFP-Lib: theory JNF-AFP-Lib.Regular_Exp
14:43:00 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Library
14:43:00 Quick_Sort_Cost: theory Quick_Sort_Cost.Group_Sort
14:43:00 Applicative_Lifting: theory Applicative_Lifting.Joinable
14:43:00 Applicative_Lifting: theory Applicative_Lifting.Applicative
14:43:00 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Symbols_Definition
14:43:00 Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
14:43:00 Deep_Learning_Lib: theory Deep_Learning_Lib.Column_Operations
14:43:01 Applicative_Lifting: theory Applicative_Lifting.Combinators
14:43:01 Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
14:43:01 Deep_Learning_Lib: theory Deep_Learning_Lib.Determinant
14:43:01 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
14:43:01 Applicative_Lifting: theory Applicative_Lifting.Applicative_List
14:43:02 Quick_Sort_Cost: theory Quick_Sort_Cost.List_Index
14:43:02 Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
14:43:02 SPARCv8: theory SPARCv8.Sparc_Execution
14:43:02 Quick_Sort_Cost: theory Quick_Sort_Cost.Linorder_Relations
14:43:03 SPARCv8: theory SPARCv8.Sparc_Properties
14:43:03 Quick_Sort_Cost: theory Quick_Sort_Cost.Regular_Set
14:43:03 Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
14:43:03 Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
14:43:03 Applicative_Lifting: theory Applicative_Lifting.Applicative_State
14:43:04 Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
14:43:04 JNF-AFP-Lib: theory JNF-AFP-Lib.NDerivative
14:43:04 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Real_Products
14:43:04 Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
14:43:04 Deep_Learning_Lib: theory Deep_Learning_Lib.SumSpaces
14:43:04 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
14:43:05 Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
14:43:05 Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
14:43:05 Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
14:43:05 Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
14:43:05 Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
14:43:06 Deep_Learning_Lib: theory Deep_Learning_Lib.VectorSpace
14:43:06 Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
14:43:07 Psi_Calculi: theory Psi_Calculi.Tau_Stat_Imp
14:43:08 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Order
14:43:08 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Simprocs
14:43:08 Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
14:43:09 JNF-AFP-Lib: theory JNF-AFP-Lib.Equivalence_Checking
14:43:09 Quick_Sort_Cost: theory Quick_Sort_Cost.Asymptotic_Equivalence
14:43:09 Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
14:43:09 JNF-AFP-Lib: theory JNF-AFP-Lib.Relation_Interpretation
14:43:09 JNF-AFP-Lib: theory JNF-AFP-Lib.Regexp_Method
14:43:09 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_More
14:43:10 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Symbols
14:43:10 JNF-AFP-Lib: theory JNF-AFP-Lib.RingModuleFacts
14:43:11 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Mapping2
14:43:12 JNF-AFP-Lib: theory JNF-AFP-Lib.MonoidSums
14:43:12 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Set2
14:43:13 JNF-AFP-Lib: theory JNF-AFP-Lib.LinearCombinations
14:43:14 JNF-AFP-Lib: theory JNF-AFP-Lib.Set_Impl
14:43:15 Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
14:43:18 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_VectorSpace
14:43:20 Deep_Learning_Lib: theory Deep_Learning_Lib.VS_Connect
14:43:21 Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
14:43:23 Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
14:43:23 Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
14:43:23 Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
14:43:23 JNF-AFP-Lib: theory JNF-AFP-Lib.Seq
14:43:24 JNF-AFP-Lib: theory JNF-AFP-Lib.Abstract_Rewriting
14:43:26 JNF-AFP-Lib: theory JNF-AFP-Lib.Relative_Rewriting
14:43:28 JNF-AFP-Lib: theory JNF-AFP-Lib.SN_Orders
14:43:31 JNF-AFP-Lib: theory JNF-AFP-Lib.Ordered_Semiring
14:43:32 JNF-AFP-Lib: theory JNF-AFP-Lib.SN_Order_Carrier
14:43:34 JNF-AFP-Lib: theory JNF-AFP-Lib.Show
14:43:35 JNF-AFP-Lib: theory JNF-AFP-Lib.Show_Instances
14:43:36 JNF-AFP-Lib: theory JNF-AFP-Lib.SumSpaces
14:43:38 JNF-AFP-Lib: theory JNF-AFP-Lib.Utility
14:43:38 JNF-AFP-Lib: theory JNF-AFP-Lib.VectorSpace
14:43:38 Psi_Calculi: theory Psi_Calculi.Tau_Laws_No_Weak
14:43:44 Psi_Calculi: theory Psi_Calculi.Tau_Laws_Weak
14:43:50 IP_Addresses: theory IP_Addresses.IP_Address_Parser
14:43:56 IP_Addresses: theory IP_Addresses.IP_Address_toString
14:44:07 Timing Quick_Sort_Cost (2 threads, 26.348s elapsed time, 47.240s cpu time, 1.984s GC time, factor 1.79)
14:44:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Quick_Sort_Cost
14:44:07 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Quick_Sort_Cost/document.pdf
14:44:07 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Quick_Sort_Cost/outline.pdf
14:44:07 Finished Quick_Sort_Cost (0:01:19 elapsed time, 0:02:06 cpu time, factor 1.60)
14:44:07 Building Randomised_Social_Choice ...
14:44:13 Timing Applicative_Lifting (2 threads, 31.568s elapsed time, 58.172s cpu time, 3.468s GC time, factor 1.84)
14:44:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Applicative_Lifting
14:44:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Applicative_Lifting/document.pdf
14:44:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Applicative_Lifting/outline.pdf
14:44:13 Finished Applicative_Lifting (0:01:31 elapsed time, 0:02:26 cpu time, factor 1.59)
14:44:13 Running Algebraic_VCs ...
14:44:17 Algebraic_VCs: theory Algebraic_VCs.Eisbach
14:44:17 Algebraic_VCs: theory Algebraic_VCs.Heap
14:44:17 Algebraic_VCs: theory Algebraic_VCs.Domain_Semiring
14:44:19 Randomised_Social_Choice: theory Randomised_Social_Choice.List_Index
14:44:22 Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
14:44:22 Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
14:44:22 Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
14:44:23 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
14:44:24 Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
14:44:24 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
14:44:25 Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
14:44:26 Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
14:44:26 Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
14:44:27 Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
14:44:30 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
14:44:30 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
14:44:31 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
14:44:32 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
14:44:33 Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
14:44:40 Algebraic_VCs: theory Algebraic_VCs.Antidomain_Semiring
14:45:23 Algebraic_VCs: theory Algebraic_VCs.Modal_Kleene_Algebra_Applications
14:45:23 Algebraic_VCs: theory Algebraic_VCs.Range_Semiring
14:45:26 Timing Randomised_Social_Choice (2 threads, 24.518s elapsed time, 47.960s cpu time, 2.352s GC time, factor 1.96)
14:45:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Randomised_Social_Choice
14:45:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Randomised_Social_Choice/document.pdf
14:45:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Randomised_Social_Choice/outline.pdf
14:45:26 Finished Randomised_Social_Choice (0:01:17 elapsed time, 0:02:03 cpu time, factor 1.59)
14:45:26 Running Native_Word ...
14:45:28 Native_Word: theory Native_Word.Code_Target_Int
14:45:28 Native_Word: theory Native_Word.Char_ord
14:45:29 Native_Word: theory Native_Word.Code_Char
14:45:29 Native_Word: theory Native_Word.Code_Test
14:45:30 Native_Word: theory Native_Word.More_Bits_Int
14:45:32 Native_Word: theory Native_Word.Bits_Integer
14:45:32 Native_Word: theory Native_Word.Word_Misc
14:45:45 Native_Word: theory Native_Word.Uint
14:45:45 Native_Word: theory Native_Word.Uint16
14:45:46 Native_Word: theory Native_Word.Uint32
14:45:47 Native_Word: theory Native_Word.Uint8
14:45:48 Native_Word: theory Native_Word.Code_Target_Bits_Int
14:45:49 Native_Word: theory Native_Word.Native_Cast
14:45:51 Native_Word: theory Native_Word.Native_Word_Test
14:45:58 Timing Deep_Learning_Lib (2 threads, 150.435s elapsed time, 285.100s cpu time, 12.504s GC time, factor 1.90)
14:45:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning_Lib
14:45:58 Finished Deep_Learning_Lib (0:03:36 elapsed time, 0:06:18 cpu time, factor 1.75)
14:45:58 Algebraic_VCs: theory Algebraic_VCs.Modal_Kleene_Algebra
14:45:58 Running Probabilistic_Noninterference ...
14:46:12 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_Nat
14:46:13 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_List
14:46:22 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_Stream
14:46:23 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Markov_Models_Auxiliary
14:46:27 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Discrete_Time_Markov_Chain
14:46:29 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
14:46:32 Algebraic_VCs: theory Algebraic_VCs.Modal_Kleene_Algebra_Models
14:46:41 Timing JNF-AFP-Lib (2 threads, 154.355s elapsed time, 300.556s cpu time, 16.200s GC time, factor 1.95)
14:46:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/JNF-AFP-Lib
14:46:41 Finished JNF-AFP-Lib (0:04:04 elapsed time, 0:07:19 cpu time, factor 1.80)
14:46:41 Building Jordan_Normal_Form ...
14:46:47 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_scratch
14:46:47 Algebraic_VCs: theory Algebraic_VCs.P2S2R
14:46:48 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_scratch
14:46:50 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
14:46:50 Algebraic_VCs: theory Algebraic_VCs.Domain_Quantale
14:46:51 Algebraic_VCs: theory Algebraic_VCs.VC_KAD
14:46:54 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
14:46:58 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
14:47:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Permutations
14:47:02 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
14:47:02 Jordan_Normal_Form: theory Jordan_Normal_Form.Order_Polynomial
14:47:02 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
14:47:02 Jordan_Normal_Form: theory Jordan_Normal_Form.Fundamental_Theorem_Algebra_Factorized
14:47:03 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
14:47:03 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
14:47:04 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
14:47:05 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom
14:47:06 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
14:47:06 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
14:47:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
14:47:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Poly
14:47:09 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
14:47:09 Algebraic_VCs: theory Algebraic_VCs.Path_Model_Example
14:47:10 Timing SPARCv8 (2 threads, 275.699s elapsed time, 541.480s cpu time, 14.564s GC time, factor 1.96)
14:47:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8
14:47:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8/document.pdf
14:47:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8/outline.pdf
14:47:10 Finished SPARCv8 (0:04:49 elapsed time, 0:09:18 cpu time, factor 1.93)
14:47:10 Building Pre_Polynomial_Factorization ...
14:47:13 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:47:15 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples
14:47:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
14:47:15 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_Examples2
14:47:16 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
14:47:16 Algebraic_VCs: theory Algebraic_VCs.Pointer_Examples
14:47:16 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual
14:47:19 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
14:47:19 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
14:47:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
14:47:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
14:47:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
14:47:24 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Neville_Aitken_Interpolation
14:47:24 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Improved_Code_Equations
14:47:24 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Lagrange_Interpolation
14:47:24 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.CauchysMeanTheorem
14:47:25 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
14:47:25 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian_Auxiliary
14:47:25 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Show_Poly
14:47:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
14:47:26 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Is_Rat_To_Rat
14:47:26 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
14:47:27 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Log_Impl
14:47:27 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.NthRoot_Impl
14:47:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
14:47:28 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Divmod_Int
14:47:28 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian
14:47:28 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Partial_Function_MR
14:47:29 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom
14:47:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
14:47:32 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
14:47:32 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom_Poly
14:47:33 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_dual_Examples
14:47:33 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf
14:47:35 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Newton_Interpolation
14:47:35 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
14:47:35 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
14:47:37 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
14:47:39 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
14:47:40 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Polynomial_Interpolation
14:47:40 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
14:47:40 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
14:47:42 Algebraic_VCs: theory Algebraic_VCs.VC_KAD_wf_Examples
14:47:42 Algebraic_VCs: theory Algebraic_VCs.VC_KAT
14:47:45 Algebraic_VCs: theory Algebraic_VCs.KAD_is_KAT
14:47:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:47:52 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
14:47:54 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
14:47:58 Algebraic_VCs: theory Algebraic_VCs.RKAT
14:48:00 Algebraic_VCs: theory Algebraic_VCs.RKAT_Models
14:48:00 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT
14:48:00 Algebraic_VCs: theory Algebraic_VCs.VC_RKAT_Examples
14:48:00 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples
14:48:00 Algebraic_VCs: theory Algebraic_VCs.VC_KAT_Examples2
14:48:01 Native_Word: theory Native_Word.Native_Word_Test_Emu
14:48:01 Native_Word: theory Native_Word.Native_Word_Test_PolyML
14:48:01 Native_Word: theory Native_Word.Native_Word_Test_Scala
14:48:22 Native_Word: theory Native_Word.Native_Word_Test_PolyML2
14:48:29 Native_Word: theory Native_Word.Native_Word_Test_GHC
14:48:33 Timing Complx (2 threads, 372.104s elapsed time, 709.436s cpu time, 9.752s GC time, factor 1.91)
14:48:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Complx
14:48:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Complx/document.pdf
14:48:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Complx/outline.pdf
14:48:33 Finished Complx (0:06:17 elapsed time, 0:11:55 cpu time, factor 1.90)
14:48:33 Running Markov_Models ...
14:48:45 Markov_Models: theory Markov_Models.Gauss_Jordan_Elim_Fun
14:48:45 Markov_Models: theory Markov_Models.Coinductive_Nat
14:48:45 Timing Pre_Polynomial_Factorization (2 threads, 37.340s elapsed time, 67.832s cpu time, 2.596s GC time, factor 1.82)
14:48:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization
14:48:45 Finished Pre_Polynomial_Factorization (0:01:34 elapsed time, 0:02:23 cpu time, factor 1.51)
14:48:46 Running Deep_Learning ...
14:48:47 Markov_Models: theory Markov_Models.Coinductive_List
14:48:47 Native_Word: theory Native_Word.Native_Word_Test_MLton2
14:48:47 Native_Word: theory Native_Word.Native_Word_Test_MLton
14:48:55 Markov_Models: theory Markov_Models.Coinductive_List_Prefix
14:48:55 Markov_Models: theory Markov_Models.Coinductive_Stream
14:48:56 Markov_Models: theory Markov_Models.Quotient_Coinductive_List
14:48:57 Markov_Models: theory Markov_Models.TLList
14:49:00 Markov_Models: theory Markov_Models.Quotient_TLList
14:49:01 Deep_Learning: theory Deep_Learning.DL_Missing_List
14:49:01 Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
14:49:01 Deep_Learning: theory Deep_Learning.DL_Missing_Sublist
14:49:02 Deep_Learning: theory Deep_Learning.PP_More_List2
14:49:02 Markov_Models: theory Markov_Models.Coinductive
14:49:02 Deep_Learning: theory Deep_Learning.Tensor
14:49:02 Deep_Learning: theory Deep_Learning.DL_Missing_Vector_Space
14:49:03 Deep_Learning: theory Deep_Learning.Tensor_Subtensor
14:49:03 Deep_Learning: theory Deep_Learning.Tensor_Plus
14:49:03 Deep_Learning: theory Deep_Learning.PP_Poly_Mapping
14:49:03 Timing Algebraic_VCs (2 threads, 283.124s elapsed time, 461.812s cpu time, 20.112s GC time, factor 1.63)
14:49:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_VCs
14:49:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_VCs/document.pdf
14:49:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_VCs/outline.pdf
14:49:03 Finished Algebraic_VCs (0:04:49 elapsed time, 0:07:50 cpu time, factor 1.62)
14:49:03 Running List_Update ...
14:49:03 Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
14:49:03 Deep_Learning: theory Deep_Learning.Tensor_Product
14:49:04 Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
14:49:04 Native_Word: theory Native_Word.Native_Word_Test_OCaml2
14:49:04 Native_Word: theory Native_Word.Native_Word_Test_OCaml
14:49:04 Deep_Learning: theory Deep_Learning.Tensor_Rank
14:49:04 Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
14:49:04 Deep_Learning: theory Deep_Learning.DL_Missing_Matrix
14:49:04 Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
14:49:05 Deep_Learning: theory Deep_Learning.PP_MPoly
14:49:05 Deep_Learning: theory Deep_Learning.DL_Network
14:49:05 Deep_Learning: theory Deep_Learning.PP_More_MPoly
14:49:06 Deep_Learning: theory Deep_Learning.PP_Univariate
14:49:07 Deep_Learning: theory Deep_Learning.DL_Submatrix
14:49:07 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ
14:49:07 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2
14:49:07 Deep_Learning: theory Deep_Learning.Tensor_Matricization
14:49:08 Timing Probabilistic_Noninterference (2 threads, 172.407s elapsed time, 308.884s cpu time, 9.132s GC time, factor 1.79)
14:49:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference
14:49:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference/document.pdf
14:49:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference/outline.pdf
14:49:08 Finished Probabilistic_Noninterference (0:03:09 elapsed time, 0:05:30 cpu time, factor 1.74)
14:49:08 Running Density_Compiler ...
14:49:09 Deep_Learning: theory Deep_Learning.DL_Shallow_Model
14:49:09 Deep_Learning: theory Deep_Learning.DL_Missing_VS_Connect
14:49:09 Deep_Learning: theory Deep_Learning.DL_Deep_Model
14:49:11 Deep_Learning: theory Deep_Learning.DL_Rank
14:49:13 Native_Word: theory Native_Word.Uint_Userguide
14:49:13 Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
14:49:14 Deep_Learning: theory Deep_Learning.Lebesgue_Functional
14:49:15 Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
14:49:16 List_Update: theory List_Update.List_Index
14:49:16 List_Update: theory List_Update.Regular_Set
14:49:18 List_Update: theory List_Update.Regular_Exp
14:49:21 Density_Compiler: theory Density_Compiler.Density_Predicates
14:49:21 Timing Native_Word (2 threads, 229.000s elapsed time, 208.764s cpu time, 7.096s GC time, factor 0.91)
14:49:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Native_Word
14:49:21 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Native_Word/document.pdf
14:49:21 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Native_Word/outline.pdf
14:49:21 Finished Native_Word (0:03:55 elapsed time, 0:10:46 cpu time, factor 2.75)
14:49:21 Running Ergodic_Theory ...
14:49:22 Density_Compiler: theory Density_Compiler.PDF_Transformations
14:49:22 Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
14:49:22 List_Update: theory List_Update.NDerivative
14:49:22 Density_Compiler: theory Density_Compiler.PDF_Values
14:49:25 Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
14:49:25 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
14:49:25 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
14:49:26 List_Update: theory List_Update.Equivalence_Checking
14:49:26 Density_Compiler: theory Density_Compiler.PDF_Semantics
14:49:26 Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
14:49:27 Deep_Learning: theory Deep_Learning.DL_Rank_Submatrix
14:49:28 List_Update: theory List_Update.Bit_Strings
14:49:28 List_Update: theory List_Update.Prob_Theory
14:49:28 List_Update: theory List_Update.On_Off
14:49:28 Markov_Models: theory Markov_Models.Crowds_Protocol
14:49:29 Markov_Models: theory Markov_Models.Example_A
14:49:29 List_Update: theory List_Update.Inversion
14:49:29 List_Update: theory List_Update.Swaps
14:49:29 List_Update: theory List_Update.RExp_Var
14:49:29 List_Update: theory List_Update.Competitive_Analysis
14:49:30 Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
14:49:30 Markov_Models: theory Markov_Models.Example_B
14:49:31 Markov_Models: theory Markov_Models.Gossip_Broadcast
14:49:31 List_Update: theory List_Update.Move_to_Front
14:49:31 Markov_Models: theory Markov_Models.Markov_Decision_Process
14:49:32 Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
14:49:33 Markov_Models: theory Markov_Models.Zeroconf_Analysis
14:49:34 Ergodic_Theory: theory Ergodic_Theory.Fekete
14:49:34 Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement
14:49:34 Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
14:49:35 Markov_Models: theory Markov_Models.MDP_Reachability_Problem
14:49:35 Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density
14:49:35 Markov_Models: theory Markov_Models.PGCL
14:49:35 Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
14:49:36 Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
14:49:36 Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
14:49:36 List_Update: theory List_Update.MTF2_Effects
14:49:36 Markov_Models: theory Markov_Models.MDP_RP_Certification
14:49:37 Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
14:49:37 List_Update: theory List_Update.BIT
14:49:37 List_Update: theory List_Update.Partial_Cost_Model
14:49:37 Ergodic_Theory: theory Ergodic_Theory.Recurrence
14:49:38 List_Update: theory List_Update.List_Factoring
14:49:39 Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
14:49:40 Ergodic_Theory: theory Ergodic_Theory.Invariants
14:49:41 Ergodic_Theory: theory Ergodic_Theory.Ergodicity
14:49:41 List_Update: theory List_Update.OPT2
14:49:41 Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
14:49:41 List_Update: theory List_Update.BIT_pairwise
14:49:41 Markov_Models: theory Markov_Models.Markov_Models
14:49:41 Timing IP_Addresses (2 threads, 415.278s elapsed time, 759.688s cpu time, 34.900s GC time, factor 1.83)
14:49:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IP_Addresses
14:49:41 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IP_Addresses/document.pdf
14:49:41 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IP_Addresses/outline.pdf
14:49:41 Finished IP_Addresses (0:08:26 elapsed time, 0:15:09 cpu time, factor 1.80)
14:49:42 Density_Compiler: theory Density_Compiler.PDF_Compiler
14:49:42 Building Simple_Firewall ...
14:49:42 Markov_Models: theory Markov_Models.PCTL
14:49:42 Ergodic_Theory: theory Ergodic_Theory.Kingman
14:49:43 List_Update: theory List_Update.Phase_Partitioning
14:49:44 List_Update: theory List_Update.BIT_2comp_on2
14:49:44 Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
14:49:46 List_Update: theory List_Update.TS
14:49:47 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
14:49:47 Simple_Firewall: theory Simple_Firewall.Iface
14:49:48 Simple_Firewall: theory Simple_Firewall.GroupF
14:49:48 List_Update: theory List_Update.Comb
14:49:49 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
14:49:51 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
14:49:51 Simple_Firewall: theory Simple_Firewall.List_Product_More
14:49:51 Simple_Firewall: theory Simple_Firewall.Option_Helpers
14:49:51 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
14:49:51 Simple_Firewall: theory Simple_Firewall.L4_Protocol
14:49:55 Simple_Firewall: theory Simple_Firewall.Simple_Packet
14:49:55 Simple_Firewall: theory Simple_Firewall.Primitives_toString
14:49:57 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
14:50:01 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
14:50:04 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
14:50:05 Simple_Firewall: theory Simple_Firewall.Shadowed
14:50:05 Simple_Firewall: theory Simple_Firewall.Service_Matrix
14:51:09 Timing Markov_Models (2 threads, 135.765s elapsed time, 251.772s cpu time, 12.196s GC time, factor 1.85)
14:51:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models
14:51:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models/document.pdf
14:51:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models/outline.pdf
14:51:09 Finished Markov_Models (0:02:35 elapsed time, 0:04:41 cpu time, factor 1.81)
14:51:09 Running Regular_Algebras ...
14:51:11 Timing Simple_Firewall (2 threads, 41.538s elapsed time, 80.696s cpu time, 3.892s GC time, factor 1.94)
14:51:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simple_Firewall
14:51:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simple_Firewall/document.pdf
14:51:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simple_Firewall/outline.pdf
14:51:11 Finished Simple_Firewall (0:01:29 elapsed time, 0:02:39 cpu time, factor 1.79)
14:51:12 Building Routing ...
14:51:12 Regular_Algebras: theory Regular_Algebras.Dioid_Power_Sum
14:51:13 Timing Density_Compiler (2 threads, 107.152s elapsed time, 213.120s cpu time, 5.536s GC time, factor 1.99)
14:51:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler
14:51:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler/document.pdf
14:51:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler/outline.pdf
14:51:13 Finished Density_Compiler (0:02:04 elapsed time, 0:03:52 cpu time, factor 1.87)
14:51:13 Regular_Algebras: theory Regular_Algebras.Regular_Algebras
14:51:13 Running Multirelations ...
14:51:14 Timing Deep_Learning (2 threads, 127.800s elapsed time, 252.836s cpu time, 7.224s GC time, factor 1.98)
14:51:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning
14:51:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/document.pdf
14:51:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/outline.pdf
14:51:14 Finished Deep_Learning (0:02:28 elapsed time, 0:04:35 cpu time, factor 1.85)
14:51:14 Running Call_Arity ...
14:51:17 Multirelations: theory Multirelations.C_Algebras
14:51:17 Routing: theory Routing.Adhoc_Overloading
14:51:17 Routing: theory Routing.Monad_Syntax
14:51:17 Routing: theory Routing.Linorder_Helper
14:51:17 Routing: theory Routing.Prefix_Match_toString
14:51:18 Routing: theory Routing.Routing_Table
14:51:19 Call_Arity: theory Call_Arity.BalancedTraces
14:51:19 Call_Arity: theory Call_Arity.ConstOn
14:51:19 Call_Arity: theory Call_Arity.List-Interleavings
14:51:19 Call_Arity: theory Call_Arity.Set-Cpo
14:51:20 Call_Arity: theory Call_Arity.Arity
14:51:20 Call_Arity: theory Call_Arity.TTree
14:51:20 Call_Arity: theory Call_Arity.EtaExpansion
14:51:20 Call_Arity: theory Call_Arity.SestoftConf
14:51:22 Call_Arity: theory Call_Arity.AEnv
14:51:22 Routing: theory Routing.IpRoute_Parser
14:51:23 Call_Arity: theory Call_Arity.ArityStack
14:51:23 Call_Arity: theory Call_Arity.Sestoft
14:51:23 Call_Arity: theory Call_Arity.EtaExpansionSafe
14:51:24 Call_Arity: theory Call_Arity.SestoftGC
14:51:24 Routing: theory Routing.Linux_Router
14:51:24 Call_Arity: theory Call_Arity.SestoftCorrect
14:51:25 Call_Arity: theory Call_Arity.Env-Set-Cpo
14:51:25 Call_Arity: theory Call_Arity.AList-Utils-HOLCF
14:51:26 Timing Ergodic_Theory (2 threads, 103.555s elapsed time, 201.696s cpu time, 5.664s GC time, factor 1.95)
14:51:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory
14:51:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory/document.pdf
14:51:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory/outline.pdf
14:51:26 Finished Ergodic_Theory (0:02:03 elapsed time, 0:03:43 cpu time, factor 1.81)
14:51:26 Running Pi_Calculus ...
14:51:26 Call_Arity: theory Call_Arity.AnalBinds
14:51:26 Call_Arity: theory Call_Arity.Cardinality-Domain
14:51:27 Call_Arity: theory Call_Arity.CardinalityAnalysisSig
14:51:28 Call_Arity: theory Call_Arity.CoCallGraph
14:51:28 Call_Arity: theory Call_Arity.TTree-HOLCF
14:51:28 Pi_Calculus: theory Pi_Calculus.Agent
14:51:30 Call_Arity: theory Call_Arity.TTreeAnalysisSig
14:51:30 Timing List_Update (2 threads, 125.565s elapsed time, 248.992s cpu time, 11.372s GC time, factor 1.98)
14:51:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update
14:51:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update/document.pdf
14:51:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update/outline.pdf
14:51:30 Finished List_Update (0:02:26 elapsed time, 0:04:37 cpu time, factor 1.89)
14:51:31 Call_Arity: theory Call_Arity.CoCallAnalysisSig
14:51:31 Running UpDown_Scheme ...
14:51:31 Call_Arity: theory Call_Arity.CoCallGraph-TTree
14:51:32 Call_Arity: theory Call_Arity.Arity-Nominal
14:51:32 Call_Arity: theory Call_Arity.Cardinality-Domain-Lists
14:51:33 Call_Arity: theory Call_Arity.ArityAnalysisSig
14:51:34 Call_Arity: theory Call_Arity.ArityAnalysisAbinds
14:51:35 Call_Arity: theory Call_Arity.ArityAnalysisStack
14:51:35 Call_Arity: theory Call_Arity.ArityAnalysisSpec
14:51:36 Call_Arity: theory Call_Arity.CardinalityAnalysisSpec
14:51:36 Call_Arity: theory Call_Arity.ArityAnalysisFix
14:51:36 Call_Arity: theory Call_Arity.ArityAnalysisFixProps
14:51:37 Pi_Calculus: theory Pi_Calculus.Early_Semantics
14:51:37 Pi_Calculus: theory Pi_Calculus.Late_Semantics
14:51:37 Call_Arity: theory Call_Arity.ArityConsistent
14:51:37 Multirelations: theory Multirelations.Multirelations
14:51:37 Call_Arity: theory Call_Arity.NoCardinalityAnalysis
14:51:38 Call_Arity: theory Call_Arity.CoCallAritySig
14:51:38 Call_Arity: theory Call_Arity.TTreeAnalysisSpec
14:51:39 Call_Arity: theory Call_Arity.CoCallAnalysisSpec
14:51:39 Call_Arity: theory Call_Arity.CoCallImplTTree
14:51:39 Call_Arity: theory Call_Arity.TTreeImplCardinality
14:51:41 Pi_Calculus: theory Pi_Calculus.Early_Tau_Chain
14:51:41 Call_Arity: theory Call_Arity.CoCallImplTTreeSafe
14:51:41 Pi_Calculus: theory Pi_Calculus.Weak_Early_Step_Semantics
14:51:41 Call_Arity: theory Call_Arity.TTreeImplCardinalitySafe
14:51:42 Call_Arity: theory Call_Arity.CoCallGraph-Nominal
14:51:42 Pi_Calculus: theory Pi_Calculus.Weak_Early_Semantics
14:51:42 Pi_Calculus: theory Pi_Calculus.Rel
14:51:42 Call_Arity: theory Call_Arity.CoCallAnalysisBinds
14:51:42 Pi_Calculus: theory Pi_Calculus.Strong_Early_Sim
14:51:42 Call_Arity: theory Call_Arity.TransformTools
14:51:42 Pi_Calculus: theory Pi_Calculus.Late_Semantics1
14:51:43 Pi_Calculus: theory Pi_Calculus.Strong_Early_Bisim
14:51:43 Pi_Calculus: theory Pi_Calculus.Late_Tau_Chain
14:51:43 Pi_Calculus: theory Pi_Calculus.Strong_Early_Bisim_Subst
14:51:43 Pi_Calculus: theory Pi_Calculus.Weak_Late_Step_Semantics
14:51:43 Pi_Calculus: theory Pi_Calculus.Strong_Early_Sim_Pres
14:51:43 Pi_Calculus: theory Pi_Calculus.Strong_Early_Bisim_Pres
14:51:43 UpDown_Scheme: theory UpDown_Scheme.Heap
14:51:43 UpDown_Scheme: theory UpDown_Scheme.Quicksort
14:51:44 Pi_Calculus: theory Pi_Calculus.Strong_Early_Bisim_Subst_Pres
14:51:44 Pi_Calculus: theory Pi_Calculus.Weak_Late_Semantics
14:51:44 Call_Arity: theory Call_Arity.AbstractTransform
14:51:44 Pi_Calculus: theory Pi_Calculus.Weak_Early_Sim
14:51:44 Call_Arity: theory Call_Arity.ArityEtaExpansion
14:51:44 Pi_Calculus: theory Pi_Calculus.Strong_Late_Sim
14:51:44 UpDown_Scheme: theory UpDown_Scheme.Misc
14:51:44 Pi_Calculus: theory Pi_Calculus.Weak_Early_Bisim
14:51:45 Pi_Calculus: theory Pi_Calculus.Weak_Early_Sim_Pres
14:51:45 Call_Arity: theory Call_Arity.ArityEtaExpansionSafe
14:51:45 Pi_Calculus: theory Pi_Calculus.Weak_Early_Bisim_Subst
14:51:45 Pi_Calculus: theory Pi_Calculus.Weak_Early_Step_Sim
14:51:45 Call_Arity: theory Call_Arity.CoCallFix
14:51:45 Pi_Calculus: theory Pi_Calculus.Weak_Early_Cong
14:51:46 Pi_Calculus: theory Pi_Calculus.Weak_Early_Step_Sim_Pres
14:51:46 UpDown_Scheme: theory UpDown_Scheme.Heap_Monad
14:51:46 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim
14:51:46 Pi_Calculus: theory Pi_Calculus.Weak_Early_Cong_Subst
14:51:46 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim_Subst
14:51:46 Pi_Calculus: theory Pi_Calculus.Strong_Late_Sim_Pres
14:51:46 Pi_Calculus: theory Pi_Calculus.Strong_Late_Sim_SC
14:51:47 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim_Pres
14:51:47 Pi_Calculus: theory Pi_Calculus.Weak_Late_Sim
14:51:47 Call_Arity: theory Call_Arity.ArityTransform
14:51:47 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim_Subst_Pres
14:51:47 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim_SC
14:51:48 Call_Arity: theory Call_Arity.CoCallAnalysisImpl
14:51:48 Pi_Calculus: theory Pi_Calculus.Strong_Late_Bisim_Subst_SC
14:51:48 Call_Arity: theory Call_Arity.ArityTransformSafe
14:51:48 Pi_Calculus: theory Pi_Calculus.Strong_Early_Late_Comp
14:51:49 Pi_Calculus: theory Pi_Calculus.Strong_Late_Expansion_Law
14:51:49 Pi_Calculus: theory Pi_Calculus.Strong_Early_Bisim_SC
14:51:49 Pi_Calculus: theory Pi_Calculus.Weak_Early_Bisim_SC
14:51:50 UpDown_Scheme: theory UpDown_Scheme.Array
14:51:51 Pi_Calculus: theory Pi_Calculus.Strong_Late_Axiomatisation
14:51:51 Pi_Calculus: theory Pi_Calculus.Weak_Early_Bisim_Pres
14:51:51 Call_Arity: theory Call_Arity.CardArityTransformSafe
14:51:52 Call_Arity: theory Call_Arity.CallArityEnd2End
14:51:52 Pi_Calculus: theory Pi_Calculus.Weak_Early_Cong_Pres
14:51:53 Pi_Calculus: theory Pi_Calculus.Weak_Late_Bisim
14:51:53 UpDown_Scheme: theory UpDown_Scheme.Ref
14:51:53 Pi_Calculus: theory Pi_Calculus.Weak_Early_Cong_Subst_Pres
14:51:53 UpDown_Scheme: theory UpDown_Scheme.Imperative_HOL
14:51:53 Pi_Calculus: theory Pi_Calculus.Weak_Late_Bisim_SC
14:51:53 UpDown_Scheme: theory UpDown_Scheme.Imperative_HOL_Add
14:51:53 UpDown_Scheme: theory UpDown_Scheme.Run
14:51:54 Pi_Calculus: theory Pi_Calculus.Weak_Late_Bisim_Subst
14:51:54 Pi_Calculus: theory Pi_Calculus.Weak_Late_Sim_Pres
14:51:54 Call_Arity: theory Call_Arity.CoCallImplSafe
14:51:54 Pi_Calculus: theory Pi_Calculus.Weak_Late_Step_Sim
14:51:54 Pi_Calculus: theory Pi_Calculus.Weak_Late_Bisim_Pres
14:51:54 UpDown_Scheme: theory UpDown_Scheme.Syntax_Match
14:51:54 UpDown_Scheme: theory UpDown_Scheme.Sep_Misc
14:51:55 UpDown_Scheme: theory UpDown_Scheme.Assertions
14:51:55 Call_Arity: theory Call_Arity.TrivialArityAnal
14:51:55 Call_Arity: theory Call_Arity.CallArityEnd2EndSafe
14:51:56 Call_Arity: theory Call_Arity.ArityAnalysisCorrDenotational
14:51:56 Pi_Calculus: theory Pi_Calculus.Weak_Late_Cong
14:51:57 Pi_Calculus: theory Pi_Calculus.Weak_Late_Step_Sim_Pres
14:51:57 Pi_Calculus: theory Pi_Calculus.Weak_Late_Cong_Subst
14:51:57 Pi_Calculus: theory Pi_Calculus.Weak_Late_Cong_Pres
14:51:57 Pi_Calculus: theory Pi_Calculus.Weak_Late_Cong_Subst_SC
14:52:00 UpDown_Scheme: theory UpDown_Scheme.Hoare_Triple
14:52:02 UpDown_Scheme: theory UpDown_Scheme.Automation
14:52:05 UpDown_Scheme: theory UpDown_Scheme.Sep_Main
14:52:20 Timing Routing (2 threads, 22.750s elapsed time, 38.892s cpu time, 0.972s GC time, factor 1.71)
14:52:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Routing
14:52:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Routing/document.pdf
14:52:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Routing/outline.pdf
14:52:20 Finished Routing (0:01:07 elapsed time, 0:01:28 cpu time, factor 1.31)
14:52:20 Building Iptables_Semantics ...
14:52:27 Iptables_Semantics: theory Iptables_Semantics.More_Bits_Int
14:52:27 Iptables_Semantics: theory Iptables_Semantics.LaTeXsugar
14:52:27 Iptables_Semantics: theory Iptables_Semantics.List_Misc
14:52:28 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
14:52:30 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
14:52:30 Iptables_Semantics: theory Iptables_Semantics.Bits_Integer
14:52:43 Regular_Algebras: theory Regular_Algebras.Pratts_Counterexamples
14:52:43 Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Models
14:52:43 Iptables_Semantics: theory Iptables_Semantics.Code_Target_Bits_Int
14:52:46 Regular_Algebras: theory Regular_Algebras.Regular_Algebra_Variants
14:52:47 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
14:52:47 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
14:52:47 Timing Psi_Calculi (2 threads, 672.274s elapsed time, 1198.800s cpu time, 63.208s GC time, factor 1.78)
14:52:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Psi_Calculi
14:52:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Psi_Calculi/document.pdf
14:52:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Psi_Calculi/outline.pdf
14:52:47 Finished Psi_Calculi (0:11:37 elapsed time, 0:20:28 cpu time, factor 1.76)
14:52:47 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
14:52:47 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
14:52:47 Running Random_Graph_Subgraph_Threshold ...
14:52:48 Iptables_Semantics: theory Iptables_Semantics.Ternary
14:52:48 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
14:52:51 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
14:52:53 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
14:52:54 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
14:52:55 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_toString
14:52:57 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
14:52:59 UpDown_Scheme: theory UpDown_Scheme.Grid_Point
14:53:00 UpDown_Scheme: theory UpDown_Scheme.Grid
14:53:00 Iptables_Semantics: theory Iptables_Semantics.Ports
14:53:01 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Dense_Linear_Order
14:53:01 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Girth_Chromatic_Misc
14:53:01 UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
14:53:01 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraphs
14:53:02 UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
14:53:02 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
14:53:03 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Approximation
14:53:04 UpDown_Scheme: theory UpDown_Scheme.Down
14:53:04 UpDown_Scheme: theory UpDown_Scheme.Up
14:53:05 UpDown_Scheme: theory UpDown_Scheme.Imperative
14:53:06 UpDown_Scheme: theory UpDown_Scheme.Up_Down
14:53:06 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
14:53:09 Iptables_Semantics: theory Iptables_Semantics.Semantics
14:53:09 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
14:53:10 Timing Call_Arity (2 threads, 104.174s elapsed time, 166.088s cpu time, 7.584s GC time, factor 1.59)
14:53:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity
14:53:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/document.pdf
14:53:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/outline.pdf
14:53:10 Finished Call_Arity (0:01:55 elapsed time, 0:02:59 cpu time, factor 1.56)
14:53:10 Running Elliptic_Curves_Group_Law ...
14:53:11 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
14:53:11 Iptables_Semantics: theory Iptables_Semantics.Optimizing
14:53:11 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
14:53:11 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
14:53:12 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
14:53:12 Iptables_Semantics: theory Iptables_Semantics.Matching
14:53:13 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
14:53:13 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
14:53:13 Timing Multirelations (2 threads, 112.963s elapsed time, 116.640s cpu time, 4.692s GC time, factor 1.03)
14:53:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multirelations
14:53:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multirelations/document.pdf
14:53:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multirelations/outline.pdf
14:53:13 Finished Multirelations (0:01:59 elapsed time, 0:08:56 cpu time, factor 4.50)
14:53:13 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
14:53:13 Timing Regular_Algebras (2 threads, 118.090s elapsed time, 156.900s cpu time, 4.144s GC time, factor 1.33)
14:53:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular_Algebras
14:53:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular_Algebras/document.pdf
14:53:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular_Algebras/outline.pdf
14:53:13 Finished Regular_Algebras (0:02:03 elapsed time, 0:02:52 cpu time, factor 1.39)
14:53:13 Running Bertrands_Postulate ...
14:53:13 Running Koenigsberg_Friendship ...
14:53:14 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
14:53:15 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
14:53:17 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
14:53:17 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
14:53:18 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Algebra_Aux
14:53:18 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Conversions
14:53:19 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
14:53:20 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Commutative_Ring
14:53:22 Bertrands_Postulate: theory Bertrands_Postulate.Dense_Linear_Order
14:53:22 Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph
14:53:22 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
14:53:23 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
14:53:24 Timing Pi_Calculus (2 threads, 103.622s elapsed time, 163.324s cpu time, 6.140s GC time, factor 1.58)
14:53:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pi_Calculus
14:53:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pi_Calculus/document.pdf
14:53:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pi_Calculus/outline.pdf
14:53:24 Finished Pi_Calculus (0:01:57 elapsed time, 0:03:01 cpu time, factor 1.54)
14:53:24 Bertrands_Postulate: theory Bertrands_Postulate.Approximation
14:53:24 Running SequentInvertibility ...
14:53:25 Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory
14:53:26 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
14:53:26 SequentInvertibility: theory SequentInvertibility.Cancellation
14:53:26 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
14:53:27 SequentInvertibility: theory SequentInvertibility.Multiset
14:53:27 Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge
14:53:31 Timing UpDown_Scheme (2 threads, 103.862s elapsed time, 139.048s cpu time, 4.148s GC time, factor 1.34)
14:53:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme
14:53:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme/document.pdf
14:53:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme/outline.pdf
14:53:31 Finished UpDown_Scheme (0:01:59 elapsed time, 0:02:35 cpu time, factor 1.30)
14:53:31 Running MFMC_Countable ...
14:53:32 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Reflective_Field
14:53:38 SequentInvertibility: theory SequentInvertibility.MultiSequents
14:53:38 SequentInvertibility: theory SequentInvertibility.ModalSequents
14:53:42 SequentInvertibility: theory SequentInvertibility.NominalSequents
14:53:43 MFMC_Countable: theory MFMC_Countable.MFMC_Misc
14:53:45 MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
14:53:47 SequentInvertibility: theory SequentInvertibility.SRCTransforms
14:53:48 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Axclass
14:53:48 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Locale
14:53:50 SequentInvertibility: theory SequentInvertibility.SingleSuccedent
14:53:54 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Test
14:53:56 SequentInvertibility: theory SequentInvertibility.SequentInvertibility
14:54:01 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Girth_Chromatic
14:54:02 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
14:54:06 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
14:54:07 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
14:54:07 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
14:54:07 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
14:54:08 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
14:54:09 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
14:54:10 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
14:54:11 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
14:54:12 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
14:54:12 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
14:54:13 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
14:54:14 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
14:54:16 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
14:54:17 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
14:54:19 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
14:54:20 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
14:54:22 Bertrands_Postulate: theory Bertrands_Postulate.Bertrand
14:54:23 Iptables_Semantics: theory Iptables_Semantics.Transform
14:54:23 Timing Random_Graph_Subgraph_Threshold (2 threads, 79.610s elapsed time, 136.848s cpu time, 6.492s GC time, factor 1.72)
14:54:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold
14:54:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf
14:54:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf
14:54:23 Finished Random_Graph_Subgraph_Threshold (0:01:35 elapsed time, 0:02:32 cpu time, factor 1.60)
14:54:23 Running Girth_Chromatic ...
14:54:27 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
14:54:28 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
14:54:34 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
14:54:36 Girth_Chromatic: theory Girth_Chromatic.Dense_Linear_Order
14:54:36 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
14:54:36 Girth_Chromatic: theory Girth_Chromatic.Ugraphs
14:54:37 Timing Koenigsberg_Friendship (2 threads, 71.665s elapsed time, 128.984s cpu time, 5.208s GC time, factor 1.80)
14:54:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship
14:54:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship/document.pdf
14:54:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship/outline.pdf
14:54:37 Finished Koenigsberg_Friendship (0:01:23 elapsed time, 0:02:21 cpu time, factor 1.70)
14:54:37 Running Lambda_Free_KBOs ...
14:54:38 Timing Bertrands_Postulate (2 threads, 73.901s elapsed time, 126.476s cpu time, 5.216s GC time, factor 1.71)
14:54:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate
14:54:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate/document.pdf
14:54:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate/outline.pdf
14:54:38 Finished Bertrands_Postulate (0:01:24 elapsed time, 0:02:17 cpu time, factor 1.63)
14:54:38 Running SDS_Impossibility ...
14:54:38 Girth_Chromatic: theory Girth_Chromatic.Approximation
14:54:39 Timing SequentInvertibility (2 threads, 70.348s elapsed time, 136.748s cpu time, 12.000s GC time, factor 1.94)
14:54:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SequentInvertibility
14:54:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SequentInvertibility/document.pdf
14:54:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SequentInvertibility/outline.pdf
14:54:39 Finished SequentInvertibility (0:01:14 elapsed time, 0:02:21 cpu time, factor 1.90)
14:54:39 Running VectorSpace ...
14:54:40 Timing Elliptic_Curves_Group_Law (2 threads, 77.577s elapsed time, 144.140s cpu time, 6.488s GC time, factor 1.86)
14:54:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law
14:54:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/document.pdf
14:54:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/outline.pdf
14:54:40 Finished Elliptic_Curves_Group_Law (0:01:29 elapsed time, 0:02:36 cpu time, factor 1.75)
14:54:40 Running Sort_Encodings ...
14:54:41 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Order_Union
14:54:41 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Regular_Set
14:54:41 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Utility
14:54:41 Iptables_Semantics: theory Iptables_Semantics.Parser
14:54:41 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Wellorder_Extension
14:54:41 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
14:54:42 Lambda_Free_KBOs: theory Lambda_Free_KBOs.While_Combinator
14:54:42 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Seq
14:54:43 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Regular_Exp
14:54:43 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_Util
14:54:44 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Infinite_Chain
14:54:44 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Extension_Orders
14:54:46 Sort_Encodings: theory Sort_Encodings.Preliminaries
14:54:47 Lambda_Free_KBOs: theory Lambda_Free_KBOs.NDerivative
14:54:47 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Relation_Interpretation
14:54:47 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_Term
14:54:47 Sort_Encodings: theory Sort_Encodings.Sig
14:54:48 VectorSpace: theory VectorSpace.RingModuleFacts
14:54:48 VectorSpace: theory VectorSpace.FunctionLemmas
14:54:48 Sort_Encodings: theory Sort_Encodings.TermsAndClauses
14:54:49 VectorSpace: theory VectorSpace.MonoidSums
14:54:50 VectorSpace: theory VectorSpace.LinearCombinations
14:54:50 Timing Jordan_Normal_Form (2 threads, 403.467s elapsed time, 637.960s cpu time, 15.876s GC time, factor 1.58)
14:54:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form
14:54:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form/document.pdf
14:54:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form/outline.pdf
14:54:50 Finished Jordan_Normal_Form (0:08:08 elapsed time, 0:12:44 cpu time, factor 1.56)
14:54:51 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Equivalence_Checking
14:54:51 Building Pre_Perron_Frobenius ...
14:54:51 Sort_Encodings: theory Sort_Encodings.M
14:54:51 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
14:54:51 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Regexp_Method
14:54:52 Sort_Encodings: theory Sort_Encodings.U
14:54:52 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Abstract_Rewriting
14:54:53 Sort_Encodings: theory Sort_Encodings.CU
14:54:53 Sort_Encodings: theory Sort_Encodings.CM
14:54:54 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
14:54:54 Lambda_Free_KBOs: theory Lambda_Free_KBOs.SN_Orders
14:54:55 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
14:54:55 Sort_Encodings: theory Sort_Encodings.Mono
14:54:55 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
14:54:55 Iptables_Semantics: theory Iptables_Semantics.Documentation
14:54:56 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Polynomials
14:54:58 Timing MFMC_Countable (2 threads, 68.217s elapsed time, 125.324s cpu time, 6.372s GC time, factor 1.84)
14:54:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable
14:54:58 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable/document.pdf
14:54:58 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable/outline.pdf
14:54:58 Finished MFMC_Countable (0:01:27 elapsed time, 0:02:26 cpu time, factor 1.68)
14:54:58 Building Subresultants ...
14:55:01 VectorSpace: theory VectorSpace.SumSpaces
14:55:02 Sort_Encodings: theory Sort_Encodings.Mcalc
14:55:02 Sort_Encodings: theory Sort_Encodings.Mcalc2
14:55:02 VectorSpace: theory VectorSpace.VectorSpace
14:55:05 Sort_Encodings: theory Sort_Encodings.Mcalc2C
14:55:05 Sort_Encodings: theory Sort_Encodings.T_G_Prelim
14:55:06 Sort_Encodings: theory Sort_Encodings.T
14:55:07 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.L2_Norm
14:55:07 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Polynomial_Divisibility
14:55:08 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Norm_Arith
14:55:08 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Continuum_Not_Denumerable
14:55:08 Sort_Encodings: theory Sort_Encodings.G
14:55:08 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Inner_Product
14:55:08 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Operator_Norm
14:55:08 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Summation_Tests
14:55:10 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Square_Free_Factorization
14:55:10 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Product_Vector
14:55:10 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Euclidean_Space
14:55:12 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Finite_Cartesian_Product
14:55:13 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Linear_Algebra
14:55:13 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Types_To_Sets
14:55:14 Subresultants: theory Subresultants.Coeff_Int
14:55:14 Subresultants: theory Subresultants.Dichotomous_Lazard
14:55:14 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Eisbach
14:55:15 Subresultants: theory Subresultants.Missing_Polynomial_Factorial
14:55:15 Subresultants: theory Subresultants.More_Homomorphisms
14:55:15 Subresultants: theory Subresultants.Resultant_Prelim
14:55:15 Subresultants: theory Subresultants.Binary_Exponentiation
14:55:16 Subresultants: theory Subresultants.Subresultant
14:55:17 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Topology_Euclidean_Space
14:55:20 Sort_Encodings: theory Sort_Encodings.E
14:55:22 Subresultants: theory Subresultants.Subresultant_Gcd
14:55:26 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util
14:55:27 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App
14:55:27 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std
14:55:28 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs
14:55:28 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic
14:55:29 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Convex_Euclidean_Space
14:55:29 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Bounded_Linear_Function
14:55:31 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Uniform_Limit
14:55:32 Sort_Encodings: theory Sort_Encodings.Encodings
14:55:33 Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs
14:55:35 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
14:55:36 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Continuous_Extension
14:55:37 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Path_Connected
14:55:39 Timing Sort_Encodings (2 threads, 49.728s elapsed time, 97.688s cpu time, 8.648s GC time, factor 1.96)
14:55:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sort_Encodings
14:55:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sort_Encodings/document.pdf
14:55:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sort_Encodings/outline.pdf
14:55:39 Finished Sort_Encodings (0:00:58 elapsed time, 0:01:48 cpu time, factor 1.84)
14:55:39 Running Polynomial_Factorization ...
14:55:41 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Homeomorphism
14:55:43 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Brouwer_Fixpoint
14:55:45 Timing Girth_Chromatic (2 threads, 66.052s elapsed time, 110.664s cpu time, 5.312s GC time, factor 1.68)
14:55:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Girth_Chromatic
14:55:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Girth_Chromatic/document.pdf
14:55:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Girth_Chromatic/outline.pdf
14:55:45 Finished Girth_Chromatic (0:01:21 elapsed time, 0:02:06 cpu time, factor 1.56)
14:55:45 Running Circus ...
14:55:45 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Derivative
14:55:47 Timing VectorSpace (2 threads, 56.276s elapsed time, 104.500s cpu time, 4.668s GC time, factor 1.86)
14:55:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace
14:55:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/document.pdf
14:55:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/outline.pdf
14:55:47 Finished VectorSpace (0:01:07 elapsed time, 0:01:56 cpu time, factor 1.73)
14:55:47 Running PCF ...
14:55:47 Circus: theory Circus.Sublist
14:55:48 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Cartesian_Euclidean_Space
14:55:49 PCF: theory PCF.Dual_Lattice
14:55:49 PCF: theory PCF.Nat_Discrete
14:55:50 PCF: theory PCF.Product_Plus
14:55:50 PCF: theory PCF.Product_Order
14:55:50 Timing Lambda_Free_KBOs (2 threads, 66.243s elapsed time, 122.468s cpu time, 6.100s GC time, factor 1.85)
14:55:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lambda_Free_KBOs
14:55:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lambda_Free_KBOs/document.pdf
14:55:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lambda_Free_KBOs/outline.pdf
14:55:50 Finished Lambda_Free_KBOs (0:01:12 elapsed time, 0:02:13 cpu time, factor 1.85)
14:55:50 Running Probabilistic_System_Zoo ...
14:55:50 Circus: theory Circus.Var
14:55:50 Circus: theory Circus.Var_list
14:55:50 Circus: theory Circus.Relations
14:55:51 PCF: theory PCF.Basis
14:55:51 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Determinants
14:55:52 Circus: theory Circus.Designs
14:55:52 PCF: theory PCF.Logical_Relations
14:55:52 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset
14:55:52 Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial
14:55:52 Polynomial_Factorization: theory Polynomial_Factorization.Precomputation
14:55:53 Circus: theory Circus.Reactive_Processes
14:55:53 Polynomial_Factorization: theory Polynomial_Factorization.Missing_List
14:55:53 PCF: theory PCF.PCF
14:55:55 Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots
14:55:55 Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly
14:55:56 Circus: theory Circus.CSP_Processes
14:55:57 Circus: theory Circus.Circus_Actions
14:55:58 Timing SDS_Impossibility (2 threads, 64.106s elapsed time, 95.044s cpu time, 2.292s GC time, factor 1.48)
14:55:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility
14:55:58 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility/document.pdf
14:55:58 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility/outline.pdf
14:55:58 Finished SDS_Impossibility (0:01:19 elapsed time, 0:01:50 cpu time, factor 1.40)
14:55:58 Running Probabilistic_System_Zoo-Non_BNFs ...
14:55:58 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial
14:55:58 Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization
14:55:58 Circus: theory Circus.Denotational_Semantics
14:55:59 PCF: theory PCF.Continuations
14:55:59 PCF: theory PCF.OpSem
14:55:59 Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma
14:56:00 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test
14:56:02 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Union
14:56:02 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Fun_More
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Relation_More
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Extension
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellfounded_More
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Eisbach
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Relation
14:56:03 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Embedding
14:56:04 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Constructions
14:56:05 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Order_Relation
14:56:06 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Ordinal_Arithmetic
14:56:06 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Arithmetic
14:56:07 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinals
14:56:08 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bounded_Set
14:56:08 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
14:56:10 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Union
14:56:10 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Fun_More
14:56:10 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Relation_More
14:56:10 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Extension
14:56:11 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellfounded_More
14:56:11 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Eisbach
14:56:11 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Relation
14:56:11 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Embedding
14:56:11 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Constructions
14:56:13 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Order_Relation
14:56:13 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Ordinal_Arithmetic
14:56:14 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Arithmetic
14:56:14 Circus: theory Circus.Circus_Syntax
14:56:14 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinals
14:56:14 Circus: theory Circus.Refinement
14:56:14 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Bounded_Set
14:56:15 Circus: theory Circus.Refinement_Example
14:56:16 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Nonempty_Bounded_Set
14:56:16 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy
14:56:28 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
14:56:30 Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization
14:56:34 Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:56:34 Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility
14:56:35 Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization
14:56:35 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi
14:56:42 Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly
14:56:43 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization
14:56:43 Timing PCF (2 threads, 51.296s elapsed time, 99.348s cpu time, 3.020s GC time, factor 1.94)
14:56:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF
14:56:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF/document.pdf
14:56:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF/outline.pdf
14:56:43 Finished PCF (0:00:55 elapsed time, 0:01:44 cpu time, factor 1.88)
14:56:43 Running Lp ...
14:56:45 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
14:56:51 Timing Polynomial_Factorization (2 threads, 54.709s elapsed time, 77.524s cpu time, 2.008s GC time, factor 1.42)
14:56:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization
14:56:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf
14:56:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf
14:56:51 Finished Polynomial_Factorization (0:01:11 elapsed time, 0:01:35 cpu time, factor 1.33)
14:56:51 Running Stern_Brocot ...
14:56:53 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Finitely_Bounded_Set_Counterexample
14:56:53 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi_Counterexample
14:56:55 Timing Probabilistic_System_Zoo (2 threads, 50.835s elapsed time, 87.256s cpu time, 4.312s GC time, factor 1.72)
14:56:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo
14:56:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/document.pdf
14:56:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf
14:56:55 Finished Probabilistic_System_Zoo (0:01:05 elapsed time, 0:01:42 cpu time, factor 1.57)
14:56:55 Lp: theory Lp.SG_Library_Complement
14:56:55 Running Shivers-CFA ...
14:56:56 Lp: theory Lp.Functional_Spaces
14:56:57 Timing Probabilistic_System_Zoo-Non_BNFs (2 threads, 45.259s elapsed time, 90.020s cpu time, 5.900s GC time, factor 1.99)
14:56:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs
14:56:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/document.pdf
14:56:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/outline.pdf
14:56:57 Finished Probabilistic_System_Zoo-Non_BNFs (0:00:59 elapsed time, 0:01:44 cpu time, factor 1.76)
14:56:57 Running Residuated_Lattices ...
14:56:58 Lp: theory Lp.Lp
14:56:58 Shivers-CFA: theory Shivers-CFA.Adhoc_Overloading
14:56:58 Shivers-CFA: theory Shivers-CFA.HOLCFUtils
14:56:58 Shivers-CFA: theory Shivers-CFA.FixTransform
14:56:58 Shivers-CFA: theory Shivers-CFA.Computability
14:56:58 Shivers-CFA: theory Shivers-CFA.CPSScheme
14:56:58 Shivers-CFA: theory Shivers-CFA.SetMap
14:56:59 Shivers-CFA: theory Shivers-CFA.Utils
14:56:59 Shivers-CFA: theory Shivers-CFA.MapSets
14:57:01 Residuated_Lattices: theory Residuated_Lattices.Residuated_Lattices
14:57:01 Timing Circus (2 threads, 54.041s elapsed time, 103.184s cpu time, 3.448s GC time, factor 1.91)
14:57:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus
14:57:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus/document.pdf
14:57:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus/outline.pdf
14:57:01 Finished Circus (0:01:15 elapsed time, 0:02:21 cpu time, factor 1.87)
14:57:01 Running Fermat3_4 ...
14:57:05 Stern_Brocot: theory Stern_Brocot.Cotree
14:57:07 Shivers-CFA: theory Shivers-CFA.CPSUtils
14:57:09 Fermat3_4: theory Fermat3_4.Fermat4
14:57:09 Fermat3_4: theory Fermat3_4.Quad_Form
14:57:10 Shivers-CFA: theory Shivers-CFA.Eval
14:57:10 Fermat3_4: theory Fermat3_4.Fermat3
14:57:12 Shivers-CFA: theory Shivers-CFA.AbsCF
14:57:12 Shivers-CFA: theory Shivers-CFA.ExCF
14:57:12 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
14:57:13 Residuated_Lattices: theory Residuated_Lattices.Involutive_Residuated
14:57:13 Residuated_Lattices: theory Residuated_Lattices.Action_Algebra
14:57:14 Timing Subresultants (2 threads, 79.459s elapsed time, 125.960s cpu time, 2.684s GC time, factor 1.59)
14:57:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants
14:57:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants/document.pdf
14:57:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants/outline.pdf
14:57:14 Finished Subresultants (0:02:15 elapsed time, 0:03:23 cpu time, factor 1.50)
14:57:14 Shivers-CFA: theory Shivers-CFA.ExCFSV
14:57:14 Building Pre_BZ ...
14:57:14 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
14:57:15 Residuated_Lattices: theory Residuated_Lattices.Residuated_Boolean_Algebras
14:57:16 Shivers-CFA: theory Shivers-CFA.AbsCFComp
14:57:17 Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
14:57:19 Residuated_Lattices: theory Residuated_Lattices.Action_Algebra_Models
14:57:20 Residuated_Lattices: theory Residuated_Lattices.Residuated_Relation_Algebra
14:57:30 Pre_BZ: theory Pre_BZ.Totient
14:57:30 Pre_BZ: theory Pre_BZ.Cong
14:57:31 Pre_BZ: theory Pre_BZ.Efficient_Sort
14:57:31 Pre_BZ: theory Pre_BZ.Missing_Multiset
14:57:31 Pre_BZ: theory Pre_BZ.Improved_Code_Equations
14:57:32 Pre_BZ: theory Pre_BZ.Neville_Aitken_Interpolation
14:57:32 Timing Residuated_Lattices (2 threads, 28.891s elapsed time, 51.092s cpu time, 1.784s GC time, factor 1.77)
14:57:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Residuated_Lattices
14:57:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Residuated_Lattices/document.pdf
14:57:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Residuated_Lattices/outline.pdf
14:57:32 Finished Residuated_Lattices (0:00:34 elapsed time, 0:00:58 cpu time, factor 1.66)
14:57:32 Running Pratt_Certificate ...
14:57:33 Pre_BZ: theory Pre_BZ.Residues
14:57:33 Timing Shivers-CFA (2 threads, 31.107s elapsed time, 60.216s cpu time, 2.716s GC time, factor 1.94)
14:57:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA
14:57:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document.pdf
14:57:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/outline.pdf
14:57:33 Finished Shivers-CFA (0:00:37 elapsed time, 0:01:08 cpu time, factor 1.83)
14:57:34 Running CCS ...
14:57:35 Timing Lp (2 threads, 35.663s elapsed time, 65.864s cpu time, 1.452s GC time, factor 1.85)
14:57:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp
14:57:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp/document.pdf
14:57:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp/outline.pdf
14:57:35 Finished Lp (0:00:51 elapsed time, 0:01:23 cpu time, factor 1.61)
14:57:35 Running Jordan_Hoelder ...
14:57:36 CCS: theory CCS.Agent
14:57:37 Timing Fermat3_4 (2 threads, 24.367s elapsed time, 50.184s cpu time, 0.912s GC time, factor 2.06)
14:57:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4
14:57:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4/document.pdf
14:57:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4/outline.pdf
14:57:37 Finished Fermat3_4 (0:00:35 elapsed time, 0:01:02 cpu time, factor 1.75)
14:57:37 Stern_Brocot: theory Stern_Brocot.Bird_Tree
14:57:37 Running Separation_Algebra ...
14:57:37 Pre_BZ: theory Pre_BZ.Lagrange_Interpolation
14:57:38 Pre_BZ: theory Pre_BZ.Polynomial_Divisibility
14:57:38 Pre_BZ: theory Pre_BZ.CauchysMeanTheorem
14:57:38 Pre_BZ: theory Pre_BZ.Sqrt_Babylonian_Auxiliary
14:57:38 Pre_BZ: theory Pre_BZ.Precomputation
14:57:39 Pre_BZ: theory Pre_BZ.Is_Rat_To_Rat
14:57:39 Pre_BZ: theory Pre_BZ.Log_Impl
14:57:39 Pre_BZ: theory Pre_BZ.NthRoot_Impl
14:57:39 Separation_Algebra: theory Separation_Algebra.Hoare_Logic_Abort
14:57:39 Separation_Algebra: theory Separation_Algebra.Types_D
14:57:40 CCS: theory CCS.Strong_Sim
14:57:40 CCS: theory CCS.Struct_Cong
14:57:40 CCS: theory CCS.Strong_Bisim
14:57:40 Pre_BZ: theory Pre_BZ.Sqrt_Babylonian
14:57:40 Pre_BZ: theory Pre_BZ.Show_Poly
14:57:40 CCS: theory CCS.Strong_Sim_Pres
14:57:40 CCS: theory CCS.Strong_Sim_SC
14:57:40 CCS: theory CCS.Strong_Bisim_Pres
14:57:40 Timing Stern_Brocot (2 threads, 32.872s elapsed time, 53.204s cpu time, 3.580s GC time, factor 1.62)
14:57:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot
14:57:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot/document.pdf
14:57:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot/outline.pdf
14:57:40 Finished Stern_Brocot (0:00:49 elapsed time, 0:01:11 cpu time, factor 1.44)
14:57:40 Running WorkerWrapper ...
14:57:40 CCS: theory CCS.Tau_Chain
14:57:40 CCS: theory CCS.Strong_Bisim_SC
14:57:40 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
14:57:40 CCS: theory CCS.Weak_Cong_Semantics
14:57:40 Pre_BZ: theory Pre_BZ.Explicit_Roots
14:57:41 CCS: theory CCS.Weak_Semantics
14:57:41 CCS: theory CCS.Weak_Sim
14:57:41 Pre_BZ: theory Pre_BZ.Missing_List
14:57:41 Separation_Algebra: theory Separation_Algebra.Map_Extra
14:57:41 CCS: theory CCS.Weak_Bisim
14:57:41 Pre_BZ: theory Pre_BZ.Prime_Factorization
14:57:41 Pre_BZ: theory Pre_BZ.Gauss_Lemma
14:57:41 CCS: theory CCS.Weak_Cong_Sim
14:57:42 Separation_Algebra: theory Separation_Algebra.Separation_Algebra
14:57:42 CCS: theory CCS.Weak_Sim_Pres
14:57:42 CCS: theory CCS.Weak_Cong
14:57:42 CCS: theory CCS.Weak_Cong_Sim_Pres
14:57:42 CCS: theory CCS.Weak_Bisim_Pres
14:57:42 Pre_BZ: theory Pre_BZ.Square_Free_Factorization
14:57:42 CCS: theory CCS.Weak_Cong_Pres
14:57:43 Pre_BZ: theory Pre_BZ.Gcd_Rat_Poly
14:57:43 WorkerWrapper: theory WorkerWrapper.Nats
14:57:43 WorkerWrapper: theory WorkerWrapper.Maybe
14:57:43 Separation_Algebra: theory Separation_Algebra.Sep_Heap_Instance
14:57:43 Pre_BZ: theory Pre_BZ.Rational_Root_Test
14:57:43 Separation_Algebra: theory Separation_Algebra.Sep_Tactics
14:57:43 Jordan_Hoelder: theory Jordan_Hoelder.GroupAction
14:57:43 Pre_BZ: theory Pre_BZ.Bits
14:57:43 Separation_Algebra: theory Separation_Algebra.Sep_Tactics_Test
14:57:44 Pre_BZ: theory Pre_BZ.Bits_Bit
14:57:44 Separation_Algebra: theory Separation_Algebra.Simple_Separation_Example
14:57:44 Pre_BZ: theory Pre_BZ.Divmod_Int
14:57:44 WorkerWrapper: theory WorkerWrapper.LList
14:57:44 Pre_BZ: theory Pre_BZ.Dvd_Int_Poly
14:57:44 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupConjugation
14:57:45 Jordan_Hoelder: theory Jordan_Hoelder.SndSylow
14:57:45 Separation_Algebra: theory Separation_Algebra.Abstract_Separation_D
14:57:45 Separation_Algebra: theory Separation_Algebra.VM_Example
14:57:46 Pre_BZ: theory Pre_BZ.Newton_Interpolation
14:57:46 Pre_BZ: theory Pre_BZ.Misc_Numeric
14:57:46 Pre_BZ: theory Pre_BZ.Bit_Representation
14:57:46 Separation_Algebra: theory Separation_Algebra.Separation_Algebra_Alt
14:57:46 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
14:57:46 Pre_BZ: theory Pre_BZ.Bits_Int
14:57:47 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
14:57:47 WorkerWrapper: theory WorkerWrapper.CounterExample
14:57:47 WorkerWrapper: theory WorkerWrapper.Last
14:57:47 Separation_Algebra: theory Separation_Algebra.Sep_Eq
14:57:47 WorkerWrapper: theory WorkerWrapper.Streams
14:57:47 Separation_Algebra: theory Separation_Algebra.Separation_D
14:57:48 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
14:57:48 WorkerWrapper: theory WorkerWrapper.Accumulator
14:57:48 Pre_BZ: theory Pre_BZ.Bool_List_Representation
14:57:48 WorkerWrapper: theory WorkerWrapper.Backtracking
14:57:49 WorkerWrapper: theory WorkerWrapper.Continuations
14:57:49 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp
14:57:49 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
14:57:49 Pre_BZ: theory Pre_BZ.More_Bits_Int
14:57:50 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups
14:57:50 Pre_BZ: theory Pre_BZ.Polynomial_Interpolation
14:57:50 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups
14:57:50 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
14:57:51 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
14:57:51 Pre_BZ: theory Pre_BZ.Bits_Integer
14:57:52 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
14:57:52 WorkerWrapper: theory WorkerWrapper.Nub
14:57:53 WorkerWrapper: theory WorkerWrapper.UnboxedNats
14:57:53 Pre_BZ: theory Pre_BZ.Kronecker_Factorization
14:57:56 Pre_BZ: theory Pre_BZ.Rational_Factorization
14:57:59 Timing WorkerWrapper (2 threads, 13.623s elapsed time, 25.404s cpu time, 0.936s GC time, factor 1.86)
14:57:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper
14:57:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper/document.pdf
14:57:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper/outline.pdf
14:57:59 Finished WorkerWrapper (0:00:18 elapsed time, 0:00:31 cpu time, factor 1.66)
14:57:59 Running Lam-ml-Normalization ...
14:57:59 Pre_BZ: theory Pre_BZ.Word_Miscellaneous
14:58:00 Timing CCS (2 threads, 21.383s elapsed time, 39.096s cpu time, 1.076s GC time, factor 1.83)
14:58:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CCS
14:58:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CCS/document.pdf
14:58:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CCS/outline.pdf
14:58:00 Finished CCS (0:00:26 elapsed time, 0:00:44 cpu time, factor 1.71)
14:58:00 Running Stream-Fusion ...
14:58:00 Pre_BZ: theory Pre_BZ.Misc_Typedef
14:58:00 Pre_BZ: theory Pre_BZ.Word
14:58:01 Timing Separation_Algebra (2 threads, 18.898s elapsed time, 35.320s cpu time, 1.772s GC time, factor 1.87)
14:58:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra
14:58:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra/document.pdf
14:58:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra/outline.pdf
14:58:01 Finished Separation_Algebra (0:00:24 elapsed time, 0:00:41 cpu time, factor 1.73)
14:58:01 Running Tycon ...
14:58:02 Lam-ml-Normalization: theory Lam-ml-Normalization.LaTeXsugar
14:58:02 Lam-ml-Normalization: theory Lam-ml-Normalization.Lam_ml
14:58:02 Pre_BZ: theory Pre_BZ.Code_Target_Bits_Int
14:58:02 Pre_BZ: theory Pre_BZ.Types_To_Sets
14:58:02 Stream-Fusion: theory Stream-Fusion.Int_Discrete
14:58:03 Stream-Fusion: theory Stream-Fusion.LazyList
14:58:04 Tycon: theory Tycon.TypeApp
14:58:04 Tycon: theory Tycon.Coerce
14:58:04 Tycon: theory Tycon.Functor
14:58:04 Stream-Fusion: theory Stream-Fusion.Stream
14:58:05 Tycon: theory Tycon.Monad
14:58:06 Timing Pratt_Certificate (2 threads, 22.804s elapsed time, 42.500s cpu time, 0.604s GC time, factor 1.86)
14:58:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate
14:58:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate/document.pdf
14:58:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate/outline.pdf
14:58:06 Finished Pratt_Certificate (0:00:32 elapsed time, 0:00:53 cpu time, factor 1.62)
14:58:06 Running SumSquares ...
14:58:06 Tycon: theory Tycon.Binary_Tree_Monad
14:58:06 Tycon: theory Tycon.Lift_Monad
14:58:06 Pre_BZ: theory Pre_BZ.Word_Misc
14:58:06 Stream-Fusion: theory Stream-Fusion.StreamFusion
14:58:06 Tycon: theory Tycon.Monad_Plus
14:58:07 Tycon: theory Tycon.Monad_Zero
14:58:07 Pre_BZ: theory Pre_BZ.Uint32
14:58:07 Tycon: theory Tycon.Error_Monad
14:58:07 Tycon: theory Tycon.Resumption_Transformer
14:58:08 Timing Jordan_Hoelder (2 threads, 21.321s elapsed time, 38.700s cpu time, 1.648s GC time, factor 1.82)
14:58:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder
14:58:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/document.pdf
14:58:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/outline.pdf
14:58:08 Finished Jordan_Hoelder (0:00:32 elapsed time, 0:00:50 cpu time, factor 1.56)
14:58:08 Running Random_BSTs ...
14:58:08 Tycon: theory Tycon.Error_Transformer
14:58:08 Tycon: theory Tycon.Monad_Zero_Plus
14:58:09 Tycon: theory Tycon.Writer_Monad
14:58:09 Tycon: theory Tycon.Lazy_List_Monad
14:58:10 Tycon: theory Tycon.Maybe_Monad
14:58:10 Tycon: theory Tycon.State_Transformer
14:58:10 Tycon: theory Tycon.Writer_Transformer
14:58:14 SumSquares: theory SumSquares.TwoSquares
14:58:14 SumSquares: theory SumSquares.FourSquares
14:58:15 Timing Lam-ml-Normalization (2 threads, 10.407s elapsed time, 17.004s cpu time, 0.780s GC time, factor 1.63)
14:58:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lam-ml-Normalization
14:58:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lam-ml-Normalization/document.pdf
14:58:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lam-ml-Normalization/outline.pdf
14:58:15 Finished Lam-ml-Normalization (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.50)
14:58:15 Timing Stream-Fusion (2 threads, 10.215s elapsed time, 13.700s cpu time, 0.500s GC time, factor 1.34)
14:58:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion
14:58:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion/document.pdf
14:58:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion/outline.pdf
14:58:15 Finished Stream-Fusion (0:00:14 elapsed time, 0:00:18 cpu time, factor 1.28)
14:58:15 Running Imperative_Insertion_Sort ...
14:58:15 Running Secondary_Sylow ...
14:58:16 Timing Tycon (2 threads, 9.759s elapsed time, 17.956s cpu time, 0.672s GC time, factor 1.84)
14:58:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon
14:58:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon/document.pdf
14:58:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon/outline.pdf
14:58:16 Finished Tycon (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.64)
14:58:16 Running Source_Coding_Theorem ...
14:58:21 Random_BSTs: theory Random_BSTs.Less_False
14:58:21 Random_BSTs: theory Random_BSTs.Cmp
14:58:21 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops
14:58:21 Random_BSTs: theory Random_BSTs.Sorted_Less
14:58:21 Random_BSTs: theory Random_BSTs.List_Ins_Del
14:58:22 Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
14:58:22 Random_BSTs: theory Random_BSTs.Set_by_Ordered
14:58:22 Random_BSTs: theory Random_BSTs.Tree_Set
14:58:23 Secondary_Sylow: theory Secondary_Sylow.GroupAction
14:58:24 Random_BSTs: theory Random_BSTs.Random_BSTs
14:58:24 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
14:58:24 Secondary_Sylow: theory Secondary_Sylow.SndSylow
14:58:26 Timing SumSquares (2 threads, 9.694s elapsed time, 17.292s cpu time, 0.348s GC time, factor 1.78)
14:58:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares
14:58:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares/document.pdf
14:58:26 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares/outline.pdf
14:58:26 Finished SumSquares (0:00:19 elapsed time, 0:00:28 cpu time, factor 1.41)
14:58:26 Running Fisher_Yates ...
14:58:29 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
14:58:30 Timing Imperative_Insertion_Sort (2 threads, 7.470s elapsed time, 13.300s cpu time, 0.228s GC time, factor 1.78)
14:58:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Imperative_Insertion_Sort
14:58:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Imperative_Insertion_Sort/document.pdf
14:58:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Imperative_Insertion_Sort/outline.pdf
14:58:30 Finished Imperative_Insertion_Sort (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.42)
14:58:30 Running Perfect-Number-Thm ...
14:58:31 Timing Random_BSTs (2 threads, 7.870s elapsed time, 12.132s cpu time, 0.708s GC time, factor 1.54)
14:58:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs
14:58:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/document.pdf
14:58:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/outline.pdf
14:58:31 Finished Random_BSTs (0:00:23 elapsed time, 0:00:27 cpu time, factor 1.21)
14:58:31 Timing Secondary_Sylow (2 threads, 5.702s elapsed time, 10.632s cpu time, 0.380s GC time, factor 1.86)
14:58:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow
14:58:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/document.pdf
14:58:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/outline.pdf
14:58:31 Finished Secondary_Sylow (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.35)
14:58:31 Running RIPEMD-160-SPARK ...
14:58:31 Running Ordinals_and_Cardinals ...
14:58:34 RIPEMD-160-SPARK: theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
14:58:36 Timing Source_Coding_Theorem (2 threads, 5.375s elapsed time, 9.764s cpu time, 0.204s GC time, factor 1.82)
14:58:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem
14:58:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem/document.pdf
14:58:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem/outline.pdf
14:58:36 Finished Source_Coding_Theorem (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.25)
14:58:37 Timing RIPEMD-160-SPARK (2 threads, 1.275s elapsed time, 1.360s cpu time, 0.000s GC time, factor 1.07)
14:58:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RIPEMD-160-SPARK
14:58:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RIPEMD-160-SPARK/document.pdf
14:58:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RIPEMD-160-SPARK/outline.pdf
14:58:37 Finished RIPEMD-160-SPARK (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.11)
14:58:37 Ordinals_and_Cardinals: theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
14:58:38 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
14:58:39 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
14:58:39 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
14:58:39 Timing Ordinals_and_Cardinals (2 threads, 0.155s elapsed time, 0.236s cpu time, 0.000s GC time, factor 1.52)
14:58:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinals_and_Cardinals
14:58:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinals_and_Cardinals/document.pdf
14:58:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinals_and_Cardinals/outline.pdf
14:58:39 Finished Ordinals_and_Cardinals (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.06)
14:58:39 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
14:58:42 Timing Perfect-Number-Thm (2 threads, 2.127s elapsed time, 4.160s cpu time, 0.104s GC time, factor 1.96)
14:58:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm
14:58:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/document.pdf
14:58:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/outline.pdf
14:58:42 Finished Perfect-Number-Thm (0:00:12 elapsed time, 0:00:14 cpu time, factor 1.22)
14:58:44 Timing Fisher_Yates (2 threads, 3.607s elapsed time, 6.984s cpu time, 0.128s GC time, factor 1.94)
14:58:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates
14:58:44 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates/document.pdf
14:58:44 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates/outline.pdf
14:58:44 Finished Fisher_Yates (0:00:17 elapsed time, 0:00:21 cpu time, factor 1.22)
14:58:57 Timing Iptables_Semantics (2 threads, 282.852s elapsed time, 528.740s cpu time, 46.572s GC time, factor 1.87)
14:58:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Iptables_Semantics
14:58:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Iptables_Semantics/document.pdf
14:58:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Iptables_Semantics/outline.pdf
14:58:57 Finished Iptables_Semantics (0:06:37 elapsed time, 0:12:25 cpu time, factor 1.88)
14:58:58 Running LOFT ...
14:59:09 LOFT: theory LOFT.OpenFlow_Helpers
14:59:09 LOFT: theory LOFT.Sort_Descending
14:59:10 LOFT: theory LOFT.List_Group
14:59:11 LOFT: theory LOFT.Semantics_OpenFlow
14:59:11 LOFT: theory LOFT.OpenFlow_Matches
14:59:16 LOFT: theory LOFT.Featherweight_OpenFlow_Comparison
14:59:19 LOFT: theory LOFT.OpenFlow_Action
14:59:21 LOFT: theory LOFT.OpenFlow_Serialize
14:59:21 LOFT: theory LOFT.LinuxRouter_OpenFlow_Translation
14:59:24 LOFT: theory LOFT.OpenFlow_Documentation
14:59:26 LOFT: theory LOFT.OF_conv_test
14:59:36 LOFT: theory LOFT.RFC2544
15:00:20 Timing Pre_BZ (2 threads, 117.794s elapsed time, 198.140s cpu time, 8.524s GC time, factor 1.68)
15:00:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_BZ
15:00:20 Finished Pre_BZ (0:03:05 elapsed time, 0:05:25 cpu time, factor 1.75)
15:00:20 Building Berlekamp_Zassenhaus ...
15:00:22 Timing Pre_Perron_Frobenius (2 threads, 269.575s elapsed time, 470.776s cpu time, 19.780s GC time, factor 1.75)
15:00:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Perron_Frobenius
15:00:22 Finished Pre_Perron_Frobenius (0:05:30 elapsed time, 0:09:16 cpu time, factor 1.69)
15:00:22 Running Perron_Frobenius ...
15:00:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
15:00:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
15:00:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
15:00:40 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
15:00:40 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
15:00:40 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
15:00:42 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
15:00:43 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
15:00:44 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
15:00:44 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
15:00:45 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
15:00:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
15:00:46 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
15:00:51 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
15:00:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
15:00:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
15:00:53 Timing Perron_Frobenius (2 threads, 10.346s elapsed time, 16.968s cpu time, 0.616s GC time, factor 1.64)
15:00:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius
15:00:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/document.pdf
15:00:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/outline.pdf
15:00:53 Finished Perron_Frobenius (0:00:30 elapsed time, 0:00:38 cpu time, factor 1.25)
15:00:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
15:00:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
15:00:57 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
15:00:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
15:00:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
15:01:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
15:01:04 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
15:01:05 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
15:01:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
15:01:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
15:01:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
15:01:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
15:01:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
15:01:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
15:01:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
15:01:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
15:01:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
15:01:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
15:01:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
15:01:24 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
15:02:09 Timing LOFT (2 threads, 174.705s elapsed time, 344.756s cpu time, 13.260s GC time, factor 1.97)
15:02:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT
15:02:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT/document.pdf
15:02:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT/outline.pdf
15:02:09 Finished LOFT (0:03:10 elapsed time, 0:06:09 cpu time, factor 1.94)
15:04:03 Timing Berlekamp_Zassenhaus (2 threads, 137.464s elapsed time, 266.076s cpu time, 14.320s GC time, factor 1.94)
15:04:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus
15:04:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/document.pdf
15:04:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/outline.pdf
15:04:03 Finished Berlekamp_Zassenhaus (0:03:42 elapsed time, 0:06:28 cpu time, factor 1.74)
15:04:04 Building Pre_Algebraic_Numbers ...
15:04:26 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Misc_Polynomial
15:04:26 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Compare_Rat
15:04:26 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Compare_Real
15:04:27 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Sturm_Library
15:04:27 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Show_Real
15:04:27 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Sturm_Theorem
15:04:27 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Show_Complex
15:05:20 Timing Pre_Algebraic_Numbers (2 threads, 14.458s elapsed time, 28.644s cpu time, 0.668s GC time, factor 1.98)
15:05:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Algebraic_Numbers
15:05:20 Finished Pre_Algebraic_Numbers (0:01:15 elapsed time, 0:01:50 cpu time, factor 1.47)
15:05:20 Running Algebraic_Numbers ...
15:05:20 Running Algebraic_Numbers_Lib ...
15:05:42 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Compare_Complex
15:05:42 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Complex_Roots_Real_Poly
15:05:43 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
15:05:43 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
15:05:44 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Unique_Factorization
15:05:44 Algebraic_Numbers: theory Algebraic_Numbers.Unique_Factorization
15:05:44 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Bivariate_Polynomials
15:05:44 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
15:05:57 Algebraic_Numbers: theory Algebraic_Numbers.Unique_Factorization_Poly
15:05:57 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Unique_Factorization_Poly
15:05:58 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
15:05:58 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
15:05:58 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Resultant
15:05:59 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Algebraic_Numbers_Prelim
15:06:01 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
15:06:01 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Sturm_Rat
15:06:01 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
15:06:02 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Algebraic_Numbers
15:06:05 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
15:06:06 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Algebraic_Numbers
15:06:23 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
15:06:23 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Roots
15:06:23 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
15:06:24 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
15:06:24 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
15:06:25 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Alg
15:06:25 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Complex_Algebraic_Numbers
15:06:25 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
15:06:25 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Approx
15:06:26 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Precise
15:06:27 Algebraic_Numbers: theory Algebraic_Numbers.Real_Factorization
15:06:27 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Factorization
15:07:32 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
15:07:36 Timing Algebraic_Numbers_Lib (2 threads, 113.180s elapsed time, 185.972s cpu time, 7.756s GC time, factor 1.64)
15:07:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers_Lib
15:07:36 Finished Algebraic_Numbers_Lib (0:02:16 elapsed time, 0:03:29 cpu time, factor 1.53)
15:12:00 Timing Algebraic_Numbers (2 threads, 372.053s elapsed time, 661.568s cpu time, 63.108s GC time, factor 1.78)
15:12:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers
15:12:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf
15:12:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf
15:12:00 Finished Algebraic_Numbers (0:06:40 elapsed time, 0:11:32 cpu time, factor 1.73)
15:12:00 
15:12:00 === TIMING ===
15:12:00 
15:12:00 Group AFP: 2:44:41 elapsed time, 4:50:19 cpu time, factor 1.76
15:12:00 Group main: 0:08:18 elapsed time, 0:13:36 cpu time, factor 1.64
15:12:00 Group timing: 0:11:53 elapsed time, 0:19:36 cpu time, factor 1.65
15:12:00 Overall: 0:33:50 elapsed time, 5:19:01 cpu time, factor 9.43
15:12:01 
15:12:01 === SITEGEN ===
15:12:01 
15:12:01 Writing status file ...
15:12:01 Running sitegen ...
15:12:03 Success: Generated topics.shtml
15:12:03 Success: Generated index.shtml
15:12:03 Success: Generated shtml files for 347 entries
15:12:03 Success: Generated statistics.shtml
15:12:03 Success: Generated about.shtml
15:12:03 Success: Generated citing.shtml
15:12:03 Success: Generated updating.shtml
15:12:03 Success: Generated search.shtml
15:12:03 Success: Generated submitting.shtml
15:12:03 Success: Generated using.shtml
15:12:03 Success: Generated rss.xml
15:12:03 Success: Generated status.shtml
15:12:03 Packing tars ...
15:12:09 
15:12:09 === COMPLETED ===
15:12:09 
15:12:09 Archiving artifacts
15:12:58 Started calculate disk usage of build
15:12:58 Finished Calculation of disk usage of build in 0 seconds
15:13:08 Started calculate disk usage of workspace
15:13:09 Finished Calculation of disk usage of workspace in 0 seconds
15:13:09 No emails were triggered.
15:13:09 Finished: SUCCESS