Started by upstream project "afp-repo" build number 1312 originally caused by: Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/afp-repo-afp [afp-repo-afp] $ hg showconfig paths.default [afp-repo-afp] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes no changes found [afp-repo-afp] $ hg update --clean --rev default 0 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp-repo-afp] $ hg log --rev . --template {node} [afp-repo-afp] $ hg log --rev . --template {rev} [afp] $ hg showconfig paths.default [afp] $ hg pull --rev 656846d82369b17541237349da9a1b5a93940407 pulling from https://bitbucket.org/isa-afp/afp-devel/ searching for changes adding changesets adding manifests adding file changes added 5 changesets with 236 changes to 193 files (run 'hg update' to get a working copy) [afp] $ hg update --clean --rev 656846d82369b17541237349da9a1b5a93940407 593 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg id --branch No emails were triggered. [afp-repo-afp] $ /bin/sh -xe /tmp/jenkins2425495288623540195.sh + Admin/jenkins/run_build afp + set -e + PROFILE=afp + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ci_build_afp === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1/x86_64-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="-H 4000 --maxheap 8G" === BUILD === Build started at Thu, 11 Jan 2018 20:06:17 GMT Isabelle id e9ab4ad7bd15 AFP id 656846d82369 === LOG === Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session AFP/AVL-Trees (AFP) Session AFP/AWN (AFP) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/AnselmGod (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/CISC-Kernel (AFP) Session AFP/CYK (AFP) Session AFP/Cauchy (AFP) Session AFP/Sqrt_Babylonian (AFP) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Depth-First-Search (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/DiskPaxos (AFP) Session AFP/Example-Submission (AFP) Session AFP/FFT (AFP) Session AFP/FLP (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session AFP/GPU_Kernel_PL (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/GoedelGod (AFP) Session HOL/HOL-Eisbach Session AFP/Allen_Calculus (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session HOL/HOL-Hoare Session AFP/Case_Labeling (AFP) Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session AFP/ArrowImpossibilityGS (AFP) Session AFP/Binomial-Heaps (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Buildings (AFP) Session AFP/CRDT (AFP) Session AFP/IMAP-CRDT (AFP) Session AFP/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Category (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/CoreC++ (AFP) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Efficient-Mergesort (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/FinFun (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session AFP/Group-Ring-Module (AFP) Session AFP/Valuation (AFP) Session HOL/HOL-Cardinals (timing) Session AFP/Ordinals_and_Cardinals (AFP) Session AFP/Sort_Encodings (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session AFP/JNF-HOL-Lib (AFP) Session AFP/Orbit_Stabiliser (AFP) Session AFP/Perfect-Number-Thm (AFP) Session AFP/Secondary_Sylow (AFP) Session AFP/Jordan_Hoelder (AFP) Session AFP/VectorSpace (AFP) Session HOL/HOL-Analysis (main timing) Session AFP/Bernoulli (AFP) Session AFP/Cartan_FP (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/Coinductive (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Topology (AFP) Session AFP/First_Welfare_Theorem (AFP) Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Fisher_Yates (AFP) Session AFP/Girth_Chromatic (AFP) Session AFP/Random_Graph_Subgraph_Threshold (AFP) Session AFP/Lp (AFP) Session AFP/Markov_Models (AFP) Session AFP/Monad_Normalisation (AFP) Session AFP/Monomorphic_Monad (AFP) Session AFP/Probabilistic_Noninterference (AFP) Session AFP/Probabilistic_System_Zoo (AFP) Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Probabilistic_System_Zoo-BNFs (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Hermite (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Number_Theory (main timing) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session AFP/Lehmer (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Prime_Harmonic_Series (AFP) Session AFP/RSAPSS (AFP) Session AFP/SumSquares (AFP) Session AFP/Liouville_Numbers (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Winding_Number_Eval (AFP) Session AFP/Count_Complex_Roots (AFP) Session HOL/HOL-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Imperative_Insertion_Sort (AFP) Session HOL/HOL-Nominal Session AFP/CCS (AFP) Session AFP/Lam-ml-Normalization (AFP) Session AFP/Pi_Calculus (AFP) Session AFP/Psi_Calculi (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/HyperCTL (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/Integration (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session Doc/Isar_Ref (doc) Session AFP/LTL (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Landau_Symbols (AFP) Session AFP/Landau_Analysis (AFP) Session AFP/Catalan_Numbers (AFP) Session AFP/Euler_MacLaurin (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/MuchAdoAboutTwo (AFP) Session AFP/Optics (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (AFP) Session AFP/Presburger-Automata (AFP) Session AFP/Priority_Queue_Braun (AFP) Session AFP/Program-Conflict-Analysis (AFP) Session AFP/Regular-Sets (AFP) Session AFP/Abstract-Rewriting (AFP) Session AFP/Decreasing-Diagrams (AFP) Session AFP/Matrix (AFP) Session AFP/Matrix_Tensor (AFP) Session AFP/Knot_Theory (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Trie (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-Statespace Session HOL/HOL-Types_To_Sets Session HOL/HOL-Word (main timing) Session HOL/HOL-SPARK (main) Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session AFP/Kleene_Algebra (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Multirelations (AFP) Session AFP/Regular_Algebras (AFP) Session AFP/Relation_Algebra (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/Native_Word (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/Incredible_Proof_Machine (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Deriving (AFP) Session AFP/CAVA_Base (AFP) Session AFP/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Gabow_SCC (AFP) Session AFP/LTL_to_GBA (AFP) Session AFP/CAVA_buildchain1 (AFP) Session AFP/Promela (AFP) Session AFP/CAVA_buildchain3 (AFP) Session AFP/CAVA_LTL_Modelchecker (AFP) Session AFP/Containers (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/Show (AFP) Session AFP/JNF-AFP-Lib (AFP) Session AFP/Real_Impl (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/Transitive-Closure (AFP) Session AFP/KBPs (AFP) Session AFP/Tree-Automata (AFP) Session AFP/SPARCv8 (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Separata (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session HOL/HOLCF-Library Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session AFP/Shivers-CFA (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/Tycon (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/HotelKeyCards (AFP) Session AFP/Huffman (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/InfPathElimination (AFP) Session AFP/JiveDataStoreModel (AFP) Session AFP/KAD (AFP) Session AFP/Algebraic_VCs (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Taylor_Models (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Jinja (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/LTL_to_DRA (AFP) Session AFP/List_Update (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Akra_Bazzi (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/HOL-ODE (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/HOL-ODE-Refinement (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-Examples (AFP) Session AFP/Lorenz_Approximation (AFP) Session AFP/Lorenz_C1 (AFP) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Random_BSTs (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Sepref_IICF (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/Maxflow_Lib (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/List_Interleaving (AFP) Session AFP/LocalLexing (AFP) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session AFP/MSO_Examples (AFP) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/Menger (AFP) Session AFP/MiniML (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/Launchbury (AFP) Session AFP/Call_Arity (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Rewriting_Z (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/NormByEval (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Certification_Monads (AFP) Session AFP/XML (AFP) Session AFP/Pre_Polynomial_Factorization (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Deep_Learning_Lib (AFP) Session AFP/Deep_Learning (AFP) Session AFP/Polynomials (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Subresultants (AFP) Session AFP/Pre_BZ (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Pre_Algebraic_Numbers (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/Algebraic_Numbers_Lib (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Linear_Recurrences_Test (AFP) Session AFP/Pre_Perron_Frobenius (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Regex_Equivalence (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Statecharts (AFP) Session AFP/Stone_Algebras (AFP) Session AFP/Stone_Relation_Algebras (AFP) Session AFP/Stone_Kleene_Relation_Algebras (AFP) Session AFP/Strong_Security (AFP) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Transitive-Closure-II (AFP) Session AFP/Tree_Decomposition (AFP) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/CryptHOL (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Free-Groups (AFP) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Stern_Brocot (AFP) Session Unsorted/Spec_Check Session AFP/Regex_Equivalence_Examples (AFP) Building Dirichlet_Series ... Building Affine_Arithmetic ... Building IP_Addresses ... Building HOL-ODE-Refinement ... Building Refine_Monadic ... Building UPF ... Building List-Infinite ... Building Stirling_Formula ... UPF: theory UPF.Monads IP_Addresses: theory HOL-Eisbach.Eisbach IP_Addresses: theory HOL-Library.Cancellation Refine_Monadic: theory HOL-Library.Adhoc_Overloading Refine_Monadic: theory HOL-Library.Bit Refine_Monadic: theory HOL-Library.Boolean_Algebra List-Infinite: theory List-Infinite.Util_NatInf List-Infinite: theory List-Infinite.Util_MinMax List-Infinite: theory List-Infinite.Util_Nat IP_Addresses: theory HOL-Library.Infinite_Set Stirling_Formula: theory HOL-Library.Stirling Stirling_Formula: theory Bernoulli.Bernoulli Dirichlet_Series: theory HOL-Library.Adhoc_Overloading Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading Affine_Arithmetic: theory Deriving.Comparator IP_Addresses: theory HOL-Library.Multiset Refine_Monadic: theory HOL-Library.Monad_Syntax Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure List-Infinite: theory List-Infinite.Util_Set Affine_Arithmetic: theory Deriving.Derive_Manager Affine_Arithmetic: theory Deriving.Generator_Aux Refine_Monadic: theory HOL-Library.Phantom_Type List-Infinite: theory List-Infinite.Util_Div UPF: theory UPF.UPFCore Refine_Monadic: theory HOL-Library.While_Combinator Stirling_Formula: theory Bernoulli.Periodic_Bernpoly IP_Addresses: theory HOL-Library.Option_ord Stirling_Formula: theory Bernoulli.Bernoulli_FPS Affine_Arithmetic: theory Deriving.Equality_Generator HOL-ODE-Refinement: theory HOL-Eisbach.Eisbach HOL-ODE-Refinement: theory HOL-Library.Adhoc_Overloading Stirling_Formula: theory Stirling_Formula.Stirling_Formula HOL-ODE-Refinement: theory Automatic_Refinement.Foldi IP_Addresses: theory IP_Addresses.NumberWang_IPv4 Affine_Arithmetic: theory Deriving.Equality_Instances List-Infinite: theory List-Infinite.SetInterval2 HOL-ODE-Refinement: theory Automatic_Refinement.Prio_List HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1 Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order IP_Addresses: theory IP_Addresses.NumberWang_IPv6 HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Term_Antiquot Refine_Monadic: theory HOL-Word.Bits Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers Affine_Arithmetic: theory Deriving.Compare IP_Addresses: theory IP_Addresses.Word_More HOL-ODE-Refinement: theory Automatic_Refinement.Mpat_Antiquot HOL-ODE-Refinement: theory Deriving.Comparator Refine_Monadic: theory HOL-Library.Cardinality HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree Refine_Monadic: theory HOL-Word.Bits_Bit Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction UPF: theory UPF.ElementaryPolicies Dirichlet_Series: theory HOL-Number_Theory.Cong Refine_Monadic: theory HOL-Word.Misc_Numeric UPF: theory UPF.ParallelComposition UPF: theory UPF.SeqComposition Refine_Monadic: theory HOL-Word.Bit_Representation Affine_Arithmetic: theory Deriving.Comparator_Generator HOL-ODE-Refinement: theory Automatic_Refinement.Anti_Unification HOL-ODE-Refinement: theory Automatic_Refinement.Attr_Comb HOL-ODE-Refinement: theory Automatic_Refinement.Named_Sorted_Thms HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Data HOL-ODE-Refinement: theory Automatic_Refinement.Indep_Vars HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Record_Simp HOL-ODE-Refinement: theory Automatic_Refinement.Tagged_Solver Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat Refine_Monadic: theory HOL-Library.Numeral_Type HOL-ODE-Refinement: theory Automatic_Refinement.Select_Solve Dirichlet_Series: theory HOL-Library.Code_Target_Nat HOL-ODE-Refinement: theory Deriving.Compare HOL-ODE-Refinement: theory Deriving.Derive_Manager HOL-ODE-Refinement: theory Deriving.Generator_Aux Refine_Monadic: theory HOL-Word.Bits_Int Dirichlet_Series: theory HOL-Library.Code_Target_Int HOL-ODE-Refinement: theory Deriving.Comparator_Generator UPF: theory UPF.Analysis UPF: theory UPF.Normalisation Affine_Arithmetic: theory Deriving.Compare_Generator Dirichlet_Series: theory HOL-Library.Code_Target_Numeral HOL-ODE-Refinement: theory Deriving.Equality_Generator Dirichlet_Series: theory HOL-Algebra.Congruence List-Infinite: theory List-Infinite.InfiniteSet2 List-Infinite: theory List-Infinite.SetIntervalCut Affine_Arithmetic: theory HOL-Library.Bit HOL-ODE-Refinement: theory Deriving.Equality_Instances HOL-ODE-Refinement: theory Deriving.Compare_Generator Refine_Monadic: theory HOL-Library.Type_Length HOL-ODE-Refinement: theory HOL-Library.AList Refine_Monadic: theory HOL-Word.Word_Miscellaneous Dirichlet_Series: theory HOL-Library.Function_Algebras Affine_Arithmetic: theory HOL-Library.Boolean_Algebra Dirichlet_Series: theory HOL-Library.Monad_Syntax HOL-ODE-Refinement: theory HOL-Library.Bit Dirichlet_Series: theory HOL-Library.More_List Refine_Monadic: theory HOL-Word.Misc_Typedef Affine_Arithmetic: theory HOL-Library.Permutation Affine_Arithmetic: theory HOL-Library.Char_ord Refine_Monadic: theory HOL-Word.Bool_List_Representation Refine_Monadic: theory Refine_Monadic.Example_Chapter Refine_Monadic: theory Refine_Monadic.Refine_Chapter Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover Dirichlet_Series: theory HOL-Algebra.Order HOL-ODE-Refinement: theory HOL-Library.Boolean_Algebra Affine_Arithmetic: theory Deriving.Compare_Instances Dirichlet_Series: theory HOL-Library.Stirling Refine_Monadic: theory Refine_Monadic.Refine_Misc Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat Affine_Arithmetic: theory HOL-Library.Code_Target_Nat Affine_Arithmetic: theory HOL-Library.Code_Char Affine_Arithmetic: theory HOL-Library.Code_Target_Int Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes UPF: theory UPF.NormalisationTestSpecification List-Infinite: theory List-Infinite.List2 List-Infinite: theory List-Infinite.SetIntervalStep Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral HOL-ODE-Refinement: theory HOL-Library.Permutation Affine_Arithmetic: theory HOL-Library.Mapping Affine_Arithmetic: theory HOL-Library.Monad_Syntax Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial HOL-ODE-Refinement: theory HOL-ex.Quicksort Affine_Arithmetic: theory HOL-Library.Type_Length UPF: theory UPF.UPF Affine_Arithmetic: theory HOL-Library.RBT_Impl HOL-ODE-Refinement: theory HOL-Library.Char_ord Refine_Monadic: theory HOL-Word.Word HOL-ODE-Refinement: theory Deriving.Compare_Instances Dirichlet_Series: theory HOL-Algebra.Lattice Refine_Monadic: theory Refine_Monadic.RefineG_Domain UPF: theory UPF.Service HOL-ODE-Refinement: theory HOL-Library.Code_Char HOL-ODE-Refinement: theory HOL-Library.Omega_Words_Fun HOL-ODE-Refinement: theory HOL-Library.Mapping List-Infinite: theory List-Infinite.ListInf HOL-ODE-Refinement: theory HOL-Library.Monad_Syntax Refine_Monadic: theory Refine_Monadic.RefineG_Transfer Affine_Arithmetic: theory HOL-Word.Bits HOL-ODE-Refinement: theory HOL-Library.Option_ord Affine_Arithmetic: theory HOL-Word.Bits_Bit Refine_Monadic: theory Refine_Monadic.RefineG_Assert Refine_Monadic: theory Refine_Monadic.RefineG_Recursion IP_Addresses: theory HOL-ex.Quicksort Affine_Arithmetic: theory HOL-Word.Misc_Numeric HOL-ODE-Refinement: theory Automatic_Refinement.Misc Affine_Arithmetic: theory HOL-Word.Bit_Representation Dirichlet_Series: theory HOL-Algebra.Complete_Lattice HOL-ODE-Refinement: theory HOL-Library.Type_Length Refine_Monadic: theory Refine_Monadic.RefineG_While IP_Addresses: theory Automatic_Refinement.Misc HOL-ODE-Refinement: theory HOL-Library.RBT_Impl Affine_Arithmetic: theory HOL-Word.Bits_Int Refine_Monadic: theory Refine_Monadic.Refine_Det Dirichlet_Series: theory HOL-Algebra.Group List-Infinite: theory List-Infinite.ListInf_Prefix Affine_Arithmetic: theory HOL-Word.Bool_List_Representation List-Infinite: theory List-Infinite.ListInfinite Refine_Monadic: theory Refine_Monadic.Refine_Basic Dirichlet_Series: theory HOL-Algebra.Coset Affine_Arithmetic: theory Native_Word.More_Bits_Int Dirichlet_Series: theory HOL-Algebra.FiniteProduct Dirichlet_Series: theory HOL-Algebra.Ring Affine_Arithmetic: theory Native_Word.Bits_Integer HOL-ODE-Refinement: theory Automatic_Refinement.Digraph_Basic Dirichlet_Series: theory Bernoulli.Bernoulli Dirichlet_Series: theory Bernoulli.Bernoulli_FPS Refine_Monadic: theory Refine_Monadic.Refine_Heuristics Refine_Monadic: theory Refine_Monadic.Refine_Leof Refine_Monadic: theory Refine_Monadic.Refine_Pfun HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Lib Refine_Monadic: theory Refine_Monadic.Refine_More_Comb Refine_Monadic: theory Refine_Monadic.Refine_While Refine_Monadic: theory Refine_Monadic.Refine_Transfer HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Phases Refine_Monadic: theory Refine_Monadic.Autoref_Monadic Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tagging Refine_Monadic: theory Refine_Monadic.Refine_Automation Refine_Monadic: theory Refine_Monadic.Refine_Foreach HOL-ODE-Refinement: theory Automatic_Refinement.Relators Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-ODE-Refinement: theory Automatic_Refinement.Param_Tool Dirichlet_Series: theory HOL-Algebra.AbelCoset HOL-ODE-Refinement: theory Automatic_Refinement.Param_HOL UPF: theory UPF.ServiceExample Refine_Monadic: theory Refine_Monadic.Refine_Monadic HOL-ODE-Refinement: theory Automatic_Refinement.Parametricity HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Id_Ops Refine_Monadic: theory Refine_Monadic.Breadth_First_Search Refine_Monadic: theory Refine_Monadic.WordRefine Refine_Monadic: theory Refine_Monadic.Examples HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Fix_Rel HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Translate HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Gen_Algo HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Relator_Interface HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tool HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous Affine_Arithmetic: theory HOL-Word.Misc_Typedef IP_Addresses: theory HOL-Library.Code_Abstract_Nat IP_Addresses: theory HOL-Library.Product_Lexorder IP_Addresses: theory HOL-Library.Code_Target_Nat Affine_Arithmetic: theory HOL-Word.Word IP_Addresses: theory IP_Addresses.Hs_Compat IP_Addresses: theory IP_Addresses.Lib_Numbers_toString IP_Addresses: theory IP_Addresses.Word_Next IP_Addresses: theory IP_Addresses.Lib_List_toString IP_Addresses: theory IP_Addresses.Lib_Word_toString IP_Addresses: theory IP_Addresses.WordInterval Dirichlet_Series: theory HOL-Algebra.Ideal HOL-ODE-Refinement: theory Automatic_Refinement.Automatic_Refinement HOL-ODE-Refinement: theory Collections.Intf_Comp HOL-ODE-Refinement: theory Collections.SetIterator IP_Addresses: theory IP_Addresses.IP_Address HOL-ODE-Refinement: theory Collections.Idx_Iterator IP_Addresses: theory IP_Addresses.WordInterval_Sorted Affine_Arithmetic: theory Native_Word.Word_Misc HOL-ODE-Refinement: theory Collections.SetIteratorOperations Affine_Arithmetic: theory Native_Word.Uint32 Dirichlet_Series: theory HOL-Algebra.RingHom Dirichlet_Series: theory HOL-Algebra.Module HOL-ODE-Refinement: theory Collections.Assoc_List Affine_Arithmetic: theory Collections.HashCode HOL-ODE-Refinement: theory Collections.Diff_Array Affine_Arithmetic: theory Deriving.Hash_Generator Dirichlet_Series: theory HOL-Algebra.More_Group Dirichlet_Series: theory HOL-Algebra.More_Finite_Product Dirichlet_Series: theory HOL-Algebra.More_Ring Dirichlet_Series: theory HOL-Algebra.UnivPoly Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra Affine_Arithmetic: theory Deriving.Hash_Instances IP_Addresses: theory IP_Addresses.IPv4 Affine_Arithmetic: theory Deriving.Countable_Generator Affine_Arithmetic: theory Deriving.Derive IP_Addresses: theory IP_Addresses.IPv6 HOL-ODE-Refinement: theory Collections.Impl_Array_Stack IP_Addresses: theory IP_Addresses.Prefix_Match Dirichlet_Series: theory HOL-Library.Going_To_Filter Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly HOL-ODE-Refinement: theory Collections.Proper_Iterator Affine_Arithmetic: theory HOL-Library.Lattice_Algebras Timing Stirling_Formula (2 threads, 17.724s elapsed time, 29.544s cpu time, 0.708s GC time, factor 1.67) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/outline.pdf Finished Stirling_Formula (0:00:38 elapsed time, 0:00:57 cpu time, factor 1.48) Building Jordan_Normal_Form ... Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin IP_Addresses: theory IP_Addresses.CIDR_Split HOL-ODE-Refinement: theory Collections.It_to_It HOL-ODE-Refinement: theory Collections.SetIteratorGA HOL-ODE-Refinement: theory HOL-Library.While_Combinator Dirichlet_Series: theory HOL-Number_Theory.Fib HOL-ODE-Refinement: theory HOL-Word.Bits_Bit Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers HOL-ODE-Refinement: theory Native_Word.More_Bits_Int Affine_Arithmetic: theory HOL-Library.RBT Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring Affine_Arithmetic: theory HOL-Library.RBT_Mapping Dirichlet_Series: theory HOL-Number_Theory.Totient Affine_Arithmetic: theory HOL-Library.Log_Nat Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise Dirichlet_Series: theory Landau_Symbols.Landau_Library Dirichlet_Series: theory Landau_Symbols.Landau_Symbols_Definition HOL-ODE-Refinement: theory Native_Word.Bits_Integer Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector Affine_Arithmetic: theory HOL-Library.Float Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary Affine_Arithmetic: theory Affine_Arithmetic.Polygon Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Permutations Affine_Arithmetic: theory List-Index.List_Index HOL-ODE-Refinement: theory HOL-Library.RBT Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float Dirichlet_Series: theory Landau_Symbols.Group_Sort Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds Affine_Arithmetic: theory Affine_Arithmetic.Float_Real Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space HOL-ODE-Refinement: theory HOL-Library.RBT_Mapping Timing List-Infinite (2 threads, 21.940s elapsed time, 38.340s cpu time, 1.740s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List-Infinite Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List-Infinite/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List-Infinite/outline.pdf Finished List-Infinite (0:00:47 elapsed time, 0:01:12 cpu time, factor 1.55) Building Nat-Interval-Logic ... HOL-ODE-Refinement: theory HOL-Word.Word_Miscellaneous HOL-ODE-Refinement: theory HOL-Word.Misc_Typedef HOL-ODE-Refinement: theory HOL-Word.Word Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix Nat-Interval-Logic: theory Nat-Interval-Logic.IL_Interval Nat-Interval-Logic: theory Nat-Interval-Logic.IL_IntervalOperators Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs Affine_Arithmetic: theory HOL-Decision_Procs.Approximation Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic Dirichlet_Series: theory Landau_Symbols.Asymptotic_Equivalence Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace Dirichlet_Series: theory Landau_Symbols.Landau_More Dirichlet_Series: theory Landau_Symbols.Landau_Symbols Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form HOL-ODE-Refinement: theory Native_Word.Word_Misc Dirichlet_Series: theory Matrix.Utility Dirichlet_Series: theory Polynomial_Factorization.Missing_List HOL-ODE-Refinement: theory Deriving.Countable_Generator Nat-Interval-Logic: theory Nat-Interval-Logic.IL_TemporalOperators HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Integer Timing UPF (2 threads, 31.443s elapsed time, 59.568s cpu time, 2.312s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF/outline.pdf Finished UPF (0:00:54 elapsed time, 0:01:32 cpu time, factor 1.69) Running Security_Protocol_Refinement ... HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Float Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl HOL-ODE-Refinement: theory Affine_Arithmetic.Float_Real Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant HOL-ODE-Refinement: theory Native_Word.Code_Target_Bits_Int Security_Protocol_Refinement: theory Security_Protocol_Refinement.Infra Security_Protocol_Refinement: theory Security_Protocol_Refinement.Agents Security_Protocol_Refinement: theory Security_Protocol_Refinement.Refinement HOL-ODE-Refinement: theory Collections.Code_Target_ICF HOL-ODE-Refinement: theory Native_Word.Uint HOL-ODE-Refinement: theory Native_Word.Uint32 Security_Protocol_Refinement: theory Security_Protocol_Refinement.Keys Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_Vector Security_Protocol_Refinement: theory Security_Protocol_Refinement.a0n_agree Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Security_Protocol_Refinement: theory Security_Protocol_Refinement.Atoms Affine_Arithmetic: theory Affine_Arithmetic.Intersection HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Strict HOL-ODE-Refinement: theory Collections.HashCode Security_Protocol_Refinement: theory Security_Protocol_Refinement.Channels Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl HOL-ODE-Refinement: theory Collections.Intf_Hash HOL-ODE-Refinement: theory Deriving.Hash_Generator Security_Protocol_Refinement: theory Security_Protocol_Refinement.Runs HOL-ODE-Refinement: theory Collections.Gen_Hash HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary HOL-ODE-Refinement: theory Deriving.Hash_Instances HOL-ODE-Refinement: theory Deriving.Derive Security_Protocol_Refinement: theory Security_Protocol_Refinement.Message Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm HOL-ODE-Refinement: theory Affine_Arithmetic.Polygon Security_Protocol_Refinement: theory Security_Protocol_Refinement.a0i_agree Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_auth HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Form Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix HOL-ODE-Refinement: theory Affine_Arithmetic.Floatarith_Expression Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_auth_chan Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_confid_chan Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_sig Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_enc Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison Security_Protocol_Refinement: theory Security_Protocol_Refinement.s0g_secrecy Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form Affine_Arithmetic: theory Show.Show Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix Affine_Arithmetic: theory Show.Show_Instances Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist_iirn HOL-ODE-Refinement: theory Affine_Arithmetic.Intersection Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_keydist_inrn Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_kerberos Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_nssk Dirichlet_Series: theory HOL-Number_Theory.Residues Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_kerberos Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_nssk HOL-ODE-Refinement: theory Affine_Arithmetic.Straight_Line_Program Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos4 Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos5 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Chapter HOL-ODE-Refinement: theory Refine_Monadic.Refine_Mono_Prover HOL-ODE-Refinement: theory Refine_Monadic.Refine_Misc Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_kerberos_par Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion Dirichlet_Series: theory HOL-Number_Theory.Gauss Dirichlet_Series: theory HOL-Number_Theory.Pocklington HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Domain Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_nssk Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Dirichlet_Series: theory HOL-Number_Theory.Number_Theory HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Transfer Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_nssk_par HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Assert HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Recursion Security_Protocol_Refinement: theory Security_Protocol_Refinement.m1_ds HOL-ODE-Refinement: theory Refine_Monadic.RefineG_While Security_Protocol_Refinement: theory Security_Protocol_Refinement.m2_ds Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc HOL-ODE-Refinement: theory Refine_Monadic.Refine_Det Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_ds Security_Protocol_Refinement: theory Security_Protocol_Refinement.m3_ds_par Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness Dirichlet_Series: theory Dirichlet_Series.Euler_Products HOL-ODE-Refinement: theory Refine_Monadic.Refine_Basic HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Approximation Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu Dirichlet_Series: theory Dirichlet_Series.More_Totient Dirichlet_Series: theory Dirichlet_Series.Divisor_Count Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code Dirichlet_Series: theory Dirichlet_Series.Partial_Summation HOL-ODE-Refinement: theory Refine_Monadic.Refine_Heuristics HOL-ODE-Refinement: theory Refine_Monadic.Refine_Leof HOL-ODE-Refinement: theory Refine_Monadic.Refine_More_Comb HOL-ODE-Refinement: theory Refine_Monadic.Refine_Pfun HOL-ODE-Refinement: theory Refine_Monadic.Refine_While Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis HOL-ODE-Refinement: theory Refine_Monadic.Refine_Transfer Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl HOL-ODE-Refinement: theory Refine_Monadic.Autoref_Monadic HOL-ODE-Refinement: theory Refine_Monadic.Refine_Automation HOL-ODE-Refinement: theory Refine_Monadic.Refine_Foreach Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius Timing Refine_Monadic (2 threads, 60.389s elapsed time, 106.148s cpu time, 5.044s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Monadic Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Monadic/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Monadic/outline.pdf Finished Refine_Monadic (0:01:27 elapsed time, 0:02:25 cpu time, factor 1.67) Building Collections ... HOL-ODE-Refinement: theory Refine_Monadic.Refine_Monadic HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Code HOL-ODE-Refinement: theory Collections.Gen_Iterator Collections: theory Collections.ICF_Tools Collections: theory Collections.Partial_Equivalence_Relation Collections: theory Finger-Trees.FingerTree Collections: theory Collections.Ord_Code_Preproc Collections: theory Collections.Locale_Code Collections: theory Collections.Record_Intf Collections: theory HOL-Library.AList HOL-ODE-Refinement: theory Collections.Iterator Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics HOL-ODE-Refinement: theory Collections.Array_Iterator HOL-ODE-Refinement: theory Collections.RBT_add Collections: theory Binomial-Heaps.BinomialHeap HOL-ODE-Refinement: theory Collections.Intf_Map HOL-ODE-Refinement: theory Collections.Intf_Set HOL-ODE-Refinement: theory Collections.Gen_Map HOL-ODE-Refinement: theory Collections.Impl_RBT_Map HOL-ODE-Refinement: theory Collections.Impl_Array_Map HOL-ODE-Refinement: theory Collections.Impl_List_Map Collections: theory Binomial-Heaps.SkewBinomialHeap HOL-ODE-Refinement: theory Collections.Impl_Array_Hash_Map Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression HOL-ODE-Refinement: theory Collections.Gen_Map2Set HOL-ODE-Refinement: theory Collections.Gen_Set HOL-ODE-Refinement: theory Collections.Impl_Bit_Set HOL-ODE-Refinement: theory Collections.Impl_Cfun_Set HOL-ODE-Refinement: theory Collections.Impl_List_Set HOL-ODE-Refinement: theory Collections.Impl_Uv_Set HOL-ODE-Refinement: theory Show.Show Collections: theory HOL-Library.Code_Abstract_Nat Collections: theory HOL-Library.Code_Target_Nat HOL-ODE-Refinement: theory Show.Show_Instances Collections: theory HOL-Library.Code_Target_Int Collections: theory HOL-Library.Code_Target_Numeral HOL-ODE-Refinement: theory Affine_Arithmetic.Print Collections: theory HOL-Library.Dlist Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program Collections: theory Collections.SetIterator HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Affine_Approximation Collections: theory Collections.Idx_Iterator Collections: theory Collections.SetAbstractionIterator Collections: theory Collections.SetIteratorOperations HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Ineqs Collections: theory Collections.Sorted_List_Operations HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Inter Collections: theory HOL-Library.RBT_Impl Timing Nat-Interval-Logic (2 threads, 41.824s elapsed time, 56.112s cpu time, 1.312s GC time, factor 1.34) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nat-Interval-Logic Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nat-Interval-Logic/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Nat-Interval-Logic/outline.pdf Finished Nat-Interval-Logic (0:01:04 elapsed time, 0:01:27 cpu time, factor 1.37) Running Key_Agreement_Strong_Adversaries ... Collections: theory Collections.Assoc_List Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Infra Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Messages Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Refinement Collections: theory Collections.Diff_Array Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation Collections: theory Collections.Dlist_add Collections: theory Collections.Proper_Iterator Collections: theory Collections.It_to_It Collections: theory Collections.SetIteratorGA Collections: theory Collections.DatRef HOL-ODE-Refinement: theory HOL-ODE-Refinement.GenCF_No_Comp Collections: theory Native_Word.More_Bits_Int Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationN Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Message_derivation Collections: theory Native_Word.Bits_Integer Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationI Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Channels Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.IK Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Secrecy Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Payloads Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Runs Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_asymmetric Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_lemmas Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_symmetric Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl1 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Dflt_No_Comp HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Misc Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl1 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl2 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl1 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl2 Affine_Arithmetic: theory Affine_Arithmetic.Print Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric IP_Addresses: theory IP_Addresses.IP_Address_Parser Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl2 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter Collections: theory Native_Word.Code_Target_Bits_Int Collections: theory Collections.Code_Target_ICF Collections: theory Collections.Locale_Code_Ex IP_Addresses: theory IP_Addresses.IP_Address_toString Collections: theory Native_Word.Word_Misc HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Folds Collections: theory Native_Word.Uint32 IP_Addresses: theory IP_Addresses.Prefix_Match_toString Collections: theory Collections.HashCode Collections: theory Collections.Gen_Iterator Collections: theory Collections.Iterator Collections: theory Collections.ICF_Spec_Base Collections: theory Collections.MapSpec Collections: theory Collections.Robdd Collections: theory Collections.RBT_add HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_String HOL-ODE-Refinement: theory HOL-ODE-Refinement.Weak_Set HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Arithmetic Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic Collections: theory Collections.GenCF_Chapter Collections: theory Collections.GenCF_Gen_Chapter Collections: theory Collections.GenCF_Impl_Chapter Collections: theory Collections.GenCF_Intf_Chapter Collections: theory Collections.Intf_Comp Collections: theory Collections.Impl_Array_Stack Collections: theory HOL-Library.Product_Lexorder Collections: theory Collections.Intf_Hash Collections: theory Collections.Array_Iterator Collections: theory Collections.Gen_Comp Collections: theory Collections.Intf_Map Collections: theory Collections.Intf_Set Collections: theory Collections.Gen_Map Collections: theory Collections.Impl_RBT_Map Collections: theory Collections.Impl_Array_Map Collections: theory Collections.Impl_List_Map Collections: theory Collections.Impl_Array_Hash_Map Collections: theory Collections.Gen_Map2Set Collections: theory Collections.Gen_Set Collections: theory Collections.Impl_Cfun_Set Collections: theory Collections.Impl_List_Set Collections: theory Native_Word.Uint Collections: theory Collections.Gen_Hash Collections: theory Collections.Impl_Bit_Set Collections: theory Collections.Impl_Uv_Set Collections: theory Collections.GenCF Collections: theory Collections.ICF_Gen_Algo_Chapter Collections: theory Collections.ICF_Chapter Collections: theory Collections.ICF_Impl_Chapter Collections: theory Collections.ICF_Spec_Chapter Collections: theory Trie.Trie Collections: theory HOL-Library.RBT Collections: theory Collections.AnnotatedListSpec Collections: theory Collections.Trie_Impl Collections: theory Collections.Trie2 Collections: theory Collections.ListSpec Collections: theory Collections.FTAnnotatedListImpl Collections: theory Collections.ListGA Collections: theory Collections.PrioSpec Collections: theory Collections.Fifo Collections: theory Collections.BinoPrioImpl Collections: theory Collections.PrioByAnnotatedList Collections: theory Collections.SkewPrioImpl Collections: theory Collections.PrioUniqueSpec Collections: theory Collections.FTPrioImpl Collections: theory Collections.PrioUniqueByAnnotatedList Collections: theory Collections.SetSpec Collections: theory Collections.FTPrioUniqueImpl Collections: theory Collections.Algos Timing Dirichlet_Series (2 threads, 251.709s elapsed time, 435.520s cpu time, 19.588s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_Series Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_Series/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_Series/outline.pdf Finished Dirichlet_Series (0:04:59 elapsed time, 0:08:24 cpu time, factor 1.69) Running Network_Security_Policy_Verification ... Collections: theory Collections.SetIndex Collections: theory Collections.SetIteratorCollectionsGA Network_Security_Policy_Verification: theory HOL-Eisbach.Eisbach Network_Security_Policy_Verification: theory HOL-Library.Cancellation Collections: theory Collections.MapGA Collections: theory Collections.SetGA Network_Security_Policy_Verification: theory HOL-Library.Char_ord Network_Security_Policy_Verification: theory HOL-Library.Multiset Network_Security_Policy_Verification: theory HOL-Library.Code_Abstract_Nat Network_Security_Policy_Verification: theory HOL-Library.Code_Target_Nat Network_Security_Policy_Verification: theory HOL-Library.Code_Char Network_Security_Policy_Verification: theory HOL-Library.Infinite_Set Network_Security_Policy_Verification: theory HOL-Library.List_lexord Network_Security_Policy_Verification: theory HOL-Library.Option_ord Network_Security_Policy_Verification: theory HOL-Library.Product_Lexorder Network_Security_Policy_Verification: theory HOL-Library.RBT_Impl Collections: theory Collections.ArrayMapImpl Collections: theory Collections.ListMapImpl Collections: theory Collections.ListMapImpl_Invar Collections: theory Collections.ArrayHashMap_Impl Network_Security_Policy_Verification: theory HOL-ex.Quicksort Network_Security_Policy_Verification: theory Automatic_Refinement.Misc Collections: theory Collections.TrieMapImpl Collections: theory Collections.ListSetImpl Collections: theory Collections.ArrayHashMap Collections: theory Collections.ListSetImpl_Invar Collections: theory Collections.ListSetImpl_NotDist Collections: theory Collections.ListSetImpl_Sorted Collections: theory Collections.SetByMap Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Config Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct Collections: theory Collections.RBTMapImpl Collections: theory Collections.ArrayHashSet Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_Impl Network_Security_Policy_Verification: theory Transitive-Closure.Transitive_Closure_List_Impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph Collections: theory Collections.ArraySetImpl Collections: theory Collections.TrieSetImpl Collections: theory Collections.HashMap_Impl Collections: theory Collections.RBTSetImpl Collections: theory Collections.HashMap Collections: theory Collections.HashSet Collections: theory Collections.MapStdImpl Collections: theory Collections.SetStdImpl Network_Security_Policy_Verification: theory HOL-Library.RBT Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl Collections: theory Collections.ICF_Impl Collections: theory Collections.ICF_Refine_Monadic Collections: theory Collections.ICF_Autoref Collections: theory Collections.ICF_Entrypoints_Chapter Collections: theory Collections.Collections_Entrypoints_Chapter Collections: theory Collections.Userguides_Chapter Collections: theory Collections.Collections Collections: theory Collections.Refine_Dflt Collections: theory Collections.CollectionsV1 Collections: theory Collections.ICF_Userguide Collections: theory Collections.Refine_Dflt_ICF Collections: theory Collections.Refine_Dflt_Only_ICF Collections: theory Collections.Refine_Monadic_Userguide Timing IP_Addresses (2 threads, 321.790s elapsed time, 621.968s cpu time, 33.148s GC time, factor 1.93) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/IP_Addresses/outline.pdf Finished IP_Addresses (0:06:09 elapsed time, 0:11:35 cpu time, factor 1.88) Building Simple_Firewall ... Simple_Firewall: theory HOL-Library.Char_ord Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State Simple_Firewall: theory Simple_Firewall.Iface Simple_Firewall: theory Simple_Firewall.GroupF Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString Simple_Firewall: theory Simple_Firewall.L4_Protocol Simple_Firewall: theory Simple_Firewall.List_Product_More Simple_Firewall: theory Simple_Firewall.Option_Helpers Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString Simple_Firewall: theory Simple_Firewall.Simple_Packet Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist Simple_Firewall: theory Simple_Firewall.Primitives_toString Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Matrix Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Vector_Space Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_VS_Connect Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Vertices Network_Security_Policy_Verification: theory HOL-Lattice.Orders Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface Simple_Firewall: theory Simple_Firewall.SimpleFw_toString Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics Network_Security_Policy_Verification: theory HOL-Lattice.Bounds Network_Security_Policy_Verification: theory HOL-Lattice.Lattice Network_Security_Policy_Verification: theory HOL-Lattice.CompleteLattice Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_withOffendingFlows Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.vertex_example_simps Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_ENF Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Helper Simple_Firewall: theory Simple_Firewall.Shadowed Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPstrict Simple_Firewall: theory Simple_Firewall.Service_Matrix Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets2 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Analysis_Tainting Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Interface_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Sink_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Subnets_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Tainting_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Library Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_BLP Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_generateCode Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Impl Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Network_Security_Policy_Verification Timing Simple_Firewall (2 threads, 36.065s elapsed time, 67.312s cpu time, 3.716s GC time, factor 1.87) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simple_Firewall Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simple_Firewall/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Simple_Firewall/outline.pdf Finished Simple_Firewall (0:01:05 elapsed time, 0:01:56 cpu time, factor 1.77) Building Routing ... Routing: theory HOL-Library.Adhoc_Overloading Routing: theory Routing.Linorder_Helper Routing: theory HOL-Library.Monad_Syntax Routing: theory Routing.Routing_Table Routing: theory Routing.IpRoute_Parser Routing: theory Routing.Linux_Router Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.attic Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_NetModel Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CryptoDB Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Distributed_WebApp Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Example_Forte14 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.I8_SSH_Landscape Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.IDEM Timing Collections (2 threads, 273.770s elapsed time, 468.276s cpu time, 32.208s GC time, factor 1.71) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections/outline.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections/userguide.pdf Finished Collections (0:06:19 elapsed time, 0:11:25 cpu time, factor 1.81) Timing Jordan_Normal_Form (2 threads, 360.017s elapsed time, 579.148s cpu time, 17.348s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/outline.pdf Finished Jordan_Normal_Form (0:07:10 elapsed time, 0:11:10 cpu time, factor 1.56) Timing Routing (2 threads, 14.369s elapsed time, 25.680s cpu time, 0.924s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Routing Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Routing/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Routing/outline.pdf Finished Routing (0:00:35 elapsed time, 0:00:55 cpu time, factor 1.59) Building Sepref_Prereq ... Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground Building Iptables_Semantics ... Building Formal_SSA ... Iptables_Semantics: theory HOL-Library.Code_Target_Int Iptables_Semantics: theory HOL-Library.Code_Char Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork Iptables_Semantics: theory HOL-Library.LaTeXsugar Iptables_Semantics: theory Native_Word.More_Bits_Int Iptables_Semantics: theory Iptables_Semantics.List_Misc Iptables_Semantics: theory Iptables_Semantics.Negation_Type Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example Sepref_Prereq: theory HOL-Library.Old_Datatype Sepref_Prereq: theory HOL-Library.Nat_Bijection Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.MeasrDroid Formal_SSA: theory Formal_SSA.Serial_Rel Formal_SSA: theory Dijkstra_Shortest_Path.Graph Formal_SSA: theory HOL-Library.Char_ord Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match Formal_SSA: theory HOL-Library.List_lexord Sepref_Prereq: theory HOL-Library.Countable Formal_SSA: theory HOL-Library.Mapping Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists Formal_SSA: theory HOL-Library.RBT_Set Iptables_Semantics: theory Native_Word.Bits_Integer Formal_SSA: theory HOL-Library.RBT_Mapping Sepref_Prereq: theory HOL-Imperative_HOL.Heap Formal_SSA: theory HOL-Library.Sublist Formal_SSA: theory Formal_SSA.While_Combinator_Exts Formal_SSA: theory Dijkstra_Shortest_Path.GraphSpec Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad Formal_SSA: theory Formal_SSA.FormalSSA_Misc Formal_SSA: theory Formal_SSA.Mapping_Exts Formal_SSA: theory Formal_SSA.RBT_Mapping_Exts Formal_SSA: theory Slicing.AuxLemmas Formal_SSA: theory Slicing.BasicDefs Sepref_Prereq: theory HOL-Imperative_HOL.Array Formal_SSA: theory Slicing.CFG Formal_SSA: theory Slicing.CFGExit Formal_SSA: theory Slicing.Postdomination Sepref_Prereq: theory HOL-Imperative_HOL.Ref Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions Formal_SSA: theory Slicing.DynStandardControlDependence Formal_SSA: theory Slicing.DynWeakControlDependence Formal_SSA: theory Slicing.StandardControlDependence Formal_SSA: theory Formal_SSA.Graph_path Formal_SSA: theory Slicing.WeakControlDependence Formal_SSA: theory Slicing.CFG_wf Formal_SSA: theory Slicing.CFGExit_wf Formal_SSA: theory Slicing.DynDataDependence Formal_SSA: theory Slicing.DataDependence Formal_SSA: theory Slicing.PDG Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation Formal_SSA: theory Slicing.Distance Formal_SSA: theory Slicing.Observable Formal_SSA: theory Slicing.SemanticsCFG Formal_SSA: theory Slicing.Slice Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int Formal_SSA: theory Slicing.WeakOrderDependence Formal_SSA: theory Formal_SSA.SSA_CFG Formal_SSA: theory Slicing.CDepInstantiations Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map Formal_SSA: theory Slicing.Com Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize Formal_SSA: theory Formal_SSA.Construct_SSA Iptables_Semantics: theory Iptables_Semantics.Ternary Iptables_Semantics: theory Iptables_Semantics.Firewall_Common Formal_SSA: theory Formal_SSA.Minimality Formal_SSA: theory Formal_SSA.Construct_SSA_notriv Iptables_Semantics: theory Iptables_Semantics.Conntrack_State Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags Formal_SSA: theory Formal_SSA.SSA_Semantics Formal_SSA: theory Formal_SSA.SSA_CFG_code Timing Key_Agreement_Strong_Adversaries (2 threads, 376.046s elapsed time, 636.520s cpu time, 7.708s GC time, factor 1.69) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/outline.pdf Finished Key_Agreement_Strong_Adversaries (0:06:24 elapsed time, 0:10:49 cpu time, factor 1.69) Building Subresultants ... Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet Formal_SSA: theory Slicing.Labels Formal_SSA: theory Slicing.WCFG Iptables_Semantics: theory Iptables_Semantics.IpAddresses Formal_SSA: theory Slicing.Interpretation Formal_SSA: theory Slicing.WellFormed Formal_SSA: theory Slicing.AdditionalLemmas Formal_SSA: theory Formal_SSA.Disjoin_Transform Iptables_Semantics: theory Iptables_Semantics.Ports Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial Subresultants: theory Subresultants.Coeff_Int Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg Subresultants: theory Subresultants.Dichotomous_Lazard Formal_SSA: theory Formal_SSA.Construct_SSA_code Formal_SSA: theory Formal_SSA.Construct_SSA_notriv_code Subresultants: theory Subresultants.More_Homomorphisms Subresultants: theory Subresultants.Resultant_Prelim Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax Subresultants: theory Subresultants.Binary_Exponentiation Subresultants: theory Subresultants.Subresultant Formal_SSA: theory Formal_SSA.SSA_Transfer_Rules Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA Subresultants: theory Subresultants.Subresultant_Gcd Iptables_Semantics: theory Iptables_Semantics.Semantics Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics Iptables_Semantics: theory Iptables_Semantics.Fixed_Action Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches Iptables_Semantics: theory Iptables_Semantics.Optimizing Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching Iptables_Semantics: theory Iptables_Semantics.Matching Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding Formal_SSA: theory Formal_SSA.Generic_Interpretation Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic Iptables_Semantics: theory Iptables_Semantics.Ipassmt Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt Iptables_Semantics: theory Iptables_Semantics.Word_Upto Formal_SSA: theory Formal_SSA.Generic_Extract Formal_SSA: theory Formal_SSA.WhileGraphSSA Timing Security_Protocol_Refinement (2 threads, 486.578s elapsed time, 784.084s cpu time, 8.628s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Security_Protocol_Refinement Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Security_Protocol_Refinement/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Security_Protocol_Refinement/outline.pdf Finished Security_Protocol_Refinement (0:08:14 elapsed time, 0:13:18 cpu time, factor 1.61) Building Transition_Systems_and_Automata ... Transition_Systems_and_Automata: theory HOL-Library.Old_Datatype Transition_Systems_and_Automata: theory HOL-Library.Nat_Bijection Transition_Systems_and_Automata: theory HOL-Library.Stream Transition_Systems_and_Automata: theory HOL-Library.Sublist Transition_Systems_and_Automata: theory HOL-Library.Countable Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Basic Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence Transition_Systems_and_Automata: theory HOL-Library.Countable_Set Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_Zip Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System Transition_Systems_and_Automata: theory HOL-Library.Countable_Complete_Lattices Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Extra Transition_Systems_and_Automata: theory HOL-Library.Order_Continuity Transition_Systems_and_Automata: theory HOL-Library.Extended_Nat Transition_Systems_and_Automata: theory HOL-Library.Linear_Temporal_Logic_on_Streams Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Sequence_LTL Timing Sepref_Prereq (2 threads, 58.671s elapsed time, 68.508s cpu time, 3.584s GC time, factor 1.17) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sepref_Prereq Finished Sepref_Prereq (0:01:30 elapsed time, 0:03:16 cpu time, factor 2.16) Building Refine_Imperative_HOL ... Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Refine Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Construction Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.BA Refine_Imperative_HOL: theory Refine_Imperative_HOL.PO_Normalizer Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Misc Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Add Refine_Imperative_HOL: theory List-Index.List_Index Refine_Imperative_HOL: theory Refine_Imperative_HOL.Concl_Pres_Clarification Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.DFA Refine_Imperative_HOL: theory Refine_Imperative_HOL.Named_Theorems_Rev Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Implement Refine_Imperative_HOL: theory Refine_Imperative_HOL.Structured_Apply Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Refine_Aux Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Mono_Prover Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Misc Refine_Imperative_HOL: theory Isar_Ref.Base Refine_Imperative_HOL: theory Refine_Imperative_HOL.User_Smashing Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.NFA Refine_Imperative_HOL: theory Refine_Imperative_HOL.Term_Synth Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.Transition_System_Refine Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.BA_Refine Transition_Systems_and_Automata: theory Transition_Systems_and_Automata.BA_Implement Refine_Imperative_HOL: theory HOL-Library.Rewrite Refine_Imperative_HOL: theory Refine_Imperative_HOL.Default_Insts Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_IICF Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Setup Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Tool Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Userguides Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Id_Op Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Basic Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Constraints Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Monadify Iptables_Semantics: theory Iptables_Semantics.Example_Semantics Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Frame Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Rules Iptables_Semantics: theory Iptables_Semantics.No_Spoof Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Combinator_Setup Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Definition Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Translate Iptables_Semantics: theory Iptables_Semantics.Interface_Replace Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Intf_Util Iptables_Semantics: theory Iptables_Semantics.Transform Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Tool Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_HOL_Bindings Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Foreach Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Improper Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Map Iptables_Semantics: theory Iptables_Semantics.Code_Interface Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Map Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_List Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_HOL_List Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_MS_Array_List Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Matrix Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Indexed_Array_List Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Multiset Iptables_Semantics: theory Iptables_Semantics.Parser Iptables_Semantics: theory Iptables_Semantics.Documentation Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_Matrix Iptables_Semantics: theory Iptables_Semantics.Code_haskell Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_Mset Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_MsetO Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Bag Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heap Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heapmap Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heap Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heapmap Timing Subresultants (2 threads, 73.587s elapsed time, 107.124s cpu time, 2.228s GC time, factor 1.46) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/outline.pdf Finished Subresultants (0:01:45 elapsed time, 0:02:31 cpu time, factor 1.43) Building Pre_BZ ... Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.SINVAR_Examples Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Imaginary_Factory_Network Timing Affine_Arithmetic (2 threads, 540.165s elapsed time, 881.968s cpu time, 74.000s GC time, factor 1.63) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Affine_Arithmetic/outline.pdf Finished Affine_Arithmetic (0:10:04 elapsed time, 0:16:42 cpu time, factor 1.66) Building Sepref_Basic ... Pre_BZ: theory HOL-Number_Theory.Cong Pre_BZ: theory Efficient-Mergesort.Efficient_Sort Sepref_Basic: theory Refine_Imperative_HOL.PO_Normalizer Sepref_Basic: theory Refine_Imperative_HOL.Pf_Add Sepref_Basic: theory HOL-Library.Rewrite Sepref_Basic: theory List-Index.List_Index Sepref_Basic: theory Refine_Imperative_HOL.Concl_Pres_Clarification Sepref_Basic: theory Refine_Imperative_HOL.Default_Insts Sepref_Basic: theory Refine_Imperative_HOL.Named_Theorems_Rev Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Id_Op Sepref_Basic: theory Refine_Imperative_HOL.Structured_Apply Sepref_Basic: theory Refine_Imperative_HOL.Pf_Mono_Prover Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Misc Sepref_Basic: theory Refine_Imperative_HOL.User_Smashing Pre_BZ: theory Polynomial_Factorization.Precomputation Pre_BZ: theory HOL-Types_To_Sets.Types_To_Sets Pre_BZ: theory HOL-Word.Bits Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Basic Sepref_Basic: theory Refine_Imperative_HOL.Term_Synth Pre_BZ: theory HOL-Word.Bits_Bit Pre_BZ: theory HOL-Word.Misc_Numeric Pre_BZ: theory HOL-Word.Bit_Representation Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Set Pre_BZ: theory HOL-Word.Bits_Int Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_SetO Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Sepl_Binding Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Constraints Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Monadify Pre_BZ: theory HOL-Word.Bool_List_Representation Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Frame Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Rules Pre_BZ: theory Native_Word.More_Bits_Int Pre_BZ: theory HOL-Word.Word_Miscellaneous Pre_BZ: theory HOL-Word.Misc_Typedef Pre_BZ: theory HOL-Word.Word Pre_BZ: theory Native_Word.Bits_Integer Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Combinator_Setup Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Definition Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Translate Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Intf_Util Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_General_Util Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Quickstart Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Reference Pre_BZ: theory Native_Word.Word_Misc Pre_BZ: theory Polynomial_Interpolation.Improved_Code_Equations Pre_BZ: theory Polynomial_Interpolation.Neville_Aitken_Interpolation Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Tool Pre_BZ: theory Cauchy.CauchysMeanTheorem Pre_BZ: theory Polynomial_Factorization.Polynomial_Divisibility Pre_BZ: theory Polynomial_Interpolation.Lagrange_Interpolation Sepref_Basic: theory Refine_Imperative_HOL.Sepref_HOL_Bindings Pre_BZ: theory HOL-Number_Theory.Totient Pre_BZ: theory HOL-Number_Theory.Residues Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Foreach Sepref_Basic: theory Refine_Imperative_HOL.Sepref_Improper Sepref_Basic: theory Refine_Imperative_HOL.Sepref Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Pre_BZ: theory Native_Word.Code_Target_Bits_Int Pre_BZ: theory Native_Word.Uint32 Timing Transition_Systems_and_Automata (2 threads, 44.820s elapsed time, 84.936s cpu time, 4.576s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transition_Systems_and_Automata Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transition_Systems_and_Automata/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transition_Systems_and_Automata/outline.pdf Finished Transition_Systems_and_Automata (0:01:19 elapsed time, 0:02:10 cpu time, factor 1.65) Building CAVA_Base ... Pre_BZ: theory Native_Word.Uint64 Pre_BZ: theory Polynomial_Interpolation.Is_Rat_To_Rat CAVA_Base: theory CAVA_Base.Statistics CAVA_Base: theory Deriving.Comparator CAVA_Base: theory Deriving.Derive_Manager Pre_BZ: theory Sqrt_Babylonian.Log_Impl CAVA_Base: theory Deriving.Generator_Aux CAVA_Base: theory Deriving.Equality_Generator Pre_BZ: theory Sqrt_Babylonian.NthRoot_Impl CAVA_Base: theory Deriving.Equality_Instances CAVA_Base: theory HOL-Library.Char_ord CAVA_Base: theory HOL-Library.Code_Char CAVA_Base: theory HOL-Library.Nat_Bijection CAVA_Base: theory Deriving.Compare Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian Pre_BZ: theory Polynomial_Factorization.Missing_List Pre_BZ: theory Polynomial_Factorization.Explicit_Roots CAVA_Base: theory Deriving.Comparator_Generator CAVA_Base: theory HOL-Library.Old_Datatype Pre_BZ: theory Polynomial_Interpolation.Divmod_Int Pre_BZ: theory Polynomial_Factorization.Dvd_Int_Poly CAVA_Base: theory Deriving.Compare_Generator CAVA_Base: theory Deriving.Hash_Generator CAVA_Base: theory Deriving.Compare_Instances CAVA_Base: theory Deriving.Hash_Instances CAVA_Base: theory HOL-Library.Countable CAVA_Base: theory CAVA_Base.Code_String Pre_BZ: theory Polynomial_Factorization.Gauss_Lemma CAVA_Base: theory CAVA_Base.CAVA_Code_Target CAVA_Base: theory CAVA_Base.CAVA_Base Pre_BZ: theory Polynomial_Factorization.Missing_Multiset Pre_BZ: theory Polynomial_Factorization.Prime_Factorization Pre_BZ: theory Polynomial_Factorization.Gcd_Rat_Poly CAVA_Base: theory Deriving.Countable_Generator Pre_BZ: theory Polynomial_Factorization.Square_Free_Factorization Pre_BZ: theory Polynomial_Factorization.Rational_Root_Test CAVA_Base: theory Deriving.Derive Pre_BZ: theory Polynomial_Interpolation.Newton_Interpolation CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base Pre_BZ: theory Show.Show_Poly Pre_BZ: theory Polynomial_Interpolation.Polynomial_Interpolation Pre_BZ: theory Polynomial_Factorization.Kronecker_Factorization Pre_BZ: theory Polynomial_Factorization.Rational_Factorization Timing Sepref_Basic (2 threads, 23.516s elapsed time, 41.628s cpu time, 1.416s GC time, factor 1.77) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sepref_Basic Finished Sepref_Basic (0:00:51 elapsed time, 0:01:17 cpu time, factor 1.49) Building Sepref_IICF ... Sepref_IICF: theory Refine_Imperative_HOL.IICF_List Sepref_IICF: theory Refine_Imperative_HOL.IICF_Map Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Map Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_List Sepref_IICF: theory Refine_Imperative_HOL.IICF_HOL_List Sepref_IICF: theory Refine_Imperative_HOL.IICF_MS_Array_List Sepref_IICF: theory Refine_Imperative_HOL.IICF_Matrix Timing CAVA_Base (2 threads, 8.647s elapsed time, 15.820s cpu time, 0.692s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_Base Finished CAVA_Base (0:00:34 elapsed time, 0:00:49 cpu time, factor 1.44) Building CAVA_Automata ... Sepref_IICF: theory Refine_Imperative_HOL.IICF_Indexed_Array_List CAVA_Automata: theory CAVA_Automata.Step_Conv CAVA_Automata: theory CAVA_Automata.Digraph Sepref_IICF: theory Refine_Imperative_HOL.IICF_Multiset Sepref_IICF: theory Refine_Imperative_HOL.IICF_Array_Matrix CAVA_Automata: theory CAVA_Automata.Automata Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_Mset CAVA_Automata: theory CAVA_Automata.Digraph_Impl Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_MsetO Sepref_IICF: theory Refine_Imperative_HOL.IICF_Prio_Bag Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heap Sepref_IICF: theory Refine_Imperative_HOL.IICF_Abs_Heapmap Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heap Sepref_IICF: theory Refine_Imperative_HOL.IICF_Impl_Heapmap CAVA_Automata: theory CAVA_Automata.Lasso CAVA_Automata: theory CAVA_Automata.Simulation CAVA_Automata: theory CAVA_Automata.Stuttering_Extension Sepref_IICF: theory Refine_Imperative_HOL.IICF_Set Sepref_IICF: theory Refine_Imperative_HOL.IICF_List_SetO Sepref_IICF: theory Refine_Imperative_HOL.IICF_Sepl_Binding Timing Network_Security_Policy_Verification (2 threads, 376.798s elapsed time, 716.312s cpu time, 51.336s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Network_Security_Policy_Verification Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Network_Security_Policy_Verification/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Network_Security_Policy_Verification/outline.pdf Finished Network_Security_Policy_Verification (0:06:25 elapsed time, 0:12:09 cpu time, factor 1.89) Running Stochastic_Matrices ... Stochastic_Matrices: theory HOL-Eisbach.Eisbach Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field Stochastic_Matrices: theory HOL-Library.Bit Stochastic_Matrices: theory HOL-Algebra.Congruence Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction Stochastic_Matrices: theory HOL-Library.Function_Algebras Stochastic_Matrices: theory HOL-Algebra.Order Stochastic_Matrices: theory HOL-Library.More_List Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial Sepref_IICF: theory Refine_Imperative_HOL.IICF Stochastic_Matrices: theory HOL-Algebra.Lattice CAVA_Automata: theory CAVA_Automata.Automata_Impl Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice Stochastic_Matrices: theory HOL-Algebra.Group Stochastic_Matrices: theory HOL-Algebra.Coset Stochastic_Matrices: theory HOL-Algebra.FiniteProduct Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph Stochastic_Matrices: theory HOL-Algebra.Ring Refine_Imperative_HOL: theory Collections_Examples.Buchi_Graph_Basic Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted Stochastic_Matrices: theory HOL-Algebra.Module Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Permutations Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra Stochastic_Matrices: theory Rank_Nullity_Theorem.Generalizations Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet Stochastic_Matrices: theory Jordan_Normal_Form.Matrix Timing HOL-ODE-Refinement (2 threads, 644.321s elapsed time, 1038.476s cpu time, 77.532s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE-Refinement Finished HOL-ODE-Refinement (0:11:55 elapsed time, 0:19:57 cpu time, factor 1.67) Building HOL-ODE-Numerics ... HOL-ODE-Numerics: theory Collections.ICF_Tools HOL-ODE-Numerics: theory HOL-Library.Parallel HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc HOL-ODE-Numerics: theory Collections.Locale_Code HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations Stochastic_Matrices: theory Jordan_Normal_Form.Determinant Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form Stochastic_Matrices: theory VectorSpace.FunctionLemmas Stochastic_Matrices: theory VectorSpace.RingModuleFacts Stochastic_Matrices: theory VectorSpace.MonoidSums Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous Stochastic_Matrices: theory VectorSpace.LinearCombinations Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata Stochastic_Matrices: theory VectorSpace.SumSpaces Stochastic_Matrices: theory VectorSpace.VectorSpace HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Timing CAVA_Automata (2 threads, 69.882s elapsed time, 97.052s cpu time, 5.352s GC time, factor 1.39) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_Automata Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_Automata/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_Automata/outline.pdf Finished CAVA_Automata (0:01:44 elapsed time, 0:02:29 cpu time, factor 1.43) Timing Pre_BZ (2 threads, 124.602s elapsed time, 205.924s cpu time, 8.756s GC time, factor 1.65) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_BZ Finished Pre_BZ (0:02:46 elapsed time, 0:04:49 cpu time, factor 1.74) Building LTL_to_GBA ... Building Berlekamp_Zassenhaus ... Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype LTL_to_GBA: theory HOL-Library.Countable_Set LTL_to_GBA: theory LTL.LTL LTL_to_GBA: theory HOL-Library.Countable_Complete_Lattices Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Missing_Multiset2 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd LTL_to_GBA: theory HOL-Library.Order_Continuity Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound LTL_to_GBA: theory HOL-Library.Extended_Nat Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux LTL_to_GBA: theory Stuttering_Equivalence.Samplers LTL_to_GBA: theory Stuttering_Equivalence.StutterEquivalence Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius Timing Sepref_IICF (2 threads, 81.951s elapsed time, 138.844s cpu time, 4.264s GC time, factor 1.69) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Sepref_IICF Finished Sepref_IICF (0:02:00 elapsed time, 0:03:22 cpu time, factor 1.68) Building Maxflow_Lib ... Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based LTL_to_GBA: theory LTL.LTL_Rewrite Maxflow_Lib: theory CAVA_Base.Statistics Maxflow_Lib: theory HOL-Library.Char_ord Maxflow_Lib: theory DFS_Framework.DFS_Framework_Misc Maxflow_Lib: theory Program-Conflict-Analysis.LTS Maxflow_Lib: theory HOL-Library.Code_Char Maxflow_Lib: theory CAVA_Base.Code_String Maxflow_Lib: theory DFS_Framework.DFS_Framework_Refine_Aux Maxflow_Lib: theory CAVA_Base.CAVA_Code_Target Maxflow_Lib: theory CAVA_Base.CAVA_Base Maxflow_Lib: theory Maxflow_Lib.Fofu_Abs_Base LTL_to_GBA: theory Stuttering_Equivalence.PLTL Maxflow_Lib: theory CAVA_Automata.Digraph Maxflow_Lib: theory DFS_Framework.Impl_Rev_Array_Stack LTL_to_GBA: theory LTL_to_GBA.LTL_Stutter Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark Timing Iptables_Semantics (2 threads, 247.192s elapsed time, 451.152s cpu time, 29.940s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics/outline.pdf Finished Iptables_Semantics (0:05:11 elapsed time, 0:09:43 cpu time, factor 1.87) Running Iptables_Semantics_Examples ... Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests Maxflow_Lib: theory CAVA_Automata.Digraph_Impl Maxflow_Lib: theory DFS_Framework.Param_DFS Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based Maxflow_Lib: theory DFS_Framework.DFS_Invars_Basic Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company Maxflow_Lib: theory DFS_Framework.General_DFS_Structure LTL_to_GBA: theory LTL_to_GBA.LTL_to_GBA_impl Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod Maxflow_Lib: theory DFS_Framework.Rec_Impl Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl Maxflow_Lib: theory DFS_Framework.Tailrec_Impl Maxflow_Lib: theory Refine_Imperative_HOL.Sepref_ICF_Bindings Maxflow_Lib: theory DFS_Framework.Simple_Impl Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting Maxflow_Lib: theory Maxflow_Lib.Fofu_Impl_Base Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples Maxflow_Lib: theory DFS_Framework.Restr_Impl Maxflow_Lib: theory Maxflow_Lib.Refine_Add_Fofu Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based Maxflow_Lib: theory DFS_Framework.DFS_Framework Maxflow_Lib: theory DFS_Framework.Reachable_Nodes Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly Timing Refine_Imperative_HOL (2 threads, 283.035s elapsed time, 429.204s cpu time, 18.348s GC time, factor 1.52) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Imperative_HOL Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Imperative_HOL/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Refine_Imperative_HOL/outline.pdf Finished Refine_Imperative_HOL (0:05:45 elapsed time, 0:11:36 cpu time, factor 2.02) Running DFS_Framework ... DFS_Framework: theory DFS_Framework.DFS_Framework_Misc DFS_Framework: theory DFS_Framework.On_Stack DFS_Framework: theory DFS_Framework.DFS_Framework_Refine_Aux DFS_Framework: theory DFS_Framework.Impl_Rev_Array_Stack DFS_Framework: theory DFS_Framework.DFS_Chapter_Framework DFS_Framework: theory DFS_Framework.DFS_Chapter_Examples DFS_Framework: theory DFS_Framework.Param_DFS DFS_Framework: theory DFS_Framework.DFS_Invars_Basic DFS_Framework: theory DFS_Framework.General_DFS_Structure DFS_Framework: theory DFS_Framework.DFS_Invars_SCC DFS_Framework: theory DFS_Framework.Rec_Impl DFS_Framework: theory DFS_Framework.Tailrec_Impl DFS_Framework: theory DFS_Framework.Simple_Impl DFS_Framework: theory DFS_Framework.Restr_Impl DFS_Framework: theory DFS_Framework.DFS_Framework DFS_Framework: theory DFS_Framework.Cyc_Check DFS_Framework: theory DFS_Framework.DFS_Find_Path Timing Formal_SSA (2 threads, 368.694s elapsed time, 527.180s cpu time, 14.564s GC time, factor 1.43) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Formal_SSA Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Formal_SSA/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Formal_SSA/outline.pdf Finished Formal_SSA (0:08:00 elapsed time, 0:11:04 cpu time, factor 1.38) Running Modal_Logics_for_NTS ... Modal_Logics_for_NTS: theory HOL-Cardinals.Fun_More Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Relation_More Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Union Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Extension Modal_Logics_for_NTS: theory HOL-Cardinals.Wellfounded_More Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Relation Modal_Logics_for_NTS: theory HOL-Library.Cardinal_Notations Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FS_Set Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Embedding Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Wellfounded Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Residual Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Constructions Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Transition_System Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Transition_System Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Order_Relation Modal_Logics_for_NTS: theory HOL-Cardinals.Ordinal_Arithmetic Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Arithmetic Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Transition_System Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinals Modal_Logics_for_NTS: theory HOL-Cardinals.Bounded_Set Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Bounded_Set Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Formula Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Formula Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Validity Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Logical_Equivalence Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Validity Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity Timing Maxflow_Lib (2 threads, 134.849s elapsed time, 241.196s cpu time, 10.340s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Maxflow_Lib Finished Maxflow_Lib (0:03:06 elapsed time, 0:05:27 cpu time, factor 1.76) Building Flow_Networks ... Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Formula Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Logical_Equivalence Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Validity Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.L_Transform Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Logical_Equivalence Flow_Networks: theory Flow_Networks.Graph Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity Flow_Networks: theory Flow_Networks.Network Flow_Networks: theory Flow_Networks.Residual_Graph Flow_Networks: theory Flow_Networks.Augmenting_Flow Flow_Networks: theory Flow_Networks.Augmenting_Path Flow_Networks: theory Flow_Networks.Ford_Fulkerson Flow_Networks: theory Flow_Networks.Graph_Impl Flow_Networks: theory Flow_Networks.Network_Impl Flow_Networks: theory Flow_Networks.NetCheck DFS_Framework: theory DFS_Framework.Nested_DFS DFS_Framework: theory DFS_Framework.Reachable_Nodes LTL_to_GBA: theory LTL_to_GBA.All_Of_LTL_to_GBA HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis Timing Berlekamp_Zassenhaus (2 threads, 179.311s elapsed time, 301.588s cpu time, 14.620s GC time, factor 1.68) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/outline.pdf Finished Berlekamp_Zassenhaus (0:04:42 elapsed time, 0:07:09 cpu time, factor 1.52) Building Pre_Algebraic_Numbers ... DFS_Framework: theory DFS_Framework.Tarjan_LowLink DFS_Framework: theory DFS_Framework.Tarjan Timing Flow_Networks (2 threads, 51.236s elapsed time, 69.528s cpu time, 2.656s GC time, factor 1.36) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Flow_Networks Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Flow_Networks/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Flow_Networks/outline.pdf Finished Flow_Networks (0:01:30 elapsed time, 0:02:24 cpu time, factor 1.60) Running Containers-Benchmarks ... Containers-Benchmarks: theory HOL-Eisbach.Eisbach Containers-Benchmarks: theory Automatic_Refinement.Foldi Containers-Benchmarks: theory Automatic_Refinement.Prio_List Containers-Benchmarks: theory Automatic_Refinement.Refine_Util_Bootstrap1 Containers-Benchmarks: theory Automatic_Refinement.Mk_Term_Antiquot Containers-Benchmarks: theory Automatic_Refinement.Mpat_Antiquot Containers-Benchmarks: theory Collections.ICF_Tools Containers-Benchmarks: theory Automatic_Refinement.Refine_Util Containers-Benchmarks: theory Collections.Ord_Code_Preproc Containers-Benchmarks: theory Collections.Locale_Code Containers-Benchmarks: theory Collections.Record_Intf Pre_Algebraic_Numbers: theory Deriving.Compare_Real Pre_Algebraic_Numbers: theory Deriving.Compare_Rat Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Comparison Containers-Benchmarks: theory Automatic_Refinement.Anti_Unification Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace Containers-Benchmarks: theory Automatic_Refinement.Attr_Comb Containers-Benchmarks: theory Automatic_Refinement.Named_Sorted_Thms Containers-Benchmarks: theory Automatic_Refinement.Autoref_Data Containers-Benchmarks: theory Automatic_Refinement.Indep_Vars Containers-Benchmarks: theory Automatic_Refinement.Mk_Record_Simp Containers-Benchmarks: theory Automatic_Refinement.Tagged_Solver Pre_Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial Pre_Algebraic_Numbers: theory Show.Show_Real Containers-Benchmarks: theory Automatic_Refinement.Select_Solve Containers-Benchmarks: theory Finger-Trees.FingerTree Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF Pre_Algebraic_Numbers: theory Show.Show_Complex Pre_Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library Containers-Benchmarks: theory Trie.Trie Pre_Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models Containers-Benchmarks: theory Binomial-Heaps.BinomialHeap Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius Containers-Benchmarks: theory Binomial-Heaps.SkewBinomialHeap Timing Stochastic_Matrices (2 threads, 382.104s elapsed time, 607.328s cpu time, 24.784s GC time, factor 1.59) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stochastic_Matrices Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stochastic_Matrices/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stochastic_Matrices/outline.pdf Finished Stochastic_Matrices (0:06:27 elapsed time, 0:10:16 cpu time, factor 1.59) Running LOFT ... LOFT: theory LOFT.OpenFlow_Helpers LOFT: theory LOFT.Sort_Descending Containers-Benchmarks: theory HOL-ex.Quicksort LOFT: theory LOFT.List_Group DFS_Framework: theory DFS_Framework.Feedback_Arcs Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Default Containers-Benchmarks: theory Automatic_Refinement.Misc LOFT: theory LOFT.OpenFlow_Matches LOFT: theory LOFT.Semantics_OpenFlow Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_RBT LOFT: theory LOFT.Featherweight_OpenFlow_Comparison Containers-Benchmarks: theory Collections.DatRef Containers-Benchmarks: theory Native_Word.Code_Target_Bits_Int Containers-Benchmarks: theory Collections.Code_Target_ICF Containers-Benchmarks: theory Automatic_Refinement.Digraph_Basic Containers-Benchmarks: theory Collections.SetIterator Containers-Benchmarks: theory Automatic_Refinement.Refine_Lib LOFT: theory LOFT.OpenFlow_Action Containers-Benchmarks: theory Collections.SetIteratorOperations Containers-Benchmarks: theory Automatic_Refinement.Autoref_Phases Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tagging Containers-Benchmarks: theory Automatic_Refinement.Relators LOFT: theory LOFT.OpenFlow_Serialize Containers-Benchmarks: theory Automatic_Refinement.Param_Tool Containers-Benchmarks: theory Automatic_Refinement.Param_HOL Containers-Benchmarks: theory Collections.Assoc_List Containers-Benchmarks: theory Collections.Trie_Impl Containers-Benchmarks: theory Automatic_Refinement.Parametricity Containers-Benchmarks: theory Automatic_Refinement.Autoref_Id_Ops Containers-Benchmarks: theory Collections.Diff_Array Containers-Benchmarks: theory Automatic_Refinement.Autoref_Fix_Rel LOFT: theory LOFT.LinuxRouter_OpenFlow_Translation Containers-Benchmarks: theory Automatic_Refinement.Autoref_Translate Containers-Benchmarks: theory Automatic_Refinement.Autoref_Relator_Interface Containers-Benchmarks: theory Automatic_Refinement.Autoref_Gen_Algo Containers-Benchmarks: theory Collections.Trie2 Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tool Containers-Benchmarks: theory Collections.Dlist_add Containers-Benchmarks: theory Collections.Proper_Iterator Containers-Benchmarks: theory Collections.It_to_It Containers-Benchmarks: theory Collections.SetIteratorGA Containers-Benchmarks: theory Automatic_Refinement.Autoref_Bindings_HOL Containers-Benchmarks: theory Collections.Sorted_List_Operations LOFT: theory LOFT.OpenFlow_Documentation LOFT: theory LOFT.OF_conv_test Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set LOFT: theory LOFT.RFC2544 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_Default Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Bool Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_LC Containers-Benchmarks: theory Automatic_Refinement.Automatic_Refinement Containers-Benchmarks: theory Collections.Idx_Iterator Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_LC Timing LTL_to_GBA (2 threads, 270.414s elapsed time, 461.644s cpu time, 18.356s GC time, factor 1.71) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_GBA Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_GBA/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_GBA/outline.pdf Finished LTL_to_GBA (0:05:31 elapsed time, 0:09:07 cpu time, factor 1.65) Building CAVA_buildchain1 ... Containers-Benchmarks: theory Containers-Benchmarks.Clauses Containers-Benchmarks: theory Refine_Monadic.Refine_Chapter Containers-Benchmarks: theory Refine_Monadic.Refine_Mono_Prover Containers-Benchmarks: theory Refine_Monadic.Refine_Misc CAVA_buildchain1: theory Gabow_SCC.Gabow_Skeleton CAVA_buildchain1: theory Gabow_SCC.Find_Path CAVA_buildchain1: theory Gabow_SCC.Find_Path_Impl Containers-Benchmarks: theory Refine_Monadic.RefineG_Domain Containers-Benchmarks: theory Refine_Monadic.RefineG_Transfer Timing Pre_Algebraic_Numbers (2 threads, 13.607s elapsed time, 24.272s cpu time, 0.636s GC time, factor 1.78) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Algebraic_Numbers Finished Pre_Algebraic_Numbers (0:00:51 elapsed time, 0:01:13 cpu time, factor 1.43) Building Algebraic_Numbers_Lib ... Containers-Benchmarks: theory Refine_Monadic.RefineG_Assert Containers-Benchmarks: theory Refine_Monadic.RefineG_Recursion Containers-Benchmarks: theory Refine_Monadic.RefineG_While Containers-Benchmarks: theory Refine_Monadic.Refine_Basic Containers-Benchmarks: theory Refine_Monadic.Refine_Det CAVA_buildchain1: theory Gabow_SCC.Gabow_SCC Containers-Benchmarks: theory Refine_Monadic.Refine_Heuristics Containers-Benchmarks: theory Refine_Monadic.Refine_Leof Containers-Benchmarks: theory Refine_Monadic.Refine_Pfun Containers-Benchmarks: theory Refine_Monadic.Refine_More_Comb Containers-Benchmarks: theory Refine_Monadic.Refine_While CAVA_buildchain1: theory Gabow_SCC.Gabow_GBG Algebraic_Numbers_Lib: theory Algebraic_Numbers.Compare_Complex Algebraic_Numbers_Lib: theory Algebraic_Numbers.Complex_Roots_Real_Poly Containers-Benchmarks: theory Refine_Monadic.Refine_Transfer Containers-Benchmarks: theory Refine_Monadic.Autoref_Monadic Containers-Benchmarks: theory Refine_Monadic.Refine_Automation Containers-Benchmarks: theory Refine_Monadic.Refine_Foreach Algebraic_Numbers_Lib: theory Algebraic_Numbers.Bivariate_Polynomials Algebraic_Numbers_Lib: theory Algebraic_Numbers.Algebraic_Numbers_Prelim DFS_Framework: theory DFS_Framework.DFS_All_Examples Algebraic_Numbers_Lib: theory Algebraic_Numbers.Resultant Algebraic_Numbers_Lib: theory Algebraic_Numbers.Interval_Arithmetic Containers-Benchmarks: theory Refine_Monadic.Refine_Monadic Containers-Benchmarks: theory Collections.Gen_Iterator Containers-Benchmarks: theory Collections.Intf_Map Containers-Benchmarks: theory Collections.Intf_Set Containers-Benchmarks: theory Collections.Iterator Algebraic_Numbers_Lib: theory Algebraic_Numbers.Algebraic_Numbers Containers-Benchmarks: theory Collections.Array_Iterator CAVA_buildchain1: theory Gabow_SCC.Gabow_Skeleton_Code Containers-Benchmarks: theory Collections.ICF_Spec_Base Containers-Benchmarks: theory Collections.RBT_add Containers-Benchmarks: theory Collections.AnnotatedListSpec Algebraic_Numbers_Lib: theory Algebraic_Numbers.Sturm_Rat Containers-Benchmarks: theory Collections.ListSpec Containers-Benchmarks: theory Collections.FTAnnotatedListImpl Containers-Benchmarks: theory Collections.ListGA Containers-Benchmarks: theory Collections.Fifo Containers-Benchmarks: theory Collections.MapSpec Containers-Benchmarks: theory Collections.PrioSpec Containers-Benchmarks: theory Collections.BinoPrioImpl Containers-Benchmarks: theory Collections.PrioByAnnotatedList Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Algebraic_Numbers Containers-Benchmarks: theory Collections.SkewPrioImpl Containers-Benchmarks: theory Collections.FTPrioImpl Containers-Benchmarks: theory Collections.PrioUniqueSpec Containers-Benchmarks: theory Collections.SetSpec Containers-Benchmarks: theory Collections.PrioUniqueByAnnotatedList Containers-Benchmarks: theory Collections.FTPrioUniqueImpl Containers-Benchmarks: theory Collections.Algos Containers-Benchmarks: theory Collections.SetIndex Containers-Benchmarks: theory Collections.SetIteratorCollectionsGA Containers-Benchmarks: theory Collections.MapGA Containers-Benchmarks: theory Collections.SetGA Containers-Benchmarks: theory Collections.ArrayMapImpl Containers-Benchmarks: theory Collections.ListMapImpl Containers-Benchmarks: theory Collections.ListMapImpl_Invar Containers-Benchmarks: theory Collections.ArrayHashMap_Impl Containers-Benchmarks: theory Collections.TrieMapImpl Containers-Benchmarks: theory Collections.ListSetImpl Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Roots Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Alg Containers-Benchmarks: theory Collections.ArrayHashMap Containers-Benchmarks: theory Collections.ListSetImpl_Invar Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Approx Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Precise Algebraic_Numbers_Lib: theory Algebraic_Numbers.Complex_Algebraic_Numbers Containers-Benchmarks: theory Collections.ListSetImpl_NotDist Containers-Benchmarks: theory Collections.ListSetImpl_Sorted Containers-Benchmarks: theory Collections.SetByMap CAVA_buildchain1: theory Gabow_SCC.Gabow_GBG_Code Containers-Benchmarks: theory Collections.RBTMapImpl Containers-Benchmarks: theory Collections.ArrayHashSet Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Factorization CAVA_buildchain1: theory Gabow_SCC.Gabow_SCC_Code Containers-Benchmarks: theory Collections.ArraySetImpl Containers-Benchmarks: theory Collections.TrieSetImpl Containers-Benchmarks: theory Collections.HashMap_Impl Containers-Benchmarks: theory Collections.RBTSetImpl Containers-Benchmarks: theory Collections.HashMap Containers-Benchmarks: theory Collections.HashSet Containers-Benchmarks: theory Collections.MapStdImpl Containers-Benchmarks: theory Collections.SetStdImpl Containers-Benchmarks: theory Collections.ICF_Impl Containers-Benchmarks: theory Collections.ICF_Refine_Monadic Containers-Benchmarks: theory Collections.ICF_Autoref Containers-Benchmarks: theory Collections.Collections Containers-Benchmarks: theory Collections.CollectionsV1 Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_ICF Timing DFS_Framework (2 threads, 262.990s elapsed time, 463.952s cpu time, 20.144s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/DFS_Framework Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/DFS_Framework/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/DFS_Framework/outline.pdf Finished DFS_Framework (0:04:31 elapsed time, 0:09:01 cpu time, factor 2.00) Running Algebraic_Numbers ... Timing Modal_Logics_for_NTS (2 threads, 221.879s elapsed time, 351.172s cpu time, 18.268s GC time, factor 1.58) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Modal_Logics_for_NTS Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Modal_Logics_for_NTS/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Modal_Logics_for_NTS/outline.pdf Finished Modal_Logics_for_NTS (0:03:49 elapsed time, 0:06:02 cpu time, factor 1.58) Running Dependent_SIFUM_Refinement ... Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.CompositionalRefinement Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim Algebraic_Numbers: theory Algebraic_Numbers.Resultant Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg2 Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.EgHighBranchRevC Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1 Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers CAVA_buildchain1: theory Gabow_SCC.All_Of_Gabow_SCC Algebraic_Numbers: theory Algebraic_Numbers.Real_Factorization Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial Timing Algebraic_Numbers_Lib (2 threads, 74.162s elapsed time, 136.024s cpu time, 5.904s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers_Lib Finished Algebraic_Numbers_Lib (0:02:14 elapsed time, 0:03:28 cpu time, factor 1.55) Building Pre_Perron_Frobenius ... Pre_Perron_Frobenius: theory HOL-Eisbach.Eisbach Pre_Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable Pre_Perron_Frobenius: theory HOL-Analysis.Inner_Product Pre_Perron_Frobenius: theory HOL-Analysis.L2_Norm Pre_Perron_Frobenius: theory HOL-Analysis.Operator_Norm Pre_Perron_Frobenius: theory HOL-Analysis.Norm_Arith Pre_Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order Pre_Perron_Frobenius: theory HOL-Analysis.Product_Vector Pre_Perron_Frobenius: theory HOL-Analysis.Euclidean_Space Pre_Perron_Frobenius: theory HOL-Analysis.Linear_Algebra Pre_Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product Pre_Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests Timing Containers-Benchmarks (2 threads, 203.083s elapsed time, 382.912s cpu time, 34.380s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Containers-Benchmarks Finished Containers-Benchmarks (0:03:25 elapsed time, 0:06:25 cpu time, factor 1.87) Building Linear_Recurrences ... Pre_Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function Pre_Perron_Frobenius: theory HOL-Analysis.Connected Pre_Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits Pre_Perron_Frobenius: theory HOL-Analysis.Summation_Tests Timing LOFT (2 threads, 185.361s elapsed time, 324.404s cpu time, 13.248s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LOFT Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LOFT/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LOFT/outline.pdf Finished LOFT (0:03:13 elapsed time, 0:05:44 cpu time, factor 1.78) Running Promela ... Pre_Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space Pre_Perron_Frobenius: theory HOL-Analysis.Uniform_Limit Promela: theory Promela.PromelaStatistics Promela: theory HOL-Library.IArray Promela: theory Promela.Lexord_List Promela: theory Promela.PromelaAST Pre_Perron_Frobenius: theory HOL-Analysis.Starlike Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials Linear_Recurrences: theory Linear_Recurrences.Factorizations Linear_Recurrences: theory Linear_Recurrences.RatFPS Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver Pre_Perron_Frobenius: theory HOL-Analysis.Continuous_Extension Pre_Perron_Frobenius: theory HOL-Analysis.Path_Connected Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Solver Pre_Perron_Frobenius: theory HOL-Analysis.Homeomorphism Pre_Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint Pre_Perron_Frobenius: theory HOL-Analysis.Derivative Timing CAVA_buildchain1 (2 threads, 133.968s elapsed time, 249.232s cpu time, 9.648s GC time, factor 1.86) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_buildchain1 Finished CAVA_buildchain1 (0:02:59 elapsed time, 0:05:28 cpu time, factor 1.83) Building CAVA_buildchain3 ... Pre_Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space CAVA_buildchain3: theory HOL-Library.IArray CAVA_buildchain3: theory Promela.Lexord_List CAVA_buildchain3: theory Promela.PromelaAST CAVA_buildchain3: theory Promela.PromelaStatistics Pre_Perron_Frobenius: theory HOL-Analysis.Determinants Pre_Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type Pre_Perron_Frobenius: theory Rank_Nullity_Theorem.Generalizations Pre_Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous Promela: theory Promela.PromelaDatastructures CAVA_buildchain3: theory Promela.PromelaDatastructures Timing Linear_Recurrences (2 threads, 15.777s elapsed time, 31.096s cpu time, 1.592s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences/outline.pdf Finished Linear_Recurrences (0:01:05 elapsed time, 0:01:37 cpu time, factor 1.48) Running Linear_Recurrences_Test ... Linear_Recurrences_Test: theory Linear_Recurrences_Test.Eulerian_Polynomials Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Common Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Misc Linear_Recurrences_Test: theory Linear_Recurrences_Test.Pochhammer_Polynomials Linear_Recurrences_Test: theory Linear_Recurrences_Test.Factorizations Linear_Recurrences_Test: theory Linear_Recurrences_Test.RatFPS Linear_Recurrences_Test: theory Linear_Recurrences_Test.Partial_Fraction_Decomposition Linear_Recurrences_Test: theory Linear_Recurrences_Test.Rational_FPS_Solver Linear_Recurrences_Test: theory Linear_Recurrences_Test.Show_RatFPS Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Homogenous_Recurrences Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Pretty Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Inhomogenous_Recurrences Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Solver Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Test Promela: theory Promela.PromelaInvariants Timing Dependent_SIFUM_Refinement (2 threads, 183.045s elapsed time, 300.792s cpu time, 11.156s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement/outline.pdf Finished Dependent_SIFUM_Refinement (0:03:08 elapsed time, 0:05:10 cpu time, factor 1.64) Running Isabelle_Meta_Model ... Promela: theory Promela.Promela Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Cartouche_Examples Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_code_runtime Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main0 Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_code_target Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_typedecl Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main2 Isabelle_Meta_Model: theory Isabelle_Meta_Model.Isabelle_Main1 Isabelle_Meta_Model: theory Isabelle_Meta_Model.Init Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Pure Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_SML Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_init Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Pure Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_init Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Pure Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Isabelle Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_SML CAVA_buildchain3: theory Promela.PromelaInvariants CAVA_buildchain3: theory Promela.Promela Timing Iptables_Semantics_Examples (2 threads, 596.713s elapsed time, 1164.084s cpu time, 96.996s GC time, factor 1.95) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics_Examples Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics_Examples/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf Finished Iptables_Semantics_Examples (0:10:03 elapsed time, 0:19:34 cpu time, factor 1.95) Running LTL_to_DRA ... LTL_to_DRA: theory KBPs.DFS LTL_to_DRA: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers LTL_to_DRA: theory LTL_to_DRA.LTL_FGXU LTL_to_DRA: theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping LTL_to_DRA: theory LTL_to_DRA.Map2 LTL_to_DRA: theory LTL_to_DRA.Mapping2 LTL_to_DRA: theory LTL_to_DRA.DTS LTL_to_DRA: theory LTL_to_DRA.LTL_Compat LTL_to_DRA: theory LTL_to_DRA.LTL_Impl LTL_to_DRA: theory LTL_to_DRA.Preliminaries2 LTL_to_DRA: theory LTL_to_DRA.Rabin LTL_to_DRA: theory LTL_to_DRA.Semi_Mojmir LTL_to_DRA: theory List-Index.List_Index LTL_to_DRA: theory LTL_to_DRA.List2 Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Isabelle LTL_to_DRA: theory LTL_to_DRA.af LTL_to_DRA: theory LTL_to_DRA.Mojmir LTL_to_DRA: theory LTL_to_DRA.Mojmir_Rabin LTL_to_DRA: theory LTL_to_DRA.Logical_Characterization LTL_to_DRA: theory LTL_to_DRA.Mojmir_Rabin_Impl LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin Isabelle_Meta_Model: theory Isabelle_Meta_Model.Init_rbt Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Toy_extended LTL_to_DRA: theory LTL_to_DRA.af_Impl Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_Toy LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin_Unfold_Opt Promela: theory Promela.PromelaLTL Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Toy_extended Isabelle_Meta_Model: theory Isabelle_Meta_Model.Toy_Library_Static Promela: theory Promela.PromelaLTLConv LTL_to_DRA: theory LTL_to_DRA.LTL_Rabin_Impl CAVA_buildchain3: theory Promela.PromelaLTL Isabelle_Meta_Model: theory Isabelle_Meta_Model.Meta_META Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_Toy Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Toy LTL_to_DRA: theory LTL_to_DRA.Export_Code Promela: theory Promela.All_Of_Promela Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_Toy_extended CAVA_buildchain3: theory Promela.PromelaLTLConv Timing Promela (2 threads, 161.237s elapsed time, 265.468s cpu time, 15.620s GC time, factor 1.65) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Promela Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Promela/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Promela/outline.pdf Finished Promela (0:02:48 elapsed time, 0:04:47 cpu time, factor 1.71) Running Prpu_Maxflow ... Isabelle_Meta_Model: theory Isabelle_Meta_Model.Parser_META Isabelle_Meta_Model: theory Isabelle_Meta_Model.Core_init CAVA_buildchain3: theory Promela.All_Of_Promela Prpu_Maxflow: theory Prpu_Maxflow.Graph_Topological_Ordering Prpu_Maxflow: theory Prpu_Maxflow.Generic_Push_Relabel Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer_META Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_access Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_ctxt Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_examp Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor1_infra Isabelle_Meta_Model: theory Isabelle_Meta_Model.Floor2_examp Isabelle_Meta_Model: theory Isabelle_Meta_Model.Core Isabelle_Meta_Model: theory Isabelle_Meta_Model.Printer Isabelle_Meta_Model: theory Isabelle_Meta_Model.Generator_dynamic Isabelle_Meta_Model: theory Isabelle_Meta_Model.Toy_Library Isabelle_Meta_Model: theory Isabelle_Meta_Model.Generator_static Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Inst Prpu_Maxflow: theory Prpu_Maxflow.Prpu_Common_Impl Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front Isabelle_Meta_Model: theory Isabelle_Meta_Model.Rail Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_deep Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_shallow Prpu_Maxflow: theory Prpu_Maxflow.Fifo_Push_Relabel_Impl Prpu_Maxflow: theory Prpu_Maxflow.Relabel_To_Front_Impl Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_generated_generated Isabelle_Meta_Model: theory Isabelle_Meta_Model.Design_generated Timing Isabelle_Meta_Model (2 threads, 155.336s elapsed time, 233.548s cpu time, 18.608s GC time, factor 1.50) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Isabelle_Meta_Model Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Isabelle_Meta_Model/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Isabelle_Meta_Model/outline.pdf Finished Isabelle_Meta_Model (0:02:42 elapsed time, 0:04:06 cpu time, factor 1.52) Running Gabow_SCC ... Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton Gabow_SCC: theory Gabow_SCC.Find_Path Gabow_SCC: theory Gabow_SCC.Find_Path_Impl Gabow_SCC: theory Gabow_SCC.Gabow_SCC Gabow_SCC: theory Gabow_SCC.Gabow_GBG Timing Pre_Perron_Frobenius (2 threads, 254.569s elapsed time, 436.892s cpu time, 17.288s GC time, factor 1.72) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Perron_Frobenius Finished Pre_Perron_Frobenius (0:05:02 elapsed time, 0:08:19 cpu time, factor 1.65) Running Dirichlet_L ... Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order Dirichlet_L: theory HOL-Library.Lattice_Algebras Timing Linear_Recurrences_Test (2 threads, 208.271s elapsed time, 385.500s cpu time, 46.452s GC time, factor 1.85) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences_Test Finished Linear_Recurrences_Test (0:03:38 elapsed time, 0:06:35 cpu time, factor 1.81) Timing LTL_to_DRA (2 threads, 150.676s elapsed time, 261.332s cpu time, 21.760s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_DRA Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_DRA/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/LTL_to_DRA/outline.pdf Finished LTL_to_DRA (0:02:39 elapsed time, 0:04:36 cpu time, factor 1.73) Running List_Update ... Running Taylor_Models ... Dirichlet_L: theory HOL-Library.Log_Nat Dirichlet_L: theory Bernoulli.Bernoulli_Zeta List_Update: theory HOL-Library.While_Combinator List_Update: theory List_Update.Prob_Theory Taylor_Models: theory HOL-Decision_Procs.Rat_Pair Taylor_Models: theory HOL-Decision_Procs.Polynomial_List Dirichlet_L: theory Zeta_Function.Zeta_Function Gabow_SCC: theory Gabow_SCC.Gabow_Skeleton_Code List_Update: theory List_Update.Bit_Strings List_Update: theory List_Update.On_Off List_Update: theory List-Index.List_Index List_Update: theory List_Update.Inversion List_Update: theory List_Update.Swaps List_Update: theory Regular-Sets.Regular_Set List_Update: theory List_Update.Competitive_Analysis Dirichlet_L: theory HOL-Library.Float List_Update: theory List_Update.Move_to_Front Dirichlet_L: theory Lehmer.Lehmer Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate List_Update: theory Regular-Sets.Regular_Exp Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds List_Update: theory Regular-Sets.NDerivative List_Update: theory List_Update.MTF2_Effects Dirichlet_L: theory Bertrands_Postulate.Bertrand List_Update: theory List_Update.BIT List_Update: theory List_Update.Partial_Cost_Model List_Update: theory Regular-Sets.Equivalence_Checking List_Update: theory List_Update.RExp_Var List_Update: theory List_Update.List_Factoring Prpu_Maxflow: theory Prpu_Maxflow.Generated_Code_Test Taylor_Models: theory Taylor_Models.Polynomial_Expression List_Update: theory List_Update.OPT2 List_Update: theory List_Update.BIT_pairwise List_Update: theory List_Update.Phase_Partitioning List_Update: theory List_Update.BIT_2comp_on2 List_Update: theory List_Update.TS List_Update: theory List_Update.Comb Timing Algebraic_Numbers (2 threads, 379.202s elapsed time, 695.376s cpu time, 61.464s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf Finished Algebraic_Numbers (0:06:33 elapsed time, 0:11:54 cpu time, factor 1.82) Running Separation_Logic_Imperative_HOL ... Separation_Logic_Imperative_HOL: theory HOL-Eisbach.Eisbach Separation_Logic_Imperative_HOL: theory HOL-ex.Quicksort Separation_Logic_Imperative_HOL: theory HOL-Word.Bits Separation_Logic_Imperative_HOL: theory Automatic_Refinement.Misc Separation_Logic_Imperative_HOL: theory HOL-Word.Bits_Bit Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_Numeric Separation_Logic_Imperative_HOL: theory HOL-Word.Bit_Representation Separation_Logic_Imperative_HOL: theory HOL-Word.Bits_Int Separation_Logic_Imperative_HOL: theory HOL-Word.Bool_List_Representation Gabow_SCC: theory Gabow_SCC.Gabow_GBG_Code Separation_Logic_Imperative_HOL: theory Native_Word.More_Bits_Int Separation_Logic_Imperative_HOL: theory Native_Word.Bits_Integer Separation_Logic_Imperative_HOL: theory HOL-Word.Word_Miscellaneous Gabow_SCC: theory Gabow_SCC.Gabow_SCC_Code Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_Typedef Separation_Logic_Imperative_HOL: theory HOL-Word.Word Separation_Logic_Imperative_HOL: theory Native_Word.Word_Misc Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap Timing Prpu_Maxflow (2 threads, 145.932s elapsed time, 225.352s cpu time, 9.008s GC time, factor 1.54) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prpu_Maxflow Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prpu_Maxflow/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Prpu_Maxflow/outline.pdf Finished Prpu_Maxflow (0:02:34 elapsed time, 0:04:52 cpu time, factor 1.90) Running Propositional_Proof_Systems ... Taylor_Models: theory HOL-Library.Function_Algebras Taylor_Models: theory Taylor_Models.Float_Topology Taylor_Models: theory Taylor_Models.Interval Propositional_Proof_Systems: theory HOL-Library.Cancellation Propositional_Proof_Systems: theory HOL-Library.List_lexord Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad Propositional_Proof_Systems: theory HOL-Library.Nat_Bijection Taylor_Models: theory Taylor_Models.Taylor_Models_Misc Propositional_Proof_Systems: theory HOL-Library.Old_Datatype Propositional_Proof_Systems: theory HOL-Library.Multiset Propositional_Proof_Systems: theory HOL-Library.Simps_Case_Conv Propositional_Proof_Systems: theory HOL-Library.While_Combinator Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Array Propositional_Proof_Systems: theory HOL-Library.Countable Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Ref Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL Taylor_Models: theory Taylor_Models.Horner_Eval Taylor_Models: theory Taylor_Models.Interval_Approximation Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Syntax_Match Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Bits_Int Separation_Logic_Imperative_HOL: theory Native_Word.Uint32 Separation_Logic_Imperative_HOL: theory Collections.Code_Target_ICF Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF Timing CAVA_buildchain3 (2 threads, 158.728s elapsed time, 262.716s cpu time, 14.720s GC time, factor 1.66) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_buildchain3 Finished CAVA_buildchain3 (0:05:13 elapsed time, 0:07:35 cpu time, factor 1.45) Running CAVA_LTL_Modelchecker ... Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl Propositional_Proof_Systems: theory Propositional_Proof_Systems.Formulas Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional Separation_Logic_Imperative_HOL: theory Collections.HashCode CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Formulas Propositional_Proof_Systems: theory Propositional_Proof_Systems.HC Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniFormulas Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND Propositional_Proof_Systems: theory Propositional_Proof_Systems.NDHC Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_FiniteAssms Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC_Craig Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_To_Formula Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniSC_HC CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Abstract CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs Taylor_Models: theory Taylor_Models.Taylor_Models Propositional_Proof_Systems: theory Propositional_Proof_Systems.SCND Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Cut Propositional_Proof_Systems: theory Propositional_Proof_Systems.HCSC Propositional_Proof_Systems: theory Propositional_Proof_Systems.HCSCND CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.NDFS_SI Propositional_Proof_Systems: theory Propositional_Proof_Systems.LSC Propositional_Proof_Systems: theory Propositional_Proof_Systems.LSC_Resolution Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Depth Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Gentzen Propositional_Proof_Systems: theory Propositional_Proof_Systems.Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.CNF_Formulas_Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Sound Propositional_Proof_Systems: theory Propositional_Proof_Systems.Compactness Propositional_Proof_Systems: theory Propositional_Proof_Systems.Consistency Propositional_Proof_Systems: theory Propositional_Proof_Systems.Compactness_Consistency Propositional_Proof_Systems: theory Propositional_Proof_Systems.HC_Compl_Consistency Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_Consistency Propositional_Proof_Systems: theory Propositional_Proof_Systems.MiniFormulas_Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Sound Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_Truthtable Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_Truthtable_Compact Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.ND_Compl_SC Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_SC_Full Propositional_Proof_Systems: theory Propositional_Proof_Systems.Resolution_Compl_SC_Small Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Compl_Consistency Propositional_Proof_Systems: theory Propositional_Proof_Systems.SC_Depth_Limit Propositional_Proof_Systems: theory Propositional_Proof_Systems.Substitution Propositional_Proof_Systems: theory Propositional_Proof_Systems.Tseytin Propositional_Proof_Systems: theory Propositional_Proof_Systems.Substitution_Sema Propositional_Proof_Systems: theory Propositional_Proof_Systems.Sema_Craig Propositional_Proof_Systems: theory Propositional_Proof_Systems.Tseytin_Sema Taylor_Models: theory Taylor_Models.Experiments Separation_Logic_Imperative_HOL: theory Collections.Partial_Equivalence_Relation Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Run Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Assertions Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hoare_Triple Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Automation Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Main Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Table Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_List_Spec Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.List_Seg Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Circ_List Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Open_List Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Union_Find Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl Dirichlet_L: theory Dirichlet_L.Group_Adjoin Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Idioms Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.To_List_GA Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem Gabow_SCC: theory Gabow_SCC.All_Of_Gabow_SCC Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Blit Timing Dirichlet_L (2 threads, 124.203s elapsed time, 225.688s cpu time, 6.540s GC time, factor 1.82) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_L Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_L/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_L/outline.pdf Finished Dirichlet_L (0:02:10 elapsed time, 0:03:54 cpu time, factor 1.80) Running Abortable_Linearizable_Modules ... Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.Sequences Timing Gabow_SCC (2 threads, 134.392s elapsed time, 248.252s cpu time, 9.152s GC time, factor 1.85) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gabow_SCC Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gabow_SCC/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gabow_SCC/outline.pdf Finished Gabow_SCC (0:02:21 elapsed time, 0:04:38 cpu time, factor 1.96) Running UPF_Firewall ... UPF_Firewall: theory UPF_Firewall.LTL_alike UPF_Firewall: theory UPF_Firewall.NetworkCore Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.IOA Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.RDR UPF_Firewall: theory UPF_Firewall.Ports UPF_Firewall: theory UPF_Firewall.DatatypeAddress UPF_Firewall: theory UPF_Firewall.DatatypePort UPF_Firewall: theory UPF_Firewall.IPv4 UPF_Firewall: theory UPF_Firewall.IPv4_TCPUDP UPF_Firewall: theory UPF_Firewall.IntegerAddress UPF_Firewall: theory UPF_Firewall.IntegerPort UPF_Firewall: theory UPF_Firewall.IntegerPort_TCPUDP UPF_Firewall: theory UPF_Firewall.PolicyCore UPF_Firewall: theory UPF_Firewall.NetworkModels UPF_Firewall: theory UPF_Firewall.PolicyCombinators UPF_Firewall: theory UPF_Firewall.PortCombinators UPF_Firewall: theory UPF_Firewall.ProtocolPortCombinators UPF_Firewall: theory UPF_Firewall.PacketFilter UPF_Firewall: theory UPF_Firewall.FWNormalisationCore UPF_Firewall: theory UPF_Firewall.NAT UPF_Firewall: theory UPF_Firewall.StatefulCore UPF_Firewall: theory UPF_Firewall.FTP Timing List_Update (2 threads, 126.587s elapsed time, 218.044s cpu time, 10.728s GC time, factor 1.72) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/List_Update/outline.pdf Finished List_Update (0:02:17 elapsed time, 0:03:58 cpu time, factor 1.73) Running Vickrey_Clarke_Groves ... UPF_Firewall: theory UPF_Firewall.FTP_WithPolicy UPF_Firewall: theory UPF_Firewall.VOIP Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Argmax Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.SetUtils Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Partitions Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationOperators Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Map_Impl Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Set_Impl Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.RelationProperties Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.From_List_GA Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.MiscTools Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Examples Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.Consensus Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.StrictCombinatorialAuction UPF_Firewall: theory UPF_Firewall.FTPVOIP Timing Taylor_Models (2 threads, 137.912s elapsed time, 238.156s cpu time, 9.056s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Taylor_Models Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Taylor_Models/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Taylor_Models/outline.pdf Finished Taylor_Models (0:02:24 elapsed time, 0:04:08 cpu time, factor 1.72) Running Consensus_Refined ... Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.Universes Consensus_Refined: theory Consensus_Refined.Consensus_Types Consensus_Refined: theory Consensus_Refined.Consensus_Misc Consensus_Refined: theory Consensus_Refined.Quorums Consensus_Refined: theory Consensus_Refined.Infra Consensus_Refined: theory Consensus_Refined.Refinement Consensus_Refined: theory Consensus_Refined.Three_Steps Consensus_Refined: theory Consensus_Refined.Two_Steps Consensus_Refined: theory HOL-Library.Infinite_Set Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.UniformTieBreaking Consensus_Refined: theory HOL-Library.Omega_Words_Fun Consensus_Refined: theory Heard_Of.HOModel Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuction Consensus_Refined: theory Consensus_Refined.Voting UPF_Firewall: theory UPF_Firewall.ElementaryRules UPF_Firewall: theory UPF_Firewall.NormalisationGenericProofs Timing Separation_Logic_Imperative_HOL (2 threads, 115.242s elapsed time, 151.484s cpu time, 9.620s GC time, factor 1.31) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL/outline.pdf Finished Separation_Logic_Imperative_HOL (0:02:01 elapsed time, 0:04:32 cpu time, factor 2.25) Running Collections_Examples ... Consensus_Refined: theory Consensus_Refined.Same_Vote Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction Consensus_Refined: theory Consensus_Refined.MRU_Vote Consensus_Refined: theory Consensus_Refined.MRU_Vote_Opt Consensus_Refined: theory Consensus_Refined.Observing_Quorums Consensus_Refined: theory Consensus_Refined.Three_Step_MRU Consensus_Refined: theory Consensus_Refined.Observing_Quorums_Opt Consensus_Refined: theory Consensus_Refined.Two_Step_Observing Consensus_Refined: theory Consensus_Refined.Voting_Opt Consensus_Refined: theory Consensus_Refined.Ate_Defs Collections_Examples: theory Collections_Examples.Examples_Chapter Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples_Chapter UPF_Firewall: theory UPF_Firewall.NormalisationIntegerPortProof Collections_Examples: theory Collections_Examples.ICF_Examples_Chapter Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples_Chapter Collections_Examples: theory Collections_Examples.Buchi_Graph_Basic Collections_Examples: theory Collections_Examples.Exploration Consensus_Refined: theory Consensus_Refined.BenOr_Defs Collections_Examples: theory Collections_Examples.PerformanceTest Collections_Examples: theory Collections_Examples.Exploration_DFS Consensus_Refined: theory Consensus_Refined.CT_Defs UPF_Firewall: theory UPF_Firewall.NormalisationIPPProofs Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.Simulations Collections_Examples: theory Collections_Examples.itp_2010 Consensus_Refined: theory Consensus_Refined.HO_Transition_System Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.SLin Consensus_Refined: theory Consensus_Refined.New_Algorithm_Defs Consensus_Refined: theory Consensus_Refined.OneThirdRule_Defs UPF_Firewall: theory UPF_Firewall.FWNormalisation Consensus_Refined: theory Consensus_Refined.Paxos_Defs Consensus_Refined: theory Consensus_Refined.Uv_Defs UPF_Firewall: theory UPF_Firewall.StatefulFW UPF_Firewall: theory UPF_Firewall.UPF-Firewall Consensus_Refined: theory Heard_Of.Majorities Consensus_Refined: theory Consensus_Refined.Ate_Proofs Consensus_Refined: theory Consensus_Refined.CT_Proofs Consensus_Refined: theory Consensus_Refined.New_Algorithm_Proofs Consensus_Refined: theory Consensus_Refined.OneThirdRule_Proofs UPF_Firewall: theory UPF_Firewall.DMZDatatype Collections_Examples: theory Collections_Examples.Simple_DFS Consensus_Refined: theory Consensus_Refined.Paxos_Proofs UPF_Firewall: theory UPF_Firewall.DMZInteger Consensus_Refined: theory Stuttering_Equivalence.Samplers UPF_Firewall: theory UPF_Firewall.DMZ UPF_Firewall: theory UPF_Firewall.NAT-FW Consensus_Refined: theory Stuttering_Equivalence.StutterEquivalence Consensus_Refined: theory Heard_Of.Reduction UPF_Firewall: theory UPF_Firewall.PersonalFirewallDatatype Collections_Examples: theory Collections_Examples.ICF_Examples Consensus_Refined: theory Consensus_Refined.BenOr_Proofs Consensus_Refined: theory Consensus_Refined.Uv_Proofs UPF_Firewall: theory UPF_Firewall.PersonalFirewallInt UPF_Firewall: theory UPF_Firewall.PersonalFirewallIpv4 UPF_Firewall: theory UPF_Firewall.PersonalFirewall UPF_Firewall: theory UPF_Firewall.Transformation01 Collections_Examples: theory Collections_Examples.Succ_Graph Collections_Examples: theory Collections_Examples.ICF_Test UPF_Firewall: theory UPF_Firewall.Transformation02 UPF_Firewall: theory UPF_Firewall.Transformation UPF_Firewall: theory UPF_Firewall.VoIP UPF_Firewall: theory UPF_Firewall.Examples Collections_Examples: theory Collections_Examples.Coll_Test Timing Propositional_Proof_Systems (2 threads, 113.800s elapsed time, 210.252s cpu time, 14.160s GC time, factor 1.85) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Propositional_Proof_Systems Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Propositional_Proof_Systems/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Propositional_Proof_Systems/outline.pdf Finished Propositional_Proof_Systems (0:02:03 elapsed time, 0:03:46 cpu time, factor 1.84) Running EdmondsKarp_Maxflow ... Abortable_Linearizable_Modules: theory Abortable_Linearizable_Modules.Idempotence EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.FordFulkerson_Algo EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Augmenting_Path_BFS EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Algo CAVA_LTL_Modelchecker: theory HOL-Library.Mapping CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Extras CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Simple EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.EdmondsKarp_Impl CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.BoolProgs_Programs CAVA_LTL_Modelchecker: theory HOL-Library.AList_Mapping CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.CAVA_Impl Collections_Examples: theory Collections_Examples.Nested_DFS EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Checked_Impl Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.FirstPrice Vickrey_Clarke_Groves: theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples Collections_Examples: theory Collections_Examples.Foreach_Refine Collections_Examples: theory Collections_Examples.ICF_Only_Test Collections_Examples: theory Collections_Examples.Refine_Fold Collections_Examples: theory Collections_Examples.Bfs_Impl Collections_Examples: theory Collections_Examples.Refine_Monadic_Examples Collections_Examples: theory Collections_Examples.Collection_Autoref_Examples EdmondsKarp_Maxflow: theory EdmondsKarp_Maxflow.Edka_Benchmark_Export Timing Consensus_Refined (2 threads, 83.326s elapsed time, 136.148s cpu time, 8.252s GC time, factor 1.63) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Consensus_Refined Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Consensus_Refined/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Consensus_Refined/outline.pdf Finished Consensus_Refined (0:01:29 elapsed time, 0:02:26 cpu time, factor 1.64) Running Dijkstra_Shortest_Path ... Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Misc Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Graph Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Introduction Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Weight Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphSpec Timing Abortable_Linearizable_Modules (2 threads, 106.172s elapsed time, 154.224s cpu time, 5.484s GC time, factor 1.45) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abortable_Linearizable_Modules Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abortable_Linearizable_Modules/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abortable_Linearizable_Modules/outline.pdf Finished Abortable_Linearizable_Modules (0:01:51 elapsed time, 0:02:43 cpu time, factor 1.47) Running PCF ... Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra Collections_Examples: theory Collections_Examples.Collection_Examples PCF: theory HOL-Library.Product_Plus PCF: theory PCF.Dual_Lattice PCF: theory HOL-Library.Product_Order PCF: theory PCF.Basis PCF: theory PCF.Logical_Relations Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphGA PCF: theory PCF.PCF Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.GraphByMap Timing EdmondsKarp_Maxflow (2 threads, 69.423s elapsed time, 93.928s cpu time, 3.940s GC time, factor 1.35) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/EdmondsKarp_Maxflow Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/EdmondsKarp_Maxflow/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/EdmondsKarp_Maxflow/outline.pdf Finished EdmondsKarp_Maxflow (0:01:16 elapsed time, 0:02:10 cpu time, factor 1.70) Running AutoFocus-Stream ... AutoFocus-Stream: theory AutoFocus-Stream.ListSlice Timing Collections_Examples (2 threads, 90.703s elapsed time, 175.672s cpu time, 7.700s GC time, factor 1.94) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections_Examples Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections_Examples/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Collections_Examples/outline.pdf Finished Collections_Examples (0:01:37 elapsed time, 0:03:10 cpu time, factor 1.96) Running Polynomial_Factorization ... AutoFocus-Stream: theory AutoFocus-Stream.AF_Stream Timing UPF_Firewall (2 threads, 109.924s elapsed time, 184.928s cpu time, 9.660s GC time, factor 1.68) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/outline.pdf Finished UPF_Firewall (0:01:57 elapsed time, 0:03:17 cpu time, factor 1.68) Running Perron_Frobenius ... Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.HashGraphImpl PCF: theory PCF.Continuations Polynomial_Factorization: theory Polynomial_Factorization.Precomputation Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots AutoFocus-Stream: theory AutoFocus-Stream.AF_Stream_Exec AutoFocus-Stream: theory AutoFocus-Stream.IL_AF_Stream Polynomial_Factorization: theory Polynomial_Factorization.Missing_List Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Impl Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet PCF: theory PCF.OpSem Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test AutoFocus-Stream: theory AutoFocus-Stream.IL_AF_Stream_Exec Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization Perron_Frobenius: theory Perron_Frobenius.Bij_Nat Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint Perron_Frobenius: theory Perron_Frobenius.Roots_Unity Perron_Frobenius: theory Perron_Frobenius.HMA_Connect Timing Vickrey_Clarke_Groves (2 threads, 111.330s elapsed time, 184.720s cpu time, 4.860s GC time, factor 1.66) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Vickrey_Clarke_Groves/outline.pdf Finished Vickrey_Clarke_Groves (0:01:57 elapsed time, 0:03:15 cpu time, factor 1.66) Running Incredible_Proof_Machine ... Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization Incredible_Proof_Machine: theory HOL-Eisbach.Eisbach Incredible_Proof_Machine: theory Collections.ICF_Tools Incredible_Proof_Machine: theory Collections.Ord_Code_Preproc Incredible_Proof_Machine: theory Collections.Locale_Code Incredible_Proof_Machine: theory Incredible_Proof_Machine.Indexed_FSet Incredible_Proof_Machine: theory Abstract_Completeness.Abstract_Completeness Incredible_Proof_Machine: theory Incredible_Proof_Machine.Abstract_Formula Incredible_Proof_Machine: theory Incredible_Proof_Machine.Abstract_Rules Incredible_Proof_Machine: theory Incredible_Proof_Machine.Predicate_Formulas Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux Incredible_Proof_Machine: theory Incredible_Proof_Machine.Propositional_Formulas Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory Incredible_Proof_Machine: theory Incredible_Proof_Machine.Entailment Incredible_Proof_Machine: theory Incredible_Proof_Machine.Natural_Deduction Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Signatures Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Deduction Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General Incredible_Proof_Machine: theory Incredible_Proof_Machine.Rose_Tree Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth Incredible_Proof_Machine: theory Incredible_Proof_Machine.Abstract_Rules_To_Incredible Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Correctness Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Predicate Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Propositional Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Trees Incredible_Proof_Machine: theory Incredible_Proof_Machine.Build_Incredible_Tree Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Completeness Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Everything Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Predicate_Tasks Incredible_Proof_Machine: theory Incredible_Proof_Machine.Incredible_Propositional_Tasks CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS CAVA_LTL_Modelchecker: theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker Dijkstra_Shortest_Path: theory Dijkstra_Shortest_Path.Test Timing CAVA_LTL_Modelchecker (2 threads, 242.209s elapsed time, 248.496s cpu time, 8.704s GC time, factor 1.03) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CAVA_LTL_Modelchecker/outline.pdf Finished CAVA_LTL_Modelchecker (0:04:10 elapsed time, 0:05:16 cpu time, factor 1.27) Running Game_Based_Crypto ... Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation Timing PCF (2 threads, 58.096s elapsed time, 87.432s cpu time, 2.728s GC time, factor 1.50) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PCF/outline.pdf Finished PCF (0:01:02 elapsed time, 0:01:35 cpu time, factor 1.52) Running Tree-Automata ... Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF Timing Polynomial_Factorization (2 threads, 48.968s elapsed time, 78.048s cpu time, 2.636s GC time, factor 1.59) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf Finished Polynomial_Factorization (0:00:57 elapsed time, 0:01:30 cpu time, factor 1.57) Running PLM ... Game_Based_Crypto: theory Game_Based_Crypto.RP_RF Tree-Automata: theory Tree-Automata.Tree Tree-Automata: theory Collections_Examples.Exploration Game_Based_Crypto: theory Game_Based_Crypto.Elgamal Timing Dijkstra_Shortest_Path (2 threads, 64.108s elapsed time, 82.732s cpu time, 4.036s GC time, factor 1.29) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dijkstra_Shortest_Path Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dijkstra_Shortest_Path/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dijkstra_Shortest_Path/outline.pdf Finished Dijkstra_Shortest_Path (0:01:09 elapsed time, 0:03:26 cpu time, factor 2.96) Running ROBDD ... PLM: theory HOL-Eisbach.Eisbach PLM: theory HOL-Library.LaTeXsugar PLM: theory HOL-Library.OptionalSugar Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2 PLM: theory PLM.TAO_1_Embedding PLM: theory HOL-Eisbach.Eisbach_Tools Tree-Automata: theory Tree-Automata.Ta ROBDD: theory ROBDD.Bool_Func ROBDD: theory ROBDD.Option_Helpers ROBDD: theory ROBDD.BDT ROBDD: theory ROBDD.Pointer_Map Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA ROBDD: theory ROBDD.Array_List ROBDD: theory ROBDD.Pointer_Map_Impl PLM: theory PLM.TAO_2_Semantics Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK PLM: theory PLM.TAO_3_Quantifiable Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA Timing AutoFocus-Stream (2 threads, 57.288s elapsed time, 100.004s cpu time, 1.956s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AutoFocus-Stream Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AutoFocus-Stream/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AutoFocus-Stream/outline.pdf Finished AutoFocus-Stream (0:01:04 elapsed time, 0:01:51 cpu time, factor 1.74) Running FocusStreamsCaseStudies ... PLM: theory PLM.TAO_4_BasicDefinitions PLM: theory PLM.TAO_5_MetaSolver FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ArithExtras FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.ListExtras Timing Incredible_Proof_Machine (2 threads, 46.412s elapsed time, 86.060s cpu time, 5.260s GC time, factor 1.85) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Incredible_Proof_Machine Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Incredible_Proof_Machine/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Incredible_Proof_Machine/outline.pdf Finished Incredible_Proof_Machine (0:00:52 elapsed time, 0:01:36 cpu time, factor 1.83) Running Knuth_Morris_Pratt ... FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.arith_hints Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.stream PLM: theory PLM.TAO_6_Identifiable ROBDD: theory ROBDD.Abstract_Impl Tree-Automata: theory Tree-Automata.AbsAlgo PLM: theory PLM.TAO_7_Axioms PLM: theory PLM.TAO_8_Definitions Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA PLM: theory PLM.TAO_98_ArtificialTheorems PLM: theory PLM.TAO_99_SanityTests PLM: theory PLM.TAO_9_PLM Knuth_Morris_Pratt: theory HOL-Library.Char_ord Knuth_Morris_Pratt: theory HOL-Library.Sublist Knuth_Morris_Pratt: theory HOL-Library.Code_Char FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.BitBoolTS FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_types Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_types ROBDD: theory ROBDD.Middle_Impl Knuth_Morris_Pratt: theory Knuth_Morris_Pratt.KMP FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.FR_proof FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.SteamBoiler_proof Timing Perron_Frobenius (2 threads, 53.609s elapsed time, 84.680s cpu time, 2.212s GC time, factor 1.58) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perron_Frobenius/outline.pdf Finished Perron_Frobenius (0:01:08 elapsed time, 0:01:43 cpu time, factor 1.51) Running CISC-Kernel ... PLM: theory PLM.TAO_10_PossibleWorlds FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.JoinSplitTime PLM: theory PLM.TAO_99_Paradox ROBDD: theory ROBDD.Conc_Impl PLM: theory PLM.Thesis Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec CISC-Kernel: theory CISC-Kernel.Option_Binders CISC-Kernel: theory CISC-Kernel.List_Theorems CISC-Kernel: theory CISC-Kernel.Step_configuration CISC-Kernel: theory CISC-Kernel.K Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof_aux CISC-Kernel: theory CISC-Kernel.Step_policies CISC-Kernel: theory CISC-Kernel.SK CISC-Kernel: theory CISC-Kernel.Step FocusStreamsCaseStudies: theory FocusStreamsCaseStudies.Gateway_proof CISC-Kernel: theory CISC-Kernel.ISK Tree-Automata: theory Tree-Automata.Ta_impl ROBDD: theory ROBDD.Level_Collapse CISC-Kernel: theory CISC-Kernel.CISK ROBDD: theory ROBDD.BDD_Examples Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto CISC-Kernel: theory CISC-Kernel.Step_invariants CISC-Kernel: theory CISC-Kernel.Step_vpeq CISC-Kernel: theory CISC-Kernel.Step_vpeq_locally_respects CISC-Kernel: theory CISC-Kernel.Step_vpeq_weakly_step_consistent CISC-Kernel: theory CISC-Kernel.Separation_kernel_model CISC-Kernel: theory CISC-Kernel.Link_separation_kernel_model_to_CISK Tree-Automata: theory Tree-Automata.Ta_impl_codegen ROBDD: theory ROBDD.BDD_Code Timing Knuth_Morris_Pratt (2 threads, 23.719s elapsed time, 44.752s cpu time, 1.160s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knuth_Morris_Pratt Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knuth_Morris_Pratt/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knuth_Morris_Pratt/outline.pdf Finished Knuth_Morris_Pratt (0:00:29 elapsed time, 0:00:53 cpu time, factor 1.83) Running Floyd_Warshall ... Floyd_Warshall: theory Floyd_Warshall.Floyd_Warshall Floyd_Warshall: theory Floyd_Warshall.Recursion_Combinators Timing Tree-Automata (2 threads, 33.933s elapsed time, 59.760s cpu time, 2.976s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tree-Automata Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tree-Automata/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Tree-Automata/outline.pdf Finished Tree-Automata (0:00:40 elapsed time, 0:01:10 cpu time, factor 1.72) Timing Game_Based_Crypto (2 threads, 36.467s elapsed time, 70.544s cpu time, 2.024s GC time, factor 1.93) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Game_Based_Crypto Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Game_Based_Crypto/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Game_Based_Crypto/outline.pdf Finished Game_Based_Crypto (0:00:43 elapsed time, 0:01:20 cpu time, factor 1.86) Running GraphMarkingIBP ... Running Buchi_Complementation ... GraphMarkingIBP: theory GraphMarkingIBP.Graph GraphMarkingIBP: theory LatticeProperties.Conj_Disj GraphMarkingIBP: theory LatticeProperties.WellFoundedTransitive GraphMarkingIBP: theory LatticeProperties.Complete_Lattice_Prop Timing FocusStreamsCaseStudies (2 threads, 29.618s elapsed time, 47.492s cpu time, 1.372s GC time, factor 1.60) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/FocusStreamsCaseStudies Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/FocusStreamsCaseStudies/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/FocusStreamsCaseStudies/outline.pdf Finished FocusStreamsCaseStudies (0:00:36 elapsed time, 0:00:57 cpu time, factor 1.59) Timing CISC-Kernel (2 threads, 22.831s elapsed time, 40.788s cpu time, 1.716s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CISC-Kernel Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CISC-Kernel/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/CISC-Kernel/outline.pdf Finished CISC-Kernel (0:00:29 elapsed time, 0:00:51 cpu time, factor 1.74) Timing ROBDD (2 threads, 34.249s elapsed time, 59.232s cpu time, 2.116s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/ROBDD Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/ROBDD/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/ROBDD/outline.pdf Finished ROBDD (0:00:40 elapsed time, 0:01:09 cpu time, factor 1.71) Running AVL-Trees ... Running Recursion-Theory-I ... GraphMarkingIBP: theory DataRefinementIBP.Preliminaries Running Zeta_Function ... GraphMarkingIBP: theory DataRefinementIBP.Statements Buchi_Complementation: theory HOL-Library.Lattice_Syntax Buchi_Complementation: theory Buchi_Complementation.Alternate Buchi_Complementation: theory Buchi_Complementation.Graph GraphMarkingIBP: theory DataRefinementIBP.Hoare GraphMarkingIBP: theory DataRefinementIBP.Diagram AVL-Trees: theory AVL-Trees.AVL AVL-Trees: theory AVL-Trees.AVL2 Buchi_Complementation: theory Buchi_Complementation.Ranking Recursion-Theory-I: theory Recursion-Theory-I.CPair GraphMarkingIBP: theory DataRefinementIBP.DataRefinement GraphMarkingIBP: theory GraphMarkingIBP.SetMark Recursion-Theory-I: theory Recursion-Theory-I.PRecFun Zeta_Function: theory Bernoulli.Bernoulli_Zeta Buchi_Complementation: theory Buchi_Complementation.Complementation Floyd_Warshall: theory Floyd_Warshall.FW_Code GraphMarkingIBP: theory GraphMarkingIBP.StackMark Buchi_Complementation: theory Buchi_Complementation.Complementation_Implement Recursion-Theory-I: theory Recursion-Theory-I.PRecFinSet Recursion-Theory-I: theory Recursion-Theory-I.PRecFun2 GraphMarkingIBP: theory GraphMarkingIBP.LinkMark Recursion-Theory-I: theory Recursion-Theory-I.PRecList GraphMarkingIBP: theory GraphMarkingIBP.DSWMark Recursion-Theory-I: theory Recursion-Theory-I.PRecUnGr Timing PLM (2 threads, 32.888s elapsed time, 53.800s cpu time, 1.736s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PLM Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PLM/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/PLM/outline.pdf Finished PLM (0:00:47 elapsed time, 0:01:33 cpu time, factor 1.99) Running Abstract_Soundness ... Recursion-Theory-I: theory Recursion-Theory-I.RecEnSet Zeta_Function: theory Zeta_Function.Zeta_Function Abstract_Soundness: theory Abstract_Soundness.Finite_Proof_Soundness Abstract_Soundness: theory Abstract_Soundness.Infinite_Proof_Soundness Timing Zeta_Function (2 threads, 14.075s elapsed time, 20.176s cpu time, 0.520s GC time, factor 1.43) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Zeta_Function Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Zeta_Function/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Zeta_Function/outline.pdf Finished Zeta_Function (0:00:19 elapsed time, 0:00:28 cpu time, factor 1.45) Running Minimal_SSA ... Timing AVL-Trees (2 threads, 17.199s elapsed time, 32.368s cpu time, 0.724s GC time, factor 1.88) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AVL-Trees Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AVL-Trees/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/AVL-Trees/outline.pdf Finished AVL-Trees (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.83) Running Comparison_Sort_Lower_Bound ... Minimal_SSA: theory Minimal_SSA.Irreducible Timing Floyd_Warshall (2 threads, 21.630s elapsed time, 37.780s cpu time, 1.140s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Floyd_Warshall Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Floyd_Warshall/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Floyd_Warshall/outline.pdf Finished Floyd_Warshall (0:00:28 elapsed time, 0:00:51 cpu time, factor 1.83) Timing Buchi_Complementation (2 threads, 17.762s elapsed time, 33.864s cpu time, 1.220s GC time, factor 1.91) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Buchi_Complementation Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Buchi_Complementation/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Buchi_Complementation/outline.pdf Finished Buchi_Complementation (0:00:24 elapsed time, 0:00:42 cpu time, factor 1.78) Running GPU_Kernel_PL ... Running Latin_Square ... Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations Comparison_Sort_Lower_Bound: theory List-Index.List_Index Timing Recursion-Theory-I (2 threads, 16.094s elapsed time, 28.228s cpu time, 1.148s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Recursion-Theory-I Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Recursion-Theory-I/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Recursion-Theory-I/outline.pdf Finished Recursion-Theory-I (0:00:22 elapsed time, 0:00:38 cpu time, factor 1.68) Timing GraphMarkingIBP (2 threads, 20.857s elapsed time, 37.452s cpu time, 0.796s GC time, factor 1.80) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GraphMarkingIBP Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GraphMarkingIBP/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GraphMarkingIBP/outline.pdf Finished GraphMarkingIBP (0:00:25 elapsed time, 0:00:44 cpu time, factor 1.79) Running Imperative_Insertion_Sort ... Running Case_Labeling ... GPU_Kernel_PL: theory GPU_Kernel_PL.Misc Latin_Square: theory Marriage.Marriage GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_syntax Latin_Square: theory Latin_Square.Latin_Square Timing Abstract_Soundness (2 threads, 13.033s elapsed time, 22.284s cpu time, 1.272s GC time, factor 1.71) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract_Soundness Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract_Soundness/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Abstract_Soundness/outline.pdf Finished Abstract_Soundness (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.71) Running Transitive-Closure ... Case_Labeling: theory HOL-Eisbach.Eisbach Case_Labeling: theory Case_Labeling.Case_Labeling Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations Case_Labeling: theory HOL-Hoare.Arith2 Case_Labeling: theory HOL-Hoare.Hoare_Logic Case_Labeling: theory Case_Labeling.Conditionals Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Loops Imperative_Insertion_Sort: theory Imperative_Insertion_Sort.Imperative_Insertion_Sort Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound Case_Labeling: theory Case_Labeling.Monadic_Language Transitive-Closure: theory Matrix.Utility Transitive-Closure: theory Transitive-Closure.Transitive_Closure_Impl Transitive-Closure: theory Transitive-Closure.RBT_Map_Set_Extension Case_Labeling: theory Case_Labeling.Labeled_Hoare Transitive-Closure: theory Transitive-Closure.Transitive_Closure_List_Impl Transitive-Closure: theory Transitive-Closure.Finite_Transitive_Closure_Simprocs GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_state Case_Labeling: theory Case_Labeling.Labeled_Hoare_Examples GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_wellformedness Transitive-Closure: theory Transitive-Closure.Transitive_Closure_RBT_Impl Case_Labeling: theory Case_Labeling.Case_Labeling_Examples GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_thread GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_group GPU_Kernel_PL: theory GPU_Kernel_PL.KPL_execution_kernel GPU_Kernel_PL: theory GPU_Kernel_PL.Kernel_programming_language Timing Case_Labeling (2 threads, 5.095s elapsed time, 10.056s cpu time, 0.408s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Case_Labeling Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Case_Labeling/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Case_Labeling/outline.pdf Finished Case_Labeling (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.83) Timing Transitive-Closure (2 threads, 3.656s elapsed time, 6.720s cpu time, 0.248s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transitive-Closure Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transitive-Closure/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Transitive-Closure/outline.pdf Finished Transitive-Closure (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.61) Timing GPU_Kernel_PL (2 threads, 7.296s elapsed time, 12.448s cpu time, 0.544s GC time, factor 1.71) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GPU_Kernel_PL Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GPU_Kernel_PL/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/GPU_Kernel_PL/outline.pdf Finished GPU_Kernel_PL (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.68) Timing Comparison_Sort_Lower_Bound (2 threads, 7.832s elapsed time, 15.040s cpu time, 0.776s GC time, factor 1.92) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.78) Timing Imperative_Insertion_Sort (2 threads, 6.929s elapsed time, 11.240s cpu time, 0.148s GC time, factor 1.62) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Imperative_Insertion_Sort Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Imperative_Insertion_Sort/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Imperative_Insertion_Sort/outline.pdf Finished Imperative_Insertion_Sort (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.57) Timing Minimal_SSA (2 threads, 7.921s elapsed time, 14.948s cpu time, 0.416s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Minimal_SSA Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Minimal_SSA/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Minimal_SSA/outline.pdf Finished Minimal_SSA (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.67) Timing Latin_Square (2 threads, 9.214s elapsed time, 14.200s cpu time, 0.248s GC time, factor 1.54) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Latin_Square Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Latin_Square/document.pdf Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Latin_Square/outline.pdf Finished Latin_Square (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.61) HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics Timing HOL-ODE-Numerics (2 threads, 1766.518s elapsed time, 2943.688s cpu time, 301.336s GC time, factor 1.67) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE-Numerics Finished HOL-ODE-Numerics (0:31:20 elapsed time, 0:51:47 cpu time, factor 1.65) Building Lorenz_Approximation ... Running HOL-ODE-Examples ... HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples Timing Lorenz_Approximation (2 threads, 340.538s elapsed time, 549.240s cpu time, 48.916s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lorenz_Approximation Finished Lorenz_Approximation (0:06:21 elapsed time, 0:10:06 cpu time, factor 1.59) Running Lorenz_C1 ... Lorenz_C1: theory Lorenz_C1.Lorenz_C1 Timing Lorenz_C1 (2 threads, 0.745s elapsed time, 1.308s cpu time, 0.000s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lorenz_C1 Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.03) Timing HOL-ODE-Examples (2 threads, 591.146s elapsed time, 1118.732s cpu time, 28.204s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/HOL-ODE-Examples Finished HOL-ODE-Examples (0:09:54 elapsed time, 0:18:41 cpu time, factor 1.89) === TIMING === Group AFP: 4:43:42 elapsed time, 8:04:40 cpu time, factor 1.71 Group main: 0:00:00 elapsed time Group timing: 0:00:00 elapsed time Overall: 0:54:09 elapsed time, 8:04:40 cpu time, factor 8.95 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === SITEGEN === Writing status file ... Running sitegen ... Success: Generated topics.html Success: Generated index.html Success: Generated html files for 397 entries Success: Generated statistics.html Success: Generated download.html Success: Generated about.html Success: Generated citing.html Success: Generated updating.html Success: Generated search.html Success: Generated submitting.html Success: Generated using.html Success: Generated rss.xml Success: Generated status.html Packing tars ... === COMPLETED === Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: SUCCESS