17:46:44 Started by upstream project "isabelle-repo" build number 968

17:46:44 originally caused by:

17:46:44 Started by an SCM change

17:46:44 [EnvInject] - Loading node environment variables.

17:46:44 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp

17:46:44 [isabelle-repo-afp] $ hg showconfig paths.default

17:46:44 [isabelle-repo-afp] $ hg pull --rev dd006934a7195d982ce4c0573bd419665b8f4e17

17:46:44 pulling from http://isabelle.in.tum.de/repos/isabelle/

17:46:44 searching for changes

17:46:44 adding changesets

17:46:44 adding manifests

17:46:44 adding file changes

17:46:44 added 3 changesets with 4 changes to 3 files

17:46:44 (run 'hg update' to get a working copy)

17:46:44 [isabelle-repo-afp] $ hg update --clean --rev dd006934a7195d982ce4c0573bd419665b8f4e17

17:46:45 3 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

17:46:45 [isabelle-repo-afp] $ hg id --branch

17:46:45 [afp] $ hg showconfig paths.default

17:46:45 [afp] $ hg pull --rev default

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

17:46:46 no changes found

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

17:46:46 364 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

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

17:46:46 No emails were triggered.

17:46:46 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson6523632554110814222.sh

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

17:46:46 + set -e

17:46:46 + PROFILE=afp

17:46:46 + shift

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

17:46:47 + bin/isabelle jedit -bf

17:46:47 ### Building Isabelle/Scala ...

17:47:13 ### Building Isabelle/jEdit ...

17:47:27 + bin/isabelle ci_build_afp

17:47:32

17:47:32 === CONFIGURATION ===

17:47:32

17:47:32 ISABELLE_BUILD_OPTIONS=""

17:47:32

17:47:32 ML_PLATFORM="x86_64-linux"

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

17:47:32 ML_SYSTEM="polyml-5.6"

17:47:32 ML_OPTIONS="-H 4000 --maxheap 8G"

17:47:32

17:47:32 === BUILD ===

17:47:32

17:47:32 Build started at Tue, 20 Jun 2017 15:47:32 GMT

17:47:32 Isabelle id dd006934a719

17:47:32 AFP id 6bb0ef93920d

17:47:32

17:47:32 === LOG ===

17:47:32

17:47:33 Session Pure/Pure

17:47:33 Session HOL/HOL (main)

17:47:34 Session AFP/AVL-Trees (AFP)

17:47:34 Session AFP/AWN (AFP)

17:47:34 Session AFP/Abortable_Linearizable_Modules (AFP)

17:47:34 Session AFP/Abstract-Hoare-Logics (AFP)

17:47:34 Session AFP/BinarySearchTree (AFP)

17:47:34 Session AFP/Binomial-Queues (AFP)

17:47:34 Session AFP/Bondy (AFP)

17:47:34 Session AFP/Bounded_Deducibility_Security (AFP)

17:47:34 Session AFP/BytecodeLogicJmlTypes (AFP)

17:47:34 Session AFP/CISC-Kernel (AFP)

17:47:34 Session AFP/CYK (AFP)

17:47:34 Session AFP/Cauchy (AFP)

17:47:34 Session AFP/Sqrt_Babylonian (AFP)

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

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

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

17:47:34 Session AFP/Constructor_Funs (AFP)

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

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

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

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

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

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

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

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

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

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

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

17:47:34 Session AFP/FunWithFunctions (AFP)

17:47:34 Session AFP/FunWithTilings (AFP)

17:47:34 Session AFP/GPU_Kernel_PL (AFP)

17:47:34 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

17:47:34 Session AFP/GenClock (AFP)

17:47:34 Session AFP/General-Triangle (AFP)

17:47:34 Session AFP/GoedelGod (AFP)

17:47:34 Session HOL/HOL-Eisbach

17:47:35 Session AFP/Allen_Calculus (AFP)

17:47:35 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

17:47:35 Session AFP/Dependent_SIFUM_Refinement (AFP)

17:47:35 Session AFP/Optics (AFP)

17:47:35 Session HOL/HOL-Hoare

17:47:35 Session AFP/Case_Labeling (AFP)

17:47:35 Session HOL/HOL-Library (main timing)

17:47:35 Session AFP/Abs_Int_ITP2012 (AFP)

17:47:35 Session AFP/Abstract_Completeness (AFP)

17:47:35 Session AFP/Abstract_Soundness (AFP)

17:47:35 Session AFP/Amortized_Complexity (AFP)

17:47:35 Session AFP/Dynamic_Tables (AFP)

17:47:35 Session AFP/ArrowImpossibilityGS (AFP)

17:47:35 Session AFP/Automatic_Refinement (AFP)

17:47:35 Session AFP/Bell_Numbers_Spivey (AFP)

17:47:36 Session AFP/Card_Equiv_Relations (AFP)

17:47:36 Session AFP/Binomial-Heaps (AFP)

17:47:36 Session AFP/Boolean_Expression_Checkers (AFP)

17:47:36 Session AFP/Buildings (AFP)

17:47:36 Session AFP/Card_Multisets (AFP)

17:47:36 Session AFP/Card_Number_Partitions (AFP)

17:47:36 Session AFP/Category (AFP)

17:47:36 Session AFP/Category2 (AFP)

17:47:36 Session AFP/Category3 (AFP)

17:47:36 Session AFP/MonoidalCategory (AFP)

17:47:36 Session AFP/Certification_Monads (AFP)

17:47:36 Session AFP/CofGroups (AFP)

17:47:36 Session AFP/Completeness (AFP)

17:47:36 Session AFP/ConcurrentIMP (AFP)

17:47:36 Session AFP/Concurrent_Ref_Alg (AFP)

17:47:36 Session AFP/Consensus_Refined (AFP)

17:47:36 Session AFP/CoreC++ (AFP)

17:47:36 Session AFP/Derangements (AFP)

17:47:37 Session AFP/Dict_Construction (AFP)

17:47:37 Session AFP/Discrete_Summation (AFP)

17:47:37 Session AFP/Card_Partitions (AFP)

17:47:37 Session AFP/Efficient-Mergesort (AFP)

17:47:37 Session AFP/Encodability_Process_Calculi (AFP)

17:47:37 Session AFP/Euler_Partition (AFP)

17:47:37 Session AFP/FOL-Fitting (AFP)

17:47:37 Session AFP/FOL_Harrison (AFP)

17:47:37 Session AFP/FinFun (AFP)

17:47:37 Session AFP/Finger-Trees (AFP)

17:47:37 Session AFP/Free-Boolean-Algebra (AFP)

17:47:37 Session AFP/Graph_Theory (AFP)

17:47:37 Session AFP/ShortestPath (AFP)

17:47:37 Session AFP/Group-Ring-Module (AFP)

17:47:37 Session AFP/Valuation (AFP)

17:47:37 Session HOL/HOL-Cardinals (timing)

17:47:37 Session AFP/Ordinals_and_Cardinals (AFP)

17:47:37 Session AFP/Sort_Encodings (AFP)

17:47:37 Session HOL/HOL-Computational_Algebra (timing)

17:47:38 Session AFP/Bernoulli (AFP)

17:47:38 Session AFP/Descartes_Sign_Rule (AFP)

17:47:38 Session HOL/HOL-Algebra (main timing)

17:47:38 Session AFP/Free-Groups (AFP)

17:47:38 Session AFP/Jordan_Hoelder (AFP)

17:47:38 Session AFP/Perfect-Number-Thm (AFP)

17:47:38 Session AFP/Secondary_Sylow (AFP)

17:47:38 Session AFP/VectorSpace (AFP)

17:47:38 Session HOL/HOL-Analysis (main timing)

17:47:38 Session AFP/Affine_Arithmetic (AFP)

17:47:39 Session AFP/Cartan_FP (AFP)

17:47:39 Session AFP/Cayley_Hamilton (AFP)

17:47:39 Session AFP/Chord_Segments (AFP)

17:47:39 Session AFP/Coinductive (AFP)

17:47:39 Session AFP/Lazy-Lists-II (AFP)

17:47:39 Session AFP/Topology (AFP)

17:47:39 Session AFP/Stream_Fusion_Code (AFP)

17:47:39 Session AFP/Echelon_Form (AFP)

17:47:39 Session AFP/Hermite (AFP)

17:47:39 Session AFP/Gauss_Jordan (AFP)

17:47:39 Session HOL/HOL-Probability (main timing)

17:47:39 Session AFP/Applicative_Lifting (AFP)

17:47:39 Session AFP/Stern_Brocot (AFP)

17:47:39 Session AFP/Buffons_Needle (AFP)

17:47:39 Session AFP/Deep_Learning_Lib (AFP)

17:47:40 Session AFP/Deep_Learning (AFP)

17:47:40 Session AFP/Density_Compiler (AFP)

17:47:40 Session AFP/Ergodic_Theory (AFP)

17:47:40 Session AFP/Fisher_Yates (AFP)

17:47:40 Session AFP/Girth_Chromatic (AFP)

17:47:40 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

17:47:40 Session AFP/Lp (AFP)

17:47:40 Session AFP/MFMC_Countable (AFP)

17:47:40 Session AFP/Markov_Models (AFP)

17:47:40 Session AFP/Monad_Normalisation (AFP)

17:47:40 Session AFP/Monomorphic_Monad (AFP)

17:47:40 Session AFP/Probabilistic_Noninterference (AFP)

17:47:40 Session AFP/Probabilistic_System_Zoo (AFP)

17:47:41 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

17:47:41 Session AFP/Probabilistic_While (AFP)

17:47:41 Session AFP/CryptHOL (AFP)

17:47:41 Session AFP/Game_Based_Crypto (AFP)

17:47:41 Session AFP/Source_Coding_Theorem (AFP)

17:47:41 Session AFP/Landau_Analysis (AFP)

17:47:41 Session AFP/Akra_Bazzi (AFP)

17:47:41 Session AFP/Catalan_Numbers (AFP)

17:47:41 Session AFP/Euler_MacLaurin (AFP)

17:47:41 Session AFP/Stirling_Formula (AFP)

17:47:41 Session AFP/Lower_Semicontinuous (AFP)

17:47:41 Session AFP/Ordinary_Differential_Equations (AFP)

17:47:42 Session AFP/HOL-ODE (AFP)

17:47:42 Session AFP/Differential_Dynamic_Logic (AFP)

17:47:42 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

17:47:42 Session AFP/Ptolemys_Theorem (AFP)

17:47:42 Session AFP/QR_Decomposition (AFP)

17:47:42 Session AFP/Rank_Nullity_Theorem (AFP)

17:47:42 Session AFP/Tarskis_Geometry (AFP)

17:47:42 Session AFP/Triangle (AFP)

17:47:42 Session AFP/pGCL (AFP)

17:47:42 Session HOL/HOL-Number_Theory (timing)

17:47:42 Session AFP/E_Transcendental (AFP)

17:47:42 Session AFP/Elliptic_Curves_Group_Law (AFP)

17:47:42 Session AFP/Fermat3_4 (AFP)

17:47:42 Session AFP/Koenigsberg_Friendship_Base (AFP)

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

17:47:43 Session AFP/Lehmer (AFP)

17:47:43 Session AFP/Pratt_Certificate (AFP)

17:47:43 Session AFP/Bertrands_Postulate (AFP)

17:47:43 Session AFP/Prime_Harmonic_Series (AFP)

17:47:43 Session AFP/RSAPSS (AFP)

17:47:43 Session AFP/SumSquares (AFP)

17:47:43 Session AFP/Liouville_Numbers (AFP)

17:47:43 Session AFP/Polynomial_Interpolation (AFP)

17:47:43 Session AFP/Real_Impl (AFP)

17:47:43 Session AFP/Rep_Fin_Groups (AFP)

17:47:43 Session AFP/Sturm_Sequences (AFP)

17:47:43 Session AFP/Special_Function_Bounds (AFP)

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

17:47:43 Session HOL/HOL-Imperative_HOL

17:47:43 Session AFP/Imperative_Insertion_Sort (AFP)

17:47:44 Session AFP/UpDown_Scheme (AFP)

