23:31:14 Started by upstream project "isabelle-repo" build number 937

23:31:14 originally caused by:

23:31:14 Started by an SCM change

23:31:14 [EnvInject] - Loading node environment variables.

23:31:15 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp

23:31:15 [isabelle-repo-afp] $ hg showconfig paths.default

23:31:15 [isabelle-repo-afp] $ hg pull --rev c85f677cfb0a0124197edfdc6754e87ee3620098

23:31:15 pulling from http://isabelle.in.tum.de/repos/isabelle/

23:31:15 searching for changes

23:31:15 adding changesets

23:31:15 adding manifests

23:31:15 adding file changes

23:31:15 added 13 changesets with 38 changes to 24 files

23:31:15 (run 'hg update' to get a working copy)

23:31:15 [isabelle-repo-afp] $ hg update --clean --rev c85f677cfb0a0124197edfdc6754e87ee3620098

23:31:15 24 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

23:31:16 [isabelle-repo-afp] $ hg id --branch

23:31:16 [afp] $ hg showconfig paths.default

23:31:16 [afp] $ hg pull --rev default

23:31:17 pulling from https://bitbucket.org/isa-afp/afp-devel/

23:31:17 searching for changes

23:31:17 adding changesets

23:31:17 adding manifests

23:31:17 adding file changes

23:31:17 added 2 changesets with 7 changes to 7 files

23:31:17 (run 'hg update' to get a working copy)

23:31:17 [afp] $ hg update --clean --rev default

23:31:17 366 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

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

23:31:18 No emails were triggered.

23:31:18 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson5306405377018747709.sh

23:31:18 + Admin/jenkins/run_build afp

23:31:18 + set -e

23:31:18 + PROFILE=afp

23:31:18 + shift

23:31:18 + bin/isabelle components -a

23:31:18 + bin/isabelle jedit -bf

23:31:18 ### Building Isabelle/Scala ...

23:31:44 ### Building Isabelle/jEdit ...

23:31:58 + bin/isabelle ci_build_afp

23:32:04

23:32:04 === CONFIGURATION ===

23:32:04

23:32:04 ISABELLE_BUILD_OPTIONS=""

23:32:04

23:32:04 ML_PLATFORM="x86_64-linux"

23:32:04 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

23:32:04 ML_SYSTEM="polyml-5.6"

23:32:04 ML_OPTIONS="-H 4000 --maxheap 8G"

23:32:04

23:32:04 === BUILD ===

23:32:04

23:32:04 Build started at Thu, 1 Jun 2017 21:32:03 GMT

23:32:04 Isabelle id c85f677cfb0a

23:32:04 AFP id 9ef332f7ad4c

23:32:04

23:32:04 === LOG ===

23:32:04

23:32:05 Session Pure/Pure

23:32:05 Session HOL/HOL (main)

23:32:05 Session AFP/AVL-Trees (AFP)

23:32:05 Session AFP/AWN (AFP)

23:32:05 Session AFP/Abortable_Linearizable_Modules (AFP)

23:32:05 Session AFP/Abstract-Hoare-Logics (AFP)

23:32:05 Session AFP/Allen_Calculus (AFP)

23:32:06 Session AFP/Automatic_Refinement (AFP)

23:32:06 Session AFP/Refine_Monadic (AFP)

23:32:06 Session AFP/Collections (AFP)

23:32:06 Session AFP/CAVA_Base (AFP)

23:32:06 Session AFP/CAVA_Automata (AFP)

23:32:06 Session AFP/DFS_Framework (AFP)

23:32:06 Session AFP/Gabow_SCC (AFP)

23:32:07 Session AFP/LTL_to_GBA (AFP)

23:32:07 Session AFP/CAVA_buildchain1 (AFP)

23:32:07 Session AFP/CAVA_buildchain3 (AFP)

23:32:07 Session AFP/CAVA_LTL_Modelchecker (AFP)

23:32:07 Session AFP/Promela (AFP)

23:32:07 Session AFP/Collections_Examples (AFP)

23:32:07 Session AFP/Dijkstra_Shortest_Path (AFP)

23:32:07 Session AFP/Formal_SSA (AFP)

23:32:07 Session AFP/Minimal_SSA (AFP)

23:32:07 Session AFP/Sepref_Prereq (AFP)

23:32:07 Session AFP/Refine_Imperative_HOL (AFP)

23:32:08 Session AFP/Floyd_Warshall (AFP)

23:32:08 Session AFP/Sepref_Basic (AFP)

23:32:08 Session AFP/Sepref_IICF (AFP)

23:32:08 Session AFP/EdmondsKarp_Base (AFP)

23:32:08 Session AFP/EdmondsKarp_Maxflow (AFP)

23:32:08 Session AFP/Transitive-Closure (AFP)

23:32:08 Session AFP/Tree-Automata (AFP)

23:32:08 Session AFP/BinarySearchTree (AFP)

23:32:08 Session AFP/Binomial-Queues (AFP)

23:32:08 Session AFP/Bondy (AFP)

23:32:08 Session AFP/Bounded_Deducibility_Security (AFP)

23:32:08 Session AFP/BytecodeLogicJmlTypes (AFP)

23:32:08 Session AFP/CISC-Kernel (AFP)

23:32:08 Session AFP/CYK (AFP)

23:32:08 Session AFP/Case_Labeling (AFP)

23:32:08 Session AFP/Cauchy (AFP)

23:32:08 Session AFP/Sqrt_Babylonian (AFP)

23:32:08 Session AFP/Real_Impl (AFP)

23:32:08 Session AFP/Certification_Monads (AFP)

23:32:08 Session AFP/ClockSynchInst (AFP)

23:32:09 Session AFP/Coinductive_Languages (AFP)

23:32:09 Session AFP/Compiling-Exceptions-Correctly (AFP)

23:32:09 Session AFP/Completeness (AFP)

23:32:09 Session AFP/ComponentDependencies (AFP)

23:32:09 Session AFP/Concurrent_Ref_Alg (AFP)

23:32:09 Session AFP/Consensus_Refined (AFP)

23:32:09 Session AFP/Constructor_Funs (AFP)

23:32:09 Session AFP/CryptoBasedCompositionalProperties (AFP)

23:32:09 Session AFP/DPT-SAT-Solver (AFP)

23:32:09 Session AFP/DataRefinementIBP (AFP)

23:32:09 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

23:32:09 Session AFP/Dependent_SIFUM_Refinement (AFP)

23:32:09 Session AFP/Depth-First-Search (AFP)

23:32:09 Session AFP/Dict_Construction (AFP)

23:32:09 Session AFP/DiskPaxos (AFP)

23:32:09 Session AFP/Encodability_Process_Calculi (AFP)

23:32:09 Session AFP/Euler_Partition (AFP)

23:32:09 Session AFP/Example-Submission (AFP)

23:32:09 Session AFP/FFT (AFP)

23:32:09 Session AFP/FLP (AFP)

23:32:09 Session AFP/FOL_Harrison (AFP)

23:32:09 Session AFP/FeatherweightJava (AFP)

23:32:09 Session AFP/Featherweight_OCL (AFP)

23:32:09 Session AFP/FileRefinement (AFP)

23:32:09 Session AFP/FinFun (AFP)

23:32:10 Session AFP/Finite_Automata_HF (AFP)

23:32:10 Session AFP/FocusStreamsCaseStudies (AFP)

23:32:10 Session AFP/Free-Groups (AFP)

23:32:10 Session AFP/FunWithFunctions (AFP)

23:32:10 Session AFP/FunWithTilings (AFP)

23:32:10 Session AFP/GPU_Kernel_PL (AFP)

23:32:10 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

23:32:10 Session AFP/GenClock (AFP)

23:32:10 Session AFP/General-Triangle (AFP)

23:32:10 Session AFP/GoedelGod (AFP)

23:32:10 Session AFP/GraphMarkingIBP (AFP)

23:32:10 Session HOL/HOL-Library (main timing)

23:32:10 Session AFP/Abs_Int_ITP2012 (AFP)

23:32:10 Session AFP/Abstract-Rewriting (AFP)

23:32:10 Session AFP/Decreasing-Diagrams (AFP)

23:32:10 Session AFP/Decreasing-Diagrams-II (AFP)

23:32:10 Session AFP/Matrix (AFP)

23:32:10 Session AFP/Matrix_Tensor (AFP)

23:32:11 Session AFP/Knot_Theory (AFP)

23:32:11 Session AFP/Polynomials (AFP)

23:32:11 Session AFP/Groebner_Bases (AFP)

23:32:11 Session AFP/Abstract_Completeness (AFP)

23:32:11 Session AFP/Abstract_Soundness (AFP)

23:32:11 Session AFP/Amortized_Complexity (AFP)

23:32:11 Session AFP/Dynamic_Tables (AFP)

23:32:11 Session AFP/ArrowImpossibilityGS (AFP)

23:32:11 Session AFP/Bell_Numbers_Spivey (AFP)

23:32:11 Session AFP/Card_Equiv_Relations (AFP)

23:32:11 Session AFP/Binomial-Heaps (AFP)

23:32:11 Session AFP/Boolean_Expression_Checkers (AFP)

23:32:11 Session AFP/Buildings (AFP)

23:32:11 Session AFP/Card_Multisets (AFP)

23:32:11 Session AFP/Card_Number_Partitions (AFP)

23:32:11 Session AFP/Category (AFP)

23:32:11 Session AFP/Category2 (AFP)

23:32:11 Session AFP/Category3 (AFP)

23:32:11 Session AFP/MonoidalCategory (AFP)

23:32:11 Session AFP/CofGroups (AFP)

23:32:11 Session AFP/ConcurrentIMP (AFP)

23:32:11 Session AFP/CoreC++ (AFP)

23:32:11 Session AFP/Datatype_Order_Generator (AFP)

23:32:12 Session AFP/Old_Datatype_Show (AFP)

23:32:12 Session AFP/Derangements (AFP)

23:32:12 Session AFP/Deriving (AFP)

23:32:12 Session AFP/Containers (AFP)

23:32:12 Session AFP/Containers-Benchmarks (AFP)

23:32:13 Session AFP/Show (AFP)

23:32:13 Session AFP/Discrete_Summation (AFP)

23:32:13 Session AFP/Card_Partitions (AFP)

23:32:13 Session AFP/Efficient-Mergesort (AFP)

23:32:13 Session AFP/FOL-Fitting (AFP)

23:32:13 Session AFP/Finger-Trees (AFP)

23:32:13 Session AFP/Formula_Derivatives (AFP)

23:32:13 Session AFP/Formula_Derivatives-Examples (AFP)

23:32:13 Session AFP/Free-Boolean-Algebra (AFP)

23:32:13 Session AFP/Functional-Automata (AFP)

23:32:13 Session AFP/Graph_Theory (AFP)

23:32:13 Session AFP/ShortestPath (AFP)

23:32:13 Session AFP/Group-Ring-Module (AFP)

23:32:13 Session AFP/Valuation (AFP)

23:32:13 Session HOL/HOL-Cardinals (timing)

23:32:13 Session AFP/Ordinals_and_Cardinals (AFP)

23:32:13 Session AFP/Sort_Encodings (AFP)

23:32:13 Session HOL/HOL-Computational_Algebra (timing)

23:32:13 Session AFP/Bernoulli (AFP)

23:32:13 Session AFP/Coinductive (AFP)

23:32:14 Session AFP/Lazy-Lists-II (AFP)

23:32:14 Session AFP/Topology (AFP)

23:32:14 Session AFP/Stream_Fusion_Code (AFP)

23:32:14 Session AFP/Descartes_Sign_Rule (AFP)

23:32:14 Session HOL/HOL-Algebra (main timing)

23:32:14 Session AFP/JNF-HOL-Lib (AFP)

23:32:14 Session AFP/JNF-AFP-Lib (AFP)

23:32:14 Session AFP/Jordan_Normal_Form (AFP)

23:32:14 Session AFP/Pre_Perron_Frobenius (AFP)

23:32:14 Session AFP/Perron_Frobenius (AFP)

23:32:14 Session AFP/Subresultants (AFP)

23:32:14 Session AFP/Pre_BZ (AFP)

23:32:15 Session AFP/Berlekamp_Zassenhaus (AFP)

