Skip to content
[Jenkins]Jenkins
log in
Success

Console Output

01:55:39 Started by upstream project "isabelle-repo" build number 1760


01:55:39 originally caused by:


01:55:39  Started by an SCM change


01:55:39 [EnvInject] - Loading node environment variables.


01:55:39 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp


01:55:39 [isabelle-repo-afp] $ hg showconfig paths.default


01:55:39 [isabelle-repo-afp] $ hg pull --rev f839ce4af873343accf5428d0a78d4aaf8c7d27b


01:55:40 pulling from http://isabelle.in.tum.de/repos/isabelle/


01:55:40 searching for changes


01:55:40 adding changesets


01:55:40 adding manifests


01:55:40 adding file changes


01:55:40 added 2 changesets with 1 changes to 1 files


01:55:40 (run 'hg update' to get a working copy)


01:55:40 [isabelle-repo-afp] $ hg update --clean --rev f839ce4af873343accf5428d0a78d4aaf8c7d27b


01:55:40 1 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:55:40 [isabelle-repo-afp] $ hg log --rev . --template {node}


01:55:40 [isabelle-repo-afp] $ hg log --rev . --template {rev}


01:55:40 [isabelle-repo-afp] $ hg id --branch


01:55:40 [afp] $ hg showconfig paths.default


01:55:40 [afp] $ hg pull --rev default


01:55:42 pulling from https://bitbucket.org/isa-afp/afp-devel/


01:55:42 searching for changes


01:55:42 adding changesets


01:55:42 adding manifests


01:55:42 adding file changes


01:55:42 added 1 changesets with 2 changes to 2 files


01:55:42 (run 'hg update' to get a working copy)


01:55:42 [afp] $ hg update --clean --rev default


01:55:42 428 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:55:42 [afp] $ hg --config extensions.purge= clean --all


01:55:43 [afp] $ hg log --rev . --template {node}


01:55:43 [afp] $ hg log --rev . --template {rev}


01:55:43 No emails were triggered.


01:55:43 [isabelle-repo-afp] $ /bin/sh -xe /tmp/jenkins4623244174841169208.sh


01:55:43 + Admin/jenkins/run_build afp


01:55:43 + set -e


01:55:43 + PROFILE=afp


01:55:43 + shift


01:55:43 + bin/isabelle components -a


01:55:43 + bin/isabelle jedit -bf


01:55:44 ### Building Isabelle/Scala ...


01:56:13 ### Building Isabelle/jEdit ...


01:56:31 + bin/isabelle ci_build_afp


01:56:38 

01:56:38 === CONFIGURATION ===


01:56:38 

01:56:38 ISABELLE_BUILD_OPTIONS=""


01:56:38 

01:56:38 ML_PLATFORM="x86_64-linux"


01:56:38 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-6/x86_64-linux"


01:56:38 ML_SYSTEM="polyml-5.7.1"


01:56:38 ML_OPTIONS="-H 4000 --maxheap 8G"


01:56:38 

01:56:38 === BUILD ===


01:56:38 

01:56:38 Build started at Thu, 21 Jun 2018 23:56:37 GMT


01:56:38 Isabelle id f839ce4af873


01:56:38 AFP id 3918e10b3d5f


01:56:38 

01:56:38 === LOG ===


01:56:38 

01:56:39 Session Pure/Pure


01:56:39 Session FOL/FOL


01:56:39 Session HOL/HOL (main)


01:56:40 Session AFP/AVL-Trees (AFP)


01:56:40 Session AFP/AWN (AFP)


01:56:40 Session AFP/Abortable_Linearizable_Modules (AFP)


01:56:40 Session AFP/Abstract-Hoare-Logics (AFP)


01:56:40 Session AFP/AnselmGod (AFP)


01:56:40 Session AFP/AxiomaticCategoryTheory (AFP)


01:56:40 Session AFP/BinarySearchTree (AFP)


01:56:41 Session AFP/Binomial-Queues (AFP)


01:56:41 Session AFP/Bondy (AFP)


01:56:41 Session AFP/Bounded_Deducibility_Security (AFP)


01:56:41 Session AFP/BytecodeLogicJmlTypes (AFP)


01:56:41 Session AFP/CISC-Kernel (AFP)


01:56:41 Session AFP/CYK (AFP)


01:56:41 Session AFP/Cauchy (AFP)


01:56:41 Session AFP/Sqrt_Babylonian (AFP)


01:56:41 Session AFP/ClockSynchInst (AFP)


01:56:41 Session AFP/Compiling-Exceptions-Correctly (AFP)


01:56:41 Session AFP/ComponentDependencies (AFP)


01:56:41 Session AFP/Constructor_Funs (AFP)


01:56:41 Session AFP/CryptoBasedCompositionalProperties (AFP)


01:56:41 Session AFP/DPT-SAT-Solver (AFP)


01:56:41 Session AFP/Depth-First-Search (AFP)


01:56:41 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)


01:56:41 Session AFP/HLDE (AFP)


01:56:41 Session AFP/DiskPaxos (AFP)


01:56:41 Session AFP/Example-Submission (AFP)


01:56:41 Session AFP/FFT (AFP)


01:56:41 Session AFP/FLP (AFP)


01:56:41 Session AFP/FeatherweightJava (AFP)


01:56:41 Session AFP/Featherweight_OCL (AFP)


01:56:41 Session AFP/FileRefinement (AFP)


01:56:41 Session AFP/FocusStreamsCaseStudies (AFP)


01:56:41 Session AFP/Free-Boolean-Algebra (AFP)


01:56:41 Session AFP/FunWithFunctions (AFP)


01:56:41 Session AFP/FunWithTilings (AFP)


01:56:41 Session AFP/GPU_Kernel_PL (AFP)


01:56:41 Session AFP/Gauss-Jordan-Elim-Fun (AFP)


01:56:41 Session AFP/GenClock (AFP)


01:56:41 Session AFP/General-Triangle (AFP)


01:56:41 Session AFP/GoedelGod (AFP)


01:56:41 Session HOL/HOL-Eisbach


01:56:42 Session AFP/Allen_Calculus (AFP)


01:56:42 Session AFP/Dependent_SIFUM_Type_Systems (AFP)


01:56:42 Session AFP/Dependent_SIFUM_Refinement (AFP)


01:56:42 Session HOL/HOL-Hoare


01:56:42 Session AFP/Case_Labeling (AFP)


01:56:42 Session HOL/HOL-Lattice


01:56:42 Session HOL/HOL-Library (main timing)


01:56:42 Session AFP/ArrowImpossibilityGS (AFP)


01:56:42 Session AFP/BNF_CC (AFP)


01:56:42 Session AFP/BNF_Operations (AFP)


01:56:42 Session AFP/Binomial-Heaps (AFP)


01:56:43 Session AFP/Boolean_Expression_Checkers (AFP)


01:56:43 Session AFP/Buildings (AFP)


01:56:43 Session AFP/CRDT (AFP)


01:56:43 Session AFP/IMAP-CRDT (AFP)


01:56:43 Session AFP/Card_Multisets (AFP)


01:56:43 Session AFP/Card_Number_Partitions (AFP)


01:56:43 Session AFP/Category (AFP)


01:56:43 Session AFP/Category3 (AFP)


01:56:43 Session AFP/MonoidalCategory (AFP)


01:56:43 Session AFP/CofGroups (AFP)


01:56:43 Session AFP/Completeness (AFP)


01:56:44 Session AFP/ConcurrentIMP (AFP)


01:56:44 Session AFP/Concurrent_Ref_Alg (AFP)


01:56:44 Session AFP/CoreC++ (AFP)


01:56:44 Session AFP/Decl_Sem_Fun_PL (AFP)


01:56:44 Session AFP/Derangements (AFP)


01:56:44 Session AFP/Discrete_Summation (AFP)


01:56:44 Session AFP/Card_Partitions (AFP)


01:56:44 Session AFP/Bell_Numbers_Spivey (AFP)


01:56:44 Session AFP/Card_Equiv_Relations (AFP)


01:56:44 Session AFP/Efficient-Mergesort (AFP)


01:56:44 Session AFP/Encodability_Process_Calculi (AFP)


01:56:45 Session AFP/Euler_Partition (AFP)


01:56:45 Session AFP/FOL-Fitting (AFP)


01:56:45 Session AFP/FOL_Harrison (AFP)


01:56:45 Session AFP/Falling_Factorial_Sum (AFP)


01:56:45 Session AFP/FinFun (AFP)


01:56:45 Session AFP/Finger-Trees (AFP)


01:56:45 Session AFP/Graph_Theory (AFP)


01:56:45 Session AFP/ShortestPath (AFP)