17:47:44 Session AFP/HereditarilyFinite (AFP)

17:47:44 Session AFP/Incompleteness (AFP)

17:47:44 Session AFP/Surprise_Paradox (AFP)

17:47:44 Session AFP/HyperCTL (AFP)

17:47:44 Session AFP/Incredible_Proof_Machine (AFP)

17:47:44 Session AFP/Integration (AFP)

17:47:44 Session AFP/Isabelle_Meta_Model (AFP)

17:47:44 Session AFP/LTL (AFP)

17:47:44 Session AFP/Stuttering_Equivalence (AFP)

17:47:44 Session AFP/Lambda_Free_RPOs (AFP)

17:47:44 Session AFP/Landau_Symbols (AFP)

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

17:47:44 Session AFP/LinearQuantifierElim (AFP)

17:47:44 Session AFP/List-Infinite (AFP)

17:47:44 Session AFP/Nat-Interval-Logic (AFP)

17:47:44 Session AFP/AutoFocus-Stream (AFP)

17:47:45 Session AFP/MuchAdoAboutTwo (AFP)

17:47:45 Session AFP/POPLmark-deBruijn (AFP)

17:47:45 Session AFP/Pairing_Heap (AFP)

17:47:45 Session AFP/Password_Authentication_Protocol (AFP)

17:47:45 Session AFP/Presburger-Automata (AFP)

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

17:47:45 Session AFP/Program-Conflict-Analysis (AFP)

17:47:45 Session AFP/Regular-Sets (AFP)

17:47:45 Session AFP/Abstract-Rewriting (AFP)

17:47:45 Session AFP/Decreasing-Diagrams (AFP)

17:47:45 Session AFP/Decreasing-Diagrams-II (AFP)

17:47:45 Session AFP/Matrix (AFP)

17:47:45 Session AFP/Matrix_Tensor (AFP)

17:47:45 Session AFP/Knot_Theory (AFP)

17:47:45 Session AFP/Polynomials (AFP)

17:47:45 Session AFP/Groebner_Bases (AFP)

17:47:45 Session AFP/Coinductive_Languages (AFP)

17:47:45 Session AFP/Finite_Automata_HF (AFP)

17:47:45 Session AFP/Functional-Automata (AFP)

17:47:45 Session AFP/Myhill-Nerode (AFP)

17:47:45 Session AFP/Posix-Lexing (AFP)

17:47:45 Session AFP/Regex_Equivalence (AFP)

17:47:46 Session AFP/Regex_Equivalence_Examples (AFP)

17:47:46 Session AFP/Ribbon_Proofs (AFP)

17:47:46 Session AFP/SATSolverVerification (AFP)

17:47:46 Session AFP/Selection_Heap_Sort (AFP)

17:47:46 Session AFP/Separata (AFP)

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

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

17:47:46 Session AFP/Stable_Matching (AFP)

17:47:46 Session AFP/SuperCalc (AFP)

17:47:46 Session AFP/Tail_Recursive_Functions (AFP)

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

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

17:47:46 Session AFP/KBPs (AFP)

17:47:46 Session AFP/Twelvefold_Way (AFP)

17:47:46 Session AFP/Vickrey_Clarke_Groves (AFP)

17:47:46 Session AFP/Well_Quasi_Orders (AFP)

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

17:47:46 Session HOL/HOL-Nominal

17:47:46 Session AFP/CCS (AFP)

17:47:46 Session AFP/Lam-ml-Normalization (AFP)

17:47:46 Session AFP/Pi_Calculus (AFP)

17:47:46 Session AFP/Psi_Calculi (AFP)

17:47:47 Session AFP/SequentInvertibility (AFP)

17:47:47 Session HOL/HOL-Word (main timing)

17:47:47 Session HOL/HOL-SPARK (main)

17:47:47 Session HOL/HOL-SPARK-Examples

17:47:47 Session AFP/RIPEMD-160-SPARK (AFP)

17:47:47 Session AFP/Kleene_Algebra (AFP)

17:47:47 Session AFP/KAT_and_DRA (AFP)

17:47:47 Session AFP/Algebraic_VCs (AFP)

17:47:47 Session AFP/Multirelations (AFP)

17:47:48 Session AFP/Regular_Algebras (AFP)

17:47:48 Session AFP/Relation_Algebra (AFP)

17:47:48 Session AFP/Residuated_Lattices (AFP)

17:47:48 Session AFP/Native_Word (AFP)

17:47:48 Session AFP/Datatype_Order_Generator (AFP)

17:47:48 Session AFP/Old_Datatype_Show (AFP)

17:47:48 Session AFP/Deriving (AFP)

17:47:48 Session AFP/Containers (AFP)

17:47:49 Session AFP/Containers-Benchmarks (AFP)

17:47:49 Session AFP/JNF-HOL-Lib (AFP)

17:47:49 Session AFP/JNF-AFP-Lib (AFP)

17:47:49 Session AFP/Jordan_Normal_Form (AFP)

17:47:49 Session AFP/Pre_Perron_Frobenius (AFP)

17:47:49 Session AFP/Perron_Frobenius (AFP)

17:47:49 Session AFP/Subresultants (AFP)

17:47:50 Session AFP/Pre_Polynomial_Factorization (AFP)

17:47:50 Session AFP/Polynomial_Factorization (AFP)

17:47:50 Session AFP/Show (AFP)

17:47:50 Session AFP/HOL-ODE-Refinement (AFP)

17:47:50 Session AFP/HOL-ODE-Numerics (AFP)

17:47:50 Session AFP/Pre_BZ (AFP)

17:47:51 Session AFP/Berlekamp_Zassenhaus (AFP)

17:47:51 Session AFP/Pre_Algebraic_Numbers (AFP)

17:47:51 Session AFP/Algebraic_Numbers (AFP)

17:47:51 Session AFP/Algebraic_Numbers_Lib (AFP)

17:47:51 Session AFP/Refine_Monadic (AFP)

17:47:51 Session AFP/Collections (AFP)

17:47:51 Session AFP/CAVA_Base (AFP)

17:47:52 Session AFP/CAVA_Automata (AFP)

17:47:52 Session AFP/DFS_Framework (AFP)

17:47:52 Session AFP/Gabow_SCC (AFP)

17:47:52 Session AFP/LTL_to_GBA (AFP)

17:47:52 Session AFP/CAVA_buildchain1 (AFP)

17:47:52 Session AFP/CAVA_buildchain3 (AFP)

17:47:52 Session AFP/CAVA_LTL_Modelchecker (AFP)

17:47:52 Session AFP/Promela (AFP)

17:47:52 Session AFP/Collections_Examples (AFP)

17:47:52 Session AFP/Dijkstra_Shortest_Path (AFP)

17:47:52 Session AFP/Formal_SSA (AFP)

17:47:52 Session AFP/Minimal_SSA (AFP)

17:47:52 Session AFP/Sepref_Prereq (AFP)

17:47:53 Session AFP/Transitive-Closure (AFP)

17:47:53 Session AFP/Tree-Automata (AFP)

17:47:53 Session AFP/SPARCv8 (AFP)

17:47:53 Session AFP/Separation_Algebra (AFP)

17:47:53 Session AFP/Separation_Logic_Imperative_HOL (AFP)

17:47:53 Session AFP/Word_Lib (AFP)

17:47:53 Session AFP/Complx (AFP)

17:47:53 Session AFP/IP_Addresses (AFP)

17:47:54 Session AFP/Simple_Firewall (AFP)

17:47:54 Session AFP/Routing (AFP)

17:47:54 Session AFP/Iptables_Semantics (AFP)

17:47:54 Session AFP/LOFT (AFP)

17:47:54 Session HOL/HOLCF (main timing)

17:47:54 Session AFP/Circus (AFP)

17:47:54 Session AFP/HOLCF-HOL-Library (AFP)

17:47:54 Session AFP/HOLCF-Nominal2 (AFP)

17:47:54 Session AFP/Launchbury (AFP)

17:47:54 Session AFP/Call_Arity (AFP)

17:47:54 Session HOL/HOLCF-Library

17:47:54 Session AFP/PCF (AFP)

17:47:54 Session AFP/Shivers-CFA (AFP)

17:47:55 Session AFP/Stream-Fusion (AFP)

17:47:55 Session AFP/Tycon (AFP)

17:47:55 Session AFP/WorkerWrapper (AFP)

17:47:55 Session AFP/Heard_Of (AFP)

17:47:55 Session AFP/HotelKeyCards (AFP)

17:47:55 Session AFP/Huffman (AFP)

17:47:55 Session AFP/IEEE_Floating_Point (AFP)

17:47:55 Session AFP/Impossible_Geometry (AFP)

17:47:55 Session AFP/Inductive_Confidentiality (AFP)

17:47:55 Session AFP/InfPathElimination (AFP)

17:47:55 Session AFP/JiveDataStoreModel (AFP)

17:47:55 Session AFP/KAD (AFP)

17:47:55 Session AFP/Key_Agreement_Strong_Adversaries (AFP)

17:47:55 Session AFP/LatticeProperties (AFP)

17:47:55 Session AFP/DataRefinementIBP (AFP)

17:47:55 Session AFP/GraphMarkingIBP (AFP)

17:47:55 Session AFP/MonoBoolTranAlgebra (AFP)

17:47:55 Session AFP/PseudoHoops (AFP)

17:47:55 Session AFP/Lazy_Case (AFP)

17:47:55 Session AFP/Lifting_Definition_Option (AFP)

17:47:55 Session AFP/List-Index (AFP)

17:47:55 Session AFP/Comparison_Sort_Lower_Bound (AFP)

17:47:55 Session AFP/Formula_Derivatives (AFP)

17:47:55 Session AFP/Formula_Derivatives-Examples (AFP)

17:47:55 Session AFP/Jinja (AFP)

17:47:55 Session AFP/HRB-Slicing (AFP)

17:47:55 Session AFP/InformationFlowSlicing_Inter (AFP)

17:47:55 Session AFP/Slicing (AFP)

17:47:55 Session AFP/InformationFlowSlicing (AFP)

17:47:56 Session AFP/LTL_to_DRA (AFP)

17:47:56 Session AFP/List_Update (AFP)

17:47:56 Session AFP/MSO_Regex_Equivalence (AFP)

17:47:56 Session AFP/MSO_Examples (AFP)

17:47:56 Session AFP/Quick_Sort_Cost (AFP)

17:47:56 Session AFP/Random_BSTs (AFP)

17:47:56 Session AFP/Randomised_Social_Choice (AFP)

17:47:56 Session AFP/SDS_Impossibility (AFP)

17:47:56 Session AFP/Refine_Imperative_HOL (AFP)

17:47:56 Session AFP/Floyd_Warshall (AFP)

17:47:56 Session AFP/Sepref_Basic (AFP)

17:47:56 Session AFP/Sepref_IICF (AFP)

17:47:56 Session AFP/Maxflow_Lib (AFP)

17:47:57 Session AFP/Flow_Networks (AFP)

17:47:57 Session AFP/EdmondsKarp_Maxflow (AFP)

17:47:57 Session AFP/Prpu_Maxflow (AFP)

17:47:57 Session AFP/List_Interleaving (AFP)

17:47:57 Session AFP/LocalLexing (AFP)

17:47:57 Session AFP/Locally-Nameless-Sigma (AFP)

17:47:57 Session AFP/Marriage (AFP)

17:47:57 Session AFP/Latin_Square (AFP)

17:47:57 Session AFP/Max-Card-Matching (AFP)

17:47:57 Session AFP/Menger (AFP)

17:47:57 Session AFP/MiniML (AFP)

17:47:57 Session AFP/Network_Security_Policy_Verification (AFP)

17:47:57 Session AFP/No_FTL_observers (AFP)

17:47:57 Session AFP/Nominal2 (AFP)

17:47:57 Session AFP/Modal_Logics_for_NTS (AFP)

17:47:58 Session AFP/Rewriting_Z (AFP)

17:47:58 Session AFP/Noninterference_CSP (AFP)

17:47:58 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

17:47:58 Session AFP/Noninterference_Generic_Unwinding (AFP)