23:32:15 Session AFP/Pre_Algebraic_Numbers (AFP)

23:32:15 Session AFP/Algebraic_Numbers (AFP)

23:32:15 Session AFP/Algebraic_Numbers_Lib (AFP)

23:32:15 Session AFP/Pre_Polynomial_Factorization (AFP)

23:32:15 Session AFP/Polynomial_Factorization (AFP)

23:32:15 Session AFP/Jordan_Hoelder (AFP)

23:32:15 Session AFP/Perfect-Number-Thm (AFP)

23:32:15 Session AFP/Secondary_Sylow (AFP)

23:32:15 Session AFP/VectorSpace (AFP)

23:32:15 Session HOL/HOL-Analysis (main timing)

23:32:16 Session AFP/Affine_Arithmetic (AFP)

23:32:16 Session AFP/Cartan_FP (AFP)

23:32:16 Session AFP/Cayley_Hamilton (AFP)

23:32:16 Session AFP/Chord_Segments (AFP)

23:32:16 Session AFP/Echelon_Form (AFP)

23:32:16 Session AFP/Hermite (AFP)

23:32:16 Session AFP/Gauss_Jordan (AFP)

23:32:16 Session HOL/HOL-Probability (main timing)

23:32:16 Session AFP/Applicative_Lifting (AFP)

23:32:16 Session AFP/Stern_Brocot (AFP)

23:32:16 Session AFP/Deep_Learning_Lib (AFP)

23:32:16 Session AFP/Deep_Learning (AFP)

23:32:16 Session AFP/Density_Compiler (AFP)

23:32:17 Session AFP/Ergodic_Theory (AFP)

23:32:17 Session AFP/Fisher_Yates (AFP)

23:32:17 Session AFP/Girth_Chromatic (AFP)

23:32:17 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

23:32:17 Session AFP/List_Update (AFP)

23:32:17 Session AFP/Lp (AFP)

23:32:17 Session AFP/MFMC_Countable (AFP)

23:32:17 Session AFP/Markov_Models (AFP)

23:32:17 Session AFP/Monad_Normalisation (AFP)

23:32:17 Session AFP/Monomorphic_Monad (AFP)

23:32:17 Session AFP/Probabilistic_Noninterference (AFP)

23:32:17 Session AFP/Probabilistic_System_Zoo (AFP)

23:32:17 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

23:32:18 Session AFP/Probabilistic_While (AFP)

23:32:18 Session AFP/CryptHOL (AFP)

23:32:18 Session AFP/Game_Based_Crypto (AFP)

23:32:18 Session AFP/Quick_Sort_Cost (AFP)

23:32:18 Session AFP/Random_BSTs (AFP)

23:32:18 Session AFP/Randomised_Social_Choice (AFP)

23:32:18 Session AFP/SDS_Impossibility (AFP)

23:32:18 Session AFP/Source_Coding_Theorem (AFP)

23:32:18 Session AFP/UpDown_Scheme (AFP)

23:32:18 Session AFP/Landau_Analysis (AFP)

23:32:18 Session AFP/Akra_Bazzi (AFP)

23:32:19 Session AFP/Catalan_Numbers (AFP)

23:32:19 Session AFP/Euler_MacLaurin (AFP)

23:32:19 Session AFP/Stirling_Formula (AFP)

23:32:19 Session AFP/Comparison_Sort_Lower_Bound (AFP)

23:32:19 Session AFP/Lower_Semicontinuous (AFP)

23:32:19 Session AFP/Ordinary_Differential_Equations (AFP)

23:32:19 Session AFP/HOL-ODE (AFP)

23:32:19 Session AFP/Differential_Dynamic_Logic (AFP)

23:32:19 Session AFP/HOL-ODE-Refinement (AFP)

23:32:19 Session AFP/HOL-ODE-Numerics (AFP)

23:32:20 Session AFP/Prime_Harmonic_Series (AFP)

23:32:20 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

23:32:20 Session AFP/Ptolemys_Theorem (AFP)

23:32:20 Session AFP/QR_Decomposition (AFP)

23:32:20 Session AFP/Rank_Nullity_Theorem (AFP)

23:32:20 Session AFP/Tarskis_Geometry (AFP)

23:32:20 Session AFP/Triangle (AFP)

23:32:20 Session AFP/pGCL (AFP)

23:32:20 Session HOL/HOL-Number_Theory (timing)

23:32:20 Session AFP/E_Transcendental (AFP)

23:32:20 Session AFP/Elliptic_Curves_Group_Law (AFP)

23:32:20 Session AFP/Fermat3_4 (AFP)

23:32:20 Session AFP/Koenigsberg_Friendship_Base (AFP)

23:32:20 Session AFP/Koenigsberg_Friendship (AFP)

23:32:21 Session AFP/Lehmer (AFP)

23:32:21 Session AFP/Pratt_Certificate (AFP)

23:32:21 Session AFP/Bertrands_Postulate (AFP)

23:32:21 Session AFP/SumSquares (AFP)

23:32:21 Session AFP/Liouville_Numbers (AFP)

23:32:21 Session AFP/Polynomial_Interpolation (AFP)

23:32:21 Session AFP/RSAPSS (AFP)

23:32:21 Session AFP/Rep_Fin_Groups (AFP)

23:32:21 Session AFP/Sturm_Sequences (AFP)

23:32:21 Session AFP/Special_Function_Bounds (AFP)

23:32:21 Session AFP/Sturm_Tarski (AFP)

23:32:21 Session HOL/HOL-Imperative_HOL

23:32:21 Session AFP/Imperative_Insertion_Sort (AFP)

23:32:21 Session AFP/HereditarilyFinite (AFP)

23:32:21 Session AFP/Incompleteness (AFP)

23:32:21 Session AFP/Surprise_Paradox (AFP)

23:32:21 Session AFP/HyperCTL (AFP)

23:32:21 Session AFP/Incredible_Proof_Machine (AFP)

23:32:22 Session AFP/Integration (AFP)

23:32:22 Session AFP/Isabelle_Meta_Model (AFP)

23:32:22 Session AFP/Jinja (AFP)

23:32:22 Session AFP/HRB-Slicing (AFP)

23:32:22 Session AFP/InformationFlowSlicing_Inter (AFP)

23:32:22 Session AFP/Slicing (AFP)

23:32:22 Session AFP/InformationFlowSlicing (AFP)

23:32:22 Session AFP/KBPs (AFP)

23:32:22 Session AFP/LTL (AFP)

23:32:22 Session AFP/LTL_to_DRA (AFP)

23:32:22 Session AFP/Stuttering_Equivalence (AFP)

23:32:22 Session AFP/Lambda_Free_RPOs (AFP)

23:32:22 Session AFP/Landau_Symbols (AFP)

23:32:22 Session AFP/LightweightJava (AFP)

23:32:22 Session AFP/LinearQuantifierElim (AFP)

23:32:22 Session AFP/List-Infinite (AFP)

23:32:22 Session AFP/Nat-Interval-Logic (AFP)

23:32:22 Session AFP/AutoFocus-Stream (AFP)

23:32:22 Session AFP/MSO_Regex_Equivalence (AFP)

23:32:23 Session AFP/MSO_Examples (AFP)

23:32:23 Session AFP/MuchAdoAboutTwo (AFP)

23:32:23 Session AFP/Myhill-Nerode (AFP)

23:32:23 Session AFP/POPLmark-deBruijn (AFP)

23:32:23 Session AFP/Pairing_Heap (AFP)

23:32:23 Session AFP/Password_Authentication_Protocol (AFP)

23:32:23 Session AFP/Presburger-Automata (AFP)

23:32:23 Session AFP/Priority_Queue_Braun (AFP)

23:32:23 Session AFP/Program-Conflict-Analysis (AFP)

23:32:23 Session AFP/Regex_Equivalence (AFP)

23:32:23 Session AFP/Regex_Equivalence_Examples (AFP)

23:32:23 Session AFP/Regular-Sets (AFP)

23:32:23 Session AFP/Posix-Lexing (AFP)

23:32:23 Session AFP/Ribbon_Proofs (AFP)

23:32:23 Session AFP/SATSolverVerification (AFP)

23:32:23 Session AFP/Selection_Heap_Sort (AFP)

23:32:23 Session AFP/Separata (AFP)

23:32:23 Session AFP/Separation_Logic_Imperative_HOL (AFP)

23:32:23 Session AFP/Skew_Heap (AFP)

23:32:24 Session AFP/Splay_Tree (AFP)

23:32:24 Session AFP/Stable_Matching (AFP)

23:32:24 Session AFP/SuperCalc (AFP)

23:32:24 Session AFP/Tail_Recursive_Functions (AFP)

23:32:24 Session AFP/TortoiseHare (AFP)

23:32:24 Session AFP/Trie (AFP)

23:32:24 Session AFP/Twelvefold_Way (AFP)

23:32:24 Session AFP/Vickrey_Clarke_Groves (AFP)

23:32:24 Session AFP/Well_Quasi_Orders (AFP)

23:32:24 Session AFP/XML (AFP)

23:32:24 Session HOL/HOL-Nominal

23:32:24 Session AFP/CCS (AFP)

23:32:24 Session AFP/Lam-ml-Normalization (AFP)

23:32:24 Session AFP/Pi_Calculus (AFP)

23:32:24 Session AFP/Psi_Calculi (AFP)

23:32:25 Session AFP/SequentInvertibility (AFP)

23:32:25 Session HOL/HOL-Word (main timing)

23:32:25 Session HOL/HOL-SPARK (main)

23:32:25 Session HOL/HOL-SPARK-Examples

23:32:25 Session AFP/RIPEMD-160-SPARK (AFP)

23:32:25 Session AFP/Kleene_Algebra (AFP)

23:32:25 Session AFP/KAT_and_DRA (AFP)

23:32:25 Session AFP/Algebraic_VCs (AFP)

23:32:25 Session AFP/Multirelations (AFP)

23:32:25 Session AFP/Regular_Algebras (AFP)

23:32:25 Session AFP/Relation_Algebra (AFP)

23:32:25 Session AFP/Residuated_Lattices (AFP)

23:32:25 Session AFP/Native_Word (AFP)

23:32:26 Session AFP/SPARCv8 (AFP)

23:32:26 Session AFP/Separation_Algebra (AFP)

23:32:26 Session AFP/Word_Lib (AFP)

23:32:26 Session AFP/Complx (AFP)

23:32:26 Session AFP/IP_Addresses (AFP)

23:32:26 Session AFP/Simple_Firewall (AFP)

23:32:26 Session AFP/Routing (AFP)

23:32:26 Session AFP/Iptables_Semantics (AFP)

23:32:26 Session AFP/LOFT (AFP)

23:32:26 Session HOL/HOLCF (main timing)

23:32:26 Session AFP/Circus (AFP)

23:32:27 Session AFP/HOLCF-HOL-Library (AFP)

23:32:27 Session AFP/HOLCF-Nominal2 (AFP)

23:32:27 Session AFP/Launchbury (AFP)

23:32:27 Session AFP/Call_Arity (AFP)

23:32:27 Session HOL/HOLCF-Library

23:32:27 Session AFP/PCF (AFP)

23:32:27 Session AFP/Shivers-CFA (AFP)

23:32:27 Session AFP/Stream-Fusion (AFP)

23:32:27 Session AFP/Tycon (AFP)

23:32:27 Session AFP/WorkerWrapper (AFP)

23:32:27 Session AFP/Heard_Of (AFP)

23:32:27 Session AFP/HotelKeyCards (AFP)

23:32:27 Session AFP/Huffman (AFP)

23:32:27 Session AFP/IEEE_Floating_Point (AFP)

23:32:27 Session AFP/Impossible_Geometry (AFP)

23:32:27 Session AFP/Inductive_Confidentiality (AFP)

23:32:27 Session AFP/InfPathElimination (AFP)

23:32:27 Session AFP/JiveDataStoreModel (AFP)

23:32:28 Session AFP/KAD (AFP)

23:32:28 Session AFP/Key_Agreement_Strong_Adversaries (AFP)

23:32:28 Session AFP/LatticeProperties (AFP)

23:32:28 Session AFP/MonoBoolTranAlgebra (AFP)

