17:13:14 Started by upstream project "isabelle-repo" build number 594

17:13:14 originally caused by:

17:13:14 Started by an SCM change

17:13:14 [EnvInject] - Loading node environment variables.

17:13:14 Building remotely on workermta2 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp

17:13:14 [isabelle-repo-afp] $ hg showconfig paths.default

17:13:14 [isabelle-repo-afp] $ hg pull --rev ae53f4d901a36c7a7eadb5ddebebd6ea11a968c1

17:13:15 pulling from http://isabelle.in.tum.de/repos/isabelle/

17:13:15 searching for changes

17:13:15 adding changesets

17:13:15 adding manifests

17:13:15 adding file changes

17:13:15 added 1 changesets with 5 changes to 5 files

17:13:15 (run 'hg update' to get a working copy)

17:13:15 [isabelle-repo-afp] $ hg update --clean --rev ae53f4d901a36c7a7eadb5ddebebd6ea11a968c1

17:13:15 5 files updated, 0 files merged, 0 files removed, 0 files unresolved

17:13:15 [isabelle-repo-afp] $ hg log --rev . --template {node}

17:13:15 [isabelle-repo-afp] $ hg log --rev . --template {rev}

17:13:15 [isabelle-repo-afp] $ hg id --branch

17:13:15 [afp] $ hg showconfig paths.default

17:13:15 [afp] $ hg pull --rev default

17:13:16 pulling from https://bitbucket.org/isa-afp/afp-devel/

17:13:16 searching for changes

17:13:16 adding changesets

17:13:16 adding manifests

17:13:16 adding file changes

17:13:16 added 5 changesets with 9 changes to 9 files

17:13:16 (run 'hg update' to get a working copy)

17:13:16 [afp] $ hg update --clean --rev default

17:13:17 324 files updated, 0 files merged, 4 files removed, 0 files unresolved

17:13:17 [afp] $ hg --config extensions.purge= clean --all

17:13:17 [afp] $ hg log --rev . --template {node}

17:13:17 [afp] $ hg log --rev . --template {rev}

17:13:17 No emails were triggered.

17:13:17 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson278113217018794653.sh

17:13:17 + Admin/jenkins/run_build afp

17:13:17 + set -e

17:13:17 + PROFILE=afp

17:13:17 + shift

17:13:17 + bin/isabelle components -a

17:13:17 + bin/isabelle jedit -bf

17:13:17 ### Building Isabelle/Scala ...

17:14:06 ### Building Isabelle/jEdit ...

17:14:24 + bin/isabelle ci_build_afp

17:14:30

17:14:30 === CONFIGURATION ===

17:14:30

17:14:30 ISABELLE_BUILD_OPTIONS=""

17:14:30

17:14:30 ML_PLATFORM="x86_64-linux"

17:14:30 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

17:14:30 ML_SYSTEM="polyml-5.6"

17:14:30 ML_OPTIONS="-H 4000 --maxheap 8G"

17:14:30

17:14:30 === BUILD ===

17:14:30

17:14:30 Build started at Sun, 30 Oct 2016 16:14:30 GMT

17:14:30 Isabelle id ae53f4d901a3

17:14:30 AFP id b82d07ae1088

17:14:30

17:14:30 === LOG ===

17:14:30

17:14:31 Session Pure/Pure

17:14:31 Session HOL/HOL (main)

17:14:32 Session AFP/AVL-Trees (AFP)

17:14:32 Session AFP/AWN (AFP)

17:14:32 Session AFP/Abortable_Linearizable_Modules (AFP)

17:14:32 Session AFP/Abstract-Hoare-Logics (AFP)

17:14:32 Session AFP/Abstract-Rewriting (AFP)

17:14:32 Session AFP/Decreasing-Diagrams (AFP)

17:14:32 Session AFP/Decreasing-Diagrams-II (AFP)

17:14:32 Session AFP/Matrix (AFP)

17:14:32 Session AFP/Matrix_Tensor (AFP)

17:14:32 Session AFP/Knot_Theory (AFP)

17:14:32 Session AFP/Polynomials (AFP)

17:14:32 Session AFP/Groebner_Bases (AFP)

17:14:32 Session AFP/Abstract_Completeness (AFP)

17:14:32 Session AFP/Allen_Calculus (AFP)

17:14:32 Session AFP/Automatic_Refinement (AFP)

17:14:32 Session AFP/Refine_Monadic (AFP)

17:14:33 Session AFP/Collections (AFP)

17:14:33 Session AFP/CAVA_Base (AFP)

17:14:33 Session AFP/CAVA_Automata (AFP)

17:14:33 Session AFP/DFS_Framework (AFP)

17:14:33 Session AFP/Gabow_SCC (AFP)

17:14:33 Session AFP/LTL_to_GBA (AFP)

17:14:33 Session AFP/CAVA_buildchain1 (AFP)

17:14:33 Session AFP/CAVA_buildchain3 (AFP)

17:14:33 Session AFP/CAVA_LTL_Modelchecker (AFP)

17:14:33 Session AFP/Promela (AFP)

17:14:33 Session AFP/Collections_Examples (AFP)

17:14:33 Session AFP/Dijkstra_Shortest_Path (AFP)

17:14:33 Session AFP/Formal_SSA (AFP)

17:14:33 Session AFP/Sepref_Prereq (AFP)

17:14:33 Session AFP/Refine_Imperative_HOL (AFP)

17:14:33 Session AFP/Sepref_Basic (AFP)

17:14:33 Session AFP/Sepref_IICF (AFP)

17:14:33 Session AFP/Edka_Base (AFP)

17:14:33 Session AFP/EdmondsKarp_Maxflow (AFP)

17:14:33 Session AFP/Transitive-Closure (AFP)

17:14:33 Session AFP/Tree-Automata (AFP)

17:14:33 Session AFP/BinarySearchTree (AFP)

17:14:33 Session AFP/Binomial-Queues (AFP)

17:14:33 Session AFP/Bondy (AFP)

17:14:33 Session AFP/Bounded_Deducibility_Security (AFP)

17:14:33 Session AFP/BytecodeLogicJmlTypes (AFP)

17:14:33 Session AFP/CISC-Kernel (AFP)

17:14:33 Session AFP/CYK (AFP)

17:14:33 Session AFP/Card_Number_Partitions (AFP)

17:14:33 Session AFP/Case_Labeling (AFP)

17:14:33 Session AFP/Cauchy (AFP)

17:14:33 Session AFP/Sqrt_Babylonian (AFP)

17:14:33 Session AFP/Real_Impl (AFP)

17:14:34 Session AFP/Certification_Monads (AFP)

17:14:34 Session AFP/ClockSynchInst (AFP)

17:14:34 Session AFP/Coinductive_Languages (AFP)

17:14:34 Session AFP/Compiling-Exceptions-Correctly (AFP)

17:14:34 Session AFP/Completeness (AFP)

17:14:34 Session AFP/ComponentDependencies (AFP)

17:14:34 Session AFP/Consensus_Refined (AFP)

17:14:34 Session AFP/CryptoBasedCompositionalProperties (AFP)

17:14:34 Session AFP/DPT-SAT-Solver (AFP)

17:14:34 Session AFP/DataRefinementIBP (AFP)

17:14:34 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

17:14:34 Session AFP/Dependent_SIFUM_Refinement (AFP)

17:14:34 Session AFP/Depth-First-Search (AFP)

17:14:34 Session AFP/Derangements (AFP)

17:14:34 Session AFP/Discrete_Summation (AFP)

17:14:34 Session AFP/Card_Partitions (AFP)

17:14:34 Session AFP/DiskPaxos (AFP)

17:14:34 Session AFP/Encodability_Process_Calculi (AFP)

17:14:34 Session AFP/Euler_Partition (AFP)

17:14:34 Session AFP/Example-Submission (AFP)

17:14:34 Session AFP/FFT (AFP)

17:14:34 Session AFP/FLP (AFP)

17:14:34 Session AFP/FeatherweightJava (AFP)

17:14:34 Session AFP/Featherweight_OCL (AFP)

17:14:34 Session AFP/FileRefinement (AFP)

17:14:34 Session AFP/FinFun (AFP)

17:14:34 Session AFP/Finite_Automata_HF (AFP)

17:14:34 Session AFP/FocusStreamsCaseStudies (AFP)

17:14:34 Session AFP/Free-Groups (AFP)

17:14:35 Session AFP/FunWithFunctions (AFP)

17:14:35 Session AFP/FunWithTilings (AFP)

17:14:35 Session AFP/GPU_Kernel_PL (AFP)

17:14:35 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

17:14:35 Session AFP/GenClock (AFP)

17:14:35 Session AFP/General-Triangle (AFP)

17:14:35 Session AFP/GoedelGod (AFP)

17:14:35 Session AFP/GraphMarkingIBP (AFP)

17:14:35 Session AFP/Graph_Theory (AFP)

17:14:35 Session AFP/ShortestPath (AFP)

17:14:35 Session HOL/HOL-Algebra (main timing)

17:14:35 Session AFP/JNF-HOL-Lib (AFP)

17:14:35 Session AFP/JNF-AFP-Lib (AFP)

17:14:35 Session AFP/Jordan_Normal_Form (AFP)

17:14:35 Session AFP/Pre_Perron_Frobenius (AFP)

17:14:36 Session AFP/Perron_Frobenius (AFP)

17:14:36 Session AFP/Pre_Polynomial_Factorization (AFP)

17:14:36 Session AFP/Polynomial_Factorization (AFP)

17:14:36 Session AFP/Pre_Algebraic_Numbers (AFP)

17:14:36 Session AFP/Algebraic_Numbers (AFP)

17:14:36 Session AFP/Algebraic_Numbers_Lib (AFP)

17:14:36 Session AFP/Pre_BZ (AFP)

17:14:36 Session AFP/Berlekamp_Zassenhaus (AFP)

17:14:36 Session AFP/Jordan_Hoelder (AFP)

17:14:36 Session AFP/Perfect-Number-Thm (AFP)

17:14:36 Session AFP/Secondary_Sylow (AFP)

17:14:36 Session AFP/VectorSpace (AFP)

17:14:36 Session HOL/HOL-Analysis (main timing)

17:14:36 Session AFP/Affine_Arithmetic (AFP)

17:14:36 Session AFP/Cartan_FP (AFP)

17:14:36 Session AFP/Cayley_Hamilton (AFP)

17:14:36 Session AFP/Chord_Segments (AFP)

17:14:36 Session AFP/Echelon_Form (AFP)

17:14:36 Session AFP/Hermite (AFP)

17:14:36 Session AFP/Gauss_Jordan (AFP)

17:14:37 Session HOL/HOL-Probability (timing)

17:14:37 Session AFP/Applicative_Lifting (AFP)

17:14:37 Session AFP/Stern_Brocot (AFP)

17:14:37 Session AFP/Density_Compiler (AFP)

17:14:37 Session AFP/Ergodic_Theory (AFP)

17:14:37 Session AFP/Fisher_Yates (AFP)

17:14:37 Session AFP/Girth_Chromatic (AFP)

17:14:37 Session AFP/List_Update (AFP)

17:14:37 Session AFP/Lp (AFP)

17:14:37 Session AFP/MFMC_Countable (AFP)

17:14:37 Session AFP/Markov_Models (AFP)

17:14:37 Session AFP/Probabilistic_Noninterference (AFP)

17:14:37 Session AFP/Probabilistic_System_Zoo (AFP)

17:14:37 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

17:14:37 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

17:14:38 Session AFP/Randomised_Social_Choice (AFP)

17:14:38 Session AFP/SDS_Impossibility (AFP)

17:14:38 Session AFP/Source_Coding_Theorem (AFP)

17:14:38 Session AFP/UpDown_Scheme (AFP)

17:14:38 Session AFP/Landau_Analysis (AFP)

17:14:38 Session AFP/Akra_Bazzi (AFP)

17:14:38 Session AFP/Catalan_Numbers (AFP)

17:14:38 Session AFP/Stirling_Formula (AFP)

17:14:38 Session AFP/Lower_Semicontinuous (AFP)

17:14:38 Session AFP/Ordinary_Differential_Equations (AFP)

17:14:38 Session AFP/HOL-ODE (AFP)

17:14:38 Session AFP/HOL-ODE-Refinement (AFP)

17:14:38 Session AFP/HOL-ODE-Numerics (AFP)

17:14:38 Session AFP/HOL-ODE-Examples (AFP)

17:14:38 Session AFP/Prime_Harmonic_Series (AFP)

17:14:39 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

17:14:39 Session AFP/Ptolemys_Theorem (AFP)

17:14:39 Session AFP/QR_Decomposition (AFP)

17:14:39 Session AFP/Rank_Nullity_Theorem (AFP)

17:14:39 Session AFP/Tarskis_Geometry (AFP)

17:14:39 Session AFP/Triangle (AFP)

17:14:39 Session AFP/pGCL (AFP)

17:14:39 Session HOL/HOL-Cardinals (timing)

17:14:39 Session AFP/Ordinals_and_Cardinals (AFP)

17:14:39 Session AFP/Sort_Encodings (AFP)

17:14:39 Session HOL/HOL-Imperative_HOL

17:14:39 Session AFP/Imperative_Insertion_Sort (AFP)