17:47:58 Session AFP/Noninterference_Inductive_Unwinding (AFP)

17:47:58 Session AFP/Noninterference_Sequential_Composition (AFP)

17:47:58 Session AFP/Noninterference_Concurrent_Composition (AFP)

17:47:58 Session AFP/NormByEval (AFP)

17:47:58 Session AFP/Open_Induction (AFP)

17:47:58 Session AFP/Ordinal (AFP)

17:47:58 Session AFP/Nested_Multisets_Ordinals (AFP)

17:47:58 Session AFP/Lambda_Free_KBOs (AFP)

17:47:58 Session AFP/Paraconsistency (AFP)

17:47:58 Session AFP/Parity_Game (AFP)

17:47:59 Session AFP/Partial_Function_MR (AFP)

17:47:59 Session AFP/Pop_Refinement (AFP)

17:47:59 Session AFP/Possibilistic_Noninterference (AFP)

17:47:59 Session AFP/Proof_Strategy_Language (AFP)

17:47:59 Session AFP/PropResPI (AFP)

17:47:59 Session AFP/ROBDD (AFP)

17:47:59 Session AFP/Ramsey-Infinite (AFP)

17:47:59 Session AFP/Recursion-Theory-I (AFP)

17:47:59 Session AFP/RefinementReactive (AFP)

17:47:59 Session AFP/Resolution_FOL (AFP)

17:47:59 Session AFP/Robbins-Conjecture (AFP)

17:47:59 Session AFP/Roy_Floyd_Warshall (AFP)

17:47:59 Session AFP/SIFPL (AFP)

17:47:59 Session AFP/SIFUM_Type_Systems (AFP)

17:47:59 Session AFP/Security_Protocol_Refinement (AFP)

17:47:59 Session AFP/SenSocialChoice (AFP)

17:47:59 Session AFP/Simpl (AFP)

17:48:00 Session AFP/BDD (AFP)

17:48:00 Session AFP/Planarity_Certificates (AFP)

17:48:00 Session AFP/Statecharts (AFP)

17:48:00 Session AFP/Stone_Algebras (AFP)

17:48:00 Session AFP/Stone_Relation_Algebras (AFP)

17:48:00 Session AFP/Strong_Security (AFP)

17:48:00 Session AFP/TLA (AFP)

17:48:00 Session AFP/Timed_Automata (AFP)

17:48:00 Session AFP/Transitive-Closure-II (AFP)

17:48:00 Session AFP/Tree_Decomposition (AFP)

17:48:00 Session AFP/Types_Tableaus_and_Goedels_God (AFP)

17:48:00 Session AFP/UPF (AFP)

17:48:00 Session AFP/UPF_Firewall (AFP)

17:48:00 Session AFP/Verified-Prover (AFP)

17:48:00 Session AFP/VolpanoSmith (AFP)

17:48:00 Session AFP/WHATandWHERE_Security (AFP)

17:48:03 Building HOL ...

17:48:04 HOL: theory HOL.Code_Generator

17:48:06 HOL: theory HOL.HOL

17:48:09 HOL: theory HOL.Argo

17:48:09 HOL: theory HOL.Ctr_Sugar

17:48:10 HOL: theory HOL.Orderings

17:48:10 HOL: theory HOL.SAT

17:48:11 HOL: theory HOL.Groups

17:48:14 HOL: theory HOL.Lattices

17:48:15 HOL: theory HOL.Set

17:48:17 HOL: theory HOL.Fun

17:48:17 HOL: theory HOL.Typedef

17:48:17 HOL: theory HOL.Rings

17:48:17 HOL: theory HOL.Complete_Lattices

17:48:20 HOL: theory HOL.Inductive

17:48:21 HOL: theory HOL.Product_Type

17:48:22 HOL: theory HOL.Complete_Partial_Order

17:48:23 HOL: theory HOL.Sum_Type

17:48:26 HOL: theory HOL.Nat

17:48:27 HOL: theory HOL.Fields

17:48:27 HOL: theory HOL.Meson

17:48:28 HOL: theory HOL.ATP

17:48:30 HOL: theory HOL.Metis

17:48:32 HOL: theory HOL.Finite_Set

17:48:33 HOL: theory HOL.Relation

17:48:34 HOL: theory HOL.Transitive_Closure

17:48:35 HOL: theory HOL.Wellfounded

17:48:35 HOL: theory HOL.Fun_Def_Base

17:48:35 HOL: theory HOL.Hilbert_Choice

17:48:35 HOL: theory HOL.Wfrec

17:48:35 HOL: theory HOL.Order_Relation

17:48:36 HOL: theory HOL.BNF_Wellorder_Relation

17:48:36 HOL: theory HOL.Zorn

17:48:36 HOL: theory HOL.BNF_Wellorder_Embedding

17:48:36 HOL: theory HOL.BNF_Wellorder_Constructions

17:48:37 HOL: theory HOL.BNF_Cardinal_Order_Relation

17:48:37 HOL: theory HOL.BNF_Cardinal_Arithmetic

17:48:38 HOL: theory HOL.BNF_Def

17:48:39 HOL: theory HOL.BNF_Composition

17:48:40 HOL: theory HOL.Basic_BNFs

17:48:40 HOL: theory HOL.BNF_Fixpoint_Base

17:48:42 HOL: theory HOL.BNF_Least_Fixpoint

17:48:44 HOL: theory HOL.Basic_BNF_LFPs

17:48:44 HOL: theory HOL.Transfer

17:48:45 HOL: theory HOL.Num

17:48:48 HOL: theory HOL.Power

17:48:50 HOL: theory HOL.Groups_Big

17:48:52 HOL: theory HOL.Equiv_Relations

17:48:52 HOL: theory HOL.Lifting

17:48:53 HOL: theory HOL.Lifting_Set

17:48:53 HOL: theory HOL.Option

17:48:54 HOL: theory HOL.Extraction

17:48:55 HOL: theory HOL.Lattices_Big

17:48:56 HOL: theory HOL.Partial_Function

17:48:56 HOL: theory HOL.Quotient

17:48:57 HOL: theory HOL.Fun_Def

17:48:58 HOL: theory HOL.Int

17:49:00 HOL: theory HOL.Nat_Transfer

17:49:00 HOL: theory HOL.Euclidean_Division

17:49:04 HOL: theory HOL.Parity

17:49:06 HOL: theory HOL.Divides

17:49:12 HOL: theory HOL.Code_Numeral

17:49:12 HOL: theory HOL.Numeral_Simprocs

17:49:13 HOL: theory HOL.SMT

17:49:13 HOL: theory HOL.Semiring_Normalization

17:49:14 HOL: theory HOL.Set_Interval

17:49:15 HOL: theory HOL.Groebner_Basis

17:49:17 HOL: theory HOL.Conditionally_Complete_Lattices

17:49:18 HOL: theory HOL.Filter

17:49:19 HOL: theory HOL.Presburger

17:49:21 HOL: theory HOL.Sledgehammer

17:49:22 HOL: theory HOL.List

17:49:29 HOL: theory HOL.Groups_List

17:49:29 HOL: theory HOL.Map

17:49:30 HOL: theory HOL.Factorial

17:49:30 HOL: theory HOL.GCD

17:49:30 HOL: theory HOL.Binomial

17:49:30 HOL: theory HOL.Enum

17:49:33 HOL: theory HOL.String

17:49:33 HOL: theory HOL.BNF_Greatest_Fixpoint

17:49:35 HOL: theory HOL.Predicate

17:49:36 HOL: theory HOL.Lazy_Sequence

17:49:37 HOL: theory HOL.Typerep

17:49:37 HOL: theory HOL.Limited_Sequence

17:49:38 HOL: theory HOL.Random

17:49:38 HOL: theory HOL.Code_Evaluation

17:49:39 HOL: theory HOL.Quickcheck_Random

17:49:41 HOL: theory HOL.Quickcheck_Exhaustive

17:49:41 HOL: theory HOL.Quickcheck_Narrowing

17:49:45 HOL: theory HOL.Random_Pred

17:49:45 HOL: theory HOL.Record

17:49:45 HOL: theory HOL.Random_Sequence

17:49:46 HOL: theory HOL.Predicate_Compile

17:49:46 HOL: theory HOL.Nitpick

17:49:51 HOL: theory Main

17:49:53 HOL: theory HOL.Archimedean_Field

17:49:53 HOL: theory HOL.Topological_Spaces

17:49:57 HOL: theory HOL.Rat

17:49:59 HOL: theory HOL.Real

17:50:01 HOL: theory HOL.Real_Vector_Spaces

17:50:12 HOL: theory HOL.Inequalities

17:50:12 HOL: theory HOL.Limits

17:50:15 HOL: theory HOL.Deriv

17:50:15 HOL: theory HOL.Series

17:50:20 HOL: theory HOL.NthRoot

17:50:21 HOL: theory HOL.Transcendental

17:50:25 HOL: theory HOL.Complex

17:50:25 HOL: theory HOL.MacLaurin

17:50:26 HOL: theory Complex_Main

17:52:50 Timing HOL (2 threads, 211.418s elapsed time, 403.656s cpu time, 36.176s GC time, factor 1.91)

17:52:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL

17:52:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/document.pdf

17:52:50 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/outline.pdf

17:52:50 Finished HOL (0:04:46 elapsed time, 0:08:44 cpu time, factor 1.83)

17:52:52 Building HOL-Library ...

17:52:53 Building HOLCF ...

17:52:53 Building HOL-Word ...

17:52:53 Building HOL-Nominal ...

17:52:53 Building Simpl ...

17:52:53 Building Nominal2 ...

17:52:53 Building LatticeProperties ...

17:52:53 Building Dependent_SIFUM_Type_Systems ...

17:52:55 HOLCF: theory HOLCF.Old_Datatype

17:52:55 HOLCF: theory HOLCF.Nat_Bijection

17:52:55 HOL-Nominal: theory HOL-Nominal.Infinite_Set

17:52:55 HOL-Nominal: theory HOL-Nominal.Old_Datatype

17:52:55 HOL-Word: theory HOL-Word.Bit

17:52:55 HOL-Word: theory HOL-Word.Bits

17:52:55 LatticeProperties: theory LatticeProperties.Conj_Disj

17:52:55 LatticeProperties: theory LatticeProperties.Lattice_Prop

17:52:55 Nominal2: theory Nominal2.FSet

17:52:55 Nominal2: theory Nominal2.Infinite_Set

17:52:55 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Preliminaries

17:52:55 HOL-Library: theory HOL-Library.Adhoc_Overloading

17:52:55 HOL-Library: theory HOL-Library.Preorder

17:52:55 HOL-Word: theory HOL-Word.Boolean_Algebra

17:52:55 HOL-Library: theory HOL-Library.Lattice_Syntax

17:52:55 HOL-Library: theory HOL-Library.AList

17:52:55 Simpl: theory Simpl.Cancellation

17:52:55 Simpl: theory Simpl.DistinctTreeProver

17:52:55 LatticeProperties: theory LatticeProperties.WellFoundedTransitive

17:52:55 HOL-Library: theory HOL-Library.BNF_Axiomatization

17:52:55 LatticeProperties: theory LatticeProperties.Modular_Distrib_Lattice

17:52:55 Nominal2: theory Nominal2.Old_Datatype

17:52:55 HOL-Library: theory HOL-Library.BNF_Corec

17:52:55 HOL-Word: theory HOL-Word.Bits_Bit

17:52:55 HOL-Word: theory HOL-Word.Misc_Numeric

17:52:55 LatticeProperties: theory LatticeProperties.Complete_Lattice_Prop

17:52:56 HOL-Word: theory HOL-Word.Bit_Representation

17:52:56 HOL-Word: theory HOL-Word.Word_Miscellaneous

17:52:56 Simpl: theory Simpl.Multiset

17:52:56 HOLCF: theory HOLCF.Countable

17:52:56 HOL-Word: theory HOL-Word.Misc_Typedef

17:52:56 HOL-Word: theory HOL-Word.Bits_Int

17:52:56 HOL-Nominal: theory HOL-Nominal.Nominal

17:52:56 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Language