23:32:28 Session AFP/PseudoHoops (AFP)

23:32:28 Session AFP/Lazy_Case (AFP)

23:32:28 Session AFP/Lifting_Definition_Option (AFP)

23:32:28 Session AFP/List-Index (AFP)

23:32:28 Session AFP/List_Interleaving (AFP)

23:32:28 Session AFP/Locally-Nameless-Sigma (AFP)

23:32:28 Session Doc/Main (doc)

23:32:28 Session AFP/LocalLexing (AFP)

23:32:28 Session AFP/Marriage (AFP)

23:32:28 Session AFP/Latin_Square (AFP)

23:32:28 Session AFP/Max-Card-Matching (AFP)

23:32:28 Session AFP/Menger (AFP)

23:32:28 Session AFP/MiniML (AFP)

23:32:28 Session AFP/Network_Security_Policy_Verification (AFP)

23:32:28 Session AFP/No_FTL_observers (AFP)

23:32:28 Session AFP/Nominal2 (AFP)

23:32:28 Session AFP/Modal_Logics_for_NTS (AFP)

23:32:28 Session AFP/Rewriting_Z (AFP)

23:32:28 Session AFP/Noninterference_CSP (AFP)

23:32:28 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

23:32:28 Session AFP/Noninterference_Generic_Unwinding (AFP)

23:32:29 Session AFP/Noninterference_Inductive_Unwinding (AFP)

23:32:29 Session AFP/Noninterference_Sequential_Composition (AFP)

23:32:29 Session AFP/Noninterference_Concurrent_Composition (AFP)

23:32:29 Session AFP/NormByEval (AFP)

23:32:29 Session AFP/Open_Induction (AFP)

23:32:29 Session AFP/Ordinal (AFP)

23:32:29 Session AFP/Nested_Multisets_Ordinals (AFP)

23:32:29 Session AFP/Lambda_Free_KBOs (AFP)

23:32:29 Session AFP/Paraconsistency (AFP)

23:32:29 Session AFP/Parity_Game (AFP)

23:32:29 Session AFP/Partial_Function_MR (AFP)

23:32:29 Session AFP/Pop_Refinement (AFP)

23:32:29 Session AFP/Possibilistic_Noninterference (AFP)

23:32:29 Session AFP/Proof_Strategy_Language (AFP)

23:32:29 Session AFP/PropResPI (AFP)

23:32:29 Session AFP/ROBDD (AFP)

23:32:30 Session AFP/Ramsey-Infinite (AFP)

23:32:30 Session AFP/Recursion-Theory-I (AFP)

23:32:30 Session AFP/RefinementReactive (AFP)

23:32:30 Session AFP/Resolution_FOL (AFP)

23:32:30 Session AFP/Robbins-Conjecture (AFP)

23:32:30 Session AFP/Roy_Floyd_Warshall (AFP)

23:32:30 Session AFP/SIFPL (AFP)

23:32:30 Session AFP/SIFUM_Type_Systems (AFP)

23:32:30 Session AFP/SenSocialChoice (AFP)

23:32:30 Session AFP/Simpl (AFP)

23:32:30 Session AFP/BDD (AFP)

23:32:30 Session AFP/Planarity_Certificates (AFP)

23:32:30 Session AFP/Statecharts (AFP)

23:32:30 Session AFP/Stone_Algebras (AFP)

23:32:30 Session AFP/Stone_Relation_Algebras (AFP)

23:32:30 Session AFP/Strong_Security (AFP)

23:32:30 Session AFP/TLA (AFP)

23:32:30 Session AFP/Timed_Automata (AFP)

23:32:31 Session AFP/Transitive-Closure-II (AFP)

23:32:31 Session AFP/Tree_Decomposition (AFP)

23:32:31 Session AFP/Types_Tableaus_and_Goedels_God (AFP)

23:32:31 Session AFP/UPF (AFP)

23:32:31 Session AFP/UPF_Firewall (AFP)

23:32:31 Session AFP/Verified-Prover (AFP)

23:32:31 Session AFP/VolpanoSmith (AFP)

23:32:31 Session AFP/WHATandWHERE_Security (AFP)

23:32:34 Building Pure ...

23:32:47 Pure: theory Pure

23:32:48 Pure: theory ML_Bootstrap

23:32:51 Warning: missing document directory

23:32:51 Timing Pure (1 threads, 0.577s elapsed time, 0.580s cpu time, 0.000s GC time, factor 1.00)

23:32:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/Pure/Pure

23:32:51 Finished Pure (0:00:16 elapsed time, 0:00:15 cpu time, factor 1.00)

23:32:51 Building HOL ...

23:32:52 HOL: theory HOL.Code_Generator

23:32:55 HOL: theory HOL.HOL

23:32:59 HOL: theory HOL.Argo

23:32:59 HOL: theory HOL.Ctr_Sugar

23:32:59 HOL: theory HOL.Orderings

23:33:00 HOL: theory HOL.SAT

23:33:01 HOL: theory HOL.Groups

23:33:04 HOL: theory HOL.Lattices

23:33:06 HOL: theory HOL.Set

23:33:07 HOL: theory HOL.Fun

23:33:08 HOL: theory HOL.Typedef

23:33:08 HOL: theory HOL.Rings

23:33:08 HOL: theory HOL.Complete_Lattices

23:33:11 HOL: theory HOL.Inductive

23:33:13 HOL: theory HOL.Product_Type

23:33:14 HOL: theory HOL.Complete_Partial_Order

23:33:14 HOL: theory HOL.Sum_Type

23:33:19 HOL: theory HOL.Nat

23:33:20 HOL: theory HOL.Fields

23:33:21 HOL: theory HOL.Meson

23:33:21 HOL: theory HOL.ATP

23:33:23 HOL: theory HOL.Metis

23:33:26 HOL: theory HOL.Finite_Set

23:33:27 HOL: theory HOL.Relation

23:33:28 HOL: theory HOL.Transitive_Closure

23:33:29 HOL: theory HOL.Wellfounded

23:33:30 HOL: theory HOL.Fun_Def_Base

23:33:30 HOL: theory HOL.Hilbert_Choice

23:33:30 HOL: theory HOL.Wfrec

23:33:30 HOL: theory HOL.Order_Relation

23:33:30 HOL: theory HOL.BNF_Wellorder_Relation

23:33:30 HOL: theory HOL.Zorn

23:33:31 HOL: theory HOL.BNF_Wellorder_Embedding

23:33:31 HOL: theory HOL.BNF_Wellorder_Constructions

23:33:32 HOL: theory HOL.BNF_Cardinal_Order_Relation

23:33:32 HOL: theory HOL.BNF_Cardinal_Arithmetic

23:33:33 HOL: theory HOL.BNF_Def

23:33:35 HOL: theory HOL.BNF_Composition

23:33:36 HOL: theory HOL.Basic_BNFs

23:33:36 HOL: theory HOL.BNF_Fixpoint_Base

23:33:39 HOL: theory HOL.BNF_Least_Fixpoint

23:33:41 HOL: theory HOL.Basic_BNF_LFPs

23:33:41 HOL: theory HOL.Transfer

23:33:42 HOL: theory HOL.Num

23:33:45 HOL: theory HOL.Power

23:33:48 HOL: theory HOL.Groups_Big

23:33:50 HOL: theory HOL.Equiv_Relations

23:33:50 HOL: theory HOL.Lifting

23:33:52 HOL: theory HOL.Lifting_Set

23:33:52 HOL: theory HOL.Option

23:33:53 HOL: theory HOL.Extraction

23:33:54 HOL: theory HOL.Lattices_Big

23:33:55 HOL: theory HOL.Partial_Function

23:33:56 HOL: theory HOL.Fun_Def

23:33:56 HOL: theory HOL.Quotient

23:33:57 HOL: theory HOL.Int

23:34:00 HOL: theory HOL.Nat_Transfer

23:34:01 HOL: theory HOL.Euclidean_Division

23:34:05 HOL: theory HOL.Parity

23:34:07 HOL: theory HOL.Divides

23:34:14 HOL: theory HOL.Code_Numeral

23:34:14 HOL: theory HOL.Numeral_Simprocs

23:34:15 HOL: theory HOL.SMT

23:34:15 HOL: theory HOL.Semiring_Normalization

23:34:17 HOL: theory HOL.Set_Interval

23:34:17 HOL: theory HOL.Groebner_Basis

23:34:20 HOL: theory HOL.Conditionally_Complete_Lattices

23:34:20 HOL: theory HOL.Filter

23:34:21 HOL: theory HOL.Presburger

23:34:23 HOL: theory HOL.Sledgehammer

23:34:25 HOL: theory HOL.List

23:34:33 HOL: theory HOL.Groups_List

23:34:33 HOL: theory HOL.Map

23:34:34 HOL: theory HOL.Factorial

23:34:34 HOL: theory HOL.GCD

23:34:35 HOL: theory HOL.Binomial

23:34:35 HOL: theory HOL.Enum

23:34:38 HOL: theory HOL.String

23:34:38 HOL: theory HOL.BNF_Greatest_Fixpoint

23:34:41 HOL: theory HOL.Predicate

23:34:42 HOL: theory HOL.Lazy_Sequence

23:34:43 HOL: theory HOL.Typerep

23:34:43 HOL: theory HOL.Limited_Sequence

23:34:43 HOL: theory HOL.Random

23:34:43 HOL: theory HOL.Code_Evaluation

23:34:45 HOL: theory HOL.Quickcheck_Random

23:34:47 HOL: theory HOL.Quickcheck_Exhaustive

23:34:47 HOL: theory HOL.Quickcheck_Narrowing

23:34:51 HOL: theory HOL.Random_Pred

23:34:52 HOL: theory HOL.Record

23:34:52 HOL: theory HOL.Random_Sequence

23:34:53 HOL: theory HOL.Predicate_Compile

23:34:53 HOL: theory HOL.Nitpick

23:34:59 HOL: theory Main

23:35:01 HOL: theory HOL.Archimedean_Field

23:35:01 HOL: theory HOL.Topological_Spaces

23:35:06 HOL: theory HOL.Rat

23:35:08 HOL: theory HOL.Real

23:35:10 HOL: theory HOL.Real_Vector_Spaces

23:35:22 HOL: theory HOL.Inequalities

23:35:22 HOL: theory HOL.Limits

23:35:25 HOL: theory HOL.Deriv

23:35:25 HOL: theory HOL.Series

23:35:27 HOL: theory HOL.NthRoot

23:35:28 HOL: theory HOL.Transcendental

23:35:32 HOL: theory HOL.Complex

23:35:32 HOL: theory HOL.MacLaurin

23:35:34 HOL: theory Complex_Main

23:38:34 Timing HOL (2 threads, 249.181s elapsed time, 472.940s cpu time, 45.004s GC time, factor 1.90)

23:38:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL

23:38:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/document.pdf

23:38:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/outline.pdf

23:38:34 Finished HOL (0:05:42 elapsed time, 0:10:23 cpu time, factor 1.82)

23:38:36 Building HOL-Library ...

23:38:37 Building HOLCF ...

23:38:37 Building HOL-Word ...

23:38:37 Building HOL-Nominal ...

23:38:37 Building Simpl ...

23:38:37 Building Nominal2 ...

23:38:37 Building LatticeProperties ...

23:38:37 Building Dependent_SIFUM_Type_Systems ...

23:38:39 HOLCF: theory HOLCF.Old_Datatype

23:38:39 HOLCF: theory HOLCF.Nat_Bijection

23:38:39 HOL-Nominal: theory HOL-Nominal.Infinite_Set

23:38:39 HOL-Nominal: theory HOL-Nominal.Old_Datatype

23:38:39 LatticeProperties: theory LatticeProperties.Conj_Disj

23:38:39 LatticeProperties: theory LatticeProperties.Lattice_Prop

23:38:39 HOL-Word: theory HOL-Word.Bit

23:38:39 HOL-Word: theory HOL-Word.Bits

23:38:39 Nominal2: theory Nominal2.FSet

23:38:39 Nominal2: theory Nominal2.Infinite_Set

23:38:39 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Preliminaries

23:38:39 HOL-Word: theory HOL-Word.Boolean_Algebra