17:14:39 Session HOL/HOL-Library (main timing)

17:14:39 Session AFP/Amortized_Complexity (AFP)

17:14:39 Session AFP/Dynamic_Tables (AFP)

17:14:39 Session AFP/ArrowImpossibilityGS (AFP)

17:14:39 Session AFP/Bell_Numbers_Spivey (AFP)

17:14:39 Session AFP/Card_Equiv_Relations (AFP)

17:14:39 Session AFP/Binomial-Heaps (AFP)

17:14:39 Session AFP/Boolean_Expression_Checkers (AFP)

17:14:39 Session AFP/Buildings (AFP)

17:14:39 Session AFP/Card_Multisets (AFP)

17:14:39 Session AFP/Category (AFP)

17:14:39 Session AFP/Category2 (AFP)

17:14:39 Session AFP/Category3 (AFP)

17:14:40 Session AFP/CofGroups (AFP)

17:14:40 Session AFP/Coinductive (AFP)

17:14:40 Session AFP/Lazy-Lists-II (AFP)

17:14:40 Session AFP/Topology (AFP)

17:14:40 Session AFP/Parity_Game (AFP)

17:14:40 Session AFP/Stream_Fusion_Code (AFP)

17:14:40 Session AFP/ConcurrentIMP (AFP)

17:14:40 Session AFP/CoreC++ (AFP)

17:14:40 Session AFP/Datatype_Order_Generator (AFP)

17:14:40 Session AFP/Old_Datatype_Show (AFP)

17:14:40 Session AFP/Deriving (AFP)

17:14:40 Session AFP/Containers (AFP)

17:14:40 Session AFP/Containers-Benchmarks (AFP)

17:14:40 Session AFP/Show (AFP)

17:14:40 Session AFP/Descartes_Sign_Rule (AFP)

17:14:40 Session AFP/Efficient-Mergesort (AFP)

17:14:40 Session AFP/FOL-Fitting (AFP)

17:14:40 Session AFP/Finger-Trees (AFP)

17:14:40 Session AFP/Formula_Derivatives (AFP)

17:14:40 Session AFP/Formula_Derivatives-Examples (AFP)

17:14:40 Session AFP/Free-Boolean-Algebra (AFP)

17:14:40 Session AFP/Functional-Automata (AFP)

17:14:40 Session AFP/Group-Ring-Module (AFP)

17:14:40 Session AFP/Valuation (AFP)

17:14:40 Session AFP/Isabelle_Meta_Model (AFP)

17:14:40 Session AFP/KBPs (AFP)

17:14:40 Session AFP/LTL (AFP)

17:14:40 Session AFP/LTL_to_DRA (AFP)

17:14:40 Session AFP/Stuttering_Equivalence (AFP)

17:14:40 Session AFP/Landau_Symbols (AFP)

17:14:40 Session AFP/LinearQuantifierElim (AFP)

17:14:40 Session AFP/List-Infinite (AFP)

17:14:40 Session AFP/Nat-Interval-Logic (AFP)

17:14:40 Session AFP/AutoFocus-Stream (AFP)

17:14:40 Session AFP/MSO_Regex_Equivalence (AFP)

17:14:40 Session AFP/MSO_Examples (AFP)

17:14:40 Session AFP/MuchAdoAboutTwo (AFP)

17:14:40 Session AFP/Myhill-Nerode (AFP)

17:14:40 Session AFP/POPLmark-deBruijn (AFP)

17:14:40 Session AFP/Pairing_Heap (AFP)

17:14:40 Session AFP/Presburger-Automata (AFP)

17:14:40 Session AFP/Program-Conflict-Analysis (AFP)

17:14:40 Session AFP/Regex_Equivalence (AFP)

17:14:40 Session AFP/Regex_Equivalence_Examples (AFP)

17:14:40 Session AFP/Regular-Sets (AFP)

17:14:40 Session AFP/Posix-Lexing (AFP)

17:14:40 Session AFP/Ribbon_Proofs (AFP)

17:14:40 Session AFP/SATSolverVerification (AFP)

17:14:41 Session AFP/Selection_Heap_Sort (AFP)

17:14:41 Session AFP/Separation_Logic_Imperative_HOL (AFP)

17:14:41 Session AFP/Sturm_Sequences (AFP)

17:14:41 Session AFP/Special_Function_Bounds (AFP)

17:14:41 Session AFP/SuperCalc (AFP)

17:14:41 Session AFP/Tail_Recursive_Functions (AFP)

17:14:41 Session AFP/Vickrey_Clarke_Groves (AFP)

17:14:41 Session AFP/Well_Quasi_Orders (AFP)

17:14:41 Session HOL/HOL-Nominal

17:14:41 Session AFP/CCS (AFP)

17:14:41 Session AFP/Lam-ml-Normalization (AFP)

17:14:41 Session AFP/Pi_Calculus (AFP)

17:14:41 Session AFP/Psi_Calculi (AFP)

17:14:41 Session AFP/SequentInvertibility (AFP)

17:14:41 Session HOL/HOL-Number_Theory (timing)

17:14:41 Session AFP/Fermat3_4 (AFP)

17:14:41 Session AFP/Lehmer (AFP)

17:14:41 Session AFP/Pratt_Certificate (AFP)

17:14:41 Session AFP/SumSquares (AFP)

17:14:41 Session HOL/HOL-Word (main timing)

17:14:42 Session HOL/HOL-SPARK (main)

17:14:42 Session HOL/HOL-SPARK-Examples

17:14:42 Session AFP/RIPEMD-160-SPARK (AFP)

17:14:42 Session AFP/Kleene_Algebra (AFP)

17:14:42 Session AFP/KAT_and_DRA (AFP)

17:14:42 Session AFP/Algebraic_VCs (AFP)

17:14:42 Session AFP/Multirelations (AFP)

17:14:42 Session AFP/Regular_Algebras (AFP)

17:14:42 Session AFP/Relation_Algebra (AFP)

17:14:42 Session AFP/Residuated_Lattices (AFP)

17:14:42 Session AFP/Native_Word (AFP)

17:14:42 Session AFP/SPARCv8 (AFP)

17:14:42 Session AFP/Separation_Algebra (AFP)

17:14:42 Session AFP/Word_Lib (AFP)

17:14:42 Session AFP/IP_Addresses (AFP)

17:14:42 Session AFP/Simple_Firewall (AFP)

17:14:42 Session AFP/Routing (AFP)

17:14:42 Session AFP/Iptables_Semantics (AFP)

17:14:42 Session HOL/HOLCF (main timing)

17:14:42 Session AFP/Circus (AFP)

17:14:42 Session AFP/HOLCF-HOL-Library (AFP)

17:14:42 Session AFP/HOLCF-Nominal2 (AFP)

17:14:42 Session AFP/Launchbury (AFP)

17:14:43 Session AFP/Call_Arity (AFP)

17:14:43 Session AFP/PCF (AFP)

17:14:43 Session AFP/Shivers-CFA (AFP)

17:14:43 Session AFP/Stream-Fusion (AFP)

17:14:43 Session AFP/Tycon (AFP)

17:14:43 Session AFP/WorkerWrapper (AFP)

17:14:43 Session AFP/Heard_Of (AFP)

17:14:43 Session AFP/HereditarilyFinite (AFP)

17:14:43 Session AFP/HotelKeyCards (AFP)

17:14:43 Session AFP/Huffman (AFP)

17:14:43 Session AFP/HyperCTL (AFP)

17:14:43 Session AFP/IEEE_Floating_Point (AFP)

17:14:43 Session AFP/Impossible_Geometry (AFP)

17:14:43 Session AFP/Incompleteness (AFP)

17:14:43 Session AFP/Surprise_Paradox (AFP)

17:14:43 Session AFP/Incredible_Proof_Machine (AFP)

17:14:43 Session AFP/Inductive_Confidentiality (AFP)

17:14:43 Session AFP/InfPathElimination (AFP)

17:14:43 Session AFP/Integration (AFP)

17:14:43 Session AFP/Jinja (AFP)

17:14:43 Session AFP/HRB-Slicing (AFP)

17:14:43 Session AFP/InformationFlowSlicing_Inter (AFP)

17:14:43 Session AFP/Slicing (AFP)

17:14:43 Session AFP/InformationFlowSlicing (AFP)

17:14:43 Session AFP/JiveDataStoreModel (AFP)

17:14:43 Session AFP/KAD (AFP)

17:14:43 Session AFP/Koenigsberg_Friendship_Base (AFP)

17:14:43 Session AFP/Koenigsberg_Friendship (AFP)

17:14:43 Session AFP/Lambda_Free_RPOs (AFP)

17:14:44 Session AFP/LatticeProperties (AFP)

17:14:44 Session AFP/MonoBoolTranAlgebra (AFP)

17:14:44 Session AFP/PseudoHoops (AFP)

17:14:44 Session AFP/Lifting_Definition_Option (AFP)

17:14:44 Session AFP/LightweightJava (AFP)

17:14:44 Session AFP/Liouville_Numbers (AFP)

17:14:44 Session AFP/List-Index (AFP)

17:14:44 Session AFP/List_Interleaving (AFP)

17:14:44 Session AFP/Locally-Nameless-Sigma (AFP)

17:14:44 Session AFP/Marriage (AFP)

17:14:44 Session AFP/Latin_Square (AFP)

17:14:44 Session AFP/Max-Card-Matching (AFP)

17:14:44 Session AFP/MiniML (AFP)

17:14:44 Session AFP/Network_Security_Policy_Verification (AFP)

17:14:44 Session AFP/No_FTL_observers (AFP)

17:14:44 Session AFP/Nominal2 (AFP)

17:14:44 Session AFP/Rewriting_Z (AFP)

17:14:44 Session AFP/Noninterference_CSP (AFP)

17:14:45 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

17:14:45 Session AFP/Noninterference_Generic_Unwinding (AFP)

17:14:45 Session AFP/Noninterference_Inductive_Unwinding (AFP)

17:14:45 Session AFP/Noninterference_Sequential_Composition (AFP)

17:14:45 Session AFP/Noninterference_Concurrent_Composition (AFP)

17:14:45 Session AFP/NormByEval (AFP)

17:14:45 Session AFP/Open_Induction (AFP)

17:14:45 Session AFP/Ordinal (AFP)

17:14:45 Session AFP/Partial_Function_MR (AFP)

17:14:45 Session AFP/Polynomial_Interpolation (AFP)

17:14:45 Session AFP/Pop_Refinement (AFP)

17:14:45 Session AFP/Possibilistic_Noninterference (AFP)

17:14:45 Session AFP/Priority_Queue_Braun (AFP)

17:14:45 Session AFP/PropResPI (AFP)

17:14:45 Session AFP/ROBDD (AFP)

17:14:45 Session AFP/RSAPSS (AFP)

17:14:46 Session AFP/Ramsey-Infinite (AFP)

17:14:46 Session AFP/Recursion-Theory-I (AFP)

17:14:46 Session AFP/RefinementReactive (AFP)

17:14:46 Session AFP/Rep_Fin_Groups (AFP)

17:14:46 Session AFP/Resolution_FOL (AFP)

17:14:46 Session AFP/Robbins-Conjecture (AFP)

17:14:46 Session AFP/Roy_Floyd_Warshall (AFP)

17:14:46 Session AFP/SIFPL (AFP)

17:14:46 Session AFP/SIFUM_Type_Systems (AFP)

17:14:46 Session AFP/SenSocialChoice (AFP)

17:14:46 Session AFP/Simpl (AFP)

17:14:46 Session AFP/BDD (AFP)

17:14:46 Session AFP/Planarity_Certificates (AFP)

17:14:46 Session AFP/Skew_Heap (AFP)

17:14:46 Session AFP/Splay_Tree (AFP)

17:14:47 Session AFP/Statecharts (AFP)

17:14:47 Session AFP/Stone_Algebras (AFP)

17:14:47 Session AFP/Strong_Security (AFP)

17:14:47 Session AFP/Sturm_Tarski (AFP)

17:14:47 Session AFP/TLA (AFP)

17:14:47 Session AFP/Timed_Automata (AFP)

17:14:47 Session AFP/TortoiseHare (AFP)

17:14:47 Session AFP/Transitive-Closure-II (AFP)

17:14:47 Session AFP/Tree_Decomposition (AFP)

17:14:47 Session AFP/Trie (AFP)

17:14:47 Session AFP/UPF (AFP)

17:14:47 Session AFP/Verified-Prover (AFP)

17:14:47 Session AFP/VolpanoSmith (AFP)

17:14:47 Session AFP/WHATandWHERE_Security (AFP)

17:14:47 Session AFP/XML (AFP)

17:14:49 Building HOL-Library ...

17:14:50 Building Pre_Perron_Frobenius ...

17:14:51 Building Pre_Polynomial_Factorization ...

17:14:51 Running Polynomial_Interpolation ...

17:14:52 Polynomial_Interpolation: theory Adhoc_Overloading

17:14:52 Polynomial_Interpolation: theory Infinite_Set

17:14:52 Polynomial_Interpolation: theory Monad_Syntax

17:14:52 HOL-Library: theory Adhoc_Overloading

17:14:52 HOL-Library: theory Lattice_Syntax