17:52:56 HOL-Word: theory HOL-Word.Phantom_Type

17:52:56 Simpl: theory Simpl.Generalise

17:52:57 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Security

17:52:57 Nominal2: theory Nominal2.Phantom_Type

17:52:57 Simpl: theory Simpl.StateFun

17:52:57 HOL-Library: theory HOL-Library.DAList

17:52:57 Simpl: theory Simpl.StateSpaceLocale

17:52:57 HOL-Word: theory HOL-Word.Cardinality

17:52:57 Simpl: theory Simpl.StateSpaceSyntax

17:52:57 Nominal2: theory Nominal2.Cardinality

17:52:57 LatticeProperties: theory LatticeProperties.Lattice_Ordered_Group

17:52:57 Simpl: theory Simpl.LaTeXsugar

17:52:58 Simpl: theory Simpl.Old_Recdef

17:52:58 HOLCF: theory HOLCF.Porder

17:52:58 HOL-Word: theory HOL-Word.Bool_List_Representation

17:52:58 HOLCF: theory HOLCF.Pcpo

17:52:58 HOL-Library: theory HOL-Library.Bit

17:52:58 HOL-Word: theory HOL-Word.Numeral_Type

17:52:59 Nominal2: theory Nominal2.FinFun

17:52:59 Simpl: theory Simpl.Language

17:52:59 HOL-Library: theory HOL-Library.Boolean_Algebra

17:52:59 HOL-Library: theory HOL-Library.Cancellation

17:53:00 HOL-Word: theory HOL-Word.Type_Length

17:53:00 HOL-Word: theory HOL-Word.Word

17:53:00 HOLCF: theory HOLCF.Cont

17:53:00 HOL-Library: theory HOL-Library.Multiset

17:53:00 HOLCF: theory HOLCF.Adm

17:53:00 HOLCF: theory HOLCF.Discrete

17:53:00 HOLCF: theory HOLCF.Cpodef

17:53:00 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Compositionality

17:53:01 HOLCF: theory HOLCF.Fun_Cpo

17:53:01 HOLCF: theory HOLCF.Product_Cpo

17:53:01 Simpl: theory Simpl.Permutation

17:53:01 HOLCF: theory HOLCF.Cfun

17:53:01 Simpl: theory Simpl.Simpl_Heap

17:53:01 HOL-Library: theory HOL-Library.Cardinal_Notations

17:53:01 Simpl: theory Simpl.HeapList

17:53:02 HOL-Library: theory HOL-Library.Char_ord

17:53:02 HOL-Library: theory HOL-Library.Code_Abstract_Nat

17:53:02 HOL-Library: theory HOL-Library.Code_Binary_Nat

17:53:02 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.LocallySoundModeUse

17:53:02 HOL-Library: theory HOL-Library.Code_Target_Nat

17:53:02 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystem

17:53:02 HOLCF: theory HOLCF.Completion

17:53:02 HOLCF: theory HOLCF.Cprod

17:53:02 HOLCF: theory HOLCF.Deflation

17:53:03 HOL-Library: theory HOL-Library.Code_Char

17:53:03 HOLCF: theory HOLCF.Fix

17:53:03 HOL-Library: theory HOL-Library.Code_Prolog

17:53:03 HOLCF: theory HOLCF.Sfun

17:53:03 HOLCF: theory HOLCF.Sprod

17:53:03 HOLCF: theory HOLCF.Up

17:53:03 HOL-Library: theory HOL-Library.Code_Target_Int

17:53:03 HOL-Library: theory HOL-Library.Code_Target_Numeral

17:53:04 HOL-Library: theory HOL-Library.Code_Test

17:53:04 HOLCF: theory HOLCF.Lift

17:53:04 HOLCF: theory HOLCF.One

17:53:04 HOLCF: theory HOLCF.Tr

17:53:04 HOL-Library: theory HOL-Library.Combine_PER

17:53:04 HOLCF: theory HOLCF.Ssum

17:53:05 HOL-Library: theory HOL-Library.Complete_Partial_Order2

17:53:05 HOLCF: theory HOLCF.Fixrec

17:53:05 HOLCF: theory HOLCF.Map_Functions

17:53:05 HOL-Library: theory HOL-Library.DAList_Multiset

17:53:06 HOLCF: theory HOLCF.Bifinite

17:53:06 HOL-Library: theory HOL-Library.Multiset_Order

17:53:06 Simpl: theory Simpl.Semantic

17:53:06 HOL-Library: theory HOL-Library.Permutation

17:53:06 HOLCF: theory HOLCF.Domain_Aux

17:53:06 HOL-Library: theory HOL-Library.Debug

17:53:07 HOL-Library: theory HOL-Library.Disjoint_Sets

17:53:07 HOL-Library: theory HOL-Library.Permutations

17:53:07 HOLCF: theory HOLCF.Universal

17:53:08 Nominal2: theory Nominal2.Cancellation

17:53:08 Nominal2: theory Nominal2.Quotient_Syntax

17:53:08 HOL-Library: theory HOL-Library.Dlist

17:53:08 HOL-Library: theory HOL-Library.FSet

17:53:08 Nominal2: theory Nominal2.Quotient_Option

17:53:08 Nominal2: theory Nominal2.Quotient_Product

17:53:08 Nominal2: theory Nominal2.Quotient_Set

17:53:08 Nominal2: theory Nominal2.Multiset

17:53:08 Nominal2: theory Nominal2.Quotient_List

17:53:09 HOLCF: theory HOLCF.Algebraic

17:53:09 HOLCF: theory HOLCF.Compact_Basis

17:53:09 HOLCF: theory HOLCF.LowerPD

17:53:09 HOL-Library: theory HOL-Library.Fun_Lexorder

17:53:09 HOLCF: theory HOLCF.UpperPD

17:53:09 HOL-Library: theory HOL-Library.FuncSet

17:53:10 HOLCF: theory HOLCF.Representable

17:53:10 HOL-Library: theory HOL-Library.Function_Algebras

17:53:10 HOLCF: theory HOLCF.ConvexPD

17:53:10 Simpl: theory Simpl.HoarePartialDef

17:53:10 HOL-Library: theory HOL-Library.Function_Division

17:53:10 Simpl: theory Simpl.Termination

17:53:10 HOL-Library: theory HOL-Library.Groups_Big_Fun

17:53:10 Simpl: theory Simpl.HoarePartialProps

17:53:11 Simpl: theory Simpl.HoareTotalDef

17:53:11 HOL-Library: theory HOL-Library.IArray

17:53:11 Simpl: theory Simpl.HoarePartial

17:53:12 HOL-Library: theory HOL-Library.Finite_Map

17:53:12 Simpl: theory Simpl.AlternativeSmallStep

17:53:12 HOL-Library: theory HOL-Library.Infinite_Set

17:53:12 HOL-Library: theory HOL-Library.Omega_Words_Fun

17:53:12 HOLCF: theory HOLCF.Domain

17:53:13 HOL-Library: theory HOL-Library.Ramsey

17:53:13 HOL-Library: theory HOL-Library.LaTeXsugar

17:53:13 Simpl: theory Simpl.SmallStep

17:53:13 HOL-Library: theory HOL-Library.Lattice_Constructions

17:53:13 Nominal2: theory Nominal2.Nominal2_Base

17:53:13 Timing LatticeProperties (2 threads, 3.864s elapsed time, 7.176s cpu time, 0.152s GC time, factor 1.86)

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

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

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

17:53:13 Finished LatticeProperties (0:00:20 elapsed time, 0:00:31 cpu time, factor 1.52)

17:53:13 Building Automatic_Refinement ...

17:53:14 HOLCF: theory HOLCF.Powerdomains

17:53:14 HOL-Library: theory HOL-Library.ListVector

17:53:14 HOL-Library: theory HOL-Library.List_lexord

17:53:14 HOL-Library: theory HOL-Library.Mapping

17:53:15 Simpl: theory Simpl.HoareTotalProps

17:53:15 HOLCF: theory HOLCF

17:53:15 HOL-Library: theory HOL-Library.AList_Mapping

17:53:15 HOL-Library: theory HOL-Library.Monad_Syntax

17:53:16 Automatic_Refinement: theory Automatic_Refinement.Eisbach

17:53:16 Automatic_Refinement: theory Automatic_Refinement.Cancellation

17:53:16 HOL-Library: theory HOL-Library.More_List

17:53:16 HOL-Library: theory HOL-Library.Nat_Bijection

17:53:16 Simpl: theory Simpl.Compose

17:53:16 Simpl: theory Simpl.HoareTotal

17:53:16 Automatic_Refinement: theory Automatic_Refinement.Foldi

17:53:16 Automatic_Refinement: theory Automatic_Refinement.Multiset

17:53:16 Automatic_Refinement: theory Automatic_Refinement.Infinite_Set

17:53:16 HOL-Library: theory HOL-Library.Old_Datatype

17:53:16 HOL-Library: theory HOL-Library.Stream

17:53:17 Automatic_Refinement: theory Automatic_Refinement.Omega_Words_Fun

17:53:17 Simpl: theory Simpl.Hoare

17:53:17 Automatic_Refinement: theory Automatic_Refinement.Option_ord

17:53:17 HOL-Library: theory HOL-Library.Old_Recdef

17:53:18 Timing HOL-Nominal (2 threads, 8.113s elapsed time, 15.976s cpu time, 0.768s GC time, factor 1.97)

17:53:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Nominal

17:53:18 Finished HOL-Nominal (0:00:24 elapsed time, 0:00:40 cpu time, factor 1.63)

17:53:18 Simpl: theory Simpl.Closure

17:53:18 Building Stone_Algebras ...

17:53:18 Simpl: theory Simpl.StateSpace

17:53:18 HOL-Library: theory HOL-Library.Option_ord

17:53:18 Automatic_Refinement: theory Automatic_Refinement.Prio_List

17:53:18 Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1

17:53:18 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot

17:53:18 Nominal2: theory Nominal2.Atoms

17:53:18 Nominal2: theory Nominal2.Eqvt

17:53:18 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot

17:53:18 HOL-Library: theory HOL-Library.Parallel

17:53:18 Nominal2: theory Nominal2.Nominal2_Abs

17:53:18 Automatic_Refinement: theory Automatic_Refinement.Refine_Util

17:53:18 HOL-Library: theory HOL-Library.Perm

17:53:18 Simpl: theory Simpl.Vcg

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars

17:53:19 HOL-Library: theory HOL-Library.Phantom_Type

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver

17:53:19 Automatic_Refinement: theory Automatic_Refinement.Select_Solve

17:53:20 Stone_Algebras: theory Stone_Algebras.Lattice_Basics

17:53:20 HOL-Library: theory HOL-Library.Cardinality

17:53:20 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

17:53:20 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

17:53:20 HOL-Library: theory HOL-Library.Product_Lexorder

17:53:21 HOL-Library: theory HOL-Library.Product_Plus

17:53:21 HOL-Library: theory HOL-Library.Numeral_Type

17:53:21 HOL-Library: theory HOL-Library.Product_Order

17:53:21 Simpl: theory Simpl.ProcParEx

17:53:21 Nominal2: theory Nominal2.Nominal2_FCB

17:53:21 Simpl: theory Simpl.ProcParExSP

17:53:21 Nominal2: theory Nominal2.Nominal2

17:53:21 HOL-Library: theory HOL-Library.Finite_Lattice

17:53:21 Automatic_Refinement: theory Automatic_Refinement.Quicksort

17:53:22 Simpl: theory Simpl.XVcg

17:53:22 Simpl: theory Simpl.XVcgEx

17:53:22 Automatic_Refinement: theory Automatic_Refinement.Misc

17:53:22 HOL-Library: theory HOL-Library.Type_Length

17:53:22 Simpl: theory Simpl.ClosureEx

17:53:22 HOL-Library: theory HOL-Library.Saturated

17:53:23 Simpl: theory Simpl.ComposeEx

17:53:23 HOL-Library: theory HOL-Library.Quotient_Syntax

17:53:23 HOL-Library: theory HOL-Library.Quotient_Option

17:53:23 HOL-Library: theory HOL-Library.Quotient_Product