01:56:45 Session AFP/Group-Ring-Module (AFP)


01:56:45 Session AFP/Valuation (AFP)


01:56:45 Session HOL/HOL-Cardinals (timing)


01:56:45 Session AFP/Ordinals_and_Cardinals (AFP)


01:56:45 Session AFP/Sort_Encodings (AFP)


01:56:45 Session HOL/HOL-Computational_Algebra (main timing)


01:56:46 Session AFP/Descartes_Sign_Rule (AFP)


01:56:46 Session HOL/HOL-Algebra (main timing)


01:56:46 Session HOL/HOL-Decision_Procs (timing)


01:56:46 Session AFP/JNF-HOL-Lib (AFP)


01:56:46 Session AFP/Orbit_Stabiliser (AFP)


01:56:46 Session AFP/Perfect-Number-Thm (AFP)


01:56:46 Session AFP/Secondary_Sylow (AFP)


01:56:46 Session AFP/Jordan_Hoelder (AFP)


01:56:46 Session AFP/VectorSpace (AFP)


01:56:47 Session HOL/HOL-Analysis (main timing)


01:56:47 Session AFP/Bernoulli (AFP)


01:56:47 Session AFP/Cartan_FP (AFP)


01:56:47 Session AFP/Cayley_Hamilton (AFP)


01:56:47 Session AFP/Coinductive (AFP)


01:56:48 Session AFP/DynamicArchitectures (AFP)


01:56:48 Session AFP/Architectural_Design_Patterns (AFP)


01:56:48 Session AFP/Lazy-Lists-II (AFP)


01:56:48 Session AFP/Stream_Fusion_Code (AFP)


01:56:48 Session AFP/Topology (AFP)


01:56:48 Session AFP/First_Welfare_Theorem (AFP)


01:56:48 Session AFP/Green (AFP)


01:56:48 Session HOL/HOL-Probability (main timing)


01:56:48 Session AFP/Buffons_Needle (AFP)


01:56:48 Session AFP/Density_Compiler (AFP)


01:56:48 Session AFP/Ergodic_Theory (AFP)


01:56:49 Session AFP/Gromov_Hyperbolicity (AFP)


01:56:49 Session AFP/Fisher_Yates (AFP)


01:56:49 Session AFP/Girth_Chromatic (AFP)


01:56:49 Session AFP/Random_Graph_Subgraph_Threshold (AFP)


01:56:49 Session AFP/Lp (AFP)


01:56:49 Session AFP/Markov_Models (AFP)


01:56:49 Session AFP/Monad_Normalisation (AFP)


01:56:50 Session AFP/Monomorphic_Monad (AFP)


01:56:50 Session AFP/Probabilistic_Noninterference (AFP)


01:56:50 Session AFP/Probabilistic_System_Zoo (AFP)


01:56:50 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)


01:56:50 Session AFP/Source_Coding_Theorem (AFP)


01:56:50 Session AFP/Irrationality_J_Hancl (AFP)


01:56:50 Session AFP/Kuratowski_Closure_Complement (AFP)


01:56:50 Session AFP/Lower_Semicontinuous (AFP)


01:56:50 Session AFP/Minkowskis_Theorem (AFP)


01:56:50 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)


01:56:51 Session AFP/Ptolemys_Theorem (AFP)


01:56:51 Session AFP/Rank_Nullity_Theorem (AFP)


01:56:51 Session AFP/Gauss_Jordan (AFP)


01:56:51 Session AFP/Echelon_Form (AFP)


01:56:51 Session AFP/Hermite (AFP)


01:56:51 Session AFP/Tarskis_Geometry (AFP)


01:56:51 Session AFP/Triangle (AFP)


01:56:51 Session AFP/Chord_Segments (AFP)


01:56:51 Session AFP/Stewart_Apollonius (AFP)


01:56:51 Session AFP/pGCL (AFP)


01:56:51 Session HOL/HOL-Nonstandard_Analysis (timing)


01:56:52 Session HOL/HOL-Number_Theory (main timing)


01:56:52 Session AFP/E_Transcendental (AFP)


01:56:52 Session AFP/Elliptic_Curves_Group_Law (AFP)


01:56:52 Session AFP/Fermat3_4 (AFP)


01:56:52 Session HOL/HOL-Data_Structures (timing)


01:56:52 Session HOL/HOL-ex (timing)


01:56:53 Session AFP/Automatic_Refinement (AFP)


01:56:53 Session AFP/Lehmer (AFP)


01:56:53 Session AFP/Pratt_Certificate (AFP)


01:56:53 Session AFP/Bertrands_Postulate (AFP)


01:56:53 Session AFP/Prime_Harmonic_Series (AFP)


01:56:54 Session AFP/RSAPSS (AFP)


01:56:54 Session AFP/SumSquares (AFP)


01:56:54 Session AFP/Liouville_Numbers (AFP)


01:56:54 Session AFP/Mason_Stothers (AFP)


01:56:54 Session AFP/Polynomial_Interpolation (AFP)


01:56:54 Session AFP/Rep_Fin_Groups (AFP)


01:56:54 Session AFP/Sturm_Sequences (AFP)


01:56:54 Session AFP/Special_Function_Bounds (AFP)


01:56:54 Session AFP/Sturm_Tarski (AFP)


01:56:54 Session AFP/Winding_Number_Eval (AFP)


01:56:54 Session AFP/Count_Complex_Roots (AFP)


01:56:54 Session HOL/HOL-IMP (timing)


01:56:55 Session AFP/Abs_Int_ITP2012 (AFP)


01:56:55 Session HOL/HOL-Imperative_HOL (timing)


01:56:55 Session AFP/Imperative_Insertion_Sort (AFP)


01:56:55 Session HOL/HOL-Nominal


01:56:55 Session AFP/CCS (AFP)


01:56:55 Session AFP/Lam-ml-Normalization (AFP)


01:56:55 Session AFP/Pi_Calculus (AFP)


01:56:55 Session AFP/Psi_Calculi (AFP)


01:56:55 Session AFP/SequentInvertibility (AFP)


01:56:55 Session HOL/HOL-ZF


01:56:56 Session AFP/Category2 (AFP)


01:56:56 Session AFP/HereditarilyFinite (AFP)


01:56:56 Session AFP/HyperCTL (AFP)


01:56:56 Session AFP/Integration (AFP)


01:56:56 Session AFP/Isabelle_Meta_Model (AFP)


01:56:56 Session Doc/Isar_Ref (doc)


01:56:56 Session AFP/LTL (AFP)


01:56:56 Session AFP/Stuttering_Equivalence (AFP)


01:56:56 Session AFP/Lambda_Free_RPOs (AFP)


01:56:56 Session AFP/Landau_Symbols (AFP)


01:56:56 Session AFP/Akra_Bazzi (AFP)


01:56:57 Session AFP/Catalan_Numbers (AFP)


01:56:57 Session AFP/Error_Function (AFP)


01:56:57 Session AFP/Euler_MacLaurin (AFP)


01:56:57 Session AFP/Stirling_Formula (AFP)


01:56:57 Session AFP/LightweightJava (AFP)


01:56:57 Session AFP/LinearQuantifierElim (AFP)


01:56:57 Session AFP/List-Infinite (AFP)


01:56:57 Session AFP/Nat-Interval-Logic (AFP)


01:56:57 Session AFP/AutoFocus-Stream (AFP)


01:56:57 Session AFP/MuchAdoAboutTwo (AFP)


01:56:57 Session AFP/Optics (AFP)


01:56:57 Session AFP/POPLmark-deBruijn (AFP)


01:56:57 Session AFP/Pairing_Heap (AFP)


01:56:57 Session AFP/Password_Authentication_Protocol (AFP)


01:56:57 Session AFP/Presburger-Automata (AFP)


01:56:58 Session AFP/Priority_Queue_Braun (AFP)


01:56:58 Session AFP/Program-Conflict-Analysis (AFP)


01:56:58 Session AFP/Regular-Sets (AFP)


01:56:58 Session AFP/Abstract-Rewriting (AFP)


01:56:58 Session AFP/Decreasing-Diagrams (AFP)


01:56:58 Session AFP/First_Order_Terms (AFP)


01:56:58 Session AFP/Matrix (AFP)


01:56:58 Session AFP/Matrix_Tensor (AFP)


01:56:58 Session AFP/Knot_Theory (AFP)


01:56:58 Session AFP/Coinductive_Languages (AFP)


01:56:58 Session AFP/Finite_Automata_HF (AFP)


01:56:58 Session AFP/Functional-Automata (AFP)


01:56:58 Session AFP/Posix-Lexing (AFP)