23:38:39 LatticeProperties: theory LatticeProperties.WellFoundedTransitive

23:38:39 Simpl: theory Simpl.DistinctTreeProver

23:38:39 Simpl: theory Simpl.Cancellation

23:38:39 HOL-Library: theory HOL-Library.Adhoc_Overloading

23:38:39 HOL-Library: theory HOL-Library.Preorder

23:38:40 HOL-Library: theory HOL-Library.Lattice_Syntax

23:38:40 HOL-Library: theory HOL-Library.AList

23:38:40 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice

23:38:40 HOL-Library: theory HOL-Library.BNF_Axiomatization

23:38:40 Nominal2: theory Nominal2.Old_Datatype

23:38:40 HOL-Library: theory HOL-Library.BNF_Corec

23:38:40 HOL-Word: theory HOL-Word.Misc_Numeric

23:38:40 HOL-Word: theory HOL-Word.Bits_Bit

23:38:40 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop

23:38:40 HOL-Word: theory HOL-Word.Bit_Representation

23:38:40 Simpl: theory Simpl.Multiset

23:38:40 HOL-Word: theory HOL-Word.Word_Miscellaneous

23:38:41 HOLCF: theory HOLCF.Countable

23:38:41 HOL-Word: theory HOL-Word.Bits_Int

23:38:41 HOL-Word: theory HOL-Word.Misc_Typedef

23:38:41 HOL-Nominal: theory HOL-Nominal.Nominal

23:38:41 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Language

23:38:41 HOL-Word: theory HOL-Word.Phantom_Type

23:38:41 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Security

23:38:41 Simpl: theory Simpl.Generalise

23:38:41 Nominal2: theory Nominal2.Phantom_Type

23:38:41 HOL-Library: theory HOL-Library.DAList

23:38:41 Simpl: theory Simpl.StateFun

23:38:42 Simpl: theory Simpl.StateSpaceLocale

23:38:42 Simpl: theory Simpl.StateSpaceSyntax

23:38:42 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group

23:38:42 Nominal2: theory Nominal2.Cardinality

23:38:42 HOL-Word: theory HOL-Word.Cardinality

23:38:42 Simpl: theory Simpl.LaTeXsugar

23:38:42 Simpl: theory Simpl.Old_Recdef

23:38:42 HOLCF: theory HOLCF.Porder

23:38:42 HOL-Word: theory HOL-Word.Bool_List_Representation

23:38:43 HOL-Library: theory HOL-Library.Bit

23:38:43 HOLCF: theory HOLCF.Pcpo

23:38:43 HOL-Word: theory HOL-Word.Numeral_Type

23:38:43 Nominal2: theory Nominal2.FinFun

23:38:43 Simpl: theory Simpl.Language

23:38:43 HOL-Library: theory HOL-Library.Boolean_Algebra

23:38:44 HOL-Library: theory HOL-Library.Cancellation

23:38:44 HOL-Word: theory HOL-Word.Type_Length

23:38:44 HOLCF: theory HOLCF.Cont

23:38:45 HOL-Word: theory HOL-Word.Word

23:38:45 HOL-Library: theory HOL-Library.Multiset

23:38:45 HOLCF: theory HOLCF.Adm

23:38:45 HOLCF: theory HOLCF.Discrete

23:38:45 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Compositionality

23:38:45 HOLCF: theory HOLCF.Cpodef

23:38:46 HOLCF: theory HOLCF.Fun_Cpo

23:38:46 HOLCF: theory HOLCF.Product_Cpo

23:38:46 Simpl: theory Simpl.Permutation

23:38:46 Simpl: theory Simpl.Simpl_Heap

23:38:46 HOLCF: theory HOLCF.Cfun

23:38:46 Simpl: theory Simpl.HeapList

23:38:46 HOL-Library: theory HOL-Library.Cardinal_Notations

23:38:46 HOL-Library: theory HOL-Library.Char_ord

23:38:46 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.LocallySoundModeUse

23:38:47 HOL-Library: theory HOL-Library.Code_Abstract_Nat

23:38:47 HOL-Library: theory HOL-Library.Code_Binary_Nat

23:38:47 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystem

23:38:47 HOL-Library: theory HOL-Library.Code_Target_Nat

23:38:47 HOLCF: theory HOLCF.Completion

23:38:47 HOLCF: theory HOLCF.Cprod

23:38:47 HOLCF: theory HOLCF.Deflation

23:38:48 HOL-Library: theory HOL-Library.Code_Char

23:38:48 HOLCF: theory HOLCF.Fix

23:38:48 HOLCF: theory HOLCF.Sfun

23:38:48 HOL-Library: theory HOL-Library.Code_Prolog

23:38:48 HOLCF: theory HOLCF.Sprod

23:38:48 HOLCF: theory HOLCF.Up

23:38:48 HOL-Library: theory HOL-Library.Code_Target_Int

23:38:48 HOL-Library: theory HOL-Library.Code_Target_Numeral

23:38:48 HOL-Library: theory HOL-Library.Code_Test

23:38:49 HOLCF: theory HOLCF.Lift

23:38:49 HOLCF: theory HOLCF.One

23:38:49 HOLCF: theory HOLCF.Tr

23:38:49 HOL-Library: theory HOL-Library.Combine_PER

23:38:49 HOLCF: theory HOLCF.Ssum

23:38:50 HOL-Library: theory HOL-Library.Complete_Partial_Order2

23:38:50 HOL-Library: theory HOL-Library.DAList_Multiset

23:38:50 HOLCF: theory HOLCF.Fixrec

23:38:50 HOLCF: theory HOLCF.Map_Functions

23:38:51 HOL-Library: theory HOL-Library.Multiset_Order

23:38:51 HOL-Library: theory HOL-Library.Permutation

23:38:51 HOLCF: theory HOLCF.Bifinite

23:38:51 HOL-Library: theory HOL-Library.Debug

23:38:51 HOLCF: theory HOLCF.Domain_Aux

23:38:51 HOL-Library: theory HOL-Library.Disjoint_Sets

23:38:52 HOL-Library: theory HOL-Library.Permutations

23:38:52 Simpl: theory Simpl.Semantic

23:38:52 HOLCF: theory HOLCF.Universal

23:38:53 HOL-Library: theory HOL-Library.Dlist

23:38:53 Nominal2: theory Nominal2.Cancellation

23:38:53 Nominal2: theory Nominal2.Quotient_Syntax

23:38:53 Nominal2: theory Nominal2.Quotient_Option

23:38:53 HOL-Library: theory HOL-Library.FSet

23:38:53 Nominal2: theory Nominal2.Quotient_Product

23:38:54 Nominal2: theory Nominal2.Quotient_Set

23:38:54 HOLCF: theory HOLCF.Algebraic

23:38:54 HOLCF: theory HOLCF.Compact_Basis

23:38:54 Nominal2: theory Nominal2.Quotient_List

23:38:54 Nominal2: theory Nominal2.Multiset

23:38:54 HOLCF: theory HOLCF.LowerPD

23:38:54 HOL-Library: theory HOL-Library.Fun_Lexorder

23:38:54 HOLCF: theory HOLCF.UpperPD

23:38:54 HOL-Library: theory HOL-Library.FuncSet

23:38:55 HOL-Library: theory HOL-Library.Function_Algebras

23:38:55 HOLCF: theory HOLCF.Representable

23:38:55 HOLCF: theory HOLCF.ConvexPD

23:38:55 HOL-Library: theory HOL-Library.Function_Division

23:38:55 HOL-Library: theory HOL-Library.Groups_Big_Fun

23:38:56 HOL-Library: theory HOL-Library.IArray

23:38:56 Simpl: theory Simpl.HoarePartialDef

23:38:56 Simpl: theory Simpl.Termination

23:38:57 Simpl: theory Simpl.HoarePartialProps

23:38:57 Simpl: theory Simpl.HoareTotalDef

23:38:57 HOL-Library: theory HOL-Library.Infinite_Set

23:38:57 HOL-Library: theory HOL-Library.Finite_Map

23:38:58 HOL-Library: theory HOL-Library.Omega_Words_Fun

23:38:58 HOL-Library: theory HOL-Library.Ramsey

23:38:58 Simpl: theory Simpl.AlternativeSmallStep

23:38:58 Simpl: theory Simpl.HoarePartial

23:38:58 HOL-Library: theory HOL-Library.LaTeXsugar

23:38:58 HOLCF: theory HOLCF.Domain

23:38:58 HOL-Library: theory HOL-Library.Lattice_Constructions

23:38:59 Nominal2: theory Nominal2.Nominal2_Base

23:38:59 Simpl: theory Simpl.SmallStep

23:39:00 HOL-Library: theory HOL-Library.ListVector

23:39:00 Timing LatticeProperties (2 threads, 3.992s elapsed time, 7.344s cpu time, 0.172s GC time, factor 1.84)

23:39:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties

23:39:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties/document.pdf

23:39:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties/outline.pdf

23:39:00 Finished LatticeProperties (0:00:22 elapsed time, 0:00:33 cpu time, factor 1.52)

23:39:00 Building Automatic_Refinement ...

23:39:00 HOLCF: theory HOLCF.Powerdomains

23:39:00 HOL-Library: theory HOL-Library.List_lexord

23:39:00 HOL-Library: theory HOL-Library.Mapping

23:39:01 HOLCF: theory HOLCF

23:39:01 HOL-Library: theory HOL-Library.AList_Mapping

23:39:01 Simpl: theory Simpl.HoareTotalProps

23:39:01 HOL-Library: theory HOL-Library.Monad_Syntax

23:39:02 HOL-Library: theory HOL-Library.More_List

23:39:02 HOL-Library: theory HOL-Library.Nat_Bijection

23:39:02 Automatic_Refinement: theory Automatic_Refinement.Cancellation

23:39:02 Automatic_Refinement: theory Automatic_Refinement.Foldi

23:39:02 Automatic_Refinement: theory Automatic_Refinement.Infinite_Set

23:39:02 HOL-Library: theory HOL-Library.Old_Datatype

23:39:02 HOL-Library: theory HOL-Library.Stream

23:39:03 Automatic_Refinement: theory Automatic_Refinement.Multiset

23:39:03 Automatic_Refinement: theory Automatic_Refinement.Omega_Words_Fun

23:39:03 Simpl: theory Simpl.Compose

23:39:03 Simpl: theory Simpl.HoareTotal

23:39:03 Automatic_Refinement: theory Automatic_Refinement.Option_ord

23:39:03 HOL-Library: theory HOL-Library.Old_Recdef

23:39:04 HOL-Library: theory HOL-Library.Option_ord

23:39:04 Automatic_Refinement: theory Automatic_Refinement.Prio_List

23:39:04 Automatic_Refinement: theory Automatic_Refinement.Refine_Util

23:39:04 HOL-Library: theory HOL-Library.Parallel

23:39:04 HOL-Library: theory HOL-Library.Perm

23:39:04 Simpl: theory Simpl.Hoare

23:39:04 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification

23:39:04 Timing HOL-Nominal (2 threads, 8.751s elapsed time, 17.268s cpu time, 0.904s GC time, factor 1.97)

23:39:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Nominal

23:39:04 Finished HOL-Nominal (0:00:26 elapsed time, 0:00:44 cpu time, factor 1.64)

23:39:04 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb

23:39:04 Nominal2: theory Nominal2.Atoms

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms

23:39:05 Nominal2: theory Nominal2.Eqvt

23:39:05 Simpl: theory Simpl.Closure

23:39:05 Building Stone_Algebras ...

23:39:05 Simpl: theory Simpl.StateSpace

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot

23:39:05 Nominal2: theory Nominal2.Nominal2_Abs

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver

23:39:05 Simpl: theory Simpl.Vcg

23:39:05 Automatic_Refinement: theory Automatic_Refinement.Select_Solve

23:39:07 Stone_Algebras: theory Stone_Algebras.Lattice_Basics

23:39:07 HOL-Library: theory HOL-Library.Phantom_Type

23:39:08 Nominal2: theory Nominal2.Nominal2_FCB

23:39:08 Simpl: theory Simpl.ProcParEx

23:39:08 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

23:39:08 HOL-Library: theory HOL-Library.Cardinality