17:53:23 HOL-Library: theory HOL-Library.Quotient_Set

17:53:23 HOL-Library: theory HOL-Library.Quotient_List

17:53:23 Simpl: theory Simpl.Quicksort

17:53:24 HOL-Library: theory HOL-Library.Quotient_Sum

17:53:24 HOL-Library: theory HOL-Library.Quotient_Type

17:53:24 Simpl: theory Simpl.SyntaxTest

17:53:24 HOL-Library: theory HOL-Library.RBT_Impl

17:53:25 Simpl: theory Simpl.UserGuide

17:53:25 Simpl: theory Simpl.VcgEx

17:53:27 HOL-Library: theory HOL-Library.Reflection

17:53:27 HOL-Library: theory HOL-Library.Refute

17:53:28 Stone_Algebras: theory Stone_Algebras.Filters

17:53:28 Stone_Algebras: theory Stone_Algebras.P_Algebras

17:53:28 Automatic_Refinement: theory Automatic_Refinement.Digraph_Basic

17:53:28 HOL-Library: theory HOL-Library.Rewrite

17:53:28 Simpl: theory Simpl.VcgExSP

17:53:28 HOL-Library: theory HOL-Library.Set_Algebras

17:53:29 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib

17:53:29 HOL-Library: theory HOL-Library.Simps_Case_Conv

17:53:29 HOL-Library: theory HOL-Library.Extended

17:53:30 Simpl: theory Simpl.VcgExTotal

17:53:31 HOL-Library: theory HOL-Library.State_Monad

17:53:31 HOL-Library: theory HOL-Library.Stirling

17:53:32 HOL-Library: theory HOL-Library.Sublist

17:53:32 Simpl: theory Simpl.Simpl

17:53:33 HOL-Library: theory HOL-Library.Prefix_Order

17:53:33 HOL-Library: theory HOL-Library.Subseq_Order

17:53:33 HOL-Library: theory HOL-Library.Transitive_Closure_Table

17:53:34 HOL-Library: theory HOL-Library.Tree

17:53:37 Timing HOL-Word (2 threads, 20.786s elapsed time, 40.676s cpu time, 1.620s GC time, factor 1.96)

17:53:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word

17:53:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/document.pdf

17:53:37 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/outline.pdf

17:53:37 Finished HOL-Word (0:00:43 elapsed time, 0:01:15 cpu time, factor 1.72)

17:53:37 Building Kleene_Algebra ...

17:53:37 HOL-Library: theory HOL-Library.Tree_Multiset

17:53:38 HOL-Library: theory HOL-Library.While_Combinator

17:53:39 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

17:53:39 HOL-Library: theory HOL-Library.Countable

17:53:39 Kleene_Algebra: theory Kleene_Algebra.Signatures

17:53:39 Timing HOLCF (2 threads, 20.289s elapsed time, 37.000s cpu time, 1.964s GC time, factor 1.82)

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

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

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

17:53:39 Finished HOLCF (0:00:46 elapsed time, 0:01:16 cpu time, factor 1.65)

17:53:40 Kleene_Algebra: theory Kleene_Algebra.Dioid

17:53:40 Building Word_Lib ...

17:53:41 HOL-Library: theory HOL-Library.Countable_Set

17:53:41 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

17:53:42 Word_Lib: theory Word_Lib.WordBitwise

17:53:42 Word_Lib: theory Word_Lib.Sublist

17:53:44 Word_Lib: theory Word_Lib.Prefix_Order

17:53:44 HOL-Library: theory HOL-Library.Countable_Set_Type

17:53:46 HOL-Library: theory HOL-Library.BigO

17:53:47 Word_Lib: theory Word_Lib.Hex_Words

17:53:47 Word_Lib: theory Word_Lib.Signed_Words

17:53:47 Word_Lib: theory Word_Lib.Enumeration

17:53:47 Word_Lib: theory Word_Lib.Norm_Words

17:53:47 Word_Lib: theory Word_Lib.WordBitwise_Signed

17:53:48 Word_Lib: theory Word_Lib.Word_Syntax

17:53:48 Word_Lib: theory Word_Lib.HOL_Lemmas

17:53:48 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

17:53:48 Word_Lib: theory Word_Lib.More_Divides

17:53:48 Word_Lib: theory Word_Lib.Word_Lib

17:53:48 HOL-Library: theory HOL-Library.Diagonal_Subsequence

17:53:49 HOL-Library: theory HOL-Library.Discrete

17:53:49 Word_Lib: theory Word_Lib.Word_Enum

17:53:49 Word_Lib: theory Word_Lib.Aligned

17:53:49 HOL-Library: theory HOL-Library.Function_Growth

17:53:49 Word_Lib: theory Word_Lib.Word_Setup_32

17:53:49 Word_Lib: theory Word_Lib.Word_Setup_64

17:53:49 Word_Lib: theory Word_Lib.Word_Lemmas

17:53:50 HOL-Library: theory HOL-Library.Indicator_Function

17:53:51 HOL-Library: theory HOL-Library.Lattice_Algebras

17:53:52 Stone_Algebras: theory Stone_Algebras.Stone_Construction

17:53:54 Kleene_Algebra: theory Kleene_Algebra.Conway

17:53:54 Kleene_Algebra: theory Kleene_Algebra.Dioid_Models

17:53:54 Word_Lib: theory Word_Lib.Word_Lemmas_32

17:53:55 Word_Lib: theory Word_Lib.Word_Lemmas_64

17:53:57 HOL-Library: theory HOL-Library.Liminf_Limsup

17:53:58 HOL-Library: theory HOL-Library.Log_Nat

17:53:58 HOL-Library: theory HOL-Library.Float

17:53:58 Timing Nominal2 (2 threads, 34.299s elapsed time, 66.600s cpu time, 2.976s GC time, factor 1.94)

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

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

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

17:53:58 Finished Nominal2 (0:01:04 elapsed time, 0:01:53 cpu time, factor 1.75)

17:53:59 Building UPF ...

17:54:00 HOL-Library: theory HOL-Library.RBT

17:54:01 UPF: theory UPF.Monads

17:54:01 HOL-Library: theory HOL-Library.RBT_Mapping

17:54:01 Kleene_Algebra: theory Kleene_Algebra.Finite_Suprema

17:54:01 HOL-Library: theory HOL-Library.RBT_Set

17:54:01 Kleene_Algebra: theory Kleene_Algebra.Inf_Matrix

17:54:01 HOL-Library: theory HOL-Library.Lub_Glb

17:54:02 HOL-Library: theory HOL-Library.Multiset_Permutations

17:54:02 UPF: theory UPF.UPFCore

17:54:02 Kleene_Algebra: theory Kleene_Algebra.Matrix

17:54:02 HOL-Library: theory HOL-Library.Nonpos_Ints

17:54:02 HOL-Library: theory HOL-Library.OptionalSugar

17:54:03 HOL-Library: theory HOL-Library.Order_Continuity

17:54:03 HOL-Library: theory HOL-Library.Periodic_Fun

17:54:03 UPF: theory UPF.ElementaryPolicies

17:54:03 HOL-Library: theory HOL-Library.Quadratic_Discriminant

17:54:03 UPF: theory UPF.ParallelComposition

17:54:03 UPF: theory UPF.SeqComposition

17:54:03 HOL-Library: theory HOL-Library.Sum_of_Squares

17:54:04 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra

17:54:04 HOL-Library: theory HOL-Library.Extended_Nat

17:54:04 UPF: theory UPF.Analysis

17:54:05 UPF: theory UPF.Normalisation

17:54:05 HOL-Library: theory HOL-Library.Extended_Real

17:54:06 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

17:54:07 UPF: theory UPF.NormalisationTestSpecification

17:54:07 UPF: theory UPF.UPF

17:54:08 UPF: theory UPF.Service

17:54:08 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter

17:54:08 Automatic_Refinement: theory Automatic_Refinement.Relators

17:54:09 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

17:54:09 Automatic_Refinement: theory Automatic_Refinement.Param_Tool

17:54:10 Automatic_Refinement: theory Automatic_Refinement.Param_HOL

17:54:11 Automatic_Refinement: theory Automatic_Refinement.Parametricity

17:54:11 Kleene_Algebra: theory Kleene_Algebra.DRA

17:54:11 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra

17:54:12 HOL-Library: theory HOL-Library.Library

17:54:12 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data

17:54:12 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases

17:54:12 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging

17:54:12 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops

17:54:13 Kleene_Algebra: theory Kleene_Algebra.PHL_KA

17:54:13 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel

17:54:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate

17:54:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface

17:54:14 Kleene_Algebra: theory Kleene_Algebra.PHL_DRA

17:54:14 Kleene_Algebra: theory Kleene_Algebra.Kleene_Algebra_Models

17:54:14 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo

17:54:15 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter

17:54:15 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool

17:54:15 Kleene_Algebra: theory Kleene_Algebra.Formal_Power_Series

17:54:16 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL

17:54:19 Kleene_Algebra: theory Kleene_Algebra.Omega_Algebra_Models

17:54:19 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement

17:54:22 UPF: theory UPF.ServiceExample

17:54:31 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example

17:54:31 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Eisbach

17:54:31 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Eisbach_Tools

17:54:31 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystemTactics

17:54:33 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_Swap_Add

17:54:35 Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_TypeSystem

17:54:38 Timing Stone_Algebras (2 threads, 55.456s elapsed time, 91.188s cpu time, 2.896s GC time, factor 1.64)

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

17:54:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stone_Algebras/document.pdf

17:54:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stone_Algebras/outline.pdf

17:54:38 Finished Stone_Algebras (0:01:19 elapsed time, 0:02:07 cpu time, factor 1.60)

17:54:38 Building Noninterference_Sequential_Composition ...

17:54:40 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.CSPNoninterference

17:54:40 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.ListInterleaving

17:54:42 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.IpurgeUnwinding

17:54:43 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.DeterministicProcesses

17:54:44 Timing Automatic_Refinement (2 threads, 64.085s elapsed time, 113.520s cpu time, 3.428s GC time, factor 1.77)

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

17:54:44 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/document.pdf

17:54:44 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/outline.pdf

17:54:44 Finished Automatic_Refinement (0:01:30 elapsed time, 0:02:33 cpu time, factor 1.70)

17:54:44 Building Refine_Monadic ...

17:54:47 Refine_Monadic: theory Refine_Monadic.Lattice_Syntax

17:54:47 Refine_Monadic: theory Refine_Monadic.Bit

17:54:47 Refine_Monadic: theory Refine_Monadic.Bits

17:54:47 Refine_Monadic: theory Refine_Monadic.Boolean_Algebra

17:54:48 Refine_Monadic: theory Refine_Monadic.Misc_Numeric

17:54:48 Refine_Monadic: theory Refine_Monadic.Bits_Bit

17:54:48 Refine_Monadic: theory Refine_Monadic.Bit_Representation

17:54:48 Refine_Monadic: theory Refine_Monadic.Word_Miscellaneous

17:54:49 Refine_Monadic: theory Refine_Monadic.Bits_Int

17:54:49 Refine_Monadic: theory Refine_Monadic.Misc_Typedef

17:54:49 Refine_Monadic: theory Refine_Monadic.Phantom_Type

17:54:49 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.Propaedeutics

17:54:50 Refine_Monadic: theory Refine_Monadic.Cardinality

17:54:50 Refine_Monadic: theory Refine_Monadic.Bool_List_Representation

17:54:51 Refine_Monadic: theory Refine_Monadic.Numeral_Type

17:54:51 Refine_Monadic: theory Refine_Monadic.While_Combinator

17:54:52 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.SequentialComposition

17:54:52 Refine_Monadic: theory Refine_Monadic.Adhoc_Overloading

17:54:52 Refine_Monadic: theory Refine_Monadic.Type_Length

17:54:52 Refine_Monadic: theory Refine_Monadic.Monad_Syntax

17:54:52 Refine_Monadic: theory Refine_Monadic.Word

17:54:53 Noninterference_Sequential_Composition: theory Noninterference_Sequential_Composition.Counterexamples