01:56:58 Session AFP/Ribbon_Proofs (AFP)


01:56:58 Session AFP/SATSolverVerification (AFP)


01:56:59 Session AFP/Selection_Heap_Sort (AFP)


01:56:59 Session AFP/Skew_Heap (AFP)


01:56:59 Session AFP/Splay_Tree (AFP)


01:56:59 Session AFP/Amortized_Complexity (AFP)


01:56:59 Session AFP/Dynamic_Tables (AFP)


01:56:59 Session AFP/Root_Balanced_Tree (AFP)


01:56:59 Session AFP/Stable_Matching (AFP)


01:56:59 Session AFP/SuperCalc (AFP)


01:56:59 Session AFP/Tail_Recursive_Functions (AFP)


01:57:00 Session AFP/TortoiseHare (AFP)


01:57:00 Session AFP/Trie (AFP)


01:57:00 Session AFP/Twelvefold_Way (AFP)


01:57:00 Session AFP/Vickrey_Clarke_Groves (AFP)


01:57:00 Session HOL/HOL-Statespace


01:57:00 Session HOL/HOL-Types_To_Sets


01:57:00 Session HOL/HOL-Word (main timing)


01:57:00 Session HOL/HOL-SPARK (main)


01:57:00 Session HOL/HOL-SPARK-Examples


01:57:00 Session AFP/RIPEMD-160-SPARK (AFP)


01:57:00 Session AFP/Kleene_Algebra (AFP)


01:57:00 Session AFP/KAT_and_DRA (AFP)


01:57:01 Session AFP/Multirelations (AFP)


01:57:01 Session AFP/Regular_Algebras (AFP)


01:57:01 Session AFP/Relation_Algebra (AFP)


01:57:01 Session AFP/Residuated_Lattices (AFP)


01:57:01 Session AFP/Native_Word (AFP)


01:57:01 Session AFP/WebAssembly (AFP)


01:57:01 Session AFP/Refine_Monadic (AFP)


01:57:02 Session AFP/Collections (AFP)


01:57:02 Session AFP/Abstract_Completeness (AFP)


01:57:02 Session AFP/Abstract_Soundness (AFP)


01:57:02 Session AFP/Incredible_Proof_Machine (AFP)


01:57:02 Session AFP/Deriving (AFP)


01:57:03 Session AFP/CAVA_Base (AFP)


01:57:03 Session AFP/CAVA_Automata (AFP)


01:57:03 Session AFP/DFS_Framework (AFP)


01:57:03 Session AFP/Gabow_SCC (AFP)


01:57:03 Session AFP/LTL_to_GBA (AFP)


01:57:03 Session AFP/CAVA_buildchain1 (AFP)


01:57:04 Session AFP/Promela (AFP)


01:57:04 Session AFP/CAVA_buildchain3 (AFP)


01:57:04 Session AFP/CAVA_LTL_Modelchecker (AFP)


01:57:04 Session AFP/Containers (AFP)


01:57:04 Session AFP/Collections_Examples (AFP)


01:57:05 Session AFP/Containers-Benchmarks (AFP)


01:57:05 Session AFP/Datatype_Order_Generator (AFP)


01:57:05 Session AFP/Old_Datatype_Show (AFP)


01:57:06 Session AFP/Show (AFP)


01:57:06 Session AFP/JNF-AFP-Lib (AFP)


01:57:06 Session AFP/Polynomials (AFP)


01:57:06 Session AFP/Groebner_Bases (AFP)


01:57:06 Session AFP/Real_Impl (AFP)


01:57:07 Session AFP/QR_Decomposition (AFP)


01:57:07 Session AFP/Dijkstra_Shortest_Path (AFP)


01:57:07 Session AFP/Koenigsberg_Friendship (AFP)


01:57:07 Session AFP/Transition_Systems_and_Automata (AFP)


01:57:08 Session AFP/Buchi_Complementation (AFP)


01:57:08 Session AFP/Partial_Order_Reduction (AFP)


01:57:08 Session AFP/Transitive-Closure (AFP)


01:57:08 Session AFP/KBPs (AFP)


01:57:08 Session AFP/Tree-Automata (AFP)


01:57:08 Session AFP/SPARCv8 (AFP)


01:57:08 Session AFP/Separation_Algebra (AFP)


01:57:09 Session AFP/Separata (AFP)


01:57:09 Session AFP/Separation_Logic_Imperative_HOL (AFP)


01:57:09 Session AFP/Sepref_Prereq (AFP)


01:57:09 Session AFP/ROBDD (AFP)


01:57:10 Session AFP/UpDown_Scheme (AFP)


01:57:10 Session AFP/Word_Lib (AFP)


01:57:10 Session AFP/Complx (AFP)


01:57:10 Session AFP/IEEE_Floating_Point (AFP)


01:57:10 Session AFP/IP_Addresses (AFP)


01:57:10 Session AFP/Simple_Firewall (AFP)


01:57:10 Session AFP/Routing (AFP)


01:57:11 Session AFP/Iptables_Semantics (AFP)


01:57:11 Session AFP/Iptables_Semantics_Examples (AFP)


01:57:11 Session AFP/LOFT (AFP)


01:57:11 Session AFP/LEM (AFP)


01:57:11 Session AFP/CakeML (AFP)


01:57:11 Session HOL/HOLCF (main timing)


01:57:12 Session AFP/Circus (AFP)


01:57:12 Session HOL/HOLCF-Library


01:57:12 Session AFP/PCF (AFP)


01:57:12 Session AFP/HOLCF-Prelude (AFP)


01:57:12 Session AFP/Shivers-CFA (AFP)


01:57:12 Session AFP/Stream-Fusion (AFP)


01:57:12 Session AFP/Tycon (AFP)


01:57:12 Session AFP/WorkerWrapper (AFP)


01:57:12 Session AFP/Heard_Of (AFP)


01:57:12 Session AFP/Consensus_Refined (AFP)


01:57:13 Session AFP/Hoare_Time (AFP)


01:57:13 Session AFP/HotelKeyCards (AFP)


01:57:13 Session AFP/Huffman (AFP)


01:57:13 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)


01:57:13 Session AFP/Impossible_Geometry (AFP)


01:57:13 Session AFP/Inductive_Confidentiality (AFP)


01:57:13 Session AFP/InfPathElimination (AFP)


01:57:13 Session AFP/JiveDataStoreModel (AFP)


01:57:13 Session AFP/KAD (AFP)


01:57:13 Session AFP/Algebraic_VCs (AFP)


01:57:13 Session AFP/Key_Agreement_Strong_Adversaries (AFP)


01:57:13 Session AFP/LambdaMu (AFP)


01:57:13 Session AFP/LatticeProperties (AFP)


01:57:13 Session AFP/DataRefinementIBP (AFP)


01:57:13 Session AFP/GraphMarkingIBP (AFP)


01:57:13 Session AFP/Lazy_Case (AFP)


01:57:13 Session AFP/Dict_Construction (AFP)


01:57:13 Session AFP/Lifting_Definition_Option (AFP)


01:57:14 Session AFP/List-Index (AFP)


01:57:14 Session AFP/Affine_Arithmetic (AFP)


01:57:14 Session AFP/Taylor_Models (AFP)


01:57:14 Session AFP/Comparison_Sort_Lower_Bound (AFP)


01:57:14 Session AFP/Formula_Derivatives (AFP)


01:57:15 Session AFP/Formula_Derivatives-Examples (AFP)


01:57:15 Session AFP/Jinja (AFP)


01:57:15 Session AFP/HRB-Slicing (AFP)


01:57:15 Session AFP/InformationFlowSlicing_Inter (AFP)


01:57:15 Session AFP/Slicing (AFP)


01:57:15 Session AFP/Formal_SSA (AFP)


01:57:15 Session AFP/Minimal_SSA (AFP)


01:57:16 Session AFP/InformationFlowSlicing (AFP)


01:57:16 Session AFP/LTL_to_DRA (AFP)


01:57:16 Session AFP/List_Update (AFP)


01:57:16 Session AFP/Ordinary_Differential_Equations (AFP)


01:57:16 Session AFP/Differential_Dynamic_Logic (AFP)


01:57:17 Session AFP/HOL-ODE-Numerics (AFP)


01:57:17 Session AFP/HOL-ODE-Examples (AFP)


01:57:17 Session AFP/Lorenz_Approximation (AFP)


01:57:17 Session AFP/Lorenz_C1 (AFP)


01:57:18 Session AFP/Quick_Sort_Cost (AFP)


01:57:18 Session AFP/Random_BSTs (AFP)


01:57:18 Session AFP/Treaps (AFP)


01:57:18 Session AFP/Randomised_Social_Choice (AFP)


