Started by upstream project "isabelle-repo" build number 1495 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 7b84ecd54d7070d93e0718ae88d67e69ca7a675d pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes adding changesets adding manifests adding file changes added 5 changesets with 11 changes to 11 files (run 'hg update' to get a working copy) [isabelle-repo-makeall] $ hg update --clean --rev 7b84ecd54d7070d93e0718ae88d67e69ca7a675d 11 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/jenkins7723354941792258985.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 Fri, 2 Mar 2018 18:55:38 GMT Isabelle id 7b84ecd54d70 === 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.749s elapsed time, 0.752s cpu time, 0.000s GC time, factor 1.00) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure Finished Pure (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.98) 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 HOL: theory HOL.HOL ZF: theory ZF.Fixedpt ZF: theory ZF.Sum 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 HOL: theory HOL.Argo ZF: theory ZF.CardinalArith HOL: theory HOL.Ctr_Sugar ZF: theory ZF.List_ZF HOL-Proofs: theory HOL.Argo HOL-Proofs: theory HOL.Ctr_Sugar ZF: theory ZF.Bin HOL: theory HOL.Orderings ZF: theory ZF.IntDiv_ZF HOL-Proofs: theory HOL.Orderings HOL: theory HOL.SAT ZF: theory ZF ZF: theory ZF.AC HOL-Proofs: theory HOL.SAT ZF: theory ZF.Zorn ZF: theory ZF.Cardinal_AC ZF: theory ZF.InfDatatype ZF: theory ZFC HOL: theory HOL.Groups HOL-Proofs: theory HOL.Groups HOL: theory HOL.Lattices HOL: theory HOL.Set HOL-Proofs: theory HOL.Lattices HOL: theory HOL.Fun HOL: theory HOL.Typedef HOL: theory HOL.Rings HOL: theory HOL.Complete_Lattices HOL-Proofs: theory HOL.Set HOL: theory HOL.Inductive 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, 24.234s elapsed time, 38.820s cpu time, 2.332s GC time, factor 1.60) 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:39 elapsed time, 0:01:04 cpu time, factor 1.63) Building ZF-Induct ... HOL-Proofs: theory HOL.Product_Type ZF-Induct: theory ZF-Induct.Binary_Trees ZF-Induct: theory ZF-Induct.Acc 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 HOL: theory HOL.Relation ZF-Induct: theory ZF-Induct.PropLog 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-Proofs: theory HOL.Sum_Type HOL: theory HOL.Fun_Def_Base HOL: theory HOL.Hilbert_Choice HOL: theory HOL.Wfrec HOL: theory HOL.Order_Relation HOL: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.Zorn HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.BNF_Cardinal_Arithmetic HOL-Proofs: theory HOL.Nat HOL: theory HOL.BNF_Def HOL: theory HOL.BNF_Composition HOL: theory HOL.Basic_BNFs HOL: theory HOL.BNF_Fixpoint_Base HOL-Proofs: theory HOL.Fields HOL-Proofs: theory HOL.Meson HOL-Proofs: theory HOL.ATP Timing ZF-Induct (2 threads, 8.112s elapsed time, 12.944s cpu time, 0.624s GC time, factor 1.60) 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:15 elapsed time, 0:00:24 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.708s elapsed time, 4.084s cpu time, 0.176s GC time, factor 1.10) 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:08 elapsed time, 0:00:11 cpu time, factor 1.39) Building FOLP ... FOLP: theory IFOLP FOLP: theory FOLP HOL: theory HOL.Power Timing FOLP (2 threads, 1.316s elapsed time, 1.328s 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 ZF-UNITY: theory ZF-UNITY.Constrains HOL: theory HOL.Groups_Big 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 ZF-UNITY: theory ZF-UNITY.Union ZF-UNITY: theory ZF-UNITY.Comp HOL-Proofs: theory HOL.Relation HOL: theory HOL.Equiv_Relations ZF-UNITY: theory ZF-UNITY.Guar HOL: theory HOL.Lifting ZF-UNITY: theory ZF-UNITY.AllocBase ZF-UNITY: theory ZF-UNITY.ClientImpl ZF-UNITY: theory ZF-UNITY.AllocImpl ZF-UNITY: theory ZF-UNITY.Distributor ZF-UNITY: theory ZF-UNITY.Merge 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: theory HOL.Int HOL-Proofs: theory HOL.Wellfounded HOL-Proofs: theory HOL.Fun_Def_Base HOL: theory HOL.Euclidean_Division HOL-Proofs: theory HOL.Hilbert_Choice HOL-Proofs: theory HOL.Wfrec HOL-Proofs: theory HOL.Order_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Relation HOL-Proofs: theory HOL.Zorn Timing ZF-UNITY (2 threads, 18.903s elapsed time, 33.192s cpu time, 1.300s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY Finished ZF-UNITY (0:00:19 elapsed time, 0:00:33 cpu time, factor 1.70) Running ZF-Constructible ... HOL: theory HOL.Parity ZF-Constructible: theory ZF-Constructible.Formula ZF-Constructible: theory ZF-Constructible.MetaExists ZF-Constructible: theory ZF-Constructible.Normal ZF-Constructible: theory ZF-Constructible.Reflection HOL-Proofs: theory HOL.BNF_Wellorder_Embedding ZF-Constructible: theory ZF-Constructible.Relative ZF-Constructible: theory ZF-Constructible.L_axioms ZF-Constructible: theory ZF-Constructible.Wellorderings HOL-Proofs: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.Divides 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 ZF-Constructible: theory ZF-Constructible.Internalize ZF-Constructible: theory ZF-Constructible.AC_in_L HOL: theory HOL.SMT HOL: theory HOL.Semiring_Normalization ZF-Constructible: theory ZF-Constructible.Rec_Separation ZF-Constructible: theory ZF-Constructible.Rank_Separation HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.Set_Interval 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-Proofs: theory HOL.BNF_Cardinal_Arithmetic HOL: theory HOL.Presburger 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, 20.348s elapsed time, 38.864s cpu time, 8.740s GC time, factor 1.91) 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:27 elapsed time, 0:00:51 cpu time, factor 1.88) 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 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-Proofs: theory HOL.BNF_Least_Fixpoint ZF-ex: theory ZF-ex.Ramsey ZF-ex: theory ZF-ex.misc HOL: theory HOL.Groups_List HOL: theory HOL.Map HOL: theory HOL.Factorial HOL: theory HOL.GCD HOL: theory HOL.Binomial HOL-Proofs: theory HOL.Basic_BNF_LFPs HOL-Proofs: theory HOL.Transfer HOL: theory HOL.Enum HOL-Proofs: theory HOL.Num HOL: theory HOL.String HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Predicate Timing ZF-ex (2 threads, 12.465s elapsed time, 18.204s cpu time, 0.732s GC time, factor 1.46) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex Finished ZF-ex (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.39) Running CCL ... CCL: theory IFOL HOL: theory HOL.Lazy_Sequence HOL: theory HOL.Limited_Sequence CCL: theory FOL HOL: theory HOL.Typerep HOL: theory HOL.Code_Evaluation CCL: theory CCL.Set CCL: theory CCL.Lfp CCL: theory CCL.Gfp CCL: theory CCL.CCL HOL: theory HOL.Random CCL: theory CCL.Term CCL: theory CCL.Trancl CCL: theory CCL.Type HOL-Proofs: theory HOL.Power CCL: theory CCL.Fix HOL: theory HOL.Quickcheck_Random 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.Quickcheck_Exhaustive HOL: theory HOL.Quickcheck_Narrowing Timing CCL (2 threads, 7.217s elapsed time, 9.940s cpu time, 0.740s GC time, factor 1.38) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL Finished CCL (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.28) 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.HH 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 HOL-Proofs: theory HOL.Groups_Big 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: theory HOL.Random_Pred HOL: theory HOL.Record HOL: theory HOL.Random_Sequence HOL: theory HOL.Predicate_Compile HOL: theory HOL.Nitpick HOL-Proofs: theory HOL.Equiv_Relations HOL-Proofs: theory HOL.Lifting Timing ZF-AC (2 threads, 6.827s elapsed time, 11.468s cpu time, 0.660s GC time, factor 1.68) 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:11 elapsed time, 0:00:18 cpu time, factor 1.70) 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 FOL-ex: theory FOL-ex.Propositional_Cla 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.Nunchaku FOL-ex: theory FOL-ex.Locale_Test1 HOL-Proofs: theory HOL.Lifting_Set HOL: theory Main HOL-Proofs: theory HOL.Option HOL-Proofs: theory HOL.Quotient HOL-Proofs: theory HOL.Extraction HOL: theory HOL.Archimedean_Field HOL: theory HOL.Topological_Spaces FOL-ex: theory FOL-ex.Locale_Test2 FOL-ex: theory FOL-ex.Locale_Test3 FOL-ex: theory FOL-ex.Locale_Test HOL-Proofs: theory HOL.Lattices_Big HOL-Proofs: theory HOL.Partial_Function HOL: theory HOL.Rat Timing FOL-ex (2 threads, 6.449s elapsed time, 9.136s cpu time, 0.248s GC time, factor 1.42) 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:11 elapsed time, 0:00:16 cpu time, factor 1.49) 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 HOL-Proofs: theory HOL.Fun_Def HOL: theory HOL.Real FOLP-ex: theory FOLP-ex.Foundation FOLP-ex: theory FOLP-ex.Intuitionistic FOLP-ex: theory FOLP-ex.Propositional_Int FOLP-ex: theory FOLP-ex.Quantifiers_Int HOL-Proofs: theory HOL.Int HOL: theory HOL.Real_Vector_Spaces Timing FOLP-ex (2 threads, 3.902s elapsed time, 6.780s cpu time, 0.100s GC time, factor 1.74) 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:07 cpu time, factor 1.52) Running Sequents ... Sequents: theory Sequents.Sequents Sequents: theory Sequents.ILL Sequents: theory Sequents.LK0 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-Proofs: theory HOL.Euclidean_Division Timing Sequents (2 threads, 3.749s elapsed time, 7.268s cpu time, 0.144s GC time, factor 1.94) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.66) Running LCF ... LCF: theory IFOL LCF: theory FOL HOL: theory HOL.Inequalities HOL: theory HOL.Limits LCF: theory LCF.LCF LCF: theory LCF.Ex1 LCF: theory LCF.Ex2 LCF: theory LCF.Ex3 LCF: theory LCF.Ex4 Timing LCF (2 threads, 3.642s elapsed time, 4.108s cpu time, 0.160s 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 HOL: theory HOL.Deriv Timing Spec_Check (2 threads, 1.980s elapsed time, 3.324s cpu time, 0.020s 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 ... ZF-Resid: theory ZF-Resid.Redex ZF-Resid: theory ZF-Resid.Substitution ZF-Resid: theory ZF-Resid.Residuals HOL: theory HOL.NthRoot ZF-Resid: theory ZF-Resid.Reduction ZF-Resid: theory ZF-Resid.Confluence HOL: theory HOL.Series HOL-Proofs: theory HOL.Parity HOL: theory HOL.Transcendental Timing ZF-Resid (2 threads, 1.755s elapsed time, 2.832s cpu time, 0.000s GC time, factor 1.61) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid Finished ZF-Resid (0:00:02 elapsed time, 0:00:03 cpu 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 HOL: theory HOL.Complex HOL: theory HOL.MacLaurin Timing ZF-IMP (2 threads, 1.062s elapsed time, 1.216s cpu time, 0.000s GC time, factor 1.14) 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:07 cpu time, factor 1.65) Running CTT ... CTT: theory CTT.CTT CTT: theory CTT.Elimination CTT: theory CTT.Equality CTT: theory CTT.Synthesis CTT: theory CTT.Typechecking HOL: theory Complex_Main HOL-Proofs: theory HOL.Code_Numeral Timing CTT (2 threads, 0.989s elapsed time, 1.384s cpu time, 0.000s GC time, factor 1.40) 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:07 cpu time, factor 1.69) 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 Timing ZF-Coind (2 threads, 0.743s elapsed time, 1.452s cpu time, 0.000s GC time, factor 1.95) 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.348s elapsed time, 0.360s cpu time, 0.000s GC time, factor 1.03) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube Finished Cube (0:00:00 elapsed time) Running Logics_ZF ... Logics_ZF: theory Logics_ZF.FOL_examples Logics_ZF: theory Logics_ZF.If Logics_ZF: theory Logics_ZF.ZF_Isar Logics_ZF: theory Logics_ZF.ZF_examples Logics_ZF: theory Logics_ZF.IFOL_examples HOL-Proofs: theory HOL.Numeral_Simprocs HOL-Proofs: theory HOL.Semiring_Normalization HOL-Proofs: theory HOL.SMT Timing Logics_ZF (2 threads, 0.312s elapsed time, 0.620s cpu time, 0.000s GC time, factor 1.99) 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:05 elapsed time, 0:00:05 cpu time, factor 1.15) Running Intro ... HOL-Proofs: theory HOL.Set_Interval 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:04 elapsed time, 0:00:04 cpu time, factor 1.14) Running Logics ... 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:04 elapsed time, 0:00:04 cpu time, factor 1.13) Running Nitpick ... 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.13) 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 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices Timing System (2 threads, 0.385s elapsed time, 0.552s cpu time, 0.000s GC time, factor 1.43) 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:05 cpu time, factor 1.14) Running SML ... SML: theory SML.Examples Timing SML (2 threads, 0.017s elapsed time, 0.016s cpu time, 0.000s GC time, factor 0.95) 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:04 elapsed time, 0:00:04 cpu time, factor 1.14) 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, 302.788s elapsed time, 569.148s cpu time, 61.532s GC time, factor 1.88) 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:06:30 elapsed time, 0:11:45 cpu time, factor 1.80) Building HOL-Library ... Building HOLCF ... HOLCF: theory HOL-Library.Old_Datatype HOLCF: theory HOL-Library.Nat_Bijection 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 HOL-Library: theory HOL-Library.Bit HOLCF: theory HOLCF.Cfun HOL-Library: theory HOL-Library.Boolean_Algebra HOL-Library: theory HOL-Library.Cancellation HOLCF: theory HOLCF.Completion HOLCF: theory HOLCF.Cprod HOLCF: theory HOLCF.Deflation 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 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 HOLCF: theory HOLCF.Universal HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Binary_Nat 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 HOLCF: theory HOLCF.Algebraic HOLCF: theory HOLCF.Compact_Basis HOL-Library: theory HOL-Library.DAList_Multiset HOLCF: theory HOLCF.LowerPD HOLCF: theory HOLCF.UpperPD HOLCF: theory HOLCF.Representable HOLCF: theory HOLCF.ConvexPD HOL-Library: theory HOL-Library.Multiset_Order HOL-Library: theory HOL-Library.Permutation HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Complete_Partial_Order2 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-Library: theory HOL-Library.Fun_Lexorder HOL-Library: theory HOL-Library.FuncSet HOL-Library: theory HOL-Library.Function_Algebras HOL-Library: theory HOL-Library.Function_Division HOL-Library: theory HOL-Library.Groups_Big_Fun HOLCF: theory HOLCF.Powerdomains 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 HOLCF: theory HOLCF HOL-Library: theory HOL-Library.LaTeXsugar HOL-Library: theory HOL-Library.Lattice_Constructions HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.List_lexord HOL-Library: theory HOL-Library.Mapping HOL-Library: theory HOL-Library.AList_Mapping HOL-Library: theory HOL-Library.Monad_Syntax HOL-Library: theory HOL-Library.State_Monad HOL-Library: theory HOL-Library.More_List HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Old_Datatype HOL-Library: theory HOL-Library.Stream HOL-Library: theory HOL-Library.Old_Recdef HOL-Library: theory HOL-Library.Open_State_Syntax HOL-Library: theory HOL-Library.Option_ord HOL-Library: theory HOL-Library.Parallel HOL-Library: theory HOL-Library.Pattern_Aliases HOL-Library: theory HOL-Library.Perm HOL-Library: theory HOL-Library.Phantom_Type HOL-Library: theory HOL-Library.Cardinality HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Numeral_Type 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.Finite_Lattice HOL-Library: theory HOL-Library.Type_Length HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.Quotient_Syntax HOL-Library: theory HOL-Library.Quotient_Option HOL-Proofs: theory HOL.String 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.BNF_Greatest_Fixpoint 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-Library: theory HOL-Library.Stirling HOL-Library: theory HOL-Library.Sublist HOL-Proofs: theory HOL.Predicate HOL-Library: theory HOL-Library.Prefix_Order HOL-Library: theory HOL-Library.Subseq_Order HOL-Library: theory HOL-Library.Transitive_Closure_Table HOL-Library: theory HOL-Library.Tree Timing HOLCF (2 threads, 18.279s elapsed time, 36.236s cpu time, 2.644s GC time, factor 1.98) 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:40 elapsed time, 0:01:09 cpu time, factor 1.73) Building IOA ... IOA: theory IOA.Seq IOA: theory IOA.Asig HOL-Proofs: theory HOL.Lazy_Sequence IOA: theory IOA.Automata IOA: theory IOA.Sequence HOL-Proofs: theory HOL.Limited_Sequence HOL-Library: theory HOL-Library.Tree_Multiset IOA: theory IOA.Pred HOL-Proofs: theory HOL.Typerep HOL-Library: theory HOL-Library.Uprod IOA: theory IOA.Traces IOA: theory IOA.TL HOL-Library: theory HOL-Library.While_Combinator HOL-Proofs: theory HOL.Code_Evaluation IOA: theory IOA.CompoExecs HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint IOA: theory IOA.RefMappings IOA: theory IOA.RefCorrectness IOA: theory IOA.CompoScheds HOL-Library: theory HOL-Library.Countable IOA: theory IOA.Simulations IOA: theory IOA.SimCorrectness IOA: theory IOA.Deadlock IOA: theory IOA.ShortExecutions HOL-Library: theory HOL-Library.Countable_Set HOL-Proofs: theory HOL.Random IOA: theory IOA.CompoTraces HOL-Library: theory HOL-Library.Countable_Complete_Lattices HOL-Proofs: theory HOL.Quickcheck_Random IOA: theory IOA.Compositionality IOA: theory IOA.IOA IOA: theory IOA.TLS IOA: theory IOA.LiveIOA IOA: theory IOA.Abstraction HOL-Library: theory HOL-Library.Countable_Set_Type HOL-Proofs: theory HOL.Quickcheck_Exhaustive HOL-Library: theory HOL-Library.FSet HOL-Library: theory HOL-Library.Finite_Map HOL-Proofs: theory HOL.Record HOL-Library: theory HOL-Library.BigO HOL-Proofs: theory HOL.Nitpick 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.RBT HOL-Library: theory HOL-Library.Float HOL-Proofs: theory HOL.Nunchaku HOL-Library: theory HOL-Library.RBT_Mapping HOL-Library: theory HOL-Library.RBT_Set HOL-Proofs: theory HOL.Quickcheck_Narrowing 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.Sum_of_Squares HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Extended_Real HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Proofs: theory HOL.Random_Pred Timing IOA (2 threads, 17.608s elapsed time, 33.316s cpu time, 1.612s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA Finished IOA (0:00:32 elapsed time, 0:00:53 cpu time, factor 1.64) Building HOL-TLA ... HOL-Proofs: theory HOL.Random_Sequence HOL-TLA: theory HOL-TLA.Intensional HOL-Library: theory HOL-Library.Tree_Real HOL-TLA: theory HOL-TLA.Stfun HOL-TLA: theory HOL-TLA.Action HOL-Proofs: theory HOL.Predicate_Compile HOL-TLA: theory HOL-TLA.Init HOL-TLA: theory HOL-TLA.TLA HOL-Library: theory HOL-Library.Extended_Nonnegative_Real HOL-Library: theory HOL-Library.Library HOL-Proofs: theory Main HOL-Proofs: theory HOL-Library.Realizers Timing HOL-TLA (2 threads, 1.830s elapsed time, 2.968s cpu time, 0.000s GC time, factor 1.62) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA Finished HOL-TLA (0:00:12 elapsed time, 0:00:15 cpu time, factor 1.31) 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-Library.Set_Algebras HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring HOL-Analysis: theory HOL-Library.Permutations 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-Computational_Algebra.Euclidean_Algorithm HOL-Analysis: theory HOL-Analysis.Product_Vector 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-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Library.Discrete HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Library.Liminf_Limsup 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-Analysis.Norm_Arith HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real 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.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Tagged_Division HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Starlike HOL-Analysis: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Uniform_Limit 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.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers 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, 203.385s elapsed time, 386.124s cpu time, 28.004s GC time, factor 1.90) 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:04:35 elapsed time, 0:08:17 cpu time, factor 1.80) Building HOL-Computational_Algebra ... HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure 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.Nth_Powers HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring 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, 67.649s elapsed time, 120.236s cpu time, 6.868s GC time, factor 1.78) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Computational_Algebra Finished HOL-Computational_Algebra (0:01:36 elapsed time, 0:02:37 cpu time, factor 1.64) Building HOL-Number_Theory ... HOL-Number_Theory: theory HOL-Number_Theory.Cong HOL-Number_Theory: theory HOL-Algebra.Congruence 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.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.Ideal 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.Pocklington HOL-Number_Theory: theory HOL-Number_Theory.Gauss HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory Timing HOL-Number_Theory (2 threads, 109.648s elapsed time, 197.340s cpu time, 13.852s GC time, factor 1.80) 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:41 elapsed time, 0:04:24 cpu time, factor 1.64) Building HOL-Algebra ... HOL-Algebra: theory HOL-Algebra.Exponent HOL-Algebra: theory HOL-Algebra.Congruence 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.FiniteProduct HOL-Algebra: theory HOL-Algebra.Ring HOL-Algebra: theory HOL-Algebra.Sylow HOL-Algebra: theory HOL-Algebra.Divisibility 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, 90.379s elapsed time, 163.592s cpu time, 19.840s GC time, factor 1.81) 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:29 elapsed time, 0:04:00 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-Word.Bit_Representation HOL-Word: theory HOL-Library.Cardinality 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.Bit_Comparison HOL-Word: theory HOL-Word.Bool_List_Representation HOL-Word: theory HOL-Word.Word_Miscellaneous 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, 24.524s elapsed time, 47.360s cpu time, 2.364s GC time, factor 1.93) 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:43 elapsed time, 0:01:16 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, 14.915s elapsed time, 29.384s cpu time, 1.396s 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:29 elapsed time, 0:00:47 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.667s elapsed time, 3.548s cpu time, 0.132s GC time, factor 1.33) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK Finished HOL-SPARK (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.28) 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.Shared 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.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, 773.917s elapsed time, 1384.140s cpu time, 61.948s 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:14:32 elapsed time, 0:25:16 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.Probability_Mass_Function HOL-Probability: theory HOL-Probability.Projective_Family HOL-Probability: theory HOL-Probability.Infinite_Product_Measure HOL-Probability: theory HOL-Probability.Independent_Family 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.Convolution HOL-Probability: theory HOL-Probability.Information HOL-Probability: theory HOL-Probability.Distributions HOL-Probability: theory HOL-Probability.Projective_Limit HOL-Probability: theory HOL-Probability.Characteristic_Functions HOL-Probability: theory HOL-Probability.Sinc_Integral HOL-Probability: theory HOL-Probability.Stream_Space HOL-Probability: theory HOL-Probability.Levy HOL-Probability: theory HOL-Probability.Tree_Space HOL-Probability: theory HOL-Probability.Central_Limit_Theorem HOL-Probability: theory HOL-Probability.Probability Timing HOL-Auth (2 threads, 187.166s elapsed time, 299.636s cpu time, 13.900s GC time, factor 1.60) 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:41 elapsed time, 0:05:53 cpu time, factor 1.59) 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, 11.090s elapsed time, 21.112s cpu time, 1.280s 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:35 elapsed time, 0:00:58 cpu time, factor 1.63) Building HOL-Nominal ... HOL-Nominal: theory HOL-Nominal.Nominal Timing HOL-Nominal (2 threads, 7.427s elapsed time, 13.280s cpu time, 0.736s 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:25 elapsed time, 0:00:38 cpu time, factor 1.47) 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, 4.027s elapsed time, 8.064s cpu time, 0.260s 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:15 elapsed time, 0:00:23 cpu time, factor 1.49) Building Codegen_Basics ... Codegen_Basics: theory Codegen_Basics.Setup Timing Codegen_Basics (2 threads, 1.446s elapsed time, 1.568s cpu time, 0.000s GC time, factor 1.08) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics Finished Codegen_Basics (0:00:17 elapsed time, 0:00:22 cpu time, factor 1.29) Building Typeclass_Hierarchy_Basics ... Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup Timing Typeclass_Hierarchy_Basics (2 threads, 0.870s elapsed time, 0.980s cpu time, 0.000s GC time, factor 1.13) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics Finished Typeclass_Hierarchy_Basics (0:00:17 elapsed time, 0:00:22 cpu time, factor 1.30) Building HOL-Mirabelle ... HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test Timing HOL-Mirabelle (2 threads, 0.559s elapsed time, 0.656s cpu time, 0.000s GC time, factor 1.17) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle Finished HOL-Mirabelle (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.26) 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, 169.344s elapsed time, 311.920s cpu time, 21.872s 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:03:31 elapsed time, 0:06:15 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-Nominal-Examples: theory HOL-Nominal-Examples.Crary HOL-Decision_Procs: theory HOL-Decision_Procs.MIR 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-Nominal-Examples: theory HOL-Nominal-Examples.SOS HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation HOL-Nominal-Examples: theory HOL-Nominal-Examples.W 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.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, 625.690s elapsed time, 1196.032s cpu time, 115.444s 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:10:29 elapsed time, 0:19:58 cpu time, factor 1.91) 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-Data_Structures.Tree234_Map HOL-Data_Structures: theory HOL-Library.Tree_Real 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, 659.748s elapsed time, 1231.688s cpu time, 147.764s GC time, factor 1.87) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples Finished HOL-Nominal-Examples (0:11:02 elapsed time, 0:20:33 cpu time, factor 1.86) 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 Timing HOL-Data_Structures (2 threads, 528.517s elapsed time, 907.552s cpu time, 36.348s GC time, factor 1.72) 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:54 elapsed time, 0:15:14 cpu time, factor 1.71) 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 HOL-ex: theory HOL-ex.MonoidGroup HOL-ex: theory HOL-ex.Multiquote HOL-ex: theory HOL-ex.NatSum HOL-ex: theory HOL-ex.PER HOL-ex: theory HOL-ex.Peano_Axioms HOL-ex: theory HOL-ex.PresburgerEx HOL-ex: theory HOL-ex.Primrec HOL-ex: theory HOL-ex.Records HOL-ex: theory HOL-ex.Rewrite_Examples HOL-ex: theory HOL-ex.Seq HOL-ex: theory HOL-ex.Serbian 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-ex: theory HOL-ex.Unification HOL-ex: theory HOL-ex.Word_Type HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC HOL-ex: theory HOL-ex.veriT_Preprocessing HOL-ex: theory HOL-ex.Transfer_Debug HOL-ex: theory HOL-ex.Function_Growth HOL-ex: theory HOL-ex.SOS HOL-ex: theory HOL-ex.SOS_Cert HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton HOL-ex: theory HOL-ex.Argo_Examples HOL-ex: theory HOL-ex.Ballot HOL-ex: theory HOL-ex.BinEx HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml HOL-ex: theory HOL-ex.Code_Binary_Nat_examples HOL-ex: theory HOL-ex.Cubic_Quartic HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ HOL-ex: theory HOL-ex.Dedekind_Real HOL-ex: theory HOL-ex.Eval_Examples Timing HOL-Codegenerator_Test (2 threads, 502.425s elapsed time, 475.864s cpu time, 21.568s GC time, factor 0.95) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Codegenerator_Test Finished HOL-Codegenerator_Test (0:08:25 elapsed time, 0:19:59 cpu time, factor 2.37) Running HOL-Corec_Examples ... HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter 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-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor HOL-ex: theory HOL-ex.Sqrt HOL-ex: theory HOL-ex.Sqrt_Script HOL-ex: theory HOL-ex.Sum_of_Powers HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A 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-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete 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, 296.084s elapsed time, 564.960s cpu time, 64.888s GC time, factor 1.91) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples Finished HOL-Corec_Examples (0:04:58 elapsed time, 0:09:27 cpu time, factor 1.90) Running HOL-Nitpick_Examples ... HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Datatype_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Core_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Hotel_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Induct_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Integer_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mini_Nits 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-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-Nitpick_Examples: theory HOL-Nitpick_Examples.Typedef_Nits HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Nitpick_Examples HOL-ex: theory HOL-ex.Meson_Test HOL-ex: theory HOL-ex.SAT_Examples Timing HOL-ex (2 threads, 464.193s elapsed time, 847.740s cpu time, 68.808s GC time, factor 1.83) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex Finished HOL-ex (0:07:48 elapsed time, 0:14:38 cpu time, factor 1.88) 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 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec 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-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec Timing HOL-Nitpick_Examples (2 threads, 234.522s elapsed time, 145.320s cpu time, 2.952s GC time, factor 0.62) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples Finished HOL-Nitpick_Examples (0:03:56 elapsed time, 0:11:11 cpu time, factor 2.83) Running HOL-Hoare_Parallel ... HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph 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.RG_Syntax HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax 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 Timing HOL-Datatype_Examples (2 threads, 172.294s elapsed time, 337.976s cpu time, 42.516s GC time, factor 1.96) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples Finished HOL-Datatype_Examples (0:02:54 elapsed time, 0:05:40 cpu time, factor 1.94) 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.Example HOL-MicroJava: theory HOL-MicroJava.JListExample HOL-MicroJava: theory HOL-MicroJava.JTypeSafe HOL-MicroJava: theory HOL-MicroJava.TypeInf HOL-MicroJava: theory HOL-MicroJava.Effect 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.EffectMono HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError HOL-MicroJava: theory HOL-MicroJava.JVM HOL-MicroJava: theory HOL-MicroJava.BVExample HOL-MicroJava: theory HOL-MicroJava.CorrCompTp HOL-MicroJava: theory HOL-MicroJava.LBVJVM HOL-MicroJava: theory HOL-MicroJava.MicroJava Timing HOL-Hoare_Parallel (2 threads, 178.990s elapsed time, 328.204s cpu time, 9.308s 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:03:06 elapsed time, 0:05:39 cpu time, factor 1.83) 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.OO HOL-IMP: theory HOL-IMP.Com 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.Sec_Typing HOL-IMP: theory HOL-IMP.Sec_TypingT HOL-IMP: theory HOL-IMP.Sem_Equiv HOL-IMP: theory HOL-IMP.Vars HOL-IMP: theory HOL-IMP.Procs HOL-IMP: theory HOL-IMP.Def_Init HOL-IMP: theory HOL-IMP.Def_Init_Exp HOL-IMP: theory HOL-IMP.Def_Init_Big HOL-IMP: theory HOL-IMP.Fold 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-IMP: theory HOL-IMP.Collecting HOL-IMP: theory HOL-IMP.Collecting1 HOL-IMP: theory HOL-IMP.Collecting_Examples HOL-IMP: theory HOL-IMP.Star HOL-IMP: theory HOL-IMP.Compiler HOL-IMP: theory HOL-IMP.Def_Init_Small HOL-IMP: theory HOL-IMP.Small_Step HOL-IMP: theory HOL-IMP.Compiler2 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-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-MicroJava (2 threads, 175.457s elapsed time, 307.748s cpu time, 14.992s GC time, factor 1.75) 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:03:03 elapsed time, 0:05:21 cpu time, factor 1.75) 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.Quickcheck_Narrowing_Examples HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example Timing HOL-IMP (2 threads, 181.478s elapsed time, 323.668s cpu time, 24.888s GC time, factor 1.78) 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:03:09 elapsed time, 0:05:33 cpu time, factor 1.76) 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 Timing HOL-Quickcheck_Examples (2 threads, 150.087s elapsed time, 181.236s cpu time, 6.940s GC time, factor 1.21) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples Finished HOL-Quickcheck_Examples (0:02:32 elapsed time, 0:04:44 cpu time, factor 1.87) Running HOL-Predicate_Compile_Examples ... HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2 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-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-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples 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 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-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, 120.096s elapsed time, 200.612s cpu time, 14.312s GC time, factor 1.67) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples Finished HOL-Predicate_Compile_Examples (0:02:02 elapsed time, 0:05:12 cpu time, factor 2.54) 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 Timing HOL-Bali (2 threads, 134.637s elapsed time, 224.348s cpu time, 15.812s GC time, factor 1.67) 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:29 elapsed time, 0:04:07 cpu time, factor 1.65) 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.Subarray HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex Timing HOL-Imperative_HOL (2 threads, 73.954s elapsed time, 71.460s cpu time, 2.732s GC time, factor 0.97) 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:20 elapsed time, 0:04:02 cpu time, factor 3.01) Running HOL-UNITY ... HOL-UNITY: theory HOL-UNITY.UNITY HOL-UNITY: theory HOL-UNITY.ListOrder Timing HOL-Word-SMT_Examples (2 threads, 67.533s elapsed time, 91.920s cpu time, 0.960s GC time, factor 1.36) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples Finished HOL-Word-SMT_Examples (0:01:09 elapsed time, 0:01:35 cpu time, factor 1.37) Running Corec ... 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 Corec: theory Datatypes.Setup Corec: theory Corec.Corec 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.Extend HOL-UNITY: theory HOL-UNITY.Transformers HOL-UNITY: theory HOL-UNITY.Project HOL-UNITY: theory HOL-UNITY.Rename HOL-UNITY: theory HOL-UNITY.Lift_prog HOL-UNITY: theory HOL-UNITY.ELT HOL-UNITY: theory HOL-UNITY.PPROD HOL-UNITY: theory HOL-UNITY.ProgressSets 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 Corec (2 threads, 57.018s elapsed time, 84.068s cpu time, 5.828s GC time, factor 1.47) 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:01:02 elapsed time, 0:01:30 cpu time, factor 1.44) 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 Timing HOL-UNITY (2 threads, 67.325s elapsed time, 104.376s cpu time, 9.072s GC time, factor 1.55) 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:14 elapsed time, 0:01:56 cpu time, factor 1.56) Running Datatypes ... HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol Datatypes: theory Datatypes.Setup Datatypes: theory Datatypes.Datatypes Timing HOL-SET_Protocol (2 threads, 57.770s elapsed time, 98.268s cpu time, 3.232s GC time, factor 1.70) 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:01:03 elapsed time, 0:01:47 cpu time, factor 1.70) Running HOL-Probability-ex ... Timing Datatypes (2 threads, 48.294s elapsed time, 70.308s cpu time, 5.492s GC time, factor 1.46) 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:54 elapsed time, 0:01:16 cpu time, factor 1.41) Running HOL-Quotient_Examples ... 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 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-Quotient_Examples (2 threads, 34.600s elapsed time, 44.836s cpu time, 3.772s GC time, factor 1.30) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples Finished HOL-Quotient_Examples (0:00:37 elapsed time, 0:01:19 cpu time, factor 2.09) Running HOL-Analysis-ex ... HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations Timing HOL-Probability-ex (2 threads, 45.385s elapsed time, 55.448s cpu time, 1.964s 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:48 elapsed time, 0:00:57 cpu time, factor 1.18) Running HOL-Metis_Examples ... HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction 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-Analysis-ex (2 threads, 38.810s elapsed time, 47.972s cpu time, 0.712s GC time, factor 1.24) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex Finished HOL-Analysis-ex (0:00:40 elapsed time, 0:00:49 cpu time, factor 1.21) Running Tutorial ... Tutorial: theory Tutorial.ToyList_Test Tutorial: theory Tutorial.AB Tutorial: theory Tutorial.ABexpr 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.Advanced Tutorial: theory Tutorial.Fundata Tutorial: theory Tutorial.Ifexpr Tutorial: theory Tutorial.Itrev Tutorial: theory Tutorial.Mutual Tutorial: theory Tutorial.Option2 Tutorial: theory Tutorial.Plus Tutorial: theory Tutorial.Star Tutorial: theory Tutorial.ToyList Tutorial: theory Tutorial.Tree Tutorial: theory Tutorial.Trie Tutorial: theory Tutorial.Tree2 Tutorial: theory Tutorial.appendix Tutorial: theory Tutorial.case_exprs Tutorial: theory Tutorial.fakenat Tutorial: theory Tutorial.fun0 Timing HOL-Metis_Examples (2 threads, 42.171s elapsed time, 64.348s cpu time, 3.848s GC time, factor 1.53) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples Finished HOL-Metis_Examples (0:00:44 elapsed time, 0:01:22 cpu time, factor 1.85) Running HOL-Hoare ... 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.Heap HOL-Hoare: theory HOL-Hoare.Arith2 HOL-Hoare: theory HOL-Hoare.Hoare_Logic HOL-Hoare: theory HOL-Hoare.Hoare_Logic_Abort HOL-Hoare: theory HOL-Hoare.Examples HOL-Hoare: theory HOL-Hoare.HeapSyntax HOL-Hoare: theory HOL-Hoare.Pointer_Examples HOL-Hoare: theory HOL-Hoare.SchorrWaite HOL-Hoare: theory HOL-Hoare.Pointers0 HOL-Hoare: theory HOL-Hoare.ExamplesAbort HOL-Hoare: theory HOL-Hoare.HeapSyntaxAbort HOL-Hoare: theory HOL-Hoare.Pointer_ExamplesAbort HOL-Hoare: theory HOL-Hoare.SepLogHeap 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 Tutorial (2 threads, 32.180s elapsed time, 61.076s cpu time, 8.100s 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:39 elapsed time, 0:01:09 cpu time, factor 1.74) 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 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic Timing HOL-Hoare (2 threads, 25.581s elapsed time, 45.844s cpu time, 1.744s GC time, factor 1.79) 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:30 elapsed time, 0:00:54 cpu time, factor 1.78) Running HOL-Induct ... 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.Common_Patterns 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, 19.182s elapsed time, 36.528s cpu time, 6.244s GC time, factor 1.90) 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:24 elapsed time, 0:00:45 cpu time, factor 1.84) Running HOL-SPARK-Examples ... Timing HOL-Cardinals (2 threads, 22.158s elapsed time, 41.660s cpu time, 2.088s GC time, factor 1.88) 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:29 elapsed time, 0:00:53 cpu time, factor 1.81) Running HOL-Statespace ... 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-Statespace: theory HOL-Statespace.DistinctTreeProver HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification HOL-SPARK-Examples: theory HOL-SPARK-Examples.F 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.Hash 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, 19.086s elapsed time, 31.096s cpu time, 1.112s GC time, factor 1.63) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples Finished HOL-SPARK-Examples (0:00:20 elapsed time, 0:00:32 cpu time, factor 1.55) Running HOLCF-Tutorial ... Timing HOL-Statespace (2 threads, 17.097s elapsed time, 19.912s cpu time, 0.832s 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:21 elapsed time, 0:00:27 cpu time, factor 1.29) Running HOL-TLA-Memory ... HOLCF-Tutorial: theory HOLCF-Tutorial.Domain_ex HOLCF-Tutorial: theory HOLCF-Tutorial.Fixrec_ex 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-TLA-Memory: theory HOL-TLA-Memory.MemClerkParameters HOL-TLA-Memory: theory HOL-TLA-Memory.RPC HOLCF-Tutorial: theory HOLCF-Tutorial.New_Domain HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerk HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryImplementation Timing HOL-TLA-Memory (2 threads, 13.993s elapsed time, 24.632s cpu time, 0.972s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory Finished HOL-TLA-Memory (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.64) 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 Timing HOLCF-Tutorial (2 threads, 14.952s elapsed time, 19.248s cpu time, 0.768s GC time, factor 1.29) 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:19 elapsed time, 0:00:26 cpu time, factor 1.39) Running Isar_Ref ... HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeHOL HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeNumeral HOL-Matrix_LP: theory HOL-Matrix_LP.SparseMatrix 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 Isar_Ref: theory Isar_Ref.Proof_Script Isar_Ref: theory Isar_Ref.Quick_Reference Isar_Ref: theory Isar_Ref.Spec HOL-Matrix_LP: theory HOL-Matrix_LP.Cplex Isar_Ref: theory Isar_Ref.Symbols Isar_Ref: theory Isar_Ref.Synopsis Timing HOL-Matrix_LP (2 threads, 14.279s elapsed time, 27.580s cpu time, 1.472s 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:19 elapsed time, 0:00:36 cpu time, factor 1.84) 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 Codegen: theory Codegen.Foundations Codegen: theory Codegen.Refinement Timing Isar_Ref (2 threads, 10.794s elapsed time, 16.844s cpu time, 1.220s GC time, factor 1.56) 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:22 elapsed time, 0:00:28 cpu time, factor 1.30) Running IOA-NTP ... 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 Codegen (2 threads, 7.767s elapsed time, 15.248s cpu time, 0.936s GC time, factor 1.96) 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:14 elapsed time, 0:00:22 cpu time, factor 1.57) Timing IOA-NTP (2 threads, 7.541s elapsed time, 14.248s cpu time, 0.808s GC time, factor 1.89) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP Finished IOA-NTP (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.65) Running HOL-TPTP ... 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-NanoJava: theory HOL-NanoJava.Equivalence HOL-TPTP: theory HOL-TPTP.TPTP_Interpret HOL-NanoJava: theory HOL-NanoJava.Example HOL-TPTP: theory HOL-TPTP.TPTP_Proof_Reconstruction HOL-TPTP: theory HOL-TPTP.ATP_Problem_Import Timing HOL-TPTP (2 threads, 7.350s elapsed time, 8.596s cpu time, 0.400s GC time, factor 1.17) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP Finished HOL-TPTP (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.08) Running HOLCF-IMP ... HOLCF-IMP: theory HOL-IMP.AExp Timing HOL-NanoJava (2 threads, 6.497s elapsed time, 11.588s cpu time, 0.712s GC time, factor 1.78) 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:11 elapsed time, 0:00:19 cpu time, factor 1.79) Running HOL-Unix ... HOLCF-IMP: theory HOL-IMP.BExp HOL-Unix: theory HOL-Unix.Nested_Environment HOLCF-IMP: theory HOL-IMP.Com HOL-Unix: theory HOL-Unix.Unix HOLCF-IMP: theory HOL-IMP.Big_Step HOLCF-IMP: theory HOLCF-IMP.Denotational HOLCF-IMP: theory HOLCF-IMP.HoareEx Timing HOLCF-IMP (2 threads, 6.603s elapsed time, 12.428s cpu time, 0.572s GC time, factor 1.88) 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:11 elapsed time, 0:00:19 cpu time, factor 1.80) Running HOL-Mirabelle-ex ... HOL-Mirabelle-ex: theory HOL-Mirabelle-ex.Ex Timing HOL-Unix (2 threads, 6.769s elapsed time, 11.128s cpu time, 0.620s GC time, factor 1.64) 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:11 elapsed time, 0:00:19 cpu time, factor 1.64) Running Prog_Prove ... Prog_Prove: theory Prog_Prove.Bool_nat_list Prog_Prove: theory Prog_Prove.Basics Prog_Prove: theory Prog_Prove.LaTeXsugar Prog_Prove: theory Prog_Prove.Isar Prog_Prove: theory Prog_Prove.Logic Prog_Prove: theory Prog_Prove.MyList Prog_Prove: theory Prog_Prove.Types_and_funs Timing HOL-Mirabelle-ex (2 threads, 6.006s elapsed time, 0.036s 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:07 elapsed time, 0:00:09 cpu time, factor 1.22) Running HOL-Isar_Examples ... 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 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 Prog_Prove (2 threads, 6.016s elapsed time, 11.616s cpu time, 0.872s GC time, factor 1.93) 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:11 elapsed time, 0:00:17 cpu time, factor 1.53) 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 HOL-Isar_Examples (2 threads, 5.772s elapsed time, 10.748s cpu time, 0.776s GC time, factor 1.86) 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:11 elapsed time, 0:00:20 cpu time, factor 1.74) Running IOA-ABP ... IOA-ABP: theory IOA-ABP.Lemmas IOA-ABP: theory IOA-ABP.Packet IOA-ABP: theory IOA-ABP.Action Timing HOLCF-ex (2 threads, 5.426s elapsed time, 10.764s cpu time, 0.268s GC time, factor 1.98) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex Finished HOLCF-ex (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.66) Running HOL-SPARK-Manual ... IOA-ABP: theory IOA-ABP.Abschannel IOA-ABP: theory IOA-ABP.Env IOA-ABP: theory IOA-ABP.Receiver 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 IOA-ABP: theory IOA-ABP.Sender HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles IOA-ABP: theory IOA-ABP.Abschannel_finite HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference IOA-ABP: theory IOA-ABP.Impl IOA-ABP: theory IOA-ABP.Impl_finite HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification IOA-ABP: theory IOA-ABP.Spec IOA-ABP: theory IOA-ABP.Correctness Timing IOA-ABP (2 threads, 5.904s elapsed time, 10.892s cpu time, 0.340s GC time, factor 1.84) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP Finished IOA-ABP (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.59) Running HOL-ZF ... HOL-ZF: theory HOL-ZF.LProd HOL-ZF: theory HOL-ZF.HOLZF HOL-ZF: theory HOL-ZF.Zet HOL-ZF: theory HOL-ZF.MainZF HOL-ZF: theory HOL-ZF.Games Timing HOL-SPARK-Manual (2 threads, 5.350s elapsed time, 8.488s cpu time, 0.252s GC time, factor 1.59) 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:11 elapsed time, 0:00:18 cpu time, factor 1.66) Running HOL-IMPP ... HOL-IMPP: theory HOL-IMPP.Com HOL-IMPP: theory HOL-IMPP.Natural HOL-IMPP: theory HOL-IMPP.Hoare Timing HOL-ZF (2 threads, 4.564s elapsed time, 8.268s cpu time, 0.264s GC time, factor 1.81) 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:09 elapsed time, 0:00:17 cpu time, factor 1.75) Running HOLCF-FOCUS ... HOL-IMPP: theory HOL-IMPP.Misc HOL-IMPP: theory HOL-IMPP.EvenOdd HOLCF-FOCUS: theory HOLCF-FOCUS.Fstream HOLCF-FOCUS: theory HOLCF-FOCUS.Fstreams HOLCF-FOCUS: theory HOLCF-FOCUS.FOCUS HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer HOLCF-FOCUS: theory HOLCF-FOCUS.Stream_adm Timing HOL-IMPP (2 threads, 4.470s elapsed time, 7.416s cpu time, 0.276s GC time, factor 1.66) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP Finished HOL-IMPP (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.41) Running HOL-Hahn_Banach ... HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer_adm 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 Timing HOLCF-FOCUS (2 threads, 4.394s elapsed time, 8.656s cpu time, 0.320s GC time, factor 1.97) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS Finished HOLCF-FOCUS (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.60) Running Implementation ... HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach Implementation: theory Implementation.Base Implementation: theory Implementation.Eq Implementation: theory Implementation.Integration 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 Implementation: theory Implementation.Logic Timing HOL-Hahn_Banach (2 threads, 4.413s elapsed time, 8.476s cpu time, 0.284s GC time, factor 1.92) 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:10 elapsed time, 0:00:17 cpu time, factor 1.75) Running Functions ... Functions: theory Functions.Functions Timing Implementation (2 threads, 4.023s elapsed time, 6.948s cpu time, 0.120s GC time, factor 1.73) 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:10 elapsed time, 0:00:13 cpu time, factor 1.35) Running HOL-Nonstandard_Analysis-Examples ... HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes Timing Functions (2 threads, 3.298s elapsed time, 4.536s cpu time, 0.316s 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:07 elapsed time, 0:00:09 cpu time, factor 1.25) Running HOL-IOA ... HOL-IOA: theory HOL-IOA.Asig HOL-IOA: theory HOL-IOA.IOA HOL-IOA: theory HOL-IOA.Solve Timing HOL-Nonstandard_Analysis-Examples (2 threads, 3.025s elapsed time, 3.892s cpu time, 0.220s GC time, factor 1.29) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples Finished HOL-Nonstandard_Analysis-Examples (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.06) Running HOL-TLA-Inc ... HOL-TLA-Inc: theory HOL-TLA-Inc.Inc Timing HOL-IOA (2 threads, 2.778s elapsed time, 4.064s cpu time, 0.192s GC time, factor 1.46) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA Finished HOL-IOA (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.19) Running HOL-Lattice ... HOL-Lattice: theory HOL-Lattice.Orders Timing HOL-TLA-Inc (2 threads, 2.425s elapsed time, 4.224s cpu time, 0.172s GC time, factor 1.74) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc Finished HOL-TLA-Inc (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.33) Running Classes ... HOL-Lattice: theory HOL-Lattice.Bounds HOL-Lattice: theory HOL-Lattice.Lattice Classes: theory Classes.Setup HOL-Lattice: theory HOL-Lattice.CompleteLattice Classes: theory Classes.Classes Timing HOL-Lattice (2 threads, 2.095s elapsed time, 3.660s cpu time, 0.000s GC time, factor 1.75) 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:06 elapsed time, 0:00:11 cpu time, factor 1.75) Running IOA-Storage ... IOA-Storage: theory IOA-Storage.Action Timing Classes (2 threads, 2.032s elapsed time, 2.416s cpu time, 0.000s GC time, factor 1.19) 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:06 elapsed time, 0:00:07 cpu time, factor 1.13) Running Eisbach ... IOA-Storage: theory IOA-Storage.Impl IOA-Storage: theory IOA-Storage.Spec IOA-Storage: theory IOA-Storage.Correctness Eisbach: theory Eisbach.Base Eisbach: theory Eisbach.Preface Eisbach: theory Eisbach.Manual Timing IOA-Storage (2 threads, 1.609s elapsed time, 2.380s cpu time, 0.000s GC time, factor 1.48) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage Finished IOA-Storage (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.08) Running Main ... Main: theory Main.Main_Doc Timing Eisbach (2 threads, 1.681s elapsed time, 2.204s cpu time, 0.000s GC time, factor 1.31) 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:06 elapsed time, 0:00:07 cpu time, factor 1.17) Timing Main (2 threads, 1.333s elapsed time, 1.424s cpu time, 0.000s GC time, factor 1.07) 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:05 cpu time, factor 1.13) Running Locales ... Running HOL-Import ... HOL-Import: theory HOL-Import.Import_Setup Locales: theory Locales.Examples HOL-Import: theory HOL-Import.HOL_Light_Maps Locales: theory Locales.Examples1 Locales: theory Locales.Examples2 Locales: theory Locales.Examples3 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE) Timing HOL-Import (2 threads, 0.977s elapsed time, 1.756s cpu time, 0.000s GC time, factor 1.80) 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 ... Sugar: theory HOL-Library.LaTeXsugar Sugar: theory HOL-Library.OptionalSugar Sugar: theory Sugar.Sugar Timing Locales (2 threads, 1.313s elapsed time, 2.388s cpu time, 0.000s GC time, factor 1.82) 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:07 cpu time, factor 1.29) Running HOL-Types_To_Sets ... HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces Timing Sugar (2 threads, 0.939s elapsed time, 1.056s cpu time, 0.000s GC time, factor 1.12) 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:05 cpu time, factor 1.12) Running IOA-ex ... IOA-ex: theory IOA-ex.TrivEx2 IOA-ex: theory IOA-ex.TrivEx Timing HOL-Types_To_Sets (2 threads, 0.926s elapsed time, 1.472s cpu time, 0.000s GC time, factor 1.59) 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 HOL-Mutabelle ... HOL-Mutabelle: theory HOL-Mutabelle.MutabelleExtra Timing IOA-ex (2 threads, 0.803s elapsed time, 1.704s cpu time, 0.000s GC time, factor 2.12) 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-TLA-Buffer ... HOL-TLA-Buffer: theory HOL-TLA-Buffer.Buffer HOL-TLA-Buffer: theory HOL-TLA-Buffer.DBuffer Timing HOL-Mutabelle (2 threads, 0.638s elapsed time, 0.740s cpu time, 0.000s GC time, factor 1.16) 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 ... Timing HOL-TLA-Buffer (2 threads, 0.600s elapsed time, 1.116s cpu time, 0.000s GC time, factor 1.86) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer Finished HOL-TLA-Buffer (0:00:02 elapsed time) Running HOL-Prolog ... JEdit: theory JEdit.Base JEdit: theory JEdit.JEdit 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.347s elapsed time, 0.544s cpu time, 0.000s GC time, factor 1.57) Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog Finished HOL-Prolog (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.367s elapsed time, 0.528s cpu time, 0.000s GC time, factor 1.44) 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:04 elapsed time, 0:00:04 cpu time, factor 1.16) Running Typeclass_Hierarchy ... Typeclass_Hierarchy: theory Typeclass_Hierarchy.Typeclass_Hierarchy Timing JEdit (2 threads, 0.586s elapsed time, 0.644s cpu time, 0.000s GC time, factor 1.10) 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:11 elapsed time, 0:00:12 cpu time, factor 1.05) Timing Typeclass_Hierarchy (2 threads, 0.258s elapsed time, 0.368s cpu time, 0.000s GC time, factor 1.43) 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:05 elapsed time, 0:00:05 cpu time, factor 1.12) 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 HOL-Proofs FAILED (see also /media/data/jenkins/workspace/isabelle-repo-makeall/heaps/polyml-5.7.1_x86_64-linux/log/HOL-Proofs) ### Value identifier (s) has not been referenced. ### ML warning (line 192 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (used) has not been referenced. ### ML warning (line 159 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 165 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 186 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (U) has not been referenced. ### ML warning (line 186 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (Ts) has not been referenced. ### ML warning (line 204 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (induct) has not been referenced. ### ML warning (line 227 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 228 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 243 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 325 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 340 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 348 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 367 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 384 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 392 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 407 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 431 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. signature INDUCTIVE_REALIZER = sig val add_ind_realizers: string -> string list -> theory -> theory end structure InductiveRealizer: INDUCTIVE_REALIZER ### theory "HOL-Library.Realizers" ### 3.002s elapsed time, 3.340s cpu time, 0.000s GC time HOL-Proofs-Lambda CANCELLED HOL-Proofs-Extraction CANCELLED HOL-Proofs-ex CANCELLED Unfinished session(s): HOL-Proofs, HOL-Proofs-Extraction, HOL-Proofs-Lambda, HOL-Proofs-ex === TIMING === Group main: 0:38:15 elapsed time, 1:06:24 cpu time, factor 1.74 Group doc: 0:04:54 elapsed time, 0:06:50 cpu time, factor 1.39 Group timing: 3:45:17 elapsed time, 3:25:33 cpu time, factor 0.91 Overall: 1:59:08 elapsed time, 4:31:31 cpu time, factor 2.28 === FAILED SESSIONS === Session HOL-Proofs-ex: CANCELLED Session HOL-Proofs: FAILED 143 Session HOL-Proofs-Extraction: CANCELLED Session HOL-Proofs-Lambda: CANCELLED Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: ABORTED