23:39:08 Nominal2: theory Nominal2.Nominal2

23:39:08 Simpl: theory Simpl.ProcParExSP

23:39:08 Automatic_Refinement: theory Automatic_Refinement.Quicksort

23:39:08 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

23:39:09 Automatic_Refinement: theory Automatic_Refinement.Misc

23:39:09 Simpl: theory Simpl.XVcg

23:39:09 HOL-Library: theory HOL-Library.Product_Lexorder

23:39:09 Simpl: theory Simpl.XVcgEx

23:39:09 HOL-Library: theory HOL-Library.Product_Plus

23:39:09 HOL-Library: theory HOL-Library.Product_Order

23:39:09 HOL-Library: theory HOL-Library.Numeral_Type

23:39:09 HOL-Library: theory HOL-Library.Finite_Lattice

23:39:10 Simpl: theory Simpl.ClosureEx

23:39:10 Simpl: theory Simpl.ComposeEx

23:39:10 HOL-Library: theory HOL-Library.Type_Length

23:39:11 HOL-Library: theory HOL-Library.Saturated

23:39:11 Simpl: theory Simpl.Quicksort

23:39:11 HOL-Library: theory HOL-Library.Quotient_Syntax

23:39:11 HOL-Library: theory HOL-Library.Quotient_Option

23:39:11 HOL-Library: theory HOL-Library.Quotient_Product

23:39:12 Simpl: theory Simpl.SyntaxTest

23:39:12 HOL-Library: theory HOL-Library.Quotient_Set

23:39:12 HOL-Library: theory HOL-Library.Quotient_List

23:39:12 Simpl: theory Simpl.UserGuide

23:39:12 Simpl: theory Simpl.VcgEx

23:39:13 HOL-Library: theory HOL-Library.Quotient_Sum

23:39:13 HOL-Library: theory HOL-Library.Quotient_Type

23:39:13 HOL-Library: theory HOL-Library.RBT_Impl

23:39:13 HOL-Library: theory HOL-Library.Reflection

23:39:14 HOL-Library: theory HOL-Library.Refute

23:39:14 Automatic_Refinement: theory Automatic_Refinement.Digraph_Basic

23:39:14 HOL-Library: theory HOL-Library.Rewrite

23:39:14 HOL-Library: theory HOL-Library.Set_Algebras

23:39:15 Stone_Algebras: theory Stone_Algebras.Filters

23:39:15 Stone_Algebras: theory Stone_Algebras.P_Algebras

23:39:15 HOL-Library: theory HOL-Library.Simps_Case_Conv

23:39:15 HOL-Library: theory HOL-Library.Extended

23:39:15 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib

23:39:16 Simpl: theory Simpl.VcgExSP

23:39:17 HOL-Library: theory HOL-Library.State_Monad

23:39:17 Simpl: theory Simpl.VcgExTotal

23:39:17 HOL-Library: theory HOL-Library.Stirling

23:39:18 HOL-Library: theory HOL-Library.Sublist

23:39:19 HOL-Library: theory HOL-Library.Prefix_Order

23:39:19 HOL-Library: theory HOL-Library.Subseq_Order

23:39:19 HOL-Library: theory HOL-Library.Transitive_Closure_Table

23:39:20 HOL-Library: theory HOL-Library.Tree

23:39:20 Simpl: theory Simpl.Simpl

23:39:24 HOL-Library: theory HOL-Library.Tree_Multiset

23:39:24 HOL-Library: theory HOL-Library.While_Combinator

23:39:25 Timing HOL-Word (2 threads, 22.172s elapsed time, 43.280s cpu time, 1.804s GC time, factor 1.95)

23:39:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word

23:39:25 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/document.pdf

23:39:25 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/outline.pdf

23:39:25 Finished HOL-Word (0:00:47 elapsed time, 0:01:22 cpu time, factor 1.73)

23:39:25 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

23:39:25 Building Kleene_Algebra ...

23:39:26 HOL-Library: theory HOL-Library.Countable

23:39:27 HOL-Library: theory HOL-Library.Countable_Set

23:39:28 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

23:39:28 Kleene_Algebra: theory Kleene_Algebra.Signatures

23:39:28 Kleene_Algebra: theory Kleene_Algebra.Dioid

23:39:28 Timing HOLCF (2 threads, 22.419s elapsed time, 40.548s cpu time, 2.276s GC time, factor 1.81)

23:39:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF

23:39:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/document.pdf

23:39:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/outline.pdf

23:39:28 Finished HOLCF (0:00:51 elapsed time, 0:01:24 cpu time, factor 1.65)

23:39:29 Building Word_Lib ...

23:39:31 HOL-Library: theory HOL-Library.Countable_Set_Type

23:39:31 Word_Lib: theory Word_Lib.Sublist

23:39:31 Word_Lib: theory Word_Lib.WordBitwise

23:39:33 Word_Lib: theory Word_Lib.Prefix_Order

23:39:34 HOL-Library: theory HOL-Library.BigO

23:39:35 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

23:39:35 HOL-Library: theory HOL-Library.Diagonal_Subsequence

23:39:36 HOL-Library: theory HOL-Library.Discrete

23:39:36 HOL-Library: theory HOL-Library.Function_Growth

23:39:36 Word_Lib: theory Word_Lib.Signed_Words

23:39:36 Word_Lib: theory Word_Lib.Hex_Words

23:39:37 Word_Lib: theory Word_Lib.Enumeration

23:39:37 Word_Lib: theory Word_Lib.Norm_Words

23:39:37 Word_Lib: theory Word_Lib.WordBitwise_Signed

23:39:37 Word_Lib: theory Word_Lib.Word_Syntax

23:39:37 Word_Lib: theory Word_Lib.HOL_Lemmas

23:39:37 Word_Lib: theory Word_Lib.Word_Lib

23:39:37 HOL-Library: theory HOL-Library.Indicator_Function

23:39:37 Word_Lib: theory Word_Lib.More_Divides

23:39:38 HOL-Library: theory HOL-Library.Lattice_Algebras

23:39:38 Word_Lib: theory Word_Lib.Word_Enum

23:39:38 Word_Lib: theory Word_Lib.Aligned

23:39:39 Word_Lib: theory Word_Lib.Word_Setup_32

23:39:39 Word_Lib: theory Word_Lib.Word_Setup_64

23:39:39 Word_Lib: theory Word_Lib.Word_Lemmas

23:39:40 Stone_Algebras: theory Stone_Algebras.Stone_Construction

23:39:43 Kleene_Algebra: theory Kleene_Algebra.Conway

23:39:43 Kleene_Algebra: theory Kleene_Algebra.Dioid_Models

23:39:44 HOL-Library: theory HOL-Library.Liminf_Limsup

23:39:44 Word_Lib: theory Word_Lib.Word_Lemmas_32

23:39:45 HOL-Library: theory HOL-Library.Log_Nat

23:39:45 HOL-Library: theory HOL-Library.Float

23:39:45 Word_Lib: theory Word_Lib.Word_Lemmas_64

23:39:47 Timing Nominal2 (2 threads, 36.811s elapsed time, 70.896s cpu time, 3.448s GC time, factor 1.93)

23:39:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nominal2

23:39:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nominal2/document.pdf

23:39:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nominal2/outline.pdf

23:39:47 Finished Nominal2 (0:01:09 elapsed time, 0:02:02 cpu time, factor 1.75)

23:39:48 Building UPF ...

23:39:48 HOL-Library: theory HOL-Library.RBT

23:39:49 HOL-Library: theory HOL-Library.Lub_Glb

23:39:49 HOL-Library: theory HOL-Library.RBT_Mapping

23:39:49 HOL-Library: theory HOL-Library.RBT_Set

23:39:50 HOL-Library: theory HOL-Library.Multiset_Permutations

23:39:50 UPF: theory UPF.Monads

23:39:50 Kleene_Algebra: theory Kleene_Algebra.Finite_Suprema

23:39:50 HOL-Library: theory HOL-Library.Nonpos_Ints

23:39:51 Kleene_Algebra: theory Kleene_Algebra.Inf_Matrix

23:39:51 HOL-Library: theory HOL-Library.OptionalSugar

23:39:51 UPF: theory UPF.UPFCore

23:39:51 HOL-Library: theory HOL-Library.Order_Continuity

23:39:51 Kleene_Algebra: theory Kleene_Algebra.Matrix

23:39:51 HOL-Library: theory HOL-Library.Periodic_Fun

23:39:52 HOL-Library: theory HOL-Library.Quadratic_Discriminant

23:39:52 HOL-Library: theory HOL-Library.Sum_of_Squares

23:39:52 HOL-Library: theory HOL-Library.Extended_Nat

23:39:52 UPF: theory UPF.ElementaryPolicies

23:39:53 UPF: theory UPF.ParallelComposition

23:39:53 UPF: theory UPF.SeqComposition

23:39:53 HOL-Library: theory HOL-Library.Extended_Real

23:39:53 UPF: theory UPF.Analysis

23:39:53 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra

23:39:54 UPF: theory UPF.Normalisation

23:39:55 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

23:39:56 UPF: theory UPF.NormalisationTestSpecification

23:39:57 UPF: theory UPF.UPF

23:39:57 Automatic_Refinement: theory Automatic_Refinement.Relators

23:39:57 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter

23:39:57 UPF: theory UPF.Service

23:39:58 Automatic_Refinement: theory Automatic_Refinement.Param_Tool

23:39:58 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

23:39:58 Automatic_Refinement: theory Automatic_Refinement.Param_HOL

23:39:59 Automatic_Refinement: theory Automatic_Refinement.Parametricity

23:40:00 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data

23:40:00 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases

23:40:00 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging

23:40:00 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops

23:40:00 HOL-Library: theory HOL-Library.Library

23:40:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel

23:40:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate

23:40:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface

23:40:02 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo

23:40:02 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter

23:40:02 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool

23:40:02 Kleene_Algebra: theory Kleene_Algebra.DRA

23:40:03 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL

23:40:04 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra

23:40:04 Kleene_Algebra: theory Kleene_Algebra.PHL_KA

23:40:05 Kleene_Algebra: theory Kleene_Algebra.PHL_DRA

23:40:06 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra_Models

23:40:07 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement

23:40:07 Kleene_Algebra: theory Kleene_Algebra.Formal_Power_Series

23:40:10 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra_Models

23:40:12 UPF: theory UPF.ServiceExample

23:40:22 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Eisbach

23:40:22 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example

23:40:22 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Eisbach_Tools

23:40:22 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystemTactics

23:40:24 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_Swap_Add

23:40:26 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_TypeSystem

23:40:28 Timing Stone_Algebras (2 threads, 58.231s elapsed time, 95.784s cpu time, 2.964s GC time, factor 1.64)

23:40:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stone_Algebras

23:40:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stone_Algebras/document.pdf

23:40:28 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stone_Algebras/outline.pdf

23:40:28 Finished Stone_Algebras (0:01:22 elapsed time, 0:02:12 cpu time, factor 1.60)

23:40:28 Building Noninterference_Sequential_Composition ...

23:40:30 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.ListInterleaving

23:40:30 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.CSPNoninterference

23:40:32 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.IpurgeUnwinding

23:40:33 Timing Automatic_Refinement (2 threads, 64.997s elapsed time, 113.076s cpu time, 3.640s GC time, factor 1.74)

23:40:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement

23:40:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/document.pdf

23:40:33 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/outline.pdf

23:40:33 Finished Automatic_Refinement (0:01:32 elapsed time, 0:02:34 cpu time, factor 1.67)

23:40:33 Building Refine_Monadic ...

23:40:33 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.DeterministicProcesses

23:40:36 Refine_Monadic: theory Refine_Monadic.Lattice_Syntax

23:40:36 Refine_Monadic: theory Refine_Monadic.Bit

23:40:36 Refine_Monadic: theory Refine_Monadic.Bits

23:40:36 Refine_Monadic: theory Refine_Monadic.Boolean_Algebra

23:40:36 Refine_Monadic: theory Refine_Monadic.Misc_Numeric

23:40:36 Refine_Monadic: theory Refine_Monadic.Bits_Bit

23:40:36 Refine_Monadic: theory Refine_Monadic.Bit_Representation