17:14:52 HOL-Library: theory AList

17:14:52 Polynomial_Interpolation: theory More_List

17:14:52 HOL-Library: theory BNF_Axiomatization

17:14:53 Polynomial_Interpolation: theory Sqrt_Babylonian_Auxiliary

17:14:53 HOL-Library: theory BNF_Corec

17:14:53 Polynomial_Interpolation: theory Polynomial

17:14:54 HOL-Library: theory DAList

17:14:55 Pre_Polynomial_Factorization: theory Divmod_Int

17:14:55 Pre_Polynomial_Factorization: theory Partial_Function_MR

17:14:55 Pre_Polynomial_Factorization: theory RBT

17:14:55 Pre_Polynomial_Factorization: theory Improved_Code_Equations

17:14:56 HOL-Library: theory Stirling

17:14:56 Pre_Polynomial_Factorization: theory Neville_Aitken_Interpolation

17:14:56 Pre_Polynomial_Factorization: theory RBT_Mapping

17:14:56 HOL-Library: theory Bit

17:14:56 Pre_Polynomial_Factorization: theory Show_Poly

17:14:57 HOL-Library: theory Bits

17:14:57 Pre_Polynomial_Factorization: theory CauchysMeanTheorem

17:14:57 HOL-Library: theory Bits_Bit

17:14:57 Pre_Polynomial_Factorization: theory Lagrange_Interpolation

17:14:57 Pre_Polynomial_Factorization: theory Sqrt_Babylonian_Auxiliary

17:14:57 HOL-Library: theory Boolean_Algebra

17:14:57 Pre_Polynomial_Factorization: theory Ring_Hom_Poly

17:14:58 Pre_Perron_Frobenius: theory Eisbach

17:14:58 Pre_Perron_Frobenius: theory Bit

17:14:58 HOL-Library: theory Cardinal_Notations

17:14:58 HOL-Library: theory Char_ord

17:14:58 Pre_Polynomial_Factorization: theory Is_Rat_To_Rat

17:14:58 HOL-Library: theory Code_Abstract_Nat

17:14:58 HOL-Library: theory Code_Binary_Nat

17:14:58 Pre_Perron_Frobenius: theory Dual_Order

17:14:58 HOL-Library: theory Code_Target_Nat

17:14:58 Pre_Perron_Frobenius: theory Nat_Bijection

17:14:58 Pre_Perron_Frobenius: theory Old_Datatype

17:14:58 HOL-Library: theory Code_Char

17:14:59 HOL-Library: theory Code_Prolog

17:14:59 Pre_Perron_Frobenius: theory Code_Set

17:14:59 Pre_Perron_Frobenius: theory Numeral_Type

17:14:59 Pre_Polynomial_Factorization: theory NthRoot_Impl

17:14:59 HOL-Library: theory Code_Test

17:15:00 HOL-Library: theory Combine_PER

17:15:00 HOL-Library: theory Complete_Partial_Order2

17:15:00 Pre_Polynomial_Factorization: theory Newton_Interpolation

17:15:00 Pre_Perron_Frobenius: theory Countable

17:15:00 Pre_Perron_Frobenius: theory Product_Plus

17:15:00 Pre_Polynomial_Factorization: theory Sqrt_Babylonian

17:15:00 HOL-Library: theory Debug

17:15:00 HOL-Library: theory Discrete

17:15:00 Pre_Perron_Frobenius: theory Product_Order

17:15:01 HOL-Library: theory Disjoint_Sets

17:15:01 Pre_Perron_Frobenius: theory Set_Algebras

17:15:01 HOL-Library: theory Dlist

17:15:01 Pre_Perron_Frobenius: theory L2_Norm

17:15:01 Pre_Perron_Frobenius: theory Indicator_Function

17:15:02 Pre_Perron_Frobenius: theory Countable_Set

17:15:02 Pre_Perron_Frobenius: theory Inner_Product

17:15:02 Pre_Perron_Frobenius: theory Countable_Complete_Lattices

17:15:02 HOL-Library: theory FSet

17:15:03 Pre_Perron_Frobenius: theory Continuum_Not_Denumerable

17:15:03 Polynomial_Interpolation: theory Divmod_Int

17:15:03 Polynomial_Interpolation: theory Fraction_Field

17:15:03 Polynomial_Interpolation: theory Multiset

17:15:03 Pre_Polynomial_Factorization: theory Polynomial_Interpolation

17:15:04 HOL-Library: theory Fraction_Field

17:15:04 Pre_Perron_Frobenius: theory Product_Vector

17:15:04 Pre_Perron_Frobenius: theory Euclidean_Space

17:15:05 Polynomial_Interpolation: theory Improved_Code_Equations

17:15:05 Pre_Perron_Frobenius: theory Liminf_Limsup

17:15:05 Polynomial_Interpolation: theory Neville_Aitken_Interpolation

17:15:05 HOL-Library: theory Fun_Lexorder

17:15:05 HOL-Library: theory FuncSet

17:15:05 HOL-Library: theory Finite_Map

17:15:06 HOL-Library: theory Function_Algebras

17:15:06 Pre_Perron_Frobenius: theory Nonpos_Ints

17:15:06 Pre_Perron_Frobenius: theory Finite_Cartesian_Product

17:15:06 HOL-Library: theory Function_Division

17:15:06 Polynomial_Interpolation: theory Missing_Unsorted

17:15:06 Pre_Perron_Frobenius: theory Linear_Algebra

17:15:06 HOL-Library: theory Code_Target_Int

17:15:06 HOL-Library: theory Code_Target_Numeral

17:15:06 HOL-Library: theory Groups_Big_Fun

17:15:07 Pre_Perron_Frobenius: theory Operator_Norm

17:15:07 HOL-Library: theory IArray

17:15:07 Pre_Perron_Frobenius: theory Order_Continuity

17:15:07 HOL-Library: theory Infinite_Set

17:15:08 HOL-Library: theory Omega_Words_Fun

17:15:08 Polynomial_Interpolation: theory Is_Rat_To_Rat

17:15:08 HOL-Library: theory LaTeXsugar

17:15:08 Polynomial_Interpolation: theory Factorial_Ring

17:15:08 HOL-Library: theory Lattice_Constructions

17:15:08 Pre_Perron_Frobenius: theory Extended_Nat

17:15:08 HOL-Library: theory ListVector

17:15:09 HOL-Library: theory List_lexord

17:15:09 HOL-Library: theory Mapping

17:15:09 Pre_Perron_Frobenius: theory Extended_Real

17:15:09 Pre_Perron_Frobenius: theory Periodic_Fun

17:15:09 Polynomial_Interpolation: theory Ring_Hom

17:15:10 Pre_Perron_Frobenius: theory Poly_Roots

17:15:10 Pre_Perron_Frobenius: theory Polynomial_Divisibility

17:15:10 Pre_Perron_Frobenius: theory Sum_of_Squares

17:15:10 HOL-Library: theory AList_Mapping

17:15:11 HOL-Library: theory Misc_Numeric

17:15:11 HOL-Library: theory Bit_Representation

17:15:11 HOL-Library: theory Misc_Typedef

17:15:11 HOL-Library: theory Bits_Int

17:15:11 HOL-Library: theory Monad_Syntax

17:15:11 HOL-Library: theory More_List

17:15:12 HOL-Library: theory Multiset

17:15:13 Pre_Perron_Frobenius: theory Norm_Arith

17:15:13 HOL-Library: theory Nat_Bijection

17:15:13 Pre_Perron_Frobenius: theory Topology_Euclidean_Space

17:15:13 Pre_Perron_Frobenius: theory Extended_Nonnegative_Real

17:15:13 HOL-Library: theory Stream

17:15:16 Polynomial_Interpolation: theory Euclidean_Algorithm

17:15:16 Pre_Perron_Frobenius: theory Sigma_Algebra

17:15:17 HOL-Library: theory Old_Datatype

17:15:18 HOL-Library: theory Countable

17:15:19 HOL-Library: theory DAList_Multiset

17:15:19 Pre_Perron_Frobenius: theory Measurable

17:15:20 HOL-Library: theory Factorial_Ring

17:15:20 HOL-Library: theory Multiset_Order

17:15:20 HOL-Library: theory Permutation

17:15:20 Pre_Perron_Frobenius: theory Measure_Space

17:15:21 HOL-Library: theory Permutations

17:15:22 HOL-Library: theory Countable_Set

17:15:22 HOL-Library: theory Countable_Complete_Lattices

17:15:23 Pre_Perron_Frobenius: theory Bounded_Linear_Function

17:15:23 Pre_Perron_Frobenius: theory Caratheodory

17:15:24 Pre_Perron_Frobenius: theory Convex_Euclidean_Space

17:15:25 Polynomial_Interpolation: theory Normalized_Fraction

17:15:25 Pre_Perron_Frobenius: theory Extended_Real_Limits

17:15:25 Polynomial_Interpolation: theory Polynomial_Factorial

17:15:25 HOL-Library: theory Countable_Set_Type

17:15:26 Pre_Perron_Frobenius: theory Tagged_Division

17:15:27 HOL-Library: theory Old_Recdef

17:15:27 Pre_Perron_Frobenius: theory Summation_Tests

17:15:28 HOL-Library: theory Euclidean_Algorithm

17:15:28 HOL-Library: theory Option_ord

17:15:28 Pre_Perron_Frobenius: theory Uniform_Limit

17:15:28 HOL-Library: theory Parallel

17:15:29 Polynomial_Interpolation: theory Missing_Polynomial

17:15:29 HOL-Library: theory Perm

17:15:29 Pre_Perron_Frobenius: theory Types_To_Sets

17:15:29 Pre_Perron_Frobenius: theory Square_Free_Factorization

17:15:30 Polynomial_Interpolation: theory Lagrange_Interpolation

17:15:30 Polynomial_Interpolation: theory Ring_Hom_Poly

17:15:30 Pre_Perron_Frobenius: theory Continuous_Extension

17:15:30 HOL-Library: theory Phantom_Type

17:15:31 Pre_Perron_Frobenius: theory Path_Connected

17:15:31 Polynomial_Interpolation: theory Newton_Interpolation

17:15:31 HOL-Library: theory Cardinality

17:15:32 HOL-Library: theory FinFun

17:15:35 Polynomial_Interpolation: theory Polynomial_Interpolation

17:15:35 HOL-Library: theory Numeral_Type

17:15:35 Pre_Perron_Frobenius: theory Homeomorphism

17:15:36 Pre_Perron_Frobenius: theory Brouwer_Fixpoint

17:15:36 HOL-Library: theory Type_Length

17:15:36 HOL-Library: theory Saturated

17:15:36 HOL-Library: theory Predicate_Compile_Alternative_Defs

17:15:36 HOL-Library: theory Normalized_Fraction

17:15:37 HOL-Library: theory Predicate_Compile_Quickcheck

17:15:37 HOL-Library: theory Product_Lexorder

17:15:37 HOL-Library: theory Product_Plus

17:15:37 HOL-Library: theory Quotient_Syntax

17:15:37 HOL-Library: theory Quotient_Option

17:15:37 HOL-Library: theory Product_Order

17:15:38 HOL-Library: theory Quotient_Product

17:15:38 Pre_Perron_Frobenius: theory Derivative

17:15:38 HOL-Library: theory Quotient_Set

17:15:38 HOL-Library: theory Finite_Lattice

17:15:38 HOL-Library: theory Quotient_List

17:15:38 HOL-Library: theory Quotient_Sum

17:15:38 HOL-Library: theory Quotient_Type

17:15:39 HOL-Library: theory RBT_Impl

17:15:40 Pre_Perron_Frobenius: theory Cartesian_Euclidean_Space

17:15:40 Pre_Perron_Frobenius: theory Weierstrass_Theorems

17:15:41 HOL-Library: theory Ramsey

17:15:41 HOL-Library: theory Reflection

17:15:41 HOL-Library: theory Refute

17:15:42 HOL-Library: theory Rewrite

17:15:42 HOL-Library: theory Set_Algebras

17:15:43 HOL-Library: theory Simps_Case_Conv

17:15:43 Pre_Perron_Frobenius: theory Determinants

17:15:43 Pre_Perron_Frobenius: theory Fashoda_Theorem

17:15:43 HOL-Library: theory Extended

17:15:43 Pre_Perron_Frobenius: theory Mod_Type

17:15:44 Pre_Perron_Frobenius: theory Generalizations

17:15:45 HOL-Library: theory State_Monad

17:15:45 HOL-Library: theory Sublist

17:15:46 Pre_Perron_Frobenius: theory Square_Matrix

17:15:46 HOL-Library: theory Prefix_Order

17:15:46 HOL-Library: theory Sublist_Order

17:15:46 Pre_Perron_Frobenius: theory Miscellaneous

17:15:46 HOL-Library: theory Polynomial

17:15:47 Pre_Perron_Frobenius: theory Cayley_Hamilton

17:15:48 Pre_Perron_Frobenius: theory Code_Matrix

17:15:48 Pre_Perron_Frobenius: theory Fundamental_Subspaces

17:15:48 Pre_Perron_Frobenius: theory Rref

17:15:48 Pre_Perron_Frobenius: theory Dim_Formula