01:57:18 Session AFP/Fishburn_Impossibility (AFP)


01:57:18 Session AFP/SDS_Impossibility (AFP)


01:57:19 Session AFP/Refine_Imperative_HOL (AFP)


01:57:19 Session AFP/Floyd_Warshall (AFP)


01:57:19 Session AFP/Sepref_Basic (AFP)


01:57:19 Session AFP/Sepref_IICF (AFP)


01:57:19 Session AFP/Knuth_Morris_Pratt (AFP)


01:57:20 Session AFP/Maxflow_Lib (AFP)


01:57:20 Session AFP/Flow_Networks (AFP)


01:57:20 Session AFP/EdmondsKarp_Maxflow (AFP)


01:57:20 Session AFP/MFMC_Countable (AFP)


01:57:20 Session AFP/Prpu_Maxflow (AFP)


01:57:21 Session AFP/VerifyThis2018 (AFP)


01:57:21 Session AFP/List_Interleaving (AFP)


01:57:21 Session AFP/LocalLexing (AFP)


01:57:21 Session AFP/Lowe_Ontological_Argument (AFP)


01:57:21 Session AFP/MSO_Regex_Equivalence (AFP)


01:57:21 Session AFP/MSO_Examples (AFP)


01:57:21 Session AFP/Marriage (AFP)


01:57:21 Session AFP/Latin_Square (AFP)


01:57:21 Session AFP/Max-Card-Matching (AFP)


01:57:21 Session AFP/Median_Of_Medians_Selection (AFP)


01:57:22 Session AFP/Menger (AFP)


01:57:22 Session AFP/MiniML (AFP)


01:57:22 Session AFP/Modular_Assembly_Kit_Security (AFP)


01:57:22 Session AFP/Monad_Memo_DP (AFP)


01:57:22 Session AFP/Hidden_Markov_Models (AFP)


01:57:22 Session AFP/Optimal_BST (AFP)


01:57:22 Session AFP/MonoBoolTranAlgebra (AFP)


01:57:22 Session AFP/Name_Carrying_Type_Inference (AFP)


01:57:22 Session AFP/Network_Security_Policy_Verification (AFP)


01:57:23 Session AFP/No_FTL_observers (AFP)


01:57:23 Session AFP/Nominal2 (AFP)


01:57:23 Session AFP/Incompleteness (AFP)


01:57:24 Session AFP/Surprise_Paradox (AFP)


01:57:24 Session AFP/Launchbury (AFP)


01:57:24 Session AFP/Call_Arity (AFP)


01:57:24 Session AFP/Modal_Logics_for_NTS (AFP)


01:57:24 Session AFP/Rewriting_Z (AFP)


01:57:24 Session AFP/Noninterference_CSP (AFP)


01:57:24 Session AFP/Noninterference_Ipurge_Unwinding (AFP)


01:57:24 Session AFP/Noninterference_Generic_Unwinding (AFP)


01:57:24 Session AFP/Noninterference_Inductive_Unwinding (AFP)


01:57:24 Session AFP/Noninterference_Sequential_Composition (AFP)


01:57:24 Session AFP/Noninterference_Concurrent_Composition (AFP)


01:57:24 Session AFP/NormByEval (AFP)


01:57:24 Session AFP/OpSets (AFP)


01:57:24 Session AFP/Open_Induction (AFP)


01:57:24 Session AFP/Well_Quasi_Orders (AFP)


01:57:25 Session AFP/Decreasing-Diagrams-II (AFP)


01:57:25 Session AFP/Myhill-Nerode (AFP)


01:57:25 Session AFP/Ordinal (AFP)


01:57:25 Session AFP/Nested_Multisets_Ordinals (AFP)


01:57:25 Session AFP/Lambda_Free_KBOs (AFP)


01:57:25 Session AFP/Ordered_Resolution_Prover (AFP)


01:57:25 Session AFP/PLM (AFP)


01:57:26 Session AFP/PSemigroupsConvolution (AFP)


01:57:26 Session AFP/Paraconsistency (AFP)


01:57:26 Session AFP/Parity_Game (AFP)


01:57:26 Session AFP/Partial_Function_MR (AFP)


01:57:26 Session AFP/Certification_Monads (AFP)


01:57:26 Session AFP/XML (AFP)


01:57:26 Session AFP/Pre_Polynomial_Factorization (AFP)


01:57:26 Session AFP/Polynomial_Factorization (AFP)


01:57:27 Session AFP/Dirichlet_Series (AFP)


01:57:27 Session AFP/Zeta_Function (AFP)


01:57:27 Session AFP/Dirichlet_L (AFP)


01:57:28 Session AFP/Jordan_Normal_Form (AFP)


01:57:28 Session AFP/Deep_Learning_Lib (AFP)


01:57:28 Session AFP/Deep_Learning (AFP)


01:57:29 Session AFP/Perron_Frobenius (AFP)


01:57:29 Session AFP/Stochastic_Matrices (AFP)


01:57:29 Session AFP/Subresultants (AFP)


01:57:30 Session AFP/Pre_BZ (AFP)


01:57:30 Session AFP/Berlekamp_Zassenhaus (AFP)


01:57:30 Session AFP/Algebraic_Numbers (AFP)


01:57:30 Session AFP/Algebraic_Numbers_Lib (AFP)


01:57:31 Session AFP/Linear_Recurrences (AFP)


01:57:31 Session AFP/Linear_Recurrences_Test (AFP)


01:57:31 Session AFP/LLL_Basis_Reduction (AFP)


01:57:31 Session AFP/LLL_Factorization (AFP)


01:57:32 Session AFP/Probabilistic_While (AFP)


01:57:32 Session AFP/Pop_Refinement (AFP)


01:57:32 Session AFP/Possibilistic_Noninterference (AFP)


01:57:32 Session AFP/Proof_Strategy_Language (AFP)


01:57:32 Session AFP/PropResPI (AFP)


01:57:32 Session AFP/Propositional_Proof_Systems (AFP)


01:57:32 Session AFP/PseudoHoops (AFP)


01:57:32 Session AFP/Ramsey-Infinite (AFP)


01:57:32 Session AFP/Recursion-Theory-I (AFP)


01:57:32 Session AFP/RefinementReactive (AFP)


01:57:33 Session AFP/Regex_Equivalence (AFP)


01:57:33 Session AFP/Resolution_FOL (AFP)


01:57:33 Session AFP/Robbins-Conjecture (AFP)


01:57:33 Session AFP/Roy_Floyd_Warshall (AFP)


01:57:33 Session AFP/SIFPL (AFP)


01:57:33 Session AFP/SIFUM_Type_Systems (AFP)


01:57:33 Session AFP/Security_Protocol_Refinement (AFP)


01:57:33 Session AFP/SenSocialChoice (AFP)


01:57:33 Session AFP/Simpl (AFP)


01:57:34 Session AFP/BDD (AFP)


01:57:34 Session AFP/Planarity_Certificates (AFP)


01:57:34 Session AFP/Statecharts (AFP)


01:57:34 Session AFP/Stone_Algebras (AFP)


01:57:34 Session AFP/Stone_Relation_Algebras (AFP)


01:57:34 Session AFP/Stone_Kleene_Relation_Algebras (AFP)


01:57:34 Session AFP/Strong_Security (AFP)


01:57:34 Session AFP/TLA (AFP)


01:57:34 Session AFP/Timed_Automata (AFP)


01:57:34 Session AFP/PTA_library (AFP)


01:57:34 Session AFP/Probabilistic_Timed_Automata (AFP)


01:57:35 Session AFP/Transitive-Closure-II (AFP)


01:57:35 Session AFP/Tree_Decomposition (AFP)


01:57:35 Session AFP/Types_Tableaus_and_Goedels_God (AFP)


01:57:35 Session AFP/UPF (AFP)


01:57:35 Session AFP/UPF_Firewall (AFP)


01:57:35 Session AFP/Verified-Prover (AFP)


01:57:35 Session AFP/VolpanoSmith (AFP)


01:57:35 Session AFP/WHATandWHERE_Security (AFP)


01:57:35 Session AFP/Weight_Balanced_Trees (AFP)


01:57:35 Session HOL/HOL-Proofs (timing)


01:57:35 Session HOL/HOL-Proofs-Lambda (timing)


01:57:35 Session AFP/Applicative_Lifting (AFP)


01:57:36 Session AFP/CryptHOL (AFP)


01:57:36 Session AFP/Game_Based_Crypto (AFP)


01:57:36 Session AFP/Free-Groups (AFP)


01:57:37 Session AFP/Locally-Nameless-Sigma (AFP)


01:57:37 Session AFP/Stern_Brocot (AFP)