23:40:37 Refine_Monadic: theory Refine_Monadic.Word_Miscellaneous

23:40:37 Refine_Monadic: theory Refine_Monadic.Bits_Int

23:40:37 Refine_Monadic: theory Refine_Monadic.Misc_Typedef

23:40:37 Refine_Monadic: theory Refine_Monadic.Phantom_Type

23:40:38 Refine_Monadic: theory Refine_Monadic.Cardinality

23:40:39 Refine_Monadic: theory Refine_Monadic.Bool_List_Representation

23:40:39 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.Propaedeutics

23:40:39 Refine_Monadic: theory Refine_Monadic.Numeral_Type

23:40:40 Refine_Monadic: theory Refine_Monadic.While_Combinator

23:40:40 Refine_Monadic: theory Refine_Monadic.Adhoc_Overloading

23:40:40 Refine_Monadic: theory Refine_Monadic.Monad_Syntax

23:40:41 Refine_Monadic: theory Refine_Monadic.Type_Length

23:40:41 Refine_Monadic: theory Refine_Monadic.Word

23:40:42 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.SequentialComposition

23:40:43 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.Counterexamples

23:40:53 Timing Kleene_Algebra (2 threads, 53.452s elapsed time, 92.188s cpu time, 4.176s GC time, factor 1.72)

23:40:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra

23:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/document.pdf

23:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/outline.pdf

23:40:53 Finished Kleene_Algebra (0:01:27 elapsed time, 0:02:23 cpu time, factor 1.65)

23:40:53 Timing UPF (2 threads, 33.517s elapsed time, 64.472s cpu time, 2.468s GC time, factor 1.92)

23:40:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF

23:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF/document.pdf

23:40:53 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF/outline.pdf

23:40:53 Finished UPF (0:01:04 elapsed time, 0:01:52 cpu time, factor 1.74)

23:40:54 Building KAT_and_DRA ...

23:40:54 Building Relation_Algebra ...

23:40:57 KAT_and_DRA: theory KAT_and_DRA.Test_Dioid

23:40:57 KAT_and_DRA: theory KAT_and_DRA.KAT2

23:40:57 Relation_Algebra: theory Relation_Algebra.More_Boolean_Algebra

23:40:58 KAT_and_DRA: theory KAT_and_DRA.DRAT2

23:40:58 Refine_Monadic: theory Refine_Monadic.Example_Chapter

23:40:58 Refine_Monadic: theory Refine_Monadic.Refine_Chapter

23:40:58 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover

23:40:58 Relation_Algebra: theory Relation_Algebra.Relation_Algebra

23:40:58 Refine_Monadic: theory Refine_Monadic.Refine_Misc

23:40:59 Refine_Monadic: theory Refine_Monadic.RefineG_Domain

23:40:59 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer

23:40:59 Refine_Monadic: theory Refine_Monadic.RefineG_Assert

23:40:59 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion

23:41:00 Refine_Monadic: theory Refine_Monadic.RefineG_While

23:41:00 Refine_Monadic: theory Refine_Monadic.Refine_Basic

23:41:01 Refine_Monadic: theory Refine_Monadic.Refine_Det

23:41:02 Timing Word_Lib (2 threads, 69.118s elapsed time, 135.564s cpu time, 3.244s GC time, factor 1.96)

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

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

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

23:41:02 Finished Word_Lib (0:01:33 elapsed time, 0:02:51 cpu time, factor 1.84)

23:41:02 Building IP_Addresses ...

23:41:03 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics

23:41:04 Refine_Monadic: theory Refine_Monadic.Refine_Leof

23:41:04 Refine_Monadic: theory Refine_Monadic.Refine_While

23:41:04 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Models

23:41:04 Refine_Monadic: theory Refine_Monadic.Refine_Pfun

23:41:04 KAT_and_DRA: theory KAT_and_DRA.Conway_Tests

23:41:05 IP_Addresses: theory IP_Addresses.Cancellation

23:41:05 IP_Addresses: theory IP_Addresses.Char_ord

23:41:06 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_RTC

23:41:06 Refine_Monadic: theory Refine_Monadic.Refine_Transfer

23:41:06 IP_Addresses: theory IP_Addresses.Code_Abstract_Nat

23:41:06 IP_Addresses: theory IP_Addresses.Code_Target_Nat

23:41:06 IP_Addresses: theory IP_Addresses.Code_Char

23:41:06 IP_Addresses: theory IP_Addresses.Multiset

23:41:06 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic

23:41:06 IP_Addresses: theory IP_Addresses.Code_Target_Int

23:41:06 Refine_Monadic: theory Refine_Monadic.Refine_Automation

23:41:06 Refine_Monadic: theory Refine_Monadic.Refine_Foreach

23:41:06 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Tests

23:41:06 IP_Addresses: theory IP_Addresses.Infinite_Set

23:41:06 KAT_and_DRA: theory KAT_and_DRA.KAT

23:41:07 IP_Addresses: theory IP_Addresses.NumberWang_IPv4

23:41:07 IP_Addresses: theory IP_Addresses.Option_ord

23:41:08 IP_Addresses: theory IP_Addresses.NumberWang_IPv6

23:41:08 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Vectors

23:41:08 IP_Addresses: theory IP_Addresses.Word_More

23:41:09 Refine_Monadic: theory Refine_Monadic.Refine_Monadic

23:41:09 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Functions

23:41:10 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search

23:41:10 Refine_Monadic: theory Refine_Monadic.WordRefine

23:41:10 KAT_and_DRA: theory KAT_and_DRA.DRAT

23:41:10 KAT_and_DRA: theory KAT_and_DRA.PHL_KAT

23:41:11 Refine_Monadic: theory Refine_Monadic.Examples

23:41:11 IP_Addresses: theory IP_Addresses.Quicksort

23:41:12 IP_Addresses: theory IP_Addresses.Misc

23:41:12 KAT_and_DRA: theory KAT_and_DRA.DRA_Models

23:41:13 KAT_and_DRA: theory KAT_and_DRA.FolkTheorem

23:41:13 Timing Noninterference_Sequential_Composition (2 threads, 20.830s elapsed time, 38.520s cpu time, 1.916s GC time, factor 1.85)

23:41:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Sequential_Composition

23:41:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Sequential_Composition/document.pdf

23:41:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Sequential_Composition/outline.pdf

23:41:13 Finished Noninterference_Sequential_Composition (0:00:45 elapsed time, 0:01:14 cpu time, factor 1.65)

23:41:14 Building HOLCF-HOL-Library ...

23:41:14 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Direct_Products

23:41:14 KAT_and_DRA: theory KAT_and_DRA.KAT_Models

23:41:15 KAT_and_DRA: theory KAT_and_DRA.PHL_DRAT

23:41:16 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Cancellation

23:41:16 HOLCF-HOL-Library: theory HOLCF-HOL-Library.AList

23:41:17 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Multiset

23:41:18 HOLCF-HOL-Library: theory HOLCF-HOL-Library.FuncSet

23:41:19 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Infinite_Set

23:41:19 HOLCF-HOL-Library: theory HOLCF-HOL-Library.LaTeXsugar

23:41:19 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Syntax

23:41:19 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Option

23:41:22 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Permutation

23:41:34 Timing Simpl (2 threads, 112.842s elapsed time, 215.008s cpu time, 11.828s GC time, factor 1.91)

23:41:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl

23:41:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl/document.pdf

23:41:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl/outline.pdf

23:41:34 Finished Simpl (0:02:56 elapsed time, 0:05:15 cpu time, factor 1.78)

23:41:35 Building HOLCF-Library ...

23:41:38 HOLCF-Library: theory HOLCF-Library.Infinite_Set

23:41:38 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

23:41:38 HOLCF-Library: theory HOLCF-Library.Char_Discrete

23:41:38 HOLCF-Library: theory HOLCF-Library.Countable_Set

23:41:38 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

23:41:39 HOLCF-Library: theory HOLCF-Library.Countable_Complete_Lattices

23:41:39 HOLCF-Library: theory HOLCF-Library.Int_Discrete

23:41:39 HOLCF-Library: theory HOLCF-Library.List_Cpo

23:41:40 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

23:41:40 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

23:41:41 HOLCF-Library: theory HOLCF-Library.List_Predomain

23:41:42 HOLCF-Library: theory HOLCF-Library.Option_Cpo

23:41:42 HOLCF-Library: theory HOLCF-Library.Order_Continuity

23:41:42 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

23:41:43 HOLCF-Library: theory HOLCF-Library.Extended_Nat

23:41:44 HOLCF-Library: theory HOLCF-Library.Stream

23:41:46 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

23:41:47 Timing Relation_Algebra (2 threads, 25.447s elapsed time, 49.180s cpu time, 1.724s GC time, factor 1.93)

23:41:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra

23:41:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra/document.pdf

23:41:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Relation_Algebra/outline.pdf

23:41:47 Finished Relation_Algebra (0:00:53 elapsed time, 0:01:29 cpu time, factor 1.69)

23:41:47 Building Noninterference_CSP ...

23:41:49 Noninterference_CSP: theory Noninterference_CSP.CSPNoninterference

23:41:49 IP_Addresses: theory IP_Addresses.Hs_Compat

23:41:49 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString

23:41:49 IP_Addresses: theory IP_Addresses.Product_Lexorder

23:41:49 IP_Addresses: theory IP_Addresses.Lib_List_toString

23:41:50 IP_Addresses: theory IP_Addresses.Lib_Word_toString

23:41:50 IP_Addresses: theory IP_Addresses.Word_Next

23:41:50 IP_Addresses: theory IP_Addresses.WordInterval

23:41:50 Noninterference_CSP: theory Noninterference_CSP.ClassicalNoninterference

23:41:51 Noninterference_CSP: theory Noninterference_CSP.GeneralizedNoninterference

23:41:52 Timing HOLCF-HOL-Library (2 threads, 16.982s elapsed time, 31.900s cpu time, 1.520s GC time, factor 1.88)

23:41:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-HOL-Library

23:41:52 Finished HOLCF-HOL-Library (0:00:37 elapsed time, 0:01:02 cpu time, factor 1.66)

23:41:52 Building HOLCF-Nominal2 ...

23:41:55 IP_Addresses: theory IP_Addresses.IP_Address

23:41:55 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Set

23:41:55 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Product

23:41:55 HOLCF-Nominal2: theory HOLCF-Nominal2.FSet

23:41:55 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_List

23:41:55 IP_Addresses: theory IP_Addresses.WordInterval_Sorted

23:41:56 HOLCF-Nominal2: theory HOLCF-Nominal2.Phantom_Type

23:41:56 HOLCF-Nominal2: theory HOLCF-Nominal2.Cardinality

23:41:58 HOLCF-Nominal2: theory HOLCF-Nominal2.FinFun

23:41:59 IP_Addresses: theory IP_Addresses.IPv4

23:41:59 IP_Addresses: theory IP_Addresses.IPv6

23:42:01 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Base

23:42:01 Timing KAT_and_DRA (2 threads, 42.452s elapsed time, 80.732s cpu time, 2.824s GC time, factor 1.90)

23:42:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA

23:42:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/document.pdf

23:42:01 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/outline.pdf

23:42:01 Finished KAT_and_DRA (0:01:07 elapsed time, 0:02:03 cpu time, factor 1.83)

23:42:02 Building Ordinal ...

23:42:02 IP_Addresses: theory IP_Addresses.Prefix_Match

23:42:03 Ordinal: theory Ordinal.OrdinalDef

23:42:04 IP_Addresses: theory IP_Addresses.CIDR_Split

23:42:05 Ordinal: theory Ordinal.OrdinalInduct

23:42:05 Timing Refine_Monadic (2 threads, 57.668s elapsed time, 104.864s cpu time, 4.680s GC time, factor 1.82)

23:42:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic

23:42:05 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic/document.pdf

23:42:05 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic/outline.pdf

23:42:05 Finished Refine_Monadic (0:01:31 elapsed time, 0:02:36 cpu time, factor 1.71)

23:42:05 Ordinal: theory Ordinal.OrdinalCont

23:42:05 Building Collections ...

23:42:05 Ordinal: theory Ordinal.OrdinalRec