17:15:49 Pre_Perron_Frobenius: theory Elementary_Operations

17:15:49 Pre_Perron_Frobenius: theory Rank

17:15:49 Pre_Perron_Frobenius: theory Ordered_Euclidean_Space

17:15:49 Pre_Perron_Frobenius: theory Gauss_Jordan

17:15:51 HOL-Library: theory BigO

17:15:51 Pre_Perron_Frobenius: theory Linear_Maps

17:15:52 HOL-Library: theory Bool_List_Representation

17:15:53 Pre_Perron_Frobenius: theory Gauss_Jordan_PA

17:15:54 Pre_Perron_Frobenius: theory Determinants2

17:15:54 HOL-Library: theory Code_Real_Approx_By_Float

17:15:54 Timing Pre_Polynomial_Factorization (2 threads, 28.366s elapsed time, 54.908s cpu time, 2.600s GC time, factor 1.94)

17:15:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization

17:15:54 Finished Pre_Polynomial_Factorization (0:01:02 elapsed time, 0:01:46 cpu time, factor 1.69)

17:15:54 Building Polynomial_Factorization ...

17:15:54 HOL-Library: theory Diagonal_Subsequence

17:15:54 Pre_Perron_Frobenius: theory Polytope

17:15:54 HOL-Library: theory Formal_Power_Series

17:15:55 Pre_Perron_Frobenius: theory Borel_Space

17:15:56 Timing Polynomial_Interpolation (2 threads, 58.231s elapsed time, 114.284s cpu time, 5.852s GC time, factor 1.96)

17:15:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Interpolation

17:15:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Interpolation/document.pdf

17:15:56 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Interpolation/outline.pdf

17:15:56 Finished Polynomial_Interpolation (0:01:05 elapsed time, 0:02:03 cpu time, factor 1.90)

17:15:58 Pre_Perron_Frobenius: theory Nonnegative_Lebesgue_Integration

17:15:58 Pre_Perron_Frobenius: theory Regularity

17:15:59 Polynomial_Factorization: theory Missing_Multiset

17:15:59 Polynomial_Factorization: theory Precomputation

17:15:59 HOL-Library: theory Polynomial_FPS

17:15:59 Polynomial_Factorization: theory Order_Polynomial

17:15:59 Polynomial_Factorization: theory Missing_List

17:16:00 HOL-Library: theory Fundamental_Theorem_Algebra

17:16:00 Pre_Perron_Frobenius: theory Binary_Product_Measure

17:16:00 HOL-Library: theory Indicator_Function

17:16:01 HOL-Library: theory Lattice_Algebras

17:16:01 Pre_Perron_Frobenius: theory Embed_Measure

17:16:01 Pre_Perron_Frobenius: theory Finite_Product_Measure

17:16:01 Polynomial_Factorization: theory Explicit_Roots

17:16:01 Polynomial_Factorization: theory Dvd_Int_Poly

17:16:03 Pre_Perron_Frobenius: theory Bochner_Integration

17:16:03 Pre_Perron_Frobenius: theory Function_Topology

17:16:04 Polynomial_Factorization: theory Prime_Factorization

17:16:04 Polynomial_Factorization: theory Gauss_Lemma

17:16:05 Pre_Perron_Frobenius: theory Complete_Measure

17:16:05 Pre_Perron_Frobenius: theory Radon_Nikodym

17:16:05 Polynomial_Factorization: theory Rational_Root_Test

17:16:06 Pre_Perron_Frobenius: theory Set_Integral

17:16:06 Pre_Perron_Frobenius: theory Lebesgue_Measure

17:16:07 HOL-Library: theory Liminf_Limsup

17:16:07 HOL-Library: theory Log_Nat

17:16:08 HOL-Library: theory Float

17:16:08 Pre_Perron_Frobenius: theory Henstock_Kurzweil_Integration

17:16:10 HOL-Library: theory Lub_Glb

17:16:11 HOL-Library: theory Multiset_Permutations

17:16:12 Pre_Perron_Frobenius: theory Bounded_Continuous_Function

17:16:12 Pre_Perron_Frobenius: theory Equivalence_Lebesgue_Henstock_Integration

17:16:12 HOL-Library: theory Nonpos_Ints

17:16:12 Pre_Perron_Frobenius: theory Integral_Test

17:16:13 HOL-Library: theory OptionalSugar

17:16:13 HOL-Library: theory RBT

17:16:13 HOL-Library: theory Order_Continuity

17:16:13 Pre_Perron_Frobenius: theory Complex_Analysis_Basics

17:16:13 Pre_Perron_Frobenius: theory Interval_Integral

17:16:13 HOL-Library: theory RBT_Mapping

17:16:13 HOL-Library: theory RBT_Set

17:16:14 HOL-Library: theory Extended_Nat

17:16:14 Pre_Perron_Frobenius: theory Lebesgue_Integral_Substitution

17:16:14 HOL-Library: theory Periodic_Fun

17:16:15 HOL-Library: theory Extended_Real

17:16:15 HOL-Library: theory Linear_Temporal_Logic_on_Streams

17:16:15 Pre_Perron_Frobenius: theory Complex_Transcendental

17:16:17 HOL-Library: theory Polynomial_Factorial

17:16:17 Pre_Perron_Frobenius: theory Generalised_Binomial_Theorem

17:16:17 Pre_Perron_Frobenius: theory Harmonic_Numbers

17:16:17 Pre_Perron_Frobenius: theory Cauchy_Integral_Theorem

17:16:18 Pre_Perron_Frobenius: theory Gamma_Function

17:16:19 HOL-Library: theory Extended_Nonnegative_Real

17:16:20 HOL-Library: theory Quadratic_Discriminant

17:16:20 HOL-Library: theory Sum_of_Squares

17:16:21 HOL-Library: theory Transitive_Closure_Table

17:16:22 Pre_Perron_Frobenius: theory Conformal_Mappings

17:16:22 Pre_Perron_Frobenius: theory Further_Topology

17:16:22 HOL-Library: theory Tree

17:16:23 HOL-Library: theory Types_To_Sets

17:16:23 HOL-Library: theory While_Combinator

17:16:24 HOL-Library: theory Bourbaki_Witt_Fixpoint

17:16:24 Pre_Perron_Frobenius: theory Analysis

17:16:24 HOL-Library: theory Word_Miscellaneous

17:16:25 HOL-Library: theory Word

17:16:25 HOL-Library: theory Tree_Multiset

17:16:26 HOL-Library: theory Preorder

17:16:26 HOL-Library: theory Function_Growth

17:16:26 Polynomial_Factorization: theory Kronecker_Factorization

17:16:27 HOL-Library: theory Library

17:16:28 Pre_Perron_Frobenius: theory Rings2

17:16:30 Polynomial_Factorization: theory Fundamental_Theorem_Algebra_Factorized

17:16:30 Polynomial_Factorization: theory Polynomial_Divisibility

17:16:30 Polynomial_Factorization: theory Square_Free_Factorization

17:16:31 HOL-Library: theory Old_SMT

17:16:37 Polynomial_Factorization: theory Polynomial_Division

17:16:37 Polynomial_Factorization: theory Rational_Factorization

17:17:00 Pre_Perron_Frobenius: theory Cayley_Hamilton_Compatible

17:17:02 Pre_Perron_Frobenius: theory Code_Cayley_Hamilton

17:17:16 Timing Polynomial_Factorization (2 threads, 43.045s elapsed time, 87.096s cpu time, 2.440s GC time, factor 2.02)

17:17:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization

17:17:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf

17:17:16 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf

17:17:16 Finished Polynomial_Factorization (0:01:21 elapsed time, 0:02:23 cpu time, factor 1.76)

17:17:16 Building Pre_Algebraic_Numbers ...

17:17:16 Building Pre_BZ ...

17:17:21 Pre_BZ: theory MiscAlgebra

17:17:21 Pre_BZ: theory Missing_Ring

17:17:21 Pre_Algebraic_Numbers: theory Binary_Exponentiation

17:17:21 Pre_Algebraic_Numbers: theory MiscAlgebra

17:17:21 Pre_Algebraic_Numbers: theory Missing_Ring

17:17:22 Pre_BZ: theory Efficient_Sort

17:17:22 Pre_Algebraic_Numbers: theory Compare_Rat

17:17:23 Pre_Algebraic_Numbers: theory Compare_Real

17:17:23 Pre_Algebraic_Numbers: theory Efficient_Sort

17:17:26 Pre_BZ: theory Cong

17:17:27 Pre_Algebraic_Numbers: theory Arithmetic_Record_Based

17:17:27 Pre_BZ: theory Residues

17:17:29 Pre_BZ: theory Missing_Permutations

17:17:29 Pre_BZ: theory Types_To_Sets

17:17:29 Pre_BZ: theory Missing_VectorSpace

17:17:29 Pre_Algebraic_Numbers: theory Cong

17:17:30 Pre_BZ: theory Matrix

17:17:30 Pre_Algebraic_Numbers: theory Missing_Permutations

17:17:30 Pre_Algebraic_Numbers: theory Residues

17:17:31 Pre_Algebraic_Numbers: theory Show_Real

17:17:31 Pre_BZ: theory Missing_Fraction_Field

17:17:31 Pre_Algebraic_Numbers: theory Show_Complex

17:17:32 Pre_Algebraic_Numbers: theory Code_Abort_Gcd

17:17:32 Pre_Algebraic_Numbers: theory Misc_Polynomial

17:17:32 Pre_Algebraic_Numbers: theory Chinese_Remainder_Poly

17:17:32 Pre_Algebraic_Numbers: theory Sturm_Library

17:17:33 Pre_Algebraic_Numbers: theory Sturm_Theorem

17:17:33 Pre_BZ: theory Gauss_Jordan_Elimination

17:17:33 Pre_BZ: theory Matrix_IArray_Impl

17:17:33 Pre_Algebraic_Numbers: theory Polynomial_Record_Based

17:17:34 Pre_Algebraic_Numbers: theory Degree_Bound

17:17:35 Pre_BZ: theory Column_Operations

17:17:36 Pre_Algebraic_Numbers: theory Finite_Field

17:17:36 Pre_BZ: theory VS_Connect

17:17:36 Pre_BZ: theory Gauss_Jordan_IArray_Impl

17:17:36 Pre_Algebraic_Numbers: theory Types_To_Sets

17:17:36 Pre_Algebraic_Numbers: theory Sublist_Iteration

17:17:38 Pre_BZ: theory Determinant

17:17:39 Pre_Algebraic_Numbers: theory Finite_Field_Record_Based

17:17:40 Pre_BZ: theory Determinant_Impl

17:17:40 Pre_BZ: theory Matrix_Kernel

17:17:41 Pre_Algebraic_Numbers: theory Missing_VectorSpace

17:17:42 Pre_Algebraic_Numbers: theory Matrix

17:17:43 Pre_Algebraic_Numbers: theory Missing_Fraction_Field

17:17:44 Pre_Algebraic_Numbers: theory Bivariate_Polynomials

17:17:44 Pre_Algebraic_Numbers: theory Distinct_Degree_Factorization

17:17:46 Pre_Algebraic_Numbers: theory Gauss_Jordan_Elimination

17:17:46 Pre_Algebraic_Numbers: theory Matrix_IArray_Impl

17:17:48 Pre_Algebraic_Numbers: theory Column_Operations

17:17:48 Pre_Algebraic_Numbers: theory Show_Matrix

17:17:49 Pre_Algebraic_Numbers: theory Gauss_Jordan_IArray_Impl

17:17:49 Pre_Algebraic_Numbers: theory VS_Connect

17:17:50 Pre_Algebraic_Numbers: theory Matrix_Record_Based

17:17:52 Pre_Algebraic_Numbers: theory Determinant

17:17:52 Pre_Algebraic_Numbers: theory Poly_Mod

17:17:53 Pre_Algebraic_Numbers: theory Poly_Mod_Finite_Field

17:17:54 Pre_Algebraic_Numbers: theory Determinant_Impl

17:17:55 Pre_Algebraic_Numbers: theory Matrix_Kernel

17:17:56 Pre_Algebraic_Numbers: theory Char_Poly

17:17:58 Pre_Algebraic_Numbers: theory Poly_Mod_Finite_Field_Record_Based

17:17:58 Pre_Algebraic_Numbers: theory Berlekamp_Type_Based

17:17:59 Pre_Algebraic_Numbers: theory Factor_Bound

17:18:03 Pre_Algebraic_Numbers: theory Hensel_Lifting

17:18:03 Pre_Algebraic_Numbers: theory Finite_Field_Factorization

17:18:04 Pre_Algebraic_Numbers: theory Finite_Field_Factorization_Record_Based

17:18:08 Pre_Algebraic_Numbers: theory Resultant

17:18:09 Pre_Algebraic_Numbers: theory Berlekamp_Hensel

17:18:10 Pre_Algebraic_Numbers: theory Reconstruction

17:18:12 Pre_Algebraic_Numbers: theory Square_Free_Int_To_Square_Free_GFp

17:18:14 Pre_Algebraic_Numbers: theory Square_Free_Factorization_Int

17:18:14 Pre_Algebraic_Numbers: theory Suitable_Prime

17:18:16 Pre_Algebraic_Numbers: theory Berlekamp_Zassenhaus

