Console Output

09:14:20 Started by upstream project "afp-repo" build number 857
09:14:20 originally caused by:
09:14:20  Started by an SCM change
09:14:20 [EnvInject] - Loading node environment variables.
09:14:20 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/afp-repo-afp
09:14:20 [afp-repo-afp] $ hg showconfig paths.default
09:14:20 [afp-repo-afp] $ hg pull --rev default
09:14:21 pulling from http://isabelle.in.tum.de/repos/isabelle/
09:14:21 searching for changes
09:14:21 adding changesets
09:14:21 adding manifests
09:14:21 adding file changes
09:14:21 added 2 changesets with 2 changes to 2 files
09:14:21 (run 'hg update' to get a working copy)
09:14:21 [afp-repo-afp] $ hg update --clean --rev default
09:14:21 2 files updated, 0 files merged, 0 files removed, 0 files unresolved
09:14:21 [afp-repo-afp] $ hg log --rev . --template {node}
09:14:21 [afp-repo-afp] $ hg log --rev . --template {rev}
09:14:21 [afp] $ hg showconfig paths.default
09:14:21 [afp] $ hg pull --rev d8029bd41c4cd90a77a5824af44cc44fdfdffdc9
09:14:22 pulling from https://bitbucket.org/isa-afp/afp-devel/
09:14:22 searching for changes
09:14:22 adding changesets
09:14:22 adding manifests
09:14:22 adding file changes
09:14:22 added 2 changesets with 2 changes to 2 files
09:14:22 (run 'hg update' to get a working copy)
09:14:22 [afp] $ hg update --clean --rev d8029bd41c4cd90a77a5824af44cc44fdfdffdc9
09:14:23 351 files updated, 0 files merged, 0 files removed, 0 files unresolved
09:14:23 [afp] $ hg --config extensions.purge= clean --all
09:14:23 [afp] $ hg log --rev . --template {node}
09:14:23 [afp] $ hg log --rev . --template {rev}
09:14:23 [afp] $ hg id --branch
09:14:23 No emails were triggered.
09:14:23 [afp-repo-afp] $ /bin/sh -xe /tmp/hudson8199440034093004631.sh
09:14:23 + Admin/jenkins/run_build afp
09:14:23 + set -e
09:14:23 + PROFILE=afp
09:14:23 + shift
09:14:23 + bin/isabelle components -a
09:14:23 + bin/isabelle jedit -bf
09:14:23 ### Building Isabelle/Scala ...
09:14:51 ### Building Isabelle/jEdit ...
09:15:06 + bin/isabelle ci_build_afp
09:15:12 
09:15:12 === CONFIGURATION ===
09:15:12 
09:15:12 ISABELLE_BUILD_OPTIONS=""
09:15:12 
09:15:12 ML_PLATFORM="x86_64-linux"
09:15:12 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
09:15:12 ML_SYSTEM="polyml-5.6"
09:15:12 ML_OPTIONS="-H 4000 --maxheap 8G"
09:15:12 
09:15:12 === BUILD ===
09:15:12 
09:15:12 Build started at Tue, 25 Apr 2017 07:15:12 GMT
09:15:12 Isabelle id 32d4117ad6e8
09:15:12 AFP id d8029bd41c4c
09:15:12 
09:15:12 === LOG ===
09:15:12 
09:15:13 Session Pure/Pure
09:15:13 Session HOL/HOL (main)
09:15:14 Session AFP/AVL-Trees (AFP)
09:15:14 Session AFP/AWN (AFP)
09:15:14 Session AFP/Abortable_Linearizable_Modules (AFP)
09:15:14 Session AFP/Abstract-Hoare-Logics (AFP)
09:15:14 Session AFP/Allen_Calculus (AFP)
09:15:14 Session AFP/Automatic_Refinement (AFP)
09:15:14 Session AFP/Refine_Monadic (AFP)
09:15:15 Session AFP/Collections (AFP)
09:15:15 Session AFP/CAVA_Base (AFP)
09:15:15 Session AFP/CAVA_Automata (AFP)
09:15:15 Session AFP/DFS_Framework (AFP)
09:15:15 Session AFP/Gabow_SCC (AFP)
09:15:15 Session AFP/LTL_to_GBA (AFP)
09:15:15 Session AFP/CAVA_buildchain1 (AFP)
09:15:15 Session AFP/CAVA_buildchain3 (AFP)
09:15:16 Session AFP/CAVA_LTL_Modelchecker (AFP)
09:15:16 Session AFP/Promela (AFP)
09:15:16 Session AFP/Collections_Examples (AFP)
09:15:16 Session AFP/Dijkstra_Shortest_Path (AFP)
09:15:16 Session AFP/Formal_SSA (AFP)
09:15:16 Session AFP/Minimal_SSA (AFP)
09:15:16 Session AFP/Sepref_Prereq (AFP)
09:15:16 Session AFP/Refine_Imperative_HOL (AFP)
09:15:16 Session AFP/Sepref_Basic (AFP)
09:15:16 Session AFP/Sepref_IICF (AFP)
09:15:16 Session AFP/EdmondsKarp_Base (AFP)
09:15:16 Session AFP/EdmondsKarp_Maxflow (AFP)
09:15:16 Session AFP/Transitive-Closure (AFP)
09:15:16 Session AFP/Tree-Automata (AFP)
09:15:16 Session AFP/BinarySearchTree (AFP)
09:15:16 Session AFP/Binomial-Queues (AFP)
09:15:16 Session AFP/Bondy (AFP)
09:15:16 Session AFP/Bounded_Deducibility_Security (AFP)
09:15:16 Session AFP/BytecodeLogicJmlTypes (AFP)
09:15:17 Session AFP/CISC-Kernel (AFP)
09:15:17 Session AFP/CYK (AFP)
09:15:17 Session AFP/Case_Labeling (AFP)
09:15:17 Session AFP/Cauchy (AFP)
09:15:17 Session AFP/Sqrt_Babylonian (AFP)
09:15:17 Session AFP/Real_Impl (AFP)
09:15:17 Session AFP/Certification_Monads (AFP)
09:15:17 Session AFP/ClockSynchInst (AFP)
09:15:17 Session AFP/Coinductive_Languages (AFP)
09:15:17 Session AFP/Compiling-Exceptions-Correctly (AFP)
09:15:17 Session AFP/Completeness (AFP)
09:15:17 Session AFP/ComponentDependencies (AFP)
09:15:17 Session AFP/Concurrent_Ref_Alg (AFP)
09:15:17 Session AFP/Consensus_Refined (AFP)
09:15:17 Session AFP/Constructor_Funs (AFP)
09:15:17 Session AFP/CryptoBasedCompositionalProperties (AFP)
09:15:17 Session AFP/DPT-SAT-Solver (AFP)
09:15:17 Session AFP/DataRefinementIBP (AFP)
09:15:17 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
09:15:17 Session AFP/Dependent_SIFUM_Refinement (AFP)
09:15:17 Session AFP/Depth-First-Search (AFP)
09:15:17 Session AFP/DiskPaxos (AFP)
09:15:17 Session AFP/Encodability_Process_Calculi (AFP)
09:15:17 Session AFP/Euler_Partition (AFP)
09:15:18 Session AFP/Example-Submission (AFP)
09:15:18 Session AFP/FFT (AFP)
09:15:18 Session AFP/FLP (AFP)
09:15:18 Session AFP/FOL_Harrison (AFP)
09:15:18 Session AFP/FeatherweightJava (AFP)
09:15:18 Session AFP/Featherweight_OCL (AFP)
09:15:18 Session AFP/FileRefinement (AFP)
09:15:18 Session AFP/FinFun (AFP)
09:15:18 Session AFP/Finite_Automata_HF (AFP)
09:15:18 Session AFP/FocusStreamsCaseStudies (AFP)
09:15:18 Session AFP/Free-Groups (AFP)
09:15:18 Session AFP/FunWithFunctions (AFP)
09:15:18 Session AFP/FunWithTilings (AFP)
09:15:18 Session AFP/GPU_Kernel_PL (AFP)
09:15:18 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
09:15:18 Session AFP/GenClock (AFP)
09:15:18 Session AFP/General-Triangle (AFP)
09:15:18 Session AFP/GoedelGod (AFP)
09:15:18 Session AFP/GraphMarkingIBP (AFP)
09:15:18 Session HOL/HOL-Library (main timing)
09:15:18 Session AFP/Abs_Int_ITP2012 (AFP)
09:15:19 Session AFP/Abstract-Rewriting (AFP)
09:15:19 Session AFP/Decreasing-Diagrams (AFP)
09:15:19 Session AFP/Decreasing-Diagrams-II (AFP)
09:15:19 Session AFP/Matrix (AFP)
09:15:19 Session AFP/Matrix_Tensor (AFP)
09:15:19 Session AFP/Knot_Theory (AFP)
09:15:19 Session AFP/Polynomials (AFP)
09:15:19 Session AFP/Groebner_Bases (AFP)
09:15:19 Session AFP/Abstract_Completeness (AFP)
09:15:19 Session AFP/Abstract_Soundness (AFP)
09:15:19 Session AFP/Amortized_Complexity (AFP)
09:15:19 Session AFP/Dynamic_Tables (AFP)
09:15:19 Session AFP/ArrowImpossibilityGS (AFP)
09:15:19 Session AFP/Bell_Numbers_Spivey (AFP)
09:15:19 Session AFP/Card_Equiv_Relations (AFP)
09:15:19 Session AFP/Binomial-Heaps (AFP)
09:15:19 Session AFP/Boolean_Expression_Checkers (AFP)
09:15:19 Session AFP/Buildings (AFP)
09:15:19 Session AFP/Card_Multisets (AFP)
09:15:19 Session AFP/Card_Number_Partitions (AFP)
09:15:19 Session AFP/Category (AFP)
09:15:19 Session AFP/Category2 (AFP)
09:15:19 Session AFP/Category3 (AFP)
09:15:19 Session AFP/CofGroups (AFP)
09:15:19 Session AFP/ConcurrentIMP (AFP)
09:15:19 Session AFP/CoreC++ (AFP)
09:15:19 Session AFP/Datatype_Order_Generator (AFP)
09:15:20 Session AFP/Old_Datatype_Show (AFP)
09:15:20 Session AFP/Derangements (AFP)
09:15:20 Session AFP/Deriving (AFP)
09:15:20 Session AFP/Containers (AFP)
09:15:20 Session AFP/Containers-Benchmarks (AFP)
09:15:21 Session AFP/Show (AFP)
09:15:21 Session AFP/Discrete_Summation (AFP)
09:15:21 Session AFP/Card_Partitions (AFP)
09:15:21 Session AFP/Efficient-Mergesort (AFP)
09:15:21 Session AFP/FOL-Fitting (AFP)
09:15:21 Session AFP/Finger-Trees (AFP)
09:15:21 Session AFP/Formula_Derivatives (AFP)
09:15:21 Session AFP/Formula_Derivatives-Examples (AFP)
09:15:21 Session AFP/Free-Boolean-Algebra (AFP)
09:15:21 Session AFP/Functional-Automata (AFP)
09:15:21 Session AFP/Graph_Theory (AFP)
09:15:21 Session AFP/ShortestPath (AFP)
09:15:21 Session AFP/Group-Ring-Module (AFP)
09:15:21 Session AFP/Valuation (AFP)
09:15:21 Session HOL/HOL-Cardinals (timing)
09:15:21 Session AFP/Ordinals_and_Cardinals (AFP)
09:15:21 Session AFP/Sort_Encodings (AFP)
09:15:21 Session HOL/HOL-Computational_Algebra
09:15:21 Session AFP/Bernoulli (AFP)
09:15:21 Session AFP/Coinductive (AFP)
09:15:22 Session AFP/Lazy-Lists-II (AFP)
09:15:22 Session AFP/Topology (AFP)
09:15:22 Session AFP/Stream_Fusion_Code (AFP)
09:15:22 Session AFP/Descartes_Sign_Rule (AFP)
09:15:22 Session HOL/HOL-Algebra (main timing)
09:15:22 Session AFP/JNF-HOL-Lib (AFP)
09:15:22 Session AFP/JNF-AFP-Lib (AFP)
09:15:22 Session AFP/Jordan_Normal_Form (AFP)
09:15:22 Session AFP/Pre_Perron_Frobenius (AFP)
09:15:22 Session AFP/Perron_Frobenius (AFP)
09:15:22 Session AFP/Subresultants (AFP)
09:15:23 Session AFP/Pre_BZ (AFP)
09:15:23 Session AFP/Berlekamp_Zassenhaus (AFP)
09:15:23 Session AFP/Pre_Algebraic_Numbers (AFP)
09:15:23 Session AFP/Algebraic_Numbers (AFP)
09:15:23 Session AFP/Algebraic_Numbers_Lib (AFP)
09:15:23 Session AFP/Pre_Polynomial_Factorization (AFP)
09:15:23 Session AFP/Polynomial_Factorization (AFP)
09:15:23 Session AFP/Jordan_Hoelder (AFP)
09:15:23 Session AFP/Perfect-Number-Thm (AFP)
09:15:23 Session AFP/Secondary_Sylow (AFP)
09:15:23 Session AFP/VectorSpace (AFP)
09:15:23 Session HOL/HOL-Analysis (main timing)
09:15:24 Session AFP/Affine_Arithmetic (AFP)
09:15:24 Session AFP/Cartan_FP (AFP)
09:15:24 Session AFP/Cayley_Hamilton (AFP)
09:15:24 Session AFP/Chord_Segments (AFP)
09:15:24 Session AFP/Echelon_Form (AFP)
09:15:24 Session AFP/Hermite (AFP)
09:15:24 Session AFP/Gauss_Jordan (AFP)
09:15:24 Session HOL/HOL-Probability (main timing)
09:15:24 Session AFP/Applicative_Lifting (AFP)
09:15:24 Session AFP/Stern_Brocot (AFP)
09:15:24 Session AFP/Deep_Learning_Lib (AFP)
09:15:24 Session AFP/Deep_Learning (AFP)
09:15:25 Session AFP/Density_Compiler (AFP)
09:15:25 Session AFP/Ergodic_Theory (AFP)
09:15:25 Session AFP/Fisher_Yates (AFP)
09:15:25 Session AFP/Girth_Chromatic (AFP)
09:15:25 Session AFP/List_Update (AFP)
09:15:25 Session AFP/Lp (AFP)
09:15:25 Session AFP/MFMC_Countable (AFP)
09:15:25 Session AFP/Markov_Models (AFP)
09:15:25 Session AFP/Probabilistic_Noninterference (AFP)
09:15:25 Session AFP/Probabilistic_System_Zoo (AFP)
09:15:25 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
09:15:26 Session AFP/Quick_Sort_Cost (AFP)
09:15:26 Session AFP/Random_BSTs (AFP)
09:15:26 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
09:15:26 Session AFP/Randomised_Social_Choice (AFP)
09:15:26 Session AFP/SDS_Impossibility (AFP)
09:15:26 Session AFP/Source_Coding_Theorem (AFP)
09:15:26 Session AFP/UpDown_Scheme (AFP)
09:15:26 Session AFP/Landau_Analysis (AFP)
09:15:26 Session AFP/Akra_Bazzi (AFP)
09:15:26 Session AFP/Catalan_Numbers (AFP)
09:15:27 Session AFP/Euler_MacLaurin (AFP)
09:15:27 Session AFP/Stirling_Formula (AFP)
09:15:27 Session AFP/Comparison_Sort_Lower_Bound (AFP)
09:15:27 Session AFP/Lower_Semicontinuous (AFP)
09:15:27 Session AFP/Ordinary_Differential_Equations (AFP)
09:15:27 Session AFP/HOL-ODE (AFP)
09:15:27 Session AFP/Differential_Dynamic_Logic (AFP)
09:15:27 Session AFP/HOL-ODE-Refinement (AFP)
09:15:28 Session AFP/HOL-ODE-Numerics (AFP)
09:15:28 Session AFP/Prime_Harmonic_Series (AFP)
09:15:28 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
09:15:28 Session AFP/Ptolemys_Theorem (AFP)
09:15:28 Session AFP/QR_Decomposition (AFP)
09:15:28 Session AFP/Rank_Nullity_Theorem (AFP)
09:15:28 Session AFP/Tarskis_Geometry (AFP)
09:15:28 Session AFP/Triangle (AFP)
09:15:28 Session AFP/pGCL (AFP)
09:15:28 Session HOL/HOL-Number_Theory (timing)
09:15:28 Session AFP/Bertrands_Postulate (AFP)
09:15:29 Session AFP/E_Transcendental (AFP)
09:15:29 Session AFP/Elliptic_Curves_Group_Law (AFP)
09:15:29 Session AFP/Fermat3_4 (AFP)
09:15:29 Session AFP/Koenigsberg_Friendship_Base (AFP)
09:15:29 Session AFP/Koenigsberg_Friendship (AFP)
09:15:29 Session AFP/Lehmer (AFP)
09:15:29 Session AFP/Pratt_Certificate (AFP)
09:15:29 Session AFP/SumSquares (AFP)
09:15:29 Session AFP/Liouville_Numbers (AFP)
09:15:29 Session AFP/Polynomial_Interpolation (AFP)
09:15:29 Session AFP/RSAPSS (AFP)
09:15:29 Session AFP/Rep_Fin_Groups (AFP)
09:15:29 Session AFP/Sturm_Sequences (AFP)
09:15:29 Session AFP/Special_Function_Bounds (AFP)
09:15:29 Session AFP/Sturm_Tarski (AFP)
09:15:29 Session HOL/HOL-Imperative_HOL
09:15:29 Session AFP/Imperative_Insertion_Sort (AFP)
09:15:29 Session AFP/HereditarilyFinite (AFP)
09:15:29 Session AFP/Incompleteness (AFP)
09:15:30 Session AFP/Surprise_Paradox (AFP)
09:15:30 Session AFP/HyperCTL (AFP)
09:15:30 Session AFP/Incredible_Proof_Machine (AFP)
09:15:30 Session AFP/Integration (AFP)
09:15:30 Session AFP/Isabelle_Meta_Model (AFP)
09:15:30 Session AFP/Jinja (AFP)
09:15:30 Session AFP/HRB-Slicing (AFP)
09:15:30 Session AFP/InformationFlowSlicing_Inter (AFP)
09:15:30 Session AFP/Slicing (AFP)
09:15:30 Session AFP/InformationFlowSlicing (AFP)
09:15:30 Session AFP/KBPs (AFP)
09:15:30 Session AFP/LTL (AFP)
09:15:30 Session AFP/LTL_to_DRA (AFP)
09:15:30 Session AFP/Stuttering_Equivalence (AFP)
09:15:30 Session AFP/Lambda_Free_RPOs (AFP)
09:15:30 Session AFP/Landau_Symbols (AFP)
09:15:31 Session AFP/LightweightJava (AFP)
09:15:31 Session AFP/LinearQuantifierElim (AFP)
09:15:31 Session AFP/List-Infinite (AFP)
09:15:31 Session AFP/Nat-Interval-Logic (AFP)
09:15:31 Session AFP/AutoFocus-Stream (AFP)
09:15:31 Session AFP/MSO_Regex_Equivalence (AFP)
09:15:31 Session AFP/MSO_Examples (AFP)
09:15:31 Session AFP/MuchAdoAboutTwo (AFP)
09:15:31 Session AFP/Myhill-Nerode (AFP)
09:15:31 Session AFP/POPLmark-deBruijn (AFP)
09:15:31 Session AFP/Pairing_Heap (AFP)
09:15:31 Session AFP/Password_Authentication_Protocol (AFP)
09:15:31 Session AFP/Presburger-Automata (AFP)
09:15:31 Session AFP/Priority_Queue_Braun (AFP)
09:15:31 Session AFP/Program-Conflict-Analysis (AFP)
09:15:31 Session AFP/Regex_Equivalence (AFP)
09:15:31 Session AFP/Regex_Equivalence_Examples (AFP)
09:15:31 Session AFP/Regular-Sets (AFP)
09:15:31 Session AFP/Posix-Lexing (AFP)
09:15:31 Session AFP/Ribbon_Proofs (AFP)
09:15:31 Session AFP/SATSolverVerification (AFP)
09:15:31 Session AFP/Selection_Heap_Sort (AFP)
09:15:31 Session AFP/Separata (AFP)
09:15:32 Session AFP/Separation_Logic_Imperative_HOL (AFP)
09:15:32 Session AFP/Skew_Heap (AFP)
09:15:32 Session AFP/Splay_Tree (AFP)
09:15:32 Session AFP/Stable_Matching (AFP)
09:15:32 Session AFP/SuperCalc (AFP)
09:15:32 Session AFP/Tail_Recursive_Functions (AFP)
09:15:32 Session AFP/TortoiseHare (AFP)
09:15:32 Session AFP/Trie (AFP)
09:15:32 Session AFP/Twelvefold_Way (AFP)
09:15:32 Session AFP/Vickrey_Clarke_Groves (AFP)
09:15:32 Session AFP/Well_Quasi_Orders (AFP)
09:15:32 Session AFP/XML (AFP)
09:15:32 Session HOL/HOL-Nominal
09:15:32 Session AFP/CCS (AFP)
09:15:33 Session AFP/Lam-ml-Normalization (AFP)
09:15:33 Session AFP/Pi_Calculus (AFP)
09:15:33 Session AFP/Psi_Calculi (AFP)
09:15:33 Session AFP/SequentInvertibility (AFP)
09:15:33 Session HOL/HOL-Word (main timing)
09:15:33 Session HOL/HOL-SPARK (main)
09:15:33 Session HOL/HOL-SPARK-Examples
09:15:33 Session AFP/RIPEMD-160-SPARK (AFP)
09:15:33 Session AFP/Kleene_Algebra (AFP)
09:15:33 Session AFP/KAT_and_DRA (AFP)
09:15:34 Session AFP/Algebraic_VCs (AFP)
09:15:34 Session AFP/Multirelations (AFP)
09:15:34 Session AFP/Regular_Algebras (AFP)
09:15:34 Session AFP/Relation_Algebra (AFP)
09:15:34 Session AFP/Residuated_Lattices (AFP)
09:15:34 Session AFP/Native_Word (AFP)
09:15:34 Session AFP/SPARCv8 (AFP)
09:15:34 Session AFP/Separation_Algebra (AFP)
09:15:34 Session AFP/Word_Lib (AFP)
09:15:34 Session AFP/Complx (AFP)
09:15:34 Session AFP/IP_Addresses (AFP)
09:15:34 Session AFP/Simple_Firewall (AFP)
09:15:34 Session AFP/Routing (AFP)
09:15:34 Session AFP/Iptables_Semantics (AFP)
09:15:35 Session AFP/LOFT (AFP)
09:15:35 Session HOL/HOLCF (main timing)
09:15:35 Session AFP/Circus (AFP)
09:15:35 Session AFP/HOLCF-HOL-Library (AFP)
09:15:35 Session AFP/HOLCF-Nominal2 (AFP)
09:15:35 Session AFP/Launchbury (AFP)
09:15:35 Session AFP/Call_Arity (AFP)
09:15:35 Session HOL/HOLCF-Library
09:15:35 Session AFP/PCF (AFP)
09:15:35 Session AFP/Shivers-CFA (AFP)
09:15:36 Session AFP/Stream-Fusion (AFP)
09:15:36 Session AFP/Tycon (AFP)
09:15:36 Session AFP/WorkerWrapper (AFP)
09:15:36 Session AFP/Heard_Of (AFP)
09:15:36 Session AFP/HotelKeyCards (AFP)
09:15:36 Session AFP/Huffman (AFP)
09:15:36 Session AFP/IEEE_Floating_Point (AFP)
09:15:36 Session AFP/Impossible_Geometry (AFP)
09:15:36 Session AFP/Inductive_Confidentiality (AFP)
09:15:36 Session AFP/InfPathElimination (AFP)
09:15:36 Session AFP/JiveDataStoreModel (AFP)
09:15:36 Session AFP/KAD (AFP)
09:15:36 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
09:15:36 Session AFP/LatticeProperties (AFP)
09:15:36 Session AFP/MonoBoolTranAlgebra (AFP)
09:15:36 Session AFP/PseudoHoops (AFP)
09:15:36 Session AFP/Lazy_Case (AFP)
09:15:36 Session AFP/Lifting_Definition_Option (AFP)
09:15:36 Session AFP/List-Index (AFP)
09:15:36 Session AFP/List_Interleaving (AFP)
09:15:36 Session AFP/Locally-Nameless-Sigma (AFP)
09:15:36 Session AFP/Marriage (AFP)
09:15:36 Session AFP/Latin_Square (AFP)
09:15:36 Session AFP/Max-Card-Matching (AFP)
09:15:36 Session AFP/Menger (AFP)
09:15:36 Session AFP/MiniML (AFP)
09:15:36 Session AFP/Network_Security_Policy_Verification (AFP)
09:15:36 Session AFP/No_FTL_observers (AFP)
09:15:36 Session AFP/Nominal2 (AFP)
09:15:37 Session AFP/Modal_Logics_for_NTS (AFP)
09:15:37 Session AFP/Rewriting_Z (AFP)
09:15:37 Session AFP/Noninterference_CSP (AFP)
09:15:37 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
09:15:37 Session AFP/Noninterference_Generic_Unwinding (AFP)
09:15:37 Session AFP/Noninterference_Inductive_Unwinding (AFP)
09:15:37 Session AFP/Noninterference_Sequential_Composition (AFP)
09:15:37 Session AFP/Noninterference_Concurrent_Composition (AFP)
09:15:37 Session AFP/NormByEval (AFP)
09:15:37 Session AFP/Open_Induction (AFP)
09:15:37 Session AFP/Ordinal (AFP)
09:15:37 Session AFP/Nested_Multisets_Ordinals (AFP)
09:15:37 Session AFP/Lambda_Free_KBOs (AFP)
09:15:37 Session AFP/Paraconsistency (AFP)
09:15:37 Session AFP/Parity_Game (AFP)
09:15:37 Session AFP/Partial_Function_MR (AFP)
09:15:37 Session AFP/Pop_Refinement (AFP)
09:15:38 Session AFP/Possibilistic_Noninterference (AFP)
09:15:38 Session AFP/Proof_Strategy_Language (AFP)
09:15:38 Session AFP/PropResPI (AFP)
09:15:38 Session AFP/ROBDD (AFP)
09:15:38 Session AFP/Ramsey-Infinite (AFP)
09:15:38 Session AFP/Recursion-Theory-I (AFP)
09:15:38 Session AFP/RefinementReactive (AFP)
09:15:38 Session AFP/Resolution_FOL (AFP)
09:15:38 Session AFP/Robbins-Conjecture (AFP)
09:15:38 Session AFP/Roy_Floyd_Warshall (AFP)
09:15:38 Session AFP/SIFPL (AFP)
09:15:38 Session AFP/SIFUM_Type_Systems (AFP)
09:15:38 Session AFP/SenSocialChoice (AFP)
09:15:38 Session AFP/Simpl (AFP)
09:15:38 Session AFP/BDD (AFP)
09:15:38 Session AFP/Planarity_Certificates (AFP)
09:15:38 Session AFP/Statecharts (AFP)
09:15:39 Session AFP/Stone_Algebras (AFP)
09:15:39 Session AFP/Stone_Relation_Algebras (AFP)
09:15:39 Session AFP/Strong_Security (AFP)
09:15:39 Session AFP/TLA (AFP)
09:15:39 Session AFP/Timed_Automata (AFP)
09:15:39 Session AFP/Transitive-Closure-II (AFP)
09:15:39 Session AFP/Tree_Decomposition (AFP)
09:15:39 Session AFP/UPF (AFP)
09:15:39 Session AFP/UPF_Firewall (AFP)
09:15:39 Session AFP/Verified-Prover (AFP)
09:15:39 Session AFP/VolpanoSmith (AFP)
09:15:39 Session AFP/WHATandWHERE_Security (AFP)
09:15:41 Building HOL-Computational_Algebra ...
09:15:42 Building HOLCF ...
09:15:42 Running Knot_Theory ...
09:15:42 Running Show ...
09:15:44 HOLCF: theory HOLCF.Old_Datatype
09:15:44 HOLCF: theory HOLCF.Nat_Bijection
09:15:45 HOLCF: theory HOLCF.Countable
09:15:46 HOLCF: theory HOLCF.Porder
09:15:47 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
09:15:47 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
09:15:47 HOLCF: theory HOLCF.Pcpo
09:15:48 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
09:15:48 HOLCF: theory HOLCF.Cont
09:15:48 Knot_Theory: theory Knot_Theory.Fraction_Field
09:15:48 Knot_Theory: theory Knot_Theory.Polynomial
09:15:49 HOLCF: theory HOLCF.Adm
09:15:49 HOLCF: theory HOLCF.Discrete
09:15:49 Show: theory Show.Polynomial
09:15:49 Show: theory Show.Show
09:15:49 HOLCF: theory HOLCF.Cpodef
09:15:49 HOLCF: theory HOLCF.Fun_Cpo
09:15:49 HOLCF: theory HOLCF.Product_Cpo
09:15:50 HOLCF: theory HOLCF.Cfun
09:15:50 Show: theory Show.Show_Instances
09:15:51 HOLCF: theory HOLCF.Completion
09:15:51 HOLCF: theory HOLCF.Cprod
09:15:51 HOLCF: theory HOLCF.Deflation
09:15:51 HOLCF: theory HOLCF.Fix
09:15:51 HOLCF: theory HOLCF.Sfun
09:15:51 HOLCF: theory HOLCF.Sprod
09:15:51 HOLCF: theory HOLCF.Up
09:15:52 Show: theory Show.Show_Real
09:15:52 Show: theory Show.Show_Complex
09:15:52 HOLCF: theory HOLCF.Lift
09:15:53 Show: theory Show.Show_Real_Impl
09:15:53 HOLCF: theory HOLCF.One
09:15:53 HOLCF: theory HOLCF.Tr
09:15:53 HOLCF: theory HOLCF.Ssum
09:15:53 HOLCF: theory HOLCF.Fixrec
09:15:53 HOLCF: theory HOLCF.Map_Functions
09:15:54 HOLCF: theory HOLCF.Bifinite
09:15:55 HOLCF: theory HOLCF.Domain_Aux
09:15:56 HOLCF: theory HOLCF.Universal
09:15:56 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
09:15:56 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
09:15:57 Show: theory Show.Show_Poly
09:15:57 HOLCF: theory HOLCF.Algebraic
09:15:57 HOLCF: theory HOLCF.Compact_Basis
09:15:57 HOLCF: theory HOLCF.LowerPD
09:15:57 HOLCF: theory HOLCF.UpperPD
09:15:57 HOLCF: theory HOLCF.Representable
09:15:58 HOLCF: theory HOLCF.ConvexPD
09:16:00 Knot_Theory: theory Knot_Theory.Preliminaries
09:16:00 Knot_Theory: theory Knot_Theory.Tangle_Relation
09:16:00 HOLCF: theory HOLCF.Domain
09:16:01 Knot_Theory: theory Knot_Theory.Tangles
09:16:02 Knot_Theory: theory Knot_Theory.Tangle_Algebra
09:16:02 HOLCF: theory HOLCF.Powerdomains
09:16:03 Knot_Theory: theory Knot_Theory.Tangle_Moves
09:16:03 HOLCF: theory HOLCF
09:16:03 Knot_Theory: theory Knot_Theory.Link_Algebra
09:16:04 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
09:16:04 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
09:16:04 Knot_Theory: theory Knot_Theory.Example
09:16:04 Knot_Theory: theory Knot_Theory.Kauffman_Matrix
09:16:05 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
09:16:05 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
09:16:06 Timing Show (2 threads, 13.434s elapsed time, 25.180s cpu time, 1.448s GC time, factor 1.87)
09:16:06 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Show
09:16:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Show/document.pdf
09:16:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Show/outline.pdf
09:16:06 Finished Show (0:00:23 elapsed time, 0:00:36 cpu time, factor 1.56)
09:16:06 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
09:16:07 Knot_Theory: theory Knot_Theory.Computations
09:16:07 Knot_Theory: theory Knot_Theory.Linkrel_Kauffman
09:16:08 Knot_Theory: theory Knot_Theory.Kauffman_Invariance
09:16:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
09:16:08 Knot_Theory: theory Knot_Theory.Knot_Theory
09:16:09 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
09:16:26 Timing HOLCF (2 threads, 19.484s elapsed time, 36.068s cpu time, 2.296s GC time, factor 1.85)
09:16:26 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF
09:16:26 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF/document.pdf
09:16:26 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF/outline.pdf
09:16:26 Finished HOLCF (0:00:44 elapsed time, 0:01:13 cpu time, factor 1.67)
09:16:26 Building HOLCF-HOL-Library ...
09:16:26 Building HOLCF-Library ...
09:16:27 Running Circus ...
09:16:27 Running Shivers-CFA ...
09:16:27 Running WorkerWrapper ...
09:16:27 Running Tycon ...
09:16:29 Shivers-CFA: theory Shivers-CFA.Adhoc_Overloading
09:16:29 Circus: theory Circus.Sublist
09:16:29 HOLCF-Library: theory HOLCF-Library.Infinite_Set
09:16:29 HOLCF-Library: theory HOLCF-Library.Bool_Discrete
09:16:29 HOLCF-HOL-Library: theory HOLCF-HOL-Library.AList
09:16:29 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Cancellation
09:16:29 WorkerWrapper: theory WorkerWrapper.Maybe
09:16:29 WorkerWrapper: theory WorkerWrapper.Nats
09:16:29 Tycon: theory Tycon.Coerce
09:16:29 Tycon: theory Tycon.TypeApp
09:16:29 Shivers-CFA: theory Shivers-CFA.FixTransform
09:16:29 Shivers-CFA: theory Shivers-CFA.HOLCFUtils
09:16:29 HOLCF-Library: theory HOLCF-Library.Char_Discrete
09:16:29 Shivers-CFA: theory Shivers-CFA.CPSScheme
09:16:29 Shivers-CFA: theory Shivers-CFA.Computability
09:16:29 Tycon: theory Tycon.Functor
09:16:29 HOLCF-Library: theory HOLCF-Library.Countable_Set
09:16:30 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite
09:16:30 Shivers-CFA: theory Shivers-CFA.SetMap
09:16:30 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Multiset
09:16:30 Shivers-CFA: theory Shivers-CFA.Utils
09:16:30 Shivers-CFA: theory Shivers-CFA.MapSets
09:16:30 HOLCF-Library: theory HOLCF-Library.Countable_Complete_Lattices
09:16:30 WorkerWrapper: theory WorkerWrapper.LList
09:16:30 HOLCF-Library: theory HOLCF-Library.Int_Discrete
09:16:31 Tycon: theory Tycon.Monad
09:16:31 HOLCF-Library: theory HOLCF-Library.List_Cpo
09:16:31 HOLCF-HOL-Library: theory HOLCF-HOL-Library.FuncSet
09:16:31 HOLCF-Library: theory HOLCF-Library.Nat_Discrete
09:16:31 HOLCF-Library: theory HOLCF-Library.Sum_Cpo
09:16:31 Tycon: theory Tycon.Binary_Tree_Monad
09:16:31 Tycon: theory Tycon.Lift_Monad
09:16:31 Circus: theory Circus.Var
09:16:31 Circus: theory Circus.Var_list
09:16:31 Circus: theory Circus.Relations
09:16:31 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Infinite_Set
09:16:32 Tycon: theory Tycon.Monad_Plus
09:16:32 HOLCF-HOL-Library: theory HOLCF-HOL-Library.LaTeXsugar
09:16:32 HOLCF-Library: theory HOLCF-Library.List_Predomain
09:16:32 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Syntax
09:16:32 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Option
09:16:32 Tycon: theory Tycon.Monad_Zero
09:16:32 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
09:16:33 Tycon: theory Tycon.Error_Monad
09:16:33 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
09:16:33 Tycon: theory Tycon.Resumption_Transformer
09:16:33 WorkerWrapper: theory WorkerWrapper.CounterExample
09:16:33 WorkerWrapper: theory WorkerWrapper.Last
09:16:33 Circus: theory Circus.Designs
09:16:33 HOLCF-Library: theory HOLCF-Library.Option_Cpo
09:16:33 WorkerWrapper: theory WorkerWrapper.Streams
09:16:33 Tycon: theory Tycon.Error_Transformer
09:16:33 HOLCF-Library: theory HOLCF-Library.Order_Continuity
09:16:33 HOLCF-Library: theory HOLCF-Library.HOL_Cpo
09:16:34 Circus: theory Circus.Reactive_Processes
09:16:34 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
09:16:34 Tycon: theory Tycon.Monad_Zero_Plus
09:16:34 WorkerWrapper: theory WorkerWrapper.Accumulator
09:16:34 Tycon: theory Tycon.Writer_Monad
09:16:34 Tycon: theory Tycon.Lazy_List_Monad
09:16:34 WorkerWrapper: theory WorkerWrapper.Backtracking
09:16:34 HOLCF-Library: theory HOLCF-Library.Extended_Nat
09:16:35 Tycon: theory Tycon.Maybe_Monad
09:16:35 WorkerWrapper: theory WorkerWrapper.Continuations
09:16:35 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Permutation
09:16:35 Tycon: theory Tycon.State_Transformer
09:16:36 Tycon: theory Tycon.Writer_Transformer
09:16:36 HOLCF-Library: theory HOLCF-Library.Stream
09:16:37 Tycon: theory Tycon.Monad_Transformer
09:16:37 Circus: theory Circus.CSP_Processes
09:16:37 HOLCF-Library: theory HOLCF-Library.HOLCF_Library
09:16:37 WorkerWrapper: theory WorkerWrapper.Nub
09:16:38 Circus: theory Circus.Circus_Actions
09:16:38 Shivers-CFA: theory Shivers-CFA.CPSUtils
09:16:38 WorkerWrapper: theory WorkerWrapper.UnboxedNats
09:16:39 Circus: theory Circus.Denotational_Semantics
09:16:41 Shivers-CFA: theory Shivers-CFA.Eval
09:16:42 Timing Tycon (2 threads, 10.472s elapsed time, 19.480s cpu time, 0.580s GC time, factor 1.86)
09:16:42 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tycon
09:16:42 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tycon/document.pdf
09:16:42 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tycon/outline.pdf
09:16:42 Finished Tycon (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.67)
09:16:42 Running Stream-Fusion ...
09:16:42 Shivers-CFA: theory Shivers-CFA.AbsCF
09:16:42 Shivers-CFA: theory Shivers-CFA.ExCF
09:16:44 Timing WorkerWrapper (2 threads, 12.631s elapsed time, 23.720s cpu time, 1.008s GC time, factor 1.88)
09:16:44 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/WorkerWrapper
09:16:44 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/WorkerWrapper/document.pdf
09:16:44 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/WorkerWrapper/outline.pdf
09:16:44 Finished WorkerWrapper (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.70)
09:16:45 Shivers-CFA: theory Shivers-CFA.ExCFSV
09:16:45 Stream-Fusion: theory Stream-Fusion.Int_Discrete
09:16:45 Stream-Fusion: theory Stream-Fusion.LazyList
09:16:46 Stream-Fusion: theory Stream-Fusion.Stream
09:16:46 Shivers-CFA: theory Shivers-CFA.AbsCFComp
09:16:48 Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
09:16:48 Stream-Fusion: theory Stream-Fusion.StreamFusion
09:16:54 Circus: theory Circus.Circus_Syntax
09:16:54 Circus: theory Circus.Refinement
09:16:54 Circus: theory Circus.Refinement_Example
09:16:57 Timing Stream-Fusion (2 threads, 10.046s elapsed time, 13.492s cpu time, 0.460s GC time, factor 1.34)
09:16:57 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream-Fusion
09:16:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream-Fusion/document.pdf
09:16:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream-Fusion/outline.pdf
09:16:57 Finished Stream-Fusion (0:00:14 elapsed time, 0:00:18 cpu time, factor 1.29)
09:17:02 Timing HOLCF-Library (2 threads, 14.739s elapsed time, 29.112s cpu time, 1.120s GC time, factor 1.98)
09:17:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOLCF-Library
09:17:02 Finished HOLCF-Library (0:00:34 elapsed time, 0:00:58 cpu time, factor 1.68)
09:17:02 Running PCF ...
09:17:03 Timing HOLCF-HOL-Library (2 threads, 15.854s elapsed time, 30.496s cpu time, 1.296s GC time, factor 1.92)
09:17:03 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOLCF-HOL-Library
09:17:03 Finished HOLCF-HOL-Library (0:00:36 elapsed time, 0:01:01 cpu time, factor 1.68)
09:17:03 Timing Shivers-CFA (2 threads, 30.177s elapsed time, 58.668s cpu time, 2.848s GC time, factor 1.94)
09:17:03 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Shivers-CFA
09:17:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Shivers-CFA/document.pdf
09:17:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Shivers-CFA/outline.pdf
09:17:03 Finished Shivers-CFA (0:00:36 elapsed time, 0:01:06 cpu time, factor 1.83)
09:17:03 Building HOLCF-Nominal2 ...
09:17:05 PCF: theory PCF.Product_Plus
09:17:05 PCF: theory PCF.Dual_Lattice
09:17:05 PCF: theory PCF.Product_Order
09:17:06 PCF: theory PCF.Basis
09:17:06 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Set
09:17:06 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Product
09:17:07 HOLCF-Nominal2: theory HOLCF-Nominal2.FSet
09:17:07 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_List
09:17:07 HOLCF-Nominal2: theory HOLCF-Nominal2.Phantom_Type
09:17:07 PCF: theory PCF.Logical_Relations
09:17:08 HOLCF-Nominal2: theory HOLCF-Nominal2.Cardinality
09:17:08 PCF: theory PCF.PCF
09:17:09 HOLCF-Nominal2: theory HOLCF-Nominal2.FinFun
09:17:12 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Base
09:17:13 PCF: theory PCF.Continuations
09:17:13 PCF: theory PCF.OpSem
09:17:15 Warning: missing document directory
09:17:15 Timing HOL-Computational_Algebra (2 threads, 57.520s elapsed time, 105.072s cpu time, 4.656s GC time, factor 1.83)
09:17:15 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Computational_Algebra
09:17:15 Finished HOL-Computational_Algebra (0:01:32 elapsed time, 0:02:37 cpu time, factor 1.69)
09:17:15 Building HOL-Analysis ...
09:17:15 Building HOL-Number_Theory ...
09:17:16 Building HOL-Algebra ...
09:17:16 Building Coinductive ...
09:17:17 HOLCF-Nominal2: theory HOLCF-Nominal2.Atoms
09:17:17 HOLCF-Nominal2: theory HOLCF-Nominal2.Eqvt
09:17:17 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Abs
09:17:19 Timing Knot_Theory (2 threads, 86.873s elapsed time, 169.700s cpu time, 5.344s GC time, factor 1.95)
09:17:19 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory
09:17:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory/document.pdf
09:17:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory/outline.pdf
09:17:19 Finished Knot_Theory (0:01:36 elapsed time, 0:03:00 cpu time, factor 1.87)
09:17:19 Building Sturm_Sequences ...
09:17:19 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_FCB
09:17:20 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2
09:17:22 HOL-Number_Theory: theory HOL-Number_Theory.Congruence
09:17:22 Coinductive: theory Coinductive.L2_Norm
09:17:22 Coinductive: theory Coinductive.Inner_Product
09:17:22 HOL-Algebra: theory HOL-Algebra.Exponent
09:17:22 HOL-Algebra: theory HOL-Algebra.Congruence
09:17:22 Coinductive: theory Coinductive.Norm_Arith
09:17:23 HOL-Number_Theory: theory HOL-Number_Theory.Order
09:17:23 HOL-Analysis: theory HOL-Analysis.L2_Norm
09:17:23 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
09:17:23 HOL-Algebra: theory HOL-Algebra.Order
09:17:23 HOL-Analysis: theory HOL-Analysis.Inner_Product
09:17:23 Coinductive: theory Coinductive.Product_Vector
09:17:24 HOL-Analysis: theory HOL-Analysis.Operator_Norm
09:17:24 HOL-Analysis: theory HOL-Analysis.Poly_Roots
09:17:24 Coinductive: theory Coinductive.Euclidean_Space
09:17:24 HOL-Analysis: theory HOL-Analysis.Summation_Tests
09:17:24 HOL-Number_Theory: theory HOL-Number_Theory.Lattice
09:17:25 HOL-Algebra: theory HOL-Algebra.Lattice
09:17:25 HOL-Analysis: theory HOL-Analysis.Product_Vector
09:17:25 Sturm_Sequences: theory Sturm_Sequences.Sturm_Library_Document
09:17:25 Sturm_Sequences: theory Sturm_Sequences.Misc_Polynomial
09:17:25 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
09:17:25 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
09:17:26 HOL-Number_Theory: theory HOL-Number_Theory.Complete_Lattice
09:17:26 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
09:17:26 Coinductive: theory Coinductive.Linear_Algebra
09:17:27 HOL-Number_Theory: theory HOL-Number_Theory.Group
09:17:27 HOL-Algebra: theory HOL-Algebra.Galois_Connection
09:17:28 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
09:17:28 HOL-Algebra: theory HOL-Algebra.Group
09:17:28 HOL-Number_Theory: theory HOL-Number_Theory.FiniteProduct
09:17:29 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
09:17:29 HOL-Analysis: theory HOL-Analysis.Measurable
09:17:29 HOL-Number_Theory: theory HOL-Number_Theory.Ring
09:17:29 Coinductive: theory Coinductive.Topology_Euclidean_Space
09:17:30 HOL-Analysis: theory HOL-Analysis.Measure_Space
09:17:30 Sturm_Sequences: theory Sturm_Sequences.Sturm_Library
09:17:30 HOL-Algebra: theory HOL-Algebra.Bij
09:17:30 HOL-Algebra: theory HOL-Algebra.Coset
09:17:30 HOL-Algebra: theory HOL-Algebra.FiniteProduct
09:17:30 Sturm_Sequences: theory Sturm_Sequences.Sturm_Theorem
09:17:31 HOL-Algebra: theory HOL-Algebra.Ring
09:17:31 HOL-Algebra: theory HOL-Algebra.Sylow
09:17:32 Sturm_Sequences: theory Sturm_Sequences.Sturm_Method
09:17:32 HOL-Analysis: theory HOL-Analysis.Norm_Arith
09:17:32 HOL-Algebra: theory HOL-Algebra.Divisibility
09:17:32 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
09:17:32 Sturm_Sequences: theory Sturm_Sequences.Sturm
09:17:33 HOL-Analysis: theory HOL-Analysis.Caratheodory
09:17:33 Sturm_Sequences: theory Sturm_Sequences.Sturm_Ex
09:17:35 HOL-Algebra: theory HOL-Algebra.AbelCoset
09:17:36 HOL-Algebra: theory HOL-Algebra.Module
09:17:37 Timing Circus (2 threads, 49.081s elapsed time, 94.568s cpu time, 3.160s GC time, factor 1.93)
09:17:37 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Circus
09:17:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Circus/document.pdf
09:17:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Circus/outline.pdf
09:17:37 Finished Circus (0:01:10 elapsed time, 0:02:12 cpu time, factor 1.89)
09:17:37 Running RSAPSS ...
09:17:38 HOL-Algebra: theory HOL-Algebra.More_Group
09:17:38 HOL-Algebra: theory HOL-Algebra.More_Finite_Product
09:17:39 HOL-Algebra: theory HOL-Algebra.More_Ring
09:17:40 Coinductive: theory Coinductive.Extended_Real_Limits
09:17:42 HOL-Algebra: theory HOL-Algebra.Ideal
09:17:43 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
09:17:43 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
09:17:44 RSAPSS: theory RSAPSS.Word
09:17:45 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
09:17:46 HOL-Analysis: theory HOL-Analysis.Tagged_Division
09:17:47 HOL-Algebra: theory HOL-Algebra.RingHom
09:17:47 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
09:17:49 RSAPSS: theory RSAPSS.Cong
09:17:49 RSAPSS: theory RSAPSS.Totient
09:17:49 RSAPSS: theory RSAPSS.Congruence
09:17:49 HOL-Algebra: theory HOL-Algebra.QuotRing
09:17:49 HOL-Algebra: theory HOL-Algebra.UnivPoly
09:17:49 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
09:17:49 RSAPSS: theory RSAPSS.Mod
09:17:49 RSAPSS: theory RSAPSS.Crypt
09:17:49 RSAPSS: theory RSAPSS.Pdifference
09:17:50 HOL-Analysis: theory HOL-Analysis.Path_Connected
09:17:50 RSAPSS: theory RSAPSS.Order
09:17:50 HOL-Algebra: theory HOL-Algebra.IntRing
09:17:50 RSAPSS: theory RSAPSS.Productdivides
09:17:50 RSAPSS: theory RSAPSS.WordOperations
09:17:51 Timing HOLCF-Nominal2 (2 threads, 22.398s elapsed time, 44.176s cpu time, 2.228s GC time, factor 1.97)
09:17:51 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOLCF-Nominal2
09:17:51 Finished HOLCF-Nominal2 (0:00:46 elapsed time, 0:01:20 cpu time, factor 1.71)
09:17:51 Building Launchbury ...
09:17:51 RSAPSS: theory RSAPSS.Lattice
09:17:53 RSAPSS: theory RSAPSS.Complete_Lattice
09:17:53 RSAPSS: theory RSAPSS.SHA1Padding
09:17:53 RSAPSS: theory RSAPSS.SHA1
09:17:53 Timing PCF (2 threads, 46.326s elapsed time, 89.132s cpu time, 2.696s GC time, factor 1.92)
09:17:53 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF
09:17:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF/document.pdf
09:17:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF/outline.pdf
09:17:53 Finished PCF (0:00:51 elapsed time, 0:01:34 cpu time, factor 1.85)
09:17:53 Running Rep_Fin_Groups ...
09:17:53 RSAPSS: theory RSAPSS.Group
09:17:54 RSAPSS: theory RSAPSS.Wordarith
09:17:54 HOL-Analysis: theory HOL-Analysis.Homeomorphism
09:17:54 RSAPSS: theory RSAPSS.EMSAPSS
09:17:54 Launchbury: theory Launchbury.Mono-Nat-Fun
09:17:54 Launchbury: theory Launchbury.Nominal-Utils
09:17:54 Launchbury: theory Launchbury.Vars
09:17:55 Launchbury: theory Launchbury.C
09:17:55 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
09:17:55 Launchbury: theory Launchbury.HOLCF-Join
09:17:55 RSAPSS: theory RSAPSS.Coset
09:17:55 Launchbury: theory Launchbury.HOLCF-Join-Classes
09:17:55 Launchbury: theory Launchbury.CValue
09:17:56 RSAPSS: theory RSAPSS.FiniteProduct
09:17:56 Launchbury: theory Launchbury.HOLCF-Meet
09:17:56 RSAPSS: theory RSAPSS.Ring
09:17:57 Launchbury: theory Launchbury.Value
09:17:57 HOL-Number_Theory: theory HOL-Number_Theory.Cong
09:17:57 HOL-Number_Theory: theory HOL-Number_Theory.Totient
09:17:57 Launchbury: theory Launchbury.C-Meet
09:17:57 HOL-Analysis: theory HOL-Analysis.Derivative
09:17:57 HOL-Number_Theory: theory HOL-Number_Theory.Coset
09:17:57 Launchbury: theory Launchbury.AList-Utils
09:17:57 Launchbury: theory Launchbury.Env
09:17:58 Launchbury: theory Launchbury.AList-Utils-Nominal
09:17:58 HOL-Number_Theory: theory HOL-Number_Theory.Module
09:17:58 Launchbury: theory Launchbury.Pointwise
09:17:58 Launchbury: theory Launchbury.HOLCF-Utils
09:17:58 Launchbury: theory Launchbury.Terms
09:17:58 Launchbury: theory Launchbury.C-restr
09:17:59 HOL-Number_Theory: theory HOL-Number_Theory.AbelCoset
09:17:59 Launchbury: theory Launchbury.Env-HOLCF
09:17:59 Launchbury: theory Launchbury.Iterative
09:18:00 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
09:18:00 Launchbury: theory Launchbury.EvalHeap
09:18:00 Rep_Fin_Groups: theory Rep_Fin_Groups.Rep_Fin_Groups
09:18:00 HOL-Number_Theory: theory HOL-Number_Theory.More_Group
09:18:01 RSAPSS: theory RSAPSS.AbelCoset
09:18:01 HOL-Number_Theory: theory HOL-Number_Theory.More_Finite_Product
09:18:01 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
09:18:01 HOL-Number_Theory: theory HOL-Number_Theory.More_Ring
09:18:01 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
09:18:02 RSAPSS: theory RSAPSS.Module
09:18:02 Launchbury: theory Launchbury.Nominal-HOLCF
09:18:02 HOL-Number_Theory: theory HOL-Number_Theory.Fib
09:18:03 HOL-Analysis: theory HOL-Analysis.Determinants
09:18:04 Launchbury: theory Launchbury.CValue-Nominal
09:18:04 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
09:18:04 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
09:18:04 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
09:18:04 RSAPSS: theory RSAPSS.More_Group
09:18:04 RSAPSS: theory RSAPSS.More_Finite_Product
09:18:04 Launchbury: theory Launchbury.Env-Nominal
09:18:05 RSAPSS: theory RSAPSS.More_Ring
09:18:05 Launchbury: theory Launchbury.HasESem
09:18:06 Launchbury: theory Launchbury.HeapSemantics
09:18:06 HOL-Number_Theory: theory HOL-Number_Theory.Ideal
09:18:06 HOL-Analysis: theory HOL-Analysis.Polytope
09:18:07 Launchbury: theory Launchbury.Substitution
09:18:07 Launchbury: theory Launchbury.AbstractDenotational
09:18:08 Launchbury: theory Launchbury.Launchbury
09:18:08 RSAPSS: theory RSAPSS.Ideal
09:18:09 Launchbury: theory Launchbury.Abstract-Denotational-Props
09:18:09 Launchbury: theory Launchbury.ResourcedDenotational
09:18:10 Launchbury: theory Launchbury.Value-Nominal
09:18:10 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
09:18:11 HOL-Analysis: theory HOL-Analysis.Borel_Space
09:18:11 Launchbury: theory Launchbury.CorrectnessResourced
09:18:11 HOL-Number_Theory: theory HOL-Number_Theory.RingHom
09:18:11 Launchbury: theory Launchbury.Denotational
09:18:11 Launchbury: theory Launchbury.ResourcedAdequacy
09:18:11 Launchbury: theory Launchbury.ValueSimilarity
09:18:11 Launchbury: theory Launchbury.CorrectnessOriginal
09:18:12 Launchbury: theory Launchbury.Denotational-Related
09:18:13 HOL-Number_Theory: theory HOL-Number_Theory.UnivPoly
09:18:13 RSAPSS: theory RSAPSS.RingHom
09:18:13 Launchbury: theory Launchbury.Adequacy
09:18:14 Coinductive: theory Coinductive.Resumption
09:18:14 Coinductive: theory Coinductive.Coinductive_Nat
09:18:14 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
09:18:14 Launchbury: theory Launchbury.EverythingAdequacy
09:18:15 Coinductive: theory Coinductive.Coinductive_List
09:18:15 RSAPSS: theory RSAPSS.UnivPoly
09:18:15 Coinductive: theory Coinductive.CCPO_Topology
09:18:16 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
09:18:17 HOL-Analysis: theory HOL-Analysis.Regularity
09:18:17 HOL-Analysis: theory HOL-Analysis.Embed_Measure
09:18:18 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
09:18:19 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
09:18:20 HOL-Analysis: theory HOL-Analysis.Function_Topology
09:18:21 HOL-Analysis: theory HOL-Analysis.Complete_Measure
09:18:21 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
09:18:22 Coinductive: theory Coinductive.Coinductive_List_Prefix
09:18:22 HOL-Analysis: theory HOL-Analysis.Set_Integral
09:18:22 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
09:18:22 Coinductive: theory Coinductive.Hamming_Stream
09:18:23 Coinductive: theory Coinductive.Koenigslemma
09:18:24 Coinductive: theory Coinductive.LMirror
09:18:24 Coinductive: theory Coinductive.Lazy_LList
09:18:24 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
09:18:24 Coinductive: theory Coinductive.Quotient_Coinductive_List
09:18:24 Coinductive: theory Coinductive.TLList
09:18:25 Coinductive: theory Coinductive.Coinductive_Stream
09:18:26 Coinductive: theory Coinductive.LList_CCPO_Topology
09:18:27 Coinductive: theory Coinductive.Lazy_TLList
09:18:28 Coinductive: theory Coinductive.Quotient_TLList
09:18:28 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
09:18:28 HOL-Number_Theory: theory HOL-Number_Theory.Multiplicative_Group
09:18:28 Coinductive: theory Coinductive.TLList_CCPO
09:18:28 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
09:18:28 HOL-Analysis: theory HOL-Analysis.Integral_Test
09:18:29 Coinductive: theory Coinductive.TLList_CCPO_Examples
09:18:29 Coinductive: theory Coinductive.Coinductive
09:18:29 Coinductive: theory Coinductive.Coinductive_Examples
09:18:29 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
09:18:29 HOL-Analysis: theory HOL-Analysis.Interval_Integral
09:18:30 RSAPSS: theory RSAPSS.Multiplicative_Group
09:18:30 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
09:18:31 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
09:18:31 HOL-Number_Theory: theory HOL-Number_Theory.Residues
09:18:33 Timing Sturm_Sequences (2 threads, 42.111s elapsed time, 82.452s cpu time, 1.568s GC time, factor 1.96)
09:18:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Sequences
09:18:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Sequences/document.pdf
09:18:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Sequences/outline.pdf
09:18:33 Finished Sturm_Sequences (0:01:13 elapsed time, 0:02:07 cpu time, factor 1.72)
09:18:33 Running Special_Function_Bounds ...
09:18:33 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
09:18:33 RSAPSS: theory RSAPSS.Residues
09:18:33 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
09:18:33 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem
09:18:34 HOL-Analysis: theory HOL-Analysis.Further_Topology
09:18:35 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
09:18:35 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
09:18:35 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
09:18:36 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
09:18:36 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
09:18:37 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
09:18:37 RSAPSS: theory RSAPSS.Cryptinverts
09:18:38 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings
09:18:38 HOL-Analysis: theory HOL-Analysis.Gamma_Function
09:18:38 RSAPSS: theory RSAPSS.RSAPSS
09:18:39 HOL-Analysis: theory HOL-Analysis.Great_Picard
09:18:39 Special_Function_Bounds: theory Special_Function_Bounds.Bounds_Lemmas
09:18:40 Special_Function_Bounds: theory Special_Function_Bounds.Atan_CF_Bounds
09:18:40 Special_Function_Bounds: theory Special_Function_Bounds.Exp_Bounds
09:18:40 HOL-Analysis: theory HOL-Analysis.Winding_Numbers
09:18:41 Special_Function_Bounds: theory Special_Function_Bounds.Log_CF_Bounds
09:18:41 Special_Function_Bounds: theory Special_Function_Bounds.Sin_Cos_Bounds
09:18:41 Special_Function_Bounds: theory Special_Function_Bounds.Sqrt_Bounds
09:18:42 HOL-Analysis: theory HOL-Analysis.Analysis
09:19:18 Timing Launchbury (2 threads, 49.691s elapsed time, 91.820s cpu time, 3.204s GC time, factor 1.85)
09:19:18 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Launchbury
09:19:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Launchbury/document.pdf
09:19:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Launchbury/outline.pdf
09:19:18 Finished Launchbury (0:01:26 elapsed time, 0:02:28 cpu time, factor 1.71)
09:19:18 Running Call_Arity ...
09:19:19 Timing Special_Function_Bounds (2 threads, 36.736s elapsed time, 66.620s cpu time, 1.128s GC time, factor 1.81)
09:19:19 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Special_Function_Bounds
09:19:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Special_Function_Bounds/document.pdf
09:19:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Special_Function_Bounds/outline.pdf
09:19:19 Finished Special_Function_Bounds (0:00:45 elapsed time, 0:01:16 cpu time, factor 1.68)
09:19:19 Running Polynomial_Interpolation ...
09:19:23 Call_Arity: theory Call_Arity.BalancedTraces
09:19:23 Call_Arity: theory Call_Arity.ConstOn
09:19:23 Call_Arity: theory Call_Arity.List-Interleavings
09:19:23 Call_Arity: theory Call_Arity.Set-Cpo
09:19:23 Call_Arity: theory Call_Arity.Arity
09:19:23 Call_Arity: theory Call_Arity.TTree
09:19:24 Call_Arity: theory Call_Arity.EtaExpansion
09:19:24 Call_Arity: theory Call_Arity.SestoftConf
09:19:25 Call_Arity: theory Call_Arity.AEnv
09:19:25 Timing RSAPSS (2 threads, 98.508s elapsed time, 192.312s cpu time, 10.020s GC time, factor 1.95)
09:19:25 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS
09:19:25 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS/document.pdf
09:19:25 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS/outline.pdf
09:19:25 Finished RSAPSS (0:01:47 elapsed time, 0:03:21 cpu time, factor 1.88)
09:19:25 Running Sturm_Tarski ...
09:19:25 Polynomial_Interpolation: theory Polynomial_Interpolation.Sqrt_Babylonian_Auxiliary
09:19:26 Call_Arity: theory Call_Arity.ArityStack
09:19:26 Call_Arity: theory Call_Arity.Sestoft
09:19:26 Call_Arity: theory Call_Arity.EtaExpansionSafe
09:19:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
09:19:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Improved_Code_Equations
09:19:27 Call_Arity: theory Call_Arity.SestoftGC
09:19:27 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Unsorted
09:19:27 Call_Arity: theory Call_Arity.SestoftCorrect
09:19:27 Call_Arity: theory Call_Arity.Env-Set-Cpo
09:19:28 Polynomial_Interpolation: theory Polynomial_Interpolation.Is_Rat_To_Rat
09:19:28 Call_Arity: theory Call_Arity.AList-Utils-HOLCF
09:19:28 Call_Arity: theory Call_Arity.AnalBinds
09:19:28 Call_Arity: theory Call_Arity.Cardinality-Domain
09:19:28 Call_Arity: theory Call_Arity.CardinalityAnalysisSig
09:19:29 Polynomial_Interpolation: theory Polynomial_Interpolation.Missing_Polynomial
09:19:29 Polynomial_Interpolation: theory Polynomial_Interpolation.Divmod_Int
09:19:29 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom
09:19:30 Call_Arity: theory Call_Arity.CoCallGraph
09:19:30 Call_Arity: theory Call_Arity.TTree-HOLCF
09:19:30 Polynomial_Interpolation: theory Polynomial_Interpolation.Lagrange_Interpolation
09:19:31 Call_Arity: theory Call_Arity.TTreeAnalysisSig
09:19:31 Polynomial_Interpolation: theory Polynomial_Interpolation.Ring_Hom_Poly
09:19:32 Sturm_Tarski: theory Sturm_Tarski.PolyMisc
09:19:32 Call_Arity: theory Call_Arity.CoCallAnalysisSig
09:19:32 Sturm_Tarski: theory Sturm_Tarski.Sturm_Tarski
09:19:32 Call_Arity: theory Call_Arity.CoCallGraph-TTree
09:19:33 Call_Arity: theory Call_Arity.Arity-Nominal
09:19:33 Polynomial_Interpolation: theory Polynomial_Interpolation.Newton_Interpolation
09:19:33 Timing HOL-Algebra (2 threads, 86.741s elapsed time, 164.340s cpu time, 9.352s GC time, factor 1.89)
09:19:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra
09:19:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf
09:19:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf
09:19:33 Finished HOL-Algebra (0:02:17 elapsed time, 0:04:00 cpu time, factor 1.75)
09:19:33 Call_Arity: theory Call_Arity.Cardinality-Domain-Lists
09:19:34 Call_Arity: theory Call_Arity.ArityAnalysisSig
09:19:34 Building JNF-HOL-Lib ...
09:19:34 Call_Arity: theory Call_Arity.ArityAnalysisAbinds
09:19:35 Call_Arity: theory Call_Arity.ArityAnalysisStack
09:19:35 Call_Arity: theory Call_Arity.ArityAnalysisSpec
09:19:36 Call_Arity: theory Call_Arity.CardinalityAnalysisSpec
09:19:36 Call_Arity: theory Call_Arity.ArityAnalysisFix
09:19:36 Call_Arity: theory Call_Arity.ArityAnalysisFixProps
09:19:37 Call_Arity: theory Call_Arity.ArityConsistent
09:19:37 Call_Arity: theory Call_Arity.NoCardinalityAnalysis
09:19:37 Polynomial_Interpolation: theory Polynomial_Interpolation.Polynomial_Interpolation
09:19:38 Call_Arity: theory Call_Arity.CoCallAritySig
09:19:38 Call_Arity: theory Call_Arity.TTreeAnalysisSpec
09:19:38 Timing Rep_Fin_Groups (2 threads, 93.707s elapsed time, 146.988s cpu time, 4.280s GC time, factor 1.57)
09:19:38 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rep_Fin_Groups
09:19:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rep_Fin_Groups/document.pdf
09:19:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rep_Fin_Groups/outline.pdf
09:19:38 Finished Rep_Fin_Groups (0:01:44 elapsed time, 0:02:39 cpu time, factor 1.53)
09:19:38 Call_Arity: theory Call_Arity.CoCallAnalysisSpec
09:19:38 Running VectorSpace ...
09:19:39 Call_Arity: theory Call_Arity.CoCallImplTTree
09:19:39 Call_Arity: theory Call_Arity.TTreeImplCardinality
09:19:40 Call_Arity: theory Call_Arity.CoCallImplTTreeSafe
09:19:41 Call_Arity: theory Call_Arity.TTreeImplCardinalitySafe
09:19:41 Call_Arity: theory Call_Arity.CoCallGraph-Nominal
09:19:41 Call_Arity: theory Call_Arity.CoCallAnalysisBinds
09:19:42 JNF-HOL-Lib: theory JNF-HOL-Lib.Order_Union
09:19:42 Call_Arity: theory Call_Arity.TransformTools
09:19:42 JNF-HOL-Lib: theory JNF-HOL-Lib.Wellorder_Extension
09:19:43 Call_Arity: theory Call_Arity.AbstractTransform
09:19:43 Call_Arity: theory Call_Arity.ArityEtaExpansion
09:19:43 Timing Coinductive (2 threads, 99.001s elapsed time, 183.952s cpu time, 7.332s GC time, factor 1.86)
09:19:43 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive
09:19:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive/document.pdf
09:19:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Coinductive/outline.pdf
09:19:43 Finished Coinductive (0:02:27 elapsed time, 0:04:22 cpu time, factor 1.78)
09:19:44 Building Lazy-Lists-II ...
09:19:44 Call_Arity: theory Call_Arity.ArityEtaExpansionSafe
09:19:44 Call_Arity: theory Call_Arity.CoCallFix
09:19:45 Call_Arity: theory Call_Arity.ArityTransform
09:19:46 Call_Arity: theory Call_Arity.CoCallAnalysisImpl
09:19:46 Call_Arity: theory Call_Arity.ArityTransformSafe
09:19:46 VectorSpace: theory VectorSpace.FunctionLemmas
09:19:46 VectorSpace: theory VectorSpace.RingModuleFacts
09:19:48 Call_Arity: theory Call_Arity.CardArityTransformSafe
09:19:48 Call_Arity: theory Call_Arity.CallArityEnd2End
09:19:48 VectorSpace: theory VectorSpace.MonoidSums
09:19:49 VectorSpace: theory VectorSpace.LinearCombinations
09:19:49 Call_Arity: theory Call_Arity.CoCallImplSafe
09:19:49 Timing Polynomial_Interpolation (2 threads, 20.686s elapsed time, 40.832s cpu time, 1.668s GC time, factor 1.97)
09:19:49 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Interpolation
09:19:49 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Interpolation/document.pdf
09:19:49 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Interpolation/outline.pdf
09:19:49 Finished Polynomial_Interpolation (0:00:30 elapsed time, 0:00:51 cpu time, factor 1.71)
09:19:49 Running Jordan_Hoelder ...
09:19:50 Call_Arity: theory Call_Arity.TrivialArityAnal
09:19:50 Call_Arity: theory Call_Arity.CallArityEnd2EndSafe
09:19:50 Call_Arity: theory Call_Arity.ArityAnalysisCorrDenotational
09:19:51 Timing Sturm_Tarski (2 threads, 16.859s elapsed time, 33.332s cpu time, 0.600s GC time, factor 1.98)
09:19:51 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Tarski
09:19:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Tarski/document.pdf
09:19:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sturm_Tarski/outline.pdf
09:19:51 Finished Sturm_Tarski (0:00:25 elapsed time, 0:00:42 cpu time, factor 1.68)
09:19:51 Running Stream_Fusion_Code ...
09:19:52 Lazy-Lists-II: theory Lazy-Lists-II.LList2
09:19:52 Timing HOL-Number_Theory (2 threads, 106.582s elapsed time, 205.692s cpu time, 9.196s GC time, factor 1.93)
09:19:52 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory
09:19:52 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/document.pdf
09:19:52 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/outline.pdf
09:19:52 Finished HOL-Number_Theory (0:02:35 elapsed time, 0:04:39 cpu time, factor 1.79)
09:19:52 Building Lehmer ...
09:19:58 Jordan_Hoelder: theory Jordan_Hoelder.GroupAction
09:19:58 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupConjugation
09:19:59 Jordan_Hoelder: theory Jordan_Hoelder.SndSylow
09:19:59 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion
09:19:59 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List
09:19:59 VectorSpace: theory VectorSpace.SumSpaces
09:20:01 Lehmer: theory Lehmer.Lehmer
09:20:01 VectorSpace: theory VectorSpace.VectorSpace
09:20:03 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
09:20:03 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp
09:20:03 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups
09:20:04 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups
09:20:04 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
09:20:04 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
09:20:05 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
09:20:07 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList
09:20:08 Timing JNF-HOL-Lib (2 threads, 1.493s elapsed time, 2.848s cpu time, 0.000s GC time, factor 1.91)
09:20:08 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/JNF-HOL-Lib
09:20:08 Finished JNF-HOL-Lib (0:00:34 elapsed time, 0:00:47 cpu time, factor 1.41)
09:20:08 Building JNF-AFP-Lib ...
09:20:09 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples
09:20:17 JNF-AFP-Lib: theory JNF-AFP-Lib.IArray_Addenda
09:20:17 JNF-AFP-Lib: theory JNF-AFP-Lib.Containers_Auxiliary
09:20:17 JNF-AFP-Lib: theory JNF-AFP-Lib.IArray_Haskell
09:20:17 JNF-AFP-Lib: theory JNF-AFP-Lib.Missing_Unsorted
09:20:17 JNF-AFP-Lib: theory JNF-AFP-Lib.Comparator
09:20:18 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare
09:20:19 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Comparator_Impl
09:20:19 JNF-AFP-Lib: theory JNF-AFP-Lib.Missing_Polynomial
09:20:20 Timing Lazy-Lists-II (2 threads, 2.207s elapsed time, 3.968s cpu time, 0.200s GC time, factor 1.80)
09:20:20 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lazy-Lists-II
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lazy-Lists-II/document.pdf
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lazy-Lists-II/outline.pdf
09:20:20 Finished Lazy-Lists-II (0:00:35 elapsed time, 0:00:51 cpu time, factor 1.44)
09:20:20 Timing Stream_Fusion_Code (2 threads, 17.287s elapsed time, 32.820s cpu time, 1.532s GC time, factor 1.90)
09:20:20 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream_Fusion_Code
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream_Fusion_Code/document.pdf
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stream_Fusion_Code/outline.pdf
09:20:20 Finished Stream_Fusion_Code (0:00:28 elapsed time, 0:00:46 cpu time, factor 1.59)
09:20:20 JNF-AFP-Lib: theory JNF-AFP-Lib.Derive_Manager
09:20:20 Timing Jordan_Hoelder (2 threads, 19.662s elapsed time, 36.476s cpu time, 1.428s GC time, factor 1.86)
09:20:20 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder/document.pdf
09:20:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder/outline.pdf
09:20:20 Finished Jordan_Hoelder (0:00:30 elapsed time, 0:00:48 cpu time, factor 1.57)
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.Equal
09:20:21 Building Koenigsberg_Friendship_Base ...
09:20:21 Running Elliptic_Curves_Group_Law ...
09:20:21 Running Bertrands_Postulate ...
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.Closure_Set
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.Extend_Partial_Order
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.FunctionLemmas
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.Generator_Aux
09:20:21 JNF-AFP-Lib: theory JNF-AFP-Lib.Comparator_Generator
09:20:23 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare_Generator
09:20:23 JNF-AFP-Lib: theory JNF-AFP-Lib.Compare_Instances
09:20:24 JNF-AFP-Lib: theory JNF-AFP-Lib.Containers_Generator
09:20:24 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Enum
09:20:24 JNF-AFP-Lib: theory JNF-AFP-Lib.Equality_Generator
09:20:25 JNF-AFP-Lib: theory JNF-AFP-Lib.Equality_Instances
09:20:25 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Eq
09:20:25 JNF-AFP-Lib: theory JNF-AFP-Lib.List_Fusion
09:20:26 JNF-AFP-Lib: theory JNF-AFP-Lib.DList_Set
09:20:26 JNF-AFP-Lib: theory JNF-AFP-Lib.Lexicographic_Order
09:20:27 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_ext
09:20:27 JNF-AFP-Lib: theory JNF-AFP-Lib.Set_Linorder
09:20:28 Timing Lehmer (2 threads, 1.903s elapsed time, 3.456s cpu time, 0.000s GC time, factor 1.82)
09:20:28 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer
09:20:28 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer/document.pdf
09:20:28 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer/outline.pdf
09:20:28 Finished Lehmer (0:00:35 elapsed time, 0:00:50 cpu time, factor 1.43)
09:20:28 Running Fermat3_4 ...
09:20:29 Koenigsberg_Friendship_Base: theory Koenigsberg_Friendship_Base.Graph
09:20:29 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Conversions
09:20:29 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Algebra_Aux
09:20:29 Bertrands_Postulate: theory Bertrands_Postulate.Dense_Linear_Order
09:20:29 JNF-AFP-Lib: theory JNF-AFP-Lib.Regular_Set
09:20:30 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Commutative_Ring
09:20:31 JNF-AFP-Lib: theory JNF-AFP-Lib.Regular_Exp
09:20:31 Bertrands_Postulate: theory Bertrands_Postulate.Approximation
09:20:34 JNF-AFP-Lib: theory JNF-AFP-Lib.NDerivative
09:20:36 Fermat3_4: theory Fermat3_4.Fermat4
09:20:36 Fermat3_4: theory Fermat3_4.Quad_Form
09:20:37 Fermat3_4: theory Fermat3_4.Fermat3
09:20:38 JNF-AFP-Lib: theory JNF-AFP-Lib.Collection_Order
09:20:39 JNF-AFP-Lib: theory JNF-AFP-Lib.Equivalence_Checking
09:20:39 JNF-AFP-Lib: theory JNF-AFP-Lib.Relation_Interpretation
09:20:39 JNF-AFP-Lib: theory JNF-AFP-Lib.Regexp_Method
09:20:40 JNF-AFP-Lib: theory JNF-AFP-Lib.RingModuleFacts
09:20:41 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Mapping2
09:20:41 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Reflective_Field
09:20:42 JNF-AFP-Lib: theory JNF-AFP-Lib.MonoidSums
09:20:42 JNF-AFP-Lib: theory JNF-AFP-Lib.RBT_Set2
09:20:42 JNF-AFP-Lib: theory JNF-AFP-Lib.LinearCombinations
09:20:43 Timing VectorSpace (2 threads, 53.944s elapsed time, 95.480s cpu time, 4.324s GC time, factor 1.77)
09:20:43 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace
09:20:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace/document.pdf
09:20:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace/outline.pdf
09:20:43 Finished VectorSpace (0:01:04 elapsed time, 0:01:46 cpu time, factor 1.66)
09:20:43 Running Pratt_Certificate ...
09:20:44 JNF-AFP-Lib: theory JNF-AFP-Lib.Set_Impl
09:20:48 Timing Call_Arity (2 threads, 79.447s elapsed time, 151.364s cpu time, 6.760s GC time, factor 1.91)
09:20:48 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Call_Arity
09:20:48 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Call_Arity/document.pdf
09:20:48 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Call_Arity/outline.pdf
09:20:48 Finished Call_Arity (0:01:29 elapsed time, 0:02:44 cpu time, factor 1.84)
09:20:48 Running SumSquares ...
09:20:51 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
09:20:52 JNF-AFP-Lib: theory JNF-AFP-Lib.Seq
09:20:53 JNF-AFP-Lib: theory JNF-AFP-Lib.Abstract_Rewriting
09:20:54 Timing Koenigsberg_Friendship_Base (2 threads, 1.111s elapsed time, 1.724s cpu time, 0.000s GC time, factor 1.55)
09:20:54 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship_Base
09:20:54 Finished Koenigsberg_Friendship_Base (0:00:33 elapsed time, 0:00:47 cpu time, factor 1.41)
09:20:55 Running Koenigsberg_Friendship ...
09:20:55 JNF-AFP-Lib: theory JNF-AFP-Lib.Relative_Rewriting
09:20:55 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Locale
09:20:55 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Axclass
09:20:56 SumSquares: theory SumSquares.FourSquares
09:20:56 SumSquares: theory SumSquares.TwoSquares
09:20:56 JNF-AFP-Lib: theory JNF-AFP-Lib.SN_Orders
09:20:59 JNF-AFP-Lib: theory JNF-AFP-Lib.Ordered_Semiring
09:21:00 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Test
09:21:00 JNF-AFP-Lib: theory JNF-AFP-Lib.SN_Order_Carrier
09:21:02 JNF-AFP-Lib: theory JNF-AFP-Lib.Show
09:21:03 Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph
09:21:03 JNF-AFP-Lib: theory JNF-AFP-Lib.Show_Instances
09:21:04 Timing Fermat3_4 (2 threads, 24.077s elapsed time, 49.896s cpu time, 0.872s GC time, factor 2.07)
09:21:04 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4
09:21:04 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4/document.pdf
09:21:04 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4/outline.pdf
09:21:04 Finished Fermat3_4 (0:00:34 elapsed time, 0:01:01 cpu time, factor 1.76)
09:21:04 Running Bernoulli ...
09:21:04 JNF-AFP-Lib: theory JNF-AFP-Lib.SumSpaces
09:21:05 JNF-AFP-Lib: theory JNF-AFP-Lib.Utility
09:21:05 JNF-AFP-Lib: theory JNF-AFP-Lib.VectorSpace
09:21:06 Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory
09:21:08 Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge
09:21:10 Timing SumSquares (2 threads, 10.383s elapsed time, 17.848s cpu time, 0.380s GC time, factor 1.72)
09:21:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares
09:21:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares/document.pdf
09:21:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares/outline.pdf
09:21:10 Finished SumSquares (0:00:20 elapsed time, 0:00:28 cpu time, factor 1.40)
09:21:10 Running Topology ...
09:21:10 Bernoulli: theory Bernoulli.Bernoulli
09:21:11 Bernoulli: theory Bernoulli.Bernoulli_FPS
09:21:11 Bernoulli: theory Bernoulli.Periodic_Bernpoly
09:21:17 Timing Pratt_Certificate (2 threads, 22.998s elapsed time, 44.064s cpu time, 0.664s GC time, factor 1.92)
09:21:17 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate
09:21:17 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate/document.pdf
09:21:17 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate/outline.pdf
09:21:17 Finished Pratt_Certificate (0:00:33 elapsed time, 0:00:54 cpu time, factor 1.66)
09:21:17 Running Secondary_Sylow ...
09:21:18 Topology: theory Topology.Topology
09:21:21 Topology: theory Topology.LList_Topology
09:21:21 Timing Bernoulli (2 threads, 8.752s elapsed time, 15.760s cpu time, 0.348s GC time, factor 1.80)
09:21:21 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bernoulli
09:21:21 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bernoulli/document.pdf
09:21:21 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bernoulli/outline.pdf
09:21:21 Finished Bernoulli (0:00:17 elapsed time, 0:00:25 cpu time, factor 1.45)
09:21:21 Running Descartes_Sign_Rule ...
09:21:25 Secondary_Sylow: theory Secondary_Sylow.GroupAction
09:21:25 Bertrands_Postulate: theory Bertrands_Postulate.Bertrand
09:21:26 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
09:21:26 Secondary_Sylow: theory Secondary_Sylow.SndSylow
09:21:27 Timing Topology (2 threads, 6.168s elapsed time, 11.928s cpu time, 0.920s GC time, factor 1.93)
09:21:27 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Topology
09:21:27 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Topology/document.pdf
09:21:27 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Topology/outline.pdf
09:21:27 Finished Topology (0:00:16 elapsed time, 0:00:23 cpu time, factor 1.40)
09:21:27 Running Liouville_Numbers ...
09:21:28 Descartes_Sign_Rule: theory Descartes_Sign_Rule.Descartes_Sign_Rule
09:21:33 Timing Descartes_Sign_Rule (2 threads, 2.976s elapsed time, 5.316s cpu time, 0.192s GC time, factor 1.79)
09:21:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Descartes_Sign_Rule
09:21:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Descartes_Sign_Rule/document.pdf
09:21:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Descartes_Sign_Rule/outline.pdf
09:21:33 Finished Descartes_Sign_Rule (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.26)
09:21:33 Timing Secondary_Sylow (2 threads, 5.742s elapsed time, 11.032s cpu time, 0.328s GC time, factor 1.92)
09:21:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow
09:21:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow/document.pdf
09:21:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow/outline.pdf
09:21:33 Finished Secondary_Sylow (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.37)
09:21:33 Running Perfect-Number-Thm ...
09:21:33 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers_Misc
09:21:34 Liouville_Numbers: theory Liouville_Numbers.Liouville_Numbers
09:21:38 Timing Liouville_Numbers (2 threads, 2.438s elapsed time, 4.100s cpu time, 0.000s GC time, factor 1.68)
09:21:38 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Liouville_Numbers
09:21:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Liouville_Numbers/document.pdf
09:21:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Liouville_Numbers/outline.pdf
09:21:38 Finished Liouville_Numbers (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.21)
09:21:41 Timing Bertrands_Postulate (2 threads, 69.562s elapsed time, 117.688s cpu time, 4.904s GC time, factor 1.69)
09:21:41 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate
09:21:41 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate/document.pdf
09:21:41 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate/outline.pdf
09:21:41 Finished Bertrands_Postulate (0:01:19 elapsed time, 0:02:08 cpu time, factor 1.61)
09:21:41 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
09:21:41 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
09:21:42 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
09:21:43 Timing Elliptic_Curves_Group_Law (2 threads, 71.323s elapsed time, 133.844s cpu time, 5.964s GC time, factor 1.88)
09:21:43 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law
09:21:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/document.pdf
09:21:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/outline.pdf
09:21:43 Finished Elliptic_Curves_Group_Law (0:01:22 elapsed time, 0:02:26 cpu time, factor 1.77)
09:21:45 Timing Perfect-Number-Thm (2 threads, 2.159s elapsed time, 4.156s cpu time, 0.092s GC time, factor 1.92)
09:21:45 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm
09:21:45 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm/document.pdf
09:21:45 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm/outline.pdf
09:21:45 Finished Perfect-Number-Thm (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.22)
09:22:11 Timing Koenigsberg_Friendship (2 threads, 64.349s elapsed time, 119.548s cpu time, 5.056s GC time, factor 1.86)
09:22:11 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship
09:22:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship/document.pdf
09:22:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship/outline.pdf
09:22:11 Finished Koenigsberg_Friendship (0:01:16 elapsed time, 0:02:12 cpu time, factor 1.74)
09:23:48 Timing JNF-AFP-Lib (2 threads, 147.021s elapsed time, 287.328s cpu time, 16.548s GC time, factor 1.95)
09:23:48 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/JNF-AFP-Lib
09:23:48 Finished JNF-AFP-Lib (0:03:39 elapsed time, 0:06:41 cpu time, factor 1.83)
09:23:49 Building Jordan_Normal_Form ...
09:23:49 Building Pre_Polynomial_Factorization ...
09:24:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
09:24:00 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Improved_Code_Equations
09:24:00 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Neville_Aitken_Interpolation
09:24:01 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Lagrange_Interpolation
09:24:01 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.CauchysMeanTheorem
09:24:01 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian_Auxiliary
09:24:01 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Show_Poly
09:24:02 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Is_Rat_To_Rat
09:24:03 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Log_Impl
09:24:03 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.NthRoot_Impl
09:24:04 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Divmod_Int
09:24:04 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Partial_Function_MR
09:24:04 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian
09:24:04 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom
09:24:05 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Permutations
09:24:06 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom_Poly
09:24:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
09:24:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Order_Polynomial
09:24:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Fundamental_Theorem_Algebra_Factorized
09:24:08 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Newton_Interpolation
09:24:08 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
09:24:08 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
09:24:09 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
09:24:09 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom
09:24:11 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Polynomial_Interpolation
09:24:11 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
09:24:12 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Poly
09:24:16 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
09:24:17 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
09:24:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
09:24:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
09:24:19 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
09:24:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
09:24:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
09:24:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
09:24:24 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
09:24:24 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
09:24:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
09:24:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
09:24:29 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
09:24:29 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
09:24:31 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
09:24:32 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
09:24:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
09:24:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
09:24:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
09:24:35 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
09:24:40 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
09:24:44 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
09:24:47 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
09:25:02 Timing Pre_Polynomial_Factorization (2 threads, 26.803s elapsed time, 55.020s cpu time, 2.660s GC time, factor 2.05)
09:25:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization
09:25:02 Finished Pre_Polynomial_Factorization (0:01:12 elapsed time, 0:02:00 cpu time, factor 1.65)
09:25:02 Running Polynomial_Factorization ...
09:25:15 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset
09:25:15 Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial
09:25:15 Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility
09:25:15 Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
09:25:15 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial
09:25:16 Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots
09:25:16 Polynomial_Factorization: theory Polynomial_Factorization.Precomputation
09:25:16 Polynomial_Factorization: theory Polynomial_Factorization.Missing_List
09:25:17 Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly
09:25:17 Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization
09:25:18 Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma
09:25:18 Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization
09:25:19 Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly
09:25:20 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test
09:25:20 Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization
09:25:23 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization
09:26:05 Timing Polynomial_Factorization (2 threads, 45.872s elapsed time, 70.740s cpu time, 2.156s GC time, factor 1.54)
09:26:05 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization
09:26:05 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf
09:26:05 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf
09:26:05 Finished Polynomial_Factorization (0:01:02 elapsed time, 0:01:28 cpu time, factor 1.42)
09:30:38 Timing Jordan_Normal_Form (2 threads, 339.259s elapsed time, 572.796s cpu time, 18.372s GC time, factor 1.69)
09:30:38 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form
09:30:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/document.pdf
09:30:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/outline.pdf
09:30:38 Finished Jordan_Normal_Form (0:06:49 elapsed time, 0:11:15 cpu time, factor 1.65)
09:30:39 Building Pre_Perron_Frobenius ...
09:30:39 Building Subresultants ...
09:30:54 Subresultants: theory Subresultants.Coeff_Int
09:30:54 Subresultants: theory Subresultants.Dichotomous_Lazard
09:30:54 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.L2_Norm
09:30:54 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Polynomial_Divisibility
09:30:54 Subresultants: theory Subresultants.Missing_Polynomial_Factorial
09:30:54 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Norm_Arith
09:30:55 Subresultants: theory Subresultants.More_Homomorphisms
09:30:55 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Continuum_Not_Denumerable
09:30:55 Subresultants: theory Subresultants.Resultant_Prelim
09:30:55 Subresultants: theory Subresultants.Binary_Exponentiation
09:30:55 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Inner_Product
09:30:55 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Operator_Norm
09:30:55 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Summation_Tests
09:30:56 Subresultants: theory Subresultants.Subresultant
09:30:56 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Square_Free_Factorization
09:30:56 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Product_Vector
09:30:57 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Euclidean_Space
09:30:59 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Finite_Cartesian_Product
09:31:00 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Linear_Algebra
09:31:00 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Types_To_Sets
09:31:01 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Eisbach
09:31:01 Subresultants: theory Subresultants.Subresultant_Gcd
09:31:03 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Topology_Euclidean_Space
09:31:13 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Convex_Euclidean_Space
09:31:14 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Bounded_Linear_Function
09:31:15 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Uniform_Limit
09:31:19 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Continuous_Extension
09:31:20 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Path_Connected
09:31:24 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Homeomorphism
09:31:25 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Brouwer_Fixpoint
09:31:27 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Derivative
09:31:29 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Cartesian_Euclidean_Space
09:31:32 Pre_Perron_Frobenius: theory Pre_Perron_Frobenius.Determinants
09:31:53 Timing HOL-Analysis (2 threads, 759.491s elapsed time, 1291.152s cpu time, 104.684s GC time, factor 1.70)
09:31:53 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis
09:31:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis/document.pdf
09:31:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis/outline.pdf
09:31:53 Finished HOL-Analysis (0:14:36 elapsed time, 0:24:26 cpu time, factor 1.67)
09:31:54 Building HOL-Probability ...
09:31:54 Building Landau_Analysis ...
09:31:54 Building Echelon_Form ...
09:31:54 Building Ordinary_Differential_Equations ...
09:31:54 Running QR_Decomposition ...
09:31:54 Running Affine_Arithmetic ...
09:32:04 Landau_Analysis: theory Landau_Analysis.Group_Sort
09:32:04 Landau_Analysis: theory Landau_Analysis.Landau_Library
09:32:04 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Dense_Linear_Order
09:32:05 Echelon_Form: theory Echelon_Form.Dual_Order
09:32:05 Echelon_Form: theory Echelon_Form.Code_Bit
09:32:05 QR_Decomposition: theory QR_Decomposition.Code_Bit
09:32:05 QR_Decomposition: theory QR_Decomposition.Real_Impl_Auxiliary
09:32:05 Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
09:32:05 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
09:32:05 QR_Decomposition: theory QR_Decomposition.Code_Set
09:32:05 Landau_Analysis: theory Landau_Analysis.Landau_Symbols_Definition
09:32:05 Echelon_Form: theory Echelon_Form.IArray_Addenda
09:32:05 QR_Decomposition: theory QR_Decomposition.Code_Real_Approx_By_Float_Haskell
09:32:05 HOL-Probability: theory HOL-Probability.Fin_Map
09:32:05 HOL-Probability: theory HOL-Probability.Discrete_Topology
09:32:05 QR_Decomposition: theory QR_Decomposition.Generalizations
09:32:05 Echelon_Form: theory Echelon_Form.Code_Set
09:32:05 QR_Decomposition: theory QR_Decomposition.CauchysMeanTheorem
09:32:05 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
09:32:05 Echelon_Form: theory Echelon_Form.Mod_Type
09:32:05 Echelon_Form: theory Echelon_Form.Generalizations
09:32:05 HOL-Probability: theory HOL-Probability.Essential_Supremum
09:32:05 QR_Decomposition: theory QR_Decomposition.Sqrt_Babylonian_Auxiliary
09:32:06 HOL-Probability: theory HOL-Probability.Probability_Measure
09:32:06 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
09:32:06 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
09:32:06 QR_Decomposition: theory QR_Decomposition.Log_Impl
09:32:07 QR_Decomposition: theory QR_Decomposition.NthRoot_Impl
09:32:07 HOL-Probability: theory HOL-Probability.Stopping_Time
09:32:07 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Approximation
09:32:07 QR_Decomposition: theory QR_Decomposition.Derive_Manager
09:32:07 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
09:32:07 QR_Decomposition: theory QR_Decomposition.Dual_Order
09:32:08 Echelon_Form: theory Echelon_Form.Square_Matrix
09:32:08 QR_Decomposition: theory QR_Decomposition.Sqrt_Babylonian
09:32:08 QR_Decomposition: theory QR_Decomposition.Mod_Type
09:32:08 Affine_Arithmetic: theory Affine_Arithmetic.Polygon
09:32:08 HOL-Probability: theory HOL-Probability.Conditional_Expectation
09:32:08 Echelon_Form: theory Echelon_Form.Miscellaneous
09:32:08 HOL-Probability: theory HOL-Probability.Distribution_Functions
09:32:08 QR_Decomposition: theory QR_Decomposition.Prime_Product
09:32:08 Landau_Analysis: theory Landau_Analysis.Landau_Real_Products
09:32:08 Affine_Arithmetic: theory Affine_Arithmetic.Euclidean_Space_Explicit
09:32:08 Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
09:32:09 HOL-Probability: theory HOL-Probability.Weak_Convergence
09:32:09 HOL-Probability: theory HOL-Probability.Giry_Monad
09:32:09 HOL-Probability: theory HOL-Probability.Helly_Selection
09:32:09 QR_Decomposition: theory QR_Decomposition.Real_Impl
09:32:09 Echelon_Form: theory Echelon_Form.Cayley_Hamilton
09:32:10 Echelon_Form: theory Echelon_Form.Code_Matrix
09:32:10 Echelon_Form: theory Echelon_Form.Fundamental_Subspaces
09:32:11 QR_Decomposition: theory QR_Decomposition.Generator_Aux
09:32:11 Echelon_Form: theory Echelon_Form.Rref
09:32:11 QR_Decomposition: theory QR_Decomposition.Show
09:32:11 Echelon_Form: theory Echelon_Form.Dim_Formula
09:32:11 QR_Decomposition: theory QR_Decomposition.Miscellaneous
09:32:11 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
09:32:11 Echelon_Form: theory Echelon_Form.Rank
09:32:11 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
09:32:11 Echelon_Form: theory Echelon_Form.Elementary_Operations
09:32:11 HOL-Probability: theory HOL-Probability.Projective_Family
09:32:12 Landau_Analysis: theory Landau_Analysis.Landau_Simprocs
09:32:12 QR_Decomposition: theory QR_Decomposition.Show_Instances
09:32:12 Echelon_Form: theory Echelon_Form.Matrix_To_IArray
09:32:12 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
09:32:13 QR_Decomposition: theory QR_Decomposition.Code_Matrix
09:32:13 Landau_Analysis: theory Landau_Analysis.Asymptotic_Equivalence
09:32:13 Landau_Analysis: theory Landau_Analysis.Landau_More
09:32:13 Echelon_Form: theory Echelon_Form.Gauss_Jordan
09:32:13 QR_Decomposition: theory QR_Decomposition.Fundamental_Subspaces
09:32:13 QR_Decomposition: theory QR_Decomposition.Rref
09:32:13 Landau_Analysis: theory Landau_Analysis.Landau_Symbols
09:32:13 QR_Decomposition: theory QR_Decomposition.Dim_Formula
09:32:14 HOL-Probability: theory HOL-Probability.Independent_Family
09:32:14 QR_Decomposition: theory QR_Decomposition.Rank
09:32:14 HOL-Probability: theory HOL-Probability.PMF_Impl
09:32:14 QR_Decomposition: theory QR_Decomposition.Elementary_Operations
09:32:14 QR_Decomposition: theory QR_Decomposition.Show_Real
09:32:15 QR_Decomposition: theory QR_Decomposition.Real_Unique_Impl
09:32:15 Echelon_Form: theory Echelon_Form.Gauss_Jordan_IArrays
09:32:15 Echelon_Form: theory Echelon_Form.Linear_Maps
09:32:15 QR_Decomposition: theory QR_Decomposition.Gauss_Jordan
09:32:16 HOL-Probability: theory HOL-Probability.Random_Permutations
09:32:16 Echelon_Form: theory Echelon_Form.Gauss_Jordan_PA
09:32:17 HOL-Probability: theory HOL-Probability.SPMF
09:32:17 HOL-Probability: theory HOL-Probability.Convolution
09:32:18 Echelon_Form: theory Echelon_Form.Bases_Of_Fundamental_Subspaces
09:32:18 QR_Decomposition: theory QR_Decomposition.Linear_Maps
09:32:18 HOL-Probability: theory HOL-Probability.Information
09:32:18 Echelon_Form: theory Echelon_Form.Determinants2
09:32:18 Echelon_Form: theory Echelon_Form.Gauss_Jordan_PA_IArrays
09:32:19 Echelon_Form: theory Echelon_Form.Inverse
09:32:19 Echelon_Form: theory Echelon_Form.System_Of_Equations
09:32:19 Echelon_Form: theory Echelon_Form.Inverse_IArrays
09:32:19 QR_Decomposition: theory QR_Decomposition.Gauss_Jordan_PA
09:32:20 Echelon_Form: theory Echelon_Form.Examples_Gauss_Jordan_Abstract
09:32:20 QR_Decomposition: theory QR_Decomposition.Bases_Of_Fundamental_Subspaces
09:32:21 QR_Decomposition: theory QR_Decomposition.Determinants2
09:32:21 QR_Decomposition: theory QR_Decomposition.Inverse
09:32:21 QR_Decomposition: theory QR_Decomposition.System_Of_Equations
09:32:21 HOL-Probability: theory HOL-Probability.Distributions
09:32:22 HOL-Probability: theory HOL-Probability.Projective_Limit
09:32:22 QR_Decomposition: theory QR_Decomposition.Examples_Gauss_Jordan_Abstract
09:32:23 HOL-Probability: theory HOL-Probability.Characteristic_Functions
09:32:24 HOL-Probability: theory HOL-Probability.Sinc_Integral
09:32:24 HOL-Probability: theory HOL-Probability.Stream_Space
09:32:25 HOL-Probability: theory HOL-Probability.Levy
09:32:26 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
09:32:27 HOL-Probability: theory Probability
09:32:29 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
09:32:29 Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
09:32:32 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
09:32:33 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
09:32:37 Affine_Arithmetic: theory Affine_Arithmetic.Intersection
09:32:42 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
09:32:54 Timing Subresultants (2 threads, 73.511s elapsed time, 117.404s cpu time, 2.800s GC time, factor 1.60)
09:32:54 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants
09:32:54 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/document.pdf
09:32:54 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/outline.pdf
09:32:54 Finished Subresultants (0:02:14 elapsed time, 0:03:23 cpu time, factor 1.51)
09:32:54 Building Pre_BZ ...
09:32:59 Timing Landau_Analysis (2 threads, 14.998s elapsed time, 28.688s cpu time, 1.468s GC time, factor 1.91)
09:32:59 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Landau_Analysis
09:32:59 Finished Landau_Analysis (0:01:04 elapsed time, 0:01:40 cpu time, factor 1.56)
09:32:59 Building Stirling_Formula ...
09:33:04 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
09:33:04 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
09:33:10 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
09:33:10 Pre_BZ: theory Pre_BZ.Totient
09:33:10 Pre_BZ: theory Pre_BZ.Cong
09:33:10 Pre_BZ: theory Pre_BZ.Efficient_Sort
09:33:10 Stirling_Formula: theory Stirling_Formula.Bernoulli
09:33:10 Stirling_Formula: theory Stirling_Formula.Stirling_Formula
09:33:11 Stirling_Formula: theory Stirling_Formula.Bernoulli_FPS
09:33:11 Pre_BZ: theory Pre_BZ.Missing_Multiset
09:33:11 Pre_BZ: theory Pre_BZ.Improved_Code_Equations
09:33:11 Pre_BZ: theory Pre_BZ.Neville_Aitken_Interpolation
09:33:12 Stirling_Formula: theory Stirling_Formula.Periodic_Bernpoly
09:33:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
09:33:12 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
09:33:13 Pre_BZ: theory Pre_BZ.Residues
09:33:13 Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics
09:33:13 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
09:33:13 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
09:33:17 Pre_BZ: theory Pre_BZ.Lagrange_Interpolation
09:33:18 Pre_BZ: theory Pre_BZ.Polynomial_Divisibility
09:33:18 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
09:33:18 Pre_BZ: theory Pre_BZ.CauchysMeanTheorem
09:33:18 Pre_BZ: theory Pre_BZ.Sqrt_Babylonian_Auxiliary
09:33:18 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
09:33:19 Pre_BZ: theory Pre_BZ.Precomputation
09:33:19 Pre_BZ: theory Pre_BZ.Show_Poly
09:33:19 Pre_BZ: theory Pre_BZ.Is_Rat_To_Rat
09:33:19 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
09:33:20 Pre_BZ: theory Pre_BZ.Log_Impl
09:33:20 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
09:33:20 Pre_BZ: theory Pre_BZ.NthRoot_Impl
09:33:20 Pre_BZ: theory Pre_BZ.Missing_List
09:33:21 Pre_BZ: theory Pre_BZ.Prime_Factorization
09:33:22 Pre_BZ: theory Pre_BZ.Sqrt_Babylonian
09:33:22 Pre_BZ: theory Pre_BZ.Explicit_Roots
09:33:22 Pre_BZ: theory Pre_BZ.Gauss_Lemma
09:33:23 Pre_BZ: theory Pre_BZ.Square_Free_Factorization
09:33:24 Pre_BZ: theory Pre_BZ.Gcd_Rat_Poly
09:33:24 Pre_BZ: theory Pre_BZ.Rational_Root_Test
09:33:25 Pre_BZ: theory Pre_BZ.Bits
09:33:25 Pre_BZ: theory Pre_BZ.Bits_Bit
09:33:25 Pre_BZ: theory Pre_BZ.Divmod_Int
09:33:26 Pre_BZ: theory Pre_BZ.Dvd_Int_Poly
09:33:27 Pre_BZ: theory Pre_BZ.Newton_Interpolation
09:33:27 Pre_BZ: theory Pre_BZ.Misc_Numeric
09:33:27 Pre_BZ: theory Pre_BZ.Bit_Representation
09:33:28 Pre_BZ: theory Pre_BZ.Bits_Int
09:33:29 Pre_BZ: theory Pre_BZ.Bool_List_Representation
09:33:31 Pre_BZ: theory Pre_BZ.More_Bits_Int
09:33:31 Pre_BZ: theory Pre_BZ.Polynomial_Interpolation
09:33:33 Pre_BZ: theory Pre_BZ.Bits_Integer
09:33:34 Pre_BZ: theory Pre_BZ.Kronecker_Factorization
09:33:37 Pre_BZ: theory Pre_BZ.Rational_Factorization
09:33:41 Pre_BZ: theory Pre_BZ.Word_Miscellaneous
09:33:41 Pre_BZ: theory Pre_BZ.Misc_Typedef
09:33:42 Pre_BZ: theory Pre_BZ.Word
09:33:45 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
09:33:46 Pre_BZ: theory Pre_BZ.Code_Target_Bits_Int
09:33:46 Pre_BZ: theory Pre_BZ.Types_To_Sets
09:33:49 Pre_BZ: theory Pre_BZ.Word_Misc
09:33:50 Pre_BZ: theory Pre_BZ.Uint32
09:33:52 Echelon_Form: theory Echelon_Form.Rings2
09:34:08 Timing Stirling_Formula (2 threads, 17.627s elapsed time, 34.128s cpu time, 1.144s GC time, factor 1.94)
09:34:08 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula
09:34:08 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/document.pdf
09:34:08 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/outline.pdf
09:34:08 Finished Stirling_Formula (0:01:08 elapsed time, 0:01:45 cpu time, factor 1.53)
09:34:08 Running Gauss_Jordan ...
09:34:19 Gauss_Jordan: theory Gauss_Jordan.Dual_Order
09:34:19 Gauss_Jordan: theory Gauss_Jordan.Generalizations
09:34:19 Gauss_Jordan: theory Gauss_Jordan.Mod_Type
09:34:22 Gauss_Jordan: theory Gauss_Jordan.Miscellaneous
09:34:24 Gauss_Jordan: theory Gauss_Jordan.Fundamental_Subspaces
09:34:25 Gauss_Jordan: theory Gauss_Jordan.Dim_Formula
09:34:28 Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
09:34:30 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
09:34:31 Echelon_Form: theory Echelon_Form.Echelon_Form
09:34:33 Echelon_Form: theory Echelon_Form.Echelon_Form_Det
09:34:34 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
09:34:34 Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
09:34:35 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
09:34:36 Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
09:34:36 QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR
09:34:36 QR_Decomposition: theory QR_Decomposition.Generalizations2
09:34:36 QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR
09:34:37 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
09:34:37 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
09:34:38 QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR
09:34:38 QR_Decomposition: theory QR_Decomposition.Projections
09:34:39 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
09:34:39 QR_Decomposition: theory QR_Decomposition.Gram_Schmidt
09:34:40 QR_Decomposition: theory QR_Decomposition.QR_Decomposition
09:34:40 QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float
09:34:40 QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays
09:34:41 QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays
09:34:41 QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float
09:34:44 QR_Decomposition: theory QR_Decomposition.QR_Efficient
09:34:45 QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation
09:34:45 QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic
09:34:45 Gauss_Jordan: theory Gauss_Jordan.Code_Bit
09:34:45 Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda
09:34:45 Gauss_Jordan: theory Gauss_Jordan.Code_Set
09:34:46 Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
09:34:46 Gauss_Jordan: theory Gauss_Jordan.IArray_Haskell
09:34:46 Gauss_Jordan: theory Gauss_Jordan.Code_Matrix
09:34:46 Gauss_Jordan: theory Gauss_Jordan.Rank
09:34:46 Gauss_Jordan: theory Gauss_Jordan.Rref
09:34:46 Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations
09:34:47 Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray
09:34:47 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan
09:34:50 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays
09:34:50 Gauss_Jordan: theory Gauss_Jordan.Linear_Maps
09:34:51 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA
09:34:52 Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
09:34:52 Gauss_Jordan: theory Gauss_Jordan.Determinants2
09:34:53 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
09:34:53 Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays
09:34:53 Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays
09:34:54 Gauss_Jordan: theory Gauss_Jordan.Inverse
09:34:54 Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations
09:34:54 Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays
09:34:55 Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
09:34:55 Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays
09:34:56 Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays
09:34:56 QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic
09:34:59 Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays
09:35:01 Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML
09:35:01 Gauss_Jordan: theory Gauss_Jordan.Code_Rational
09:35:03 Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell
09:35:46 Timing HOL-Probability (2 threads, 157.908s elapsed time, 293.872s cpu time, 10.120s GC time, factor 1.86)
09:35:46 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability
09:35:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability/document.pdf
09:35:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability/outline.pdf
09:35:46 Finished HOL-Probability (0:03:51 elapsed time, 0:06:42 cpu time, factor 1.74)
09:35:46 Building Deep_Learning_Lib ...
09:35:59 Deep_Learning_Lib: theory Deep_Learning_Lib.Congruence
09:35:59 Deep_Learning_Lib: theory Deep_Learning_Lib.FunctionLemmas
09:35:59 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Unsorted
09:36:00 Deep_Learning_Lib: theory Deep_Learning_Lib.Order
09:36:01 Deep_Learning_Lib: theory Deep_Learning_Lib.Ring_Hom
09:36:02 Deep_Learning_Lib: theory Deep_Learning_Lib.Lattice
09:36:03 Deep_Learning_Lib: theory Deep_Learning_Lib.Complete_Lattice
09:36:05 Deep_Learning_Lib: theory Deep_Learning_Lib.Group
09:36:06 Deep_Learning_Lib: theory Deep_Learning_Lib.Coset
09:36:08 Deep_Learning_Lib: theory Deep_Learning_Lib.FiniteProduct
09:36:09 Deep_Learning_Lib: theory Deep_Learning_Lib.Ring
09:36:13 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Ring
09:36:13 Deep_Learning_Lib: theory Deep_Learning_Lib.Module
09:36:16 Deep_Learning_Lib: theory Deep_Learning_Lib.RingModuleFacts
09:36:17 Deep_Learning_Lib: theory Deep_Learning_Lib.MonoidSums
09:36:18 Deep_Learning_Lib: theory Deep_Learning_Lib.LinearCombinations
09:36:18 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_Permutations
09:36:19 Timing Affine_Arithmetic (2 threads, 248.982s elapsed time, 481.468s cpu time, 23.428s GC time, factor 1.93)
09:36:19 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic
09:36:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic/document.pdf
09:36:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic/outline.pdf
09:36:19 Finished Affine_Arithmetic (0:04:24 elapsed time, 0:08:19 cpu time, factor 1.89)
09:36:19 Deep_Learning_Lib: theory Deep_Learning_Lib.Matrix
09:36:19 Building Applicative_Lifting ...
09:36:24 Deep_Learning_Lib: theory Deep_Learning_Lib.Gauss_Jordan_Elimination
09:36:26 Deep_Learning_Lib: theory Deep_Learning_Lib.Column_Operations
09:36:27 Deep_Learning_Lib: theory Deep_Learning_Lib.Determinant
09:36:30 Deep_Learning_Lib: theory Deep_Learning_Lib.SumSpaces
09:36:31 Deep_Learning_Lib: theory Deep_Learning_Lib.VectorSpace
09:36:31 Applicative_Lifting: theory Applicative_Lifting.Commutation
09:36:31 Applicative_Lifting: theory Applicative_Lifting.Lambda
09:36:32 Applicative_Lifting: theory Applicative_Lifting.Free_Ultrafilter
09:36:32 Applicative_Lifting: theory Applicative_Lifting.StarDef
09:36:32 Timing Pre_BZ (2 threads, 137.816s elapsed time, 231.812s cpu time, 9.864s GC time, factor 1.68)
09:36:32 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_BZ
09:36:32 Finished Pre_BZ (0:03:38 elapsed time, 0:06:24 cpu time, factor 1.76)
09:36:32 Applicative_Lifting: theory Applicative_Lifting.ParRed
09:36:33 Building Berlekamp_Zassenhaus ...
09:36:33 Applicative_Lifting: theory Applicative_Lifting.Eta
09:36:36 Timing Pre_Perron_Frobenius (2 threads, 285.544s elapsed time, 498.964s cpu time, 20.488s GC time, factor 1.75)
09:36:36 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Perron_Frobenius
09:36:36 Finished Pre_Perron_Frobenius (0:05:56 elapsed time, 0:10:02 cpu time, factor 1.69)
09:36:36 Building Quick_Sort_Cost ...
09:36:40 Applicative_Lifting: theory Applicative_Lifting.Applicative
09:36:40 Applicative_Lifting: theory Applicative_Lifting.Joinable
09:36:40 Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
09:36:40 Applicative_Lifting: theory Applicative_Lifting.Combinators
09:36:40 Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
09:36:41 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment
09:36:41 Applicative_Lifting: theory Applicative_Lifting.Applicative_List
09:36:41 Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid
09:36:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_Option
09:36:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_Set
09:36:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_State
09:36:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
09:36:43 Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
09:36:44 Deep_Learning_Lib: theory Deep_Learning_Lib.Missing_VectorSpace
09:36:44 Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
09:36:44 Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
09:36:44 Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
09:36:45 Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List
09:36:45 Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra
09:36:45 Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
09:36:45 Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
09:36:46 Deep_Learning_Lib: theory Deep_Learning_Lib.VS_Connect
09:36:48 Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
09:36:48 Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
09:36:49 Quick_Sort_Cost: theory Quick_Sort_Cost.Group_Sort
09:36:49 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Library
09:36:49 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Symbols_Definition
09:36:50 Quick_Sort_Cost: theory Quick_Sort_Cost.List_Index
09:36:51 Quick_Sort_Cost: theory Quick_Sort_Cost.Linorder_Relations
09:36:52 Quick_Sort_Cost: theory Quick_Sort_Cost.Regular_Set
09:36:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
09:36:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
09:36:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
09:36:53 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Real_Products
09:36:54 Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
09:36:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
09:36:57 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Simprocs
09:36:57 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
09:36:57 Quick_Sort_Cost: theory Quick_Sort_Cost.Asymptotic_Equivalence
09:36:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
09:36:58 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_More
09:36:58 Quick_Sort_Cost: theory Quick_Sort_Cost.Landau_Symbols
09:36:58 Timing Gauss_Jordan (2 threads, 152.486s elapsed time, 282.884s cpu time, 9.104s GC time, factor 1.86)
09:36:58 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gauss_Jordan
09:36:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gauss_Jordan/document.pdf
09:36:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gauss_Jordan/outline.pdf
09:36:58 Finished Gauss_Jordan (0:02:49 elapsed time, 0:05:03 cpu time, factor 1.79)
09:36:58 Building Randomised_Social_Choice ...
09:36:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
09:37:01 Timing Ordinary_Differential_Equations (2 threads, 229.953s elapsed time, 376.372s cpu time, 11.504s GC time, factor 1.64)
09:37:01 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ordinary_Differential_Equations
09:37:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ordinary_Differential_Equations/document.pdf
09:37:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf
09:37:01 Finished Ordinary_Differential_Equations (0:05:06 elapsed time, 0:08:11 cpu time, factor 1.60)
09:37:01 Building HOL-ODE ...
09:37:02 Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
09:37:03 Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
09:37:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
09:37:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
09:37:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
09:37:09 Timing QR_Decomposition (2 threads, 300.890s elapsed time, 567.732s cpu time, 19.388s GC time, factor 1.89)
09:37:09 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/QR_Decomposition
09:37:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/QR_Decomposition/document.pdf
09:37:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/QR_Decomposition/outline.pdf
09:37:09 Finished QR_Decomposition (0:05:14 elapsed time, 0:09:43 cpu time, factor 1.85)
09:37:10 Running Probabilistic_Noninterference ...
09:37:10 Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
09:37:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
09:37:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
09:37:11 Randomised_Social_Choice: theory Randomised_Social_Choice.List_Index
09:37:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
09:37:12 Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
09:37:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
09:37:14 Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries
09:37:14 Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact
09:37:14 Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
09:37:14 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
09:37:15 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
09:37:16 Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
09:37:16 Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
09:37:16 Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
09:37:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
09:37:17 Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
09:37:18 Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
09:37:19 Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
09:37:19 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
09:37:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
09:37:21 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
09:37:21 Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
09:37:22 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_Nat
09:37:22 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
09:37:23 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_List
09:37:24 Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
09:37:25 Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
09:37:25 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
09:37:25 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
09:37:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
09:37:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
09:37:30 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
09:37:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
09:37:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
09:37:31 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Coinductive_Stream
09:37:32 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Markov_Models_Auxiliary
09:37:35 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
09:37:35 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Discrete_Time_Markov_Chain
09:37:36 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
09:37:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
09:37:37 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
09:37:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
09:37:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
09:37:44 Timing HOL-ODE (2 threads, 0.162s elapsed time, 0.164s cpu time, 0.000s GC time, factor 1.01)
09:37:44 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE
09:37:44 Finished HOL-ODE (0:00:42 elapsed time, 0:00:58 cpu time, factor 1.37)
09:37:44 Building HOL-ODE-Refinement ...
09:37:48 Timing Applicative_Lifting (2 threads, 32.794s elapsed time, 59.224s cpu time, 3.644s GC time, factor 1.81)
09:37:48 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Applicative_Lifting
09:37:48 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Applicative_Lifting/document.pdf
09:37:48 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Applicative_Lifting/outline.pdf
09:37:48 Finished Applicative_Lifting (0:01:28 elapsed time, 0:02:20 cpu time, factor 1.58)
09:37:48 Running Differential_Dynamic_Logic ...
09:37:56 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
09:37:56 Timing Quick_Sort_Cost (2 threads, 26.844s elapsed time, 48.168s cpu time, 2.432s GC time, factor 1.79)
09:37:56 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Quick_Sort_Cost
09:37:56 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Quick_Sort_Cost/document.pdf
09:37:56 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Quick_Sort_Cost/outline.pdf
09:37:56 Finished Quick_Sort_Cost (0:01:19 elapsed time, 0:02:07 cpu time, factor 1.61)
09:37:56 Running Markov_Models ...
09:37:58 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Quicksort
09:37:58 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bits
09:37:58 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bits_Bit
09:37:59 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Foldi
09:37:59 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Misc
09:37:59 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Misc_Numeric
09:37:59 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bit_Representation
09:38:00 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bits_Int
09:38:01 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bool_List_Representation
09:38:01 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
09:38:01 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
09:38:02 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
09:38:02 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
09:38:03 HOL-ODE-Refinement: theory HOL-ODE-Refinement.More_Bits_Int
09:38:05 HOL-ODE-Refinement: theory HOL-ODE-Refinement.SetIterator
09:38:05 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Bits_Integer
09:38:05 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
09:38:07 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Word_Miscellaneous
09:38:07 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Misc_Typedef
09:38:08 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Word
09:38:08 Markov_Models: theory Markov_Models.Coinductive_Nat
09:38:08 Markov_Models: theory Markov_Models.Gauss_Jordan_Elim_Fun
09:38:09 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
09:38:10 Markov_Models: theory Markov_Models.Coinductive_List
09:38:10 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
09:38:13 Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
09:38:15 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Word_Misc
09:38:16 Timing Randomised_Social_Choice (2 threads, 23.382s elapsed time, 45.728s cpu time, 2.404s GC time, factor 1.96)
09:38:16 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Randomised_Social_Choice
09:38:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Randomised_Social_Choice/document.pdf
09:38:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Randomised_Social_Choice/outline.pdf
09:38:16 Finished Randomised_Social_Choice (0:01:16 elapsed time, 0:01:58 cpu time, factor 1.54)
09:38:16 Running E_Transcendental ...
09:38:16 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Prio_List
09:38:16 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Chapter
09:38:17 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Util
09:38:17 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
09:38:17 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Anti_Unification
09:38:17 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Attr_Comb
09:38:17 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Named_Sorted_Thms
09:38:18 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Data
09:38:18 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Digraph_Basic
09:38:19 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Mk_Term_Antiquot
09:38:19 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Mpat_Antiquot
09:38:19 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Code_Target_Bits_Int
09:38:19 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Uint
09:38:20 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Code_Target_ICF
09:38:20 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Uint32
09:38:21 Markov_Models: theory Markov_Models.Coinductive_List_Prefix
09:38:21 Markov_Models: theory Markov_Models.Coinductive_Stream
09:38:21 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Indep_Vars
09:38:21 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Mk_Record_Simp
09:38:21 Markov_Models: theory Markov_Models.Quotient_Coinductive_List
09:38:21 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Tagged_Solver
09:38:22 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Select_Solve
09:38:22 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Lib
09:38:22 HOL-ODE-Refinement: theory HOL-ODE-Refinement.HashCode
09:38:22 Markov_Models: theory Markov_Models.TLList
09:38:22 HOL-ODE-Refinement: theory HOL-ODE-Refinement.SetIteratorOperations
09:38:23 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
09:38:23 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Phases
09:38:23 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Tagging
09:38:23 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Mono_Prover
09:38:24 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Relators
09:38:24 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Param_Tool
09:38:25 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Param_HOL
09:38:25 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Assoc_List
09:38:26 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
09:38:26 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Proper_Iterator
09:38:26 Markov_Models: theory Markov_Models.Quotient_TLList
09:38:26 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Parametricity
09:38:27 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Id_Ops
09:38:27 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
09:38:27 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Diff_Array
09:38:27 E_Transcendental: theory E_Transcendental.Cong
09:38:27 E_Transcendental: theory E_Transcendental.Eratosthenes
09:38:27 Markov_Models: theory Markov_Models.Coinductive
09:38:28 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Fix_Rel
09:38:28 E_Transcendental: theory E_Transcendental.Totient
09:38:28 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
09:38:28 E_Transcendental: theory E_Transcendental.Congruence
09:38:28 E_Transcendental: theory E_Transcendental.Fib
09:38:28 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Translate
09:38:28 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Gen_Algo
09:38:29 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Relator_Interface
09:38:29 HOL-ODE-Refinement: theory HOL-ODE-Refinement.It_to_It
09:38:29 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Tool
09:38:29 HOL-ODE-Refinement: theory HOL-ODE-Refinement.SetIteratorGA
09:38:29 E_Transcendental: theory E_Transcendental.Order
09:38:30 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Bindings_HOL
09:38:31 E_Transcendental: theory E_Transcendental.Lattice
09:38:32 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
09:38:33 E_Transcendental: theory E_Transcendental.Complete_Lattice
09:38:33 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
09:38:33 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
09:38:34 E_Transcendental: theory E_Transcendental.Group
09:38:35 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Automatic_Refinement
09:38:35 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Idx_Iterator
09:38:35 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
09:38:35 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Intf_Comp
09:38:37 E_Transcendental: theory E_Transcendental.Coset
09:38:37 E_Transcendental: theory E_Transcendental.FiniteProduct
09:38:38 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Intf_Hash
09:38:38 E_Transcendental: theory E_Transcendental.Ring
09:38:39 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Gen_Hash
09:38:39 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Misc
09:38:40 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RefineG_Domain
09:38:41 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RefineG_Transfer
09:38:41 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RefineG_Assert
09:38:41 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RefineG_Recursion
09:38:42 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RefineG_While
09:38:43 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Det
09:38:44 E_Transcendental: theory E_Transcendental.AbelCoset
09:38:44 E_Transcendental: theory E_Transcendental.Module
09:38:46 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Basic
09:38:47 E_Transcendental: theory E_Transcendental.More_Group
09:38:48 E_Transcendental: theory E_Transcendental.More_Finite_Product
09:38:48 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
09:38:48 E_Transcendental: theory E_Transcendental.More_Ring
09:38:50 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
09:38:50 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Heuristics
09:38:51 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Leof
09:38:51 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Pfun
09:38:51 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_While
09:38:53 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Transfer
09:38:53 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
09:38:54 E_Transcendental: theory E_Transcendental.Ideal
09:38:54 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Monadic
09:38:54 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Automation
09:38:54 Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
09:38:54 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Foreach
09:38:57 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Monadic
09:38:58 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
09:38:58 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
09:38:58 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Intf_Map
09:38:59 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Intf_Set
09:39:00 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Cfun_Set
09:39:00 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Array_Stack
09:39:00 E_Transcendental: theory E_Transcendental.RingHom
09:39:00 Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
09:39:00 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Gen_Iterator
09:39:01 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Iterator
09:39:02 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Array_Iterator
09:39:02 Markov_Models: theory Markov_Models.Crowds_Protocol
09:39:02 E_Transcendental: theory E_Transcendental.UnivPoly
09:39:02 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Gen_Map
09:39:03 Markov_Models: theory Markov_Models.Example_A
09:39:03 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Gen_Map2Set
09:39:04 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Gen_Set
09:39:05 Markov_Models: theory Markov_Models.Example_B
09:39:05 Markov_Models: theory Markov_Models.Gossip_Broadcast
09:39:05 Markov_Models: theory Markov_Models.Markov_Decision_Process
09:39:06 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Array_Map
09:39:07 Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
09:39:07 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Bit_Set
09:39:07 Markov_Models: theory Markov_Models.Zeroconf_Analysis
09:39:09 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_List_Map
09:39:09 Markov_Models: theory Markov_Models.MDP_Reachability_Problem
09:39:10 Markov_Models: theory Markov_Models.PGCL
09:39:10 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Array_Hash_Map
09:39:11 Markov_Models: theory Markov_Models.MDP_RP_Certification
09:39:14 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_List_Set
09:39:14 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_Uv_Set
09:39:14 Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
09:39:16 HOL-ODE-Refinement: theory HOL-ODE-Refinement.RBT_add
09:39:16 Markov_Models: theory Markov_Models.Markov_Models
09:39:17 Markov_Models: theory Markov_Models.PCTL
09:39:17 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Impl_RBT_Map
09:39:19 E_Transcendental: theory E_Transcendental.Multiplicative_Group
09:39:23 E_Transcendental: theory E_Transcendental.Residues
09:39:23 Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
09:39:28 E_Transcendental: theory E_Transcendental.Euler_Criterion
09:39:28 E_Transcendental: theory E_Transcendental.Gauss
09:39:28 E_Transcendental: theory E_Transcendental.Quadratic_Reciprocity
09:39:29 E_Transcendental: theory E_Transcendental.Pocklington
09:39:30 E_Transcendental: theory E_Transcendental.Number_Theory
09:39:30 HOL-ODE-Refinement: theory HOL-ODE-Refinement.GenCF_No_Comp
09:39:35 Timing Deep_Learning_Lib (2 threads, 152.950s elapsed time, 292.184s cpu time, 12.928s GC time, factor 1.91)
09:39:35 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deep_Learning_Lib
09:39:35 Finished Deep_Learning_Lib (0:03:48 elapsed time, 0:06:40 cpu time, factor 1.75)
09:39:36 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Dflt_No_Comp
09:39:36 Running Deep_Learning ...
09:39:51 Deep_Learning: theory Deep_Learning.DL_Missing_List
09:39:51 Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
09:39:51 Deep_Learning: theory Deep_Learning.DL_Missing_Sublist
09:39:51 Timing Echelon_Form (2 threads, 415.521s elapsed time, 735.032s cpu time, 48.212s GC time, factor 1.77)
09:39:51 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Echelon_Form
09:39:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Echelon_Form/document.pdf
09:39:51 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Echelon_Form/outline.pdf
09:39:51 Finished Echelon_Form (0:07:56 elapsed time, 0:13:43 cpu time, factor 1.73)
09:39:51 Deep_Learning: theory Deep_Learning.PP_More_List2
09:39:52 Deep_Learning: theory Deep_Learning.Tensor
09:39:52 Deep_Learning: theory Deep_Learning.DL_Missing_Vector_Space
09:39:52 Running List_Update ...
09:39:52 Deep_Learning: theory Deep_Learning.Tensor_Subtensor
09:39:52 Deep_Learning: theory Deep_Learning.Tensor_Plus
09:39:52 Deep_Learning: theory Deep_Learning.PP_Poly_Mapping
09:39:53 Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
09:39:53 Deep_Learning: theory Deep_Learning.Tensor_Product
09:39:53 Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
09:39:53 Deep_Learning: theory Deep_Learning.Tensor_Rank
09:39:54 Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
09:39:54 Deep_Learning: theory Deep_Learning.DL_Missing_Matrix
09:39:54 Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
09:39:54 Deep_Learning: theory Deep_Learning.PP_MPoly
09:39:54 Deep_Learning: theory Deep_Learning.DL_Network
09:39:55 Deep_Learning: theory Deep_Learning.PP_More_MPoly
09:39:55 Deep_Learning: theory Deep_Learning.PP_Univariate
09:39:56 Deep_Learning: theory Deep_Learning.DL_Submatrix
09:39:57 Deep_Learning: theory Deep_Learning.Tensor_Matricization
09:39:59 Deep_Learning: theory Deep_Learning.DL_Shallow_Model
09:39:59 Deep_Learning: theory Deep_Learning.DL_Missing_VS_Connect
09:39:59 Deep_Learning: theory Deep_Learning.DL_Deep_Model
09:40:00 Deep_Learning: theory Deep_Learning.DL_Rank
09:40:03 Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
09:40:04 List_Update: theory List_Update.List_Index
09:40:04 List_Update: theory List_Update.Regular_Set
09:40:04 Deep_Learning: theory Deep_Learning.Lebesgue_Functional
09:40:04 Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
09:40:05 Timing Probabilistic_Noninterference (2 threads, 158.756s elapsed time, 301.740s cpu time, 9.092s GC time, factor 1.90)
09:40:05 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_Noninterference
09:40:05 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_Noninterference/document.pdf
09:40:05 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_Noninterference/outline.pdf
09:40:05 Finished Probabilistic_Noninterference (0:02:54 elapsed time, 0:05:22 cpu time, factor 1.85)
09:40:05 Running Prime_Harmonic_Series ...
09:40:06 List_Update: theory List_Update.Regular_Exp
09:40:10 List_Update: theory List_Update.NDerivative
09:40:13 Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
09:40:14 List_Update: theory List_Update.Equivalence_Checking
09:40:15 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Totient
09:40:15 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Cong
09:40:16 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Fib
09:40:16 List_Update: theory List_Update.Bit_Strings
09:40:16 List_Update: theory List_Update.Prob_Theory
09:40:16 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Congruence
09:40:16 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Eratosthenes
09:40:16 Deep_Learning: theory Deep_Learning.DL_Rank_Submatrix
09:40:16 List_Update: theory List_Update.On_Off
09:40:17 List_Update: theory List_Update.Inversion
09:40:17 List_Update: theory List_Update.Swaps
09:40:17 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Order
09:40:17 List_Update: theory List_Update.RExp_Var
09:40:18 List_Update: theory List_Update.Competitive_Analysis
09:40:18 Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
09:40:19 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Lattice
09:40:19 List_Update: theory List_Update.Move_to_Front
09:40:20 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Complete_Lattice
09:40:21 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Group
09:40:23 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Coset
09:40:23 Prime_Harmonic_Series: theory Prime_Harmonic_Series.FiniteProduct
09:40:24 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Ring
09:40:24 E_Transcendental: theory E_Transcendental.E_Transcendental
09:40:24 List_Update: theory List_Update.MTF2_Effects
09:40:25 List_Update: theory List_Update.BIT
09:40:25 List_Update: theory List_Update.Partial_Cost_Model
09:40:26 List_Update: theory List_Update.List_Factoring
09:40:28 Prime_Harmonic_Series: theory Prime_Harmonic_Series.AbelCoset
09:40:29 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Module
09:40:29 List_Update: theory List_Update.OPT2
09:40:29 List_Update: theory List_Update.BIT_pairwise
09:40:30 Markov_Models: theory Markov_Models.MDP_RP
09:40:31 Timing E_Transcendental (2 threads, 121.610s elapsed time, 236.792s cpu time, 11.504s GC time, factor 1.95)
09:40:31 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/E_Transcendental
09:40:31 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/E_Transcendental/document.pdf
09:40:31 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/E_Transcendental/outline.pdf
09:40:31 Finished E_Transcendental (0:02:14 elapsed time, 0:04:10 cpu time, factor 1.86)
09:40:31 Running Ergodic_Theory ...
09:40:31 List_Update: theory List_Update.Phase_Partitioning
09:40:32 Prime_Harmonic_Series: theory Prime_Harmonic_Series.More_Group
09:40:32 Prime_Harmonic_Series: theory Prime_Harmonic_Series.More_Finite_Product
09:40:32 List_Update: theory List_Update.BIT_2comp_on2
09:40:32 Prime_Harmonic_Series: theory Prime_Harmonic_Series.More_Ring
09:40:35 List_Update: theory List_Update.TS
09:40:37 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Ideal
09:40:37 List_Update: theory List_Update.Comb
09:40:42 Prime_Harmonic_Series: theory Prime_Harmonic_Series.RingHom
09:40:42 Timing Markov_Models (2 threads, 146.720s elapsed time, 267.116s cpu time, 12.600s GC time, factor 1.82)
09:40:42 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Markov_Models
09:40:42 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Markov_Models/document.pdf
09:40:42 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Markov_Models/outline.pdf
09:40:42 Finished Markov_Models (0:02:46 elapsed time, 0:04:58 cpu time, factor 1.80)
09:40:43 Running Density_Compiler ...
09:40:43 Ergodic_Theory: theory Ergodic_Theory.Fekete
09:40:43 Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement
09:40:44 Prime_Harmonic_Series: theory Prime_Harmonic_Series.UnivPoly
09:40:44 Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
09:40:44 Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density
09:40:45 Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
09:40:46 Timing Berlekamp_Zassenhaus (2 threads, 155.624s elapsed time, 302.068s cpu time, 13.532s GC time, factor 1.94)
09:40:46 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus
09:40:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/document.pdf
09:40:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/outline.pdf
09:40:46 Finished Berlekamp_Zassenhaus (0:04:13 elapsed time, 0:07:23 cpu time, factor 1.75)
09:40:47 Building Pre_Algebraic_Numbers ...
09:40:47 Ergodic_Theory: theory Ergodic_Theory.Recurrence
09:40:49 Ergodic_Theory: theory Ergodic_Theory.Invariants
09:40:50 Ergodic_Theory: theory Ergodic_Theory.Ergodicity
09:40:52 Ergodic_Theory: theory Ergodic_Theory.Kingman
09:40:54 Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
09:40:55 Density_Compiler: theory Density_Compiler.Density_Predicates
09:40:56 Density_Compiler: theory Density_Compiler.PDF_Transformations
09:40:56 Density_Compiler: theory Density_Compiler.PDF_Values
09:41:00 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Multiplicative_Group
09:41:01 Density_Compiler: theory Density_Compiler.PDF_Semantics
09:41:04 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Residues
09:41:08 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Euler_Criterion
09:41:08 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Gauss
09:41:09 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Quadratic_Reciprocity
09:41:09 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Pocklington
09:41:10 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Compare_Rat
09:41:10 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Misc_Polynomial
09:41:10 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Number_Theory
09:41:10 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Compare_Real
09:41:10 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Sturm_Library
09:41:11 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Show_Real
09:41:11 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Sturm_Theorem
09:41:11 Pre_Algebraic_Numbers: theory Pre_Algebraic_Numbers.Show_Complex
09:41:12 Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
09:41:12 Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
09:41:13 Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
09:41:17 Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
09:41:18 Density_Compiler: theory Density_Compiler.PDF_Compiler
09:42:08 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc
09:42:08 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat
09:42:08 Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic
09:42:09 Timing Deep_Learning (2 threads, 132.167s elapsed time, 251.832s cpu time, 7.384s GC time, factor 1.91)
09:42:09 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deep_Learning
09:42:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deep_Learning/document.pdf
09:42:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Deep_Learning/outline.pdf
09:42:09 Finished Deep_Learning (0:02:32 elapsed time, 0:04:34 cpu time, factor 1.80)
09:42:09 Running Akra_Bazzi ...
09:42:11 Timing Pre_Algebraic_Numbers (2 threads, 16.254s elapsed time, 31.444s cpu time, 0.620s GC time, factor 1.93)
09:42:11 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Algebraic_Numbers
09:42:11 Finished Pre_Algebraic_Numbers (0:01:23 elapsed time, 0:02:03 cpu time, factor 1.47)
09:42:11 Running Algebraic_Numbers ...
09:42:13 Timing Prime_Harmonic_Series (2 threads, 115.518s elapsed time, 227.708s cpu time, 10.972s GC time, factor 1.97)
09:42:13 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prime_Harmonic_Series
09:42:13 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prime_Harmonic_Series/document.pdf
09:42:13 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prime_Harmonic_Series/outline.pdf
09:42:13 Finished Prime_Harmonic_Series (0:02:07 elapsed time, 0:04:00 cpu time, factor 1.88)
09:42:13 Running Algebraic_Numbers_Lib ...
09:42:20 Akra_Bazzi: theory Akra_Bazzi.Dense_Linear_Order
09:42:21 Timing List_Update (2 threads, 128.969s elapsed time, 246.584s cpu time, 10.736s GC time, factor 1.91)
09:42:21 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update
09:42:21 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update/document.pdf
09:42:21 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update/outline.pdf
09:42:21 Finished List_Update (0:02:28 elapsed time, 0:04:32 cpu time, factor 1.83)
09:42:21 Running UpDown_Scheme ...
09:42:23 Akra_Bazzi: theory Akra_Bazzi.Approximation
09:42:24 Timing HOL-ODE-Refinement (2 threads, 189.478s elapsed time, 332.432s cpu time, 19.400s GC time, factor 1.75)
09:42:24 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE-Refinement
09:42:24 Finished HOL-ODE-Refinement (0:04:39 elapsed time, 0:09:02 cpu time, factor 1.94)
09:42:25 Running HOL-ODE-Numerics ...
09:42:28 Timing Differential_Dynamic_Logic (2 threads, 257.996s elapsed time, 460.024s cpu time, 23.832s GC time, factor 1.78)
09:42:28 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Differential_Dynamic_Logic
09:42:28 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Differential_Dynamic_Logic/document.pdf
09:42:28 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Differential_Dynamic_Logic/outline.pdf
09:42:28 Finished Differential_Dynamic_Logic (0:04:38 elapsed time, 0:08:03 cpu time, factor 1.73)
09:42:28 Running Random_Graph_Subgraph_Threshold ...
09:42:30 Timing Ergodic_Theory (2 threads, 99.397s elapsed time, 196.200s cpu time, 5.220s GC time, factor 1.97)
09:42:30 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ergodic_Theory
09:42:30 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ergodic_Theory/document.pdf
09:42:30 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ergodic_Theory/outline.pdf
09:42:30 Finished Ergodic_Theory (0:01:59 elapsed time, 0:03:37 cpu time, factor 1.83)
09:42:30 Running MFMC_Countable ...
09:42:33 UpDown_Scheme: theory UpDown_Scheme.Quicksort
09:42:33 UpDown_Scheme: theory UpDown_Scheme.Heap
09:42:34 UpDown_Scheme: theory UpDown_Scheme.Misc
09:42:34 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
09:42:34 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
09:42:35 UpDown_Scheme: theory UpDown_Scheme.Heap_Monad
09:42:35 Algebraic_Numbers: theory Algebraic_Numbers.Unique_Factorization
09:42:36 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
09:42:36 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Compare_Complex
09:42:36 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Complex_Roots_Real_Poly
09:42:37 UpDown_Scheme: theory UpDown_Scheme.Array
09:42:38 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Unique_Factorization
09:42:38 UpDown_Scheme: theory UpDown_Scheme.Ref
09:42:38 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Bivariate_Polynomials
09:42:39 UpDown_Scheme: theory UpDown_Scheme.Imperative_HOL
09:42:39 UpDown_Scheme: theory UpDown_Scheme.Imperative_HOL_Add
09:42:39 UpDown_Scheme: theory UpDown_Scheme.Run
09:42:39 UpDown_Scheme: theory UpDown_Scheme.Syntax_Match
09:42:39 UpDown_Scheme: theory UpDown_Scheme.Sep_Misc
09:42:40 UpDown_Scheme: theory UpDown_Scheme.Assertions
09:42:40 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Dense_Linear_Order
09:42:40 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Girth_Chromatic_Misc
09:42:40 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraphs
09:42:42 UpDown_Scheme: theory UpDown_Scheme.Hoare_Triple
09:42:42 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Approximation
09:42:42 UpDown_Scheme: theory UpDown_Scheme.Automation
09:42:43 MFMC_Countable: theory MFMC_Countable.MFMC_Misc
09:42:44 UpDown_Scheme: theory UpDown_Scheme.Sep_Main
09:42:44 MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
09:42:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Float_Real
09:42:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Affine_Form
09:42:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Counterclockwise
09:42:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Counterclockwise_Vector
09:42:46 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Counterclockwise_2D_Strict
09:42:46 Timing Density_Compiler (2 threads, 105.727s elapsed time, 209.184s cpu time, 5.536s GC time, factor 1.98)
09:42:46 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Density_Compiler
09:42:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Density_Compiler/document.pdf
09:42:46 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Density_Compiler/outline.pdf
09:42:46 Finished Density_Compiler (0:02:03 elapsed time, 0:03:48 cpu time, factor 1.85)
09:42:47 Running Girth_Chromatic ...
09:42:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Counterclockwise_2D_Arbitrary
09:42:47 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Polygon
09:42:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Euclidean_Space_Explicit
09:42:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Executable_Euclidean_Space
09:42:49 Algebraic_Numbers: theory Algebraic_Numbers.Unique_Factorization_Poly
09:42:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Affine_Approximation
09:42:51 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
09:42:51 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
09:42:52 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Unique_Factorization_Poly
09:42:53 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
09:42:53 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Resultant
09:42:53 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Algebraic_Numbers_Prelim
09:42:54 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
09:42:56 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Sturm_Rat
09:42:57 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Algebraic_Numbers
09:42:58 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
09:42:59 Girth_Chromatic: theory Girth_Chromatic.Dense_Linear_Order
09:42:59 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
09:42:59 Girth_Chromatic: theory Girth_Chromatic.Ugraphs
09:43:00 MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
09:43:01 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Algebraic_Numbers
09:43:01 Girth_Chromatic: theory Girth_Chromatic.Approximation
09:43:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Affine_Code
09:43:11 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Ex_Affine_Approximation
09:43:12 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Ex_Ineqs
09:43:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Intersection
09:43:18 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
09:43:19 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
09:43:19 Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral
09:43:19 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library
09:43:19 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
09:43:19 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics
09:43:20 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
09:43:20 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real
09:43:20 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
09:43:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Ex_Inter
09:43:22 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi
09:43:22 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Roots
09:43:22 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Alg
09:43:23 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Approx
09:43:23 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Show_Real_Precise
09:43:23 Algebraic_Numbers: theory Algebraic_Numbers.Real_Factorization
09:43:24 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Complex_Algebraic_Numbers
09:43:24 Akra_Bazzi: theory Akra_Bazzi.Master_Theorem
09:43:26 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method
09:43:27 Algebraic_Numbers_Lib: theory Algebraic_Numbers_Lib.Real_Factorization
09:43:28 Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation
09:43:29 Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples
09:43:34 UpDown_Scheme: theory UpDown_Scheme.Grid_Point
09:43:35 UpDown_Scheme: theory UpDown_Scheme.Grid
09:43:36 UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
09:43:37 UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
09:43:39 UpDown_Scheme: theory UpDown_Scheme.Down
09:43:39 UpDown_Scheme: theory UpDown_Scheme.Up
09:43:40 UpDown_Scheme: theory UpDown_Scheme.Imperative
09:43:40 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Girth_Chromatic
09:43:41 UpDown_Scheme: theory UpDown_Scheme.Up_Down
09:43:47 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
09:43:49 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
09:43:50 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
09:43:51 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
09:43:52 Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
09:43:56 Timing Akra_Bazzi (2 threads, 91.795s elapsed time, 160.400s cpu time, 7.100s GC time, factor 1.75)
09:43:56 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Akra_Bazzi
09:43:56 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Akra_Bazzi/document.pdf
09:43:56 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Akra_Bazzi/outline.pdf
09:43:56 Finished Akra_Bazzi (0:01:46 elapsed time, 0:02:56 cpu time, factor 1.66)
09:43:56 Running Hermite ...
09:43:59 Timing MFMC_Countable (2 threads, 69.716s elapsed time, 128.732s cpu time, 6.368s GC time, factor 1.85)
09:43:59 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/MFMC_Countable
09:43:59 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/MFMC_Countable/document.pdf
09:43:59 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/MFMC_Countable/outline.pdf
09:43:59 Finished MFMC_Countable (0:01:28 elapsed time, 0:02:29 cpu time, factor 1.69)
09:43:59 Running SDS_Impossibility ...
09:43:59 Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
09:44:02 Timing Random_Graph_Subgraph_Threshold (2 threads, 78.909s elapsed time, 136.796s cpu time, 6.608s GC time, factor 1.73)
09:44:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold
09:44:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf
09:44:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf
09:44:02 Finished Random_Graph_Subgraph_Threshold (0:01:33 elapsed time, 0:02:32 cpu time, factor 1.63)
09:44:02 Running Tarskis_Geometry ...
09:44:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Straight_Line_Program
09:44:06 Timing UpDown_Scheme (2 threads, 90.106s elapsed time, 140.848s cpu time, 4.596s GC time, factor 1.56)
09:44:06 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UpDown_Scheme
09:44:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UpDown_Scheme/document.pdf
09:44:06 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UpDown_Scheme/outline.pdf
09:44:06 Finished UpDown_Scheme (0:01:45 elapsed time, 0:02:36 cpu time, factor 1.49)
09:44:06 Running Probabilistic_System_Zoo-BNFs ...
09:44:07 Timing Girth_Chromatic (2 threads, 66.313s elapsed time, 113.940s cpu time, 5.584s GC time, factor 1.72)
09:44:07 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Girth_Chromatic
09:44:07 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Girth_Chromatic/document.pdf
09:44:07 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Girth_Chromatic/outline.pdf
09:44:07 Finished Girth_Chromatic (0:01:20 elapsed time, 0:02:08 cpu time, factor 1.60)
09:44:07 Running Probabilistic_System_Zoo ...
09:44:08 Hermite: theory Hermite.Hermite
09:44:12 SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
09:44:12 Tarskis_Geometry: theory Tarskis_Geometry.Congruence
09:44:13 Hermite: theory Hermite.Hermite_IArrays
09:44:14 Tarskis_Geometry: theory Tarskis_Geometry.Order
09:44:15 Tarskis_Geometry: theory Tarskis_Geometry.Lattice
09:44:16 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Order_Union
09:44:16 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Probability_Measure
09:44:16 Tarskis_Geometry: theory Tarskis_Geometry.Complete_Lattice
09:44:16 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Fun_More
09:44:17 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Order_Relation_More
09:44:17 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellfounded_More
09:44:17 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Relation
09:44:17 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Embedding
09:44:18 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Constructions
09:44:18 Tarskis_Geometry: theory Tarskis_Geometry.Group
09:44:19 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Giry_Monad
09:44:19 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinal_Order_Relation
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Union
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Fun_More
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Relation_More
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Extension
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellfounded_More
09:44:20 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinal_Arithmetic
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Eisbach
09:44:20 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Relation
09:44:21 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Ordinal_Arithmetic
09:44:21 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Embedding
09:44:21 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Constructions
09:44:21 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Extension
09:44:22 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Order_Relation
09:44:22 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Ordinal_Arithmetic
09:44:22 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinals
09:44:23 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Arithmetic
09:44:24 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinals
09:44:24 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bounded_Set
09:44:25 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Affine_Arithmetic
09:44:25 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
09:44:30 Timing Algebraic_Numbers_Lib (2 threads, 112.911s elapsed time, 207.508s cpu time, 7.888s GC time, factor 1.84)
09:44:30 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers_Lib
09:44:30 Finished Algebraic_Numbers_Lib (0:02:16 elapsed time, 0:03:51 cpu time, factor 1.69)
09:44:30 Running Probabilistic_System_Zoo-Non_BNFs ...
09:44:32 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Union
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Fun_More
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Relation_More
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Extension
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Eisbach
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellfounded_More
09:44:43 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Relation
09:44:44 Tarskis_Geometry: theory Tarskis_Geometry.Metric
09:44:44 Tarskis_Geometry: theory Tarskis_Geometry.Action
09:44:44 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Embedding
09:44:44 Tarskis_Geometry: theory Tarskis_Geometry.Miscellany
09:44:44 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Constructions
09:44:45 Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2
09:44:45 Tarskis_Geometry: theory Tarskis_Geometry.Tarski
09:44:45 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Order_Relation
09:44:45 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Ordinal_Arithmetic
09:44:46 Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski
09:44:46 Tarskis_Geometry: theory Tarskis_Geometry.Projective
09:44:46 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
09:44:47 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Arithmetic
09:44:47 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinals
09:44:47 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Bounded_Set
09:44:48 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Nonempty_Bounded_Set
09:44:49 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy
09:44:49 Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski
09:45:02 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Probability_Mass_Function
09:45:02 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bool_Bounded_Set
09:45:03 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bounded_Set
09:45:03 Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Nonempty_Bounded_Set
09:45:06 Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
09:45:10 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi
09:45:14 Timing SDS_Impossibility (2 threads, 60.034s elapsed time, 104.604s cpu time, 2.852s GC time, factor 1.74)
09:45:14 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SDS_Impossibility
09:45:14 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SDS_Impossibility/document.pdf
09:45:14 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SDS_Impossibility/outline.pdf
09:45:14 Finished SDS_Impossibility (0:01:15 elapsed time, 0:02:00 cpu time, factor 1.60)
09:45:14 Running pGCL ...
09:45:18 Timing Probabilistic_System_Zoo (2 threads, 56.367s elapsed time, 95.536s cpu time, 4.928s GC time, factor 1.69)
09:45:18 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo
09:45:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/document.pdf
09:45:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf
09:45:18 Finished Probabilistic_System_Zoo (0:01:10 elapsed time, 0:01:50 cpu time, factor 1.57)
09:45:18 Running Lp ...
09:45:20 Timing Tarskis_Geometry (2 threads, 61.382s elapsed time, 112.764s cpu time, 4.332s GC time, factor 1.84)
09:45:20 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tarskis_Geometry
09:45:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tarskis_Geometry/document.pdf
09:45:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tarskis_Geometry/outline.pdf
09:45:20 Finished Tarskis_Geometry (0:01:17 elapsed time, 0:02:10 cpu time, factor 1.69)
09:45:20 Running Stern_Brocot ...
09:45:20 Timing Probabilistic_System_Zoo-BNFs (2 threads, 61.456s elapsed time, 113.288s cpu time, 4.476s GC time, factor 1.84)
09:45:20 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs
09:45:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs/document.pdf
09:45:20 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs/outline.pdf
09:45:20 Finished Probabilistic_System_Zoo-BNFs (0:01:14 elapsed time, 0:02:07 cpu time, factor 1.71)
09:45:20 Running Rank_Nullity_Theorem ...
09:45:24 Timing Hermite (2 threads, 73.532s elapsed time, 129.772s cpu time, 15.820s GC time, factor 1.76)
09:45:24 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Hermite
09:45:24 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Hermite/document.pdf
09:45:24 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Hermite/outline.pdf
09:45:24 Finished Hermite (0:01:28 elapsed time, 0:02:25 cpu time, factor 1.65)
09:45:24 Running Euler_MacLaurin ...
09:45:25 pGCL: theory pGCL.Misc
09:45:25 pGCL: theory pGCL.Expectations
09:45:26 pGCL: theory pGCL.Transformers
09:45:27 pGCL: theory pGCL.Induction
09:45:28 pGCL: theory pGCL.Embedding
09:45:28 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Finitely_Bounded_Set_Counterexample
09:45:28 Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi_Counterexample
09:45:29 pGCL: theory pGCL.Healthiness
09:45:30 pGCL: theory pGCL.Continuity
09:45:30 Lp: theory Lp.SG_Library_Complement
09:45:31 pGCL: theory pGCL.LoopInduction
09:45:31 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
09:45:31 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Generalizations
09:45:31 pGCL: theory pGCL.Sublinearity
09:45:31 Lp: theory Lp.Functional_Spaces
09:45:31 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
09:45:31 pGCL: theory pGCL.WellDefined
09:45:32 pGCL: theory pGCL.Algebra
09:45:33 Lp: theory Lp.Lp
09:45:33 Timing Probabilistic_System_Zoo-Non_BNFs (2 threads, 48.295s elapsed time, 95.724s cpu time, 5.864s GC time, factor 1.98)
09:45:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs
09:45:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/document.pdf
09:45:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/outline.pdf
09:45:33 Finished Probabilistic_System_Zoo-Non_BNFs (0:01:02 elapsed time, 0:01:50 cpu time, factor 1.77)
09:45:33 Running Perron_Frobenius ...
09:45:33 pGCL: theory pGCL.StructuredReasoning
09:45:34 Stern_Brocot: theory Stern_Brocot.Cotree
09:45:34 pGCL: theory pGCL.Automation
09:45:34 pGCL: theory pGCL.Determinism
09:45:34 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
09:45:35 pGCL: theory pGCL.Loops
09:45:35 pGCL: theory pGCL.Termination
09:45:35 Euler_MacLaurin: theory Euler_MacLaurin.Bernoulli
09:45:35 pGCL: theory pGCL.pGCL
09:45:35 Euler_MacLaurin: theory Euler_MacLaurin.Bernoulli_FPS
09:45:35 Euler_MacLaurin: theory Euler_MacLaurin.Periodic_Bernpoly
09:45:36 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
09:45:36 pGCL: theory pGCL.LoopExamples
09:45:36 pGCL: theory pGCL.Monty
09:45:37 Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
09:45:38 pGCL: theory pGCL.Primitives
09:45:42 Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
09:45:43 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
09:45:44 Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
09:45:45 Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
09:45:51 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
09:45:51 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
09:45:51 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
09:45:55 Timing Euler_MacLaurin (2 threads, 16.961s elapsed time, 31.956s cpu time, 0.796s GC time, factor 1.88)
09:45:55 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Euler_MacLaurin
09:45:55 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Euler_MacLaurin/document.pdf
09:45:55 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Euler_MacLaurin/outline.pdf
09:45:55 Finished Euler_MacLaurin (0:00:30 elapsed time, 0:00:46 cpu time, factor 1.52)
09:45:55 Running Chord_Segments ...
09:45:56 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
09:45:56 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
09:45:58 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
09:45:58 Timing Rank_Nullity_Theorem (2 threads, 23.164s elapsed time, 38.020s cpu time, 1.648s GC time, factor 1.64)
09:45:58 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rank_Nullity_Theorem
09:45:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rank_Nullity_Theorem/document.pdf
09:45:58 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf
09:45:58 Finished Rank_Nullity_Theorem (0:00:36 elapsed time, 0:00:52 cpu time, factor 1.44)
09:45:58 Running Lower_Semicontinuous ...
09:46:04 Timing Perron_Frobenius (2 threads, 10.794s elapsed time, 17.748s cpu time, 0.544s GC time, factor 1.64)
09:46:04 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius
09:46:04 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius/document.pdf
09:46:04 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius/outline.pdf
09:46:04 Finished Perron_Frobenius (0:00:30 elapsed time, 0:00:38 cpu time, factor 1.25)
09:46:04 Running Comparison_Sort_Lower_Bound ...
09:46:05 Chord_Segments: theory Chord_Segments.Angles
09:46:06 Chord_Segments: theory Chord_Segments.Triangle
09:46:07 Stern_Brocot: theory Stern_Brocot.Bird_Tree
09:46:08 Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
09:46:10 Timing pGCL (2 threads, 38.943s elapsed time, 76.964s cpu time, 2.556s GC time, factor 1.98)
09:46:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/pGCL
09:46:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/pGCL/document.pdf
09:46:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/pGCL/outline.pdf
09:46:10 Finished pGCL (0:00:55 elapsed time, 0:01:35 cpu time, factor 1.74)
09:46:10 Running Random_BSTs ...
09:46:11 Timing Stern_Brocot (2 threads, 34.322s elapsed time, 56.144s cpu time, 3.820s GC time, factor 1.64)
09:46:11 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stern_Brocot
09:46:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stern_Brocot/document.pdf
09:46:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stern_Brocot/outline.pdf
09:46:11 Finished Stern_Brocot (0:00:50 elapsed time, 0:01:13 cpu time, factor 1.45)
09:46:11 Running Triangle ...
09:46:11 Chord_Segments: theory Chord_Segments.Chord_Segments
09:46:13 Timing Lp (2 threads, 38.484s elapsed time, 69.400s cpu time, 1.356s GC time, factor 1.80)
09:46:13 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lp
09:46:13 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lp/document.pdf
09:46:13 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lp/outline.pdf
09:46:13 Finished Lp (0:00:54 elapsed time, 0:01:26 cpu time, factor 1.59)
09:46:13 Running Source_Coding_Theorem ...
09:46:16 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.List_Index
09:46:16 Timing Chord_Segments (2 threads, 8.001s elapsed time, 10.320s cpu time, 0.244s GC time, factor 1.29)
09:46:16 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Chord_Segments
09:46:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Chord_Segments/document.pdf
09:46:16 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Chord_Segments/outline.pdf
09:46:16 Finished Chord_Segments (0:00:20 elapsed time, 0:00:23 cpu time, factor 1.16)
09:46:16 Running Cayley_Hamilton ...
09:46:18 Timing Lower_Semicontinuous (2 threads, 7.582s elapsed time, 14.352s cpu time, 0.344s GC time, factor 1.89)
09:46:18 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lower_Semicontinuous
09:46:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lower_Semicontinuous/document.pdf
09:46:18 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lower_Semicontinuous/outline.pdf
09:46:18 Finished Lower_Semicontinuous (0:00:20 elapsed time, 0:00:27 cpu time, factor 1.37)
09:46:18 Running Catalan_Numbers ...
09:46:18 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
09:46:19 Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
09:46:21 Triangle: theory Triangle.Angles
09:46:22 Triangle: theory Triangle.Triangle
09:46:23 Random_BSTs: theory Random_BSTs.Cmp
09:46:23 Random_BSTs: theory Random_BSTs.Less_False
09:46:23 Random_BSTs: theory Random_BSTs.Sorted_Less
09:46:23 Random_BSTs: theory Random_BSTs.List_Ins_Del
09:46:24 Random_BSTs: theory Random_BSTs.Set_by_Ordered
09:46:24 Random_BSTs: theory Random_BSTs.Tree_Set
09:46:25 Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
09:46:25 Random_BSTs: theory Random_BSTs.Random_BSTs
09:46:25 Timing Comparison_Sort_Lower_Bound (2 threads, 7.522s elapsed time, 12.928s cpu time, 0.536s GC time, factor 1.72)
09:46:25 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound
09:46:25 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf
09:46:25 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf
09:46:25 Finished Comparison_Sort_Lower_Bound (0:00:21 elapsed time, 0:00:27 cpu time, factor 1.29)
09:46:26 Running Fisher_Yates ...
09:46:26 Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
09:46:28 Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
09:46:29 Timing Triangle (2 threads, 5.613s elapsed time, 7.304s cpu time, 0.148s GC time, factor 1.30)
09:46:29 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Triangle
09:46:29 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Triangle/document.pdf
09:46:29 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Triangle/outline.pdf
09:46:29 Finished Triangle (0:00:17 elapsed time, 0:00:19 cpu time, factor 1.13)
09:46:29 Running Ptolemys_Theorem ...
09:46:29 Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
09:46:29 Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
09:46:33 Timing Random_BSTs (2 threads, 7.691s elapsed time, 12.468s cpu time, 0.764s GC time, factor 1.62)
09:46:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_BSTs
09:46:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_BSTs/document.pdf
09:46:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Random_BSTs/outline.pdf
09:46:33 Finished Random_BSTs (0:00:22 elapsed time, 0:00:28 cpu time, factor 1.24)
09:46:33 Timing Source_Coding_Theorem (2 threads, 5.665s elapsed time, 10.032s cpu time, 0.244s GC time, factor 1.77)
09:46:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Source_Coding_Theorem
09:46:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Source_Coding_Theorem/document.pdf
09:46:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Source_Coding_Theorem/outline.pdf
09:46:33 Finished Source_Coding_Theorem (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.26)
09:46:33 Running Cartan_FP ...
09:46:34 Timing Cayley_Hamilton (2 threads, 5.612s elapsed time, 10.396s cpu time, 0.220s GC time, factor 1.85)
09:46:34 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cayley_Hamilton
09:46:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cayley_Hamilton/document.pdf
09:46:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cayley_Hamilton/outline.pdf
09:46:34 Finished Cayley_Hamilton (0:00:17 elapsed time, 0:00:23 cpu time, factor 1.32)
09:46:35 Timing Catalan_Numbers (2 threads, 3.828s elapsed time, 7.080s cpu time, 0.144s GC time, factor 1.85)
09:46:35 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Catalan_Numbers
09:46:35 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Catalan_Numbers/document.pdf
09:46:35 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Catalan_Numbers/outline.pdf
09:46:35 Finished Catalan_Numbers (0:00:16 elapsed time, 0:00:20 cpu time, factor 1.24)
09:46:38 Fisher_Yates: theory Fisher_Yates.Fisher_Yates
09:46:39 Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
09:46:42 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Generator_Aux
09:46:42 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Derive_Manager
09:46:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ICF_Tools
09:46:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Show
09:46:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Ord_Code_Preproc
09:46:43 Cartan_FP: theory Cartan_FP.Cartan
09:46:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Locale_Code
09:46:43 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
09:46:43 Timing Fisher_Yates (2 threads, 3.698s elapsed time, 7.120s cpu time, 0.140s GC time, factor 1.93)
09:46:43 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fisher_Yates
09:46:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fisher_Yates/document.pdf
09:46:43 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fisher_Yates/outline.pdf
09:46:43 Finished Fisher_Yates (0:00:17 elapsed time, 0:00:21 cpu time, factor 1.23)
09:46:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Show_Instances
09:46:44 Timing Ptolemys_Theorem (2 threads, 3.354s elapsed time, 4.980s cpu time, 0.080s GC time, factor 1.48)
09:46:44 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ptolemys_Theorem
09:46:44 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ptolemys_Theorem/document.pdf
09:46:44 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Ptolemys_Theorem/outline.pdf
09:46:44 Finished Ptolemys_Theorem (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.15)
09:46:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
09:46:46 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
09:46:47 Timing Cartan_FP (2 threads, 2.320s elapsed time, 4.304s cpu time, 0.132s GC time, factor 1.86)
09:46:47 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cartan_FP
09:46:47 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cartan_FP/document.pdf
09:46:47 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Cartan_FP/outline.pdf
09:46:47 Finished Cartan_FP (0:00:14 elapsed time, 0:00:17 cpu time, factor 1.18)
09:46:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
09:46:51 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
09:46:55 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
09:46:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Optimize_Integer
09:46:58 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Optimize_Float
09:46:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Print
09:47:03 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Plot
09:47:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
09:47:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
09:49:24 Timing Algebraic_Numbers (2 threads, 404.049s elapsed time, 723.552s cpu time, 56.712s GC time, factor 1.79)
09:49:24 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers
09:49:24 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf
09:49:24 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf
09:49:24 Finished Algebraic_Numbers (0:07:13 elapsed time, 0:12:35 cpu time, factor 1.74)
09:55:33 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
09:55:44 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
09:56:00 Timing HOL-ODE-Numerics (2 threads, 794.730s elapsed time, 1489.100s cpu time, 61.124s GC time, factor 1.87)
09:56:00 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE-Numerics
09:56:00 Finished HOL-ODE-Numerics (0:13:34 elapsed time, 0:25:08 cpu time, factor 1.85)
09:56:00 
09:56:00 === TIMING ===
09:56:00 
09:56:00 Group AFP: 2:50:59 elapsed time, 4:53:21 cpu time, factor 1.72
09:56:00 Group main: 0:21:29 elapsed time, 0:36:24 cpu time, factor 1.69
09:56:00 Group timing: 0:24:05 elapsed time, 0:41:03 cpu time, factor 1.70
09:56:00 Overall: 0:40:47 elapsed time, 5:38:00 cpu time, factor 8.29
09:56:00 
09:56:00 === SITEGEN ===
09:56:00 
09:56:00 Writing status file ...
09:56:00 Running sitegen ...
09:56:02 Success: Generated topics.shtml
09:56:02 Success: Generated index.shtml
09:56:02 Success: Generated shtml files for 347 entries
09:56:02 Success: Generated statistics.shtml
09:56:02 Success: Generated about.shtml
09:56:02 Success: Generated citing.shtml
09:56:02 Success: Generated updating.shtml
09:56:02 Success: Generated search.shtml
09:56:02 Success: Generated submitting.shtml
09:56:02 Success: Generated using.shtml
09:56:02 Success: Generated rss.xml
09:56:02 Success: Generated status.shtml
09:56:02 Packing tars ...
09:56:08 
09:56:08 === COMPLETED ===
09:56:08 
09:56:08 Archiving artifacts
09:56:57 Started calculate disk usage of build
09:56:57 Finished Calculation of disk usage of build in 0 seconds
09:57:05 Started calculate disk usage of workspace
09:57:06 Finished Calculation of disk usage of workspace in 0 seconds
09:57:06 No emails were triggered.
09:57:06 Finished: SUCCESS