23:42:05 HOLCF-Nominal2: theory HOLCF-Nominal2.Atoms

23:42:05 HOLCF-Nominal2: theory HOLCF-Nominal2.Eqvt

23:42:05 Ordinal: theory Ordinal.OrdinalArith

23:42:06 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Abs

23:42:06 Ordinal: theory Ordinal.OrdinalInverse

23:42:06 Ordinal: theory Ordinal.OrdinalFix

23:42:06 Ordinal: theory Ordinal.OrdinalOmega

23:42:07 Ordinal: theory Ordinal.OrdinalVeblen

23:42:07 Ordinal: theory Ordinal.Ordinal

23:42:08 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_FCB

23:42:09 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2

23:42:09 Collections: theory Collections.SetIterator

23:42:09 Collections: theory Collections.AList

23:42:10 Timing HOLCF-Library (2 threads, 15.145s elapsed time, 29.476s cpu time, 1.200s GC time, factor 1.95)

23:42:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF-Library

23:42:10 Finished HOLCF-Library (0:00:34 elapsed time, 0:00:57 cpu time, factor 1.68)

23:42:10 Building Marriage ...

23:42:11 Collections: theory Collections.BinomialHeap

23:42:11 Collections: theory Collections.Idx_Iterator

23:42:11 Collections: theory Collections.Code_Abstract_Nat

23:42:12 Collections: theory Collections.Code_Target_Nat

23:42:12 Collections: theory Collections.Code_Target_Int

23:42:12 Marriage: theory Marriage.Marriage

23:42:12 Collections: theory Collections.Code_Target_Numeral

23:42:12 Collections: theory Collections.Dlist

23:42:13 Timing Noninterference_CSP (2 threads, 6.301s elapsed time, 11.892s cpu time, 0.596s GC time, factor 1.89)

23:42:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_CSP

23:42:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_CSP/document.pdf

23:42:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_CSP/outline.pdf

23:42:13 Finished Noninterference_CSP (0:00:24 elapsed time, 0:00:39 cpu time, factor 1.57)

23:42:13 Building Noninterference_Ipurge_Unwinding ...

23:42:13 Collections: theory Collections.FingerTree

23:42:15 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.ListInterleaving

23:42:15 Collections: theory Collections.ICF_Tools

23:42:15 Collections: theory Collections.Ord_Code_Preproc

23:42:15 Collections: theory Collections.Locale_Code

23:42:15 Collections: theory Collections.Partial_Equivalence_Relation

23:42:15 Collections: theory Collections.RBT_Impl

23:42:18 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding

23:42:20 Timing Dependent_SIFUM_Type_Systems (2 threads, 173.084s elapsed time, 297.928s cpu time, 10.920s GC time, factor 1.72)

23:42:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems

23:42:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/document.pdf

23:42:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/outline.pdf

23:42:20 Finished Dependent_SIFUM_Type_Systems (0:03:41 elapsed time, 0:06:15 cpu time, factor 1.69)

23:42:20 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses

23:42:20 Building Cauchy ...

23:42:22 Cauchy: theory Cauchy.CauchysMeanTheorem

23:42:22 Cauchy: theory Cauchy.CauchySchwarz

23:42:23 Timing Ordinal (2 threads, 3.604s elapsed time, 6.248s cpu time, 0.204s GC time, factor 1.73)

23:42:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinal

23:42:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinal/document.pdf

23:42:23 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ordinal/outline.pdf

23:42:23 Finished Ordinal (0:00:21 elapsed time, 0:00:32 cpu time, factor 1.52)

23:42:23 Building Nested_Multisets_Ordinals ...

23:42:25 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cancellation

23:42:25 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cardinal_Notations

23:42:25 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.FSet

23:42:26 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset

23:42:28 Collections: theory Collections.Record_Intf

23:42:28 Collections: theory Collections.SetAbstractionIterator

23:42:29 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Infinite_Set

23:42:29 Collections: theory Collections.SetIteratorOperations

23:42:29 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.List_Index

23:42:29 Timing Marriage (2 threads, 2.880s elapsed time, 5.068s cpu time, 0.060s GC time, factor 1.76)

23:42:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage

23:42:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage/document.pdf

23:42:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage/outline.pdf

23:42:29 Finished Marriage (0:00:19 elapsed time, 0:00:28 cpu time, factor 1.50)

23:42:29 Building HOL-SPARK ...

23:42:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nat_Bijection

23:42:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Old_Datatype

23:42:31 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_Order

23:42:31 Collections: theory Collections.Assoc_List

23:42:31 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Plus

23:42:32 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable

23:42:32 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Order

23:42:32 Collections: theory Collections.Diff_Array

23:42:32 HOL-SPARK: theory HOL-SPARK.Bit_Comparison

23:42:32 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

23:42:32 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Sublist

23:42:34 Collections: theory Collections.Dlist_add

23:42:34 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set

23:42:34 Collections: theory Collections.Proper_Iterator

23:42:34 HOL-SPARK: theory SPARK

23:42:34 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Complete_Lattices

23:42:34 Collections: theory Collections.It_to_It

23:42:34 Collections: theory Collections.SetIteratorGA

23:42:35 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set_Type

23:42:36 Collections: theory Collections.SkewBinomialHeap

23:42:37 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Order_Continuity

23:42:38 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Extended_Nat

23:42:39 Timing HOLCF-Nominal2 (2 threads, 22.940s elapsed time, 45.296s cpu time, 1.996s GC time, factor 1.97)

23:42:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Nominal2

23:42:39 Finished HOLCF-Nominal2 (0:00:47 elapsed time, 0:01:21 cpu time, factor 1.72)

23:42:40 Timing Cauchy (2 threads, 2.635s elapsed time, 5.128s cpu time, 0.112s GC time, factor 1.95)

23:42:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy

23:42:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy/document.pdf

23:42:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy/outline.pdf

23:42:40 Finished Cauchy (0:00:18 elapsed time, 0:00:28 cpu time, factor 1.51)

23:42:40 Building Launchbury ...

23:42:40 Building Sqrt_Babylonian ...

23:42:40 Timing Noninterference_Ipurge_Unwinding (2 threads, 9.066s elapsed time, 14.660s cpu time, 0.680s GC time, factor 1.62)

23:42:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Ipurge_Unwinding

23:42:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Ipurge_Unwinding/document.pdf

23:42:40 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Noninterference_Ipurge_Unwinding/outline.pdf

23:42:40 Finished Noninterference_Ipurge_Unwinding (0:00:27 elapsed time, 0:00:41 cpu time, factor 1.51)

23:42:41 Building Main ...

23:42:42 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

23:42:42 Main: theory Main.Main_Doc

23:42:43 Sqrt_Babylonian: theory Sqrt_Babylonian.Log_Impl

23:42:43 Sqrt_Babylonian: theory Sqrt_Babylonian.NthRoot_Impl

23:42:43 Launchbury: theory Launchbury.Mono-Nat-Fun

23:42:43 Launchbury: theory Launchbury.Nominal-Utils

23:42:44 Launchbury: theory Launchbury.Vars

23:42:44 Launchbury: theory Launchbury.C

23:42:44 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian

23:42:44 Launchbury: theory Launchbury.HOLCF-Join

23:42:44 Launchbury: theory Launchbury.HOLCF-Join-Classes

23:42:45 Launchbury: theory Launchbury.CValue

23:42:45 Launchbury: theory Launchbury.HOLCF-Meet

23:42:46 Launchbury: theory Launchbury.Value

23:42:46 Launchbury: theory Launchbury.C-Meet

23:42:46 Launchbury: theory Launchbury.AList-Utils

23:42:47 Launchbury: theory Launchbury.Env

23:42:47 Launchbury: theory Launchbury.AList-Utils-Nominal

23:42:47 Launchbury: theory Launchbury.Pointwise

23:42:47 Launchbury: theory Launchbury.HOLCF-Utils

23:42:47 Launchbury: theory Launchbury.Terms

23:42:48 Launchbury: theory Launchbury.C-restr

23:42:48 Launchbury: theory Launchbury.Env-HOLCF

23:42:48 Launchbury: theory Launchbury.Iterative

23:42:49 Timing HOL-SPARK (2 threads, 2.459s elapsed time, 4.144s cpu time, 0.140s GC time, factor 1.69)

23:42:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK

23:42:49 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.47)

23:42:49 Building HOL-SPARK-Examples ...

23:42:49 Launchbury: theory Launchbury.EvalHeap

23:42:49 Collections: theory Collections.Sorted_List_Operations

23:42:50 Collections: theory Collections.More_Bits_Int

23:42:51 Launchbury: theory Launchbury.Nominal-HOLCF

23:42:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas

23:42:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD

23:42:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor

23:42:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence

23:42:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification

23:42:52 Collections: theory Collections.Bits_Integer

23:42:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F

23:42:53 Launchbury: theory Launchbury.CValue-Nominal

23:42:54 Launchbury: theory Launchbury.Env-Nominal

23:42:54 Launchbury: theory Launchbury.HasESem

23:42:55 Launchbury: theory Launchbury.HeapSemantics

23:42:55 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash

23:42:56 Launchbury: theory Launchbury.Substitution

23:42:56 Collections: theory Collections.Word_Misc

23:42:57 Launchbury: theory Launchbury.Launchbury

23:42:57 Launchbury: theory Launchbury.AbstractDenotational

23:42:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L

23:42:57 Timing Main (2 threads, 1.395s elapsed time, 1.472s cpu time, 0.000s GC time, factor 1.05)

23:42:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/Doc/Main

23:42:57 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/Doc/Main/main.pdf

23:42:57 Finished Main (0:00:16 elapsed time, 0:00:22 cpu time, factor 1.37)

23:42:57 Running Psi_Calculi ...

23:42:57 Collections: theory Collections.DatRef

23:42:57 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R

23:42:58 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L

23:42:58 Launchbury: theory Launchbury.Abstract-Denotational-Props

23:42:58 Collections: theory Collections.Gen_Iterator

23:42:59 Launchbury: theory Launchbury.ResourcedDenotational

23:42:59 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R

23:42:59 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round

23:42:59 Launchbury: theory Launchbury.Value-Nominal

23:43:00 Collections: theory Collections.Iterator

23:43:00 Launchbury: theory Launchbury.Denotational

23:43:00 Psi_Calculi: theory Psi_Calculi.Chain

23:43:00 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L

23:43:00 Launchbury: theory Launchbury.CorrectnessResourced

23:43:00 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_More

23:43:00 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.McCarthy_91

23:43:00 Collections: theory Collections.ICF_Spec_Base

23:43:01 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nested_Multiset

23:43:01 Collections: theory Collections.MapSpec

23:43:01 Launchbury: theory Launchbury.CorrectnessOriginal

23:43:01 Launchbury: theory Launchbury.ResourcedAdequacy

23:43:01 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R

23:43:01 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Multiset

23:43:01 Launchbury: theory Launchbury.ValueSimilarity

23:43:02 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hereditary_Multiset

23:43:02 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt

23:43:02 Psi_Calculi: theory Psi_Calculi.Subst_Term

23:43:02 Launchbury: theory Launchbury.Denotational-Related

23:43:02 Psi_Calculi: theory Psi_Calculi.Agent

23:43:03 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset

23:43:03 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Unary_PCF

23:43:03 Launchbury: theory Launchbury.Adequacy

23:43:03 Collections: theory Collections.Code_Target_Bits_Int

23:43:03 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal

23:43:04 Collections: theory Collections.Code_Target_ICF

23:43:04 Collections: theory Collections.Locale_Code_Ex

23:43:04 Launchbury: theory Launchbury.EverythingAdequacy

23:43:05 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Goodstein_Sequence

23:43:05 Collections: theory Collections.Uint32

23:43:05 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hydra_Battle

23:43:05 Collections: theory Collections.Robdd

23:43:06 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal

23:43:07 Collections: theory Collections.HashCode

23:43:07 Collections: theory Collections.RBT_add

23:43:07 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge

23:43:15 Timing Sqrt_Babylonian (2 threads, 15.009s elapsed time, 24.732s cpu time, 0.460s GC time, factor 1.65)

23:43:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sqrt_Babylonian