17:55:00 Timing UPF (2 threads, 32.091s elapsed time, 61.768s cpu time, 2.292s GC time, factor 1.92)

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

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

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

17:55:00 Finished UPF (0:01:01 elapsed time, 0:01:46 cpu time, factor 1.74)

17:55:00 Timing Kleene_Algebra (2 threads, 50.886s elapsed time, 87.072s cpu time, 3.752s GC time, factor 1.71)

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

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

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

17:55:00 Finished Kleene_Algebra (0:01:23 elapsed time, 0:02:16 cpu time, factor 1.64)

17:55:01 Building KAT_and_DRA ...

17:55:01 Building Relation_Algebra ...

17:55:04 KAT_and_DRA: theory KAT_and_DRA.KAT2

17:55:04 KAT_and_DRA: theory KAT_and_DRA.Test_Dioid

17:55:04 Relation_Algebra: theory Relation_Algebra.More_Boolean_Algebra

17:55:05 KAT_and_DRA: theory KAT_and_DRA.DRAT2

17:55:05 Relation_Algebra: theory Relation_Algebra.Relation_Algebra

17:55:07 Timing Word_Lib (2 threads, 65.175s elapsed time, 128.056s cpu time, 2.888s GC time, factor 1.96)

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

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

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

17:55:07 Finished Word_Lib (0:01:27 elapsed time, 0:02:40 cpu time, factor 1.84)

17:55:07 Building IP_Addresses ...

17:55:09 Refine_Monadic: theory Refine_Monadic.Example_Chapter

17:55:09 Refine_Monadic: theory Refine_Monadic.Refine_Chapter

17:55:09 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover

17:55:09 Refine_Monadic: theory Refine_Monadic.Refine_Misc

17:55:10 Refine_Monadic: theory Refine_Monadic.RefineG_Domain

17:55:10 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer

17:55:10 Refine_Monadic: theory Refine_Monadic.RefineG_Assert

17:55:10 IP_Addresses: theory IP_Addresses.Cancellation

17:55:10 IP_Addresses: theory IP_Addresses.Char_ord

17:55:10 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion

17:55:11 IP_Addresses: theory IP_Addresses.Code_Abstract_Nat

17:55:11 IP_Addresses: theory IP_Addresses.Code_Target_Nat

17:55:11 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Models

17:55:11 IP_Addresses: theory IP_Addresses.Code_Char

17:55:11 IP_Addresses: theory IP_Addresses.Multiset

17:55:11 IP_Addresses: theory IP_Addresses.Code_Target_Int

17:55:11 KAT_and_DRA: theory KAT_and_DRA.Conway_Tests

17:55:11 Refine_Monadic: theory Refine_Monadic.RefineG_While

17:55:11 Refine_Monadic: theory Refine_Monadic.Refine_Basic

17:55:11 IP_Addresses: theory IP_Addresses.Infinite_Set

17:55:12 Refine_Monadic: theory Refine_Monadic.Refine_Det

17:55:12 IP_Addresses: theory IP_Addresses.NumberWang_IPv4

17:55:12 IP_Addresses: theory IP_Addresses.Option_ord

17:55:12 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_RTC

17:55:13 IP_Addresses: theory IP_Addresses.NumberWang_IPv6

17:55:13 IP_Addresses: theory IP_Addresses.Word_More

17:55:13 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Tests

17:55:13 IP_Addresses: theory IP_Addresses.Eisbach

17:55:13 KAT_and_DRA: theory KAT_and_DRA.KAT

17:55:14 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Vectors

17:55:15 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics

17:55:15 Refine_Monadic: theory Refine_Monadic.Refine_Leof

17:55:15 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Functions

17:55:15 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb

17:55:16 Refine_Monadic: theory Refine_Monadic.Refine_While

17:55:16 Refine_Monadic: theory Refine_Monadic.Refine_Pfun

17:55:16 IP_Addresses: theory IP_Addresses.Quicksort

17:55:17 IP_Addresses: theory IP_Addresses.Misc

17:55:17 KAT_and_DRA: theory KAT_and_DRA.DRAT

17:55:17 KAT_and_DRA: theory KAT_and_DRA.PHL_KAT

17:55:17 Refine_Monadic: theory Refine_Monadic.Refine_Transfer

17:55:18 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic

17:55:18 Refine_Monadic: theory Refine_Monadic.Refine_Automation

17:55:18 Refine_Monadic: theory Refine_Monadic.Refine_Foreach

17:55:19 KAT_and_DRA: theory KAT_and_DRA.DRA_Models

17:55:19 KAT_and_DRA: theory KAT_and_DRA.FolkTheorem

17:55:20 Relation_Algebra: theory Relation_Algebra.Relation_Algebra_Direct_Products

17:55:21 KAT_and_DRA: theory KAT_and_DRA.KAT_Models

17:55:21 Refine_Monadic: theory Refine_Monadic.Refine_Monadic

17:55:21 KAT_and_DRA: theory KAT_and_DRA.PHL_DRAT

17:55:22 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search

17:55:22 Refine_Monadic: theory Refine_Monadic.WordRefine

17:55:22 Timing Noninterference_Sequential_Composition (2 threads, 20.578s elapsed time, 38.152s cpu time, 1.988s GC time, factor 1.85)

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

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

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

17:55:22 Finished Noninterference_Sequential_Composition (0:00:44 elapsed time, 0:01:13 cpu time, factor 1.66)

17:55:23 Building HOLCF-HOL-Library ...

17:55:23 Refine_Monadic: theory Refine_Monadic.Examples

17:55:25 HOLCF-HOL-Library: theory HOLCF-HOL-Library.AList

17:55:25 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Cancellation

17:55:26 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Multiset

17:55:27 HOLCF-HOL-Library: theory HOLCF-HOL-Library.FuncSet

17:55:28 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Infinite_Set

17:55:28 HOLCF-HOL-Library: theory HOLCF-HOL-Library.LaTeXsugar

17:55:28 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Syntax

17:55:28 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Quotient_Option

17:55:31 HOLCF-HOL-Library: theory HOLCF-HOL-Library.Permutation

17:55:44 Timing Simpl (2 threads, 108.612s elapsed time, 202.808s cpu time, 10.880s GC time, factor 1.87)

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

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

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

17:55:44 Finished Simpl (0:02:50 elapsed time, 0:05:00 cpu time, factor 1.76)

17:55:45 Building HOLCF-Library ...

17:55:48 HOLCF-Library: theory HOLCF-Library.Infinite_Set

17:55:48 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

17:55:48 HOLCF-Library: theory HOLCF-Library.Char_Discrete

17:55:48 HOLCF-Library: theory HOLCF-Library.Countable_Set

17:55:48 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

17:55:49 HOLCF-Library: theory HOLCF-Library.Countable_Complete_Lattices

17:55:49 HOLCF-Library: theory HOLCF-Library.Int_Discrete

17:55:49 HOLCF-Library: theory HOLCF-Library.List_Cpo

17:55:50 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

17:55:50 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

17:55:50 HOLCF-Library: theory HOLCF-Library.List_Predomain

17:55:52 HOLCF-Library: theory HOLCF-Library.Option_Cpo

17:55:52 Timing Relation_Algebra (2 threads, 24.239s elapsed time, 47.784s cpu time, 1.760s GC time, factor 1.97)

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

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

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

17:55:52 Finished Relation_Algebra (0:00:50 elapsed time, 0:01:26 cpu time, factor 1.71)

17:55:52 HOLCF-Library: theory HOLCF-Library.Order_Continuity

17:55:52 Building Noninterference_CSP ...

17:55:52 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

17:55:53 HOLCF-Library: theory HOLCF-Library.Extended_Nat

17:55:54 Noninterference_CSP: theory Noninterference_CSP.CSPNoninterference

17:55:54 IP_Addresses: theory IP_Addresses.Hs_Compat

17:55:54 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString

17:55:54 IP_Addresses: theory IP_Addresses.Product_Lexorder

17:55:54 HOLCF-Library: theory HOLCF-Library.Stream

17:55:54 IP_Addresses: theory IP_Addresses.Lib_List_toString

17:55:54 IP_Addresses: theory IP_Addresses.Lib_Word_toString

17:55:55 IP_Addresses: theory IP_Addresses.Word_Next

17:55:55 Noninterference_CSP: theory Noninterference_CSP.ClassicalNoninterference

17:55:55 IP_Addresses: theory IP_Addresses.WordInterval

17:55:56 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

17:55:56 Noninterference_CSP: theory Noninterference_CSP.GeneralizedNoninterference

17:55:59 IP_Addresses: theory IP_Addresses.IP_Address

17:56:00 Timing HOLCF-HOL-Library (2 threads, 16.471s elapsed time, 30.892s cpu time, 1.376s GC time, factor 1.88)

17:56:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-HOL-Library

17:56:00 Finished HOLCF-HOL-Library (0:00:36 elapsed time, 0:01:00 cpu time, factor 1.66)

17:56:00 Building HOLCF-Nominal2 ...

17:56:01 IP_Addresses: theory IP_Addresses.WordInterval_Sorted

17:56:03 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Product

17:56:03 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_Set

17:56:03 IP_Addresses: theory IP_Addresses.IPv4

17:56:03 HOLCF-Nominal2: theory HOLCF-Nominal2.FSet

17:56:03 HOLCF-Nominal2: theory HOLCF-Nominal2.Quotient_List

17:56:04 HOLCF-Nominal2: theory HOLCF-Nominal2.Phantom_Type

17:56:04 IP_Addresses: theory IP_Addresses.IPv6

17:56:04 HOLCF-Nominal2: theory HOLCF-Nominal2.Cardinality

17:56:06 HOLCF-Nominal2: theory HOLCF-Nominal2.FinFun

17:56:07 Timing KAT_and_DRA (2 threads, 41.449s elapsed time, 78.660s cpu time, 2.764s GC time, factor 1.90)

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

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

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

17:56:07 Finished KAT_and_DRA (0:01:05 elapsed time, 0:02:00 cpu time, factor 1.83)

17:56:07 Building Ordinal ...

17:56:08 IP_Addresses: theory IP_Addresses.Prefix_Match

17:56:09 IP_Addresses: theory IP_Addresses.CIDR_Split

17:56:09 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Base

17:56:09 Ordinal: theory Ordinal.OrdinalDef

17:56:10 Ordinal: theory Ordinal.OrdinalInduct

17:56:10 Ordinal: theory Ordinal.OrdinalCont

17:56:11 Ordinal: theory Ordinal.OrdinalRec

17:56:11 Ordinal: theory Ordinal.OrdinalArith

17:56:11 Ordinal: theory Ordinal.OrdinalInverse

17:56:12 Ordinal: theory Ordinal.OrdinalFix

17:56:12 Ordinal: theory Ordinal.OrdinalOmega

17:56:12 Ordinal: theory Ordinal.OrdinalVeblen

17:56:12 Ordinal: theory Ordinal.Ordinal

17:56:14 HOLCF-Nominal2: theory HOLCF-Nominal2.Atoms

17:56:14 HOLCF-Nominal2: theory HOLCF-Nominal2.Eqvt

17:56:14 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_Abs

17:56:16 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2_FCB

17:56:17 Timing Noninterference_CSP (2 threads, 6.067s elapsed time, 11.476s cpu time, 0.476s GC time, factor 1.89)

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

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

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

17:56:17 Finished Noninterference_CSP (0:00:24 elapsed time, 0:00:38 cpu time, factor 1.57)

17:56:17 Building Noninterference_Ipurge_Unwinding ...

17:56:17 HOLCF-Nominal2: theory HOLCF-Nominal2.Nominal2

17:56:18 Timing HOLCF-Library (2 threads, 14.512s elapsed time, 28.788s cpu time, 1.136s GC time, factor 1.98)

17:56:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF-Library

17:56:18 Finished HOLCF-Library (0:00:33 elapsed time, 0:00:55 cpu time, factor 1.69)

17:56:19 Timing Refine_Monadic (2 threads, 60.536s elapsed time, 110.716s cpu time, 5.336s GC time, factor 1.83)

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

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

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

17:56:19 Finished Refine_Monadic (0:01:33 elapsed time, 0:02:41 cpu time, factor 1.72)