01:57:37 Session Unsorted/Spec_Check


01:57:37 Session AFP/Regex_Equivalence_Examples (AFP)


01:57:47 Building HOL-Algebra ...


01:57:51 HOL-Algebra: theory HOL-Algebra.Exponent


01:57:51 HOL-Algebra: theory HOL-Algebra.Congruence


01:57:52 HOL-Algebra: theory HOL-Algebra.Order


01:57:53 HOL-Algebra: theory HOL-Algebra.Lattice


01:57:55 HOL-Algebra: theory HOL-Algebra.Complete_Lattice


01:57:56 HOL-Algebra: theory HOL-Algebra.Galois_Connection


01:57:56 HOL-Algebra: theory HOL-Algebra.Group


01:57:58 HOL-Algebra: theory HOL-Algebra.Bij


01:57:58 HOL-Algebra: theory HOL-Algebra.Coset


01:57:58 HOL-Algebra: theory HOL-Algebra.FiniteProduct


01:57:59 HOL-Algebra: theory HOL-Algebra.Ring


01:57:59 HOL-Algebra: theory HOL-Algebra.Group_Action


01:58:00 HOL-Algebra: theory HOL-Algebra.Sylow


01:58:01 HOL-Algebra: theory HOL-Algebra.Zassenhaus


01:58:01 HOL-Algebra: theory HOL-Algebra.Divisibility


01:58:03 HOL-Algebra: theory HOL-Algebra.AbelCoset


01:58:06 HOL-Algebra: theory HOL-Algebra.Module


01:58:09 HOL-Algebra: theory HOL-Algebra.Ideal


01:58:11 HOL-Algebra: theory HOL-Algebra.RingHom


01:58:13 HOL-Algebra: theory HOL-Algebra.QuotRing


01:58:13 HOL-Algebra: theory HOL-Algebra.UnivPoly


01:58:13 HOL-Algebra: theory HOL-Algebra.IntRing


01:58:26 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group


01:59:45 Timing HOL-Algebra (2 threads, 82.738s elapsed time, 153.624s cpu time, 18.784s GC time, factor 1.86)


01:59:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra


01:59:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf


01:59:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf


01:59:45 Finished HOL-Algebra (0:01:56 elapsed time, 0:03:24 cpu time, factor 1.76)


01:59:45 Building JNF-HOL-Lib ...


01:59:45 Running VectorSpace ...


01:59:45 Running Jordan_Hoelder ...


01:59:45 Running Orbit_Stabiliser ...


01:59:45 Running Secondary_Sylow ...


01:59:45 Running Perfect-Number-Thm ...


01:59:47 VectorSpace: theory VectorSpace.RingModuleFacts


01:59:47 VectorSpace: theory VectorSpace.FunctionLemmas


01:59:47 Jordan_Hoelder: theory Secondary_Sylow.GroupAction


01:59:47 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses


01:59:47 JNF-HOL-Lib: theory HOL-Cardinals.Order_Union


01:59:47 Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset


01:59:47 Secondary_Sylow: theory Secondary_Sylow.GroupAction


01:59:47 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics


01:59:47 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma


01:59:47 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser


01:59:47 JNF-HOL-Lib: theory HOL-Cardinals.Wellorder_Extension


01:59:47 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron


01:59:47 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect


01:59:47 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation


01:59:47 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation


01:59:48 Jordan_Hoelder: theory Secondary_Sylow.SndSylow


01:59:48 VectorSpace: theory VectorSpace.MonoidSums


01:59:48 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp


01:59:48 Secondary_Sylow: theory Secondary_Sylow.SndSylow


01:59:48 VectorSpace: theory VectorSpace.LinearCombinations


01:59:48 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups


01:59:49 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups


01:59:49 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups


01:59:49 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries


01:59:50 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder


01:59:52 Timing Perfect-Number-Thm (2 threads, 1.742s elapsed time, 3.412s cpu time, 0.000s GC time, factor 1.96)


01:59:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm


01:59:52 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/document.pdf


01:59:52 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/outline.pdf


01:59:52 Finished Perfect-Number-Thm (0:00:06 elapsed time, 0:00:12 cpu time, factor 1.80)


01:59:54 VectorSpace: theory VectorSpace.SumSpaces


01:59:55 VectorSpace: theory VectorSpace.VectorSpace


01:59:57 Timing Secondary_Sylow (2 threads, 5.634s elapsed time, 9.560s cpu time, 0.440s GC time, factor 1.70)


01:59:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow


01:59:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/document.pdf


01:59:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/outline.pdf


01:59:57 Finished Secondary_Sylow (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.73)


02:00:03 Timing Orbit_Stabiliser (2 threads, 11.545s elapsed time, 15.684s cpu time, 0.780s GC time, factor 1.36)


02:00:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser


02:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser/document.pdf


02:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser/outline.pdf


02:00:03 Finished Orbit_Stabiliser (0:00:17 elapsed time, 0:00:25 cpu time, factor 1.50)


02:00:06 Timing JNF-HOL-Lib (2 threads, 1.708s elapsed time, 2.804s cpu time, 0.000s GC time, factor 1.64)


02:00:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/JNF-HOL-Lib


02:00:06 Finished JNF-HOL-Lib (0:00:20 elapsed time, 0:00:27 cpu time, factor 1.33)


02:00:06 Building JNF-AFP-Lib ...


02:00:09 Timing Jordan_Hoelder (2 threads, 17.222s elapsed time, 32.076s cpu time, 1.668s GC time, factor 1.86)


02:00:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder


02:00:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/document.pdf


02:00:09 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/outline.pdf


02:00:09 Finished Jordan_Hoelder (0:00:23 elapsed time, 0:00:43 cpu time, factor 1.84)


02:00:13 JNF-AFP-Lib: theory Containers.Extend_Partial_Order


02:00:13 JNF-AFP-Lib: theory Containers.Equal


02:00:13 JNF-AFP-Lib: theory Containers.Closure_Set


02:00:13 JNF-AFP-Lib: theory Containers.List_Fusion


02:00:13 JNF-AFP-Lib: theory Deriving.Comparator


02:00:14 JNF-AFP-Lib: theory Deriving.Compare


02:00:14 JNF-AFP-Lib: theory Deriving.Derive_Manager


02:00:14 JNF-AFP-Lib: theory Deriving.Generator_Aux


02:00:14 JNF-AFP-Lib: theory Containers.Containers_Auxiliary


02:00:14 JNF-AFP-Lib: theory Deriving.Comparator_Generator


02:00:14 JNF-AFP-Lib: theory Deriving.Equality_Generator


02:00:15 JNF-AFP-Lib: theory Deriving.Equality_Instances


02:00:15 JNF-AFP-Lib: theory Containers.Lexicographic_Order


02:00:15 JNF-AFP-Lib: theory Deriving.Compare_Generator


02:00:15 JNF-AFP-Lib: theory Gauss_Jordan.IArray_Addenda


02:00:15 JNF-AFP-Lib: theory Deriving.Compare_Instances


02:00:16 JNF-AFP-Lib: theory Gauss_Jordan.IArray_Haskell


02:00:16 JNF-AFP-Lib: theory Abstract-Rewriting.Seq


02:00:16 JNF-AFP-Lib: theory Containers.Containers_Generator


02:00:16 JNF-AFP-Lib: theory Containers.Set_Linorder


02:00:16 JNF-AFP-Lib: theory Containers.Collection_Enum


02:00:17 JNF-AFP-Lib: theory Containers.Collection_Eq


02:00:18 JNF-AFP-Lib: theory Containers.DList_Set


02:00:19 JNF-AFP-Lib: theory Containers.RBT_ext


02:00:21 JNF-AFP-Lib: theory Deriving.RBT_Comparator_Impl


02:00:27 JNF-AFP-Lib: theory Polynomial_Interpolation.Missing_Unsorted


02:00:29 JNF-AFP-Lib: theory Containers.Collection_Order


02:00:29 JNF-AFP-Lib: theory Polynomial_Interpolation.Missing_Polynomial


02:00:30 JNF-AFP-Lib: theory Matrix.Utility


02:00:31 JNF-AFP-Lib: theory Polynomial_Interpolation.Ring_Hom


02:00:31 JNF-AFP-Lib: theory Containers.RBT_Mapping2


02:00:33 JNF-AFP-Lib: theory Containers.RBT_Set2


02:00:33 Timing VectorSpace (2 threads, 41.555s elapsed time, 73.020s cpu time, 7.352s GC time, factor 1.76)


02:00:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace


02:00:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/document.pdf


02:00:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/outline.pdf