23:43:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sqrt_Babylonian/document.pdf

23:43:15 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Sqrt_Babylonian/outline.pdf

23:43:15 Finished Sqrt_Babylonian (0:00:34 elapsed time, 0:00:53 cpu time, factor 1.54)

23:43:15 Running Key_Agreement_Strong_Adversaries ...

23:43:17 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Infra

23:43:17 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Messages

23:43:17 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Refinement

23:43:19 IP_Addresses: theory IP_Addresses.IP_Address_Parser

23:43:19 Psi_Calculi: theory Psi_Calculi.Close_Subst

23:43:20 Psi_Calculi: theory Psi_Calculi.Frame

23:43:20 Psi_Calculi: theory Psi_Calculi.Structural_Congruence

23:43:22 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationN

23:43:22 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Message_derivation

23:43:23 Psi_Calculi: theory Psi_Calculi.Semantics

23:43:24 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.AuthenticationI

23:43:24 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Channels

23:43:24 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.IK

23:43:24 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Secrecy

23:43:25 IP_Addresses: theory IP_Addresses.IP_Address_toString

23:43:25 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Payloads

23:43:25 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Runs

23:43:26 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem

23:43:26 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_asymmetric

23:43:26 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_lemmas

23:43:26 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.Implem_symmetric

23:43:27 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl1

23:43:27 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl1

23:43:28 Timing HOL-SPARK-Examples (2 threads, 19.128s elapsed time, 32.680s cpu time, 0.776s GC time, factor 1.71)

23:43:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK-Examples

23:43:28 Finished HOL-SPARK-Examples (0:00:39 elapsed time, 0:01:02 cpu time, factor 1.59)

23:43:28 Running Network_Security_Policy_Verification ...

23:43:29 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl2

23:43:29 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl1

23:43:30 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3

23:43:30 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl2

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Cancellation

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Char_ord

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Abstract_Nat

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Target_Nat

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Multiset

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Char

23:43:31 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph

23:43:32 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric

23:43:32 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric

23:43:32 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl2

23:43:32 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3

23:43:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Infinite_Set

23:43:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.List_lexord

23:43:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Config

23:43:33 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3

23:43:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz

23:43:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable

23:43:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Option_ord

23:43:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Orders

23:43:34 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric

23:43:34 Timing HOL-Library (2 threads, 202.727s elapsed time, 382.200s cpu time, 20.736s GC time, factor 1.89)

23:43:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library

23:43:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/document.pdf

23:43:34 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/outline.pdf

23:43:34 Finished HOL-Library (0:04:56 elapsed time, 0:08:53 cpu time, factor 1.80)

23:43:34 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric

23:43:35 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric

23:43:35 Key_Agreement_Strong_Adversaries: theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric

23:43:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Bounds

23:43:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Lattice

23:43:35 Building HOL-Computational_Algebra ...

23:43:36 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CompleteLattice

23:43:36 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Product_Lexorder

23:43:37 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.RBT_Impl

23:43:37 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Quicksort

23:43:37 Psi_Calculi: theory Psi_Calculi.Simulation

23:43:37 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Misc

23:43:38 Psi_Calculi: theory Psi_Calculi.Bisimulation

23:43:39 Psi_Calculi: theory Psi_Calculi.Sim_Pres

23:43:40 Psi_Calculi: theory Psi_Calculi.Sim_Struct_Cong

23:43:41 Psi_Calculi: theory Psi_Calculi.Sum

23:43:41 Psi_Calculi: theory Psi_Calculi.Bisim_Pres

23:43:41 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

23:43:41 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

23:43:42 Psi_Calculi: theory Psi_Calculi.Tau_Chain

23:43:43 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

23:43:43 Psi_Calculi: theory Psi_Calculi.Bisim_Struct_Cong

23:43:44 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util

23:43:44 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct

23:43:44 Psi_Calculi: theory Psi_Calculi.Weak_Simulation

23:43:44 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp

23:43:45 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Transitive_Closure_Impl

23:43:45 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp_Pres

23:43:46 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Transitive_Closure_List_Impl

23:43:46 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Simulation

23:43:46 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph

23:43:46 Psi_Calculi: theory Psi_Calculi.Weak_Sim_Pres

23:43:47 Psi_Calculi: theory Psi_Calculi.Bisim_Subst

23:43:50 Psi_Calculi: theory Psi_Calculi.Weak_Bisimulation

23:43:50 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Sim_Pres

23:43:51 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

23:43:51 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

23:43:53 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Pres

23:43:56 Psi_Calculi: theory Psi_Calculi.Weak_Psi_Congruence

23:43:56 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Struct_Cong

23:43:58 Psi_Calculi: theory Psi_Calculi.Weakening

23:43:59 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Pres

23:44:00 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

23:44:00 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

23:44:00 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

23:44:01 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

23:44:02 Psi_Calculi: theory Psi_Calculi.Weaken_Transition

23:44:02 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Struct_Cong

23:44:02 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

23:44:04 Psi_Calculi: theory Psi_Calculi.Weaken_Stat_Imp

23:44:05 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

23:44:06 Psi_Calculi: theory Psi_Calculi.Weak_Congruence

23:44:06 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

23:44:07 Psi_Calculi: theory Psi_Calculi.Weaken_Simulation

23:44:08 Timing Nested_Multisets_Ordinals (2 threads, 67.739s elapsed time, 128.212s cpu time, 4.908s GC time, factor 1.89)

23:44:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals

23:44:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/document.pdf

23:44:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/outline.pdf

23:44:08 Finished Nested_Multisets_Ordinals (0:01:44 elapsed time, 0:03:04 cpu time, factor 1.77)

23:44:08 Building Abstract-Rewriting ...

23:44:10 Psi_Calculi: theory Psi_Calculi.Weaken_Bisimulation

23:44:10 Timing Launchbury (2 threads, 49.873s elapsed time, 91.448s cpu time, 3.144s GC time, factor 1.83)

23:44:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury

23:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/document.pdf

23:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/outline.pdf

23:44:10 Finished Launchbury (0:01:29 elapsed time, 0:02:32 cpu time, factor 1.70)

23:44:10 Building Jinja ...

23:44:12 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.RBT

23:44:13 Psi_Calculi: theory Psi_Calculi.Tau

23:44:13 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl

23:44:14 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Set

23:44:16 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Exp

23:44:16 Jinja: theory Jinja.Auxiliary

23:44:16 Jinja: theory Jinja.List_Index

23:44:17 Jinja: theory Jinja.Type

23:44:17 Jinja: theory Jinja.Hidden

23:44:17 Jinja: theory Jinja.Semilat

23:44:17 Jinja: theory Jinja.Decl

23:44:17 Jinja: theory Jinja.TypeRel

23:44:18 Jinja: theory Jinja.Err

23:44:19 Jinja: theory Jinja.Listn

23:44:19 Jinja: theory Jinja.Value

23:44:19 Jinja: theory Jinja.Opt

23:44:19 Jinja: theory Jinja.Product

23:44:20 Jinja: theory Jinja.Semilattices

23:44:20 Abstract-Rewriting: theory Abstract-Rewriting.NDerivative

23:44:20 Abstract-Rewriting: theory Abstract-Rewriting.Relation_Interpretation

23:44:20 Jinja: theory Jinja.Objects

23:44:20 Jinja: theory Jinja.Typing_Framework

23:44:20 Jinja: theory Jinja.SemilatAlg

23:44:20 Jinja: theory Jinja.Exceptions

23:44:20 Jinja: theory Jinja.JVMState

23:44:20 Jinja: theory Jinja.Conform

23:44:21 Jinja: theory Jinja.Expr

23:44:21 Jinja: theory Jinja.State

23:44:21 Jinja: theory Jinja.SystemClasses

23:44:21 Jinja: theory Jinja.JVMInstructions

23:44:24 Jinja: theory Jinja.JVMExceptions

23:44:24 Abstract-Rewriting: theory Abstract-Rewriting.Equivalence_Checking

23:44:24 Jinja: theory Jinja.JVMExecInstr

23:44:24 Abstract-Rewriting: theory Abstract-Rewriting.Regexp_Method

23:44:25 Jinja: theory Jinja.JVMExec

23:44:26 Jinja: theory Jinja.JVMDefensive

23:44:27 Abstract-Rewriting: theory Abstract-Rewriting.Seq

23:44:28 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting

23:44:28 Jinja: theory Jinja.Examples

23:44:29 Jinja: theory Jinja.BigStep

23:44:29 Psi_Calculi: theory Psi_Calculi.Tau_Sim

23:44:30 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting

23:44:30 Jinja: theory Jinja.SmallStep

23:44:31 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders

23:44:31 Collections: theory Collections.Intf_Comp

23:44:31 Collections: theory Collections.GenCF_Chapter

23:44:32 Collections: theory Collections.GenCF_Gen_Chapter

23:44:32 Collections: theory Collections.GenCF_Impl_Chapter

23:44:32 Collections: theory Collections.GenCF_Intf_Chapter

23:44:32 Collections: theory Collections.Product_Lexorder

23:44:32 Collections: theory Collections.Impl_Array_Stack

23:44:32 Jinja: theory Jinja.DefAss

23:44:33 Jinja: theory Jinja.J1

23:44:33 Collections: theory Collections.Intf_Hash

23:44:33 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier

23:44:33 Collections: theory Collections.Gen_Comp

23:44:34 Collections: theory Collections.Array_Iterator

23:44:34 Collections: theory Collections.Intf_Map

23:44:34 Collections: theory Collections.Intf_Set

23:44:34 Collections: theory Collections.Gen_Map

23:44:35 Collections: theory Collections.Impl_RBT_Map

23:44:35 Collections: theory Collections.Impl_Array_Map

23:44:36 Collections: theory Collections.Impl_List_Map

23:44:37 Jinja: theory Jinja.execute_Bigstep

23:44:38 Collections: theory Collections.Impl_Array_Hash_Map

23:44:38 Jinja: theory Jinja.JVMListExample

23:44:39 Jinja: theory Jinja.WellType

23:44:40 Jinja: theory Jinja.Annotate

23:44:40 Collections: theory Collections.Gen_Map2Set

23:44:40 Jinja: theory Jinja.WellTypeRT

23:44:41 Collections: theory Collections.Gen_Set

23:44:41 Collections: theory Collections.Impl_Cfun_Set

23:44:41 Collections: theory Collections.Impl_List_Set

23:44:42 Jinja: theory Jinja.execute_WellType

23:44:44 Jinja: theory Jinja.WellForm

23:44:45 Jinja: theory Jinja.PCompiler

23:44:45 Jinja: theory Jinja.Compiler2

23:44:46 Jinja: theory Jinja.Correctness2

23:44:48 Jinja: theory Jinja.WWellForm

23:44:49 Jinja: theory Jinja.Equivalence

23:44:50 Jinja: theory Jinja.Progress

23:44:51 Jinja: theory Jinja.JWellForm

23:44:52 Jinja: theory Jinja.J1WellForm

23:44:53 Jinja: theory Jinja.TypeSafe

23:44:54 Jinja: theory Jinja.Compiler1

23:44:54 Jinja: theory Jinja.Correctness1

23:44:55 Jinja: theory Jinja.Compiler

23:44:55 Jinja: theory Jinja.SemiType

23:44:55 Jinja: theory Jinja.JVM_SemiType

23:44:56 Jinja: theory Jinja.Effect

23:44:58 Psi_Calculi: theory Psi_Calculi.Tau_Stat_Imp

23:45:07 Jinja: theory Jinja.BVSpec

23:45:08 Jinja: theory Jinja.BVConform

23:45:08 Collections: theory Collections.Uint

23:45:08 Collections: theory Collections.Gen_Hash

23:45:08 Jinja: theory Jinja.TypeComp

23:45:08 Collections: theory Collections.Impl_Bit_Set

23:45:08 Jinja: theory Jinja.BVSpecTypeSafe

23:45:09 Collections: theory Collections.Impl_Uv_Set

23:45:10 Jinja: theory Jinja.BVNoTypeError

23:45:10 Jinja: theory Jinja.EffectMono

23:45:10 Jinja: theory Jinja.Kildall

23:45:10 Jinja: theory Jinja.LBVSpec