17:56:19 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.ListInterleaving

17:56:19 Building Collections ...

17:56:19 Building HOL-Eisbach ...

17:56:21 HOL-Eisbach: theory HOL-Eisbach.Eisbach

17:56:21 HOL-Eisbach: theory IFOL

17:56:22 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

17:56:22 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

17:56:22 HOL-Eisbach: theory HOL-Eisbach.Examples

17:56:22 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding

17:56:22 HOL-Eisbach: theory HOL-Eisbach.Tests

17:56:23 HOL-Eisbach: theory FOL

17:56:23 Collections: theory Collections.SetIterator

17:56:23 Collections: theory Collections.AList

17:56:24 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

17:56:24 Noninterference_Ipurge_Unwinding: theory Noninterference_Ipurge_Unwinding.DeterministicProcesses

17:56:25 Timing Dependent_SIFUM_Type_Systems (2 threads, 164.848s elapsed time, 284.256s cpu time, 9.964s GC time, factor 1.72)

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

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

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

17:56:25 Finished Dependent_SIFUM_Type_Systems (0:03:31 elapsed time, 0:05:58 cpu time, factor 1.69)

17:56:25 Collections: theory Collections.BinomialHeap

17:56:25 Collections: theory Collections.Idx_Iterator

17:56:25 Building Marriage ...

17:56:26 Collections: theory Collections.Code_Abstract_Nat

17:56:26 Collections: theory Collections.Code_Target_Nat

17:56:26 Collections: theory Collections.Code_Target_Int

17:56:26 Collections: theory Collections.Code_Target_Numeral

17:56:27 Collections: theory Collections.Dlist

17:56:27 Marriage: theory Marriage.Marriage

17:56:28 Timing Ordinal (2 threads, 3.575s elapsed time, 6.172s cpu time, 0.204s GC time, factor 1.73)

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

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

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

17:56:28 Finished Ordinal (0:00:20 elapsed time, 0:00:31 cpu time, factor 1.53)

17:56:28 Building Nested_Multisets_Ordinals ...

17:56:28 Collections: theory Collections.FingerTree

17:56:29 Collections: theory Collections.ICF_Tools

17:56:29 Collections: theory Collections.Ord_Code_Preproc

17:56:29 Collections: theory Collections.Locale_Code

17:56:29 Collections: theory Collections.Partial_Equivalence_Relation

17:56:30 Collections: theory Collections.RBT_Impl

17:56:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cancellation

17:56:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Cardinal_Notations

17:56:30 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.FSet

17:56:31 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset

17:56:34 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Infinite_Set

17:56:35 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.List_Index

17:56:35 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nat_Bijection

17:56:36 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Old_Datatype

17:56:36 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_Order

17:56:37 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Plus

17:56:37 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Product_Order

17:56:37 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable

17:56:37 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Sublist

17:56:38 Warning: missing document directory

17:56:38 Timing HOL-Eisbach (2 threads, 3.152s elapsed time, 5.988s cpu time, 0.180s GC time, factor 1.90)

17:56:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Eisbach

17:56:38 Finished HOL-Eisbach (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.53)

17:56:38 Building Cauchy ...

17:56:39 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set

17:56:39 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Complete_Lattices

17:56:39 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Countable_Set_Type

17:56:40 Cauchy: theory Cauchy.CauchySchwarz

17:56:40 Cauchy: theory Cauchy.CauchysMeanTheorem

17:56:42 Collections: theory Collections.Record_Intf

17:56:42 Collections: theory Collections.SetAbstractionIterator

17:56:42 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Order_Continuity

17:56:43 Collections: theory Collections.SetIteratorOperations

17:56:43 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Extended_Nat

17:56:44 Timing Marriage (2 threads, 2.840s elapsed time, 5.028s cpu time, 0.060s GC time, factor 1.77)

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

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

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

17:56:44 Finished Marriage (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.50)

17:56:44 Building HOL-SPARK ...

17:56:44 Timing Noninterference_Ipurge_Unwinding (2 threads, 9.174s elapsed time, 14.516s cpu time, 0.624s GC time, factor 1.58)

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

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

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

17:56:44 Finished Noninterference_Ipurge_Unwinding (0:00:27 elapsed time, 0:00:40 cpu time, factor 1.50)

17:56:44 Running Psi_Calculi ...

17:56:45 Collections: theory Collections.Assoc_List

17:56:46 Collections: theory Collections.Diff_Array

17:56:46 HOL-SPARK: theory HOL-SPARK.Bit_Comparison

17:56:46 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

17:56:46 Timing HOLCF-Nominal2 (2 threads, 23.057s elapsed time, 45.488s cpu time, 2.168s GC time, factor 1.97)

17:56:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Nominal2

17:56:46 Finished HOLCF-Nominal2 (0:00:45 elapsed time, 0:01:19 cpu time, factor 1.72)

17:56:47 Building Launchbury ...

17:56:47 Psi_Calculi: theory Psi_Calculi.Chain

17:56:48 Collections: theory Collections.Dlist_add

17:56:48 Collections: theory Collections.Proper_Iterator

17:56:48 Psi_Calculi: theory Psi_Calculi.Subst_Term

17:56:48 Collections: theory Collections.It_to_It

17:56:48 HOL-SPARK: theory SPARK

17:56:49 Psi_Calculi: theory Psi_Calculi.Agent

17:56:49 Collections: theory Collections.SetIteratorGA

17:56:50 Collections: theory Collections.SkewBinomialHeap

17:56:50 Launchbury: theory Launchbury.Nominal-Utils

17:56:50 Launchbury: theory Launchbury.Mono-Nat-Fun

17:56:51 Launchbury: theory Launchbury.Vars

17:56:51 Launchbury: theory Launchbury.C

17:56:51 Launchbury: theory Launchbury.HOLCF-Join

17:56:51 Launchbury: theory Launchbury.HOLCF-Join-Classes

17:56:52 Launchbury: theory Launchbury.CValue

17:56:52 Launchbury: theory Launchbury.HOLCF-Meet

17:56:53 Launchbury: theory Launchbury.Value

17:56:53 Launchbury: theory Launchbury.C-Meet

17:56:53 Launchbury: theory Launchbury.AList-Utils

17:56:53 Launchbury: theory Launchbury.Env

17:56:54 Launchbury: theory Launchbury.AList-Utils-Nominal

17:56:54 Launchbury: theory Launchbury.Pointwise

17:56:54 Launchbury: theory Launchbury.HOLCF-Utils

17:56:54 Launchbury: theory Launchbury.Terms

17:56:54 Launchbury: theory Launchbury.C-restr

17:56:55 Launchbury: theory Launchbury.Env-HOLCF

17:56:55 Launchbury: theory Launchbury.Iterative

17:56:56 Launchbury: theory Launchbury.EvalHeap

17:56:57 Timing Cauchy (2 threads, 2.656s elapsed time, 5.060s cpu time, 0.092s GC time, factor 1.90)

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

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

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

17:56:57 Finished Cauchy (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.49)

17:56:57 Building Sqrt_Babylonian ...

17:56:58 Launchbury: theory Launchbury.Nominal-HOLCF

17:56:59 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

17:56:59 Launchbury: theory Launchbury.CValue-Nominal

17:57:00 Sqrt_Babylonian: theory Sqrt_Babylonian.Log_Impl

17:57:00 Sqrt_Babylonian: theory Sqrt_Babylonian.NthRoot_Impl

17:57:00 Launchbury: theory Launchbury.Env-Nominal

17:57:01 Sqrt_Babylonian: theory Sqrt_Babylonian.Sqrt_Babylonian

17:57:01 Launchbury: theory Launchbury.HasESem

17:57:02 Launchbury: theory Launchbury.HeapSemantics

17:57:02 Launchbury: theory Launchbury.Substitution

17:57:02 Timing HOL-SPARK (2 threads, 2.576s elapsed time, 4.236s cpu time, 0.148s GC time, factor 1.64)

17:57:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK

17:57:02 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:26 cpu time, factor 1.44)

17:57:02 Building HOL-SPARK-Examples ...

17:57:03 Launchbury: theory Launchbury.Launchbury

17:57:03 Collections: theory Collections.Sorted_List_Operations

17:57:03 Launchbury: theory Launchbury.AbstractDenotational

17:57:03 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Multiset_More

17:57:03 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.McCarthy_91

17:57:04 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Nested_Multiset

17:57:04 Collections: theory Collections.More_Bits_Int

17:57:04 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Multiset

17:57:05 Launchbury: theory Launchbury.Abstract-Denotational-Props

17:57:05 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hereditary_Multiset

17:57:05 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas

17:57:05 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD

17:57:05 Launchbury: theory Launchbury.ResourcedDenotational

17:57:05 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor

17:57:05 Launchbury: theory Launchbury.Value-Nominal

17:57:05 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence

17:57:06 Psi_Calculi: theory Psi_Calculi.Close_Subst

17:57:06 Psi_Calculi: theory Psi_Calculi.Frame

17:57:06 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset

17:57:06 Psi_Calculi: theory Psi_Calculi.Structural_Congruence

17:57:06 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Unary_PCF

17:57:06 Collections: theory Collections.Bits_Integer

17:57:06 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification

17:57:06 Launchbury: theory Launchbury.Denotational

17:57:06 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal

17:57:06 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F

17:57:06 Launchbury: theory Launchbury.CorrectnessResourced

17:57:07 Launchbury: theory Launchbury.CorrectnessOriginal

17:57:07 Launchbury: theory Launchbury.ResourcedAdequacy

17:57:07 Launchbury: theory Launchbury.ValueSimilarity

17:57:07 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Goodstein_Sequence

17:57:08 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Hydra_Battle

17:57:08 Launchbury: theory Launchbury.Denotational-Related

17:57:09 Launchbury: theory Launchbury.Adequacy

17:57:09 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash

17:57:09 Psi_Calculi: theory Psi_Calculi.Semantics

17:57:09 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal

17:57:10 Launchbury: theory Launchbury.EverythingAdequacy

17:57:10 Collections: theory Collections.Word_Misc

17:57:10 Nested_Multisets_Ordinals: theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge

17:57:11 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L

17:57:11 Collections: theory Collections.DatRef

17:57:11 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R

17:57:12 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L

17:57:12 Collections: theory Collections.Gen_Iterator

17:57:13 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R

17:57:13 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round

17:57:13 Collections: theory Collections.Iterator

17:57:14 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L

17:57:14 Collections: theory Collections.ICF_Spec_Base

17:57:14 Collections: theory Collections.MapSpec

17:57:15 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R

17:57:16 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt

17:57:18 Collections: theory Collections.Robdd

17:57:18 Collections: theory Collections.Code_Target_Bits_Int

17:57:19 Collections: theory Collections.Code_Target_ICF

17:57:19 Collections: theory Collections.Locale_Code_Ex

17:57:20 Collections: theory Collections.Uint32

17:57:21 IP_Addresses: theory IP_Addresses.IP_Address_Parser

17:57:22 Collections: theory Collections.RBT_add

17:57:22 Collections: theory Collections.HashCode

17:57:23 Psi_Calculi: theory Psi_Calculi.Simulation

17:57:24 Psi_Calculi: theory Psi_Calculi.Bisimulation

17:57:26 Psi_Calculi: theory Psi_Calculi.Sim_Pres

17:57:26 Psi_Calculi: theory Psi_Calculi.Sim_Struct_Cong

17:57:27 IP_Addresses: theory IP_Addresses.IP_Address_toString

17:57:27 Psi_Calculi: theory Psi_Calculi.Bisim_Pres

17:57:27 Psi_Calculi: theory Psi_Calculi.Sum

17:57:28 Psi_Calculi: theory Psi_Calculi.Tau_Chain

17:57:29 Psi_Calculi: theory Psi_Calculi.Bisim_Struct_Cong

17:57:30 Timing Sqrt_Babylonian (2 threads, 14.203s elapsed time, 23.980s cpu time, 0.460s GC time, factor 1.69)

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

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

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

17:57:30 Finished Sqrt_Babylonian (0:00:32 elapsed time, 0:00:49 cpu time, factor 1.53)