02:00:33 Finished VectorSpace (0:00:47 elapsed time, 0:01:24 cpu time, factor 1.77)


02:00:33 JNF-AFP-Lib: theory Polynomial_Interpolation.Ring_Hom_Poly


02:00:34 JNF-AFP-Lib: theory Containers.Set_Impl


02:00:35 JNF-AFP-Lib: theory Regular-Sets.Regular_Set


02:00:38 JNF-AFP-Lib: theory Regular-Sets.Regular_Exp


02:00:43 JNF-AFP-Lib: theory Regular-Sets.NDerivative


02:00:47 JNF-AFP-Lib: theory Regular-Sets.Equivalence_Checking


02:00:47 JNF-AFP-Lib: theory Regular-Sets.Relation_Interpretation


02:00:47 JNF-AFP-Lib: theory Regular-Sets.Regexp_Method


02:00:48 JNF-AFP-Lib: theory Abstract-Rewriting.Abstract_Rewriting


02:00:50 JNF-AFP-Lib: theory Abstract-Rewriting.Relative_Rewriting


02:00:51 JNF-AFP-Lib: theory Abstract-Rewriting.SN_Orders


02:00:52 JNF-AFP-Lib: theory Show.Show


02:00:53 JNF-AFP-Lib: theory Abstract-Rewriting.SN_Order_Carrier


02:00:53 JNF-AFP-Lib: theory Matrix.Ordered_Semiring


02:00:54 JNF-AFP-Lib: theory Show.Show_Instances


02:00:56 JNF-AFP-Lib: theory VectorSpace.FunctionLemmas


02:00:56 JNF-AFP-Lib: theory VectorSpace.RingModuleFacts


02:00:56 JNF-AFP-Lib: theory VectorSpace.MonoidSums


02:00:57 JNF-AFP-Lib: theory VectorSpace.LinearCombinations


02:01:02 JNF-AFP-Lib: theory VectorSpace.SumSpaces


02:01:02 JNF-AFP-Lib: theory VectorSpace.VectorSpace


02:03:07 Timing JNF-AFP-Lib (2 threads, 139.641s elapsed time, 256.636s cpu time, 22.228s GC time, factor 1.84)


02:03:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/JNF-AFP-Lib


02:03:07 Finished JNF-AFP-Lib (0:02:59 elapsed time, 0:05:20 cpu time, factor 1.78)


02:03:07 Building Jordan_Normal_Form ...


02:03:08 Building Pre_Polynomial_Factorization ...


02:03:10 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring


02:03:10 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Improved_Code_Equations


02:03:10 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Neville_Aitken_Interpolation


02:03:10 Pre_Polynomial_Factorization: theory Cauchy.CauchysMeanTheorem


02:03:10 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Lagrange_Interpolation


02:03:10 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary


02:03:11 Pre_Polynomial_Factorization: theory Partial_Function_MR.Partial_Function_MR


02:03:11 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Divmod_Int


02:03:11 Pre_Polynomial_Factorization: theory Show.Show_Poly


02:03:11 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Is_Rat_To_Rat


02:03:12 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Log_Impl


02:03:12 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Newton_Interpolation


02:03:12 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.NthRoot_Impl


02:03:13 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Permutations


02:03:13 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian


02:03:15 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial


02:03:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate


02:03:15 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized


02:03:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix


02:03:16 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Polynomial_Interpolation


02:03:17 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound


02:03:17 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic


02:03:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace


02:03:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination


02:03:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl


02:03:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations


02:03:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant


02:03:24 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl


02:03:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl


02:03:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm


02:03:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix


02:03:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code


02:03:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly


02:03:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form


02:03:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison


02:03:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier


02:03:31 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix


02:03:34 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect


02:03:35 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity


02:03:38 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt


02:03:38 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel


02:03:40 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition


02:03:41 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness


02:03:44 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence


02:03:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl


02:03:49 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius


02:03:55 Timing Pre_Polynomial_Factorization (2 threads, 23.946s elapsed time, 45.776s cpu time, 2.472s GC time, factor 1.91)


02:03:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization


02:03:55 Finished Pre_Polynomial_Factorization (0:00:46 elapsed time, 0:01:16 cpu time, factor 1.64)


02:03:55 Running Polynomial_Factorization ...


02:03:57 Polynomial_Factorization: theory Polynomial_Factorization.Precomputation


02:03:57 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial


02:03:57 Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial


02:03:58 Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility


02:03:58 Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized


02:03:58 Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots


02:03:58 Polynomial_Factorization: theory Polynomial_Factorization.Missing_List


02:03:58 Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly


02:04:00 Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma


02:04:01 Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly


02:04:01 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset


02:04:01 Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization


02:04:01 Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization


02:04:02 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test


02:04:03 Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization


02:04:05 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization


02:04:56 Timing Polynomial_Factorization (2 threads, 53.050s elapsed time, 89.188s cpu time, 3.956s GC time, factor 1.68)


02:04:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization


02:04:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf


02:04:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf


02:04:56 Finished Polynomial_Factorization (0:01:00 elapsed time, 0:01:42 cpu time, factor 1.69)


02:08:00 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List


02:08:00 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist


02:08:00 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank


02:08:00 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix


02:08:06 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix


02:08:56 Timing Jordan_Normal_Form (2 threads, 304.410s elapsed time, 507.208s cpu time, 20.532s GC time, factor 1.67)


02:08:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form


02:08:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form/document.pdf


02:08:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Normal_Form/outline.pdf


02:08:56 Finished Jordan_Normal_Form (0:05:47 elapsed time, 0:09:31 cpu time, factor 1.64)


02:08:56 Building Subresultants ...


02:08:56 Running Perron_Frobenius ...


02:08:58 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial


02:08:58 Subresultants: theory Subresultants.Coeff_Int


02:08:58 Perron_Frobenius: theory HOL-Eisbach.Eisbach


02:08:58 Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets


02:08:58 Subresultants: theory Subresultants.Dichotomous_Lazard


02:08:58 Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable


02:08:59 Subresultants: theory Subresultants.More_Homomorphisms


02:08:59 Perron_Frobenius: theory HOL-Analysis.Inner_Product


02:08:59 Subresultants: theory Subresultants.Resultant_Prelim


02:08:59 Perron_Frobenius: theory HOL-Analysis.L2_Norm


02:08:59 Perron_Frobenius: theory HOL-Analysis.Operator_Norm


02:08:59 Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Divisibility


02:08:59 Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial


02:08:59 Subresultants: theory Subresultants.Binary_Exponentiation


02:09:00 Subresultants: theory Subresultants.Subresultant


02:09:00 Perron_Frobenius: theory Sturm_Sequences.Sturm_Library


02:09:00 Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem


02:09:00 Perron_Frobenius: theory HOL-Analysis.Product_Vector


02:09:01 Perron_Frobenius: theory HOL-Analysis.Euclidean_Space


02:09:01 Perron_Frobenius: theory Sturm_Sequences.Sturm_Method


02:09:02 Perron_Frobenius: theory HOL-Analysis.Norm_Arith


02:09:02 Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization


02:09:03 Perron_Frobenius: theory HOL-Analysis.Linear_Algebra


02:09:04 Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product


02:09:05 Subresultants: theory Subresultants.Subresultant_Gcd


02:09:05 Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space


02:09:07 Perron_Frobenius: theory HOL-Analysis.Cartesian_Space


02:09:08 Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order


02:09:12 Perron_Frobenius: theory HOL-Analysis.Connected


02:09:13 Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits


02:09:14 Perron_Frobenius: theory HOL-Analysis.Summation_Tests


02:09:15 Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space


02:09:15 Perron_Frobenius: theory HOL-Analysis.Uniform_Limit


02:09:17 Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function


02:09:20 Perron_Frobenius: theory HOL-Analysis.Starlike


02:09:24 Perron_Frobenius: theory HOL-Analysis.Continuous_Extension


02:09:24 Perron_Frobenius: theory HOL-Analysis.Path_Connected


02:09:28 Perron_Frobenius: theory HOL-Analysis.Homeomorphism


02:09:29 Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint


02:09:32 Perron_Frobenius: theory HOL-Analysis.Derivative


02:09:37 Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space


02:09:38 Perron_Frobenius: theory HOL-Analysis.Determinants


02:09:39 Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type


02:09:41 Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous


02:10:39 Timing Subresultants (2 threads, 72.519s elapsed time, 110.388s cpu time, 3.604s GC time, factor 1.52)


02:10:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants


02:10:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants/document.pdf


02:10:39 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Subresultants/outline.pdf


02:10:39 Finished Subresultants (0:01:42 elapsed time, 0:02:35 cpu time, factor 1.51)