17:18:17 Pre_Algebraic_Numbers: theory Factorize_Int_Poly

17:18:18 Pre_Algebraic_Numbers: theory Factorize_Rat_Poly

17:19:30 Timing Pre_BZ (2 threads, 86.187s elapsed time, 172.016s cpu time, 7.548s GC time, factor 2.00)

17:19:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_BZ

17:19:30 Finished Pre_BZ (0:02:14 elapsed time, 0:04:04 cpu time, factor 1.82)

17:19:31 Running Berlekamp_Zassenhaus ...

17:19:37 Berlekamp_Zassenhaus: theory Arithmetic_Record_Based

17:19:37 Berlekamp_Zassenhaus: theory Binary_Exponentiation

17:19:37 Berlekamp_Zassenhaus: theory Code_Abort_Gcd

17:19:37 Berlekamp_Zassenhaus: theory Chinese_Remainder_Poly

17:19:38 Berlekamp_Zassenhaus: theory Degree_Bound

17:19:39 Berlekamp_Zassenhaus: theory Polynomial_Record_Based

17:19:40 Berlekamp_Zassenhaus: theory Finite_Field

17:19:43 Berlekamp_Zassenhaus: theory Sublist_Iteration

17:19:43 Berlekamp_Zassenhaus: theory Finite_Field_Record_Based

17:19:44 Berlekamp_Zassenhaus: theory Matrix_Record_Based

17:19:46 Berlekamp_Zassenhaus: theory Bivariate_Polynomials

17:19:47 Berlekamp_Zassenhaus: theory Distinct_Degree_Factorization

17:19:48 Berlekamp_Zassenhaus: theory Poly_Mod

17:19:49 Berlekamp_Zassenhaus: theory Poly_Mod_Finite_Field

17:19:49 Berlekamp_Zassenhaus: theory Resultant

17:19:51 Berlekamp_Zassenhaus: theory Berlekamp_Type_Based

17:19:54 Berlekamp_Zassenhaus: theory Poly_Mod_Finite_Field_Record_Based

17:19:56 Berlekamp_Zassenhaus: theory Factor_Bound

17:19:56 Berlekamp_Zassenhaus: theory Finite_Field_Factorization

17:19:57 Berlekamp_Zassenhaus: theory Finite_Field_Factorization_Record_Based

17:19:59 Berlekamp_Zassenhaus: theory Hensel_Lifting

17:20:01 Berlekamp_Zassenhaus: theory Square_Free_Int_To_Square_Free_GFp

17:20:02 Berlekamp_Zassenhaus: theory Square_Free_Factorization_Int

17:20:03 Berlekamp_Zassenhaus: theory Suitable_Prime

17:20:05 Berlekamp_Zassenhaus: theory Berlekamp_Hensel

17:20:07 Berlekamp_Zassenhaus: theory Hensel_Lifting_Type_Based

17:20:07 Berlekamp_Zassenhaus: theory Reconstruction

17:20:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus

17:20:12 Berlekamp_Zassenhaus: theory Factorize_Int_Poly

17:20:13 Berlekamp_Zassenhaus: theory Factorize_Rat_Poly

17:21:03 Timing HOL-Library (2 threads, 246.106s elapsed time, 492.352s cpu time, 27.916s GC time, factor 2.00)

17:21:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library

17:21:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/document.pdf

17:21:03 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/outline.pdf

17:21:03 Finished HOL-Library (0:06:11 elapsed time, 0:11:36 cpu time, factor 1.87)

17:21:05 Building Coinductive ...

17:21:05 Building Deriving ...

17:21:05 Building LTL ...

17:21:05 Building MSO_Regex_Equivalence ...

17:21:05 Building Formula_Derivatives ...

17:21:09 LTL: theory LTL

17:21:09 Deriving: theory More_Bits_Int

17:21:09 MSO_Regex_Equivalence: theory Comparator

17:21:09 MSO_Regex_Equivalence: theory Derive_Manager

17:21:09 Formula_Derivatives: theory Coinductive_Language

17:21:09 Formula_Derivatives: theory Comparator

17:21:09 Coinductive: theory Primes

17:21:09 Coinductive: theory L2_Norm

17:21:09 MSO_Regex_Equivalence: theory Generator_Aux

17:21:09 MSO_Regex_Equivalence: theory List_Index

17:21:09 Coinductive: theory Inner_Product

17:21:10 MSO_Regex_Equivalence: theory List_More

17:21:10 Coinductive: theory Norm_Arith

17:21:10 MSO_Regex_Equivalence: theory Compare

17:21:10 Formula_Derivatives: theory Compare

17:21:10 MSO_Regex_Equivalence: theory Comparator_Generator

17:21:11 Coinductive: theory Product_Vector

17:21:11 Formula_Derivatives: theory Derive_Manager

17:21:11 MSO_Regex_Equivalence: theory Compare_Generator

17:21:11 Formula_Derivatives: theory FSet_More

17:21:11 Formula_Derivatives: theory Generator_Aux

17:21:11 Coinductive: theory Euclidean_Space

17:21:11 Deriving: theory Bits_Integer

17:21:12 Formula_Derivatives: theory List_Index

17:21:12 Deriving: theory Word_Misc

17:21:12 MSO_Regex_Equivalence: theory Compare_Instances

17:21:12 Formula_Derivatives: theory Comparator_Generator

17:21:12 Formula_Derivatives: theory While_Default

17:21:12 Formula_Derivatives: theory Compare_Generator

17:21:13 Formula_Derivatives: theory Compare_Instances

17:21:14 Coinductive: theory Linear_Algebra

17:21:16 MSO_Regex_Equivalence: theory Pi_Regular_Set

17:21:17 MSO_Regex_Equivalence: theory Pi_Regular_Exp

17:21:17 Coinductive: theory Topology_Euclidean_Space

17:21:19 LTL: theory LTL_Rewrite

17:21:19 Formula_Derivatives: theory WS1S_Prelim

17:21:19 Formula_Derivatives: theory Automaton

17:21:20 Formula_Derivatives: theory Abstract_Formula

17:21:25 LTL: theory LTL_Example

17:21:26 Deriving: theory Code_Target_Bits_Int

17:21:26 Deriving: theory Code_Target_ICF

17:21:27 Deriving: theory Uint32

17:21:28 Coinductive: theory Extended_Real_Limits

17:21:29 Deriving: theory HashCode

17:21:32 Deriving: theory Comparator

17:21:33 Deriving: theory Compare

17:21:34 Deriving: theory Derive_Manager

17:21:34 Deriving: theory Generator_Aux

17:21:34 Deriving: theory Countable_Generator

17:21:34 Deriving: theory Comparator_Generator

17:21:34 Deriving: theory Equality_Generator

17:21:35 Deriving: theory Equality_Instances

17:21:35 Deriving: theory RBT_Comparator_Impl

17:21:35 Deriving: theory Compare_Generator

17:21:35 Deriving: theory Compare_Instances

17:21:36 Deriving: theory Compare_Rat

17:21:36 Deriving: theory Compare_Real

17:21:37 Deriving: theory Compare_Order_Instances

17:21:38 Deriving: theory RBT_Compare_Order_Impl

17:21:38 Deriving: theory Hash_Generator

17:21:40 Deriving: theory Hash_Instances

17:21:40 Deriving: theory Derive

17:21:42 Deriving: theory Derive_Examples

17:21:52 Timing Berlekamp_Zassenhaus (2 threads, 127.478s elapsed time, 250.420s cpu time, 11.684s GC time, factor 1.96)

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

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

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

17:21:52 Finished Berlekamp_Zassenhaus (0:02:20 elapsed time, 0:04:26 cpu time, factor 1.89)

17:21:52 Building Group-Ring-Module ...

17:21:57 Group-Ring-Module: theory Algebra1

17:22:01 Coinductive: theory Resumption

17:22:01 Coinductive: theory Coinductive_Nat

17:22:02 MSO_Regex_Equivalence: theory Pi_Derivatives

17:22:02 Coinductive: theory Coinductive_List

17:22:02 MSO_Regex_Equivalence: theory PNormalization

17:22:03 Coinductive: theory CCPO_Topology

17:22:03 MSO_Regex_Equivalence: theory Pi_Regular_Exp_Dual

17:22:03 Group-Ring-Module: theory Algebra2

17:22:08 Group-Ring-Module: theory Algebra3

17:22:10 Coinductive: theory Coinductive_List_Prefix

17:22:10 Coinductive: theory Hamming_Stream

17:22:11 Coinductive: theory Koenigslemma

17:22:11 Coinductive: theory LMirror

17:22:11 Coinductive: theory Lazy_LList

17:22:12 Coinductive: theory Quotient_Coinductive_List

17:22:12 Coinductive: theory TLList

17:22:12 Coinductive: theory Coinductive_Stream

17:22:13 Group-Ring-Module: theory Algebra4

17:22:14 Coinductive: theory LList_CCPO_Topology

17:22:15 Coinductive: theory Lazy_TLList

17:22:15 MSO_Regex_Equivalence: theory Init_Normalization

17:22:16 Coinductive: theory Quotient_TLList

17:22:16 Coinductive: theory TLList_CCPO

17:22:17 Coinductive: theory TLList_CCPO_Examples

17:22:17 Coinductive: theory Coinductive

17:22:17 Coinductive: theory Coinductive_Examples

17:22:18 Timing LTL (2 threads, 29.325s elapsed time, 55.392s cpu time, 2.196s GC time, factor 1.89)

17:22:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL

17:22:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL/document.pdf

17:22:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL/outline.pdf

17:22:18 Finished LTL (0:01:12 elapsed time, 0:02:00 cpu time, factor 1.66)

17:22:18 Building Datatype_Order_Generator ...

17:22:20 Formula_Derivatives: theory Presburger_Formula

17:22:20 Formula_Derivatives: theory WS1S_Alt_Formula

17:22:20 Group-Ring-Module: theory Algebra5

17:22:22 Datatype_Order_Generator: theory More_Bits_Int

17:22:25 Datatype_Order_Generator: theory Bits_Integer

17:22:25 Datatype_Order_Generator: theory Word_Misc

17:22:26 Group-Ring-Module: theory Algebra6

17:22:29 Timing Pre_Algebraic_Numbers (2 threads, 218.982s elapsed time, 435.096s cpu time, 20.880s GC time, factor 1.99)

17:22:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pre_Algebraic_Numbers

17:22:29 Finished Pre_Algebraic_Numbers (0:05:12 elapsed time, 0:09:41 cpu time, factor 1.86)

17:22:29 Building Amortized_Complexity ...

17:22:33 Formula_Derivatives: theory WS1S_Formula

17:22:33 Group-Ring-Module: theory Algebra7

17:22:34 Amortized_Complexity: theory Pairing_Heap_List1

17:22:34 Amortized_Complexity: theory Pairing_Heap_List2

17:22:37 Amortized_Complexity: theory Splay_Tree

17:22:37 Amortized_Complexity: theory Pairing_Heap_Tree

17:22:38 Datatype_Order_Generator: theory Code_Target_Bits_Int

17:22:38 Amortized_Complexity: theory Skew_Heap

17:22:38 Datatype_Order_Generator: theory Code_Target_ICF

17:22:39 Amortized_Complexity: theory Splay_Heap

17:22:39 Datatype_Order_Generator: theory Uint32

17:22:41 Group-Ring-Module: theory Algebra8

17:22:41 Datatype_Order_Generator: theory HashCode

17:22:42 MSO_Regex_Equivalence: theory Pi_Equivalence_Checking

17:22:43 Group-Ring-Module: theory Algebra9

17:22:43 Datatype_Order_Generator: theory Derive_Manager

17:22:44 Datatype_Order_Generator: theory Derive_Aux

17:22:44 Datatype_Order_Generator: theory Order_Generator

17:22:44 Datatype_Order_Generator: theory Countable_Generator

17:22:44 Datatype_Order_Generator: theory Hash_Generator

17:22:45 Datatype_Order_Generator: theory Derive

17:22:46 MSO_Regex_Equivalence: theory Pi_Regular_Operators

17:22:46 Datatype_Order_Generator: theory Derive_Examples

17:22:47 MSO_Regex_Equivalence: theory Formula

17:22:49 Timing Deriving (2 threads, 48.199s elapsed time, 73.604s cpu time, 3.732s GC time, factor 1.53)

17:22:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deriving

17:22:49 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deriving/document.pdf

17:22:49 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deriving/outline.pdf

17:22:49 Finished Deriving (0:01:43 elapsed time, 0:03:07 cpu time, factor 1.80)

17:22:49 Building Containers ...

17:22:52 MSO_Regex_Equivalence: theory M2L

17:22:55 Containers: theory Regular_Set

17:22:55 MSO_Regex_Equivalence: theory M2L_Normalization

17:22:56 MSO_Regex_Equivalence: theory WS1S

17:22:57 Containers: theory Regular_Exp

17:23:00 MSO_Regex_Equivalence: theory WS1S_Normalization

17:23:01 Containers: theory NDerivative

17:23:01 Containers: theory Relation_Interpretation

17:23:04 Formula_Derivatives: theory WS1S_Nameful

17:23:05 Containers: theory Equivalence_Checking

