Console Output

23:16:14 Started by upstream project "isabelle-repo" build number 860
23:16:14 originally caused by:
23:16:14  Started by an SCM change
23:16:14 [EnvInject] - Loading node environment variables.
23:16:14 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp
23:16:14 [isabelle-repo-afp] $ hg showconfig paths.default
23:16:14 [isabelle-repo-afp] $ hg pull --rev 8376f83f909458ddba232454b62258b5f7ed5a06
23:16:14 pulling from http://isabelle.in.tum.de/repos/isabelle/
23:16:14 searching for changes
23:16:14 adding changesets
23:16:14 adding manifests
23:16:14 adding file changes
23:16:14 added 1 changesets with 1 changes to 1 files
23:16:14 (run 'hg update' to get a working copy)
23:16:14 [isabelle-repo-afp] $ hg update --clean --rev 8376f83f909458ddba232454b62258b5f7ed5a06
23:16:14 1 files updated, 0 files merged, 0 files removed, 0 files unresolved
23:16:14 [isabelle-repo-afp] $ hg log --rev . --template {node}
23:16:14 [isabelle-repo-afp] $ hg log --rev . --template {rev}
23:16:14 [isabelle-repo-afp] $ hg id --branch
23:16:15 [afp] $ hg showconfig paths.default
23:16:15 [afp] $ hg pull --rev default
23:16:16 pulling from https://bitbucket.org/isa-afp/afp-devel/
23:16:16 searching for changes
23:16:16 adding changesets
23:16:16 adding manifests
23:16:16 adding file changes
23:16:16 added 11 changesets with 25 changes to 25 files
23:16:16 (run 'hg update' to get a working copy)
23:16:16 [afp] $ hg update --clean --rev default
23:16:16 374 files updated, 0 files merged, 2 files removed, 0 files unresolved
23:16:16 [afp] $ hg --config extensions.purge= clean --all
23:16:16 [afp] $ hg log --rev . --template {node}
23:16:16 [afp] $ hg log --rev . --template {rev}
23:16:16 No emails were triggered.
23:16:16 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson4138414001306606233.sh
23:16:16 + Admin/jenkins/run_build afp
23:16:16 + set -e
23:16:16 + PROFILE=afp
23:16:16 + shift
23:16:16 + bin/isabelle components -a
23:16:17 + bin/isabelle jedit -bf
23:16:17 ### Building Isabelle/Scala ...
23:16:46 ### Building Isabelle/jEdit ...
23:17:02 + bin/isabelle ci_build_afp
23:17:08 
23:17:08 === CONFIGURATION ===
23:17:08 
23:17:08 ISABELLE_BUILD_OPTIONS=""
23:17:08 
23:17:08 ML_PLATFORM="x86_64-linux"
23:17:08 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
23:17:08 ML_SYSTEM="polyml-5.6"
23:17:08 ML_OPTIONS="-H 4000 --maxheap 8G"
23:17:08 
23:17:08 === BUILD ===
23:17:08 
23:17:08 Build started at Mon, 24 Apr 2017 21:17:08 GMT
23:17:08 Isabelle id 8376f83f9094
23:17:08 AFP id a663f5cf7dfa
23:17:08 
23:17:08 === LOG ===
23:17:08 
23:17:09 Session Pure/Pure
23:17:09 Session HOL/HOL (main)
23:17:10 Session AFP/AVL-Trees (AFP)
23:17:10 Session AFP/AWN (AFP)
23:17:10 Session AFP/Abortable_Linearizable_Modules (AFP)
23:17:10 Session AFP/Abstract-Hoare-Logics (AFP)
23:17:10 Session AFP/Allen_Calculus (AFP)
23:17:10 Session AFP/Automatic_Refinement (AFP)
23:17:10 Session AFP/Refine_Monadic (AFP)
23:17:11 Session AFP/Collections (AFP)
23:17:11 Session AFP/CAVA_Base (AFP)
23:17:11 Session AFP/CAVA_Automata (AFP)
23:17:11 Session AFP/DFS_Framework (AFP)
23:17:11 Session AFP/Gabow_SCC (AFP)
23:17:11 Session AFP/LTL_to_GBA (AFP)
23:17:11 Session AFP/CAVA_buildchain1 (AFP)
23:17:11 Session AFP/CAVA_buildchain3 (AFP)
23:17:11 Session AFP/CAVA_LTL_Modelchecker (AFP)
23:17:11 Session AFP/Promela (AFP)
23:17:12 Session AFP/Collections_Examples (AFP)
23:17:12 Session AFP/Dijkstra_Shortest_Path (AFP)
23:17:12 Session AFP/Formal_SSA (AFP)
23:17:12 Session AFP/Minimal_SSA (AFP)
23:17:12 Session AFP/Sepref_Prereq (AFP)
23:17:12 Session AFP/Refine_Imperative_HOL (AFP)
23:17:12 Session AFP/Sepref_Basic (AFP)
23:17:12 Session AFP/Sepref_IICF (AFP)
23:17:12 Session AFP/EdmondsKarp_Base (AFP)
23:17:12 Session AFP/EdmondsKarp_Maxflow (AFP)
23:17:12 Session AFP/Transitive-Closure (AFP)
23:17:12 Session AFP/Tree-Automata (AFP)
23:17:12 Session AFP/BinarySearchTree (AFP)
23:17:12 Session AFP/Binomial-Queues (AFP)
23:17:12 Session AFP/Bondy (AFP)
23:17:12 Session AFP/Bounded_Deducibility_Security (AFP)
23:17:12 Session AFP/BytecodeLogicJmlTypes (AFP)
23:17:13 Session AFP/CISC-Kernel (AFP)
23:17:13 Session AFP/CYK (AFP)
23:17:13 Session AFP/Case_Labeling (AFP)
23:17:13 Session AFP/Cauchy (AFP)
23:17:13 Session AFP/Sqrt_Babylonian (AFP)
23:17:13 Session AFP/Real_Impl (AFP)
23:17:13 Session AFP/Certification_Monads (AFP)
23:17:13 Session AFP/ClockSynchInst (AFP)
23:17:13 Session AFP/Coinductive_Languages (AFP)
23:17:13 Session AFP/Compiling-Exceptions-Correctly (AFP)
23:17:13 Session AFP/Completeness (AFP)
23:17:13 Session AFP/ComponentDependencies (AFP)
23:17:13 Session AFP/Concurrent_Ref_Alg (AFP)
23:17:13 Session AFP/Consensus_Refined (AFP)
23:17:13 Session AFP/Constructor_Funs (AFP)
23:17:13 Session AFP/CryptoBasedCompositionalProperties (AFP)
23:17:13 Session AFP/DPT-SAT-Solver (AFP)
23:17:13 Session AFP/DataRefinementIBP (AFP)
23:17:13 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
23:17:13 Session AFP/Dependent_SIFUM_Refinement (AFP)
23:17:13 Session AFP/Depth-First-Search (AFP)
23:17:13 Session AFP/DiskPaxos (AFP)
23:17:13 Session AFP/Encodability_Process_Calculi (AFP)
23:17:14 Session AFP/Euler_Partition (AFP)
23:17:14 Session AFP/Example-Submission (AFP)
23:17:14 Session AFP/FFT (AFP)
23:17:14 Session AFP/FLP (AFP)
23:17:14 Session AFP/FOL_Harrison (AFP)
23:17:14 Session AFP/FeatherweightJava (AFP)
23:17:14 Session AFP/Featherweight_OCL (AFP)
23:17:14 Session AFP/FileRefinement (AFP)
23:17:14 Session AFP/FinFun (AFP)
23:17:14 Session AFP/Finite_Automata_HF (AFP)
23:17:14 Session AFP/FocusStreamsCaseStudies (AFP)
23:17:14 Session AFP/Free-Groups (AFP)
23:17:14 Session AFP/FunWithFunctions (AFP)
23:17:14 Session AFP/FunWithTilings (AFP)
23:17:14 Session AFP/GPU_Kernel_PL (AFP)
23:17:14 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
23:17:14 Session AFP/GenClock (AFP)
23:17:14 Session AFP/General-Triangle (AFP)
23:17:14 Session AFP/GoedelGod (AFP)
23:17:14 Session AFP/GraphMarkingIBP (AFP)
23:17:14 Session HOL/HOL-Library (main timing)
23:17:15 Session AFP/Abs_Int_ITP2012 (AFP)
23:17:15 Session AFP/Abstract-Rewriting (AFP)
23:17:15 Session AFP/Decreasing-Diagrams (AFP)
23:17:15 Session AFP/Decreasing-Diagrams-II (AFP)
23:17:15 Session AFP/Matrix (AFP)
23:17:15 Session AFP/Matrix_Tensor (AFP)
23:17:15 Session AFP/Knot_Theory (AFP)
23:17:15 Session AFP/Polynomials (AFP)
23:17:15 Session AFP/Groebner_Bases (AFP)
23:17:15 Session AFP/Abstract_Completeness (AFP)
23:17:15 Session AFP/Abstract_Soundness (AFP)
23:17:15 Session AFP/Amortized_Complexity (AFP)
23:17:15 Session AFP/Dynamic_Tables (AFP)
23:17:15 Session AFP/ArrowImpossibilityGS (AFP)
23:17:15 Session AFP/Bell_Numbers_Spivey (AFP)
23:17:15 Session AFP/Card_Equiv_Relations (AFP)
23:17:15 Session AFP/Binomial-Heaps (AFP)
23:17:15 Session AFP/Boolean_Expression_Checkers (AFP)
23:17:15 Session AFP/Buildings (AFP)
23:17:15 Session AFP/Card_Multisets (AFP)
23:17:15 Session AFP/Card_Number_Partitions (AFP)
23:17:15 Session AFP/Category (AFP)
23:17:15 Session AFP/Category2 (AFP)
23:17:15 Session AFP/Category3 (AFP)
23:17:16 Session AFP/CofGroups (AFP)
23:17:16 Session AFP/ConcurrentIMP (AFP)
23:17:16 Session AFP/CoreC++ (AFP)
23:17:16 Session AFP/Datatype_Order_Generator (AFP)
23:17:16 Session AFP/Old_Datatype_Show (AFP)
23:17:16 Session AFP/Derangements (AFP)
23:17:16 Session AFP/Deriving (AFP)
23:17:16 Session AFP/Containers (AFP)
23:17:17 Session AFP/Containers-Benchmarks (AFP)
23:17:17 Session AFP/Show (AFP)
23:17:17 Session AFP/Discrete_Summation (AFP)
23:17:17 Session AFP/Card_Partitions (AFP)
23:17:17 Session AFP/Efficient-Mergesort (AFP)
23:17:17 Session AFP/FOL-Fitting (AFP)
23:17:17 Session AFP/Finger-Trees (AFP)
23:17:17 Session AFP/Formula_Derivatives (AFP)
23:17:17 Session AFP/Formula_Derivatives-Examples (AFP)
23:17:17 Session AFP/Free-Boolean-Algebra (AFP)
23:17:17 Session AFP/Functional-Automata (AFP)
23:17:17 Session AFP/Graph_Theory (AFP)
23:17:17 Session AFP/ShortestPath (AFP)
23:17:17 Session AFP/Group-Ring-Module (AFP)
23:17:17 Session AFP/Valuation (AFP)
23:17:17 Session HOL/HOL-Cardinals (timing)
23:17:17 Session AFP/Ordinals_and_Cardinals (AFP)
23:17:18 Session AFP/Sort_Encodings (AFP)
23:17:18 Session HOL/HOL-Computational_Algebra
23:17:18 Session AFP/Bernoulli (AFP)
23:17:18 Session AFP/Coinductive (AFP)
23:17:18 Session AFP/Lazy-Lists-II (AFP)
23:17:18 Session AFP/Topology (AFP)
23:17:18 Session AFP/Stream_Fusion_Code (AFP)
23:17:18 Session AFP/Descartes_Sign_Rule (AFP)
23:17:18 Session HOL/HOL-Algebra (main timing)
23:17:18 Session AFP/JNF-HOL-Lib (AFP)
23:17:18 Session AFP/JNF-AFP-Lib (AFP)
23:17:18 Session AFP/Jordan_Normal_Form (AFP)
23:17:18 Session AFP/Pre_Perron_Frobenius (AFP)
23:17:19 Session AFP/Perron_Frobenius (AFP)
23:17:19 Session AFP/Subresultants (AFP)
23:17:19 Session AFP/Pre_BZ (AFP)
23:17:19 Session AFP/Berlekamp_Zassenhaus (AFP)
23:17:19 Session AFP/Pre_Algebraic_Numbers (AFP)
23:17:19 Session AFP/Algebraic_Numbers (AFP)
23:17:19 Session AFP/Algebraic_Numbers_Lib (AFP)
23:17:19 Session AFP/Pre_Polynomial_Factorization (AFP)
23:17:19 Session AFP/Polynomial_Factorization (AFP)
23:17:20 Session AFP/Jordan_Hoelder (AFP)
23:17:20 Session AFP/Perfect-Number-Thm (AFP)
23:17:20 Session AFP/Secondary_Sylow (AFP)
23:17:20 Session AFP/VectorSpace (AFP)
23:17:20 Session HOL/HOL-Analysis (main timing)
23:17:20 Session AFP/Affine_Arithmetic (AFP)
23:17:20 Session AFP/Cartan_FP (AFP)
23:17:20 Session AFP/Cayley_Hamilton (AFP)
23:17:20 Session AFP/Chord_Segments (AFP)
23:17:20 Session AFP/Echelon_Form (AFP)
23:17:20 Session AFP/Hermite (AFP)
23:17:20 Session AFP/Gauss_Jordan (AFP)
23:17:20 Session HOL/HOL-Probability (main timing)
23:17:21 Session AFP/Applicative_Lifting (AFP)
23:17:21 Session AFP/Stern_Brocot (AFP)
23:17:21 Session AFP/Deep_Learning_Lib (AFP)
23:17:21 Session AFP/Deep_Learning (AFP)
23:17:21 Session AFP/Density_Compiler (AFP)
23:17:21 Session AFP/Ergodic_Theory (AFP)
23:17:21 Session AFP/Fisher_Yates (AFP)
23:17:21 Session AFP/Girth_Chromatic (AFP)
23:17:21 Session AFP/List_Update (AFP)
23:17:21 Session AFP/Lp (AFP)
23:17:21 Session AFP/MFMC_Countable (AFP)
23:17:22 Session AFP/Markov_Models (AFP)
23:17:22 Session AFP/Probabilistic_Noninterference (AFP)
23:17:22 Session AFP/Probabilistic_System_Zoo (AFP)
23:17:22 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
23:17:22 Session AFP/Quick_Sort_Cost (AFP)
23:17:22 Session AFP/Random_BSTs (AFP)
23:17:22 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
23:17:22 Session AFP/Randomised_Social_Choice (AFP)
23:17:22 Session AFP/SDS_Impossibility (AFP)
23:17:22 Session AFP/Source_Coding_Theorem (AFP)
23:17:23 Session AFP/UpDown_Scheme (AFP)
23:17:23 Session AFP/Landau_Analysis (AFP)
23:17:23 Session AFP/Akra_Bazzi (AFP)
23:17:23 Session AFP/Catalan_Numbers (AFP)
23:17:23 Session AFP/Euler_MacLaurin (AFP)
23:17:23 Session AFP/Stirling_Formula (AFP)
23:17:23 Session AFP/Comparison_Sort_Lower_Bound (AFP)
23:17:23 Session AFP/Lower_Semicontinuous (AFP)
23:17:23 Session AFP/Ordinary_Differential_Equations (AFP)
23:17:24 Session AFP/HOL-ODE (AFP)
23:17:24 Session AFP/Differential_Dynamic_Logic (AFP)
23:17:24 Session AFP/HOL-ODE-Refinement (AFP)
23:17:24 Session AFP/HOL-ODE-Numerics (AFP)
23:17:24 Session AFP/Prime_Harmonic_Series (AFP)
23:17:24 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
23:17:24 Session AFP/Ptolemys_Theorem (AFP)
23:17:24 Session AFP/QR_Decomposition (AFP)
23:17:25 Session AFP/Rank_Nullity_Theorem (AFP)
23:17:25 Session AFP/Tarskis_Geometry (AFP)
23:17:25 Session AFP/Triangle (AFP)
23:17:25 Session AFP/pGCL (AFP)
23:17:25 Session HOL/HOL-Number_Theory (timing)
23:17:25 Session AFP/Bertrands_Postulate (AFP)
23:17:25 Session AFP/E_Transcendental (AFP)
23:17:25 Session AFP/Elliptic_Curves_Group_Law (AFP)
23:17:25 Session AFP/Fermat3_4 (AFP)
23:17:25 Session AFP/Koenigsberg_Friendship_Base (AFP)
23:17:25 Session AFP/Koenigsberg_Friendship (AFP)
23:17:25 Session AFP/Lehmer (AFP)
23:17:25 Session AFP/Pratt_Certificate (AFP)
23:17:26 Session AFP/SumSquares (AFP)
23:17:26 Session AFP/Liouville_Numbers (AFP)
23:17:26 Session AFP/Polynomial_Interpolation (AFP)
23:17:26 Session AFP/RSAPSS (AFP)
23:17:26 Session AFP/Rep_Fin_Groups (AFP)
23:17:26 Session AFP/Sturm_Sequences (AFP)
23:17:26 Session AFP/Special_Function_Bounds (AFP)
23:17:26 Session AFP/Sturm_Tarski (AFP)
23:17:26 Session HOL/HOL-Imperative_HOL
23:17:26 Session AFP/Imperative_Insertion_Sort (AFP)
23:17:26 Session AFP/HereditarilyFinite (AFP)
23:17:26 Session AFP/Incompleteness (AFP)
23:17:26 Session AFP/Surprise_Paradox (AFP)
23:17:26 Session AFP/HyperCTL (AFP)
23:17:26 Session AFP/Incredible_Proof_Machine (AFP)
23:17:26 Session AFP/Integration (AFP)
23:17:26 Session AFP/Isabelle_Meta_Model (AFP)
23:17:26 Session AFP/Jinja (AFP)
23:17:27 Session AFP/HRB-Slicing (AFP)
23:17:27 Session AFP/InformationFlowSlicing_Inter (AFP)
23:17:27 Session AFP/Slicing (AFP)
23:17:27 Session AFP/InformationFlowSlicing (AFP)
23:17:27 Session AFP/KBPs (AFP)
23:17:27 Session AFP/LTL (AFP)
23:17:27 Session AFP/LTL_to_DRA (AFP)
23:17:27 Session AFP/Stuttering_Equivalence (AFP)
23:17:27 Session AFP/Lambda_Free_RPOs (AFP)
23:17:27 Session AFP/Landau_Symbols (AFP)
23:17:27 Session AFP/LightweightJava (AFP)
23:17:27 Session AFP/LinearQuantifierElim (AFP)
23:17:27 Session AFP/List-Infinite (AFP)
23:17:27 Session AFP/Nat-Interval-Logic (AFP)
23:17:27 Session AFP/AutoFocus-Stream (AFP)
23:17:27 Session AFP/MSO_Regex_Equivalence (AFP)
23:17:27 Session AFP/MSO_Examples (AFP)
23:17:27 Session AFP/MuchAdoAboutTwo (AFP)
23:17:27 Session AFP/Myhill-Nerode (AFP)
23:17:28 Session AFP/POPLmark-deBruijn (AFP)
23:17:28 Session AFP/Pairing_Heap (AFP)
23:17:28 Session AFP/Password_Authentication_Protocol (AFP)
23:17:28 Session AFP/Presburger-Automata (AFP)
23:17:28 Session AFP/Priority_Queue_Braun (AFP)
23:17:28 Session AFP/Program-Conflict-Analysis (AFP)
23:17:28 Session AFP/Regex_Equivalence (AFP)
23:17:28 Session AFP/Regex_Equivalence_Examples (AFP)
23:17:28 Session AFP/Regular-Sets (AFP)
23:17:28 Session AFP/Posix-Lexing (AFP)
23:17:28 Session AFP/Ribbon_Proofs (AFP)
23:17:28 Session AFP/SATSolverVerification (AFP)
23:17:28 Session AFP/Selection_Heap_Sort (AFP)
23:17:28 Session AFP/Separata (AFP)
23:17:28 Session AFP/Separation_Logic_Imperative_HOL (AFP)
23:17:28 Session AFP/Skew_Heap (AFP)
23:17:28 Session AFP/Splay_Tree (AFP)
23:17:28 Session AFP/Stable_Matching (AFP)
23:17:29 Session AFP/SuperCalc (AFP)
23:17:29 Session AFP/Tail_Recursive_Functions (AFP)
23:17:29 Session AFP/TortoiseHare (AFP)
23:17:29 Session AFP/Trie (AFP)
23:17:29 Session AFP/Twelvefold_Way (AFP)
23:17:29 Session AFP/Vickrey_Clarke_Groves (AFP)
23:17:29 Session AFP/Well_Quasi_Orders (AFP)
23:17:29 Session AFP/XML (AFP)
23:17:29 Session HOL/HOL-Nominal
23:17:29 Session AFP/CCS (AFP)
23:17:29 Session AFP/Lam-ml-Normalization (AFP)
23:17:29 Session AFP/Pi_Calculus (AFP)
23:17:29 Session AFP/Psi_Calculi (AFP)
23:17:29 Session AFP/SequentInvertibility (AFP)
23:17:30 Session HOL/HOL-Word (main timing)
23:17:30 Session HOL/HOL-SPARK (main)
23:17:30 Session HOL/HOL-SPARK-Examples
23:17:30 Session AFP/RIPEMD-160-SPARK (AFP)
23:17:30 Session AFP/Kleene_Algebra (AFP)
23:17:30 Session AFP/KAT_and_DRA (AFP)
23:17:30 Session AFP/Algebraic_VCs (AFP)
23:17:30 Session AFP/Multirelations (AFP)
23:17:30 Session AFP/Regular_Algebras (AFP)
23:17:30 Session AFP/Relation_Algebra (AFP)
23:17:30 Session AFP/Residuated_Lattices (AFP)
23:17:30 Session AFP/Native_Word (AFP)
23:17:30 Session AFP/SPARCv8 (AFP)
23:17:31 Session AFP/Separation_Algebra (AFP)
23:17:31 Session AFP/Word_Lib (AFP)
23:17:31 Session AFP/Complx (AFP)
23:17:31 Session AFP/IP_Addresses (AFP)
23:17:31 Session AFP/Simple_Firewall (AFP)
23:17:31 Session AFP/Routing (AFP)
23:17:31 Session AFP/Iptables_Semantics (AFP)
23:17:31 Session AFP/LOFT (AFP)
23:17:31 Session HOL/HOLCF (main timing)
23:17:31 Session AFP/Circus (AFP)
23:17:31 Session AFP/HOLCF-HOL-Library (AFP)
23:17:32 Session AFP/HOLCF-Nominal2 (AFP)
23:17:32 Session AFP/Launchbury (AFP)
23:17:32 Session AFP/Call_Arity (AFP)
23:17:32 Session HOL/HOLCF-Library
23:17:32 Session AFP/PCF (AFP)
23:17:32 Session AFP/Shivers-CFA (AFP)
23:17:32 Session AFP/Stream-Fusion (AFP)
23:17:32 Session AFP/Tycon (AFP)
23:17:32 Session AFP/WorkerWrapper (AFP)
23:17:32 Session AFP/Heard_Of (AFP)
23:17:32 Session AFP/HotelKeyCards (AFP)
23:17:32 Session AFP/Huffman (AFP)
23:17:32 Session AFP/IEEE_Floating_Point (AFP)
23:17:32 Session AFP/Impossible_Geometry (AFP)
23:17:32 Session AFP/Inductive_Confidentiality (AFP)
23:17:32 Session AFP/InfPathElimination (AFP)
23:17:32 Session AFP/JiveDataStoreModel (AFP)
23:17:32 Session AFP/KAD (AFP)
23:17:32 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
23:17:32 Session AFP/LatticeProperties (AFP)
23:17:32 Session AFP/MonoBoolTranAlgebra (AFP)
23:17:32 Session AFP/PseudoHoops (AFP)
23:17:33 Session AFP/Lazy_Case (AFP)
23:17:33 Session AFP/Lifting_Definition_Option (AFP)
23:17:33 Session AFP/List-Index (AFP)
23:17:33 Session AFP/List_Interleaving (AFP)
23:17:33 Session AFP/Locally-Nameless-Sigma (AFP)
23:17:33 Session AFP/Marriage (AFP)
23:17:33 Session AFP/Latin_Square (AFP)
23:17:33 Session AFP/Max-Card-Matching (AFP)
23:17:33 Session AFP/Menger (AFP)
23:17:33 Session AFP/MiniML (AFP)
23:17:33 Session AFP/Network_Security_Policy_Verification (AFP)
23:17:33 Session AFP/No_FTL_observers (AFP)
23:17:33 Session AFP/Nominal2 (AFP)
23:17:33 Session AFP/Modal_Logics_for_NTS (AFP)
23:17:33 Session AFP/Rewriting_Z (AFP)
23:17:33 Session AFP/Noninterference_CSP (AFP)
23:17:33 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
23:17:33 Session AFP/Noninterference_Generic_Unwinding (AFP)
23:17:33 Session AFP/Noninterference_Inductive_Unwinding (AFP)
23:17:33 Session AFP/Noninterference_Sequential_Composition (AFP)
23:17:33 Session AFP/Noninterference_Concurrent_Composition (AFP)
23:17:33 Session AFP/NormByEval (AFP)
23:17:33 Session AFP/Open_Induction (AFP)
23:17:33 Session AFP/Ordinal (AFP)
23:17:33 Session AFP/Nested_Multisets_Ordinals (AFP)
23:17:34 Session AFP/Lambda_Free_KBOs (AFP)
23:17:34 Session AFP/Paraconsistency (AFP)
23:17:34 Session AFP/Parity_Game (AFP)
23:17:34 Session AFP/Partial_Function_MR (AFP)
23:17:34 Session AFP/Pop_Refinement (AFP)
23:17:34 Session AFP/Possibilistic_Noninterference (AFP)
23:17:34 Session AFP/Proof_Strategy_Language (AFP)
23:17:34 Session AFP/PropResPI (AFP)
23:17:34 Session AFP/ROBDD (AFP)
23:17:34 Session AFP/Ramsey-Infinite (AFP)
23:17:34 Session AFP/Recursion-Theory-I (AFP)
23:17:34 Session AFP/RefinementReactive (AFP)
23:17:34 Session AFP/Resolution_FOL (AFP)
23:17:35 Session AFP/Robbins-Conjecture (AFP)
23:17:35 Session AFP/Roy_Floyd_Warshall (AFP)
23:17:35 Session AFP/SIFPL (AFP)
23:17:35 Session AFP/SIFUM_Type_Systems (AFP)
23:17:35 Session AFP/SenSocialChoice (AFP)
23:17:35 Session AFP/Simpl (AFP)
23:17:35 Session AFP/BDD (AFP)
23:17:35 Session AFP/Planarity_Certificates (AFP)
23:17:35 Session AFP/Statecharts (AFP)
23:17:35 Session AFP/Stone_Algebras (AFP)
23:17:35 Session AFP/Stone_Relation_Algebras (AFP)
23:17:35 Session AFP/Strong_Security (AFP)
23:17:35 Session AFP/TLA (AFP)
23:17:35 Session AFP/Timed_Automata (AFP)
23:17:35 Session AFP/Transitive-Closure-II (AFP)
23:17:35 Session AFP/Tree_Decomposition (AFP)
23:17:35 Session AFP/UPF (AFP)
23:17:35 Session AFP/UPF_Firewall (AFP)
23:17:35 Session AFP/Verified-Prover (AFP)
23:17:35 Session AFP/VolpanoSmith (AFP)
23:17:35 Session AFP/WHATandWHERE_Security (AFP)
23:17:39 Building HOLCF ...
23:17:39 Building Abstract-Rewriting ...
23:17:39 Building CAVA_Automata ...
23:17:39 Building Discrete_Summation ...
23:17:39 Building Pre_Polynomial_Factorization ...
23:17:39 Running Key_Agreement_Strong_Adversaries ...
23:17:39 Running SPARCv8 ...
23:17:39 Running Markov_Models ...
23:17:41 HOLCF: theory HOLCF.Old_Datatype
23:17:41 HOLCF: theory HOLCF.Nat_Bijection
23:17:41 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Infra
23:17:41 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Messages
23:17:41 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Refinement
23:17:42 SPARCv8: theory SPARCv8.WordDecl
23:17:42 SPARCv8: theory SPARCv8.Adhoc_Overloading
23:17:42 HOLCF: theory HOLCF.Countable
23:17:43 SPARCv8: theory SPARCv8.RegistersOps
23:17:43 SPARCv8: theory SPARCv8.Lib
23:17:43 SPARCv8: theory SPARCv8.Sparc_Types
23:17:43 SPARCv8: theory SPARCv8.DetMonad
23:17:44 SPARCv8: theory SPARCv8.DetMonadLemmas
23:17:44 HOLCF: theory HOLCF.Porder
23:17:44 SPARCv8: theory SPARCv8.Eisbach
23:17:44 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Set
23:17:44 SPARCv8: theory SPARCv8.Eisbach_Tools
23:17:44 Discrete_Summation: theory Discrete_Summation.Discrete_Summation
23:17:44 Discrete_Summation: theory Discrete_Summation.Factorials
23:17:44 HOLCF: theory HOLCF.Pcpo
23:17:45 Discrete_Summation: theory Discrete_Summation.Summation_Conversion
23:17:46 Discrete_Summation: theory Discrete_Summation.Examples
23:17:46 HOLCF: theory HOLCF.Cont
23:17:46 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationN
23:17:46 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Message_derivation
23:17:46 HOLCF: theory HOLCF.Adm
23:17:46 HOLCF: theory HOLCF.Discrete
23:17:47 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Exp
23:17:47 HOLCF: theory HOLCF.Cpodef
23:17:47 HOLCF: theory HOLCF.Fun_Cpo
23:17:47 HOLCF: theory HOLCF.Product_Cpo
23:17:47 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationI
23:17:47 HOLCF: theory HOLCF.Cfun
23:17:48 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Channels
23:17:48 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.IK
23:17:48 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Secrecy
23:17:48 HOLCF: theory HOLCF.Completion
23:17:48 HOLCF: theory HOLCF.Cprod
23:17:49 HOLCF: theory HOLCF.Deflation
23:17:49 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Payloads
23:17:49 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Runs
23:17:49 HOLCF: theory HOLCF.Fix
23:17:49 HOLCF: theory HOLCF.Sfun
23:17:49 HOLCF: theory HOLCF.Sprod
23:17:49 HOLCF: theory HOLCF.Up
23:17:49 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem
23:17:50 HOLCF: theory HOLCF.Lift
23:17:50 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_asymmetric
23:17:50 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_lemmas
23:17:50 HOLCF: theory HOLCF.One
23:17:50 HOLCF: theory HOLCF.Tr
23:17:50 Abstract-Rewriting: theory Abstract-Rewriting.NDerivative
23:17:50 Abstract-Rewriting: theory Abstract-Rewriting.Relation_Interpretation
23:17:50 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_symmetric
23:17:50 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl1
23:17:51 HOLCF: theory HOLCF.Ssum
23:17:51 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl1
23:17:51 HOLCF: theory HOLCF.Fixrec
23:17:51 HOLCF: theory HOLCF.Map_Functions
23:17:51 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Neville_Aitken_Interpolation
23:17:51 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Improved_Code_Equations
23:17:52 Markov_Models: theory Markov_Models.Coinductive_Nat
23:17:52 Markov_Models: theory Markov_Models.Gauss_Jordan_Elim_Fun
23:17:52 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Lagrange_Interpolation
23:17:52 CAVA_Automata: theory CAVA_Automata.Step_Conv
23:17:52 CAVA_Automata: theory CAVA_Automata.Digraph
23:17:52 HOLCF: theory HOLCF.Bifinite
23:17:52 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.CauchysMeanTheorem
23:17:52 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl2
23:17:52 HOLCF: theory HOLCF.Domain_Aux
23:17:52 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl1
23:17:52 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian_Auxiliary
23:17:53 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Show_Poly
23:17:53 Markov_Models: theory Markov_Models.Coinductive_List
23:17:53 CAVA_Automata: theory CAVA_Automata.Automata
23:17:53 CAVA_Automata: theory CAVA_Automata.Digraph_Impl
23:17:53 HOLCF: theory HOLCF.Universal
23:17:53 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Is_Rat_To_Rat
23:17:54 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Log_Impl
23:17:54 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3
23:17:54 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl2
23:17:54 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.NthRoot_Impl
23:17:54 Abstract-Rewriting: theory Abstract-Rewriting.Equivalence_Checking
23:17:55 Abstract-Rewriting: theory Abstract-Rewriting.Regexp_Method
23:17:55 HOLCF: theory HOLCF.Algebraic
23:17:55 HOLCF: theory HOLCF.Compact_Basis
23:17:55 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Divmod_Int
23:17:55 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Sqrt_Babylonian
23:17:55 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Partial_Function_MR
23:17:55 HOLCF: theory HOLCF.LowerPD
23:17:55 HOLCF: theory HOLCF.UpperPD
23:17:55 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom
23:17:55 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric
23:17:56 HOLCF: theory HOLCF.Representable
23:17:56 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric
23:17:56 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl2
23:17:56 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3
23:17:56 HOLCF: theory HOLCF.ConvexPD
23:17:57 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3
23:17:57 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric
23:17:58 Abstract-Rewriting: theory Abstract-Rewriting.Seq
23:17:58 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Ring_Hom_Poly
23:17:58 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric
23:17:58 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
23:17:59 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric
23:17:59 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric
23:17:59 HOLCF: theory HOLCF.Domain
23:18:00 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Newton_Interpolation
23:18:00 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
23:18:01 HOLCF: theory HOLCF.Powerdomains
23:18:01 Markov_Models: theory Markov_Models.Coinductive_List_Prefix
23:18:01 Markov_Models: theory Markov_Models.Coinductive_Stream
23:18:01 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
23:18:02 HOLCF: theory HOLCF
23:18:02 Markov_Models: theory Markov_Models.Quotient_Coinductive_List
23:18:02 CAVA_Automata: theory CAVA_Automata.Lasso
23:18:02 Markov_Models: theory Markov_Models.TLList
23:18:04 Pre_Polynomial_Factorization: theory Pre_Polynomial_Factorization.Polynomial_Interpolation
23:18:04 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
23:18:04 CAVA_Automata: theory CAVA_Automata.Simulation
23:18:05 CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
23:18:06 Markov_Models: theory Markov_Models.Quotient_TLList
23:18:07 Markov_Models: theory Markov_Models.Coinductive
23:18:11 SPARCv8: theory SPARCv8.MMU
23:18:11 Timing Discrete_Summation (2 threads, 2.812s elapsed time, 5.424s cpu time, 0.124s GC time, factor 1.93)
23:18:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation
23:18:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation/document.pdf
23:18:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation/outline.pdf
23:18:11 Finished Discrete_Summation (0:00:31 elapsed time, 0:00:46 cpu time, factor 1.47)
23:18:12 Running AWN ...
23:18:13 SPARCv8: theory SPARCv8.Sparc_State
23:18:14 AWN: theory AWN.TransitionSystems
23:18:14 AWN: theory AWN.Lib
23:18:14 AWN: theory AWN.AWN
23:18:14 AWN: theory AWN.Invariants
23:18:15 AWN: theory AWN.OInvariants
23:18:17 SPARCv8: theory SPARCv8.Sparc_Instruction
23:18:19 CAVA_Automata: theory CAVA_Automata.Automata_Impl
23:18:22 SPARCv8: theory SPARCv8.Sparc_Execution
23:18:23 SPARCv8: theory SPARCv8.Sparc_Properties
23:18:27 AWN: theory AWN.AWN_Cterms
23:18:28 Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
23:18:29 Timing HOLCF (2 threads, 20.932s elapsed time, 38.776s cpu time, 2.136s GC time, factor 1.85)
23:18:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF
23:18:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/document.pdf
23:18:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/outline.pdf
23:18:29 Finished HOLCF (0:00:50 elapsed time, 0:01:23 cpu time, factor 1.67)
23:18:29 Building HOLCF-HOL-Library ...
23:18:31 AWN: theory AWN.AWN_Labels
23:18:31 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
23:18:31 Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
23:18:32 HOLCF-HOL-Library: theory HOLCF-HOL-Library.AList
23:18:32 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Cancellation
23:18:32 AWN: theory AWN.Inv_Cterms
23:18:33 AWN: theory AWN.AWN_SOS
23:18:33 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Multiset
23:18:33 Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
23:18:33 AWN: theory AWN.OAWN_SOS
23:18:34 HOLCF-HOL-Library: theory HOLCF-HOL-Library.FuncSet
23:18:35 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Infinite_Set
23:18:35 Markov_Models: theory Markov_Models.Crowds_Protocol
23:18:35 HOLCF-HOL-Library: theory HOLCF-HOL-Library.LaTeXsugar
23:18:35 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Syntax
23:18:35 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Option
23:18:35 Markov_Models: theory Markov_Models.Example_A
23:18:37 Markov_Models: theory Markov_Models.Example_B
23:18:37 AWN: theory AWN.AWN_SOS_Labels
23:18:37 Markov_Models: theory Markov_Models.Gossip_Broadcast
23:18:38 Markov_Models: theory Markov_Models.Markov_Decision_Process
23:18:38 AWN: theory AWN.AWN_Invariants
23:18:38 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Permutation
23:18:39 Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
23:18:39 AWN: theory AWN.Qmsg
23:18:40 Markov_Models: theory Markov_Models.Zeroconf_Analysis
23:18:40 AWN: theory AWN.Pnet
23:18:40 AWN: theory AWN.OAWN_Invariants
23:18:41 Markov_Models: theory Markov_Models.MDP_Reachability_Problem
23:18:41 AWN: theory AWN.Closed
23:18:41 AWN: theory AWN.OAWN_SOS_Labels
23:18:41 Markov_Models: theory Markov_Models.PGCL
23:18:42 AWN: theory AWN.ONode_Lifting
23:18:42 AWN: theory AWN.OAWN_Convert
23:18:42 Markov_Models: theory Markov_Models.MDP_RP_Certification
23:18:42 AWN: theory AWN.OPnet
23:18:43 AWN: theory AWN.Qmsg_Lifting
23:18:43 AWN: theory AWN.OPnet_Lifting
23:18:43 AWN: theory AWN.OClosed_Lifting
23:18:44 AWN: theory AWN.OClosed_Transfer
23:18:45 AWN: theory AWN.AWN_Main
23:18:45 AWN: theory AWN.Toy
23:18:46 Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
23:18:48 Markov_Models: theory Markov_Models.Markov_Models
23:18:48 Markov_Models: theory Markov_Models.PCTL
23:18:53 Timing Abstract-Rewriting (2 threads, 33.111s elapsed time, 58.716s cpu time, 3.036s GC time, factor 1.77)
23:18:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting
23:18:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/document.pdf
23:18:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/outline.pdf
23:18:53 Finished Abstract-Rewriting (0:01:14 elapsed time, 0:02:04 cpu time, factor 1.68)
23:18:54 Building Matrix ...
23:18:59 Timing Pre_Polynomial_Factorization (2 threads, 28.771s elapsed time, 59.116s cpu time, 2.344s GC time, factor 2.05)
23:18:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization
23:18:59 Finished Pre_Polynomial_Factorization (0:01:19 elapsed time, 0:02:12 cpu time, factor 1.66)
23:18:59 Building Polynomials ...
23:19:00 Matrix: theory Matrix.Congruence
23:19:01 Matrix: theory Matrix.Order
23:19:03 Matrix: theory Matrix.Lattice
23:19:04 Matrix: theory Matrix.Complete_Lattice
23:19:05 CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
23:19:05 Matrix: theory Matrix.Group
23:19:06 Polynomials: theory Polynomials.Utility
23:19:06 Polynomials: theory Polynomials.Power_Products
23:19:06 Polynomials: theory Polynomials.Polynomials
23:19:07 Matrix: theory Matrix.FiniteProduct
23:19:08 Matrix: theory Matrix.Ring
23:19:09 Timing HOLCF-HOL-Library (2 threads, 16.736s elapsed time, 31.728s cpu time, 1.480s GC time, factor 1.90)
23:19:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-HOL-Library
23:19:09 Finished HOLCF-HOL-Library (0:00:39 elapsed time, 0:01:05 cpu time, factor 1.66)
23:19:09 Building HOLCF-Nominal2 ...
23:19:10 Polynomials: theory Polynomials.Abstract_Poly
23:19:12 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Set
23:19:12 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Product
23:19:13 HOLCF-Nominal2: theory HOLCF-Nominal2.FSet
23:19:13 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_List
23:19:13 HOLCF-Nominal2: theory HOLCF-Nominal2.Phantom_Type
23:19:13 Polynomials: theory Polynomials.Poly_Lists
23:19:14 HOLCF-Nominal2: theory HOLCF-Nominal2.Cardinality
23:19:14 Polynomials: theory Polynomials.NZM
23:19:16 HOLCF-Nominal2: theory HOLCF-Nominal2.FinFun
23:19:19 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Base
23:19:25 HOLCF-Nominal2: theory HOLCF-Nominal2.Atoms
23:19:25 HOLCF-Nominal2: theory HOLCF-Nominal2.Eqvt
23:19:25 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Abs
23:19:28 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_FCB
23:19:28 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2
23:19:40 Matrix: theory Matrix.Ordered_Semiring
23:19:40 Matrix: theory Matrix.Utility
23:19:42 Matrix: theory Matrix.Matrix_Arith
23:19:43 Matrix: theory Matrix.Matrix_Comparison
23:19:45 Matrix: theory Matrix.Matrix
23:19:51 AWN: theory AWN.AWN_Term_Graph
23:19:56 Timing CAVA_Automata (2 threads, 74.662s elapsed time, 105.568s cpu time, 5.672s GC time, factor 1.41)
23:19:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_Automata
23:19:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_Automata/document.pdf
23:19:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_Automata/outline.pdf
23:19:56 Finished CAVA_Automata (0:02:16 elapsed time, 0:03:19 cpu time, factor 1.46)
23:19:56 Building LTL_to_GBA ...
23:20:00 Timing AWN (2 threads, 101.367s elapsed time, 195.156s cpu time, 7.320s GC time, factor 1.93)
23:20:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/AWN
23:20:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/AWN/document.pdf
23:20:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/AWN/outline.pdf
23:20:00 Finished AWN (0:01:47 elapsed time, 0:03:23 cpu time, factor 1.89)
23:20:00 Building HOLCF-Library ...
23:20:02 HOLCF-Library: theory HOLCF-Library.Infinite_Set
23:20:02 HOLCF-Library: theory HOLCF-Library.Bool_Discrete
23:20:02 HOLCF-Library: theory HOLCF-Library.Char_Discrete
23:20:03 HOLCF-Library: theory HOLCF-Library.Countable_Set
23:20:03 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite
23:20:03 Timing HOLCF-Nominal2 (2 threads, 27.194s elapsed time, 53.496s cpu time, 2.756s GC time, factor 1.97)
23:20:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Nominal2
23:20:03 Finished HOLCF-Nominal2 (0:00:53 elapsed time, 0:01:33 cpu time, factor 1.73)
23:20:03 Markov_Models: theory Markov_Models.MDP_RP
23:20:03 HOLCF-Library: theory HOLCF-Library.Countable_Complete_Lattices
23:20:04 Building Launchbury ...
23:20:04 HOLCF-Library: theory HOLCF-Library.Int_Discrete
23:20:04 HOLCF-Library: theory HOLCF-Library.List_Cpo
23:20:04 HOLCF-Library: theory HOLCF-Library.Nat_Discrete
23:20:05 HOLCF-Library: theory HOLCF-Library.Sum_Cpo
23:20:05 HOLCF-Library: theory HOLCF-Library.List_Predomain
23:20:06 HOLCF-Library: theory HOLCF-Library.Option_Cpo
23:20:06 HOLCF-Library: theory HOLCF-Library.Order_Continuity
23:20:07 HOLCF-Library: theory HOLCF-Library.HOL_Cpo
23:20:07 Launchbury: theory Launchbury.Nominal-Utils
23:20:07 Launchbury: theory Launchbury.Mono-Nat-Fun
23:20:07 Launchbury: theory Launchbury.Vars
23:20:07 Launchbury: theory Launchbury.C
23:20:07 HOLCF-Library: theory HOLCF-Library.Extended_Nat
23:20:08 Launchbury: theory Launchbury.HOLCF-Join
23:20:08 Launchbury: theory Launchbury.HOLCF-Join-Classes
23:20:08 Launchbury: theory Launchbury.CValue
23:20:09 HOLCF-Library: theory HOLCF-Library.Stream
23:20:09 Launchbury: theory Launchbury.HOLCF-Meet
23:20:09 Launchbury: theory Launchbury.Value
23:20:10 Launchbury: theory Launchbury.C-Meet
23:20:10 LTL_to_GBA: theory LTL_to_GBA.LTL
23:20:10 LTL_to_GBA: theory LTL_to_GBA.Samplers
23:20:10 Launchbury: theory Launchbury.AList-Utils
23:20:10 Launchbury: theory Launchbury.Env
23:20:10 LTL_to_GBA: theory LTL_to_GBA.StutterEquivalence
23:20:10 Launchbury: theory Launchbury.AList-Utils-Nominal
23:20:11 Timing Polynomials (2 threads, 29.333s elapsed time, 56.972s cpu time, 2.932s GC time, factor 1.94)
23:20:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomials
23:20:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomials/document.pdf
23:20:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomials/outline.pdf
23:20:11 Finished Polynomials (0:01:10 elapsed time, 0:01:58 cpu time, factor 1.67)
23:20:11 HOLCF-Library: theory HOLCF-Library.HOLCF_Library
23:20:11 Launchbury: theory Launchbury.Pointwise
23:20:11 Launchbury: theory Launchbury.HOLCF-Utils
23:20:11 Running DFS_Framework ...
23:20:11 Launchbury: theory Launchbury.Terms
23:20:11 Launchbury: theory Launchbury.C-restr
23:20:12 Launchbury: theory Launchbury.Env-HOLCF
23:20:12 Launchbury: theory Launchbury.Iterative
23:20:12 Launchbury: theory Launchbury.EvalHeap
23:20:14 Launchbury: theory Launchbury.Nominal-HOLCF
23:20:16 Timing Markov_Models (2 threads, 136.714s elapsed time, 255.668s cpu time, 12.200s GC time, factor 1.87)
23:20:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models
23:20:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models/document.pdf
23:20:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Markov_Models/outline.pdf
23:20:16 Finished Markov_Models (0:02:36 elapsed time, 0:04:45 cpu time, factor 1.82)
23:20:16 Running Gabow_SCC ...
23:20:16 Launchbury: theory Launchbury.CValue-Nominal
23:20:17 Launchbury: theory Launchbury.Env-Nominal
23:20:18 Launchbury: theory Launchbury.HasESem
23:20:19 Launchbury: theory Launchbury.HeapSemantics
23:20:19 Launchbury: theory Launchbury.Substitution
23:20:19 LTL_to_GBA: theory LTL_to_GBA.PLTL
23:20:20 Launchbury: theory Launchbury.AbstractDenotational
23:20:20 Launchbury: theory Launchbury.Launchbury
23:20:22 Launchbury: theory Launchbury.Abstract-Denotational-Props
23:20:22 Launchbury: theory Launchbury.ResourcedDenotational
23:20:23 Launchbury: theory Launchbury.Value-Nominal
23:20:23 Launchbury: theory Launchbury.CorrectnessResourced
23:20:23 Launchbury: theory Launchbury.Denotational
23:20:24 LTL_to_GBA: theory LTL_to_GBA.Countable_Set
23:20:24 LTL_to_GBA: theory LTL_to_GBA.LTL_Stutter
23:20:24 Launchbury: theory Launchbury.ResourcedAdequacy
23:20:24 Launchbury: theory Launchbury.CorrectnessOriginal
23:20:24 Launchbury: theory Launchbury.ValueSimilarity
23:20:24 LTL_to_GBA: theory LTL_to_GBA.Countable_Complete_Lattices
23:20:25 DFS_Framework: theory DFS_Framework.DFS_Framework_Misc
23:20:25 DFS_Framework: theory DFS_Framework.On_Stack
23:20:25 DFS_Framework: theory DFS_Framework.DFS_Framework_Refine_Aux
23:20:25 Launchbury: theory Launchbury.Denotational-Related
23:20:25 DFS_Framework: theory DFS_Framework.Impl_Rev_Array_Stack
23:20:26 Launchbury: theory Launchbury.Adequacy
23:20:27 Launchbury: theory Launchbury.EverythingAdequacy
23:20:27 DFS_Framework: theory DFS_Framework.DFS_Chapter_Framework
23:20:27 DFS_Framework: theory DFS_Framework.DFS_Chapter_Examples
23:20:28 DFS_Framework: theory DFS_Framework.Param_DFS
23:20:28 LTL_to_GBA: theory LTL_to_GBA.Order_Continuity
23:20:29 LTL_to_GBA: theory LTL_to_GBA.Extended_Nat
23:20:30 LTL_to_GBA: theory LTL_to_GBA.LTL_Rewrite
23:20:30 Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton
23:20:30 Gabow_SCC: theory Gabow_SCC.Find_Path
23:20:30 Gabow_SCC: theory Gabow_SCC.Find_Path_Impl
23:20:32 Timing Matrix (2 threads, 58.714s elapsed time, 107.832s cpu time, 4.092s GC time, factor 1.84)
23:20:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix
23:20:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix/document.pdf
23:20:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix/outline.pdf
23:20:32 Finished Matrix (0:01:38 elapsed time, 0:02:45 cpu time, factor 1.69)
23:20:32 Building Matrix_Tensor ...
23:20:34 DFS_Framework: theory DFS_Framework.DFS_Invars_Basic
23:20:34 DFS_Framework: theory DFS_Framework.General_DFS_Structure
23:20:35 Gabow_SCC: theory Gabow_SCC.Gabow_SCC
23:20:35 LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA
23:20:36 DFS_Framework: theory DFS_Framework.DFS_Invars_SCC
23:20:36 Gabow_SCC: theory Gabow_SCC.Gabow_GBG
23:20:37 Timing HOLCF-Library (2 threads, 16.376s elapsed time, 30.100s cpu time, 1.048s GC time, factor 1.84)
23:20:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF-Library
23:20:37 Finished HOLCF-Library (0:00:37 elapsed time, 0:01:00 cpu time, factor 1.64)
23:20:37 Running Abs_Int_ITP2012 ...
23:20:39 Matrix_Tensor: theory Matrix_Tensor.Matrix_Tensor
23:20:41 DFS_Framework: theory DFS_Framework.Rec_Impl
23:20:41 DFS_Framework: theory DFS_Framework.Tailrec_Impl
23:20:43 Abs_Int_ITP2012: theory Abs_Int_ITP2012.AExp
23:20:44 Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton_Code
23:20:45 Abs_Int_ITP2012: theory Abs_Int_ITP2012.BExp
23:20:46 LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA_impl
23:20:47 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Com
23:20:47 DFS_Framework: theory DFS_Framework.Simple_Impl
23:20:48 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Vars
23:20:50 Abs_Int_ITP2012: theory Abs_Int_ITP2012.ACom
23:20:50 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int_Tests
23:20:50 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Complete_Lattice_ix
23:20:53 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Collecting
23:20:53 DFS_Framework: theory DFS_Framework.Restr_Impl
23:20:55 DFS_Framework: theory DFS_Framework.DFS_Framework
23:20:56 DFS_Framework: theory DFS_Framework.Cyc_Check
23:20:57 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int0
23:21:02 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_State
23:21:02 DFS_Framework: theory DFS_Framework.DFS_Find_Path
23:21:03 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int1
23:21:04 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int2
23:21:07 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int2_ivl
23:21:09 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int3
23:21:16 Gabow_SCC: theory Gabow_SCC.Gabow_GBG_Code
23:21:19 Gabow_SCC: theory Gabow_SCC.Gabow_SCC_Code
23:21:35 Timing Launchbury (2 threads, 53.381s elapsed time, 96.120s cpu time, 3.200s GC time, factor 1.80)
23:21:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury
23:21:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/document.pdf
23:21:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/outline.pdf
23:21:35 Finished Launchbury (0:01:31 elapsed time, 0:02:34 cpu time, factor 1.68)
23:21:36 Running Call_Arity ...
23:21:38 Timing Matrix_Tensor (2 threads, 32.113s elapsed time, 62.852s cpu time, 2.728s GC time, factor 1.96)
23:21:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix_Tensor
23:21:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix_Tensor/document.pdf
23:21:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix_Tensor/outline.pdf
23:21:38 Finished Matrix_Tensor (0:01:05 elapsed time, 0:01:49 cpu time, factor 1.67)
23:21:39 Running Knot_Theory ...
23:21:40 Call_Arity: theory Call_Arity.BalancedTraces
23:21:40 Call_Arity: theory Call_Arity.ConstOn
23:21:41 Call_Arity: theory Call_Arity.List-Interleavings
23:21:41 Call_Arity: theory Call_Arity.Set-Cpo
23:21:41 Call_Arity: theory Call_Arity.Arity
23:21:41 Call_Arity: theory Call_Arity.TTree
23:21:41 Call_Arity: theory Call_Arity.EtaExpansion
23:21:41 Call_Arity: theory Call_Arity.SestoftConf
23:21:43 Call_Arity: theory Call_Arity.AEnv
23:21:44 Call_Arity: theory Call_Arity.ArityStack
23:21:44 Call_Arity: theory Call_Arity.Sestoft
23:21:44 Call_Arity: theory Call_Arity.EtaExpansionSafe
23:21:44 Call_Arity: theory Call_Arity.SestoftGC
23:21:45 Call_Arity: theory Call_Arity.SestoftCorrect
23:21:45 Call_Arity: theory Call_Arity.Env-Set-Cpo
23:21:45 Call_Arity: theory Call_Arity.AList-Utils-HOLCF
23:21:46 Call_Arity: theory Call_Arity.AnalBinds
23:21:46 Knot_Theory: theory Knot_Theory.Fraction_Field
23:21:46 Knot_Theory: theory Knot_Theory.Polynomial
23:21:46 Call_Arity: theory Call_Arity.Cardinality-Domain
23:21:46 Call_Arity: theory Call_Arity.CardinalityAnalysisSig
23:21:48 Call_Arity: theory Call_Arity.CoCallGraph
23:21:48 Call_Arity: theory Call_Arity.TTree-HOLCF
23:21:49 Call_Arity: theory Call_Arity.TTreeAnalysisSig
23:21:50 Call_Arity: theory Call_Arity.CoCallAnalysisSig
23:21:50 Call_Arity: theory Call_Arity.CoCallGraph-TTree
23:21:51 Call_Arity: theory Call_Arity.Arity-Nominal
23:21:51 Call_Arity: theory Call_Arity.Cardinality-Domain-Lists
23:21:52 Call_Arity: theory Call_Arity.ArityAnalysisSig
23:21:54 Call_Arity: theory Call_Arity.ArityAnalysisAbinds
23:21:54 Call_Arity: theory Call_Arity.ArityAnalysisStack
23:21:54 Call_Arity: theory Call_Arity.ArityAnalysisSpec
23:21:55 Call_Arity: theory Call_Arity.CardinalityAnalysisSpec
23:21:55 Call_Arity: theory Call_Arity.ArityAnalysisFix
23:21:55 Call_Arity: theory Call_Arity.ArityAnalysisFixProps
23:21:55 Call_Arity: theory Call_Arity.ArityConsistent
23:21:56 Call_Arity: theory Call_Arity.NoCardinalityAnalysis
23:21:57 Call_Arity: theory Call_Arity.CoCallAritySig
23:21:57 Call_Arity: theory Call_Arity.TTreeAnalysisSpec
23:21:57 Call_Arity: theory Call_Arity.CoCallAnalysisSpec
23:21:58 Call_Arity: theory Call_Arity.CoCallImplTTree
23:21:58 Call_Arity: theory Call_Arity.TTreeImplCardinality
23:21:59 Knot_Theory: theory Knot_Theory.Tangle_Relation
23:21:59 Knot_Theory: theory Knot_Theory.Preliminaries
23:21:59 Call_Arity: theory Call_Arity.CoCallImplTTreeSafe
23:22:00 Call_Arity: theory Call_Arity.TTreeImplCardinalitySafe
23:22:00 Call_Arity: theory Call_Arity.CoCallGraph-Nominal
23:22:01 Knot_Theory: theory Knot_Theory.Tangles
23:22:01 Call_Arity: theory Call_Arity.CoCallAnalysisBinds
23:22:01 Call_Arity: theory Call_Arity.TransformTools
23:22:01 Knot_Theory: theory Knot_Theory.Tangle_Algebra
23:22:02 Knot_Theory: theory Knot_Theory.Tangle_Moves
23:22:02 Call_Arity: theory Call_Arity.AbstractTransform
23:22:03 Call_Arity: theory Call_Arity.ArityEtaExpansion
23:22:03 Knot_Theory: theory Knot_Theory.Link_Algebra
23:22:04 Call_Arity: theory Call_Arity.ArityEtaExpansionSafe
23:22:04 Call_Arity: theory Call_Arity.CoCallFix
23:22:04 Knot_Theory: theory Knot_Theory.Example
23:22:04 Knot_Theory: theory Knot_Theory.Kauffman_Matrix
23:22:05 DFS_Framework: theory DFS_Framework.Nested_DFS
23:22:05 Call_Arity: theory Call_Arity.ArityTransform
23:22:06 Call_Arity: theory Call_Arity.CoCallAnalysisImpl
23:22:06 Call_Arity: theory Call_Arity.ArityTransformSafe
23:22:08 Knot_Theory: theory Knot_Theory.Computations
23:22:08 Call_Arity: theory Call_Arity.CardArityTransformSafe
23:22:08 Knot_Theory: theory Knot_Theory.Linkrel_Kauffman
23:22:08 Call_Arity: theory Call_Arity.CallArityEnd2End
23:22:09 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int1_parity
23:22:09 Abs_Int_ITP2012: theory Abs_Int_ITP2012.Abs_Int1_const
23:22:09 Knot_Theory: theory Knot_Theory.Kauffman_Invariance
23:22:09 Knot_Theory: theory Knot_Theory.Knot_Theory
23:22:10 Call_Arity: theory Call_Arity.CoCallImplSafe
23:22:11 Call_Arity: theory Call_Arity.TrivialArityAnal
23:22:11 Call_Arity: theory Call_Arity.CallArityEnd2EndSafe
23:22:11 Call_Arity: theory Call_Arity.ArityAnalysisCorrDenotational
23:22:20 SPARCv8: theory SPARCv8.Sparc_Init_State
23:22:20 SPARCv8: theory SPARCv8.Sparc_Code_Gen
23:22:20 Timing Abs_Int_ITP2012 (2 threads, 94.345s elapsed time, 181.232s cpu time, 5.860s GC time, factor 1.92)
23:22:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abs_Int_ITP2012
23:22:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abs_Int_ITP2012/document.pdf
23:22:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abs_Int_ITP2012/outline.pdf
23:22:20 Finished Abs_Int_ITP2012 (0:01:42 elapsed time, 0:03:10 cpu time, factor 1.86)
23:22:20 Running Vickrey_Clarke_Groves ...
23:22:25 DFS_Framework: theory DFS_Framework.Reachable_Nodes
23:22:26 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Argmax
23:22:26 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.SetUtils
23:22:26 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Partitions
23:22:26 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationOperators
23:22:27 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationProperties
23:22:27 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.MiscTools
23:22:30 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.StrictCombinatorialAuction
23:22:31 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Universes
23:22:33 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.UniformTieBreaking
23:22:34 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuction
23:22:35 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction
23:22:41 Timing SPARCv8 (2 threads, 287.771s elapsed time, 537.304s cpu time, 12.172s GC time, factor 1.87)
23:22:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8
23:22:41 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8/document.pdf
23:22:41 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SPARCv8/outline.pdf
23:22:41 Finished SPARCv8 (0:05:01 elapsed time, 0:09:14 cpu time, factor 1.84)
23:22:41 Running Polynomial_Factorization ...
23:22:52 DFS_Framework: theory DFS_Framework.Tarjan_LowLink
23:22:52 Gabow_SCC: theory Gabow_SCC.All_Of_Gabow_SCC
23:22:53 DFS_Framework: theory DFS_Framework.Tarjan
23:22:55 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset
23:22:55 Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial
23:22:55 Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility
23:22:55 Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
23:22:55 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial
23:22:56 Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots
23:22:56 Polynomial_Factorization: theory Polynomial_Factorization.Precomputation
23:22:56 Polynomial_Factorization: theory Polynomial_Factorization.Missing_List
23:22:56 Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly
23:22:57 Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization
23:22:57 Timing Gabow_SCC (2 threads, 143.363s elapsed time, 274.024s cpu time, 8.856s GC time, factor 1.91)
23:22:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gabow_SCC
23:22:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gabow_SCC/document.pdf
23:22:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gabow_SCC/outline.pdf
23:22:57 Finished Gabow_SCC (0:02:40 elapsed time, 0:05:10 cpu time, factor 1.93)
23:22:57 Running Circus ...
23:22:58 Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma
23:22:58 Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization
23:22:59 Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly
23:23:00 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test
23:23:00 Circus: theory Circus.Sublist
23:23:00 Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization
23:23:02 Circus: theory Circus.Var_list
23:23:02 Circus: theory Circus.Var
23:23:02 Circus: theory Circus.Relations
23:23:03 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization
23:23:04 Circus: theory Circus.Designs
23:23:05 Circus: theory Circus.Reactive_Processes
23:23:08 Circus: theory Circus.CSP_Processes
23:23:09 Circus: theory Circus.Circus_Actions
23:23:09 Circus: theory Circus.Denotational_Semantics
23:23:12 Timing Call_Arity (2 threads, 85.274s elapsed time, 160.828s cpu time, 8.472s GC time, factor 1.89)
23:23:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity
23:23:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/document.pdf
23:23:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/outline.pdf
23:23:12 Finished Call_Arity (0:01:35 elapsed time, 0:02:54 cpu time, factor 1.82)
23:23:12 Running PCF ...
23:23:15 DFS_Framework: theory DFS_Framework.Feedback_Arcs
23:23:15 PCF: theory PCF.Product_Plus
23:23:15 PCF: theory PCF.Dual_Lattice
23:23:15 PCF: theory PCF.Product_Order
23:23:16 PCF: theory PCF.Basis
23:23:18 PCF: theory PCF.Logical_Relations
23:23:19 PCF: theory PCF.PCF
23:23:22 Timing Knot_Theory (2 threads, 92.547s elapsed time, 178.492s cpu time, 5.224s GC time, factor 1.93)
23:23:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory
23:23:22 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory/document.pdf
23:23:22 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory/outline.pdf
23:23:22 Finished Knot_Theory (0:01:42 elapsed time, 0:03:09 cpu time, factor 1.84)
23:23:22 Running LightweightJava ...
23:23:24 PCF: theory PCF.Continuations
23:23:24 PCF: theory PCF.OpSem
23:23:25 Circus: theory Circus.Circus_Syntax
23:23:25 Circus: theory Circus.Refinement
23:23:26 Circus: theory Circus.Refinement_Example
23:23:27 LightweightJava: theory LightweightJava.Lightweight_Java_Definition
23:23:39 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples
23:23:39 Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.FirstPrice
23:23:41 LightweightJava: theory LightweightJava.Lightweight_Java_Equivalence
23:23:42 LightweightJava: theory LightweightJava.Lightweight_Java_Proof
23:23:47 Timing Polynomial_Factorization (2 threads, 48.833s elapsed time, 75.036s cpu time, 2.120s GC time, factor 1.54)
23:23:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization
23:23:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf
23:23:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf
23:23:47 Finished Polynomial_Factorization (0:01:06 elapsed time, 0:01:33 cpu time, factor 1.42)
23:23:48 Running Decreasing-Diagrams-II ...
23:23:54 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Order_Union
23:23:54 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Infinite_Sequences
23:23:54 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Least_Enum
23:23:54 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Restricted_Predicates
23:23:54 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Wellorder_Extension
23:23:55 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Minimal_Elements
23:23:55 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Multiset_Extension
23:23:55 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Almost_Full
23:23:57 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Minimal_Bad_Sequences
23:23:57 DFS_Framework: theory DFS_Framework.DFS_All_Examples
23:23:57 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Almost_Full_Relations
23:23:58 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Well_Quasi_Orders
23:24:05 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux
23:24:06 Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II
23:24:08 Timing PCF (2 threads, 50.406s elapsed time, 96.572s cpu time, 2.812s GC time, factor 1.92)
23:24:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF
23:24:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF/document.pdf
23:24:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/PCF/outline.pdf
23:24:08 Finished PCF (0:00:55 elapsed time, 0:01:42 cpu time, factor 1.85)
23:24:08 Running Bernoulli ...
23:24:12 Timing Circus (2 threads, 52.214s elapsed time, 100.268s cpu time, 3.416s GC time, factor 1.92)
23:24:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus
23:24:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus/document.pdf
23:24:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Circus/outline.pdf
23:24:12 Finished Circus (0:01:14 elapsed time, 0:02:20 cpu time, factor 1.88)
23:24:12 Running Groebner_Bases ...
23:24:15 Bernoulli: theory Bernoulli.Bernoulli
23:24:15 Bernoulli: theory Bernoulli.Bernoulli_FPS
23:24:15 Bernoulli: theory Bernoulli.Periodic_Bernpoly
23:24:18 Timing Vickrey_Clarke_Groves (2 threads, 108.025s elapsed time, 207.384s cpu time, 5.540s GC time, factor 1.92)
23:24:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves
23:24:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves/document.pdf
23:24:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves/outline.pdf
23:24:19 Finished Vickrey_Clarke_Groves (0:01:57 elapsed time, 0:03:38 cpu time, factor 1.86)
23:24:19 Running Decreasing-Diagrams ...
23:24:19 Groebner_Bases: theory Groebner_Bases.Confluence
23:24:19 Timing LightweightJava (2 threads, 49.852s elapsed time, 84.884s cpu time, 3.384s GC time, factor 1.70)
23:24:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava
23:24:19 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava/document.pdf
23:24:19 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava/outline.pdf
23:24:19 Finished LightweightJava (0:00:56 elapsed time, 0:01:32 cpu time, factor 1.62)
23:24:19 Running Shivers-CFA ...
23:24:20 Groebner_Bases: theory Groebner_Bases.Groebner_Bases
23:24:22 Shivers-CFA: theory Shivers-CFA.Adhoc_Overloading
23:24:22 Shivers-CFA: theory Shivers-CFA.FixTransform
23:24:22 Shivers-CFA: theory Shivers-CFA.HOLCFUtils
23:24:22 Shivers-CFA: theory Shivers-CFA.CPSScheme
23:24:22 Shivers-CFA: theory Shivers-CFA.Computability
23:24:22 Shivers-CFA: theory Shivers-CFA.SetMap
23:24:23 Shivers-CFA: theory Shivers-CFA.Utils
23:24:23 Shivers-CFA: theory Shivers-CFA.MapSets
23:24:23 Groebner_Bases: theory Groebner_Bases.Computations
23:24:23 LTL_to_GBA: theory LTL_to_GBA.All_Of_LTL_to_GBA
23:24:23 Timing Decreasing-Diagrams-II (2 threads, 27.250s elapsed time, 45.416s cpu time, 1.524s GC time, factor 1.67)
23:24:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams-II
23:24:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams-II/document.pdf
23:24:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams-II/outline.pdf
23:24:23 Finished Decreasing-Diagrams-II (0:00:35 elapsed time, 0:00:54 cpu time, factor 1.53)
23:24:23 Running Trie ...
23:24:24 Decreasing-Diagrams: theory Decreasing-Diagrams.Decreasing_Diagrams
23:24:24 Timing Bernoulli (2 threads, 7.447s elapsed time, 14.508s cpu time, 0.376s GC time, factor 1.95)
23:24:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli
23:24:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli/document.pdf
23:24:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli/outline.pdf
23:24:24 Finished Bernoulli (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.48)
23:24:25 Running Card_Number_Partitions ...
23:24:29 Trie: theory Trie.Trie
23:24:30 Card_Number_Partitions: theory Card_Number_Partitions.Additions_to_Main
23:24:30 Card_Number_Partitions: theory Card_Number_Partitions.Number_Partition
23:24:30 Card_Number_Partitions: theory Card_Number_Partitions.Card_Number_Partitions
23:24:31 Trie: theory Trie.Tries
23:24:32 Shivers-CFA: theory Shivers-CFA.CPSUtils
23:24:34 Shivers-CFA: theory Shivers-CFA.Eval
23:24:36 Shivers-CFA: theory Shivers-CFA.AbsCF
23:24:37 Shivers-CFA: theory Shivers-CFA.ExCF
23:24:38 Timing Card_Number_Partitions (2 threads, 5.786s elapsed time, 11.632s cpu time, 0.196s GC time, factor 2.01)
23:24:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Number_Partitions
23:24:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Number_Partitions/document.pdf
23:24:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Number_Partitions/outline.pdf
23:24:38 Finished Card_Number_Partitions (0:00:13 elapsed time, 0:00:19 cpu time, factor 1.49)
23:24:38 Running Integration ...
23:24:39 Shivers-CFA: theory Shivers-CFA.ExCFSV
23:24:40 Shivers-CFA: theory Shivers-CFA.AbsCFComp
23:24:40 Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
23:24:44 Integration: theory Integration.MonConv
23:24:44 Integration: theory Integration.Sigma_Algebra
23:24:44 Integration: theory Integration.Measure
23:24:45 Integration: theory Integration.RealRandVar
23:24:46 Integration: theory Integration.Failure
23:24:46 Integration: theory Integration.Integral
23:24:51 Timing Decreasing-Diagrams (2 threads, 23.810s elapsed time, 41.788s cpu time, 1.300s GC time, factor 1.76)
23:24:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams
23:24:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams/document.pdf
23:24:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Decreasing-Diagrams/outline.pdf
23:24:51 Finished Decreasing-Diagrams (0:00:32 elapsed time, 0:00:51 cpu time, factor 1.58)
23:24:51 Running WorkerWrapper ...
23:24:53 WorkerWrapper: theory WorkerWrapper.Nats
23:24:53 WorkerWrapper: theory WorkerWrapper.Maybe
23:24:55 WorkerWrapper: theory WorkerWrapper.LList
23:24:55 Timing Trie (2 threads, 23.776s elapsed time, 26.340s cpu time, 1.036s GC time, factor 1.11)
23:24:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Trie
23:24:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Trie/document.pdf
23:24:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Trie/outline.pdf
23:24:55 Finished Trie (0:00:31 elapsed time, 0:00:34 cpu time, factor 1.10)
23:24:55 Running Stream-Fusion ...
23:24:57 WorkerWrapper: theory WorkerWrapper.FixedPointTheorems
23:24:57 WorkerWrapper: theory WorkerWrapper.WorkerWrapper
23:24:57 WorkerWrapper: theory WorkerWrapper.CounterExample
23:24:57 WorkerWrapper: theory WorkerWrapper.Last
23:24:57 Stream-Fusion: theory Stream-Fusion.Int_Discrete
23:24:57 Timing Groebner_Bases (2 threads, 35.093s elapsed time, 68.604s cpu time, 2.396s GC time, factor 1.95)
23:24:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Groebner_Bases
23:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Groebner_Bases/document.pdf
23:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Groebner_Bases/outline.pdf
23:24:57 Finished Groebner_Bases (0:00:44 elapsed time, 0:01:19 cpu time, factor 1.77)
23:24:57 Timing Shivers-CFA (2 threads, 31.021s elapsed time, 61.772s cpu time, 2.744s GC time, factor 1.99)
23:24:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA
23:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document.pdf
23:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/outline.pdf
23:24:57 Finished Shivers-CFA (0:00:37 elapsed time, 0:01:10 cpu time, factor 1.87)
23:24:58 Stream-Fusion: theory Stream-Fusion.LazyList
23:24:58 WorkerWrapper: theory WorkerWrapper.Streams
23:24:58 Running Tycon ...
23:24:58 Running Card_Partitions ...
23:24:58 WorkerWrapper: theory WorkerWrapper.WorkerWrapperNew
23:24:58 WorkerWrapper: theory WorkerWrapper.Accumulator
23:24:59 WorkerWrapper: theory WorkerWrapper.Backtracking
23:24:59 Timing Integration (2 threads, 11.937s elapsed time, 23.424s cpu time, 0.752s GC time, factor 1.96)
23:24:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Integration
23:24:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Integration/document.pdf
23:24:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Integration/outline.pdf
23:24:59 Finished Integration (0:00:20 elapsed time, 0:00:32 cpu time, factor 1.62)
23:24:59 Running Proof_Strategy_Language ...
23:24:59 Stream-Fusion: theory Stream-Fusion.Stream
23:24:59 WorkerWrapper: theory WorkerWrapper.Continuations
23:25:00 Tycon: theory Tycon.TypeApp
23:25:00 Tycon: theory Tycon.Coerce
23:25:01 Tycon: theory Tycon.Functor
23:25:01 Proof_Strategy_Language: theory Proof_Strategy_Language.Try_Hard
23:25:01 Proof_Strategy_Language: theory Proof_Strategy_Language.Eisbach
23:25:01 Stream-Fusion: theory Stream-Fusion.StreamFusion
23:25:01 Proof_Strategy_Language: theory Proof_Strategy_Language.PSL
23:25:01 Proof_Strategy_Language: theory Proof_Strategy_Language.Example
23:25:02 Tycon: theory Tycon.Monad
23:25:02 WorkerWrapper: theory WorkerWrapper.Nub
23:25:02 Tycon: theory Tycon.Binary_Tree_Monad
23:25:02 Tycon: theory Tycon.Lift_Monad
23:25:03 WorkerWrapper: theory WorkerWrapper.UnboxedNats
23:25:03 Tycon: theory Tycon.Monad_Plus
23:25:03 Tycon: theory Tycon.Monad_Zero
23:25:03 Card_Partitions: theory Card_Partitions.Card_Partitions
23:25:04 Tycon: theory Tycon.Error_Monad
23:25:04 Tycon: theory Tycon.Resumption_Transformer
23:25:04 Tycon: theory Tycon.Error_Transformer
23:25:05 Tycon: theory Tycon.Monad_Zero_Plus
23:25:05 Tycon: theory Tycon.Writer_Monad
23:25:05 Tycon: theory Tycon.Lazy_List_Monad
23:25:06 Timing DFS_Framework (2 threads, 276.187s elapsed time, 497.232s cpu time, 19.672s GC time, factor 1.80)
23:25:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/DFS_Framework
23:25:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/DFS_Framework/document.pdf
23:25:06 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/DFS_Framework/outline.pdf
23:25:06 Finished DFS_Framework (0:04:54 elapsed time, 0:09:33 cpu time, factor 1.95)
23:25:06 Tycon: theory Tycon.Maybe_Monad
23:25:06 Tycon: theory Tycon.State_Transformer
23:25:07 Tycon: theory Tycon.Writer_Transformer
23:25:08 Tycon: theory Tycon.Monad_Transformer
23:25:09 Timing WorkerWrapper (2 threads, 12.751s elapsed time, 23.976s cpu time, 0.988s GC time, factor 1.88)
23:25:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper
23:25:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper/document.pdf
23:25:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/WorkerWrapper/outline.pdf
23:25:09 Finished WorkerWrapper (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.70)
23:25:10 Timing Stream-Fusion (2 threads, 10.528s elapsed time, 14.176s cpu time, 0.552s GC time, factor 1.35)
23:25:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion
23:25:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion/document.pdf
23:25:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stream-Fusion/outline.pdf
23:25:10 Finished Stream-Fusion (0:00:14 elapsed time, 0:00:19 cpu time, factor 1.29)
23:25:10 Timing Card_Partitions (2 threads, 5.168s elapsed time, 8.412s cpu time, 0.100s GC time, factor 1.63)
23:25:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Partitions
23:25:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Partitions/document.pdf
23:25:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Card_Partitions/outline.pdf
23:25:10 Finished Card_Partitions (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.30)
23:25:13 Timing Tycon (2 threads, 10.598s elapsed time, 19.816s cpu time, 0.684s GC time, factor 1.87)
23:25:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon
23:25:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon/document.pdf
23:25:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tycon/outline.pdf
23:25:13 Finished Tycon (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.67)
23:25:34 Timing LTL_to_GBA (2 threads, 259.527s elapsed time, 496.420s cpu time, 16.960s GC time, factor 1.91)
23:25:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL_to_GBA
23:25:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL_to_GBA/document.pdf
23:25:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL_to_GBA/outline.pdf
23:25:34 Finished LTL_to_GBA (0:05:38 elapsed time, 0:10:17 cpu time, factor 1.83)
23:25:35 Building CAVA_buildchain1 ...
23:25:35 Running Promela ...
23:25:43 Timing Key_Agreement_Strong_Adversaries (2 threads, 476.269s elapsed time, 759.456s cpu time, 8.432s GC time, factor 1.59)
23:25:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries
23:25:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/document.pdf
23:25:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/outline.pdf
23:25:43 Finished Key_Agreement_Strong_Adversaries (0:08:03 elapsed time, 0:12:50 cpu time, factor 1.59)
23:25:45 Timing Proof_Strategy_Language (2 threads, 42.020s elapsed time, 73.696s cpu time, 1.976s GC time, factor 1.75)
23:25:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Proof_Strategy_Language
23:25:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Proof_Strategy_Language/document.pdf
23:25:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Proof_Strategy_Language/outline.pdf
23:25:45 Finished Proof_Strategy_Language (0:00:45 elapsed time, 0:01:22 cpu time, factor 1.81)
23:25:51 Promela: theory Promela.IArray
23:25:51 Promela: theory Promela.PromelaStatistics
23:25:52 CAVA_buildchain1: theory CAVA_buildchain1.Find_Path
23:25:52 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_Skeleton
23:25:52 CAVA_buildchain1: theory CAVA_buildchain1.Find_Path_Impl
23:25:53 Promela: theory Promela.Lexord_List
23:25:53 Promela: theory Promela.PromelaAST
23:25:56 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_SCC
23:25:58 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_GBG
23:26:04 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_Skeleton_Code
23:26:12 Promela: theory Promela.PromelaDatastructures
23:26:34 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_GBG_Code
23:26:37 CAVA_buildchain1: theory CAVA_buildchain1.Gabow_SCC_Code
23:27:29 Promela: theory Promela.PromelaInvariants
23:27:31 Promela: theory Promela.Promela
23:27:50 CAVA_buildchain1: theory CAVA_buildchain1.All_Of_Gabow_SCC
23:28:21 Promela: theory Promela.PromelaLTL
23:28:29 Promela: theory Promela.PromelaLTLConv
23:28:35 Promela: theory Promela.All_Of_Promela
23:28:39 Timing Promela (2 threads, 164.762s elapsed time, 274.152s cpu time, 15.956s GC time, factor 1.66)
23:28:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Promela
23:28:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Promela/document.pdf
23:28:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Promela/outline.pdf
23:28:39 Finished Promela (0:03:04 elapsed time, 0:05:10 cpu time, factor 1.69)
23:28:58 Timing CAVA_buildchain1 (2 threads, 133.323s elapsed time, 258.204s cpu time, 10.408s GC time, factor 1.94)
23:28:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_buildchain1
23:28:58 Finished CAVA_buildchain1 (0:03:22 elapsed time, 0:06:23 cpu time, factor 1.89)
23:28:58 Building CAVA_buildchain3 ...
23:29:15 CAVA_buildchain3: theory CAVA_buildchain3.IArray
23:29:15 CAVA_buildchain3: theory CAVA_buildchain3.Lexord_List
23:29:16 CAVA_buildchain3: theory CAVA_buildchain3.PromelaAST
23:29:17 CAVA_buildchain3: theory CAVA_buildchain3.PromelaStatistics
23:29:35 CAVA_buildchain3: theory CAVA_buildchain3.PromelaDatastructures
23:30:51 CAVA_buildchain3: theory CAVA_buildchain3.PromelaInvariants
23:30:53 CAVA_buildchain3: theory CAVA_buildchain3.Promela
23:31:43 CAVA_buildchain3: theory CAVA_buildchain3.PromelaLTL
23:31:51 CAVA_buildchain3: theory CAVA_buildchain3.PromelaLTLConv
23:31:57 CAVA_buildchain3: theory CAVA_buildchain3.All_Of_Promela
23:33:41 Timing CAVA_buildchain3 (2 threads, 162.848s elapsed time, 273.048s cpu time, 16.576s GC time, factor 1.68)
23:33:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_buildchain3
23:33:41 Finished CAVA_buildchain3 (0:04:42 elapsed time, 0:07:52 cpu time, factor 1.67)
23:33:42 Running CAVA_LTL_Modelchecker ...
23:34:06 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
23:34:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI
23:35:50 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract
23:35:52 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.Mapping
23:35:53 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.AList_Mapping
23:35:54 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs
23:36:04 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras
23:36:06 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
23:36:06 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
23:36:07 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
23:36:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
23:36:08 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple
23:36:09 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs
23:36:10 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl
23:38:06 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
23:38:07 CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
23:38:15 Timing CAVA_LTL_Modelchecker (2 threads, 246.542s elapsed time, 258.964s cpu time, 8.984s GC time, factor 1.05)
23:38:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker
23:38:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker/document.pdf
23:38:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker/outline.pdf
23:38:15 Finished CAVA_LTL_Modelchecker (0:04:32 elapsed time, 0:06:09 cpu time, factor 1.35)
23:38:16 
23:38:16 === TIMING ===
23:38:16 
23:38:16 Group AFP: 1:15:36 elapsed time, 2:10:03 cpu time, factor 1.72
23:38:16 Group main: 0:00:50 elapsed time, 0:01:23 cpu time, factor 1.67
23:38:16 Group timing: 0:00:50 elapsed time, 0:01:23 cpu time, factor 1.67
23:38:16 Overall: 0:21:07 elapsed time, 2:12:27 cpu time, factor 6.27
23:38:16 
23:38:16 === SITEGEN ===
23:38:16 
23:38:16 Writing status file ...
23:38:16 Running sitegen ...
23:38:18 Success: Generated topics.shtml
23:38:18 Success: Generated index.shtml
23:38:18 Success: Generated shtml files for 347 entries
23:38:18 Success: Generated statistics.shtml
23:38:18 Success: Generated about.shtml
23:38:18 Success: Generated citing.shtml
23:38:18 Success: Generated updating.shtml
23:38:18 Success: Generated search.shtml
23:38:18 Success: Generated submitting.shtml
23:38:18 Success: Generated using.shtml
23:38:18 Success: Generated rss.xml
23:38:18 Success: Generated status.shtml
23:38:18 Packing tars ...
23:38:24 
23:38:24 === COMPLETED ===
23:38:24 
23:38:24 Archiving artifacts
23:39:11 Started calculate disk usage of build
23:39:11 Finished Calculation of disk usage of build in 0 seconds
23:39:14 Started calculate disk usage of workspace
23:39:14 Finished Calculation of disk usage of workspace in 0 seconds
23:39:14 No emails were triggered.
23:39:14 Finished: SUCCESS