02:10:39 Building Pre_BZ ...


02:10:42 Pre_BZ: theory Efficient-Mergesort.Efficient_Sort


02:10:42 Pre_BZ: theory HOL-Number_Theory.Cong


02:10:43 Pre_BZ: theory Polynomial_Factorization.Precomputation


02:10:44 Pre_BZ: theory HOL-Types_To_Sets.Types_To_Sets


02:10:44 Pre_BZ: theory HOL-Word.Bits


02:10:44 Pre_BZ: theory HOL-Word.Bits_Bit


02:10:44 Pre_BZ: theory HOL-Word.Misc_Numeric


02:10:44 Pre_BZ: theory HOL-Word.Bit_Representation


02:10:45 Pre_BZ: theory HOL-Word.Bits_Int


02:10:47 Pre_BZ: theory HOL-Word.Bool_List_Representation


02:10:48 Pre_BZ: theory Native_Word.More_Bits_Int


02:10:49 Pre_BZ: theory HOL-Word.Word_Miscellaneous


02:10:49 Pre_BZ: theory HOL-Word.Misc_Typedef


02:10:49 Pre_BZ: theory HOL-Word.Word


02:10:49 Pre_BZ: theory Native_Word.Bits_Integer


02:10:55 Pre_BZ: theory Native_Word.Word_Misc


02:10:56 Pre_BZ: theory Polynomial_Interpolation.Improved_Code_Equations


02:10:56 Pre_BZ: theory Polynomial_Interpolation.Neville_Aitken_Interpolation


02:10:57 Pre_BZ: theory Cauchy.CauchysMeanTheorem


02:10:57 Pre_BZ: theory Polynomial_Factorization.Polynomial_Divisibility


02:10:57 Pre_BZ: theory Polynomial_Interpolation.Lagrange_Interpolation


02:10:57 Pre_BZ: theory HOL-Number_Theory.Totient


02:10:58 Pre_BZ: theory HOL-Number_Theory.Residues


02:11:00 Pre_BZ: theory Native_Word.Code_Target_Bits_Int


02:11:02 Pre_BZ: theory Native_Word.Uint32


02:11:02 Pre_BZ: theory Native_Word.Uint64


02:11:04 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary


02:11:04 Pre_BZ: theory Polynomial_Factorization.Missing_List


02:11:04 Pre_BZ: theory Polynomial_Interpolation.Is_Rat_To_Rat


02:11:05 Pre_BZ: theory Sqrt_Babylonian.Log_Impl


02:11:06 Pre_BZ: theory Sqrt_Babylonian.NthRoot_Impl


02:11:07 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian


02:11:07 Pre_BZ: theory Polynomial_Factorization.Missing_Multiset


02:11:07 Pre_BZ: theory Polynomial_Factorization.Prime_Factorization


02:11:07 Pre_BZ: theory Polynomial_Factorization.Explicit_Roots


02:11:08 Pre_BZ: theory Polynomial_Interpolation.Divmod_Int


02:11:08 Pre_BZ: theory Polynomial_Factorization.Dvd_Int_Poly


02:11:08 Pre_BZ: theory Polynomial_Factorization.Gauss_Lemma


02:11:08 Pre_BZ: theory Polynomial_Factorization.Square_Free_Factorization


02:11:09 Pre_BZ: theory Polynomial_Factorization.Gcd_Rat_Poly


02:11:09 Pre_BZ: theory Polynomial_Factorization.Rational_Root_Test


02:11:10 Pre_BZ: theory Polynomial_Interpolation.Newton_Interpolation


02:11:11 Pre_BZ: theory Show.Show_Poly


02:11:13 Pre_BZ: theory Polynomial_Interpolation.Polynomial_Interpolation


02:11:16 Pre_BZ: theory Polynomial_Factorization.Kronecker_Factorization


02:11:18 Pre_BZ: theory Polynomial_Factorization.Rational_Factorization


02:13:15 Perron_Frobenius: theory Perron_Frobenius.Bij_Nat


02:13:15 Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint


02:13:16 Perron_Frobenius: theory Perron_Frobenius.Roots_Unity


02:13:16 Perron_Frobenius: theory Perron_Frobenius.HMA_Connect


02:13:17 Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan


02:13:19 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux


02:13:20 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius


02:13:21 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible


02:13:21 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory


02:13:22 Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General


02:13:23 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block


02:13:26 Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2


02:13:27 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth


02:13:28 Timing Pre_BZ (2 threads, 129.899s elapsed time, 224.536s cpu time, 17.484s GC time, factor 1.73)


02:13:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_BZ


02:13:28 Finished Pre_BZ (0:02:48 elapsed time, 0:05:14 cpu time, factor 1.87)


02:13:28 Building Berlekamp_Zassenhaus ...


02:13:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Missing_Multiset2


02:13:31 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based


02:13:32 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd


02:13:32 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound


02:13:33 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication


02:13:34 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly


02:13:35 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration


02:13:37 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based


02:13:41 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based


02:13:42 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization


02:13:43 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field


02:13:46 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based


02:13:51 Timing Perron_Frobenius (2 threads, 286.268s elapsed time, 503.900s cpu time, 27.108s GC time, factor 1.76)


02:13:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius


02:13:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/document.pdf


02:13:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/outline.pdf


02:13:51 Finished Perron_Frobenius (0:04:54 elapsed time, 0:08:38 cpu time, factor 1.76)


02:13:52 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly


02:13:53 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp


02:13:54 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod


02:13:57 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field


02:13:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based


02:13:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based


02:14:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting


02:14:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure


02:14:07 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based


02:14:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound


02:14:09 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime


02:14:09 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization


02:14:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization


02:14:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl


02:14:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based


02:14:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int


02:14:15 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel


02:14:16 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction


02:14:19 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus


02:14:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly


02:14:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly


02:17:28 Timing Berlekamp_Zassenhaus (2 threads, 188.111s elapsed time, 307.100s cpu time, 19.152s GC time, factor 1.63)


02:17:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus


02:17:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/document.pdf


02:17:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Berlekamp_Zassenhaus/outline.pdf


02:17:28 Finished Berlekamp_Zassenhaus (0:03:58 elapsed time, 0:06:21 cpu time, factor 1.60)


02:17:28 Building LLL_Basis_Reduction ...


02:17:28 Building Algebraic_Numbers_Lib ...


02:17:28 Running Algebraic_Numbers ...


02:17:33 LLL_Basis_Reduction: theory HOL-Eisbach.Eisbach


02:17:33 LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray


02:17:34 LLL_Basis_Reduction: theory Perron_Frobenius.Bij_Nat


02:17:34 LLL_Basis_Reduction: theory Perron_Frobenius.Cancel_Card_Constraint


02:17:34 LLL_Basis_Reduction: theory HOL-Analysis.Continuum_Not_Denumerable


02:17:34 LLL_Basis_Reduction: theory HOL-Analysis.Inner_Product


02:17:34 LLL_Basis_Reduction: theory HOL-Analysis.L2_Norm


02:17:34 LLL_Basis_Reduction: theory HOL-Analysis.Operator_Norm


02:17:35 LLL_Basis_Reduction: theory HOL-Analysis.Norm_Arith


02:17:35 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost


02:17:35 LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation


02:17:35 LLL_Basis_Reduction: theory HOL-Analysis.Product_Vector


02:17:35 LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials


02:17:36 LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant


02:17:36 LLL_Basis_Reduction: theory HOL-Analysis.Euclidean_Space


02:17:38 LLL_Basis_Reduction: theory HOL-Analysis.Linear_Algebra


02:17:39 LLL_Basis_Reduction: theory HOL-Analysis.Finite_Cartesian_Product


02:17:39 LLL_Basis_Reduction: theory HOL-Analysis.Topology_Euclidean_Space


02:17:40 Algebraic_Numbers_Lib: theory Deriving.Compare_Rat


02:17:40 Algebraic_Numbers_Lib: theory Deriving.Compare_Real


02:17:40 Algebraic_Numbers_Lib: theory Sturm_Sequences.Misc_Polynomial


02:17:40 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Compare_Complex


02:17:40 Algebraic_Numbers: theory Deriving.Compare_Rat


02:17:40 Algebraic_Numbers: theory Deriving.Compare_Real


02:17:40 Algebraic_Numbers_Lib: theory Sturm_Sequences.Sturm_Library


02:17:40 Algebraic_Numbers_Lib: theory Sturm_Sequences.Sturm_Theorem


02:17:41 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial


02:17:41 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex


02:17:41 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library


02:17:41 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem


02:17:41 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Complex_Roots_Real_Poly