17:23:05 Containers: theory Regexp_Method

17:23:07 Formula_Derivatives: theory WS1S_Presburger_Equivalence

17:23:08 Amortized_Complexity: theory Priority_Queue_ops_meld

17:23:08 Amortized_Complexity: theory Priority_Queue_ops

17:23:08 Containers: theory AssocList

17:23:08 Containers: theory Equal

17:23:09 Containers: theory Closure_Set

17:23:09 Containers: theory Extend_Partial_Order

17:23:09 Containers: theory List_Fusion

17:23:09 Containers: theory Containers_Auxiliary

17:23:10 Containers: theory Card_Datatype

17:23:10 Containers: theory Containers_Generator

17:23:10 Amortized_Complexity: theory Amortized_Framework

17:23:10 Amortized_Complexity: theory Amortized_Framework0

17:23:10 Containers: theory Collection_Enum

17:23:10 Containers: theory Lexicographic_Order

17:23:11 Containers: theory Set_Linorder

17:23:11 Containers: theory Collection_Eq

17:23:11 Amortized_Complexity: theory Amortized_Examples

17:23:12 Containers: theory DList_Set

17:23:13 Containers: theory RBT_ext

17:23:15 Amortized_Complexity: theory Lemmas_log

17:23:16 Amortized_Complexity: theory Pairing_Heap_List1_Analysis

17:23:19 Amortized_Complexity: theory Pairing_Heap_List2_Analysis

17:23:21 MSO_Regex_Equivalence: theory M2L_Equivalence_Checking

17:23:22 Containers: theory Collection_Order

17:23:23 Amortized_Complexity: theory Splay_Tree_Analysis_Base

17:23:23 Amortized_Complexity: theory Pairing_Heap_Tree_Analysis

17:23:25 Containers: theory List_Proper_Interval

17:23:25 Containers: theory RBT_Mapping2

17:23:25 MSO_Regex_Equivalence: theory WS1S_Equivalence_Checking

17:23:26 Amortized_Complexity: theory Splay_Tree_Analysis

17:23:27 Containers: theory RBT_Set2

17:23:28 Amortized_Complexity: theory Splay_Tree_Analysis_Optimal

17:23:28 Amortized_Complexity: theory Pairing_Heap_List1_Analysis2

17:23:29 Containers: theory Set_Impl

17:23:29 Amortized_Complexity: theory Skew_Heap_Analysis

17:23:29 Amortized_Complexity: theory Splay_Heap_Analysis

17:23:46 Timing Coinductive (2 threads, 102.909s elapsed time, 194.204s cpu time, 7.640s GC time, factor 1.89)

17:23:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Coinductive

17:23:46 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Coinductive/document.pdf

17:23:46 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Coinductive/outline.pdf

17:23:46 Finished Coinductive (0:02:41 elapsed time, 0:04:49 cpu time, factor 1.80)

17:23:46 Building Regex_Equivalence ...

17:23:48 Containers: theory Mapping_Impl

17:23:50 Containers: theory Map_To_Mapping

17:23:51 Regex_Equivalence: theory Efficient_Sort

17:23:51 Regex_Equivalence: theory Regular_Set

17:23:51 Containers: theory Containers

17:23:51 Containers: theory Containers_Userguide

17:23:51 Containers: theory Compatibility_Containers_Regular_Sets

17:23:54 Regex_Equivalence: theory Regular_Exp

17:23:59 Regex_Equivalence: theory Derivatives

17:23:59 Regex_Equivalence: theory NDerivative

17:24:12 Regex_Equivalence: theory Automaton

17:24:12 Regex_Equivalence: theory Derivatives_Finite

17:24:13 Regex_Equivalence: theory Position_Autos

17:24:15 Regex_Equivalence: theory After2

17:24:16 Regex_Equivalence: theory Deriv_PDeriv

17:24:20 Regex_Equivalence: theory Deriv_Autos

17:24:21 Regex_Equivalence: theory Before2

17:24:32 Regex_Equivalence: theory Regex_Equivalence

17:24:48 Containers: theory Card_Datatype_Ex

17:24:48 Containers: theory Map_To_Mapping_Ex

17:25:32 Timing Amortized_Complexity (2 threads, 98.446s elapsed time, 194.036s cpu time, 7.464s GC time, factor 1.97)

17:25:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Amortized_Complexity

17:25:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Amortized_Complexity/document.pdf

17:25:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Amortized_Complexity/outline.pdf

17:25:32 Finished Amortized_Complexity (0:03:01 elapsed time, 0:05:26 cpu time, factor 1.79)

17:25:33 Building Sturm_Sequences ...

17:25:37 Sturm_Sequences: theory Sturm_Library_Document

17:25:37 Sturm_Sequences: theory Misc_Polynomial

17:25:42 Sturm_Sequences: theory Sturm_Library

17:25:44 Sturm_Sequences: theory Sturm_Theorem

17:25:45 Sturm_Sequences: theory Sturm_Method

17:25:46 Sturm_Sequences: theory Sturm

17:25:46 Sturm_Sequences: theory Sturm_Ex

17:25:53 Timing Regex_Equivalence (2 threads, 63.099s elapsed time, 124.048s cpu time, 5.988s GC time, factor 1.97)

17:25:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regex_Equivalence

17:25:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regex_Equivalence/document.pdf

17:25:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regex_Equivalence/outline.pdf

17:25:53 Finished Regex_Equivalence (0:02:06 elapsed time, 0:03:46 cpu time, factor 1.79)

17:25:53 Building Regular-Sets ...

17:25:58 Regular-Sets: theory Regular_Set

17:26:00 Regular-Sets: theory Regular_Exp

17:26:00 Regular-Sets: theory Regular_Exp2

17:26:03 Regular-Sets: theory Equivalence_Checking2

17:26:04 Regular-Sets: theory Derivatives

17:26:05 Regular-Sets: theory NDerivative

17:26:10 Regular-Sets: theory Relation_Interpretation

17:26:10 Regular-Sets: theory Equivalence_Checking

17:26:10 Regular-Sets: theory Regexp_Method

17:26:11 Regular-Sets: theory pEquivalence_Checking

17:26:30 Timing Containers (2 threads, 120.878s elapsed time, 227.516s cpu time, 11.552s GC time, factor 1.88)

17:26:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers

17:26:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers/document.pdf

17:26:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers/outline.pdf

17:26:30 Finished Containers (0:03:40 elapsed time, 0:06:30 cpu time, factor 1.77)

17:26:31 Building List-Infinite ...

17:26:35 List-Infinite: theory Util_NatInf

17:26:35 List-Infinite: theory Util_MinMax

17:26:36 List-Infinite: theory Util_Nat

17:26:36 List-Infinite: theory Util_Set

17:26:36 List-Infinite: theory Util_Div

17:26:37 List-Infinite: theory SetInterval2

17:26:39 List-Infinite: theory InfiniteSet2

17:26:40 List-Infinite: theory SetIntervalCut

17:26:41 List-Infinite: theory List2

17:26:41 List-Infinite: theory SetIntervalStep

17:26:43 List-Infinite: theory ListInf

17:26:45 List-Infinite: theory ListInf_Prefix

17:26:47 List-Infinite: theory ListInfinite

17:26:50 Timing Group-Ring-Module (2 threads, 231.478s elapsed time, 458.328s cpu time, 19.900s GC time, factor 1.98)

17:26:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Group-Ring-Module

17:26:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Group-Ring-Module/document.pdf

17:26:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Group-Ring-Module/outline.pdf

17:26:50 Finished Group-Ring-Module (0:04:57 elapsed time, 0:09:18 cpu time, factor 1.88)

17:26:50 Building Bell_Numbers_Spivey ...

17:26:55 Bell_Numbers_Spivey: theory Additions_to_Main

17:26:55 Timing Sturm_Sequences (2 threads, 47.693s elapsed time, 95.980s cpu time, 1.792s GC time, factor 2.01)

17:26:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sturm_Sequences

17:26:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sturm_Sequences/document.pdf

17:26:55 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sturm_Sequences/outline.pdf

17:26:55 Finished Sturm_Sequences (0:01:22 elapsed time, 0:02:27 cpu time, factor 1.78)

17:26:55 Building Lazy-Lists-II ...

17:26:56 Bell_Numbers_Spivey: theory Eisbach

17:26:56 Bell_Numbers_Spivey: theory Card_Partitions

17:26:56 Bell_Numbers_Spivey: theory Set_Partition

17:26:57 Bell_Numbers_Spivey: theory Bell_Numbers

17:27:00 Lazy-Lists-II: theory LList2

17:27:27 Timing Regular-Sets (2 threads, 44.616s elapsed time, 86.164s cpu time, 3.996s GC time, factor 1.93)

17:27:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular-Sets

17:27:27 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular-Sets/document.pdf

17:27:27 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Regular-Sets/outline.pdf

17:27:27 Finished Regular-Sets (0:01:33 elapsed time, 0:02:44 cpu time, factor 1.76)

17:27:27 Running Category3 ...

17:27:30 Timing Lazy-Lists-II (2 threads, 2.224s elapsed time, 5.788s cpu time, 0.152s GC time, factor 2.60)

17:27:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lazy-Lists-II

17:27:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lazy-Lists-II/document.pdf

17:27:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lazy-Lists-II/outline.pdf

17:27:30 Finished Lazy-Lists-II (0:00:35 elapsed time, 0:00:53 cpu time, factor 1.53)

17:27:30 Running Algebraic_Numbers ...

17:27:32 Category3: theory Category

17:27:32 Timing List-Infinite (2 threads, 23.423s elapsed time, 48.104s cpu time, 2.192s GC time, factor 2.05)

17:27:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List-Infinite

17:27:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List-Infinite/document.pdf

17:27:32 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List-Infinite/outline.pdf

17:27:32 Finished List-Infinite (0:01:00 elapsed time, 0:01:44 cpu time, factor 1.71)

17:27:33 Building Nat-Interval-Logic ...

17:27:33 Category3: theory AbstractedCategory

17:27:33 Category3: theory DiscreteCategory

17:27:33 Category3: theory DualCategory

17:27:33 Category3: theory EpiMonoIso

17:27:33 Category3: theory FreeCategory

17:27:33 Category3: theory InitialTerminal

17:27:33 Category3: theory Functor

17:27:35 Category3: theory ProductCategory

17:27:36 Category3: theory NaturalTransformation

17:27:36 Category3: theory SetCategory

17:27:37 Nat-Interval-Logic: theory IL_Interval

17:27:37 Algebraic_Numbers: theory Compare_Complex

17:27:37 Algebraic_Numbers: theory Complex_Roots_Real_Poly

17:27:38 Category3: theory SetCat

17:27:39 Algebraic_Numbers: theory Algebraic_Numbers_Prelim

17:27:39 Category3: theory BinaryFunctor

17:27:39 Nat-Interval-Logic: theory IL_IntervalOperators

17:27:40 Algebraic_Numbers: theory Algebraic_Numbers

17:27:40 Timing Bell_Numbers_Spivey (2 threads, 17.897s elapsed time, 36.664s cpu time, 0.712s GC time, factor 2.05)

17:27:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bell_Numbers_Spivey

17:27:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bell_Numbers_Spivey/document.pdf

17:27:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bell_Numbers_Spivey/outline.pdf

17:27:40 Finished Bell_Numbers_Spivey (0:00:49 elapsed time, 0:01:22 cpu time, factor 1.68)

17:27:40 Running CoreC++ ...

17:27:40 Algebraic_Numbers: theory Sturm_Rat

17:27:43 Category3: theory FunctorCategory

17:27:43 Nat-Interval-Logic: theory IL_TemporalOperators

17:27:44 Algebraic_Numbers: theory Real_Algebraic_Numbers

17:27:45 CoreC++: theory Auxiliary

17:27:45 CoreC++: theory Type

17:27:47 CoreC++: theory Value

17:27:48 Category3: theory Yoneda

17:27:48 CoreC++: theory Expr

17:27:54 CoreC++: theory Decl

17:27:55 CoreC++: theory ClassRel

17:27:55 CoreC++: theory SubObj

17:27:57 Category3: theory Adjunction

17:27:57 CoreC++: theory Objects

17:27:57 CoreC++: theory TypeRel

17:27:57 CoreC++: theory Exceptions

17:27:58 CoreC++: theory State

17:27:58 CoreC++: theory Syntax

17:27:58 CoreC++: theory SystemClasses

17:27:58 CoreC++: theory BigStep

17:27:58 CoreC++: theory SmallStep

17:28:02 Algebraic_Numbers: theory Real_Roots

17:28:02 Algebraic_Numbers: theory Show_Real_Alg

17:28:02 Algebraic_Numbers: theory Show_Real_Approx

17:28:03 Algebraic_Numbers: theory Show_Real_Precise

17:28:03 Algebraic_Numbers: theory Complex_Algebraic_Numbers

17:28:04 CoreC++: theory DefAss

17:28:05 CoreC++: theory WellType

17:28:06 Algebraic_Numbers: theory Real_Factorization

17:28:06 CoreC++: theory Annotate

17:28:07 CoreC++: theory Execute

17:28:07 CoreC++: theory WellForm

17:28:08 CoreC++: theory WellTypeRT

