Started by upstream project "isabelle-repo" build number 1531 originally caused by: Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall [isabelle-repo-makeall] $ hg showconfig paths.default [isabelle-repo-makeall] $ hg pull --rev 730fa992da38447dcea42acf9676599355d8d191 pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes adding changesets adding manifests adding file changes added 1 changesets with 1 changes to 1 files (run 'hg update' to get a working copy) [isabelle-repo-makeall] $ hg update --clean --rev 730fa992da38447dcea42acf9676599355d8d191 1 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-repo-makeall] $ hg log --rev . --template {node} [isabelle-repo-makeall] $ hg log --rev . --template {rev} [isabelle-repo-makeall] $ hg id --branch No emails were triggered. [isabelle-repo-makeall] $ /bin/sh -xe /tmp/jenkins1115252240311173944.sh + Admin/jenkins/run_build makeall + set -e + PROFILE=makeall + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ci_build_makeall === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-5/x86_64-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="-H 4000 --maxheap 8G" === BUILD === Build started at Sun, 18 Mar 2018 01:10:17 GMT Isabelle id 730fa992da38 === LOG === Session Pure/Pure Session CTT/CTT Session Cube/Cube Session FOL/FOL Session CCL/CCL Session FOL/FOL-ex Session FOLP/FOLP Session FOLP/FOLP-ex Session HOL/HOL (main) Session Doc/Classes (doc) Session Doc/Functions (doc) Session HOL/HOL-Eisbach Session Doc/Eisbach (doc) Session HOL/HOL-Hoare Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-IMPP Session HOL/HOL-IOA Session HOL/HOL-Import Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session Doc/Codegen_Basics Session Doc/Codegen (doc) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Cardinals (timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session HOL/HOL-Analysis (main timing) Session HOL/HOL-Analysis-ex Session HOL/HOL-Probability (main timing) Session HOL/HOL-Probability-ex (timing) Session HOL/HOL-Isar_Examples Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session HOL/HOL-Codegenerator_Test Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-Hahn_Banach Session HOL/HOL-IMP (timing) Session HOL/HOL-Imperative_HOL (timing) Session HOL/HOL-Induct Session HOL/HOL-Matrix_LP Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mutabelle Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal Session HOL/HOL-Nominal-Examples (timing) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-TPTP Session HOL/HOL-Unix Session HOL/HOL-ZF Session Doc/Isar_Ref (doc) Session Doc/Typeclass_Hierarchy_Basics Session Doc/Typeclass_Hierarchy (doc) Session HOL/HOL-Mirabelle Session HOL/HOL-Mirabelle-ex Session HOL/HOL-NanoJava Session HOL/HOL-Prolog Session HOL/HOL-Statespace Session HOL/HOL-TLA Session HOL/HOL-TLA-Buffer Session HOL/HOL-TLA-Inc Session HOL/HOL-TLA-Memory Session HOL/HOL-Types_To_Sets Session HOL/HOL-Word (main timing) Session HOL/HOL-SPARK (main) Session HOL/HOL-SPARK-Examples Session HOL/HOL-SPARK-Manual Session HOL/HOL-Word-SMT_Examples (timing) Session HOL/HOLCF (main timing) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session HOL/HOLCF-Tutorial Session HOL/IOA (timing) Session HOL/IOA-ABP Session HOL/IOA-NTP Session HOL/IOA-Storage Session HOL/IOA-ex Session Doc/How_to_Prove_it Session Doc/Implementation (doc) Session Doc/JEdit (doc) Session Doc/Locales (doc) Session Doc/Main (doc) Session Doc/Prog_Prove (doc) Session Doc/Sugar (doc) Session Doc/Tutorial (doc) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session HOL/HOL-Proofs-ex Session Doc/Intro (doc) Session LCF/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Unsorted/SML Session Sequents/Sequents Session Doc/Sledgehammer (doc) Session Unsorted/Spec_Check Session Doc/System (doc) Session ZF/ZF (main timing) Session Doc/Logics_ZF (doc) Session ZF/ZF-AC Session ZF/ZF-Coind Session ZF/ZF-Constructible Session ZF/ZF-IMP Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Session ZF/ZF-Resid Session ZF/ZF-ex Cleaning Pure ... Cleaning SML ... Cleaning Sequents ... Cleaning Sledgehammer ... Cleaning Spec_Check ... Cleaning System ... Cleaning ZF ... Cleaning ZF-AC ... Cleaning ZF-Coind ... Cleaning ZF-Constructible ... Cleaning ZF-IMP ... Cleaning ZF-Induct ... Cleaning ZF-UNITY ... Cleaning ZF-Resid ... Cleaning ZF-ex ... Cleaning Nitpick ... Cleaning Logics_ZF ... Cleaning Logics ... Cleaning LCF ... Cleaning Intro ... Cleaning HOL-Proofs ... Cleaning HOL-Proofs-Extraction ... Cleaning HOL-Proofs-Lambda ... Cleaning HOL-Proofs-ex ... Cleaning HOL ... Cleaning HOL-Analysis ... Cleaning HOL-Analysis-ex ... Cleaning HOL-Probability ... Cleaning HOL-Probability-ex ... Cleaning HOL-Data_Structures ... Cleaning HOL-Eisbach ... Cleaning HOL-Hoare ... Cleaning HOL-Hoare_Parallel ... Cleaning HOL-IMPP ... Cleaning HOL-IOA ... Cleaning HOL-Import ... Cleaning HOL-Lattice ... Cleaning HOL-Library ... Cleaning HOL-Auth ... Cleaning HOL-UNITY ... Cleaning HOL-Bali ... Cleaning HOL-Cardinals ... Cleaning HOL-Computational_Algebra ... Cleaning HOL-Algebra ... Cleaning HOL-Decision_Procs ... Cleaning HOL-Quotient_Examples ... Cleaning HOL-Isar_Examples ... Cleaning HOL-Nonstandard_Analysis ... Cleaning HOL-Nonstandard_Analysis-Examples ... Cleaning HOL-Number_Theory ... Cleaning HOL-Codegenerator_Test ... Cleaning HOL-ex ... Cleaning HOL-Corec_Examples ... Cleaning HOL-Datatype_Examples ... Cleaning HOL-Hahn_Banach ... Cleaning HOL-IMP ... Cleaning HOL-Imperative_HOL ... Cleaning HOL-Induct ... Cleaning HOL-Matrix_LP ... Cleaning HOL-Metis_Examples ... Cleaning HOL-MicroJava ... Cleaning HOL-Mutabelle ... Cleaning HOL-Nitpick_Examples ... Cleaning HOL-Nominal ... Cleaning HOL-Nominal-Examples ... Cleaning HOL-Predicate_Compile_Examples ... Cleaning HOL-Quickcheck_Examples ... Cleaning HOL-SET_Protocol ... Cleaning HOL-TPTP ... Cleaning HOL-Unix ... Cleaning HOL-ZF ... Cleaning Isar_Ref ... Cleaning Typeclass_Hierarchy_Basics ... Cleaning Typeclass_Hierarchy ... Cleaning HOL-Mirabelle ... Cleaning HOL-Mirabelle-ex ... Cleaning HOL-NanoJava ... Cleaning HOL-Prolog ... Cleaning HOL-Statespace ... Cleaning HOL-TLA ... Cleaning HOL-TLA-Buffer ... Cleaning HOL-TLA-Inc ... Cleaning HOL-TLA-Memory ... Cleaning HOL-Types_To_Sets ... Cleaning HOL-Word ... Cleaning HOL-SPARK ... Cleaning HOL-SPARK-Examples ... Cleaning HOL-SPARK-Manual ... Cleaning HOL-Word-SMT_Examples ... Cleaning HOLCF ... Cleaning HOLCF-IMP ... Cleaning HOLCF-Library ... Cleaning HOLCF-FOCUS ... Cleaning HOLCF-ex ... Cleaning HOLCF-Tutorial ... Cleaning IOA ... Cleaning IOA-ABP ... Cleaning IOA-NTP ... Cleaning IOA-Storage ... Cleaning IOA-ex ... Cleaning How_to_Prove_it ... Cleaning Implementation ... Cleaning JEdit ... Cleaning Locales ... Cleaning Main ... Cleaning Prog_Prove ... Cleaning Sugar ... Cleaning Tutorial ... Cleaning Functions ... Cleaning FOLP ... Cleaning FOLP-ex ... Cleaning FOL ... Cleaning FOL-ex ... Cleaning Eisbach ... Cleaning Datatypes ... Cleaning Cube ... Cleaning Corec ... Cleaning Codegen_Basics ... Cleaning Codegen ... Cleaning Classes ... Cleaning CTT ... Cleaning CCL ... Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Pure: theory Pure.Sessions Timing Pure (1 threads, 0.711s elapsed time, 0.716s cpu time, 0.000s GC time, factor 1.01) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.97) Building HOL ... Building ZF ... Building HOL-Proofs ... ZF: theory IFOL ZF: theory FOL HOL: theory HOL.Code_Generator HOL-Proofs: theory HOL.Code_Generator ZF: theory ZF.ZF_Base ZF: theory ZF.upair ZF: theory ZF.pair ZF: theory ZF.Bool ZF: theory ZF.equalities ZF: theory ZF.Fixedpt ZF: theory ZF.Sum HOL: theory HOL.HOL ZF: theory ZF.func HOL-Proofs: theory HOL.HOL ZF: theory ZF.Perm ZF: theory ZF.QPair ZF: theory ZF.Trancl ZF: theory ZF.EquivClass ZF: theory ZF.WF ZF: theory ZF.Order ZF: theory ZF.Ordinal ZF: theory ZF.OrdQuant ZF: theory ZF.OrderArith ZF: theory ZF.Nat_ZF ZF: theory ZF.Epsilon ZF: theory ZF.OrderType ZF: theory ZF.Inductive_ZF ZF: theory ZF.Finite ZF: theory ZF.Cardinal ZF: theory ZF.Univ ZF: theory ZF.Arith ZF: theory ZF.QUniv ZF: theory ZF.Datatype_ZF ZF: theory ZF.ArithSimp ZF: theory ZF.Int_ZF ZF: theory ZF.CardinalArith HOL: theory HOL.Argo HOL: theory HOL.Ctr_Sugar ZF: theory ZF.List_ZF ZF: theory ZF.Bin HOL-Proofs: theory HOL.Argo HOL-Proofs: theory HOL.Ctr_Sugar ZF: theory ZF.IntDiv_ZF HOL: theory HOL.Orderings HOL-Proofs: theory HOL.Orderings HOL: theory HOL.SAT ZF: theory ZF ZF: theory ZF.AC ZF: theory ZF.Zorn ZF: theory ZF.Cardinal_AC ZF: theory ZF.InfDatatype ZF: theory ZFC HOL-Proofs: theory HOL.SAT HOL: theory HOL.Groups HOL-Proofs: theory HOL.Groups HOL: theory HOL.Lattices HOL: theory HOL.Set HOL: theory HOL.Fun HOL-Proofs: theory HOL.Lattices HOL: theory HOL.Typedef HOL: theory HOL.Rings HOL: theory HOL.Complete_Lattices HOL: theory HOL.Inductive HOL-Proofs: theory HOL.Set HOL: theory HOL.Product_Type HOL: theory HOL.Complete_Partial_Order HOL: theory HOL.Sum_Type HOL-Proofs: theory HOL.Fun HOL-Proofs: theory HOL.Typedef HOL-Proofs: theory HOL.Rings HOL: theory HOL.Nat HOL-Proofs: theory HOL.Complete_Lattices HOL: theory HOL.Fields HOL: theory HOL.Meson HOL: theory HOL.ATP HOL-Proofs: theory HOL.Inductive HOL: theory HOL.Metis HOL: theory HOL.Finite_Set Timing ZF (2 threads, 21.801s elapsed time, 37.040s cpu time, 2.320s GC time, factor 1.70) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf Finished ZF (0:00:33 elapsed time, 0:00:56 cpu time, factor 1.69) Building ZF-Induct ... ZF-Induct: theory ZF-Induct.Acc ZF-Induct: theory ZF-Induct.Binary_Trees ZF-Induct: theory ZF-Induct.Comb ZF-Induct: theory ZF-Induct.Datatypes ZF-Induct: theory ZF-Induct.FoldSet ZF-Induct: theory ZF-Induct.ListN ZF-Induct: theory ZF-Induct.Mutil ZF-Induct: theory ZF-Induct.Multiset ZF-Induct: theory ZF-Induct.Ntree ZF-Induct: theory ZF-Induct.Primrec ZF-Induct: theory ZF-Induct.PropLog HOL: theory HOL.Relation HOL-Proofs: theory HOL.Product_Type ZF-Induct: theory ZF-Induct.Rmap ZF-Induct: theory ZF-Induct.Term ZF-Induct: theory ZF-Induct.Tree_Forest ZF-Induct: theory ZF-Induct.Brouwer HOL: theory HOL.Transitive_Closure HOL-Proofs: theory HOL.Complete_Partial_Order HOL: theory HOL.Wellfounded HOL: theory HOL.Fun_Def_Base HOL-Proofs: theory HOL.Sum_Type 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-Proofs: theory HOL.Nat HOL: theory HOL.BNF_Def HOL: theory HOL.BNF_Composition HOL: theory HOL.Basic_BNFs HOL-Proofs: theory HOL.Fields HOL: theory HOL.BNF_Fixpoint_Base HOL-Proofs: theory HOL.Meson HOL-Proofs: theory HOL.ATP Timing ZF-Induct (2 threads, 6.541s elapsed time, 10.600s cpu time, 0.440s GC time, factor 1.62) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf Finished ZF-Induct (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.60) Building FOL ... FOL: theory IFOL FOL: theory FOL HOL: theory HOL.BNF_Least_Fixpoint HOL-Proofs: theory HOL.Metis HOL: theory HOL.Basic_BNF_LFPs HOL: theory HOL.Transfer HOL-Proofs: theory HOL.Finite_Set HOL: theory HOL.Num Timing FOL (2 threads, 3.115s elapsed time, 3.456s cpu time, 0.160s GC time, factor 1.11) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf Finished FOL (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.34) Building FOLP ... FOLP: theory IFOLP FOLP: theory FOLP HOL: theory HOL.Power Timing FOLP (2 threads, 1.079s elapsed time, 1.092s cpu time, 0.000s GC time, factor 1.01) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP Finished FOLP (0:00:02 elapsed time) Running ZF-UNITY ... ZF-UNITY: theory ZF-UNITY.MultisetSum ZF-UNITY: theory ZF-UNITY.GenPrefix ZF-UNITY: theory ZF-UNITY.State ZF-UNITY: theory ZF-UNITY.UNITY ZF-UNITY: theory ZF-UNITY.Monotonicity HOL: theory HOL.Groups_Big ZF-UNITY: theory ZF-UNITY.Constrains ZF-UNITY: theory ZF-UNITY.FP ZF-UNITY: theory ZF-UNITY.WFair ZF-UNITY: theory ZF-UNITY.Increasing ZF-UNITY: theory ZF-UNITY.SubstAx ZF-UNITY: theory ZF-UNITY.Follows ZF-UNITY: theory ZF-UNITY.Mutex HOL-Proofs: theory HOL.Relation HOL: theory HOL.Equiv_Relations ZF-UNITY: theory ZF-UNITY.Union ZF-UNITY: theory ZF-UNITY.Comp HOL: theory HOL.Lifting ZF-UNITY: theory ZF-UNITY.Guar ZF-UNITY: theory ZF-UNITY.AllocBase ZF-UNITY: theory ZF-UNITY.ClientImpl ZF-UNITY: theory ZF-UNITY.Distributor ZF-UNITY: theory ZF-UNITY.Merge ZF-UNITY: theory ZF-UNITY.AllocImpl HOL: theory HOL.Lifting_Set HOL: theory HOL.Option HOL: theory HOL.Quotient HOL: theory HOL.Extraction HOL-Proofs: theory HOL.Transitive_Closure HOL: theory HOL.Lattices_Big HOL: theory HOL.Partial_Function HOL: theory HOL.Fun_Def HOL-Proofs: theory HOL.Wellfounded HOL: theory HOL.Int HOL-Proofs: theory HOL.Fun_Def_Base HOL-Proofs: theory HOL.Hilbert_Choice HOL: theory HOL.Euclidean_Division HOL-Proofs: theory HOL.Wfrec HOL-Proofs: theory HOL.Order_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.Parity HOL-Proofs: theory HOL.Zorn Timing ZF-UNITY (2 threads, 14.562s elapsed time, 26.912s cpu time, 0.956s GC time, factor 1.85) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY Finished ZF-UNITY (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.77) Running ZF-Constructible ... HOL-Proofs: theory HOL.BNF_Wellorder_Embedding ZF-Constructible: theory ZF-Constructible.MetaExists ZF-Constructible: theory ZF-Constructible.Formula ZF-Constructible: theory ZF-Constructible.Normal ZF-Constructible: theory ZF-Constructible.Reflection ZF-Constructible: theory ZF-Constructible.Relative HOL-Proofs: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.Divides ZF-Constructible: theory ZF-Constructible.L_axioms ZF-Constructible: theory ZF-Constructible.Wellorderings ZF-Constructible: theory ZF-Constructible.WFrec ZF-Constructible: theory ZF-Constructible.WF_absolute ZF-Constructible: theory ZF-Constructible.Datatype_absolute ZF-Constructible: theory ZF-Constructible.Rank HOL: theory HOL.Code_Numeral HOL: theory HOL.Numeral_Simprocs ZF-Constructible: theory ZF-Constructible.Separation HOL: theory HOL.Semiring_Normalization HOL: theory HOL.SMT ZF-Constructible: theory ZF-Constructible.Internalize ZF-Constructible: theory ZF-Constructible.AC_in_L HOL: theory HOL.Set_Interval ZF-Constructible: theory ZF-Constructible.Rec_Separation HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation ZF-Constructible: theory ZF-Constructible.Rank_Separation ZF-Constructible: theory ZF-Constructible.Satisfies_absolute HOL: theory HOL.Groebner_Basis ZF-Constructible: theory ZF-Constructible.DPow_absolute HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.Filter HOL: theory HOL.Presburger HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic HOL-Proofs: theory HOL.BNF_Def HOL: theory HOL.Sledgehammer HOL: theory HOL.List HOL-Proofs: theory HOL.BNF_Composition HOL-Proofs: theory HOL.Basic_BNFs HOL-Proofs: theory HOL.BNF_Fixpoint_Base Timing ZF-Constructible (2 threads, 15.119s elapsed time, 28.648s cpu time, 5.316s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf Finished ZF-Constructible (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.84) Running ZF-ex ... ZF-ex: theory ZF-ex.BinEx ZF-ex: theory ZF-ex.CoUnit ZF-ex: theory ZF-ex.Commutation ZF-ex: theory ZF-ex.Group ZF-ex: theory ZF-ex.LList HOL-Proofs: theory HOL.BNF_Least_Fixpoint ZF-ex: theory ZF-ex.Limit ZF-ex: theory ZF-ex.Ring ZF-ex: theory ZF-ex.NatSum ZF-ex: theory ZF-ex.Primes HOL: theory HOL.Groups_List ZF-ex: theory ZF-ex.Ramsey ZF-ex: theory ZF-ex.misc HOL: theory HOL.Map HOL: theory HOL.Factorial HOL: theory HOL.Binomial HOL: theory HOL.GCD HOL: theory HOL.Enum HOL-Proofs: theory HOL.Basic_BNF_LFPs HOL-Proofs: theory HOL.Transfer HOL-Proofs: theory HOL.Num HOL: theory HOL.String HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Predicate HOL: theory HOL.Lazy_Sequence HOL: theory HOL.Limited_Sequence HOL: theory HOL.Typerep HOL-Proofs: theory HOL.Power HOL: theory HOL.Code_Evaluation Timing ZF-ex (2 threads, 10.579s elapsed time, 15.516s cpu time, 0.468s GC time, factor 1.47) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex Finished ZF-ex (0:00:11 elapsed time, 0:00:15 cpu time, factor 1.39) Running CCL ... HOL: theory HOL.Random CCL: theory IFOL HOL: theory HOL.Quickcheck_Random CCL: theory FOL HOL-Proofs: theory HOL.Groups_Big HOL: theory HOL.Quickcheck_Exhaustive HOL: theory HOL.Quickcheck_Narrowing CCL: theory CCL.Set CCL: theory CCL.Lfp CCL: theory CCL.Gfp CCL: theory CCL.CCL CCL: theory CCL.Term CCL: theory CCL.Trancl CCL: theory CCL.Type CCL: theory CCL.Fix CCL: theory CCL.Hered CCL: theory CCL.Wfd CCL: theory CCL.Nat CCL: theory CCL.List CCL: theory CCL.Flag CCL: theory CCL.Stream HOL: theory HOL.Random_Pred Timing CCL (2 threads, 5.628s elapsed time, 7.996s cpu time, 0.500s GC time, factor 1.42) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL Finished CCL (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.29) Running FOL-ex ... FOL-ex: theory FOL-ex.Classical FOL-ex: theory FOL-ex.If FOL-ex: theory FOL-ex.Intro FOL-ex: theory FOL-ex.Miniscope FOL-ex: theory FOL-ex.Nat FOL-ex: theory FOL-ex.Nat_Class FOL-ex: theory FOL-ex.Natural_Numbers FOL-ex: theory FOL-ex.Prolog HOL: theory HOL.Random_Sequence FOL-ex: theory FOL-ex.Propositional_Cla HOL: theory HOL.Record FOL-ex: theory FOL-ex.Quantifiers_Cla FOL-ex: theory FOL-ex.Foundation FOL-ex: theory FOL-ex.Intuitionistic FOL-ex: theory FOL-ex.Propositional_Int FOL-ex: theory FOL-ex.Quantifiers_Int HOL: theory HOL.Predicate_Compile HOL: theory HOL.Nitpick FOL-ex: theory FOL-ex.Locale_Test1 HOL-Proofs: theory HOL.Equiv_Relations FOL-ex: theory FOL-ex.Locale_Test2 FOL-ex: theory FOL-ex.Locale_Test3 FOL-ex: theory FOL-ex.Locale_Test HOL: theory HOL.Nunchaku HOL-Proofs: theory HOL.Lifting HOL: theory Main Timing FOL-ex (2 threads, 5.423s elapsed time, 7.604s cpu time, 0.200s GC time, factor 1.40) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf Finished FOL-ex (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.46) Running ZF-AC ... ZF-AC: theory ZF-AC.AC_Equiv ZF-AC: theory ZF-AC.AC18_AC19 ZF-AC: theory ZF-AC.AC7_AC9 ZF-AC: theory ZF-AC.Cardinal_aux ZF-AC: theory ZF-AC.Hartog ZF-AC: theory ZF-AC.WO6_WO1 ZF-AC: theory ZF-AC.AC16_lemmas ZF-AC: theory ZF-AC.AC16_WO4 ZF-AC: theory ZF-AC.DC ZF-AC: theory ZF-AC.HH HOL: theory HOL.Archimedean_Field HOL: theory HOL.Topological_Spaces ZF-AC: theory ZF-AC.AC15_WO6 ZF-AC: theory ZF-AC.AC17_AC1 ZF-AC: theory ZF-AC.WO1_AC ZF-AC: theory ZF-AC.WO1_WO7 ZF-AC: theory ZF-AC.WO2_AC16 HOL-Proofs: theory HOL.Lifting_Set HOL-Proofs: theory HOL.Option HOL-Proofs: theory HOL.Quotient HOL: theory HOL.Rat HOL-Proofs: theory HOL.Extraction HOL: theory HOL.Real HOL-Proofs: theory HOL.Lattices_Big HOL-Proofs: theory HOL.Partial_Function HOL: theory HOL.Real_Vector_Spaces HOL-Proofs: theory HOL.Fun_Def Timing ZF-AC (2 threads, 5.547s elapsed time, 9.376s cpu time, 0.504s GC time, factor 1.69) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf Finished ZF-AC (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.61) Running FOLP-ex ... FOLP-ex: theory FOLP-ex.Classical FOLP-ex: theory FOLP-ex.If FOLP-ex: theory FOLP-ex.Intro FOLP-ex: theory FOLP-ex.Nat FOLP-ex: theory FOLP-ex.Propositional_Cla FOLP-ex: theory FOLP-ex.Quantifiers_Cla FOLP-ex: theory FOLP-ex.Foundation FOLP-ex: theory FOLP-ex.Intuitionistic HOL-Proofs: theory HOL.Int FOLP-ex: theory FOLP-ex.Propositional_Int FOLP-ex: theory FOLP-ex.Quantifiers_Int Timing FOLP-ex (2 threads, 3.534s elapsed time, 6.128s cpu time, 0.108s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex Finished FOLP-ex (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.49) Running Sequents ... Sequents: theory Sequents.Sequents Sequents: theory Sequents.LK0 Sequents: theory Sequents.ILL Sequents: theory Sequents.ILL_predlog Sequents: theory Sequents.Washing Sequents: theory Sequents.LK Sequents: theory Sequents.Modal0 Sequents: theory Sequents.S4 Sequents: theory Sequents.S43 Sequents: theory Sequents.Hard_Quantifiers Sequents: theory Sequents.Nat Sequents: theory Sequents.Propositional Sequents: theory Sequents.Quantifiers Sequents: theory Sequents.T HOL: theory HOL.Inequalities HOL: theory HOL.Limits HOL-Proofs: theory HOL.Euclidean_Division Timing Sequents (2 threads, 3.405s elapsed time, 6.640s cpu time, 0.124s GC time, factor 1.95) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents Finished Sequents (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.65) Running LCF ... LCF: theory IFOL HOL: theory HOL.Deriv LCF: theory FOL HOL: theory HOL.NthRoot HOL: theory HOL.Series LCF: theory LCF.LCF HOL: theory HOL.Transcendental LCF: theory LCF.Ex1 LCF: theory LCF.Ex2 LCF: theory LCF.Ex3 LCF: theory LCF.Ex4 Timing LCF (2 threads, 3.319s elapsed time, 3.760s cpu time, 0.136s GC time, factor 1.13) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF Finished LCF (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.99) Running Spec_Check ... Spec_Check: theory Spec_Check.Spec_Check Spec_Check: theory Spec_Check.Examples Timing Spec_Check (2 threads, 1.757s elapsed time, 2.960s cpu time, 0.016s GC time, factor 1.68) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time) Running ZF-Resid ... HOL: theory HOL.Complex HOL: theory HOL.MacLaurin ZF-Resid: theory ZF-Resid.Redex ZF-Resid: theory ZF-Resid.Substitution ZF-Resid: theory ZF-Resid.Residuals HOL-Proofs: theory HOL.Parity ZF-Resid: theory ZF-Resid.Reduction ZF-Resid: theory ZF-Resid.Confluence HOL: theory Complex_Main Timing ZF-Resid (2 threads, 1.516s elapsed time, 2.544s cpu time, 0.000s GC time, factor 1.68) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid Finished ZF-Resid (0:00:02 elapsed time) Running ZF-IMP ... ZF-IMP: theory ZF-IMP.Com ZF-IMP: theory ZF-IMP.Denotation ZF-IMP: theory ZF-IMP.Equiv HOL-Proofs: theory HOL.Divides Timing ZF-IMP (2 threads, 1.004s elapsed time, 1.208s cpu time, 0.000s GC time, factor 1.20) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/outline.pdf Finished ZF-IMP (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.56) Running CTT ... CTT: theory CTT.CTT CTT: theory CTT.Elimination CTT: theory CTT.Equality CTT: theory CTT.Synthesis CTT: theory CTT.Typechecking Timing CTT (2 threads, 0.861s elapsed time, 1.248s cpu time, 0.000s GC time, factor 1.45) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf Finished CTT (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.65) Running ZF-Coind ... ZF-Coind: theory ZF-Coind.Language ZF-Coind: theory ZF-Coind.Map ZF-Coind: theory ZF-Coind.Types ZF-Coind: theory ZF-Coind.Values ZF-Coind: theory ZF-Coind.Dynamic ZF-Coind: theory ZF-Coind.Static ZF-Coind: theory ZF-Coind.ECR HOL-Proofs: theory HOL.Code_Numeral Timing ZF-Coind (2 threads, 0.639s elapsed time, 1.264s cpu time, 0.000s GC time, factor 1.98) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind Finished ZF-Coind (0:00:01 elapsed time) Running Cube ... Cube: theory Cube.Cube Cube: theory Cube.Example Timing Cube (2 threads, 0.325s elapsed time, 0.332s cpu time, 0.000s GC time, factor 1.02) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube Finished Cube (0:00:00 elapsed time) Running Intro ... HOL-Proofs: theory HOL.Numeral_Simprocs HOL-Proofs: theory HOL.Semiring_Normalization Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf Finished Intro (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.08) Running Logics ... HOL-Proofs: theory HOL.SMT HOL-Proofs: theory HOL.Set_Interval Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf Finished Logics (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.09) Running System ... System: theory System.Base System: theory System.Environment System: theory System.Misc System: theory System.Presentation System: theory System.Scala System: theory System.Sessions Timing System (2 threads, 0.293s elapsed time, 0.412s cpu time, 0.000s GC time, factor 1.41) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf Finished System (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.13) Running Logics_ZF ... Logics_ZF: theory Logics_ZF.If Logics_ZF: theory Logics_ZF.FOL_examples Logics_ZF: theory Logics_ZF.ZF_Isar Logics_ZF: theory Logics_ZF.ZF_examples Logics_ZF: theory Logics_ZF.IFOL_examples Timing Logics_ZF (2 threads, 0.277s elapsed time, 0.548s cpu time, 0.000s GC time, factor 1.98) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf Finished Logics_ZF (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.14) Running Nitpick ... HOL-Proofs: theory HOL.Conditionally_Complete_Lattices Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf Finished Nitpick (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.12) Running SML ... SML: theory SML.Examples Timing SML (2 threads, 0.026s elapsed time, 0.028s cpu time, 0.000s GC time, factor 1.08) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML Finished SML (0:00:00 elapsed time) Running Sledgehammer ... HOL-Proofs: theory HOL.Filter Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf Finished Sledgehammer (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.13) HOL-Proofs: theory HOL.Groebner_Basis HOL-Proofs: theory HOL.Presburger HOL-Proofs: theory HOL.Sledgehammer HOL-Proofs: theory HOL.List HOL-Proofs: theory HOL.Groups_List HOL-Proofs: theory HOL.Factorial HOL-Proofs: theory HOL.Binomial HOL-Proofs: theory HOL.GCD HOL-Proofs: theory HOL.Map HOL-Proofs: theory HOL.Enum Timing HOL (2 threads, 243.369s elapsed time, 454.032s cpu time, 47.992s GC time, factor 1.87) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf Finished HOL (0:05:13 elapsed time, 0:09:22 cpu time, factor 1.80) Building HOL-Library ... Building HOLCF ... HOLCF: theory HOL-Library.Nat_Bijection HOLCF: theory HOL-Library.Old_Datatype HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.Lattice_Syntax HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.BNF_Corec HOLCF: theory HOLCF.Porder HOLCF: theory HOL-Library.Countable HOLCF: theory HOLCF.Pcpo HOL-Library: theory HOL-Library.DAList HOLCF: theory HOLCF.Cont HOLCF: theory HOLCF.Adm HOLCF: theory HOLCF.Discrete HOLCF: theory HOLCF.Cpodef HOLCF: theory HOLCF.Fun_Cpo HOLCF: theory HOLCF.Product_Cpo HOLCF: theory HOLCF.Cfun HOL-Library: theory HOL-Library.Bit HOL-Library: theory HOL-Library.Boolean_Algebra HOLCF: theory HOLCF.Completion HOLCF: theory HOLCF.Cprod HOLCF: theory HOLCF.Deflation HOL-Library: theory HOL-Library.Cancellation HOL-Proofs: theory HOL.String HOLCF: theory HOLCF.Fix HOLCF: theory HOLCF.Sfun HOLCF: theory HOLCF.Sprod HOLCF: theory HOLCF.Up HOL-Library: theory HOL-Library.Multiset HOLCF: theory HOLCF.Lift HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint HOLCF: theory HOLCF.One HOLCF: theory HOLCF.Tr HOLCF: theory HOLCF.Ssum HOLCF: theory HOLCF.Fixrec HOLCF: theory HOLCF.Map_Functions HOLCF: theory HOLCF.Bifinite HOLCF: theory HOLCF.Domain_Aux HOL-Library: theory HOL-Library.Cardinal_Notations HOL-Library: theory HOL-Library.Char_ord HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Binary_Nat HOLCF: theory HOLCF.Universal HOL-Library: theory HOL-Library.Code_Target_Nat HOL-Library: theory HOL-Library.Code_Char HOL-Library: theory HOL-Library.Code_Prolog HOL-Library: theory HOL-Library.Code_Target_Int HOL-Library: theory HOL-Library.Code_Target_Numeral HOL-Library: theory HOL-Library.Code_Test HOL-Library: theory HOL-Library.DAList_Multiset HOLCF: theory HOLCF.Algebraic HOLCF: theory HOLCF.Compact_Basis HOLCF: theory HOLCF.LowerPD HOLCF: theory HOLCF.UpperPD HOL-Library: theory HOL-Library.Multiset_Order HOL-Library: theory HOL-Library.Permutation HOLCF: theory HOLCF.Representable HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Complete_Partial_Order2 HOLCF: theory HOLCF.ConvexPD HOL-Library: theory HOL-Library.Conditional_Parametricity HOL-Library: theory HOL-Library.Datatype_Records HOL-Library: theory HOL-Library.Debug HOL-Library: theory HOL-Library.Disjoint_Sets HOL-Library: theory HOL-Library.Permutations HOLCF: theory HOLCF.Domain HOL-Library: theory HOL-Library.Dlist HOL-Proofs: theory HOL.Predicate 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.Groups_Big_Fun HOLCF: theory HOLCF.Powerdomains HOL-Library: theory HOL-Library.Function_Division HOL-Library: theory HOL-Library.IArray HOL-Library: theory HOL-Library.Infinite_Set HOL-Library: theory HOL-Library.Omega_Words_Fun HOL-Library: theory HOL-Library.Ramsey HOL-Library: theory HOL-Library.LaTeXsugar HOLCF: theory HOLCF HOL-Library: theory HOL-Library.Lattice_Constructions HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.List_lexord HOL-Proofs: theory HOL.Lazy_Sequence HOL-Library: theory HOL-Library.Mapping HOL-Proofs: theory HOL.Limited_Sequence HOL-Library: theory HOL-Library.AList_Mapping HOL-Library: theory HOL-Library.Monad_Syntax HOL-Proofs: theory HOL.Typerep HOL-Library: theory HOL-Library.State_Monad HOL-Proofs: theory HOL.Code_Evaluation HOL-Library: theory HOL-Library.More_List HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Old_Datatype HOL-Proofs: theory HOL.Random HOL-Library: theory HOL-Library.Stream HOL-Library: theory HOL-Library.Old_Recdef HOL-Proofs: theory HOL.Quickcheck_Random 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.Cardinality HOL-Proofs: theory HOL.Quickcheck_Exhaustive HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Library: theory HOL-Library.Numeral_Type HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Preorder HOL-Library: theory HOL-Library.Product_Lexorder HOL-Library: theory HOL-Library.Product_Plus HOL-Library: theory HOL-Library.Product_Order HOL-Library: theory HOL-Library.Type_Length HOL-Library: theory HOL-Library.Finite_Lattice HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.Quotient_Syntax 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_List HOL-Library: theory HOL-Library.Quotient_Sum HOL-Library: theory HOL-Library.Quotient_Type 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-Proofs: theory HOL.Record HOL-Library: theory HOL-Library.Rewrite HOL-Library: theory HOL-Library.Set_Algebras HOL-Library: theory HOL-Library.Simps_Case_Conv HOL-Library: theory HOL-Library.Extended HOL-Proofs: theory HOL.Nitpick HOL-Library: theory HOL-Library.Stirling HOL-Library: theory HOL-Library.Sublist HOL-Library: theory HOL-Library.Prefix_Order HOL-Library: theory HOL-Library.Subseq_Order Timing HOLCF (2 threads, 15.685s elapsed time, 31.176s cpu time, 2.112s GC time, factor 1.99) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf Finished HOLCF (0:00:32 elapsed time, 0:00:56 cpu time, factor 1.74) Building IOA ... HOL-Library: theory HOL-Library.Transitive_Closure_Table IOA: theory IOA.Seq IOA: theory IOA.Asig HOL-Library: theory HOL-Library.Tree IOA: theory IOA.Automata IOA: theory IOA.Sequence IOA: theory IOA.Pred HOL-Proofs: theory HOL.Nunchaku IOA: theory IOA.Traces IOA: theory IOA.TL HOL-Proofs: theory HOL.Quickcheck_Narrowing HOL-Library: theory HOL-Library.Tree_Multiset IOA: theory IOA.CompoExecs IOA: theory IOA.RefMappings IOA: theory IOA.CompoScheds IOA: theory IOA.RefCorrectness HOL-Library: theory HOL-Library.Uprod IOA: theory IOA.Simulations IOA: theory IOA.SimCorrectness IOA: theory IOA.Deadlock HOL-Library: theory HOL-Library.While_Combinator IOA: theory IOA.ShortExecutions IOA: theory IOA.CompoTraces HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint HOL-Library: theory HOL-Library.Countable IOA: theory IOA.Compositionality IOA: theory IOA.IOA HOL-Library: theory HOL-Library.Countable_Set IOA: theory IOA.TLS HOL-Library: theory HOL-Library.Countable_Complete_Lattices IOA: theory IOA.LiveIOA IOA: theory IOA.Abstraction HOL-Proofs: theory HOL.Random_Pred HOL-Proofs: theory HOL.Random_Sequence HOL-Library: theory HOL-Library.Countable_Set_Type HOL-Proofs: theory HOL.Predicate_Compile HOL-Library: theory HOL-Library.FSet HOL-Proofs: theory Main HOL-Proofs: theory HOL-Library.Realizers HOL-Library: theory HOL-Library.Finite_Map HOL-Library: theory HOL-Library.BigO 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.Lattice_Algebras HOL-Library: theory HOL-Library.Liminf_Limsup HOL-Library: theory HOL-Library.Log_Nat HOL-Library: theory HOL-Library.Float HOL-Library: theory HOL-Library.RBT HOL-Library: theory HOL-Library.RBT_Mapping HOL-Library: theory HOL-Library.RBT_Set HOL-Library: theory HOL-Library.Lub_Glb 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.Order_Continuity HOL-Library: theory HOL-Library.Periodic_Fun HOL-Library: theory HOL-Library.Quadratic_Discriminant HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Sum_of_Squares HOL-Library: theory HOL-Library.Extended_Real Timing IOA (2 threads, 15.177s elapsed time, 28.676s cpu time, 1.276s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA Finished IOA (0:00:27 elapsed time, 0:00:44 cpu time, factor 1.65) Building HOL-TLA ... HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-TLA: theory HOL-TLA.Intensional HOL-TLA: theory HOL-TLA.Stfun HOL-TLA: theory HOL-TLA.Action HOL-TLA: theory HOL-TLA.Init HOL-TLA: theory HOL-TLA.TLA HOL-Library: theory HOL-Library.Tree_Real HOL-Library: theory HOL-Library.Extended_Nonnegative_Real HOL-Library: theory HOL-Library.Library Timing HOL-TLA (2 threads, 1.675s elapsed time, 2.772s cpu time, 0.000s GC time, factor 1.65) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA Finished HOL-TLA (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.34) Building HOL-Analysis ... HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.FuncSet HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Library.Infinite_Set HOL-Analysis: theory HOL-Library.Nat_Bijection HOL-Analysis: theory HOL-Library.Old_Datatype HOL-Analysis: theory HOL-Library.Phantom_Type HOL-Analysis: theory HOL-Library.Cardinality HOL-Analysis: theory HOL-Library.Numeral_Type HOL-Analysis: theory HOL-Library.Product_Plus HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring HOL-Analysis: theory HOL-Library.Permutations HOL-Analysis: theory HOL-Library.Set_Algebras HOL-Analysis: theory HOL-Library.Countable HOL-Analysis: theory HOL-Library.Countable_Set HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Analysis.Product_Vector HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Analysis.Linear_Algebra HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product HOL-Analysis: theory HOL-Analysis.Operator_Norm HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Library.Discrete HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Library.Liminf_Limsup HOL-Analysis: theory HOL-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Library.Nonpos_Ints HOL-Analysis: theory HOL-Library.Order_Continuity HOL-Analysis: theory HOL-Library.Extended_Nat HOL-Analysis: theory HOL-Library.Extended_Real HOL-Analysis: theory HOL-Library.Periodic_Fun HOL-Analysis: theory HOL-Library.Sum_of_Squares HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real HOL-Analysis: theory HOL-Analysis.Norm_Arith HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Sigma_Algebra HOL-Analysis: theory HOL-Analysis.Measurable HOL-Analysis: theory HOL-Analysis.Measure_Space HOL-Analysis: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Caratheodory HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Tagged_Division HOL-Analysis: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Starlike HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Continuous_Extension HOL-Analysis: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Arcwise_Connected HOL-Analysis: theory HOL-Analysis.Borel_Space HOL-Analysis: theory HOL-Analysis.Lipschitz HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure HOL-Analysis: theory HOL-Analysis.Embed_Measure HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure HOL-Analysis: theory HOL-Analysis.Bochner_Integration HOL-Analysis: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.Complete_Measure HOL-Analysis: theory HOL-Analysis.Radon_Nikodym HOL-Analysis: theory HOL-Analysis.Set_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory HOL-Analysis.Integral_Test HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics HOL-Analysis: theory HOL-Analysis.Improper_Integral HOL-Analysis: theory HOL-Analysis.Interval_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution HOL-Analysis: theory HOL-Analysis.Complex_Transcendental HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem HOL-Analysis: theory HOL-Analysis.Further_Topology HOL-Analysis: theory HOL-Analysis.Jordan_Curve HOL-Analysis: theory HOL-Analysis.Conformal_Mappings HOL-Analysis: theory HOL-Analysis.FPS_Convergence HOL-Analysis: theory HOL-Analysis.Gamma_Function HOL-Analysis: theory HOL-Analysis.Great_Picard HOL-Analysis: theory HOL-Analysis.Riemann_Mapping HOL-Analysis: theory HOL-Analysis.Ball_Volume HOL-Analysis: theory HOL-Analysis.Winding_Numbers HOL-Analysis: theory HOL-Analysis.Analysis Timing HOL-Library (2 threads, 171.943s elapsed time, 325.220s cpu time, 22.820s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf Finished HOL-Library (0:03:45 elapsed time, 0:06:47 cpu time, factor 1.81) Building HOL-Computational_Algebra ... HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra Timing HOL-Computational_Algebra (2 threads, 56.624s elapsed time, 99.524s cpu time, 5.652s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Computational_Algebra Finished HOL-Computational_Algebra (0:01:19 elapsed time, 0:02:08 cpu time, factor 1.63) Building HOL-Number_Theory ... HOL-Number_Theory: theory HOL-Algebra.Congruence HOL-Number_Theory: theory HOL-Number_Theory.Cong HOL-Number_Theory: theory HOL-Algebra.Order HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes HOL-Number_Theory: theory HOL-Number_Theory.Fib HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers HOL-Number_Theory: theory HOL-Algebra.Lattice HOL-Number_Theory: theory HOL-Number_Theory.Totient HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice HOL-Number_Theory: theory HOL-Algebra.Group HOL-Number_Theory: theory HOL-Algebra.Coset HOL-Number_Theory: theory HOL-Algebra.FiniteProduct HOL-Number_Theory: theory HOL-Algebra.Ring HOL-Number_Theory: theory HOL-Algebra.AbelCoset HOL-Number_Theory: theory HOL-Algebra.Module HOL-Number_Theory: theory HOL-Algebra.Ideal HOL-Number_Theory: theory HOL-Algebra.More_Group HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product HOL-Number_Theory: theory HOL-Algebra.More_Ring HOL-Number_Theory: theory HOL-Algebra.RingHom HOL-Number_Theory: theory HOL-Algebra.UnivPoly HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group HOL-Number_Theory: theory HOL-Number_Theory.Residues HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion HOL-Number_Theory: theory HOL-Number_Theory.Gauss HOL-Number_Theory: theory HOL-Number_Theory.Pocklington HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory Timing HOL-Number_Theory (2 threads, 91.477s elapsed time, 166.320s cpu time, 11.496s GC time, factor 1.82) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf Finished HOL-Number_Theory (0:02:15 elapsed time, 0:03:43 cpu time, factor 1.64) Building HOL-Algebra ... HOL-Algebra: theory HOL-Algebra.Congruence HOL-Algebra: theory HOL-Algebra.Exponent HOL-Algebra: theory HOL-Algebra.Order HOL-Algebra: theory HOL-Algebra.Lattice HOL-Algebra: theory HOL-Algebra.Complete_Lattice HOL-Algebra: theory HOL-Algebra.Galois_Connection HOL-Algebra: theory HOL-Algebra.Group HOL-Algebra: theory HOL-Algebra.Bij HOL-Algebra: theory HOL-Algebra.Coset HOL-Algebra: theory HOL-Algebra.Sylow HOL-Algebra: theory HOL-Algebra.Divisibility HOL-Algebra: theory HOL-Algebra.FiniteProduct HOL-Algebra: theory HOL-Algebra.Ring HOL-Algebra: theory HOL-Algebra.AbelCoset HOL-Algebra: theory HOL-Algebra.Module HOL-Algebra: theory HOL-Algebra.More_Group HOL-Algebra: theory HOL-Algebra.More_Finite_Product HOL-Algebra: theory HOL-Algebra.More_Ring HOL-Algebra: theory HOL-Algebra.Ideal HOL-Algebra: theory HOL-Algebra.RingHom HOL-Algebra: theory HOL-Algebra.QuotRing HOL-Algebra: theory HOL-Algebra.UnivPoly HOL-Algebra: theory HOL-Algebra.IntRing HOL-Algebra: theory HOL-Algebra.Multiplicative_Group Timing HOL-Algebra (2 threads, 72.600s elapsed time, 132.244s cpu time, 15.612s GC time, factor 1.82) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf Finished HOL-Algebra (0:02:01 elapsed time, 0:03:15 cpu time, factor 1.61) Building HOL-Word ... HOL-Word: theory HOL-Library.Boolean_Algebra HOL-Word: theory HOL-Library.Bit HOL-Word: theory HOL-Library.Phantom_Type HOL-Word: theory HOL-Word.Bits HOL-Word: theory HOL-Word.Bits_Bit HOL-Word: theory HOL-Word.Misc_Numeric HOL-Word: theory HOL-Library.Cardinality HOL-Word: theory HOL-Word.Bit_Representation HOL-Word: theory HOL-Word.Bits_Int HOL-Word: theory HOL-Library.Numeral_Type HOL-Word: theory HOL-Library.Type_Length HOL-Word: theory HOL-Word.Word_Miscellaneous HOL-Word: theory HOL-Word.Bit_Comparison HOL-Word: theory HOL-Word.Bool_List_Representation HOL-Word: theory HOL-Word.Misc_Typedef HOL-Word: theory HOL-Word.Word HOL-Word: theory HOL-Word.WordBitwise HOL-Word: theory HOL-Word.WordExamples Timing HOL-Word (2 threads, 20.951s elapsed time, 39.728s cpu time, 1.880s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf Finished HOL-Word (0:00:36 elapsed time, 0:01:03 cpu time, factor 1.76) Building HOLCF-Library ... HOLCF-Library: theory HOL-Library.Infinite_Set HOLCF-Library: theory HOLCF-Library.Bool_Discrete HOLCF-Library: theory HOLCF-Library.Char_Discrete HOLCF-Library: theory HOLCF-Library.Int_Discrete HOLCF-Library: theory HOL-Library.Countable_Set HOLCF-Library: theory HOLCF-Library.Defl_Bifinite HOLCF-Library: theory HOL-Library.Countable_Complete_Lattices HOLCF-Library: theory HOLCF-Library.List_Cpo HOLCF-Library: theory HOLCF-Library.Nat_Discrete HOLCF-Library: theory HOLCF-Library.Sum_Cpo HOLCF-Library: theory HOLCF-Library.List_Predomain HOLCF-Library: theory HOL-Library.Order_Continuity HOLCF-Library: theory HOLCF-Library.Option_Cpo HOLCF-Library: theory HOLCF-Library.HOL_Cpo HOLCF-Library: theory HOL-Library.Extended_Nat HOLCF-Library: theory HOLCF-Library.Stream HOLCF-Library: theory HOLCF-Library.HOLCF_Library Timing HOLCF-Library (2 threads, 12.733s elapsed time, 25.076s cpu time, 1.124s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library Finished HOLCF-Library (0:00:24 elapsed time, 0:00:39 cpu time, factor 1.65) Building HOL-SPARK ... HOL-SPARK: theory HOL-SPARK.SPARK_Setup HOL-SPARK: theory HOL-SPARK.SPARK Timing HOL-SPARK (2 threads, 2.146s elapsed time, 2.932s cpu time, 0.144s GC time, factor 1.37) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK Finished HOL-SPARK (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.26) Building HOL-Auth ... HOL-Auth: theory HOL-Auth.Message HOL-Auth: theory HOL-Auth.All_Symmetric HOL-Auth: theory HOL-Auth.Event HOL-Auth: theory HOL-Auth.EventSC HOL-Auth: theory HOL-Auth.Extensions HOL-Auth: theory HOL-Auth.Analz HOL-Auth: theory HOL-Auth.List_Msg HOL-Auth: theory HOL-Auth.Guard HOL-Auth: theory HOL-Auth.GuardK HOL-Auth: theory HOL-Auth.Public HOL-Auth: theory HOL-Auth.CertifiedEmail HOL-Auth: theory HOL-Auth.Guard_Public HOL-Auth: theory HOL-Auth.Guard_NS_Public HOL-Auth: theory HOL-Auth.P2 HOL-Auth: theory HOL-Auth.Proto HOL-Auth: theory HOL-Auth.KerberosIV HOL-Auth: theory HOL-Auth.KerberosIV_Gets HOL-Auth: theory HOL-Auth.KerberosV HOL-Auth: theory HOL-Auth.Kerberos_BAN HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets HOL-Auth: theory HOL-Auth.NS_Public HOL-Auth: theory HOL-Auth.NS_Public_Bad HOL-Auth: theory HOL-Auth.NS_Shared HOL-Auth: theory HOL-Auth.OtwayRees HOL-Auth: theory HOL-Auth.OtwayReesBella HOL-Auth: theory HOL-Auth.OtwayRees_AN HOL-Auth: theory HOL-Auth.OtwayRees_Bad HOL-Auth: theory HOL-Auth.P1 HOL-Auth: theory HOL-Auth.Recur HOL-Auth: theory HOL-Auth.WooLam HOL-Auth: theory HOL-Auth.Yahalom HOL-Auth: theory HOL-Auth.Yahalom2 HOL-Auth: theory HOL-Auth.Yahalom_Bad HOL-Auth: theory HOL-Auth.ZhouGollmann HOL-Auth: theory HOL-Auth.Auth_Shared HOL-Auth: theory HOL-Auth.Auth_Guard_Public HOL-Auth: theory HOL-Auth.Shared HOL-Auth: theory HOL-Auth.Guard_Shared HOL-Auth: theory HOL-Auth.Guard_OtwayRees HOL-Auth: theory HOL-Auth.Guard_Yahalom HOL-Auth: theory HOL-Auth.TLS HOL-Auth: theory HOL-Auth.Auth_Guard_Shared HOL-Auth: theory HOL-Auth.Smartcard HOL-Auth: theory HOL-Auth.ShoupRubin HOL-Auth: theory HOL-Auth.Auth_Public HOL-Auth: theory HOL-Auth.ShoupRubinBella HOL-Auth: theory HOL-Auth.Auth_Smartcard Timing HOL-Analysis (2 threads, 638.672s elapsed time, 1142.456s cpu time, 50.764s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/manual.pdf Finished HOL-Analysis (0:11:59 elapsed time, 0:20:50 cpu time, factor 1.74) Building HOL-Probability ... HOL-Probability: theory HOL-Library.Adhoc_Overloading HOL-Probability: theory HOL-Library.Lattice_Syntax HOL-Probability: theory HOL-Library.AList HOL-Probability: theory HOL-Library.Complete_Partial_Order2 HOL-Probability: theory HOL-Library.Mapping HOL-Probability: theory HOL-Library.AList_Mapping HOL-Probability: theory HOL-Library.Monad_Syntax HOL-Probability: theory HOL-Library.Stream HOL-Probability: theory HOL-Library.Rewrite HOL-Probability: theory HOL-Library.Sublist HOL-Probability: theory HOL-Library.Tree HOL-Probability: theory HOL-Library.FSet HOL-Probability: theory HOL-Library.Diagonal_Subsequence HOL-Probability: theory HOL-Library.Multiset_Permutations HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Probability: theory HOL-Library.Finite_Map HOL-Probability: theory HOL-Probability.Discrete_Topology HOL-Probability: theory HOL-Probability.Essential_Supremum HOL-Probability: theory HOL-Probability.Probability_Measure HOL-Probability: theory HOL-Probability.Fin_Map HOL-Probability: theory HOL-Probability.Conditional_Expectation HOL-Probability: theory HOL-Probability.Distribution_Functions HOL-Probability: theory HOL-Probability.Weak_Convergence HOL-Probability: theory HOL-Probability.Giry_Monad HOL-Probability: theory HOL-Probability.Helly_Selection HOL-Probability: theory HOL-Probability.Stopping_Time HOL-Probability: theory HOL-Probability.Tree_Space HOL-Probability: theory HOL-Probability.Probability_Mass_Function HOL-Probability: theory HOL-Probability.Projective_Family HOL-Probability: theory HOL-Probability.Infinite_Product_Measure HOL-Probability: theory HOL-Probability.PMF_Impl HOL-Probability: theory HOL-Probability.Random_Permutations HOL-Probability: theory HOL-Probability.SPMF HOL-Probability: theory HOL-Probability.Independent_Family HOL-Probability: theory HOL-Probability.Convolution HOL-Probability: theory HOL-Probability.Information HOL-Probability: theory HOL-Probability.Projective_Limit HOL-Probability: theory HOL-Probability.Distributions HOL-Probability: theory HOL-Probability.Stream_Space HOL-Probability: theory HOL-Probability.Characteristic_Functions HOL-Probability: theory HOL-Probability.Sinc_Integral HOL-Probability: theory HOL-Probability.Levy HOL-Probability: theory HOL-Probability.Central_Limit_Theorem HOL-Probability: theory HOL-Probability.Probability Timing HOL-Auth (2 threads, 157.904s elapsed time, 256.760s cpu time, 12.136s GC time, factor 1.63) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf Finished HOL-Auth (0:03:05 elapsed time, 0:04:59 cpu time, factor 1.61) Building HOL-Nonstandard_Analysis ... HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis Timing HOL-Nonstandard_Analysis (2 threads, 9.868s elapsed time, 18.768s cpu time, 1.156s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf Finished HOL-Nonstandard_Analysis (0:00:29 elapsed time, 0:00:48 cpu time, factor 1.64) Building HOL-Nominal ... HOL-Nominal: theory HOL-Nominal.Nominal Timing HOL-Nominal (2 threads, 6.378s elapsed time, 11.440s cpu time, 0.624s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal Finished HOL-Nominal (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.48) Building HOL-Eisbach ... HOL-Eisbach: theory HOL-Eisbach.Eisbach HOL-Eisbach: theory IFOL HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools HOL-Eisbach: theory HOL-Eisbach.Examples HOL-Eisbach: theory HOL-Eisbach.Tests HOL-Eisbach: theory FOL HOL-Eisbach: theory HOL-Eisbach.Examples_FOL Timing HOL-Eisbach (2 threads, 3.357s elapsed time, 6.700s cpu time, 0.236s GC time, factor 2.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach Finished HOL-Eisbach (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.51) Building Codegen_Basics ... Codegen_Basics: theory Codegen_Basics.Setup Timing Codegen_Basics (2 threads, 1.171s elapsed time, 1.280s cpu time, 0.000s GC time, factor 1.09) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics Finished Codegen_Basics (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.28) Building Typeclass_Hierarchy_Basics ... Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup Timing Typeclass_Hierarchy_Basics (2 threads, 0.778s elapsed time, 0.896s cpu time, 0.000s GC time, factor 1.15) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics Finished Typeclass_Hierarchy_Basics (0:00:13 elapsed time, 0:00:16 cpu time, factor 1.29) Building HOL-Mirabelle ... HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test Timing HOL-Mirabelle (2 threads, 0.471s elapsed time, 0.572s cpu time, 0.000s GC time, factor 1.22) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle Finished HOL-Mirabelle (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.25) Running HOL-Decision_Procs ... HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack Timing HOL-Probability (2 threads, 141.873s elapsed time, 260.772s cpu time, 18.032s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf Finished HOL-Probability (0:02:57 elapsed time, 0:05:12 cpu time, factor 1.77) Running HOL-Nominal-Examples ... HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts HOL-Decision_Procs: theory HOL-Decision_Procs.MIR HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial HOL-Nominal-Examples: theory HOL-Nominal-Examples.W HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs Timing HOL-Decision_Procs (2 threads, 519.916s elapsed time, 992.136s cpu time, 99.464s GC time, factor 1.91) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs Finished HOL-Decision_Procs (0:08:42 elapsed time, 0:16:34 cpu time, factor 1.90) Running HOL-Data_Structures ... HOL-Data_Structures: theory HOL-Data_Structures.Less_False HOL-Data_Structures: theory HOL-Data_Structures.Cmp HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del HOL-Data_Structures: theory HOL-Data_Structures.Map_by_Ordered HOL-Data_Structures: theory HOL-Data_Structures.Tree2 HOL-Data_Structures: theory HOL-Data_Structures.Set_by_Ordered HOL-Data_Structures: theory HOL-Data_Structures.Tree23 HOL-Data_Structures: theory HOL-Data_Structures.Isin2 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set HOL-Data_Structures: theory HOL-Data_Structures.Lookup2 HOL-Data_Structures: theory HOL-Data_Structures.RBT HOL-Data_Structures: theory HOL-Data_Structures.AA_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree234 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map HOL-Data_Structures: theory HOL-Library.Cancellation HOL-Data_Structures: theory HOL-Library.Multiset HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue HOL-Data_Structures: theory HOL-Library.Pattern_Aliases HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS HOL-Data_Structures: theory HOL-Library.Tree HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map HOL-Data_Structures: theory HOL-Data_Structures.Sorting HOL-Data_Structures: theory HOL-Library.Tree_Real HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map HOL-Data_Structures: theory HOL-Data_Structures.Balance HOL-Data_Structures: theory HOL-Number_Theory.Fib HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition Timing HOL-Nominal-Examples (2 threads, 553.117s elapsed time, 1019.276s cpu time, 130.384s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples Finished HOL-Nominal-Examples (0:09:15 elapsed time, 0:17:01 cpu time, factor 1.84) Running HOL-Codegenerator_Test ... HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_by_Ordered HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala HOL-Codegenerator_Test: theory HOL-ex.Records HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_by_Ordered HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Pretty_Char HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ Timing HOL-Codegenerator_Test (2 threads, 386.026s elapsed time, 340.660s cpu time, 18.104s GC time, factor 0.88) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Codegenerator_Test Finished HOL-Codegenerator_Test (0:06:28 elapsed time, 0:16:02 cpu time, factor 2.48) Running HOL-ex ... HOL-ex: theory HOL-ex.Computations HOL-ex: theory HOL-ex.Bubblesort HOL-ex: theory HOL-ex.MergeSort HOL-ex: theory HOL-ex.Quicksort HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples HOL-ex: theory HOL-ex.Datatype_Record_Examples HOL-ex: theory HOL-ex.IArray_Examples HOL-ex: theory HOL-ex.Perm_Fragments HOL-ex: theory HOL-ex.Refute_Examples HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples HOL-ex: theory HOL-ex.Radix_Sort HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex HOL-ex: theory HOL-ex.While_Combinator_Example HOL-ex: theory HOL-ex.Code_Timing HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples HOL-ex: theory HOL-ex.Antiquote HOL-ex: theory HOL-ex.Arith_Examples HOL-ex: theory HOL-ex.Birthday_Paradox HOL-ex: theory HOL-ex.CTL HOL-ex: theory HOL-ex.Cartouche_Examples HOL-ex: theory HOL-ex.Case_Product HOL-ex: theory HOL-ex.Chinese HOL-ex: theory HOL-ex.Classical HOL-ex: theory HOL-ex.Coercion_Examples HOL-ex: theory HOL-ex.Coherent HOL-ex: theory HOL-ex.Commands HOL-ex: theory HOL-ex.Erdoes_Szekeres HOL-ex: theory HOL-ex.Executable_Relation HOL-ex: theory HOL-ex.Execute_Choice HOL-ex: theory HOL-ex.Functions HOL-ex: theory HOL-ex.Groebner_Examples HOL-ex: theory HOL-ex.Guess HOL-ex: theory HOL-ex.Hebrew HOL-ex: theory HOL-ex.Hex_Bin_Examples HOL-ex: theory HOL-ex.Iff_Oracle HOL-ex: theory HOL-ex.Induction_Schema HOL-ex: theory HOL-ex.Intuitionistic HOL-ex: theory HOL-ex.Lagrange HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples HOL-ex: theory HOL-ex.LocaleTest2 HOL-ex: theory HOL-ex.ML Timing HOL-Data_Structures (2 threads, 480.615s elapsed time, 738.840s cpu time, 28.504s GC time, factor 1.54) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf Finished HOL-Data_Structures (0:08:06 elapsed time, 0:12:24 cpu time, factor 1.53) Running HOL-Nitpick_Examples ... HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Core_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Datatype_Nits HOL-ex: theory HOL-ex.MonoidGroup HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Hotel_Nits HOL-ex: theory HOL-ex.Multiquote HOL-ex: theory HOL-ex.NatSum HOL-ex: theory HOL-ex.PER HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Induct_Nits HOL-ex: theory HOL-ex.Peano_Axioms HOL-ex: theory HOL-ex.PresburgerEx HOL-ex: theory HOL-ex.Primrec HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Integer_Nits HOL-ex: theory HOL-ex.Records HOL-ex: theory HOL-ex.Rewrite_Examples HOL-ex: theory HOL-ex.Seq HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mini_Nits HOL-ex: theory HOL-ex.Serbian HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mono_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Pattern_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Record_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Refute_Nits HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples HOL-ex: theory HOL-ex.Set_Theory HOL-ex: theory HOL-ex.Simproc_Tests HOL-ex: theory HOL-ex.Sudoku HOL-ex: theory HOL-ex.Tarski HOL-ex: theory HOL-ex.Termination HOL-ex: theory HOL-ex.ThreeDivides HOL-ex: theory HOL-ex.Transfer_Int_Nat HOL-ex: theory HOL-ex.Tree23 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Special_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Tests_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Manual_Nits HOL-ex: theory HOL-ex.Unification HOL-ex: theory HOL-ex.Word_Type HOL-ex: theory HOL-ex.veriT_Preprocessing HOL-ex: theory HOL-ex.Transfer_Debug HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Typedef_Nits HOL-ex: theory HOL-ex.Function_Growth HOL-ex: theory HOL-ex.SOS HOL-ex: theory HOL-ex.SOS_Cert HOL-ex: theory HOL-ex.Argo_Examples HOL-ex: theory HOL-ex.Ballot HOL-ex: theory HOL-ex.BinEx HOL-ex: theory HOL-ex.Code_Binary_Nat_examples HOL-ex: theory HOL-ex.Cubic_Quartic HOL-ex: theory HOL-ex.Dedekind_Real HOL-ex: theory HOL-ex.Eval_Examples HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Nitpick_Examples HOL-ex: theory HOL-ex.Gauge_Integration HOL-ex: theory HOL-ex.HarmonicSeries HOL-ex: theory HOL-ex.Normalization_by_Evaluation HOL-ex: theory HOL-ex.Parallel_Example HOL-ex: theory HOL-ex.Pythagoras HOL-ex: theory HOL-ex.Reflection_Examples HOL-ex: theory HOL-ex.Sqrt HOL-ex: theory HOL-ex.Sqrt_Script HOL-ex: theory HOL-ex.Sum_of_Powers Timing HOL-Nitpick_Examples (2 threads, 212.835s elapsed time, 125.100s cpu time, 2.736s GC time, factor 0.59) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples Finished HOL-Nitpick_Examples (0:03:34 elapsed time, 0:10:03 cpu time, factor 2.81) Running HOL-Corec_Examples ... HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly HOL-ex: theory HOL-ex.Meson_Test HOL-ex: theory HOL-ex.SAT_Examples HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete Timing HOL-ex (2 threads, 395.834s elapsed time, 730.052s cpu time, 53.168s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex Finished HOL-ex (0:06:39 elapsed time, 0:12:35 cpu time, factor 1.89) Running HOL-Hoare_Parallel ... HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class Timing HOL-Corec_Examples (2 threads, 234.038s elapsed time, 449.068s cpu time, 52.876s GC time, factor 1.92) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples Finished HOL-Corec_Examples (0:03:56 elapsed time, 0:07:30 cpu time, factor 1.91) Running HOL-MicroJava ... HOL-MicroJava: theory HOL-Eisbach.Eisbach HOL-MicroJava: theory HOL-MicroJava.Semilat HOL-MicroJava: theory HOL-MicroJava.Err HOL-MicroJava: theory HOL-MicroJava.JBasis HOL-MicroJava: theory HOL-MicroJava.AuxLemmas HOL-MicroJava: theory HOL-MicroJava.Type HOL-MicroJava: theory HOL-MicroJava.Listn HOL-MicroJava: theory HOL-MicroJava.Typing_Framework HOL-MicroJava: theory HOL-MicroJava.Opt HOL-MicroJava: theory HOL-MicroJava.Product HOL-MicroJava: theory HOL-MicroJava.SemilatAlg HOL-MicroJava: theory HOL-MicroJava.Kildall HOL-MicroJava: theory HOL-MicroJava.LBVSpec HOL-MicroJava: theory HOL-MicroJava.Decl HOL-MicroJava: theory HOL-MicroJava.SystemClasses HOL-MicroJava: theory HOL-MicroJava.TypeRel HOL-MicroJava: theory HOL-MicroJava.Value HOL-MicroJava: theory HOL-MicroJava.WellForm HOL-MicroJava: theory HOL-MicroJava.State HOL-MicroJava: theory HOL-MicroJava.Term HOL-MicroJava: theory HOL-MicroJava.Exceptions HOL-MicroJava: theory HOL-MicroJava.LBVComplete HOL-MicroJava: theory HOL-MicroJava.LBVCorrect HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err HOL-MicroJava: theory HOL-MicroJava.Abstract_BV HOL-MicroJava: theory HOL-MicroJava.Semilattices HOL-MicroJava: theory HOL-MicroJava.JType HOL-MicroJava: theory HOL-MicroJava.JVMType HOL-MicroJava: theory HOL-MicroJava.WellType HOL-MicroJava: theory HOL-MicroJava.Conform HOL-MicroJava: theory HOL-MicroJava.JVMState HOL-MicroJava: theory HOL-MicroJava.JVMInstructions HOL-MicroJava: theory HOL-MicroJava.Eval HOL-MicroJava: theory HOL-MicroJava.JVMExceptions HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr HOL-MicroJava: theory HOL-MicroJava.JVMExec HOL-MicroJava: theory HOL-MicroJava.DefsComp HOL-MicroJava: theory HOL-MicroJava.Index HOL-MicroJava: theory HOL-MicroJava.JVMDefensive HOL-MicroJava: theory HOL-MicroJava.JVMListExample HOL-MicroJava: theory HOL-MicroJava.TypeInf HOL-MicroJava: theory HOL-MicroJava.Effect HOL-MicroJava: theory HOL-MicroJava.Example HOL-MicroJava: theory HOL-MicroJava.JListExample HOL-MicroJava: theory HOL-MicroJava.JTypeSafe HOL-MicroJava: theory HOL-MicroJava.TranslCompTp HOL-MicroJava: theory HOL-MicroJava.TranslComp HOL-MicroJava: theory HOL-MicroJava.LemmasComp HOL-MicroJava: theory HOL-MicroJava.CorrComp HOL-MicroJava: theory HOL-MicroJava.BVSpec HOL-MicroJava: theory HOL-MicroJava.Altern HOL-MicroJava: theory HOL-MicroJava.Correct HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe HOL-MicroJava: theory HOL-MicroJava.EffectMono HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError HOL-MicroJava: theory HOL-MicroJava.JVM HOL-MicroJava: theory HOL-MicroJava.LBVJVM HOL-MicroJava: theory HOL-MicroJava.BVExample HOL-MicroJava: theory HOL-MicroJava.CorrCompTp HOL-MicroJava: theory HOL-MicroJava.MicroJava Timing HOL-Hoare_Parallel (2 threads, 148.739s elapsed time, 271.464s cpu time, 7.932s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf Finished HOL-Hoare_Parallel (0:02:34 elapsed time, 0:04:41 cpu time, factor 1.82) Running HOL-Datatype_Examples ... HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype Timing HOL-MicroJava (2 threads, 145.780s elapsed time, 251.584s cpu time, 12.180s GC time, factor 1.73) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf Finished HOL-MicroJava (0:02:32 elapsed time, 0:04:23 cpu time, factor 1.72) Running HOL-IMP ... HOL-IMP: theory HOL-IMP.AExp HOL-IMP: theory HOL-IMP.C_like HOL-IMP: theory HOL-IMP.ASM HOL-IMP: theory HOL-IMP.BExp HOL-IMP: theory HOL-IMP.Complete_Lattice HOL-IMP: theory HOL-IMP.Com HOL-IMP: theory HOL-IMP.Procs HOL-IMP: theory HOL-IMP.ACom HOL-IMP: theory HOL-IMP.Abs_Int_Tests HOL-IMP: theory HOL-IMP.Big_Step HOL-IMP: theory HOL-IMP.Denotational HOL-IMP: theory HOL-IMP.Hoare HOL-IMP: theory HOL-IMP.Hoare_Examples HOL-IMP: theory HOL-IMP.Hoare_Total HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete HOL-IMP: theory HOL-IMP.Hoare_Total_EX HOL-IMP: theory HOL-IMP.VCG_Total_EX HOL-IMP: theory HOL-IMP.Hoare_Total_EX2 HOL-IMP: theory HOL-IMP.VCG_Total_EX2 HOL-IMP: theory HOL-IMP.VCG HOL-IMP: theory HOL-IMP.Sec_Type_Expr HOL-IMP: theory HOL-IMP.Sem_Equiv HOL-IMP: theory HOL-IMP.Vars HOL-IMP: theory HOL-IMP.Sec_Typing HOL-IMP: theory HOL-IMP.Sec_TypingT HOL-IMP: theory HOL-IMP.Def_Init HOL-IMP: theory HOL-IMP.Def_Init_Exp HOL-IMP: theory HOL-IMP.Fold HOL-IMP: theory HOL-IMP.Def_Init_Big HOL-IMP: theory HOL-IMP.Live HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec HOL-IMP: theory HOL-IMP.Collecting HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang HOL-IMP: theory HOL-IMP.Collecting1 HOL-IMP: theory HOL-IMP.Collecting_Examples HOL-IMP: theory HOL-IMP.OO HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI HOL-IMP: theory HOL-IMP.Star HOL-IMP: theory HOL-IMP.Compiler HOL-IMP: theory HOL-IMP.Compiler2 HOL-IMP: theory HOL-IMP.Def_Init_Small HOL-IMP: theory HOL-IMP.Small_Step HOL-IMP: theory HOL-IMP.Finite_Reachable HOL-IMP: theory HOL-IMP.Abs_Int_init HOL-IMP: theory HOL-IMP.Live_True HOL-IMP: theory HOL-IMP.Abs_Int0 HOL-IMP: theory HOL-IMP.Types HOL-IMP: theory HOL-IMP.Abs_State HOL-IMP: theory HOL-IMP.Abs_Int1 HOL-IMP: theory HOL-IMP.Abs_Int1_const HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec HOL-IMP: theory HOL-IMP.Abs_Int1_parity HOL-IMP: theory HOL-IMP.Abs_Int2 HOL-IMP: theory HOL-IMP.Poly_Types HOL-IMP: theory HOL-IMP.Abs_Int2_ivl HOL-IMP: theory HOL-IMP.Abs_Int3 Timing HOL-Datatype_Examples (2 threads, 145.408s elapsed time, 287.712s cpu time, 38.232s GC time, factor 1.98) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples Finished HOL-Datatype_Examples (0:02:27 elapsed time, 0:04:49 cpu time, factor 1.96) Running HOL-Quickcheck_Examples ... HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples Timing HOL-IMP (2 threads, 140.351s elapsed time, 249.048s cpu time, 15.544s GC time, factor 1.77) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf Finished HOL-IMP (0:02:26 elapsed time, 0:04:17 cpu time, factor 1.75) Running HOL-Bali ... HOL-Bali: theory HOL-Bali.Basis HOL-Bali: theory HOL-Bali.Name HOL-Bali: theory HOL-Bali.Table HOL-Bali: theory HOL-Bali.Type HOL-Bali: theory HOL-Bali.Value HOL-Bali: theory HOL-Bali.Term HOL-Bali: theory HOL-Bali.Decl HOL-Bali: theory HOL-Bali.TypeRel HOL-Bali: theory HOL-Bali.DeclConcepts HOL-Bali: theory HOL-Bali.State HOL-Bali: theory HOL-Bali.WellType HOL-Bali: theory HOL-Bali.Conform HOL-Bali: theory HOL-Bali.Eval HOL-Bali: theory HOL-Bali.DefiniteAssignment HOL-Bali: theory HOL-Bali.WellForm HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect HOL-Bali: theory HOL-Bali.Example HOL-Bali: theory HOL-Bali.TypeSafe HOL-Bali: theory HOL-Bali.Evaln HOL-Bali: theory HOL-Bali.AxSem HOL-Bali: theory HOL-Bali.Trans HOL-Bali: theory HOL-Bali.AxCompl HOL-Bali: theory HOL-Bali.AxSound HOL-Bali: theory HOL-Bali.AxExample Timing HOL-Quickcheck_Examples (2 threads, 117.389s elapsed time, 134.572s cpu time, 5.944s GC time, factor 1.15) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples Finished HOL-Quickcheck_Examples (0:01:59 elapsed time, 0:03:39 cpu time, factor 1.84) Running HOL-Predicate_Compile_Examples ... HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples Timing HOL-Bali (2 threads, 111.422s elapsed time, 183.220s cpu time, 11.028s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf Finished HOL-Bali (0:02:04 elapsed time, 0:03:23 cpu time, factor 1.63) Running HOL-Imperative_HOL ... HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example Timing HOL-Predicate_Compile_Examples (2 threads, 107.148s elapsed time, 177.272s cpu time, 11.544s GC time, factor 1.65) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples Finished HOL-Predicate_Compile_Examples (0:01:49 elapsed time, 0:04:47 cpu time, factor 2.62) Running HOL-Word-SMT_Examples ... HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex Timing HOL-Imperative_HOL (2 threads, 65.277s elapsed time, 62.632s cpu time, 2.428s GC time, factor 0.96) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf Finished HOL-Imperative_HOL (0:01:09 elapsed time, 0:03:30 cpu time, factor 3.02) Running HOL-UNITY ... HOL-UNITY: theory HOL-UNITY.ListOrder HOL-UNITY: theory HOL-UNITY.UNITY HOL-UNITY: theory HOL-UNITY.Constrains HOL-UNITY: theory HOL-UNITY.Deadlock HOL-UNITY: theory HOL-UNITY.FP HOL-UNITY: theory HOL-UNITY.Network HOL-UNITY: theory HOL-UNITY.WFair HOL-UNITY: theory HOL-UNITY.SubstAx HOL-UNITY: theory HOL-UNITY.Token HOL-UNITY: theory HOL-UNITY.Detects HOL-UNITY: theory HOL-UNITY.Follows HOL-UNITY: theory HOL-UNITY.Union HOL-UNITY: theory HOL-UNITY.Comp HOL-UNITY: theory HOL-UNITY.Guar HOL-UNITY: theory HOL-UNITY.Transformers HOL-UNITY: theory HOL-UNITY.Extend HOL-UNITY: theory HOL-UNITY.ProgressSets HOL-UNITY: theory HOL-UNITY.Project HOL-UNITY: theory HOL-UNITY.Rename HOL-UNITY: theory HOL-UNITY.ELT HOL-UNITY: theory HOL-UNITY.Lift_prog HOL-UNITY: theory HOL-UNITY.PPROD HOL-UNITY: theory HOL-UNITY.UNITY_Main HOL-UNITY: theory HOL-UNITY.AllocBase HOL-UNITY: theory HOL-UNITY.Channel HOL-UNITY: theory HOL-UNITY.Common HOL-UNITY: theory HOL-UNITY.Counter HOL-UNITY: theory HOL-UNITY.Alloc HOL-UNITY: theory HOL-UNITY.AllocImpl HOL-UNITY: theory HOL-UNITY.Client HOL-UNITY: theory HOL-UNITY.Counterc HOL-UNITY: theory HOL-UNITY.Handshake HOL-UNITY: theory HOL-UNITY.Lift HOL-UNITY: theory HOL-UNITY.Mutex HOL-UNITY: theory HOL-UNITY.NSP_Bad HOL-UNITY: theory HOL-UNITY.PriorityAux HOL-UNITY: theory HOL-UNITY.Priority HOL-UNITY: theory HOL-UNITY.Progress HOL-UNITY: theory HOL-UNITY.Reach HOL-UNITY: theory HOL-UNITY.TimerArray HOL-UNITY: theory HOL-UNITY.Reachability Timing HOL-Word-SMT_Examples (2 threads, 57.735s elapsed time, 79.912s cpu time, 0.932s GC time, factor 1.38) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples Finished HOL-Word-SMT_Examples (0:00:59 elapsed time, 0:01:23 cpu time, factor 1.40) Running HOL-SET_Protocol ... HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol Timing HOL-UNITY (2 threads, 57.884s elapsed time, 88.904s cpu time, 6.992s GC time, factor 1.54) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf Finished HOL-UNITY (0:01:03 elapsed time, 0:01:39 cpu time, factor 1.55) Running Corec ... Corec: theory Datatypes.Setup Corec: theory Corec.Corec Timing HOL-SET_Protocol (2 threads, 48.140s elapsed time, 81.040s cpu time, 2.624s GC time, factor 1.68) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf Finished HOL-SET_Protocol (0:00:52 elapsed time, 0:01:29 cpu time, factor 1.68) Running Datatypes ... Datatypes: theory Datatypes.Setup Datatypes: theory Datatypes.Datatypes Timing Corec (2 threads, 45.975s elapsed time, 70.032s cpu time, 4.828s GC time, factor 1.52) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf Finished Corec (0:00:51 elapsed time, 0:01:15 cpu time, factor 1.48) Running HOL-Probability-ex ... HOL-Probability-ex: theory HOL-Library.Permutation HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC Timing Datatypes (2 threads, 37.523s elapsed time, 56.564s cpu time, 4.688s GC time, factor 1.51) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf Finished Datatypes (0:00:43 elapsed time, 0:01:02 cpu time, factor 1.46) Running HOL-Metis_Examples ... HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree HOL-Metis_Examples: theory HOL-Metis_Examples.Message HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O HOL-Metis_Examples: theory HOL-Metis_Examples.Sets HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification Timing HOL-Probability-ex (2 threads, 37.233s elapsed time, 45.320s cpu time, 1.568s GC time, factor 1.22) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex Finished HOL-Probability-ex (0:00:39 elapsed time, 0:00:46 cpu time, factor 1.19) Running HOL-Analysis-ex ... HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations Timing HOL-Metis_Examples (2 threads, 35.821s elapsed time, 52.880s cpu time, 3.056s GC time, factor 1.48) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples Finished HOL-Metis_Examples (0:00:37 elapsed time, 0:01:10 cpu time, factor 1.86) Running HOL-Quotient_Examples ... HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat Timing HOL-Analysis-ex (2 threads, 30.181s elapsed time, 40.716s cpu time, 0.584s GC time, factor 1.35) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex Finished HOL-Analysis-ex (0:00:32 elapsed time, 0:00:42 cpu time, factor 1.31) Running Tutorial ... Tutorial: theory Tutorial.ToyList_Test Tutorial: theory Tutorial.ABexpr Tutorial: theory Tutorial.AB Tutorial: theory Tutorial.AdvancedInd Tutorial: theory Tutorial.Base Tutorial: theory Tutorial.CTL Tutorial: theory Tutorial.CTLind Tutorial: theory Tutorial.PDL Tutorial: theory Tutorial.CodeGen Tutorial: theory Tutorial.Nested Tutorial: theory Tutorial.Even Tutorial: theory Tutorial.Fundata Tutorial: theory Tutorial.Advanced Timing HOL-Quotient_Examples (2 threads, 27.990s elapsed time, 35.212s cpu time, 3.020s GC time, factor 1.26) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples Finished HOL-Quotient_Examples (0:00:30 elapsed time, 0:01:04 cpu time, factor 2.10) Running HOL-Hoare ... Tutorial: theory Tutorial.Ifexpr HOL-Hoare: theory HOL-Hoare.Heap HOL-Hoare: theory HOL-Hoare.Arith2 HOL-Hoare: theory HOL-Hoare.Hoare_Logic Tutorial: theory Tutorial.Itrev HOL-Hoare: theory HOL-Hoare.Hoare_Logic_Abort Tutorial: theory Tutorial.Mutual Tutorial: theory Tutorial.Option2 Tutorial: theory Tutorial.Plus Tutorial: theory Tutorial.Star Tutorial: theory Tutorial.ToyList Tutorial: theory Tutorial.Tree HOL-Hoare: theory HOL-Hoare.Examples Tutorial: theory Tutorial.Trie Tutorial: theory Tutorial.Tree2 HOL-Hoare: theory HOL-Hoare.HeapSyntax Tutorial: theory Tutorial.appendix Tutorial: theory Tutorial.case_exprs Tutorial: theory Tutorial.fakenat HOL-Hoare: theory HOL-Hoare.Pointer_Examples HOL-Hoare: theory HOL-Hoare.SchorrWaite Tutorial: theory Tutorial.fun0 HOL-Hoare: theory HOL-Hoare.Pointers0 Tutorial: theory Tutorial.natsum Tutorial: theory Tutorial.pairs2 Tutorial: theory Tutorial.prime_def Tutorial: theory Tutorial.simp Tutorial: theory Tutorial.simp2 Tutorial: theory Tutorial.types Tutorial: theory Tutorial.unfoldnested HOL-Hoare: theory HOL-Hoare.ExamplesAbort HOL-Hoare: theory HOL-Hoare.HeapSyntaxAbort HOL-Hoare: theory HOL-Hoare.SepLogHeap HOL-Hoare: theory HOL-Hoare.Pointer_ExamplesAbort HOL-Hoare: theory HOL-Hoare.Separation HOL-Hoare: theory HOL-Hoare.Hoare Tutorial: theory Tutorial.Message Tutorial: theory Tutorial.Documents Tutorial: theory Tutorial.Event Tutorial: theory Tutorial.Public Tutorial: theory Tutorial.NS_Public Tutorial: theory Tutorial.Setup Tutorial: theory Tutorial.Numbers Tutorial: theory Tutorial.Basic Tutorial: theory Tutorial.Blast Tutorial: theory Tutorial.Force Tutorial: theory Tutorial.Pairs Tutorial: theory Tutorial.Records Tutorial: theory Tutorial.Overloading Tutorial: theory Tutorial.Axioms Tutorial: theory Tutorial.Typedefs Tutorial: theory Tutorial.Functions Tutorial: theory Tutorial.Examples Tutorial: theory Tutorial.Recur Tutorial: theory Tutorial.Relations Tutorial: theory Tutorial.TPrimes Tutorial: theory Tutorial.Tacticals Tutorial: theory Tutorial.find2 Tutorial: theory Tutorial.Forward Timing HOL-Hoare (2 threads, 22.343s elapsed time, 40.296s cpu time, 1.560s GC time, factor 1.80) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf Finished HOL-Hoare (0:00:26 elapsed time, 0:00:47 cpu time, factor 1.79) Running HOL-Cardinals ... HOL-Cardinals: theory HOL-Cardinals.Fun_More HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More HOL-Cardinals: theory HOL-Cardinals.Order_Union HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions Timing Tutorial (2 threads, 28.967s elapsed time, 54.924s cpu time, 6.828s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf Finished Tutorial (0:00:35 elapsed time, 0:01:01 cpu time, factor 1.73) Running HOL-Induct ... HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation HOL-Induct: theory HOL-Induct.Common_Patterns HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic HOL-Cardinals: theory HOL-Cardinals.Cardinals HOL-Cardinals: theory HOL-Cardinals.Bounded_Set HOL-Induct: theory HOL-Induct.ABexp HOL-Induct: theory HOL-Induct.Com HOL-Induct: theory HOL-Induct.Comb HOL-Induct: theory HOL-Induct.Infinitely_Branching_Tree HOL-Induct: theory HOL-Induct.Nested_Datatype HOL-Induct: theory HOL-Induct.Ordinals HOL-Induct: theory HOL-Induct.PropLog HOL-Induct: theory HOL-Induct.QuoDataType HOL-Induct: theory HOL-Induct.QuoNestedDataType HOL-Induct: theory HOL-Induct.Sigma_Algebra HOL-Induct: theory HOL-Induct.Term HOL-Induct: theory HOL-Induct.Sexp HOL-Induct: theory HOL-Induct.SList Timing HOL-Induct (2 threads, 16.707s elapsed time, 32.072s cpu time, 5.616s GC time, factor 1.92) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf Finished HOL-Induct (0:00:21 elapsed time, 0:00:39 cpu time, factor 1.85) Running HOL-SPARK-Examples ... HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification HOL-SPARK-Examples: theory HOL-SPARK-Examples.F Timing HOL-Cardinals (2 threads, 19.206s elapsed time, 35.976s cpu time, 1.776s GC time, factor 1.87) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals/outline.pdf Finished HOL-Cardinals (0:00:25 elapsed time, 0:00:45 cpu time, factor 1.79) Running HOL-Statespace ... HOL-Statespace: theory HOL-Statespace.DistinctTreeProver HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash HOL-Statespace: theory HOL-Statespace.StateFun HOL-Statespace: theory HOL-Statespace.StateSpaceLocale HOL-Statespace: theory HOL-Statespace.StateSpaceSyntax HOL-Statespace: theory HOL-Statespace.StateSpaceEx HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt Timing HOL-SPARK-Examples (2 threads, 15.927s elapsed time, 26.048s cpu time, 0.916s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples Finished HOL-SPARK-Examples (0:00:17 elapsed time, 0:00:27 cpu time, factor 1.55) Running HOL-Matrix_LP ... HOL-Matrix_LP: theory HOL-Matrix_LP.Compute_Oracle HOL-Matrix_LP: theory HOL-Matrix_LP.LP HOL-Matrix_LP: theory HOL-Matrix_LP.Matrix HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeFloat HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeHOL HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeNumeral HOL-Matrix_LP: theory HOL-Matrix_LP.SparseMatrix Timing HOL-Statespace (2 threads, 15.050s elapsed time, 17.532s cpu time, 0.788s GC time, factor 1.16) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf Finished HOL-Statespace (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.28) Running HOL-TLA-Memory ... HOL-TLA-Memory: theory HOL-TLA-Memory.RPCMemoryParams HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryParameters HOL-TLA-Memory: theory HOL-TLA-Memory.ProcedureInterface HOL-TLA-Memory: theory HOL-TLA-Memory.RPCParameters HOL-TLA-Memory: theory HOL-TLA-Memory.Memory HOL-Matrix_LP: theory HOL-Matrix_LP.Cplex HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerkParameters HOL-TLA-Memory: theory HOL-TLA-Memory.RPC HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerk HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryImplementation Timing HOL-Matrix_LP (2 threads, 12.309s elapsed time, 23.724s cpu time, 1.124s GC time, factor 1.93) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf Finished HOL-Matrix_LP (0:00:17 elapsed time, 0:00:32 cpu time, factor 1.84) Timing HOL-TLA-Memory (2 threads, 11.808s elapsed time, 21.168s cpu time, 0.768s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory Finished HOL-TLA-Memory (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.66) Running HOLCF-Tutorial ... Running Isar_Ref ... HOLCF-Tutorial: theory HOLCF-Tutorial.Domain_ex HOLCF-Tutorial: theory HOLCF-Tutorial.Fixrec_ex Isar_Ref: theory Isar_Ref.Base Isar_Ref: theory Isar_Ref.Document_Preparation Isar_Ref: theory Isar_Ref.First_Order_Logic Isar_Ref: theory Isar_Ref.Framework Isar_Ref: theory Isar_Ref.Generic Isar_Ref: theory Isar_Ref.HOL_Specific Isar_Ref: theory Isar_Ref.Inner_Syntax Isar_Ref: theory Isar_Ref.Outer_Syntax Isar_Ref: theory Isar_Ref.Preface Isar_Ref: theory Isar_Ref.Proof HOLCF-Tutorial: theory HOLCF-Tutorial.New_Domain Isar_Ref: theory Isar_Ref.Proof_Script Isar_Ref: theory Isar_Ref.Quick_Reference Isar_Ref: theory Isar_Ref.Spec Isar_Ref: theory Isar_Ref.Symbols Isar_Ref: theory Isar_Ref.Synopsis Timing HOLCF-Tutorial (2 threads, 11.199s elapsed time, 14.884s cpu time, 0.572s GC time, factor 1.33) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf Finished HOLCF-Tutorial (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.42) Running Codegen ... Codegen: theory Codegen.Computations Codegen: theory Codegen.Adaptation Codegen: theory Codegen.Evaluation Codegen: theory Codegen.Further Codegen: theory Codegen.Inductive_Predicate Codegen: theory Codegen.Introduction Timing Isar_Ref (2 threads, 8.851s elapsed time, 14.256s cpu time, 0.960s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf Finished Isar_Ref (0:00:18 elapsed time, 0:00:24 cpu time, factor 1.32) Running IOA-NTP ... Codegen: theory Codegen.Foundations Codegen: theory Codegen.Refinement IOA-NTP: theory IOA-NTP.Lemmas IOA-NTP: theory IOA-NTP.Multiset IOA-NTP: theory IOA-NTP.Packet IOA-NTP: theory IOA-NTP.Action IOA-NTP: theory IOA-NTP.Abschannel IOA-NTP: theory IOA-NTP.Receiver IOA-NTP: theory IOA-NTP.Sender IOA-NTP: theory IOA-NTP.Spec IOA-NTP: theory IOA-NTP.Impl IOA-NTP: theory IOA-NTP.Correctness Timing IOA-NTP (2 threads, 6.711s elapsed time, 12.736s cpu time, 0.696s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP Finished IOA-NTP (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.66) Running HOL-TPTP ... Timing Codegen (2 threads, 6.777s elapsed time, 13.324s cpu time, 0.796s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf Finished Codegen (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.58) Running HOL-NanoJava ... HOL-NanoJava: theory HOL-NanoJava.Term HOL-TPTP: theory HOL-TPTP.TPTP_Parser HOL-TPTP: theory HOL-TPTP.MaSh_Export_Base HOL-TPTP: theory HOL-TPTP.MaSh_Eval HOL-TPTP: theory HOL-TPTP.ATP_Theory_Export HOL-TPTP: theory HOL-TPTP.THF_Arith HOL-NanoJava: theory HOL-NanoJava.Decl HOL-NanoJava: theory HOL-NanoJava.TypeRel HOL-NanoJava: theory HOL-NanoJava.State HOL-NanoJava: theory HOL-NanoJava.AxSem HOL-NanoJava: theory HOL-NanoJava.OpSem HOL-TPTP: theory HOL-TPTP.TPTP_Interpret HOL-NanoJava: theory HOL-NanoJava.Equivalence HOL-TPTP: theory HOL-TPTP.TPTP_Proof_Reconstruction HOL-NanoJava: theory HOL-NanoJava.Example HOL-TPTP: theory HOL-TPTP.ATP_Problem_Import Timing HOL-TPTP (2 threads, 6.222s elapsed time, 7.424s cpu time, 0.344s GC time, factor 1.19) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP Finished HOL-TPTP (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.09) Running Prog_Prove ... Prog_Prove: theory Prog_Prove.Basics Prog_Prove: theory Prog_Prove.Bool_nat_list Prog_Prove: theory Prog_Prove.LaTeXsugar Prog_Prove: theory Prog_Prove.Isar Prog_Prove: theory Prog_Prove.Logic Timing HOL-NanoJava (2 threads, 5.680s elapsed time, 10.152s cpu time, 0.656s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf Finished HOL-NanoJava (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.78) Running HOLCF-IMP ... Prog_Prove: theory Prog_Prove.MyList Prog_Prove: theory Prog_Prove.Types_and_funs HOLCF-IMP: theory HOL-IMP.AExp HOLCF-IMP: theory HOL-IMP.BExp HOLCF-IMP: theory HOL-IMP.Com HOLCF-IMP: theory HOL-IMP.Big_Step HOLCF-IMP: theory HOLCF-IMP.Denotational HOLCF-IMP: theory HOLCF-IMP.HoareEx Timing Prog_Prove (2 threads, 5.148s elapsed time, 10.128s cpu time, 0.804s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf Finished Prog_Prove (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.54) Running HOL-Unix ... HOL-Unix: theory HOL-Unix.Nested_Environment Timing HOLCF-IMP (2 threads, 5.669s elapsed time, 10.720s cpu time, 0.508s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/outline.pdf Finished HOLCF-IMP (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.81) Running HOL-Mirabelle-ex ... HOL-Mirabelle-ex: theory HOL-Mirabelle-ex.Ex HOL-Unix: theory HOL-Unix.Unix Timing HOL-Mirabelle-ex (2 threads, 5.208s elapsed time, 0.028s cpu time, 0.000s GC time, factor 0.01) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex Finished HOL-Mirabelle-ex (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.22) Running IOA-ABP ... IOA-ABP: theory IOA-ABP.Packet IOA-ABP: theory IOA-ABP.Lemmas IOA-ABP: theory IOA-ABP.Action IOA-ABP: theory IOA-ABP.Abschannel IOA-ABP: theory IOA-ABP.Env Timing HOL-Unix (2 threads, 5.827s elapsed time, 9.840s cpu time, 0.640s GC time, factor 1.69) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf Finished HOL-Unix (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.68) Running HOL-Isar_Examples ... IOA-ABP: theory IOA-ABP.Receiver IOA-ABP: theory IOA-ABP.Sender IOA-ABP: theory IOA-ABP.Abschannel_finite IOA-ABP: theory IOA-ABP.Impl IOA-ABP: theory IOA-ABP.Impl_finite HOL-Isar_Examples: theory HOL-Isar_Examples.Higher_Order_Logic HOL-Isar_Examples: theory HOL-Isar_Examples.First_Order_Logic HOL-Isar_Examples: theory HOL-Isar_Examples.Basic_Logic HOL-Isar_Examples: theory HOL-Isar_Examples.Cantor HOL-Isar_Examples: theory HOL-Isar_Examples.Drinker HOL-Isar_Examples: theory HOL-Isar_Examples.Expr_Compiler HOL-Isar_Examples: theory HOL-Isar_Examples.Group IOA-ABP: theory IOA-ABP.Spec IOA-ABP: theory IOA-ABP.Correctness HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Context HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Notepad HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare HOL-Isar_Examples: theory HOL-Isar_Examples.Knaster_Tarski HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare_Ex HOL-Isar_Examples: theory HOL-Isar_Examples.Mutilated_Checkerboard HOL-Isar_Examples: theory HOL-Isar_Examples.Peirce HOL-Isar_Examples: theory HOL-Isar_Examples.Puzzle HOL-Isar_Examples: theory HOL-Isar_Examples.Structured_Statements HOL-Isar_Examples: theory HOL-Isar_Examples.Summation HOL-Isar_Examples: theory HOL-Isar_Examples.Fibonacci Timing IOA-ABP (2 threads, 4.865s elapsed time, 9.156s cpu time, 0.256s GC time, factor 1.88) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP Finished IOA-ABP (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.58) Running HOLCF-ex ... HOLCF-ex: theory HOLCF-ex.Dagstuhl HOLCF-ex: theory HOLCF-ex.Focus_ex HOLCF-ex: theory HOLCF-ex.Concurrency_Monad HOLCF-ex: theory HOLCF-ex.Dnat HOLCF-ex: theory HOLCF-ex.Domain_Proofs HOLCF-ex: theory HOLCF-ex.Fix2 HOLCF-ex: theory HOLCF-ex.Hoare HOLCF-ex: theory HOLCF-ex.Letrec HOLCF-ex: theory HOLCF-ex.Loop HOLCF-ex: theory HOLCF-ex.Pattern_Match HOLCF-ex: theory HOLCF-ex.Powerdomain_ex Timing HOLCF-ex (2 threads, 4.713s elapsed time, 9.384s cpu time, 0.252s GC time, factor 1.99) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex Finished HOLCF-ex (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.64) Running HOL-SPARK-Manual ... Timing HOL-Isar_Examples (2 threads, 5.237s elapsed time, 9.808s cpu time, 0.660s GC time, factor 1.87) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf Finished HOL-Isar_Examples (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.74) Running HOLCF-FOCUS ... HOL-SPARK-Manual: theory HOL-SPARK-Manual.Complex_Types HOL-SPARK-Manual: theory HOL-SPARK-Examples.Greatest_Common_Divisor HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc1 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles HOLCF-FOCUS: theory HOLCF-FOCUS.Fstream HOLCF-FOCUS: theory HOLCF-FOCUS.Fstreams HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor HOLCF-FOCUS: theory HOLCF-FOCUS.FOCUS HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification HOLCF-FOCUS: theory HOLCF-FOCUS.Stream_adm HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer_adm Timing HOLCF-FOCUS (2 threads, 3.831s elapsed time, 7.512s cpu time, 0.228s GC time, factor 1.96) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS Finished HOLCF-FOCUS (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.58) Running HOL-IMPP ... HOL-IMPP: theory HOL-IMPP.Com HOL-IMPP: theory HOL-IMPP.Natural HOL-IMPP: theory HOL-IMPP.Hoare Timing HOL-SPARK-Manual (2 threads, 4.517s elapsed time, 7.268s cpu time, 0.224s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf Finished HOL-SPARK-Manual (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.70) Running HOL-ZF ... HOL-IMPP: theory HOL-IMPP.Misc HOL-IMPP: theory HOL-IMPP.EvenOdd HOL-ZF: theory HOL-ZF.LProd HOL-ZF: theory HOL-ZF.HOLZF HOL-ZF: theory HOL-ZF.Zet HOL-ZF: theory HOL-ZF.MainZF Timing HOL-IMPP (2 threads, 3.884s elapsed time, 6.688s cpu time, 0.236s GC time, factor 1.72) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP Finished HOL-IMPP (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.42) Running HOL-Hahn_Banach ... HOL-ZF: theory HOL-ZF.Games HOL-Hahn_Banach: theory HOL-Hahn_Banach.Zorn_Lemma HOL-Hahn_Banach: theory HOL-Analysis.Continuum_Not_Denumerable HOL-Hahn_Banach: theory HOL-Hahn_Banach.Bounds HOL-Hahn_Banach: theory HOL-Hahn_Banach.Vector_Space HOL-Hahn_Banach: theory HOL-Hahn_Banach.Linearform HOL-Hahn_Banach: theory HOL-Hahn_Banach.Subspace HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Order HOL-Hahn_Banach: theory HOL-Hahn_Banach.Normed_Space HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Norm HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Lemmas HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach Timing HOL-ZF (2 threads, 3.860s elapsed time, 7.112s cpu time, 0.244s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf Finished HOL-ZF (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.69) Running Implementation ... Implementation: theory Implementation.Base Implementation: theory Implementation.Integration Implementation: theory Implementation.Eq Implementation: theory Implementation.Isar Implementation: theory Implementation.Local_Theory Implementation: theory Implementation.ML Implementation: theory Implementation.Prelim Implementation: theory Implementation.Proof Implementation: theory Implementation.Syntax Implementation: theory Implementation.Tactic Timing HOL-Hahn_Banach (2 threads, 3.474s elapsed time, 6.576s cpu time, 0.208s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf Finished HOL-Hahn_Banach (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.72) Running Functions ... Functions: theory Functions.Functions Implementation: theory Implementation.Logic Timing Implementation (2 threads, 3.444s elapsed time, 6.020s cpu time, 0.144s GC time, factor 1.75) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf Finished Implementation (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.35) Timing Functions (2 threads, 2.840s elapsed time, 3.924s cpu time, 0.260s GC time, factor 1.38) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf Finished Functions (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.24) Running HOL-Nonstandard_Analysis-Examples ... Running HOL-IOA ... HOL-IOA: theory HOL-IOA.Asig HOL-IOA: theory HOL-IOA.IOA HOL-IOA: theory HOL-IOA.Solve HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes Timing HOL-IOA (2 threads, 2.405s elapsed time, 3.536s cpu time, 0.168s GC time, factor 1.47) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA Finished HOL-IOA (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.18) Running HOL-TLA-Inc ... HOL-TLA-Inc: theory HOL-TLA-Inc.Inc Timing HOL-Nonstandard_Analysis-Examples (2 threads, 2.698s elapsed time, 3.376s cpu time, 0.180s GC time, factor 1.25) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples Finished HOL-Nonstandard_Analysis-Examples (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.04) Running HOL-Lattice ... HOL-Lattice: theory HOL-Lattice.Orders HOL-Lattice: theory HOL-Lattice.Bounds HOL-Lattice: theory HOL-Lattice.Lattice HOL-Lattice: theory HOL-Lattice.CompleteLattice Timing HOL-TLA-Inc (2 threads, 2.093s elapsed time, 3.684s cpu time, 0.140s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc Finished HOL-TLA-Inc (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.32) Running Classes ... Classes: theory Classes.Setup Classes: theory Classes.Classes Timing HOL-Lattice (2 threads, 1.675s elapsed time, 3.044s cpu time, 0.000s GC time, factor 1.82) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf Finished HOL-Lattice (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.78) Running Eisbach ... Eisbach: theory Eisbach.Base Eisbach: theory Eisbach.Preface Eisbach: theory Eisbach.Manual Timing Classes (2 threads, 1.603s elapsed time, 1.800s cpu time, 0.000s GC time, factor 1.12) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf Finished Classes (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.10) Running IOA-Storage ... IOA-Storage: theory IOA-Storage.Action IOA-Storage: theory IOA-Storage.Impl IOA-Storage: theory IOA-Storage.Spec IOA-Storage: theory IOA-Storage.Correctness Timing IOA-Storage (2 threads, 1.322s elapsed time, 1.992s cpu time, 0.000s GC time, factor 1.51) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage Finished IOA-Storage (0:00:02 elapsed time, 0:00:03 cpu time) Running Locales ... Timing Eisbach (2 threads, 1.258s elapsed time, 1.776s cpu time, 0.000s GC time, factor 1.41) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf Finished Eisbach (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.17) Running Main ... Locales: theory Locales.Examples Locales: theory Locales.Examples1 Locales: theory Locales.Examples2 Locales: theory Locales.Examples3 Main: theory Main.Main_Doc Timing Main (2 threads, 1.183s elapsed time, 1.280s cpu time, 0.000s GC time, factor 1.08) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf Finished Main (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.10) Running HOL-Import ... Timing Locales (2 threads, 1.132s elapsed time, 2.084s cpu time, 0.000s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf Finished Locales (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.26) Running HOL-Types_To_Sets ... HOL-Import: theory HOL-Import.Import_Setup HOL-Import: theory HOL-Import.HOL_Light_Maps HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE) Timing HOL-Import (2 threads, 0.907s elapsed time, 1.664s cpu time, 0.000s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import Finished HOL-Import (0:00:02 elapsed time) Running Sugar ... Timing HOL-Types_To_Sets (2 threads, 0.866s elapsed time, 1.420s cpu time, 0.000s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets Finished HOL-Types_To_Sets (0:00:02 elapsed time) Running IOA-ex ... Sugar: theory HOL-Library.LaTeXsugar Sugar: theory HOL-Library.OptionalSugar Sugar: theory Sugar.Sugar IOA-ex: theory IOA-ex.TrivEx IOA-ex: theory IOA-ex.TrivEx2 Timing IOA-ex (2 threads, 0.703s elapsed time, 1.508s cpu time, 0.000s GC time, factor 2.14) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex Finished IOA-ex (0:00:02 elapsed time) Running HOL-Mutabelle ... HOL-Mutabelle: theory HOL-Mutabelle.MutabelleExtra Timing Sugar (2 threads, 0.864s elapsed time, 0.992s cpu time, 0.000s GC time, factor 1.15) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf Finished Sugar (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.12) Running HOL-TLA-Buffer ... HOL-TLA-Buffer: theory HOL-TLA-Buffer.Buffer HOL-TLA-Buffer: theory HOL-TLA-Buffer.DBuffer Timing HOL-Mutabelle (2 threads, 0.525s elapsed time, 0.624s cpu time, 0.000s GC time, factor 1.19) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle Finished HOL-Mutabelle (0:00:02 elapsed time) Running JEdit ... JEdit: theory JEdit.Base JEdit: theory JEdit.JEdit Timing HOL-TLA-Buffer (2 threads, 0.529s elapsed time, 0.996s cpu time, 0.000s GC time, factor 1.88) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer Finished HOL-TLA-Buffer (0:00:01 elapsed time) Running How_to_Prove_it ... How_to_Prove_it: theory How_to_Prove_it.How_to_Prove_it Timing How_to_Prove_it (2 threads, 0.281s elapsed time, 0.416s cpu time, 0.000s GC time, factor 1.48) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf Finished How_to_Prove_it (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.11) Running HOL-Prolog ... HOL-Prolog: theory HOL-Prolog.HOHH HOL-Prolog: theory HOL-Prolog.Func HOL-Prolog: theory HOL-Prolog.Test HOL-Prolog: theory HOL-Prolog.Type Timing HOL-Prolog (2 threads, 0.340s elapsed time, 0.544s cpu time, 0.000s GC time, factor 1.60) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog Finished HOL-Prolog (0:00:01 elapsed time) Running Typeclass_Hierarchy ... Typeclass_Hierarchy: theory Typeclass_Hierarchy.Typeclass_Hierarchy Timing JEdit (2 threads, 0.512s elapsed time, 0.584s cpu time, 0.000s GC time, factor 1.14) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf Finished JEdit (0:00:10 elapsed time, 0:00:10 cpu time, factor 1.04) Timing Typeclass_Hierarchy (2 threads, 0.243s elapsed time, 0.352s cpu time, 0.000s GC time, factor 1.45) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf Finished Typeclass_Hierarchy (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.14) Build timed out (after 120 minutes). Marking the build as aborted. Build was aborted 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 0 seconds No emails were triggered. Finished: ABORTED