02:17:42 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Bivariate_Polynomials


02:17:42 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly


02:17:42 LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Space


02:17:42 Algebraic_Numbers_Lib: theory Show.Show_Real


02:17:42 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials


02:17:42 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Algebraic_Numbers_Prelim


02:17:42 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Resultant


02:17:43 Algebraic_Numbers: theory Show.Show_Real


02:17:43 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas


02:17:43 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim


02:17:43 Algebraic_Numbers: theory Algebraic_Numbers.Resultant


02:17:44 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Interval_Arithmetic


02:17:45 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic


02:17:45 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Algebraic_Numbers


02:17:46 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers


02:17:47 LLL_Basis_Reduction: theory HOL-Analysis.Connected


02:17:48 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Sturm_Rat


02:17:49 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat


02:17:52 LLL_Basis_Reduction: theory HOL-Analysis.Convex_Euclidean_Space


02:17:53 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Algebraic_Numbers


02:17:54 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers


02:17:55 LLL_Basis_Reduction: theory HOL-Analysis.Starlike


02:17:59 LLL_Basis_Reduction: theory HOL-Analysis.Continuous_Extension


02:18:00 LLL_Basis_Reduction: theory HOL-Analysis.Path_Connected


02:18:07 LLL_Basis_Reduction: theory HOL-Analysis.Extended_Real_Limits


02:18:07 LLL_Basis_Reduction: theory HOL-Analysis.Homeomorphism


02:18:07 LLL_Basis_Reduction: theory HOL-Analysis.Brouwer_Fixpoint


02:18:07 LLL_Basis_Reduction: theory HOL-Analysis.Summation_Tests


02:18:09 LLL_Basis_Reduction: theory HOL-Analysis.Uniform_Limit


02:18:11 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms


02:18:11 LLL_Basis_Reduction: theory HOL-Analysis.Bounded_Linear_Function


02:18:11 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Roots


02:18:11 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Alg


02:18:12 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Approx


02:18:12 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots


02:18:12 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Show_Real_Precise


02:18:12 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg


02:18:13 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx


02:18:13 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise


02:18:13 LLL_Basis_Reduction: theory HOL-Analysis.Derivative


02:18:13 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Complex_Algebraic_Numbers


02:18:13 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers


02:18:15 LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Euclidean_Space


02:18:17 LLL_Basis_Reduction: theory HOL-Analysis.Determinants


02:18:17 Algebraic_Numbers_Lib: theory Algebraic_Numbers.Real_Factorization


02:18:18 Algebraic_Numbers: theory Algebraic_Numbers.Real_Factorization


02:18:18 LLL_Basis_Reduction: theory Perron_Frobenius.HMA_Connect


02:18:28 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations


02:18:28 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2


02:19:08 LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int


02:19:08 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL


02:19:11 Algebraic_Numbers: theory Show.Show_Complex


02:19:12 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests


02:19:19 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_GSO_Impl


02:19:19 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds


02:19:26 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Integer_Equations


02:19:27 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_GSO_Impl_Complexity


02:19:31 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Mu_Integer_Impl


02:19:39 Timing Algebraic_Numbers_Lib (2 threads, 91.431s elapsed time, 161.976s cpu time, 7.984s GC time, factor 1.77)


02:19:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers_Lib


02:19:39 Finished Algebraic_Numbers_Lib (0:02:10 elapsed time, 0:03:35 cpu time, factor 1.65)


02:19:39 Building Linear_Recurrences ...


02:19:42 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common


02:19:42 Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials


02:19:42 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc


02:19:43 Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials


02:19:43 Linear_Recurrences: theory Linear_Recurrences.Factorizations


02:19:43 Linear_Recurrences: theory Linear_Recurrences.RatFPS


02:19:43 Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition


02:19:45 Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver


02:19:47 LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Mu_Integer_Impl_Complexity


02:19:47 Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences


02:19:48 Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences


02:19:49 Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Solver


02:20:32 Timing Linear_Recurrences (2 threads, 14.947s elapsed time, 29.260s cpu time, 1.916s GC time, factor 1.96)


02:20:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences


02:20:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences/document.pdf


02:20:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences/outline.pdf


02:20:32 Finished Linear_Recurrences (0:00:52 elapsed time, 0:01:24 cpu time, factor 1.60)


02:20:32 Running Linear_Recurrences_Test ...


02:20:36 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Common


02:20:36 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Eulerian_Polynomials


02:20:36 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Misc


02:20:37 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Pochhammer_Polynomials


02:20:37 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Factorizations


02:20:37 Linear_Recurrences_Test: theory Linear_Recurrences_Test.RatFPS


02:20:37 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Partial_Fraction_Decomposition


02:20:39 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Rational_FPS_Solver


02:20:39 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Show_RatFPS


02:20:40 Linear_Recurrences_Test: theory Show.Show_Complex


02:20:41 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Homogenous_Recurrences


02:20:41 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Pretty


02:20:42 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Inhomogenous_Recurrences


02:20:43 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Solver


02:20:48 Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Test


02:23:50 Timing Linear_Recurrences_Test (2 threads, 192.966s elapsed time, 355.540s cpu time, 42.884s GC time, factor 1.84)


02:23:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences_Test


02:23:50 Finished Linear_Recurrences_Test (0:03:17 elapsed time, 0:05:59 cpu time, factor 1.82)


02:23:59 Timing Algebraic_Numbers (2 threads, 380.345s elapsed time, 678.680s cpu time, 56.192s GC time, factor 1.78)


02:23:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers


02:23:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf


02:23:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf


02:23:59 Finished Algebraic_Numbers (0:06:30 elapsed time, 0:11:35 cpu time, factor 1.78)


02:25:47 Timing LLL_Basis_Reduction (2 threads, 426.808s elapsed time, 770.960s cpu time, 46.224s GC time, factor 1.81)


02:25:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction


02:25:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/document.pdf


02:25:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/outline.pdf


02:25:47 Finished LLL_Basis_Reduction (0:08:16 elapsed time, 0:14:33 cpu time, factor 1.76)


02:25:47 Running LLL_Factorization ...


02:25:52 LLL_Factorization: theory LLL_Factorization.Sub_Sums


02:25:52 LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly


02:25:52 LLL_Factorization: theory LLL_Factorization.Factor_Bound_2


02:25:53 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl


02:25:57 LLL_Factorization: theory LLL_Factorization.LLL_Factorization


02:26:06 LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22


02:26:09 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem


02:26:53 Timing LLL_Factorization (2 threads, 57.357s elapsed time, 106.468s cpu time, 5.472s GC time, factor 1.86)


02:26:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization


02:26:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/document.pdf


02:26:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/outline.pdf


02:26:53 Finished LLL_Factorization (0:01:05 elapsed time, 0:02:00 cpu time, factor 1.83)


02:26:53 

02:26:53 === TIMING ===


02:26:53 

02:26:53 Group AFP: 0:48:19 elapsed time, 1:23:23 cpu time, factor 1.73


02:26:53 Group main: 0:01:56 elapsed time, 0:03:24 cpu time, factor 1.76


02:26:53 Group timing: 0:01:56 elapsed time, 0:03:24 cpu time, factor 1.76


02:26:53 Overall: 0:30:14 elapsed time, 1:26:47 cpu time, factor 2.87


02:26:53 

02:26:53 === DEPENDENCIES ===


02:26:53 

02:26:53 Generating dependencies file ...


02:26:59 Writing dependencies file ...


02:26:59 

02:26:59 === SITEGEN ===


02:26:59 

02:26:59 Writing status file ...


02:26:59 Running sitegen ...


02:27:01 Success: Generated topics.html


02:27:02 Success: Generated index.html


02:27:02 Success: Generated html files for 423 entries


02:27:02 Success: Generated statistics.html


02:27:02 Success: Generated download.html


02:27:03 Success: Generated about.html


02:27:03 Success: Generated citing.html


02:27:03 Success: Generated updating.html


02:27:03 Success: Generated search.html


02:27:03 Success: Generated submitting.html


02:27:03 Success: Generated using.html


02:27:03 Success: Generated rss.xml


02:27:03 Success: Generated status.html


02:27:03 Packing tars ...


02:27:09 

02:27:09 === COMPLETED ===


02:27:09 

02:27:09 Archiving artifacts


02:29:48 Started calculate disk usage of build


02:29:48 Finished Calculation of disk usage of build in 0 seconds


02:30:17 Started calculate disk usage of workspace


02:30:18 Finished Calculation of disk usage of workspace in 0 seconds


02:30:18 No emails were triggered.


02:30:18 Finished: SUCCESS