17:28:10 CoreC++: theory Conform

17:28:11 CoreC++: theory WWellForm

17:28:11 CoreC++: theory CWellForm

17:28:12 CoreC++: theory Equivalence

17:28:14 CoreC++: theory Progress

17:28:16 CoreC++: theory HeapExtension

17:28:17 CoreC++: theory TypeSafe

17:28:18 CoreC++: theory Determinism

17:28:21 Timing Pre_Perron_Frobenius (2 threads, 680.842s elapsed time, 1328.060s cpu time, 91.316s GC time, factor 1.95)

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

17:28:21 Finished Pre_Perron_Frobenius (0:13:29 elapsed time, 0:25:34 cpu time, factor 1.89)

17:28:22 Running Containers-Benchmarks ...

17:28:30 Containers-Benchmarks: theory Trie

17:28:30 Containers-Benchmarks: theory Benchmark_Comparison

17:28:30 Algebraic_Numbers: theory Algebraic_Number_Tests

17:28:31 Containers-Benchmarks: theory Benchmark_Default

17:28:31 Containers-Benchmarks: theory FingerTree

17:28:32 Containers-Benchmarks: theory Foldi

17:28:32 Containers-Benchmarks: theory ICF_Tools

17:28:32 Containers-Benchmarks: theory BinomialHeap

17:28:34 Category3: theory Limit

17:28:37 Containers-Benchmarks: theory List_More

17:28:37 Containers-Benchmarks: theory Quicksort

17:28:38 Containers-Benchmarks: theory Misc

17:28:39 Timing Datatype_Order_Generator (2 threads, 219.520s elapsed time, 418.612s cpu time, 60.988s GC time, factor 1.91)

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

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

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

17:28:39 Finished Datatype_Order_Generator (0:06:21 elapsed time, 0:11:57 cpu time, factor 1.88)

17:28:40 Running Isabelle_Meta_Model ...

17:28:42 Timing Nat-Interval-Logic (2 threads, 34.464s elapsed time, 67.744s cpu time, 1.344s GC time, factor 1.97)

17:28:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nat-Interval-Logic

17:28:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nat-Interval-Logic/document.pdf

17:28:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nat-Interval-Logic/outline.pdf

17:28:42 Finished Nat-Interval-Logic (0:01:09 elapsed time, 0:01:59 cpu time, factor 1.71)

17:28:42 Running Buildings ...

17:28:44 Isabelle_Meta_Model: theory Isabelle_Cartouche_Examples

17:28:44 Isabelle_Meta_Model: theory Isabelle_code_runtime

17:28:44 Isabelle_Meta_Model: theory Isabelle_Main0

17:28:44 Isabelle_Meta_Model: theory Isabelle_code_target

17:28:44 Isabelle_Meta_Model: theory Isabelle_typedecl

17:28:44 Isabelle_Meta_Model: theory Isabelle_Main2

17:28:44 Isabelle_Meta_Model: theory Isabelle_Main1

17:28:45 Isabelle_Meta_Model: theory Init

17:28:46 Containers-Benchmarks: theory SetIterator

17:28:47 Buildings: theory Prelim

17:28:48 Containers-Benchmarks: theory Ord_Code_Preproc

17:28:48 Containers-Benchmarks: theory Locale_Code

17:28:48 Containers-Benchmarks: theory Prio_List

17:28:48 Containers-Benchmarks: theory Benchmark_RBT

17:28:49 Containers-Benchmarks: theory Record_Intf

17:28:49 Containers-Benchmarks: theory Refine_Chapter

17:28:49 Containers-Benchmarks: theory Refine_Util

17:28:49 Containers-Benchmarks: theory Anti_Unification

17:28:49 Containers-Benchmarks: theory Attr_Comb

17:28:49 Containers-Benchmarks: theory Named_Sorted_Thms

17:28:49 Buildings: theory Simplicial

17:28:49 Buildings: theory Algebra

17:28:49 Containers-Benchmarks: theory Autoref_Data

17:28:49 Containers-Benchmarks: theory Digraph_Basic

17:28:50 Isabelle_Meta_Model: theory Meta_Pure

17:28:50 Isabelle_Meta_Model: theory Meta_SML

17:28:51 Containers-Benchmarks: theory Mk_Term_Antiquot

17:28:51 Containers-Benchmarks: theory Mpat_Antiquot

17:28:51 Containers-Benchmarks: theory Indep_Vars

17:28:51 Containers-Benchmarks: theory Mk_Record_Simp

17:28:51 Containers-Benchmarks: theory Tagged_Solver

17:28:51 Containers-Benchmarks: theory Select_Solve

17:28:51 Containers-Benchmarks: theory SetIteratorOperations

17:28:51 Containers-Benchmarks: theory Refine_Lib

17:28:52 Isabelle_Meta_Model: theory Parser_init

17:28:52 Containers-Benchmarks: theory Autoref_Phases

17:28:53 Containers-Benchmarks: theory Autoref_Tagging

17:28:53 Containers-Benchmarks: theory Refine_Mono_Prover

17:28:53 Containers-Benchmarks: theory Relators

17:28:53 Isabelle_Meta_Model: theory Parser_Pure

17:28:54 Isabelle_Meta_Model: theory Printer_init

17:28:54 Containers-Benchmarks: theory Param_Tool

17:28:54 Buildings: theory Chamber

17:28:54 Containers-Benchmarks: theory Assoc_List

17:28:54 Containers-Benchmarks: theory Param_HOL

17:28:55 Isabelle_Meta_Model: theory Meta_Isabelle

17:28:55 Containers-Benchmarks: theory Trie_Impl

17:28:55 Isabelle_Meta_Model: theory Printer_Pure

17:28:56 Containers-Benchmarks: theory Trie2

17:28:56 Isabelle_Meta_Model: theory Printer_SML

17:28:56 Containers-Benchmarks: theory Parametricity

17:28:56 Containers-Benchmarks: theory Dlist_add

17:28:56 Containers-Benchmarks: theory Autoref_Id_Ops

17:28:56 Containers-Benchmarks: theory Diff_Array

17:28:57 Containers-Benchmarks: theory Autoref_Fix_Rel

17:28:58 Containers-Benchmarks: theory Autoref_Translate

17:28:58 Containers-Benchmarks: theory Autoref_Gen_Algo

17:28:58 Containers-Benchmarks: theory Autoref_Relator_Interface

17:28:58 Containers-Benchmarks: theory Autoref_Tool

17:28:58 Containers-Benchmarks: theory Proper_Iterator

17:28:59 Containers-Benchmarks: theory It_to_It

17:28:59 Containers-Benchmarks: theory Autoref_Bindings_HOL

17:28:59 Containers-Benchmarks: theory SetIteratorGA

17:29:00 Buildings: theory Coxeter

17:29:01 Containers-Benchmarks: theory SkewBinomialHeap

17:29:03 Buildings: theory Building

17:29:04 Containers-Benchmarks: theory Automatic_Refinement

17:29:04 Containers-Benchmarks: theory Idx_Iterator

17:29:04 Containers-Benchmarks: theory Refine_Misc

17:29:05 Containers-Benchmarks: theory RefineG_Domain

17:29:06 Containers-Benchmarks: theory RefineG_Transfer

17:29:07 Containers-Benchmarks: theory RefineG_Assert

17:29:07 Containers-Benchmarks: theory RefineG_Recursion

17:29:08 Containers-Benchmarks: theory Refine_Basic

17:29:10 CoreC++: theory CoreC++

17:29:15 Containers-Benchmarks: theory Refine_Heuristics

17:29:16 Containers-Benchmarks: theory Refine_Leof

17:29:16 Isabelle_Meta_Model: theory Printer_Isabelle

17:29:16 Containers-Benchmarks: theory Sorted_List_Operations

17:29:17 Containers-Benchmarks: theory Benchmark_Bool

17:29:17 Containers-Benchmarks: theory Benchmark_LC

17:29:17 Containers-Benchmarks: theory Clauses

17:29:19 Containers-Benchmarks: theory DatRef

17:29:21 Containers-Benchmarks: theory RefineG_While

17:29:21 Containers-Benchmarks: theory Refine_Det

17:29:23 Containers-Benchmarks: theory Refine_While

17:29:24 Containers-Benchmarks: theory Refine_Pfun

17:29:25 Containers-Benchmarks: theory Refine_Transfer

17:29:25 Containers-Benchmarks: theory Benchmark_Set

17:29:25 Containers-Benchmarks: theory Autoref_Monadic

17:29:25 Containers-Benchmarks: theory Refine_Automation

17:29:26 Isabelle_Meta_Model: theory Meta_Toy_extended

17:29:26 Isabelle_Meta_Model: theory Init_rbt

17:29:26 Containers-Benchmarks: theory Refine_Foreach

17:29:26 Isabelle_Meta_Model: theory Meta_Toy

17:29:27 Containers-Benchmarks: theory Benchmark_Set_Default

17:29:29 Containers-Benchmarks: theory Refine_Monadic

17:29:29 Containers-Benchmarks: theory Benchmark_Set_LC

17:29:30 Containers-Benchmarks: theory Gen_Iterator

17:29:30 Containers-Benchmarks: theory Iterator

17:29:31 Containers-Benchmarks: theory Array_Iterator

17:29:32 Containers-Benchmarks: theory ICF_Spec_Base

17:29:32 Containers-Benchmarks: theory AnnotatedListSpec

17:29:33 Isabelle_Meta_Model: theory Parser_Toy_extended

17:29:34 Isabelle_Meta_Model: theory Toy_Library_Static

17:29:35 Containers-Benchmarks: theory FTAnnotatedListImpl

17:29:37 Containers-Benchmarks: theory ListSpec

17:29:38 Containers-Benchmarks: theory MapSpec

17:29:39 Containers-Benchmarks: theory ListGA

17:29:40 Containers-Benchmarks: theory Fifo

17:29:41 Containers-Benchmarks: theory PrioSpec

17:29:43 Containers-Benchmarks: theory PrioUniqueSpec

17:29:43 Containers-Benchmarks: theory BinoPrioImpl

17:29:44 Containers-Benchmarks: theory PrioByAnnotatedList

17:29:44 Containers-Benchmarks: theory SkewPrioImpl

17:29:45 Containers-Benchmarks: theory PrioUniqueByAnnotatedList

17:29:46 Containers-Benchmarks: theory FTPrioImpl

17:29:47 Isabelle_Meta_Model: theory Meta_META

17:29:47 Isabelle_Meta_Model: theory Parser_Toy

17:29:47 Containers-Benchmarks: theory SetSpec

17:29:48 Containers-Benchmarks: theory FTPrioUniqueImpl

17:29:49 Isabelle_Meta_Model: theory Printer_Toy

17:29:49 Containers-Benchmarks: theory RBT_add

17:29:50 Isabelle_Meta_Model: theory Printer_Toy_extended

17:29:51 Containers-Benchmarks: theory Intf_Map

17:29:52 Containers-Benchmarks: theory Intf_Set

17:29:52 Containers-Benchmarks: theory Algos

17:29:52 Containers-Benchmarks: theory SetIndex

17:29:53 Containers-Benchmarks: theory SetIteratorCollectionsGA

17:29:54 Containers-Benchmarks: theory MapGA

17:29:54 Containers-Benchmarks: theory SetGA

17:29:57 Containers-Benchmarks: theory ArrayMapImpl

17:29:59 Isabelle_Meta_Model: theory Parser_META

17:29:59 Isabelle_Meta_Model: theory Core_init

17:30:00 Containers-Benchmarks: theory ListMapImpl

17:30:01 Containers-Benchmarks: theory ListMapImpl_Invar

17:30:01 Isabelle_Meta_Model: theory Printer_META

17:30:01 Containers-Benchmarks: theory TrieMapImpl

17:30:03 Containers-Benchmarks: theory ListSetImpl

17:30:04 Containers-Benchmarks: theory ListSetImpl_Invar

17:30:05 Containers-Benchmarks: theory ListSetImpl_NotDist

17:30:05 Containers-Benchmarks: theory ListSetImpl_Sorted

17:30:05 Isabelle_Meta_Model: theory Floor1_access

17:30:05 Isabelle_Meta_Model: theory Floor1_ctxt

17:30:06 Isabelle_Meta_Model: theory Floor1_examp

17:30:06 Isabelle_Meta_Model: theory Floor1_infra

17:30:06 Isabelle_Meta_Model: theory Floor2_examp

17:30:07 Containers-Benchmarks: theory SetByMap

17:30:07 Isabelle_Meta_Model: theory Core

17:30:09 Containers-Benchmarks: theory RBTMapImpl

17:30:09 Containers-Benchmarks: theory ArraySetImpl

17:30:11 Isabelle_Meta_Model: theory Printer

17:30:12 Containers-Benchmarks: theory TrieSetImpl

17:30:12 Isabelle_Meta_Model: theory Toy_Library

17:30:12 Isabelle_Meta_Model: theory Generator_dynamic

17:30:13 Isabelle_Meta_Model: theory Generator_static

17:30:13 Containers-Benchmarks: theory RBTSetImpl

17:30:13 Isabelle_Meta_Model: theory Design_generated_generated

17:30:14 Containers-Benchmarks: theory ArrayHashMap_Impl

