Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow [isabelle-nightly-slow] $ hg showconfig paths.default [isabelle-nightly-slow] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-nightly-slow] $ hg update --clean --rev default 5 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all [isabelle-nightly-slow] $ hg log --rev . --template {node} [isabelle-nightly-slow] $ hg log --rev . --template {rev} [isabelle-nightly-slow] $ hg log --rev a7aba6db79a143c5a47e0cfadc01c50e155f6403 --template exists\n exists [isabelle-nightly-slow] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(a7aba6db79a143c5a47e0cfadc01c50e155f6403)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://bitbucket.org/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 38 files updated, 0 files merged, 1 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev 69945e1330db22c0bfcf00d214e8dbbe3def71a9 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(69945e1330db22c0bfcf00d214e8dbbe3def71a9)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins7213610976666075591.sh + Admin/jenkins/run_build slow + set -e + PROFILE=slow + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building graph browser ... warning: [options] bootstrap class path not set in conjunction with -source 6 warning: [options] source value 6 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. Note: Some input files use or override a deprecated API. Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. 3 warnings ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup # Run eval $(opam env) to update the current shell environment [NOTE] It seems you have not updated your repositories for a while. Consider updating them with: opam update [NOTE] Package zarith is already installed (current version is 1.7). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.4.4 + bin/isabelle ci_build_slow === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="-H 4000 --maxheap 20G" jobs = 1, threads = 8, numa = false === BUILD === Build started at Sun, 21 Apr 2019 01:35:12 +0200 Isabelle id ac1706cdde25 Build for AFP id 91971ca6ad5e === LOG === Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session AFP/AWN (AFP) Session AFP/AODV (AFP slow) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session AFP/Binomial-Heaps (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/ConcurrentGC (AFP slow) Session AFP/FinFun (AFP) Session AFP/Finger-Trees (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Analysis (main timing) Session AFP/Coinductive (AFP) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow) Session HOL/HOL-Word (main timing) Session AFP/Native_Word (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Collections (AFP) Session AFP/Word_Lib (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow) Session AFP/JinjaThreads (AFP slow) Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Pure: theory Pure.Sessions Timing Pure (1 threads, 1.574s elapsed time, 1.576s cpu time, 0.000s GC time, factor 1.00) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure Finished Pure (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00) Building HOL ... HOL: theory HOL.Code_Generator HOL: theory HOL.HOL HOL: theory HOL.Argo HOL: theory HOL.Ctr_Sugar HOL: theory HOL.Orderings HOL: theory HOL.Groups HOL: theory HOL.SAT HOL: theory HOL.Lattices HOL: theory HOL.Set HOL: theory HOL.Fun HOL: theory HOL.Typedef HOL: theory HOL.Complete_Lattices HOL: theory HOL.Rings HOL: theory HOL.Inductive HOL: theory HOL.Product_Type HOL: theory HOL.Sum_Type HOL: theory HOL.Complete_Partial_Order HOL: theory HOL.Nat HOL: theory HOL.Fields HOL: theory HOL.Meson HOL: theory HOL.ATP HOL: theory HOL.Metis HOL: theory HOL.Finite_Set HOL: theory HOL.Relation HOL: theory HOL.Transitive_Closure HOL: theory HOL.Wellfounded HOL: theory HOL.Fun_Def_Base HOL: theory HOL.Hilbert_Choice HOL: theory HOL.Wfrec HOL: theory HOL.Order_Relation HOL: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.Zorn HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.BNF_Cardinal_Arithmetic HOL: theory HOL.BNF_Def HOL: theory HOL.BNF_Composition HOL: theory HOL.Basic_BNFs HOL: theory HOL.BNF_Fixpoint_Base HOL: theory HOL.BNF_Least_Fixpoint HOL: theory HOL.Basic_BNF_LFPs HOL: theory HOL.Transfer HOL: theory HOL.Num HOL: theory HOL.Power HOL: theory HOL.Groups_Big HOL: theory HOL.Equiv_Relations HOL: theory HOL.Lifting HOL: theory HOL.Lifting_Set HOL: theory HOL.Option HOL: theory HOL.Quotient HOL: theory HOL.Extraction HOL: theory HOL.Lattices_Big HOL: theory HOL.Partial_Function HOL: theory HOL.Fun_Def HOL: theory HOL.Int HOL: theory HOL.Euclidean_Division HOL: theory HOL.Parity HOL: theory HOL.Divides HOL: theory HOL.Code_Numeral HOL: theory HOL.Set_Interval HOL: theory HOL.Numeral_Simprocs HOL: theory HOL.SMT HOL: theory HOL.Semiring_Normalization HOL: theory HOL.Groebner_Basis HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.Filter HOL: theory HOL.Presburger HOL: theory HOL.Sledgehammer HOL: theory HOL.List HOL: theory HOL.Groups_List HOL: theory HOL.Map HOL: theory HOL.Factorial HOL: theory HOL.GCD HOL: theory HOL.Enum HOL: theory HOL.Random HOL: theory HOL.Binomial HOL: theory HOL.String HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Predicate HOL: theory HOL.Typerep HOL: theory HOL.Lazy_Sequence HOL: theory HOL.Limited_Sequence HOL: theory HOL.Code_Evaluation HOL: theory HOL.Quickcheck_Random HOL: theory HOL.Random_Pred HOL: theory HOL.Quickcheck_Exhaustive HOL: theory HOL.Quickcheck_Narrowing HOL: theory HOL.Random_Sequence HOL: theory HOL.Record HOL: theory HOL.Predicate_Compile HOL: theory HOL.Nitpick HOL: theory HOL.Nunchaku HOL: theory Main HOL: theory HOL.Archimedean_Field HOL: theory HOL.Topological_Spaces HOL: theory HOL.Hull HOL: theory HOL.Modules HOL: theory HOL.Vector_Spaces HOL: theory HOL.Rat HOL: theory HOL.Real HOL: theory HOL.Real_Vector_Spaces HOL: theory HOL.Inequalities HOL: theory HOL.Limits HOL: theory HOL.Deriv HOL: theory HOL.Series HOL: theory HOL.NthRoot HOL: theory HOL.Transcendental HOL: theory HOL.Complex HOL: theory HOL.MacLaurin HOL: theory Complex_Main Timing HOL (8 threads, 308.904s elapsed time, 1133.400s cpu time, 111.496s GC time, factor 3.67) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf Finished HOL (0:06:45 elapsed time, 0:22:11 cpu time, factor 3.28) Running JinjaThreads ... JinjaThreads: theory HOL-Eisbach.Eisbach JinjaThreads: theory Automatic_Refinement.Prio_List JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1 JinjaThreads: theory Collections.ICF_Tools JinjaThreads: theory Automatic_Refinement.Foldi JinjaThreads: theory HOL-Library.AList JinjaThreads: theory Finger-Trees.FingerTree JinjaThreads: theory HOL-Library.Adhoc_Overloading JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot JinjaThreads: theory HOL-Library.Monad_Syntax JinjaThreads: theory Collections.Ord_Code_Preproc JinjaThreads: theory HOL-Library.Bit JinjaThreads: theory HOL-Library.Boolean_Algebra JinjaThreads: theory HOL-Library.Cancellation JinjaThreads: theory Collections.Locale_Code JinjaThreads: theory Automatic_Refinement.Refine_Util JinjaThreads: theory Collections.Record_Intf JinjaThreads: theory HOL-Library.Case_Converter JinjaThreads: theory HOL-Library.Code_Abstract_Nat JinjaThreads: theory HOL-Library.Code_Target_Nat JinjaThreads: theory HOL-Library.Simps_Case_Conv JinjaThreads: theory HOL-Library.Code_Target_Int JinjaThreads: theory HOL-Library.Dlist JinjaThreads: theory Automatic_Refinement.Anti_Unification JinjaThreads: theory Automatic_Refinement.Attr_Comb JinjaThreads: theory Automatic_Refinement.Autoref_Data JinjaThreads: theory Automatic_Refinement.Indep_Vars JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp JinjaThreads: theory Automatic_Refinement.Tagged_Solver JinjaThreads: theory Automatic_Refinement.Select_Solve JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms JinjaThreads: theory HOL-Library.Multiset JinjaThreads: theory HOL-Library.Code_Target_Numeral JinjaThreads: theory HOL-Library.Infinite_Set JinjaThreads: theory HOL-Library.Lattice_Syntax JinjaThreads: theory HOL-Library.Complete_Partial_Order2 JinjaThreads: theory HOL-Library.Nat_Bijection JinjaThreads: theory HOL-Library.Old_Datatype JinjaThreads: theory HOL-Library.Option_ord JinjaThreads: theory HOL-Library.Phantom_Type JinjaThreads: theory Trie.Trie JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs JinjaThreads: theory HOL-Library.RBT_Impl JinjaThreads: theory HOL-Library.Sublist JinjaThreads: theory HOL-Library.Transitive_Closure_Table JinjaThreads: theory HOL-Library.Cardinality JinjaThreads: theory HOL-Library.While_Combinator JinjaThreads: theory Collections.DatRef JinjaThreads: theory HOL-Word.Bit_Representation JinjaThreads: theory HOL-Word.Bits JinjaThreads: theory HOL-Word.Bits_Bit JinjaThreads: theory FinFun.FinFun JinjaThreads: theory HOL-Library.Numeral_Type JinjaThreads: theory HOL-Word.Misc_Typedef JinjaThreads: theory HOL-Library.Countable JinjaThreads: theory JinjaThreads.Set_Monad JinjaThreads: theory JinjaThreads.Set_without_equal JinjaThreads: theory Refine_Monadic.Refine_Chapter JinjaThreads: theory HOL-Word.Bool_List_Representation JinjaThreads: theory HOL-Word.Misc_Arithmetic JinjaThreads: theory HOL-Library.Type_Length JinjaThreads: theory HOL-Word.Bits_Int JinjaThreads: theory HOL-Library.Countable_Set JinjaThreads: theory Binomial-Heaps.BinomialHeap JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap JinjaThreads: theory HOL-ex.Quicksort JinjaThreads: theory Native_Word.More_Bits_Int JinjaThreads: theory HOL-Word.Word JinjaThreads: theory Automatic_Refinement.Misc JinjaThreads: theory HOL-Library.Countable_Complete_Lattices JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int JinjaThreads: theory Native_Word.Bits_Integer JinjaThreads: theory HOL-Library.Order_Continuity JinjaThreads: theory JinjaThreads.Auxiliary JinjaThreads: theory HOL-Library.Extended_Nat JinjaThreads: theory Coinductive.Coinductive_Nat JinjaThreads: theory Coinductive.Coinductive_List JinjaThreads: theory Automatic_Refinement.Refine_Lib JinjaThreads: theory Collections.SetIterator JinjaThreads: theory Collections.Sorted_List_Operations JinjaThreads: theory Automatic_Refinement.Autoref_Phases JinjaThreads: theory Automatic_Refinement.Autoref_Tagging JinjaThreads: theory Automatic_Refinement.Relators JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover JinjaThreads: theory Collections.SetIteratorOperations JinjaThreads: theory Automatic_Refinement.Param_Tool JinjaThreads: theory Automatic_Refinement.Param_HOL JinjaThreads: theory Collections.Assoc_List JinjaThreads: theory Collections.Dlist_add JinjaThreads: theory Collections.Proper_Iterator JinjaThreads: theory Collections.SetIteratorGA JinjaThreads: theory Automatic_Refinement.Parametricity JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops JinjaThreads: theory Collections.Diff_Array JinjaThreads: theory Collections.Trie_Impl JinjaThreads: theory Collections.It_to_It JinjaThreads: theory Collections.Trie2 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel JinjaThreads: theory Automatic_Refinement.Autoref_Translate JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo JinjaThreads: theory Automatic_Refinement.Autoref_Tool JinjaThreads: theory Coinductive.Lazy_LList JinjaThreads: theory Coinductive.TLList JinjaThreads: theory Native_Word.Code_Target_Bits_Int JinjaThreads: theory Native_Word.Code_Target_Word_Base JinjaThreads: theory Collections.Code_Target_ICF JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL JinjaThreads: theory Native_Word.Uint32 JinjaThreads: theory Coinductive.Lazy_TLList JinjaThreads: theory Collections.HashCode JinjaThreads: theory Automatic_Refinement.Automatic_Refinement JinjaThreads: theory Collections.Idx_Iterator JinjaThreads: theory Refine_Monadic.Refine_Misc JinjaThreads: theory Refine_Monadic.RefineG_Domain JinjaThreads: theory Refine_Monadic.RefineG_Transfer JinjaThreads: theory Refine_Monadic.RefineG_Assert JinjaThreads: theory Refine_Monadic.RefineG_Recursion JinjaThreads: theory Refine_Monadic.RefineG_While JinjaThreads: theory Refine_Monadic.Refine_Basic JinjaThreads: theory Refine_Monadic.Refine_Det JinjaThreads: theory Refine_Monadic.Refine_Heuristics JinjaThreads: theory Refine_Monadic.Refine_Leof JinjaThreads: theory Refine_Monadic.Refine_Pfun JinjaThreads: theory Refine_Monadic.Refine_More_Comb JinjaThreads: theory Refine_Monadic.Refine_While JinjaThreads: theory Refine_Monadic.Refine_Transfer JinjaThreads: theory Refine_Monadic.Autoref_Monadic JinjaThreads: theory Refine_Monadic.Refine_Automation JinjaThreads: theory Refine_Monadic.Refine_Foreach JinjaThreads: theory Refine_Monadic.Refine_Monadic JinjaThreads: theory Collections.Gen_Iterator JinjaThreads: theory Collections.Intf_Map JinjaThreads: theory Collections.Intf_Set JinjaThreads: theory Collections.Iterator JinjaThreads: theory Collections.Array_Iterator JinjaThreads: theory Collections.ICF_Spec_Base JinjaThreads: theory Collections.AnnotatedListSpec JinjaThreads: theory Collections.ListSpec JinjaThreads: theory Collections.PrioSpec JinjaThreads: theory Collections.MapSpec JinjaThreads: theory Collections.PrioUniqueSpec JinjaThreads: theory Collections.SetSpec JinjaThreads: theory Collections.BinoPrioImpl JinjaThreads: theory Collections.SkewPrioImpl JinjaThreads: theory Collections.ListGA JinjaThreads: theory Collections.FTAnnotatedListImpl JinjaThreads: theory Collections.PrioByAnnotatedList JinjaThreads: theory Collections.Fifo JinjaThreads: theory Collections.PrioUniqueByAnnotatedList JinjaThreads: theory HOL-Library.RBT JinjaThreads: theory Collections.RBT_add JinjaThreads: theory Collections.Algos JinjaThreads: theory Collections.SetIndex JinjaThreads: theory Collections.SetIteratorCollectionsGA JinjaThreads: theory Collections.MapGA JinjaThreads: theory Collections.SetGA JinjaThreads: theory Collections.FTPrioImpl JinjaThreads: theory Collections.FTPrioUniqueImpl JinjaThreads: theory Collections.ArrayMapImpl JinjaThreads: theory Collections.ListMapImpl JinjaThreads: theory Collections.ListMapImpl_Invar JinjaThreads: theory Collections.TrieMapImpl JinjaThreads: theory Collections.RBTMapImpl JinjaThreads: theory Collections.ListSetImpl JinjaThreads: theory Collections.ListSetImpl_Invar JinjaThreads: theory Collections.ListSetImpl_NotDist JinjaThreads: theory Collections.ArrayHashMap_Impl JinjaThreads: theory Collections.ListSetImpl_Sorted JinjaThreads: theory Collections.SetByMap JinjaThreads: theory Collections.HashMap_Impl JinjaThreads: theory Collections.ArraySetImpl JinjaThreads: theory Collections.TrieSetImpl JinjaThreads: theory Collections.RBTSetImpl JinjaThreads: theory Collections.ArrayHashMap JinjaThreads: theory Collections.HashMap JinjaThreads: theory Collections.ArrayHashSet JinjaThreads: theory Collections.HashSet JinjaThreads: theory Collections.MapStdImpl JinjaThreads: theory Collections.SetStdImpl JinjaThreads: theory Collections.ICF_Impl JinjaThreads: theory Collections.ICF_Refine_Monadic JinjaThreads: theory Collections.ICF_Autoref JinjaThreads: theory Collections.Collections JinjaThreads: theory Collections.CollectionsV1 JinjaThreads: theory JinjaThreads.JT_ICF JinjaThreads: theory JinjaThreads.Basic_Main JinjaThreads: theory HOL-Library.Mapping JinjaThreads: theory HOL-Library.Prefix_Order JinjaThreads: theory JinjaThreads.FWState JinjaThreads: theory JinjaThreads.LTS JinjaThreads: theory JinjaThreads.Type JinjaThreads: theory JinjaThreads.ListIndex JinjaThreads: theory JinjaThreads.Orders JinjaThreads: theory JinjaThreads.Semilat JinjaThreads: theory JinjaThreads.Err JinjaThreads: theory HOL-Library.AList_Mapping JinjaThreads: theory JinjaThreads.Listn JinjaThreads: theory JinjaThreads.Opt JinjaThreads: theory JinjaThreads.Product JinjaThreads: theory JinjaThreads.Semilattices JinjaThreads: theory JinjaThreads.Typing_Framework JinjaThreads: theory JinjaThreads.SemilatAlg JinjaThreads: theory JinjaThreads.Decl JinjaThreads: theory JinjaThreads.Kildall JinjaThreads: theory JinjaThreads.LBVSpec JinjaThreads: theory JinjaThreads.Bisimulation JinjaThreads: theory JinjaThreads.Typing_Framework_err JinjaThreads: theory JinjaThreads.LBVComplete JinjaThreads: theory JinjaThreads.LBVCorrect JinjaThreads: theory JinjaThreads.Abstract_BV JinjaThreads: theory JinjaThreads.TypeRel JinjaThreads: theory JinjaThreads.TypeRelRefine JinjaThreads: theory JinjaThreads.Value JinjaThreads: theory JinjaThreads.Exceptions JinjaThreads: theory JinjaThreads.Heap JinjaThreads: theory JinjaThreads.SystemClasses JinjaThreads: theory JinjaThreads.MM JinjaThreads: theory JinjaThreads.State JinjaThreads: theory JinjaThreads.FWCondAction JinjaThreads: theory JinjaThreads.FWInterrupt JinjaThreads: theory JinjaThreads.FWLock JinjaThreads: theory JinjaThreads.FWThread JinjaThreads: theory JinjaThreads.Observable_Events JinjaThreads: theory JinjaThreads.FWWait JinjaThreads: theory JinjaThreads.FWLocking JinjaThreads: theory JinjaThreads.FWLockingThread JinjaThreads: theory JinjaThreads.FWWellform JinjaThreads: theory JinjaThreads.FWLifting JinjaThreads: theory JinjaThreads.FWSemantics JinjaThreads: theory JinjaThreads.JVMState JinjaThreads: theory JinjaThreads.JMM_Spec JinjaThreads: theory JinjaThreads.StartConfig JinjaThreads: theory JinjaThreads.FWLiftingSem JinjaThreads: theory JinjaThreads.FWProgressAux JinjaThreads: theory JinjaThreads.Conform JinjaThreads: theory JinjaThreads.FWDeadlock JinjaThreads: theory JinjaThreads.FWLTS JinjaThreads: theory JinjaThreads.State_Refinement JinjaThreads: theory JinjaThreads.ConformThreaded JinjaThreads: theory JinjaThreads.FWProgress JinjaThreads: theory JinjaThreads.ExternalCall JinjaThreads: theory JinjaThreads.SC JinjaThreads: theory JinjaThreads.SC_Collections JinjaThreads: theory JinjaThreads.FWBisimulation JinjaThreads: theory JinjaThreads.FWInitFinLift JinjaThreads: theory JinjaThreads.Scheduler JinjaThreads: theory JinjaThreads.JMM_DRF JinjaThreads: theory JinjaThreads.Non_Speculative JinjaThreads: theory JinjaThreads.SC_Legal JinjaThreads: theory JinjaThreads.HB_Completion JinjaThreads: theory JinjaThreads.SC_Completion JinjaThreads: theory JinjaThreads.WellForm JinjaThreads: theory JinjaThreads.ExternalCall_Execute JinjaThreads: theory JinjaThreads.BinOp JinjaThreads: theory JinjaThreads.ExternalCallWF JinjaThreads: theory JinjaThreads.JMM_Heap JinjaThreads: theory JinjaThreads.SemiType JinjaThreads: theory JinjaThreads.JVM_SemiType JinjaThreads: theory JinjaThreads.Random_Scheduler JinjaThreads: theory JinjaThreads.Round_Robin JinjaThreads: theory JinjaThreads.JMM_Framework JinjaThreads: theory JinjaThreads.JMM_Type JinjaThreads: theory JinjaThreads.JMM_Type2 JinjaThreads: theory JinjaThreads.SC_Schedulers JinjaThreads: theory JinjaThreads.Expr JinjaThreads: theory JinjaThreads.JVMInstructions JinjaThreads: theory JinjaThreads.PCompiler JinjaThreads: theory JinjaThreads.PCompilerRefine JinjaThreads: theory JinjaThreads.JVMExceptions JinjaThreads: theory JinjaThreads.JVMHeap JinjaThreads: theory JinjaThreads.Effect JinjaThreads: theory JinjaThreads.JVMExecInstr JinjaThreads: theory JinjaThreads.CallExpr JinjaThreads: theory JinjaThreads.DefAss JinjaThreads: theory JinjaThreads.WWellForm JinjaThreads: theory JinjaThreads.JHeap JinjaThreads: theory JinjaThreads.WellType JinjaThreads: theory JinjaThreads.JVMExec JinjaThreads: theory JinjaThreads.ToString JinjaThreads: theory JinjaThreads.JVMDefensive JinjaThreads: theory JinjaThreads.J1State JinjaThreads: theory JinjaThreads.JMM_Typesafe JinjaThreads: theory JinjaThreads.Annotate JinjaThreads: theory JinjaThreads.SmallStep JinjaThreads: theory JinjaThreads.Compiler2 JinjaThreads: theory JinjaThreads.JVMThreaded JinjaThreads: theory JinjaThreads.J1Heap JinjaThreads: theory JinjaThreads.Compiler1 JinjaThreads: theory JinjaThreads.JMM_Common JinjaThreads: theory JinjaThreads.Exception_Tables JinjaThreads: theory JinjaThreads.JVM_Main JinjaThreads: theory JinjaThreads.JMM_JVM JinjaThreads: theory JinjaThreads.J1WellType JinjaThreads: theory JinjaThreads.Compiler JinjaThreads: theory JinjaThreads.JWellForm JinjaThreads: theory JinjaThreads.WellTypeRT JinjaThreads: theory JinjaThreads.Preprocessor JinjaThreads: theory JinjaThreads.J1WellForm JinjaThreads: theory JinjaThreads.JMM_Typesafe2 JinjaThreads: theory JinjaThreads.JVMExec_Execute JinjaThreads: theory JinjaThreads.JJ1WellForm JinjaThreads: theory JinjaThreads.FWBisimDeadlock JinjaThreads: theory JinjaThreads.FWBisimLift JinjaThreads: theory JinjaThreads.J1 JinjaThreads: theory JinjaThreads.BVSpec JinjaThreads: theory JinjaThreads.BVConform JinjaThreads: theory JinjaThreads.TypeComp JinjaThreads: theory JinjaThreads.EffectMono JinjaThreads: theory JinjaThreads.TF_JVM JinjaThreads: theory JinjaThreads.BVExec JinjaThreads: theory JinjaThreads.Common_Main JinjaThreads: theory JinjaThreads.LBVJVM JinjaThreads: theory JinjaThreads.BVSpecTypeSafe JinjaThreads: theory JinjaThreads.J1Deadlock JinjaThreads: theory JinjaThreads.BVNoTypeError JinjaThreads: theory JinjaThreads.BVProgressThreaded JinjaThreads: theory JinjaThreads.BCVExec JinjaThreads: theory JinjaThreads.JVMExec_Execute2 JinjaThreads: theory JinjaThreads.JVMTau JinjaThreads: theory JinjaThreads.Execs JinjaThreads: theory JinjaThreads.DefAssPreservation JinjaThreads: theory JinjaThreads.Threaded JinjaThreads: theory JinjaThreads.Progress JinjaThreads: theory JinjaThreads.TypeSafe JinjaThreads: theory JinjaThreads.J1JVMBisim JinjaThreads: theory JinjaThreads.J0 JinjaThreads: theory JinjaThreads.DRF_JVM JinjaThreads: theory JinjaThreads.JVMDeadlocked JinjaThreads: theory JinjaThreads.JMM_J JinjaThreads: theory JinjaThreads.ProgressThreaded JinjaThreads: theory JinjaThreads.JVM_Execute JinjaThreads: theory JinjaThreads.JVM_Execute2 JinjaThreads: theory JinjaThreads.J_Execute JinjaThreads: theory JinjaThreads.Code_Generation JinjaThreads: theory JinjaThreads.BV_Main JinjaThreads: theory JinjaThreads.DRF_J JinjaThreads: theory JinjaThreads.Deadlocked JinjaThreads: theory JinjaThreads.ApprenticeChallenge JinjaThreads: theory JinjaThreads.BufferExample JinjaThreads: theory JinjaThreads.J_Main JinjaThreads: theory JinjaThreads.J0Bisim JinjaThreads: theory JinjaThreads.J0J1Bisim JinjaThreads: theory JinjaThreads.Java2Jinja JinjaThreads: theory JinjaThreads.Examples_Main JinjaThreads: theory JinjaThreads.Correctness1 JinjaThreads: theory JinjaThreads.Correctness1Threaded JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe JinjaThreads: theory JinjaThreads.Execute_Main JinjaThreads: theory JinjaThreads.JMM_J_Typesafe JinjaThreads: theory JinjaThreads.J1JVM JinjaThreads: theory JinjaThreads.JVMJ1 JinjaThreads: theory JinjaThreads.Correctness2 JinjaThreads: theory JinjaThreads.Correctness JinjaThreads: theory JinjaThreads.Compiler_Main JinjaThreads: theory JinjaThreads.JMM_Compiler JinjaThreads: theory JinjaThreads.SC_Interp JinjaThreads: theory JinjaThreads.JMM_Interp JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2 JinjaThreads: theory JinjaThreads.JMM JinjaThreads: theory JinjaThreads.MM_Main JinjaThreads: theory JinjaThreads.JinjaThreads Timing JinjaThreads (8 threads, 3863.513s elapsed time, 18311.164s cpu time, 6141.516s GC time, factor 4.74) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf Finished JinjaThreads (1:05:25 elapsed time, 5:12:57 cpu time, factor 4.78) Building Flyspeck-Tame ... Flyspeck-Tame: theory Flyspeck-Tame.ListAux Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order Flyspeck-Tame: theory Flyspeck-Tame.RTranCl Flyspeck-Tame: theory HOL-Library.AList Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat Flyspeck-Tame: theory HOL-Library.Code_Target_Int Flyspeck-Tame: theory HOL-Library.IArray Flyspeck-Tame: theory HOL-Library.While_Combinator Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso Flyspeck-Tame: theory HOL-Library.Code_Target_Nat Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral Flyspeck-Tame: theory Flyspeck-Tame.Arch Flyspeck-Tame: theory Flyspeck-Tame.Worklist Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax Flyspeck-Tame: theory Flyspeck-Tame.ListSum Flyspeck-Tame: theory Flyspeck-Tame.Rotation Flyspeck-Tame: theory Flyspeck-Tame.Graph Flyspeck-Tame: theory Flyspeck-Tame.Maps Flyspeck-Tame: theory Trie.Trie Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision Flyspeck-Tame: theory Flyspeck-Tame.GraphProps Flyspeck-Tame: theory Flyspeck-Tame.Tame Flyspeck-Tame: theory Trie.Tries Flyspeck-Tame: theory Flyspeck-Tame.Enumerator Flyspeck-Tame: theory Flyspeck-Tame.TameProps Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps Flyspeck-Tame: theory Flyspeck-Tame.Plane Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps Flyspeck-Tame: theory Flyspeck-Tame.Plane1 Flyspeck-Tame: theory Flyspeck-Tame.Generator Flyspeck-Tame: theory Flyspeck-Tame.TameEnum Flyspeck-Tame: theory Flyspeck-Tame.Invariants Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props Flyspeck-Tame: theory Flyspeck-Tame.LowerBound Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness Timing Flyspeck-Tame (8 threads, 110.391s elapsed time, 623.584s cpu time, 48.964s GC time, factor 5.65) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf Finished Flyspeck-Tame (0:02:42 elapsed time, 0:12:24 cpu time, factor 4.57) Running Flyspeck-Tame-Computation ... Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness Timing Flyspeck-Tame-Computation (8 threads, 27856.223s elapsed time, 41379.708s cpu time, 3164.520s GC time, factor 1.49) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation Finished Flyspeck-Tame-Computation (7:44:17 elapsed time, 11:29:41 cpu time, factor 1.49) Building AWN ... AWN: theory AWN.Lib AWN: theory AWN.TransitionSystems AWN: theory AWN.AWN AWN: theory AWN.Invariants AWN: theory AWN.OInvariants AWN: theory AWN.AWN_Cterms AWN: theory AWN.AWN_SOS AWN: theory AWN.OAWN_SOS AWN: theory AWN.AWN_Labels AWN: theory AWN.Pnet AWN: theory AWN.Inv_Cterms AWN: theory AWN.AWN_Invariants AWN: theory AWN.Closed AWN: theory AWN.AWN_SOS_Labels AWN: theory AWN.Qmsg AWN: theory AWN.OAWN_Invariants AWN: theory AWN.OAWN_SOS_Labels AWN: theory AWN.ONode_Lifting AWN: theory AWN.OPnet AWN: theory AWN.OPnet_Lifting AWN: theory AWN.OClosed_Lifting AWN: theory AWN.OClosed_Transfer AWN: theory AWN.OAWN_Convert AWN: theory AWN.Qmsg_Lifting AWN: theory AWN.AWN_Main AWN: theory AWN.Toy AWN: theory AWN.AWN_Term_Graph Timing AWN (8 threads, 56.144s elapsed time, 296.608s cpu time, 9.272s GC time, factor 5.28) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf Finished AWN (0:01:27 elapsed time, 0:06:07 cpu time, factor 4.20) Running AODV ... AODV: theory AODV.Aodv_Basic AODV: theory AODV.A_Norreqid AODV: theory AODV.Aodv_Data AODV: theory AODV.Aodv_Message AODV: theory AODV.B_Fwdrreps AODV: theory AODV.C_Gtobcast AODV: theory AODV.D_Fwdrreqs AODV: theory AODV.E_All_ABCD AODV: theory AODV.A_Aodv_Data AODV: theory AODV.A_Aodv_Message AODV: theory AODV.D_Aodv_Data AODV: theory AODV.D_Aodv_Message AODV: theory AODV.B_Aodv_Data AODV: theory AODV.B_Aodv_Message AODV: theory AODV.A_Fresher AODV: theory AODV.C_Aodv_Data AODV: theory AODV.Fresher AODV: theory AODV.B_Fresher AODV: theory AODV.C_Aodv_Message AODV: theory AODV.D_Fresher AODV: theory AODV.E_Aodv_Data AODV: theory AODV.E_Aodv_Message AODV: theory AODV.A_Aodv AODV: theory AODV.Aodv AODV: theory AODV.B_Aodv AODV: theory AODV.D_Aodv AODV: theory AODV.C_Fresher AODV: theory AODV.E_Fresher AODV: theory AODV.C_Aodv AODV: theory AODV.E_Aodv AODV: theory AODV.Aodv_Predicates AODV: theory AODV.Loop_Freedom AODV: theory AODV.Quality_Increases AODV: theory AODV.Seq_Invariants AODV: theory AODV.OAodv AODV: theory AODV.Global_Invariants AODV: theory AODV.Aodv_Loop_Freedom AODV: theory AODV.A_Aodv_Predicates AODV: theory AODV.A_OAodv AODV: theory AODV.A_Loop_Freedom AODV: theory AODV.A_Quality_Increases AODV: theory AODV.A_Seq_Invariants AODV: theory AODV.A_Global_Invariants AODV: theory AODV.A_Aodv_Loop_Freedom AODV: theory AODV.D_Aodv_Predicates AODV: theory AODV.D_OAodv AODV: theory AODV.D_Loop_Freedom AODV: theory AODV.C_Aodv_Predicates AODV: theory AODV.D_Quality_Increases AODV: theory AODV.C_Loop_Freedom AODV: theory AODV.C_Quality_Increases AODV: theory AODV.B_Aodv_Predicates AODV: theory AODV.C_Seq_Invariants AODV: theory AODV.D_Seq_Invariants AODV: theory AODV.B_Loop_Freedom AODV: theory AODV.B_Quality_Increases AODV: theory AODV.B_Seq_Invariants AODV: theory AODV.B_OAodv AODV: theory AODV.C_OAodv AODV: theory AODV.E_Aodv_Predicates AODV: theory AODV.E_OAodv AODV: theory AODV.E_Loop_Freedom AODV: theory AODV.E_Quality_Increases AODV: theory AODV.E_Seq_Invariants AODV: theory AODV.D_Global_Invariants AODV: theory AODV.B_Global_Invariants AODV: theory AODV.C_Global_Invariants AODV: theory AODV.E_Global_Invariants AODV: theory AODV.B_Aodv_Loop_Freedom AODV: theory AODV.D_Aodv_Loop_Freedom AODV: theory AODV.C_Aodv_Loop_Freedom AODV: theory AODV.E_Aodv_Loop_Freedom AODV: theory AODV.All Timing AODV (8 threads, 10256.541s elapsed time, 61925.684s cpu time, 5450.092s GC time, factor 6.04) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf Finished AODV (2:51:12 elapsed time, 17:12:34 cpu time, factor 6.03) Building HOL-Library ... HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.BNF_Corec HOL-Library: theory HOL-Library.Case_Converter HOL-Library: theory HOL-Library.Bit HOL-Library: theory HOL-Library.Cancellation HOL-Library: theory HOL-Library.Boolean_Algebra HOL-Library: theory HOL-Library.Monad_Syntax HOL-Library: theory HOL-Library.Char_ord HOL-Library: theory HOL-Library.State_Monad HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Prolog HOL-Library: theory HOL-Library.Code_Lazy HOL-Library: theory HOL-Library.Simps_Case_Conv HOL-Library: theory HOL-Library.Extended HOL-Library: theory HOL-Library.Code_Binary_Nat HOL-Library: theory HOL-Library.Multiset HOL-Library: theory HOL-Library.Code_Target_Nat HOL-Library: theory HOL-Library.Code_Target_Int HOL-Library: theory HOL-Library.Code_Test HOL-Library: theory HOL-Library.Comparator HOL-Library: theory HOL-Library.Code_Target_Numeral HOL-Library: theory HOL-Library.Conditional_Parametricity HOL-Library: theory HOL-Library.Datatype_Records HOL-Library: theory HOL-Library.DAList HOL-Library: theory HOL-Library.Debug HOL-Library: theory HOL-Library.Disjoint_Sets HOL-Library: theory HOL-Library.Dlist HOL-Library: theory HOL-Library.Dual_Ordered_Lattice HOL-Library: theory HOL-Library.Fun_Lexorder HOL-Library: theory HOL-Library.FuncSet HOL-Library: theory HOL-Library.Function_Algebras HOL-Library: theory HOL-Library.Function_Division HOL-Library: theory HOL-Library.Groups_Big_Fun HOL-Library: theory HOL-Library.IArray HOL-Library: theory HOL-Library.Infinite_Set HOL-Library: theory HOL-Library.Equipollence HOL-Library: theory HOL-Library.LaTeXsugar HOL-Library: theory HOL-Library.Lattice_Constructions HOL-Library: theory HOL-Library.Omega_Words_Fun HOL-Library: theory HOL-Library.Ramsey HOL-Library: theory HOL-Library.Lattice_Syntax HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Complete_Partial_Order2 HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.List_Lexorder HOL-Library: theory HOL-Library.Mapping HOL-Library: theory HOL-Library.More_List HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Poly_Mapping HOL-Library: theory HOL-Library.Stream HOL-Library: theory HOL-Library.Old_Datatype HOL-Library: theory HOL-Library.AList_Mapping HOL-Library: theory HOL-Library.Old_Recdef HOL-Library: theory HOL-Library.Open_State_Syntax HOL-Library: theory HOL-Library.Option_ord HOL-Library: theory HOL-Library.Parallel HOL-Library: theory HOL-Library.Pattern_Aliases HOL-Library: theory HOL-Library.Perm HOL-Library: theory HOL-Library.Phantom_Type HOL-Library: theory HOL-Library.Power_By_Squaring HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Library: theory HOL-Library.Preorder HOL-Library: theory HOL-Library.Product_Lexorder HOL-Library: theory HOL-Library.DAList_Multiset HOL-Library: theory HOL-Library.Multiset_Order HOL-Library: theory HOL-Library.Permutation HOL-Library: theory HOL-Library.Permutations HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Product_Plus HOL-Library: theory HOL-Library.Cardinality HOL-Library: theory HOL-Library.Quotient_Syntax HOL-Library: theory HOL-Library.Product_Order HOL-Library: theory HOL-Library.Quotient_Option HOL-Library: theory HOL-Library.Quotient_Product HOL-Library: theory HOL-Library.Quotient_Set HOL-Library: theory HOL-Library.Quotient_Sum HOL-Library: theory HOL-Library.Quotient_List HOL-Library: theory HOL-Library.Quotient_Type HOL-Library: theory HOL-Library.Finite_Lattice HOL-Library: theory HOL-Library.RBT_Impl HOL-Library: theory HOL-Library.Realizers HOL-Library: theory HOL-Library.Reflection HOL-Library: theory HOL-Library.Refute HOL-Library: theory HOL-Library.Rewrite HOL-Library: theory HOL-Library.Set_Algebras HOL-Library: theory HOL-Library.Sorting_Algorithms HOL-Library: theory HOL-Library.Stirling HOL-Library: theory HOL-Library.Sublist HOL-Library: theory HOL-Library.Numeral_Type HOL-Library: theory HOL-Library.Transitive_Closure_Table HOL-Library: theory HOL-Library.Tree HOL-Library: theory HOL-Library.Uprod HOL-Library: theory HOL-Library.While_Combinator HOL-Library: theory HOL-Library.Countable HOL-Library: theory HOL-Library.Type_Length HOL-Library: theory HOL-Library.BigO HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint HOL-Library: theory HOL-Library.Prefix_Order HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.Subseq_Order HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float HOL-Library: theory HOL-Library.Diagonal_Subsequence HOL-Library: theory HOL-Library.Discrete HOL-Library: theory HOL-Library.Going_To_Filter HOL-Library: theory HOL-Library.Indicator_Function HOL-Library: theory HOL-Library.Landau_Symbols HOL-Library: theory HOL-Library.Lattice_Algebras HOL-Library: theory HOL-Library.Countable_Set HOL-Library: theory HOL-Library.FSet HOL-Library: theory HOL-Library.Liminf_Limsup HOL-Library: theory HOL-Library.Log_Nat HOL-Library: theory HOL-Library.Lub_Glb HOL-Library: theory HOL-Library.Countable_Complete_Lattices HOL-Library: theory HOL-Library.Countable_Set_Type HOL-Library: theory HOL-Library.Set_Idioms HOL-Library: theory HOL-Library.Tree_Multiset HOL-Library: theory HOL-Library.Multiset_Permutations HOL-Library: theory HOL-Library.Nonpos_Ints HOL-Library: theory HOL-Library.OptionalSugar HOL-Library: theory HOL-Library.Periodic_Fun HOL-Library: theory HOL-Library.Quadratic_Discriminant HOL-Library: theory HOL-Library.Sum_of_Squares HOL-Library: theory HOL-Library.Tree_Real HOL-Library: theory HOL-Library.Order_Continuity HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Finite_Map HOL-Library: theory HOL-Library.Float HOL-Library: theory HOL-Library.Extended_Real HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Library: theory HOL-Library.Extended_Nonnegative_Real HOL-Library: theory HOL-Library.Library HOL-Library: theory HOL-Library.RBT HOL-Library: theory HOL-Library.RBT_Mapping HOL-Library: theory HOL-Library.RBT_Set Timing HOL-Library (8 threads, 132.550s elapsed time, 853.040s cpu time, 47.836s GC time, factor 6.44) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf Finished HOL-Library (0:03:26 elapsed time, 0:17:49 cpu time, factor 5.17) Building ConcurrentIMP ... ConcurrentIMP: theory ConcurrentIMP.CIMP_pred ConcurrentIMP: theory ConcurrentIMP.CIMP_lang ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg ConcurrentIMP: theory ConcurrentIMP.CIMP ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex Timing ConcurrentIMP (8 threads, 22.467s elapsed time, 58.656s cpu time, 3.084s GC time, factor 2.61) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf Finished ConcurrentIMP (0:00:49 elapsed time, 0:01:56 cpu time, factor 2.36) Running ConcurrentGC ... ConcurrentGC: theory ConcurrentGC.Model ConcurrentGC: theory ConcurrentGC.Tactics ConcurrentGC: theory ConcurrentGC.Proofs_basis ConcurrentGC: theory ConcurrentGC.TSO ConcurrentGC: theory ConcurrentGC.Handshakes ConcurrentGC: theory ConcurrentGC.MarkObject ConcurrentGC: theory ConcurrentGC.StrongTricolour ConcurrentGC: theory ConcurrentGC.Proofs ConcurrentGC: theory ConcurrentGC.Concrete_heap ConcurrentGC: theory ConcurrentGC.Concrete Timing ConcurrentGC (8 threads, 9484.261s elapsed time, 36652.904s cpu time, 2347.416s GC time, factor 3.86) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf Finished ConcurrentGC (2:38:11 elapsed time, 10:11:06 cpu time, factor 3.86) Building HOL-Word ... HOL-Word: theory HOL-Library.Bit HOL-Word: theory HOL-Library.Boolean_Algebra HOL-Word: theory HOL-Library.Phantom_Type HOL-Word: theory HOL-Word.Bit_Representation HOL-Word: theory HOL-Word.Bits HOL-Word: theory HOL-Word.Misc_Typedef HOL-Word: theory HOL-Word.Bits_Bit HOL-Word: theory HOL-Library.Cardinality HOL-Word: theory HOL-Word.Bool_List_Representation HOL-Word: theory HOL-Word.Misc_Arithmetic HOL-Word: theory HOL-Library.Numeral_Type HOL-Word: theory HOL-Word.Bits_Int HOL-Word: theory HOL-Library.Type_Length HOL-Word: theory HOL-Word.Word HOL-Word: theory HOL-Word.Word_Bitwise HOL-Word: theory HOL-Word.More_Word HOL-Word: theory HOL-Word.Word_Examples Timing HOL-Word (8 threads, 15.712s elapsed time, 84.356s cpu time, 2.884s GC time, factor 5.37) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf Finished HOL-Word (0:00:35 elapsed time, 0:02:04 cpu time, factor 3.53) Building Word_Lib ... Word_Lib: theory Word_Lib.Hex_Words Word_Lib: theory HOL-Library.Sublist Word_Lib: theory Word_Lib.Word_Type_Syntax Word_Lib: theory Word_Lib.Signed_Words Word_Lib: theory Word_Lib.Enumeration Word_Lib: theory Word_Lib.HOL_Lemmas Word_Lib: theory Word_Lib.More_Divides Word_Lib: theory Word_Lib.Norm_Words Word_Lib: theory Word_Lib.WordBitwise_Signed Word_Lib: theory Word_Lib.Word_Syntax Word_Lib: theory Word_Lib.Word_Lib Word_Lib: theory Word_Lib.Word_Enum Word_Lib: theory Word_Lib.Aligned Word_Lib: theory Word_Lib.Word_Setup_32 Word_Lib: theory Word_Lib.Word_Setup_64 Word_Lib: theory Word_Lib.Word_Next Word_Lib: theory Word_Lib.Word_Lemmas Word_Lib: theory Word_Lib.Word_Lemmas_32 Word_Lib: theory Word_Lib.Word_Lemmas_64 Timing Word_Lib (8 threads, 72.769s elapsed time, 211.672s cpu time, 6.112s GC time, factor 2.91) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf Finished Word_Lib (0:01:30 elapsed time, 0:04:08 cpu time, factor 2.74) Building IP_Addresses ... IP_Addresses: theory HOL-Eisbach.Eisbach IP_Addresses: theory HOL-Library.Cancellation IP_Addresses: theory HOL-Library.Infinite_Set IP_Addresses: theory HOL-Library.Option_ord IP_Addresses: theory IP_Addresses.NumberWang_IPv4 IP_Addresses: theory IP_Addresses.NumberWang_IPv6 IP_Addresses: theory HOL-Library.Multiset IP_Addresses: theory HOL-ex.Quicksort IP_Addresses: theory Automatic_Refinement.Misc IP_Addresses: theory HOL-Library.Code_Abstract_Nat IP_Addresses: theory HOL-Library.Product_Lexorder IP_Addresses: theory IP_Addresses.Lib_Numbers_toString IP_Addresses: theory IP_Addresses.Hs_Compat IP_Addresses: theory IP_Addresses.WordInterval IP_Addresses: theory HOL-Library.Code_Target_Nat IP_Addresses: theory IP_Addresses.Lib_List_toString IP_Addresses: theory IP_Addresses.Lib_Word_toString IP_Addresses: theory IP_Addresses.IP_Address IP_Addresses: theory IP_Addresses.WordInterval_Sorted IP_Addresses: theory IP_Addresses.IPv4 IP_Addresses: theory IP_Addresses.IPv6 IP_Addresses: theory IP_Addresses.Prefix_Match IP_Addresses: theory IP_Addresses.CIDR_Split IP_Addresses: theory IP_Addresses.IP_Address_Parser IP_Addresses: theory IP_Addresses.IP_Address_toString IP_Addresses: theory IP_Addresses.Prefix_Match_toString Timing IP_Addresses (8 threads, 344.225s elapsed time, 1127.668s cpu time, 59.208s GC time, factor 3.28) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf Finished IP_Addresses (0:06:25 elapsed time, 0:20:33 cpu time, factor 3.20) Building Simple_Firewall ... Simple_Firewall: theory HOL-Library.Char_ord Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State Simple_Firewall: theory Simple_Firewall.GroupF Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString Simple_Firewall: theory Simple_Firewall.List_Product_More Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries Simple_Firewall: theory Simple_Firewall.Option_Helpers Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString Simple_Firewall: theory Simple_Firewall.Iface Simple_Firewall: theory Simple_Firewall.L4_Protocol Simple_Firewall: theory Simple_Firewall.Simple_Packet Simple_Firewall: theory Simple_Firewall.Primitives_toString Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax Simple_Firewall: theory Simple_Firewall.SimpleFw_toString Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw Simple_Firewall: theory Simple_Firewall.Shadowed Simple_Firewall: theory Simple_Firewall.Service_Matrix Timing Simple_Firewall (8 threads, 27.984s elapsed time, 120.644s cpu time, 4.792s GC time, factor 4.31) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf Finished Simple_Firewall (0:00:56 elapsed time, 0:03:11 cpu time, factor 3.41) Building Routing ... Routing: theory Routing.Linorder_Helper Routing: theory HOL-Library.Adhoc_Overloading Routing: theory HOL-Library.Monad_Syntax Routing: theory Routing.Routing_Table Routing: theory Routing.IpRoute_Parser Routing: theory Routing.Linux_Router Timing Routing (8 threads, 13.656s elapsed time, 43.044s cpu time, 1.136s GC time, factor 3.15) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf Finished Routing (0:00:33 elapsed time, 0:01:22 cpu time, factor 2.49) Building Iptables_Semantics ... Iptables_Semantics: theory Iptables_Semantics.List_Misc Iptables_Semantics: theory Iptables_Semantics.Negation_Type Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists Iptables_Semantics: theory HOL-Library.Code_Target_Int Iptables_Semantics: theory HOL-Library.LaTeXsugar Iptables_Semantics: theory Native_Word.More_Bits_Int Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize Iptables_Semantics: theory Iptables_Semantics.Ternary Iptables_Semantics: theory Iptables_Semantics.Conntrack_State Iptables_Semantics: theory Iptables_Semantics.Firewall_Common Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags Iptables_Semantics: theory Iptables_Semantics.IpAddresses Iptables_Semantics: theory Iptables_Semantics.Word_Upto Iptables_Semantics: theory Iptables_Semantics.Ports Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet Iptables_Semantics: theory Native_Word.Bits_Integer Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int Iptables_Semantics: theory Iptables_Semantics.Semantics Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics Iptables_Semantics: theory Iptables_Semantics.Matching Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings Iptables_Semantics: theory Iptables_Semantics.Fixed_Action Iptables_Semantics: theory Iptables_Semantics.Optimizing Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold Iptables_Semantics: theory Iptables_Semantics.Ipassmt Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform Iptables_Semantics: theory Iptables_Semantics.Example_Semantics Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize Iptables_Semantics: theory Iptables_Semantics.No_Spoof Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace Iptables_Semantics: theory Iptables_Semantics.Interface_Replace Iptables_Semantics: theory Iptables_Semantics.Transform Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance Iptables_Semantics: theory Iptables_Semantics.Code_Interface Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings Iptables_Semantics: theory Iptables_Semantics.Documentation Iptables_Semantics: theory Iptables_Semantics.Parser Iptables_Semantics: theory Iptables_Semantics.Code_haskell Timing Iptables_Semantics (8 threads, 203.111s elapsed time, 967.200s cpu time, 67.832s GC time, factor 4.76) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf Finished Iptables_Semantics (0:04:22 elapsed time, 0:19:37 cpu time, factor 4.49) Building Iptables_Semantics_Examples ... Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation Timing Iptables_Semantics_Examples (8 threads, 404.569s elapsed time, 2875.544s cpu time, 251.972s GC time, factor 7.11) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf Finished Iptables_Semantics_Examples (0:07:12 elapsed time, 0:48:56 cpu time, factor 6.79) Running Iptables_Semantics_Examples_Big ... Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW Timing Iptables_Semantics_Examples_Big (8 threads, 13141.456s elapsed time, 68058.876s cpu time, 23910.952s GC time, factor 5.18) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf Finished Iptables_Semantics_Examples_Big (3:39:09 elapsed time, 18:54:48 cpu time, factor 5.18) === TIMING === Group slow: 17:58:15 elapsed time, 63:01:08 cpu time, factor 3.51 Group AFP: 18:24:16 elapsed time, 64:59:27 cpu time, factor 3.53 Group main: 0:10:47 elapsed time, 0:42:05 cpu time, factor 3.90 Group timing: 0:04:02 elapsed time, 0:19:54 cpu time, factor 4.93 Group very_slow: 11:23:27 elapsed time, 30:24:30 cpu time, factor 2.67 Overall: 18:36:38 elapsed time, 65:42:06 cpu time, factor 3.53 Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 1 second No emails were triggered. Finished: SUCCESS