17:57:30 Running Network_Security_Policy_Verification ...

17:57:30 Psi_Calculi: theory Psi_Calculi.Weak_Simulation

17:57:31 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp

17:57:31 Psi_Calculi: theory Psi_Calculi.Weak_Stat_Imp_Pres

17:57:32 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Simulation

17:57:32 Psi_Calculi: theory Psi_Calculi.Weak_Sim_Pres

17:57:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Char_ord

17:57:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Cancellation

17:57:32 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Abstract_Nat

17:57:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Target_Nat

17:57:33 Psi_Calculi: theory Psi_Calculi.Bisim_Subst

17:57:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Code_Char

17:57:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Multiset

17:57:33 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteGraph

17:57:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Infinite_Set

17:57:34 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.List_lexord

17:57:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Config

17:57:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz

17:57:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.ML_GraphViz_Disable

17:57:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Option_ord

17:57:35 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Orders

17:57:35 Psi_Calculi: theory Psi_Calculi.Weak_Bisimulation

17:57:36 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Sim_Pres

17:57:36 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Bounds

17:57:37 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Lattice

17:57:37 Timing HOL-Library (2 threads, 195.531s elapsed time, 368.584s cpu time, 20.108s GC time, factor 1.89)

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

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

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

17:57:37 Finished HOL-Library (0:04:44 elapsed time, 0:08:31 cpu time, factor 1.80)

17:57:38 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.CompleteLattice

17:57:38 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Product_Lexorder

17:57:38 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.RBT_Impl

17:57:38 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Quicksort

17:57:39 Building HOL-Computational_Algebra ...

17:57:39 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.TopoS_Util

17:57:39 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Transitive_Closure_Impl

17:57:39 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Pres

17:57:39 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Transitive_Closure_List_Impl

17:57:40 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph

17:57:41 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Eisbach

17:57:41 Timing HOL-SPARK-Examples (2 threads, 18.835s elapsed time, 32.004s cpu time, 0.684s GC time, factor 1.70)

17:57:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-SPARK-Examples

17:57:41 Finished HOL-SPARK-Examples (0:00:38 elapsed time, 0:01:00 cpu time, factor 1.58)

17:57:41 Psi_Calculi: theory Psi_Calculi.Weak_Psi_Congruence

17:57:41 Building Abstract-Rewriting ...

17:57:41 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Misc

17:57:41 Psi_Calculi: theory Psi_Calculi.Weak_Bisim_Struct_Cong

17:57:44 Psi_Calculi: theory Psi_Calculi.Weakening

17:57:44 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

17:57:44 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

17:57:44 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Pres

17:57:46 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

17:57:47 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Set

17:57:47 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.Efficient_Distinct

17:57:47 Psi_Calculi: theory Psi_Calculi.Weaken_Transition

17:57:48 Psi_Calculi: theory Psi_Calculi.Weak_Cong_Struct_Cong

17:57:49 Abstract-Rewriting: theory Abstract-Rewriting.Regular_Exp

17:57:50 Psi_Calculi: theory Psi_Calculi.Weaken_Stat_Imp

17:57:51 Psi_Calculi: theory Psi_Calculi.Weak_Congruence

17:57:52 Psi_Calculi: theory Psi_Calculi.Weaken_Simulation

17:57:52 Abstract-Rewriting: theory Abstract-Rewriting.NDerivative

17:57:52 Abstract-Rewriting: theory Abstract-Rewriting.Relation_Interpretation

17:57:54 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

17:57:54 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

17:57:55 Psi_Calculi: theory Psi_Calculi.Weaken_Bisimulation

17:57:56 Abstract-Rewriting: theory Abstract-Rewriting.Equivalence_Checking

17:57:57 Abstract-Rewriting: theory Abstract-Rewriting.Regexp_Method

17:57:58 Psi_Calculi: theory Psi_Calculi.Tau

17:57:59 Abstract-Rewriting: theory Abstract-Rewriting.Seq

17:58:00 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting

17:58:01 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting

17:58:02 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

17:58:03 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

17:58:03 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

17:58:03 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders

17:58:03 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

17:58:04 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

17:58:05 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier

17:58:07 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

17:58:07 Timing Nested_Multisets_Ordinals (2 threads, 64.993s elapsed time, 123.200s cpu time, 4.540s GC time, factor 1.90)

17:58:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals

17:58:07 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/document.pdf

17:58:07 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nested_Multisets_Ordinals/outline.pdf

17:58:07 Finished Nested_Multisets_Ordinals (0:01:38 elapsed time, 0:02:54 cpu time, factor 1.77)

17:58:08 Building Jinja ...

17:58:08 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

17:58:11 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.RBT

17:58:12 Network_Security_Policy_Verification: theory Network_Security_Policy_Verification.FiniteListGraph_Impl

17:58:14 Jinja: theory Jinja.Auxiliary

17:58:14 Jinja: theory Jinja.List_Index

17:58:14 Psi_Calculi: theory Psi_Calculi.Tau_Sim

17:58:14 Timing Launchbury (2 threads, 49.615s elapsed time, 90.176s cpu time, 3.016s GC time, factor 1.82)

17:58:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury

17:58:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/document.pdf

17:58:14 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Launchbury/outline.pdf

17:58:14 Finished Launchbury (0:01:26 elapsed time, 0:02:26 cpu time, factor 1.69)

17:58:14 Jinja: theory Jinja.Type

17:58:14 Jinja: theory Jinja.Hidden

17:58:14 Building Deriving ...

17:58:14 Jinja: theory Jinja.Semilat

17:58:15 Jinja: theory Jinja.Decl

17:58:15 Jinja: theory Jinja.TypeRel

17:58:15 Jinja: theory Jinja.Err

17:58:16 Jinja: theory Jinja.Listn

17:58:16 Jinja: theory Jinja.Opt

17:58:17 Jinja: theory Jinja.Value

17:58:17 Jinja: theory Jinja.Product

17:58:17 Jinja: theory Jinja.Semilattices

17:58:17 Jinja: theory Jinja.Typing_Framework

17:58:17 Jinja: theory Jinja.SemilatAlg

17:58:17 Jinja: theory Jinja.Objects

17:58:18 Jinja: theory Jinja.Kildall

17:58:18 Jinja: theory Jinja.Exceptions

17:58:18 Jinja: theory Jinja.Conform

17:58:18 Jinja: theory Jinja.Expr

17:58:18 Jinja: theory Jinja.State

17:58:18 Jinja: theory Jinja.SystemClasses

17:58:19 Jinja: theory Jinja.JVMState

17:58:19 Jinja: theory Jinja.JVMInstructions

17:58:20 Deriving: theory Deriving.Bits

17:58:20 Deriving: theory Deriving.Misc_Numeric

17:58:20 Deriving: theory Deriving.Bit_Representation

17:58:20 Deriving: theory Deriving.Misc_Typedef

17:58:20 Deriving: theory Deriving.Bits_Bit

17:58:21 Deriving: theory Deriving.Bits_Int

17:58:21 Deriving: theory Deriving.Word_Miscellaneous

17:58:21 Jinja: theory Jinja.JVMExceptions

17:58:21 Jinja: theory Jinja.JVMExecInstr

17:58:22 Deriving: theory Deriving.Bool_List_Representation

17:58:23 Jinja: theory Jinja.JVMExec

17:58:23 Deriving: theory Deriving.More_Bits_Int

17:58:23 Deriving: theory Deriving.Word

17:58:23 Jinja: theory Jinja.JVMDefensive

17:58:25 Jinja: theory Jinja.Examples

17:58:25 Jinja: theory Jinja.BigStep

17:58:26 Deriving: theory Deriving.Bits_Integer

17:58:27 Jinja: theory Jinja.SmallStep

17:58:29 Jinja: theory Jinja.DefAss

17:58:29 Deriving: theory Deriving.Word_Misc

17:58:29 Jinja: theory Jinja.J1

17:58:33 Jinja: theory Jinja.execute_Bigstep

17:58:35 Jinja: theory Jinja.JVMListExample

17:58:36 Jinja: theory Jinja.WellType

17:58:37 Jinja: theory Jinja.Annotate

17:58:37 Deriving: theory Deriving.Uint32

17:58:38 Jinja: theory Jinja.WellTypeRT

17:58:39 Jinja: theory Jinja.execute_WellType

17:58:39 Deriving: theory Deriving.HashCode

17:58:41 Jinja: theory Jinja.WellForm

17:58:42 Collections: theory Collections.GenCF_Chapter

17:58:42 Collections: theory Collections.Intf_Comp

17:58:42 Collections: theory Collections.GenCF_Gen_Chapter

17:58:42 Jinja: theory Jinja.PCompiler

17:58:42 Collections: theory Collections.GenCF_Impl_Chapter

17:58:42 Collections: theory Collections.GenCF_Intf_Chapter

17:58:42 Collections: theory Collections.Product_Lexorder

17:58:42 Jinja: theory Jinja.Compiler2

17:58:42 Collections: theory Collections.Impl_Array_Stack

17:58:43 Psi_Calculi: theory Psi_Calculi.Tau_Stat_Imp

17:58:43 Collections: theory Collections.Intf_Hash

17:58:43 Jinja: theory Jinja.Correctness2

17:58:43 Collections: theory Collections.Gen_Comp

17:58:44 Collections: theory Collections.Array_Iterator

17:58:44 Collections: theory Collections.Intf_Map

17:58:44 Collections: theory Collections.Intf_Set

17:58:44 Collections: theory Collections.Gen_Map

17:58:44 Collections: theory Collections.Impl_RBT_Map

17:58:45 Collections: theory Collections.Impl_Array_Map

17:58:45 Jinja: theory Jinja.WWellForm

17:58:45 Jinja: theory Jinja.Equivalence

17:58:46 Collections: theory Collections.Impl_List_Map

17:58:47 Jinja: theory Jinja.Progress

17:58:47 Collections: theory Collections.Impl_Array_Hash_Map

17:58:48 Jinja: theory Jinja.JWellForm

17:58:49 Jinja: theory Jinja.J1WellForm

17:58:50 Collections: theory Collections.Gen_Map2Set

17:58:50 Jinja: theory Jinja.TypeSafe

17:58:50 Collections: theory Collections.Gen_Set

17:58:50 Collections: theory Collections.Impl_Cfun_Set

17:58:51 Jinja: theory Jinja.Compiler1

17:58:51 Collections: theory Collections.Impl_List_Set

17:58:51 Timing Abstract-Rewriting (2 threads, 31.154s elapsed time, 55.304s cpu time, 2.716s GC time, factor 1.78)

17:58:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting

17:58:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/document.pdf

17:58:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/outline.pdf

17:58:51 Finished Abstract-Rewriting (0:01:09 elapsed time, 0:01:54 cpu time, factor 1.65)

17:58:51 Jinja: theory Jinja.Correctness1

17:58:51 Building LTL ...

17:58:51 Jinja: theory Jinja.Compiler

17:58:52 Jinja: theory Jinja.SemiType

17:58:52 Jinja: theory Jinja.JVM_SemiType

17:58:53 Jinja: theory Jinja.Effect

17:58:54 Deriving: theory Deriving.Comparator

17:58:54 Deriving: theory Deriving.Derive_Manager

17:58:54 Deriving: theory Deriving.Generator_Aux

17:58:54 Deriving: theory Deriving.Equality_Generator

17:58:54 Deriving: theory Deriving.Equality_Instances

17:58:55 Deriving: theory Deriving.Hash_Generator

17:58:55 Deriving: theory Deriving.Compare

17:58:55 Deriving: theory Deriving.Comparator_Generator

17:58:55 Deriving: theory Deriving.Hash_Instances

17:58:56 Deriving: theory Deriving.RBT_Comparator_Impl

17:58:56 Deriving: theory Deriving.Compare_Generator

17:58:56 Deriving: theory Deriving.Compare_Instances

17:58:57 LTL: theory LTL.LTL

17:58:57 Deriving: theory Deriving.Compare_Order_Instances

17:58:58 Deriving: theory Deriving.RBT_Compare_Order_Impl