17:30:16 Containers-Benchmarks: theory HashMap_Impl

17:30:19 Containers-Benchmarks: theory HashMap

17:30:19 Containers-Benchmarks: theory ArrayHashMap

17:30:21 Containers-Benchmarks: theory HashSet

17:30:22 Containers-Benchmarks: theory ArrayHashSet

17:30:25 Containers-Benchmarks: theory MapStdImpl

17:30:25 Containers-Benchmarks: theory SetStdImpl

17:30:30 Containers-Benchmarks: theory ICF_Impl

17:30:37 Containers-Benchmarks: theory ICF_Refine_Monadic

17:30:38 Containers-Benchmarks: theory ICF_Autoref

17:30:42 Containers-Benchmarks: theory Collections

17:30:43 Containers-Benchmarks: theory CollectionsV1

17:30:51 Isabelle_Meta_Model: theory Design_deep

17:30:51 Isabelle_Meta_Model: theory Rail

17:30:52 Isabelle_Meta_Model: theory Design_shallow

17:30:52 Containers-Benchmarks: theory Benchmark_ICF

17:31:11 Timing Buildings (2 threads, 137.572s elapsed time, 274.512s cpu time, 5.312s GC time, factor 2.00)

17:31:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buildings

17:31:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buildings/document.pdf

17:31:11 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buildings/outline.pdf

17:31:11 Finished Buildings (0:02:27 elapsed time, 0:04:47 cpu time, factor 1.95)

17:31:11 Running LTL_to_DRA ...

17:31:15 LTL_to_DRA: theory DFS

17:31:15 LTL_to_DRA: theory List_Index

17:31:16 LTL_to_DRA: theory Boolean_Expression_Checkers

17:31:21 LTL_to_DRA: theory Boolean_Expression_Checkers_AList_Mapping

17:31:25 LTL_to_DRA: theory List2

17:31:25 LTL_to_DRA: theory LTL_FGXU

17:31:26 LTL_to_DRA: theory Map2

17:31:26 LTL_to_DRA: theory Mapping2

17:31:26 LTL_to_DRA: theory DTS

17:31:28 LTL_to_DRA: theory Preliminaries2

17:31:29 LTL_to_DRA: theory Rabin

17:31:30 LTL_to_DRA: theory Semi_Mojmir

17:31:31 Timing Isabelle_Meta_Model (2 threads, 163.007s elapsed time, 253.796s cpu time, 19.584s GC time, factor 1.56)

17:31:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Isabelle_Meta_Model

17:31:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Isabelle_Meta_Model/document.pdf

17:31:31 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Isabelle_Meta_Model/outline.pdf

17:31:31 Finished Isabelle_Meta_Model (0:02:51 elapsed time, 0:04:24 cpu time, factor 1.55)

17:31:31 Running KBPs ...

17:31:32 LTL_to_DRA: theory LTL_Compat

17:31:32 LTL_to_DRA: theory LTL_Impl

17:31:33 Timing CoreC++ (2 threads, 220.312s elapsed time, 435.776s cpu time, 33.872s GC time, factor 1.98)

17:31:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++

17:31:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/document.pdf

17:31:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/outline.pdf

17:31:33 Finished CoreC++ (0:03:52 elapsed time, 0:07:31 cpu time, factor 1.94)

17:31:33 Running SATSolverVerification ...

17:31:34 LTL_to_DRA: theory Mojmir

17:31:34 LTL_to_DRA: theory Mojmir_Rabin

17:31:35 LTL_to_DRA: theory af

17:31:35 LTL_to_DRA: theory Mojmir_Rabin_Impl

17:31:35 KBPs: theory Extra

17:31:36 KBPs: theory List_local

17:31:38 SATSolverVerification: theory MoreList

17:31:38 LTL_to_DRA: theory Logical_Characterization

17:31:38 SATSolverVerification: theory CNF

17:31:39 SATSolverVerification: theory Trail

17:31:39 LTL_to_DRA: theory af_Impl

17:31:39 LTL_to_DRA: theory LTL_Rabin

17:31:40 SATSolverVerification: theory SatSolverVerification

17:31:42 SATSolverVerification: theory BasicDPLL

17:31:42 SATSolverVerification: theory KrsticGoel

17:31:42 SATSolverVerification: theory NieuwenhuisOliverasTinelli

17:31:43 SATSolverVerification: theory SatSolverCode

17:31:46 SATSolverVerification: theory AssertLiteral

17:31:47 SATSolverVerification: theory ConflictAnalysis

17:31:47 SATSolverVerification: theory Decide

17:31:47 SATSolverVerification: theory UnitPropagate

17:31:47 LTL_to_DRA: theory LTL_Rabin_Unfold_Opt

17:31:48 SATSolverVerification: theory Initialization

17:31:48 SATSolverVerification: theory SolveLoop

17:31:49 SATSolverVerification: theory FunctionalImplementation

17:31:57 LTL_to_DRA: theory LTL_Rabin_Impl

17:31:59 Timing Formula_Derivatives (2 threads, 613.037s elapsed time, 1142.844s cpu time, 653.648s GC time, factor 1.86)

17:31:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Formula_Derivatives

17:31:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Formula_Derivatives/document.pdf

17:31:59 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Formula_Derivatives/outline.pdf

17:31:59 Finished Formula_Derivatives (0:10:53 elapsed time, 0:20:04 cpu time, factor 1.84)

17:32:00 Running LinearQuantifierElim ...

17:32:02 LTL_to_DRA: theory Export_Code

17:32:04 LinearQuantifierElim: theory Logic

17:32:05 KBPs: theory Trie

17:32:05 KBPs: theory DFS

17:32:05 KBPs: theory Kripke

17:32:07 KBPs: theory MapOps

17:32:08 KBPs: theory Traces

17:32:08 LinearQuantifierElim: theory QE

17:32:08 KBPs: theory Transitive_Closure_Impl

17:32:09 KBPs: theory KBPs

17:32:09 KBPs: theory Transitive_Closure_List_Impl

17:32:09 KBPs: theory ODList

17:32:10 LinearQuantifierElim: theory PresArith

17:32:10 LinearQuantifierElim: theory DLO

17:32:10 Timing Containers-Benchmarks (2 threads, 219.729s elapsed time, 437.472s cpu time, 41.228s GC time, factor 1.99)

17:32:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers-Benchmarks

17:32:10 Finished Containers-Benchmarks (0:03:47 elapsed time, 0:07:24 cpu time, factor 1.96)

17:32:10 Running Separation_Logic_Imperative_HOL ...

17:32:11 KBPs: theory KBPsAuto

17:32:12 KBPs: theory Eval

17:32:13 LinearQuantifierElim: theory Cooper

17:32:13 LinearQuantifierElim: theory QEpres

17:32:13 LinearQuantifierElim: theory QEdlo

17:32:13 LinearQuantifierElim: theory QEdlo_fr

17:32:14 KBPs: theory KBPsAlg

17:32:14 LinearQuantifierElim: theory QEdlo_ex

17:32:14 LinearQuantifierElim: theory QEdlo_inf

17:32:14 KBPs: theory SPRView

17:32:14 Separation_Logic_Imperative_HOL: theory List_More

17:32:14 Separation_Logic_Imperative_HOL: theory Quicksort

17:32:14 LinearQuantifierElim: theory LinArith

17:32:14 Separation_Logic_Imperative_HOL: theory Heap

17:32:15 KBPs: theory SPRViewNonDet

17:32:15 Separation_Logic_Imperative_HOL: theory Misc

17:32:16 Separation_Logic_Imperative_HOL: theory Heap_Monad

17:32:18 LinearQuantifierElim: theory FRE

17:32:18 Timing MSO_Regex_Equivalence (2 threads, 567.495s elapsed time, 1115.656s cpu time, 39.904s GC time, factor 1.97)

17:32:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MSO_Regex_Equivalence

17:32:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MSO_Regex_Equivalence/document.pdf

17:32:18 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MSO_Regex_Equivalence/outline.pdf

17:32:18 Finished MSO_Regex_Equivalence (0:11:12 elapsed time, 0:21:25 cpu time, factor 1.91)

17:32:18 LinearQuantifierElim: theory QElin

17:32:18 KBPs: theory Trie2

17:32:18 LinearQuantifierElim: theory QElin_inf

17:32:18 KBPs: theory SPRViewNonDetIndInit

17:32:18 LinearQuantifierElim: theory QElin_opt

17:32:19 Running MSO_Examples ...

17:32:19 KBPs: theory ClockView

17:32:19 Separation_Logic_Imperative_HOL: theory Array

17:32:20 Separation_Logic_Imperative_HOL: theory Ref

17:32:20 Separation_Logic_Imperative_HOL: theory Imperative_HOL

17:32:20 Separation_Logic_Imperative_HOL: theory Imperative_HOL_Add

17:32:21 KBPs: theory SPRViewDet

17:32:21 Separation_Logic_Imperative_HOL: theory Syntax_Match

17:32:21 Separation_Logic_Imperative_HOL: theory More_Bits_Int

17:32:22 Separation_Logic_Imperative_HOL: theory Sep_Misc

17:32:24 Separation_Logic_Imperative_HOL: theory Bits_Integer

17:32:24 Separation_Logic_Imperative_HOL: theory Word_Misc

17:32:24 MSO_Examples: theory M2L_Examples

17:32:24 MSO_Examples: theory WS1S_Examples

17:32:26 KBPs: theory SPRViewSingle

17:32:34 KBPs: theory Robot

17:32:34 KBPs: theory MuddyChildren

17:32:38 Separation_Logic_Imperative_HOL: theory Code_Target_Bits_Int

17:32:38 Separation_Logic_Imperative_HOL: theory Uint32

17:32:38 Separation_Logic_Imperative_HOL: theory Code_Target_ICF

17:32:40 Separation_Logic_Imperative_HOL: theory HashCode

17:32:42 KBPs: theory Views

17:32:42 KBPs: theory Examples

17:32:46 KBPs: theory KBPs_Main

17:32:56 Separation_Logic_Imperative_HOL: theory Run

17:32:56 Separation_Logic_Imperative_HOL: theory Partial_Equivalence_Relation

17:32:56 Separation_Logic_Imperative_HOL: theory Assertions

17:32:58 Separation_Logic_Imperative_HOL: theory Hoare_Triple

17:32:59 Separation_Logic_Imperative_HOL: theory Automation

17:33:00 Separation_Logic_Imperative_HOL: theory Sep_Main

17:33:00 Separation_Logic_Imperative_HOL: theory Imp_List_Spec

17:33:00 Separation_Logic_Imperative_HOL: theory Imp_Map_Spec

17:33:01 Separation_Logic_Imperative_HOL: theory Imp_Set_Spec

17:33:01 Separation_Logic_Imperative_HOL: theory List_Seg

17:33:01 Separation_Logic_Imperative_HOL: theory Union_Find

17:33:02 Separation_Logic_Imperative_HOL: theory Circ_List

17:33:06 Separation_Logic_Imperative_HOL: theory Open_List

17:33:07 Separation_Logic_Imperative_HOL: theory Hash_Table

17:33:13 Separation_Logic_Imperative_HOL: theory Hash_Map

17:33:14 Separation_Logic_Imperative_HOL: theory Hash_Map_Impl

17:33:18 Separation_Logic_Imperative_HOL: theory Hash_Set_Impl

17:33:20 Timing Algebraic_Numbers (2 threads, 337.397s elapsed time, 667.592s cpu time, 96.208s GC time, factor 1.98)

17:33:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers

17:33:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf

17:33:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf

17:33:20 Finished Algebraic_Numbers (0:05:49 elapsed time, 0:11:20 cpu time, factor 1.95)

17:33:20 Running Vickrey_Clarke_Groves ...

17:33:23 Separation_Logic_Imperative_HOL: theory Idioms

17:33:23 Separation_Logic_Imperative_HOL: theory To_List_GA

17:33:24 Vickrey_Clarke_Groves: theory Argmax

17:33:24 Vickrey_Clarke_Groves: theory SetUtils

17:33:24 Vickrey_Clarke_Groves: theory Partitions

17:33:24 Timing SATSolverVerification (2 threads, 96.569s elapsed time, 187.692s cpu time, 5.176s GC time, factor 1.94)

17:33:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SATSolverVerification

17:33:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SATSolverVerification/document.pdf

17:33:24 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SATSolverVerification/outline.pdf

17:33:24 Finished SATSolverVerification (0:01:50 elapsed time, 0:03:24 cpu time, factor 1.85)

17:33:24 Running AutoFocus-Stream ...

17:33:24 Vickrey_Clarke_Groves: theory RelationOperators

17:33:25 Vickrey_Clarke_Groves: theory RelationProperties

17:33:25 Vickrey_Clarke_Groves: theory MiscTools

17:33:29 Vickrey_Clarke_Groves: theory StrictCombinatorialAuction

17:33:29 AutoFocus-Stream: theory ListSlice

17:33:29 AutoFocus-Stream: theory AF_Stream

17:33:30 Vickrey_Clarke_Groves: theory Universes

17:33:31 Vickrey_Clarke_Groves: theory UniformTieBreaking

17:33:33 Vickrey_Clarke_Groves: theory CombinatorialAuction