Skip to content
Success

Console Output

21:31:16 Started by upstream project "isabelle-repo" build number 950

21:31:16 originally caused by:

21:31:16 Started by an SCM change

21:31:16 [EnvInject] - Loading node environment variables.

21:31:16 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

21:31:16 [isabelle-repo-makeall] $ hg showconfig paths.default

21:31:16 [isabelle-repo-makeall] $ hg pull --rev 3804a9640088520c0e781dc1a1f1aae016a640c0

21:31:17 pulling from http://isabelle.in.tum.de/repos/isabelle/

21:31:17 searching for changes

21:31:17 adding changesets

21:31:17 adding manifests

21:31:17 adding file changes

21:31:17 added 1 changesets with 1 changes to 1 files

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

21:31:17 [isabelle-repo-makeall] $ hg update --clean --rev 3804a9640088520c0e781dc1a1f1aae016a640c0

21:31:17 1 files updated, 0 files merged, 0 files removed, 0 files unresolved

21:31:17 [isabelle-repo-makeall] $ hg log --rev . --template {node}

21:31:17 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

21:31:17 [isabelle-repo-makeall] $ hg id --branch

21:31:17 No emails were triggered.

21:31:17 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson2749393596781910858.sh

21:31:17 + Admin/jenkins/run_build makeall

21:31:17 + set -e

21:31:17 + PROFILE=makeall

21:31:17 + shift

21:31:17 + bin/isabelle components -a

21:31:17 + bin/isabelle jedit -bf

21:31:17 ### Building Isabelle/Scala ...

21:31:49 ### Building Isabelle/jEdit ...

21:32:04 + bin/isabelle ci_build_makeall

21:32:08

21:32:08 === CONFIGURATION ===

21:32:08

21:32:08 ISABELLE_BUILD_OPTIONS=""

21:32:08

21:32:08 ML_PLATFORM="x86_64-linux"

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

21:32:08 ML_SYSTEM="polyml-5.6"

21:32:08 ML_OPTIONS="-H 4000 --maxheap 8G"

21:32:08

21:32:08 === BUILD ===

21:32:08

21:32:08 Build started at Fri, 9 Jun 2017 19:32:08 GMT

21:32:08 Isabelle id 3804a9640088

21:32:08

21:32:08 === LOG ===

21:32:08

21:32:08 Session Pure/Pure

21:32:09 Session CCL/CCL

21:32:09 Session CTT/CTT

21:32:09 Session Cube/Cube

21:32:09 Session FOL/FOL

21:32:09 Session FOL/FOL-ex

21:32:09 Session FOLP/FOLP

21:32:09 Session FOLP/FOLP-ex

21:32:09 Session HOL/HOL (main)

21:32:10 Session Doc/Classes (doc)

21:32:10 Session Doc/Functions (doc)

21:32:10 Session HOL/HOL-Eisbach

21:32:10 Session Doc/Eisbach (doc)

21:32:10 Session HOL/HOL-Hoare

21:32:10 Session HOL/HOL-Hoare_Parallel (timing)

21:32:10 Session HOL/HOL-IMPP

21:32:10 Session HOL/HOL-IOA

21:32:10 Session HOL/HOL-Import

21:32:10 Session HOL/HOL-Lattice

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

21:32:10 Session Doc/Codegen_Basics

21:32:10 Session Doc/Codegen (doc)

21:32:10 Session Doc/Datatypes (doc)

21:32:10 Session Doc/Corec (doc)

21:32:10 Session HOL/HOL-Auth (timing)

21:32:11 Session HOL/HOL-UNITY (timing)

21:32:11 Session HOL/HOL-Bali (timing)

21:32:11 Session HOL/HOL-Cardinals (timing)

21:32:11 Session HOL/HOL-Computational_Algebra (timing)

21:32:11 Session HOL/HOL-Algebra (main timing)

21:32:11 Session HOL/HOL-Decision_Procs (timing)

21:32:11 Session HOL/HOL-Quotient_Examples (timing)

21:32:11 Session HOL/HOL-Analysis (main timing)

21:32:12 Session HOL/HOL-Analysis-ex

21:32:12 Session HOL/HOL-Probability (main timing)

21:32:12 Session HOL/HOL-Probability-ex (timing)

21:32:12 Session HOL/HOL-Isar_Examples

21:32:12 Session HOL/HOL-Nonstandard_Analysis (timing)

21:32:12 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

21:32:12 Session HOL/HOL-Number_Theory (timing)

21:32:12 Session HOL/HOL-Data_Structures (timing)

21:32:12 Session HOL/HOL-Corec_Examples (timing)

21:32:12 Session HOL/HOL-Datatype_Examples (timing)

21:32:12 Session HOL/HOL-Hahn_Banach

21:32:12 Session HOL/HOL-IMP (timing)

21:32:13 Session HOL/HOL-Imperative_HOL

21:32:13 Session HOL/HOL-Induct

21:32:13 Session HOL/HOL-Matrix_LP

21:32:13 Session HOL/HOL-Metis_Examples (timing)

21:32:13 Session HOL/HOL-MicroJava (timing)

21:32:13 Session HOL/HOL-Mutabelle

21:32:13 Session HOL/HOL-Nitpick_Examples

21:32:13 Session HOL/HOL-Predicate_Compile_Examples (timing)

21:32:13 Session HOL/HOL-Quickcheck_Examples (timing)

21:32:13 Session HOL/HOL-SET_Protocol (timing)

21:32:13 Session HOL/HOL-TPTP

21:32:13 Session HOL/HOL-Unix

21:32:13 Session HOL/HOL-ZF

21:32:13 Session HOL/HOL-ex (timing)

21:32:13 Session HOL/HOL-Codegenerator_Test

21:32:13 Session Doc/Isar_Ref (doc)

21:32:13 Session Doc/Typeclass_Hierarchy_Basics

21:32:13 Session Doc/Typeclass_Hierarchy (doc)

21:32:13 Session HOL/HOL-Mirabelle

21:32:14 Session HOL/HOL-Mirabelle-ex

21:32:14 Session HOL/HOL-NanoJava

21:32:14 Session HOL/HOL-Nominal

21:32:14 Session HOL/HOL-Nominal-Examples (timing)

21:32:14 Session HOL/HOL-Nunchaku

21:32:14 Session HOL/HOL-Prolog

21:32:14 Session HOL/HOL-Statespace

21:32:14 Session HOL/HOL-TLA

21:32:14 Session HOL/HOL-TLA-Buffer

21:32:14 Session HOL/HOL-TLA-Inc

21:32:14 Session HOL/HOL-TLA-Memory

21:32:14 Session HOL/HOL-Types_To_Sets

21:32:14 Session HOL/HOL-Word (main timing)

21:32:14 Session HOL/HOL-SPARK (main)

21:32:14 Session HOL/HOL-SPARK-Examples

21:32:14 Session HOL/HOL-SPARK-Manual

21:32:14 Session HOL/HOL-Word-Examples

21:32:14 Session HOL/HOL-Word-SMT_Examples (timing)

21:32:14 Session HOL/HOLCF (main timing)

21:32:14 Session HOL/HOLCF-IMP

21:32:14 Session HOL/HOLCF-Library

21:32:14 Session HOL/HOLCF-FOCUS

21:32:15 Session HOL/HOLCF-ex

21:32:15 Session HOL/HOLCF-Tutorial

21:32:15 Session HOL/IOA (timing)

21:32:15 Session HOL/IOA-ABP

21:32:15 Session HOL/IOA-NTP

21:32:15 Session HOL/IOA-Storage

21:32:15 Session HOL/IOA-ex

21:32:15 Session Doc/How_to_Prove_it

21:32:15 Session Doc/Implementation (doc)

21:32:15 Session Doc/JEdit (doc)

21:32:15 Session Doc/Locales (doc)

21:32:15 Session Doc/Main (doc)

21:32:15 Session Doc/Prog_Prove (doc)

21:32:15 Session Doc/Sugar (doc)

21:32:15 Session Doc/Tutorial (doc)

21:32:15 Session HOL/HOL-Proofs (timing)

21:32:15 Session HOL/HOL-Proofs-Extraction (timing)

21:32:16 Session HOL/HOL-Proofs-Lambda (timing)

21:32:16 Session HOL/HOL-Proofs-ex

21:32:16 Session Doc/Intro (doc)

21:32:16 Session LCF/LCF

21:32:16 Session Doc/Logics (doc)

21:32:16 Session Doc/Nitpick (doc)

21:32:16 Session Unsorted/SML

21:32:16 Session Sequents/Sequents

21:32:16 Session Doc/Sledgehammer (doc)

21:32:16 Session Unsorted/Spec_Check

21:32:16 Session Doc/System (doc)

21:32:16 Session ZF/ZF (main timing ZF)

21:32:16 Session Doc/Logics_ZF (doc)

21:32:16 Session ZF/ZF-AC (ZF)

21:32:16 Session ZF/ZF-Coind (ZF)

21:32:16 Session ZF/ZF-Constructible (ZF)

21:32:16 Session ZF/ZF-IMP (ZF)

21:32:16 Session ZF/ZF-Induct (ZF)

21:32:16 Session ZF/ZF-UNITY (timing ZF)

21:32:16 Session ZF/ZF-Resid (ZF)

21:32:16 Session ZF/ZF-ex (ZF)

21:32:17 Cleaning Pure ...

21:32:17 Cleaning SML ...

21:32:17 Cleaning Sequents ...

21:32:17 Cleaning Sledgehammer ...

21:32:17 Cleaning Spec_Check ...

21:32:17 Cleaning System ...

21:32:17 Cleaning ZF ...

21:32:17 Cleaning ZF-AC ...

21:32:17 Cleaning ZF-Coind ...

21:32:17 Cleaning ZF-Constructible ...

21:32:17 Cleaning ZF-IMP ...

21:32:17 Cleaning ZF-Induct ...

21:32:17 Cleaning ZF-UNITY ...

21:32:17 Cleaning ZF-Resid ...

21:32:17 Cleaning ZF-ex ...

21:32:17 Cleaning Nitpick ...

21:32:17 Cleaning Logics_ZF ...

21:32:17 Cleaning Logics ...

21:32:17 Cleaning LCF ...

21:32:17 Cleaning Intro ...

21:32:17 Cleaning HOL-Proofs ...

21:32:17 Cleaning HOL-Proofs-Extraction ...

21:32:17 Cleaning HOL-Proofs-Lambda ...

21:32:17 Cleaning HOL-Proofs-ex ...

21:32:17 Cleaning HOL ...

21:32:17 Cleaning HOL-Data_Structures ...

21:32:17 Cleaning HOL-Eisbach ...

21:32:17 Cleaning HOL-Hoare ...

21:32:17 Cleaning HOL-Hoare_Parallel ...

21:32:17 Cleaning HOL-IMPP ...

21:32:17 Cleaning HOL-IOA ...

21:32:17 Cleaning HOL-Import ...

21:32:17 Cleaning HOL-Lattice ...

21:32:17 Cleaning HOL-Library ...

21:32:17 Cleaning HOL-Auth ...

21:32:17 Cleaning HOL-UNITY ...

21:32:17 Cleaning HOL-Bali ...

21:32:17 Cleaning HOL-Cardinals ...

21:32:17 Cleaning HOL-Computational_Algebra ...

21:32:17 Cleaning HOL-Algebra ...

21:32:17 Cleaning HOL-Decision_Procs ...

21:32:17 Cleaning HOL-Quotient_Examples ...

21:32:17 Cleaning HOL-Analysis ...

21:32:17 Cleaning HOL-Analysis-ex ...

21:32:17 Cleaning HOL-Probability ...

21:32:17 Cleaning HOL-Probability-ex ...

21:32:17 Cleaning HOL-Isar_Examples ...

21:32:17 Cleaning HOL-Nonstandard_Analysis ...

21:32:17 Cleaning HOL-Nonstandard_Analysis-Examples ...

21:32:17 Cleaning HOL-Number_Theory ...

21:32:17 Cleaning HOL-Codegenerator_Test ...

21:32:17 Cleaning HOL-Corec_Examples ...

21:32:17 Cleaning HOL-Datatype_Examples ...

21:32:17 Cleaning HOL-Hahn_Banach ...

21:32:17 Cleaning HOL-IMP ...

21:32:17 Cleaning HOL-Imperative_HOL ...

21:32:17 Cleaning HOL-Induct ...

21:32:17 Cleaning HOL-Matrix_LP ...

21:32:17 Cleaning HOL-Metis_Examples ...

21:32:17 Cleaning HOL-MicroJava ...

21:32:17 Cleaning HOL-Mutabelle ...

21:32:17 Cleaning HOL-Nitpick_Examples ...

21:32:17 Cleaning HOL-Predicate_Compile_Examples ...

21:32:17 Cleaning HOL-Quickcheck_Examples ...

21:32:17 Cleaning HOL-SET_Protocol ...

21:32:17 Cleaning HOL-TPTP ...

21:32:17 Cleaning HOL-Unix ...

21:32:17 Cleaning HOL-ZF ...

21:32:17 Cleaning HOL-ex ...

21:32:17 Cleaning Isar_Ref ...

21:32:17 Cleaning Typeclass_Hierarchy_Basics ...

21:32:17 Cleaning Typeclass_Hierarchy ...

21:32:17 Cleaning HOL-Mirabelle ...

21:32:17 Cleaning HOL-Mirabelle-ex ...

21:32:17 Cleaning HOL-NanoJava ...

21:32:17 Cleaning HOL-Nominal ...

21:32:17 Cleaning HOL-Nominal-Examples ...

21:32:17 Cleaning HOL-Nunchaku ...

21:32:17 Cleaning HOL-Prolog ...

21:32:17 Cleaning HOL-Statespace ...

21:32:17 Cleaning HOL-TLA ...

21:32:17 Cleaning HOL-TLA-Buffer ...

21:32:17 Cleaning HOL-TLA-Inc ...

21:32:17 Cleaning HOL-TLA-Memory ...

21:32:17 Cleaning HOL-Types_To_Sets ...

21:32:17 Cleaning HOL-Word ...

21:32:17 Cleaning HOL-SPARK ...

21:32:17 Cleaning HOL-SPARK-Examples ...

21:32:17 Cleaning HOL-SPARK-Manual ...

21:32:17 Cleaning HOL-Word-Examples ...

21:32:17 Cleaning HOL-Word-SMT_Examples ...

21:32:17 Cleaning HOLCF ...

21:32:17 Cleaning HOLCF-IMP ...

21:32:17 Cleaning HOLCF-Library ...

21:32:17 Cleaning HOLCF-FOCUS ...

21:32:17 Cleaning HOLCF-ex ...

21:32:17 Cleaning HOLCF-Tutorial ...

21:32:17 Cleaning IOA ...

21:32:17 Cleaning IOA-ABP ...

21:32:17 Cleaning IOA-NTP ...

21:32:17 Cleaning IOA-Storage ...

21:32:17 Cleaning IOA-ex ...

21:32:17 Cleaning How_to_Prove_it ...

21:32:17 Cleaning Implementation ...

21:32:17 Cleaning JEdit ...

21:32:17 Cleaning Locales ...

21:32:17 Cleaning Main ...

21:32:17 Cleaning Prog_Prove ...

21:32:17 Cleaning Sugar ...

21:32:17 Cleaning Tutorial ...

21:32:17 Cleaning Functions ...

21:32:17 Cleaning FOLP ...

21:32:17 Cleaning FOLP-ex ...

21:32:17 Cleaning FOL ...

21:32:17 Cleaning FOL-ex ...

21:32:17 Cleaning Eisbach ...

21:32:17 Cleaning Datatypes ...

21:32:17 Cleaning Cube ...

21:32:17 Cleaning Corec ...

21:32:17 Cleaning Codegen_Basics ...

21:32:17 Cleaning Codegen ...

21:32:17 Cleaning Classes ...

21:32:17 Cleaning CTT ...

21:32:17 Cleaning CCL ...

21:32:17 Building Pure ...

21:32:31 Pure: theory Pure

21:32:32 Pure: theory ML_Bootstrap

21:32:35 Warning: missing document directory

21:32:35 Timing Pure (1 threads, 0.624s elapsed time, 0.624s cpu time, 0.000s GC time, factor 1.00)

21:32:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

21:32:35 Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00)

21:32:35 Building HOL ...

21:32:35 Building ZF ...

21:32:35 Building HOL-Proofs ...

21:32:35 ZF: theory IFOL

21:32:36 HOL-Proofs: theory HOL.Code_Generator

21:32:36 HOL: theory HOL.Code_Generator

21:32:36 ZF: theory FOL

21:32:38 ZF: theory ZF.ZF_Base

21:32:38 ZF: theory ZF.upair

21:32:38 ZF: theory ZF.pair

21:32:39 ZF: theory ZF.Bool

21:32:39 ZF: theory ZF.equalities

21:32:39 HOL-Proofs: theory HOL.HOL

21:32:39 HOL: theory HOL.HOL

21:32:39 ZF: theory ZF.Fixedpt

21:32:39 ZF: theory ZF.Sum

21:32:39 ZF: theory ZF.func

21:32:40 ZF: theory ZF.Perm

21:32:40 ZF: theory ZF.QPair

21:32:40 ZF: theory ZF.Trancl

21:32:40 ZF: theory ZF.EquivClass

21:32:40 ZF: theory ZF.WF

21:32:41 ZF: theory ZF.Order

21:32:41 ZF: theory ZF.Ordinal

21:32:41 ZF: theory ZF.OrdQuant

21:32:41 ZF: theory ZF.OrderArith

21:32:41 ZF: theory ZF.Nat_ZF

21:32:41 ZF: theory ZF.Epsilon

21:32:41 ZF: theory ZF.OrderType

21:32:42 ZF: theory ZF.Inductive_ZF

21:32:42 ZF: theory ZF.Finite

21:32:42 ZF: theory ZF.Cardinal

21:32:42 ZF: theory ZF.Univ

21:32:43 HOL: theory HOL.Argo

21:32:43 HOL: theory HOL.Ctr_Sugar

21:32:43 ZF: theory ZF.Arith

21:32:43 ZF: theory ZF.QUniv

21:32:43 ZF: theory ZF.Datatype_ZF

21:32:43 HOL-Proofs: theory HOL.Argo

21:32:43 HOL-Proofs: theory HOL.Ctr_Sugar

21:32:43 ZF: theory ZF.ArithSimp

21:32:44 ZF: theory ZF.Int_ZF

21:32:44 ZF: theory ZF.CardinalArith

21:32:44 HOL: theory HOL.Orderings

21:32:44 ZF: theory ZF.List_ZF

21:32:44 HOL-Proofs: theory HOL.Orderings

21:32:44 ZF: theory ZF.Bin

21:32:45 HOL-Proofs: theory HOL.SAT

21:32:45 HOL: theory HOL.SAT

21:32:45 ZF: theory ZF.IntDiv_ZF

21:32:46 HOL: theory HOL.Groups

21:32:46 ZF: theory ZF

21:32:46 ZF: theory ZF.AC

21:32:46 ZF: theory ZF.Zorn

21:32:46 ZF: theory ZF.Cardinal_AC

21:32:46 ZF: theory ZF.InfDatatype

21:32:46 ZF: theory ZFC

21:32:47 HOL-Proofs: theory HOL.Groups

21:32:49 HOL: theory HOL.Lattices

21:32:51 HOL: theory HOL.Set

21:32:51 HOL-Proofs: theory HOL.Lattices

21:32:52 HOL: theory HOL.Fun

21:32:53 HOL: theory HOL.Typedef

21:32:53 HOL: theory HOL.Rings

21:32:53 HOL: theory HOL.Complete_Lattices

21:32:55 HOL-Proofs: theory HOL.Set

21:32:56 HOL: theory HOL.Inductive

21:32:58 HOL: theory HOL.Product_Type

21:33:00 HOL: theory HOL.Complete_Partial_Order

21:33:00 HOL: theory HOL.Sum_Type

21:33:01 HOL-Proofs: theory HOL.Fun

21:33:03 HOL-Proofs: theory HOL.Typedef

21:33:03 HOL-Proofs: theory HOL.Rings

21:33:04 HOL-Proofs: theory HOL.Complete_Lattices

21:33:05 HOL: theory HOL.Nat

21:33:07 HOL: theory HOL.Fields

21:33:07 HOL: theory HOL.Meson

21:33:08 HOL: theory HOL.ATP

21:33:09 HOL-Proofs: theory HOL.Inductive

21:33:10 HOL: theory HOL.Metis

21:33:11 HOL-Proofs: theory HOL.Product_Type

21:33:12 Timing ZF (2 threads, 22.725s elapsed time, 40.672s cpu time, 5.304s GC time, factor 1.79)

21:33:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF

21:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf

21:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf

21:33:12 Finished ZF (0:00:36 elapsed time, 0:01:03 cpu time, factor 1.75)

21:33:12 Building ZF-Induct ...

21:33:12 ZF-Induct: theory ZF-Induct.Binary_Trees

21:33:12 ZF-Induct: theory ZF-Induct.Acc

21:33:12 ZF-Induct: theory ZF-Induct.Comb

21:33:12 ZF-Induct: theory ZF-Induct.Datatypes

21:33:12 ZF-Induct: theory ZF-Induct.FoldSet

21:33:13 ZF-Induct: theory ZF-Induct.ListN

21:33:13 HOL: theory HOL.Finite_Set

21:33:13 ZF-Induct: theory ZF-Induct.Mutil

21:33:13 ZF-Induct: theory ZF-Induct.Multiset

21:33:13 ZF-Induct: theory ZF-Induct.Ntree

21:33:13 ZF-Induct: theory ZF-Induct.Primrec

21:33:13 ZF-Induct: theory ZF-Induct.PropLog

21:33:13 ZF-Induct: theory ZF-Induct.Rmap

21:33:13 ZF-Induct: theory ZF-Induct.Term

21:33:14 ZF-Induct: theory ZF-Induct.Tree_Forest

21:33:14 ZF-Induct: theory ZF-Induct.Brouwer

21:33:14 HOL-Proofs: theory HOL.Complete_Partial_Order

21:33:14 HOL: theory HOL.Relation

21:33:15 HOL-Proofs: theory HOL.Sum_Type

21:33:15 HOL: theory HOL.Transitive_Closure

21:33:17 HOL: theory HOL.Wellfounded

21:33:17 HOL: theory HOL.Fun_Def_Base

21:33:17 HOL: theory HOL.Hilbert_Choice

21:33:18 HOL: theory HOL.Wfrec

21:33:18 HOL: theory HOL.Order_Relation

21:33:18 HOL: theory HOL.BNF_Wellorder_Relation

21:33:18 HOL: theory HOL.Zorn

21:33:18 HOL: theory HOL.BNF_Wellorder_Embedding

21:33:19 HOL: theory HOL.BNF_Wellorder_Constructions

21:33:19 HOL: theory HOL.BNF_Cardinal_Order_Relation

21:33:19 HOL-Proofs: theory HOL.Nat

21:33:20 HOL: theory HOL.BNF_Cardinal_Arithmetic

21:33:21 HOL: theory HOL.BNF_Def

21:33:23 HOL: theory HOL.BNF_Composition

21:33:23 HOL: theory HOL.Basic_BNFs

21:33:24 HOL: theory HOL.BNF_Fixpoint_Base

21:33:24 HOL-Proofs: theory HOL.Fields

21:33:24 HOL-Proofs: theory HOL.Meson

21:33:24 HOL-Proofs: theory HOL.ATP

21:33:25 Timing ZF-Induct (2 threads, 6.884s elapsed time, 11.376s cpu time, 0.464s GC time, factor 1.65)

21:33:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

21:33:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

21:33:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

21:33:25 Finished ZF-Induct (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.60)

21:33:25 Building FOL ...

21:33:25 FOL: theory IFOL

21:33:26 FOL: theory FOL

21:33:27 HOL-Proofs: theory HOL.Metis

21:33:27 HOL: theory HOL.BNF_Least_Fixpoint

21:33:29 HOL: theory HOL.Basic_BNF_LFPs

21:33:29 HOL: theory HOL.Transfer

21:33:30 HOL: theory HOL.Num

21:33:31 Timing FOL (2 threads, 2.869s elapsed time, 3.260s cpu time, 0.220s GC time, factor 1.14)

21:33:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL

21:33:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf

21:33:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf

21:33:31 Finished FOL (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.27)

21:33:31 Building FOLP ...

21:33:32 FOLP: theory IFOLP

21:33:32 HOL-Proofs: theory HOL.Finite_Set

21:33:32 FOLP: theory FOLP

21:33:33 HOL: theory HOL.Power

21:33:33 Timing FOLP (2 threads, 0.926s elapsed time, 0.932s cpu time, 0.000s GC time, factor 1.01)

21:33:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP

21:33:33 Finished FOLP (0:00:01 elapsed time)

21:33:33 Running ZF-Constructible ...

21:33:34 ZF-Constructible: theory ZF-Constructible.Formula

21:33:34 ZF-Constructible: theory ZF-Constructible.MetaExists

21:33:34 ZF-Constructible: theory ZF-Constructible.Normal

21:33:34 ZF-Constructible: theory ZF-Constructible.Reflection

21:33:35 ZF-Constructible: theory ZF-Constructible.Relative

21:33:36 HOL: theory HOL.Groups_Big

21:33:36 ZF-Constructible: theory ZF-Constructible.L_axioms

21:33:36 ZF-Constructible: theory ZF-Constructible.Wellorderings

21:33:37 ZF-Constructible: theory ZF-Constructible.WFrec

21:33:37 ZF-Constructible: theory ZF-Constructible.WF_absolute

21:33:38 ZF-Constructible: theory ZF-Constructible.Datatype_absolute

21:33:38 ZF-Constructible: theory ZF-Constructible.Rank

21:33:38 HOL: theory HOL.Equiv_Relations

21:33:39 HOL: theory HOL.Lifting

21:33:39 ZF-Constructible: theory ZF-Constructible.Separation

21:33:39 ZF-Constructible: theory ZF-Constructible.Internalize

21:33:39 ZF-Constructible: theory ZF-Constructible.AC_in_L

21:33:40 HOL-Proofs: theory HOL.Relation

21:33:40 HOL: theory HOL.Lifting_Set

21:33:40 HOL: theory HOL.Option

21:33:41 ZF-Constructible: theory ZF-Constructible.Rec_Separation

21:33:41 ZF-Constructible: theory ZF-Constructible.Rank_Separation

21:33:41 HOL: theory HOL.Extraction

21:33:41 ZF-Constructible: theory ZF-Constructible.Satisfies_absolute

21:33:42 HOL: theory HOL.Lattices_Big

21:33:42 ZF-Constructible: theory ZF-Constructible.DPow_absolute

21:33:43 HOL-Proofs: theory HOL.Transitive_Closure

21:33:43 HOL: theory HOL.Partial_Function

21:33:44 HOL: theory HOL.Fun_Def

21:33:44 HOL: theory HOL.Quotient

21:33:46 HOL: theory HOL.Int

21:33:47 HOL-Proofs: theory HOL.Wellfounded

21:33:48 HOL: theory HOL.Nat_Transfer

21:33:49 HOL: theory HOL.Euclidean_Division

21:33:50 HOL-Proofs: theory HOL.Fun_Def_Base

21:33:50 HOL-Proofs: theory HOL.Hilbert_Choice

21:33:52 HOL-Proofs: theory HOL.Wfrec

21:33:52 HOL-Proofs: theory HOL.Order_Relation

21:33:53 HOL: theory HOL.Parity

21:33:53 HOL-Proofs: theory HOL.BNF_Wellorder_Relation

21:33:53 HOL-Proofs: theory HOL.Zorn

21:33:54 Timing ZF-Constructible (2 threads, 16.154s elapsed time, 30.360s cpu time, 5.548s GC time, factor 1.88)

21:33:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

21:33:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

21:33:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

21:33:54 Finished ZF-Constructible (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.84)

21:33:54 Running ZF-UNITY ...

21:33:54 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding

21:33:54 ZF-UNITY: theory ZF-UNITY.MultisetSum

21:33:54 ZF-UNITY: theory ZF-UNITY.GenPrefix

21:33:55 ZF-UNITY: theory ZF-UNITY.State

21:33:55 ZF-UNITY: theory ZF-UNITY.UNITY

21:33:55 ZF-UNITY: theory ZF-UNITY.Monotonicity

21:33:55 HOL: theory HOL.Divides

21:33:55 ZF-UNITY: theory ZF-UNITY.Constrains

21:33:55 ZF-UNITY: theory ZF-UNITY.FP

21:33:55 ZF-UNITY: theory ZF-UNITY.WFair

21:33:55 ZF-UNITY: theory ZF-UNITY.Increasing

21:33:56 ZF-UNITY: theory ZF-UNITY.SubstAx

21:33:56 ZF-UNITY: theory ZF-UNITY.Follows

21:33:56 ZF-UNITY: theory ZF-UNITY.Mutex

21:33:56 ZF-UNITY: theory ZF-UNITY.Union

21:33:57 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions

21:33:57 ZF-UNITY: theory ZF-UNITY.Comp

21:33:57 ZF-UNITY: theory ZF-UNITY.Guar

21:33:57 ZF-UNITY: theory ZF-UNITY.AllocBase

21:33:58 ZF-UNITY: theory ZF-UNITY.ClientImpl

21:33:58 ZF-UNITY: theory ZF-UNITY.Distributor

21:33:58 ZF-UNITY: theory ZF-UNITY.Merge

21:33:58 ZF-UNITY: theory ZF-UNITY.AllocImpl

21:34:02 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation

21:34:03 HOL: theory HOL.Code_Numeral

21:34:03 HOL: theory HOL.Numeral_Simprocs

21:34:04 HOL: theory HOL.SMT

21:34:04 HOL: theory HOL.Semiring_Normalization

21:34:06 HOL: theory HOL.Set_Interval

21:34:06 HOL: theory HOL.Groebner_Basis

21:34:06 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic

21:34:08 HOL-Proofs: theory HOL.BNF_Def

21:34:08 HOL: theory HOL.Conditionally_Complete_Lattices

21:34:09 HOL: theory HOL.Filter

21:34:10 HOL: theory HOL.Presburger

21:34:11 Timing ZF-UNITY (2 threads, 16.233s elapsed time, 28.700s cpu time, 1.132s GC time, factor 1.77)

21:34:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

21:34:11 Finished ZF-UNITY (0:00:16 elapsed time, 0:00:29 cpu time, factor 1.74)

21:34:11 Running ZF-ex ...

21:34:11 ZF-ex: theory ZF-ex.CoUnit

21:34:11 ZF-ex: theory ZF-ex.BinEx

21:34:12 ZF-ex: theory ZF-ex.Commutation

21:34:12 ZF-ex: theory ZF-ex.Group

21:34:12 ZF-ex: theory ZF-ex.LList

21:34:12 ZF-ex: theory ZF-ex.Limit

21:34:12 HOL: theory HOL.Sledgehammer

21:34:12 ZF-ex: theory ZF-ex.Ring

21:34:13 ZF-ex: theory ZF-ex.NatSum

21:34:13 ZF-ex: theory ZF-ex.Primes

21:34:13 ZF-ex: theory ZF-ex.Ramsey

21:34:13 ZF-ex: theory ZF-ex.misc

21:34:14 HOL: theory HOL.List

21:34:14 HOL-Proofs: theory HOL.BNF_Composition

21:34:14 HOL-Proofs: theory HOL.Basic_BNFs

21:34:16 HOL-Proofs: theory HOL.BNF_Fixpoint_Base

21:34:19 HOL-Proofs: theory HOL.BNF_Least_Fixpoint

21:34:22 HOL-Proofs: theory HOL.Basic_BNF_LFPs

21:34:22 HOL-Proofs: theory HOL.Transfer

21:34:22 HOL: theory HOL.Groups_List

21:34:22 HOL: theory HOL.Map

21:34:23 HOL: theory HOL.Factorial

21:34:23 HOL: theory HOL.GCD

21:34:23 Timing ZF-ex (2 threads, 11.326s elapsed time, 16.148s cpu time, 0.740s GC time, factor 1.43)

21:34:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

21:34:23 Finished ZF-ex (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.40)

21:34:23 Running ZF-AC ...

21:34:23 HOL: theory HOL.Binomial

21:34:23 ZF-AC: theory ZF-AC.AC_Equiv

21:34:24 ZF-AC: theory ZF-AC.AC18_AC19

21:34:24 ZF-AC: theory ZF-AC.AC7_AC9

21:34:24 ZF-AC: theory ZF-AC.Cardinal_aux

21:34:24 ZF-AC: theory ZF-AC.Hartog

21:34:24 ZF-AC: theory ZF-AC.HH

21:34:24 ZF-AC: theory ZF-AC.WO6_WO1

21:34:24 HOL: theory HOL.Enum

21:34:24 HOL-Proofs: theory HOL.Num

21:34:24 ZF-AC: theory ZF-AC.AC16_lemmas

21:34:24 ZF-AC: theory ZF-AC.AC16_WO4

21:34:24 ZF-AC: theory ZF-AC.DC

21:34:24 ZF-AC: theory ZF-AC.AC15_WO6

21:34:25 ZF-AC: theory ZF-AC.AC17_AC1

21:34:25 ZF-AC: theory ZF-AC.WO1_AC

21:34:25 ZF-AC: theory ZF-AC.WO1_WO7

21:34:25 ZF-AC: theory ZF-AC.WO2_AC16

21:34:27 HOL: theory HOL.String

21:34:28 HOL: theory HOL.BNF_Greatest_Fixpoint

21:34:28 HOL-Proofs: theory HOL.Power

21:34:30 HOL: theory HOL.Predicate

21:34:31 HOL: theory HOL.Lazy_Sequence

21:34:32 HOL: theory HOL.Typerep

21:34:32 Timing ZF-AC (2 threads, 5.788s elapsed time, 10.040s cpu time, 0.576s GC time, factor 1.73)

21:34:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

21:34:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

21:34:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

21:34:32 Finished ZF-AC (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.63)

21:34:32 Running FOL-ex ...

21:34:32 FOL-ex: theory FOL-ex.If

21:34:32 FOL-ex: theory FOL-ex.Classical

21:34:32 HOL: theory HOL.Limited_Sequence

21:34:32 FOL-ex: theory FOL-ex.Intro

21:34:32 FOL-ex: theory FOL-ex.Miniscope

21:34:32 FOL-ex: theory FOL-ex.Nat

21:34:32 FOL-ex: theory FOL-ex.Nat_Class

21:34:32 FOL-ex: theory FOL-ex.Natural_Numbers

21:34:32 FOL-ex: theory FOL-ex.Prolog

21:34:32 HOL-Proofs: theory HOL.Groups_Big

21:34:32 HOL: theory HOL.Random

21:34:32 FOL-ex: theory FOL-ex.Propositional_Cla

21:34:32 FOL-ex: theory FOL-ex.Quantifiers_Cla

21:34:32 FOL-ex: theory FOL-ex.Foundation

21:34:32 FOL-ex: theory FOL-ex.Intuitionistic

21:34:32 FOL-ex: theory FOL-ex.Propositional_Int

21:34:33 FOL-ex: theory FOL-ex.Quantifiers_Int

21:34:33 HOL: theory HOL.Code_Evaluation

21:34:34 HOL: theory HOL.Quickcheck_Random

21:34:35 FOL-ex: theory FOL-ex.Locale_Test1

21:34:37 HOL: theory HOL.Quickcheck_Exhaustive

21:34:37 HOL: theory HOL.Quickcheck_Narrowing

21:34:38 FOL-ex: theory FOL-ex.Locale_Test2

21:34:38 FOL-ex: theory FOL-ex.Locale_Test3

21:34:38 FOL-ex: theory FOL-ex.Locale_Test

21:34:40 HOL-Proofs: theory HOL.Equiv_Relations

21:34:40 Timing FOL-ex (2 threads, 5.766s elapsed time, 8.316s cpu time, 0.272s GC time, factor 1.44)

21:34:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

21:34:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

21:34:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

21:34:40 Finished FOL-ex (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.44)

21:34:40 Running CCL ...

21:34:41 CCL: theory IFOL

21:34:41 HOL: theory HOL.Random_Pred

21:34:41 HOL: theory HOL.Record

21:34:41 CCL: theory FOL

21:34:42 HOL: theory HOL.Random_Sequence

21:34:42 HOL: theory HOL.Predicate_Compile

21:34:43 HOL-Proofs: theory HOL.Lifting

21:34:43 HOL: theory HOL.Nitpick

21:34:43 CCL: theory CCL.Set

21:34:44 CCL: theory CCL.Lfp

21:34:44 CCL: theory CCL.Gfp

21:34:44 CCL: theory CCL.CCL

21:34:44 CCL: theory CCL.Term

21:34:44 CCL: theory CCL.Trancl

21:34:44 CCL: theory CCL.Type

21:34:44 CCL: theory CCL.Fix

21:34:45 CCL: theory CCL.Hered

21:34:45 CCL: theory CCL.Wfd

21:34:45 CCL: theory CCL.Nat

21:34:45 CCL: theory CCL.List

21:34:45 CCL: theory CCL.Flag

21:34:46 CCL: theory CCL.Stream

21:34:46 HOL-Proofs: theory HOL.Lifting_Set

21:34:46 Timing CCL (2 threads, 5.233s elapsed time, 7.668s cpu time, 0.168s GC time, factor 1.47)

21:34:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL

21:34:46 Finished CCL (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.41)

21:34:46 Running Sequents ...

21:34:47 Sequents: theory Sequents.Sequents

21:34:47 Sequents: theory Sequents.ILL

21:34:47 Sequents: theory Sequents.LK0

21:34:47 Sequents: theory Sequents.ILL_predlog

21:34:47 Sequents: theory Sequents.Washing

21:34:47 Sequents: theory Sequents.LK

21:34:47 Sequents: theory Sequents.Modal0

21:34:47 Sequents: theory Sequents.S4

21:34:47 Sequents: theory Sequents.Hard_Quantifiers

21:34:47 Sequents: theory Sequents.Nat

21:34:47 Sequents: theory Sequents.Propositional

21:34:47 HOL-Proofs: theory HOL.Option

21:34:47 Sequents: theory Sequents.Quantifiers

21:34:47 Sequents: theory Sequents.S43

21:34:47 Sequents: theory Sequents.T

21:34:48 HOL-Proofs: theory HOL.Quotient

21:34:49 HOL-Proofs: theory HOL.Extraction

21:34:49 HOL: theory Main

21:34:51 Timing Sequents (2 threads, 3.652s elapsed time, 7.032s cpu time, 0.136s GC time, factor 1.93)

21:34:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

21:34:51 Finished Sequents (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.83)

21:34:51 Running FOLP-ex ...

21:34:51 HOL: theory HOL.Archimedean_Field

21:34:51 HOL: theory HOL.Topological_Spaces

21:34:51 FOLP-ex: theory FOLP-ex.Classical

21:34:51 FOLP-ex: theory FOLP-ex.If

21:34:51 FOLP-ex: theory FOLP-ex.Intro

21:34:51 FOLP-ex: theory FOLP-ex.Nat

21:34:51 HOL-Proofs: theory HOL.Lattices_Big

21:34:52 FOLP-ex: theory FOLP-ex.Propositional_Cla

21:34:52 FOLP-ex: theory FOLP-ex.Quantifiers_Cla

21:34:52 FOLP-ex: theory FOLP-ex.Foundation

21:34:52 FOLP-ex: theory FOLP-ex.Intuitionistic

21:34:53 HOL-Proofs: theory HOL.Partial_Function

21:34:53 FOLP-ex: theory FOLP-ex.Propositional_Int

21:34:54 FOLP-ex: theory FOLP-ex.Quantifiers_Int

21:34:56 Timing FOLP-ex (2 threads, 3.637s elapsed time, 6.216s cpu time, 0.104s GC time, factor 1.71)

21:34:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex

21:34:56 Finished FOLP-ex (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.62)

21:34:56 Running LCF ...

21:34:56 LCF: theory IFOL

21:34:56 HOL: theory HOL.Rat

21:34:57 LCF: theory FOL

21:34:58 LCF: theory LCF.LCF

21:34:59 HOL: theory HOL.Real

21:34:59 LCF: theory LCF.Ex1

21:34:59 LCF: theory LCF.Ex2

21:34:59 LCF: theory LCF.Ex3

21:34:59 LCF: theory LCF.Ex4

21:34:59 Timing LCF (2 threads, 3.041s elapsed time, 3.312s cpu time, 0.180s GC time, factor 1.09)

21:34:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

21:34:59 Finished LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.06)

21:34:59 Running Spec_Check ...

21:34:59 Spec_Check: theory Spec_Check.Spec_Check

21:34:59 Spec_Check: theory Spec_Check.Examples

21:35:00 HOL-Proofs: theory HOL.Fun_Def

21:35:01 HOL: theory HOL.Real_Vector_Spaces

21:35:02 Warning: missing document directory

21:35:02 Timing Spec_Check (2 threads, 1.896s elapsed time, 3.380s cpu time, 0.012s GC time, factor 1.78)

21:35:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

21:35:02 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

21:35:02 Running ZF-Resid ...

21:35:02 ZF-Resid: theory ZF-Resid.Redex

21:35:02 ZF-Resid: theory ZF-Resid.Substitution

21:35:02 HOL-Proofs: theory HOL.Int

21:35:02 ZF-Resid: theory ZF-Resid.Residuals

21:35:03 ZF-Resid: theory ZF-Resid.Reduction

21:35:03 ZF-Resid: theory ZF-Resid.Confluence

21:35:04 Timing ZF-Resid (2 threads, 1.568s elapsed time, 2.620s cpu time, 0.000s GC time, factor 1.67)

21:35:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

21:35:04 Finished ZF-Resid (0:00:01 elapsed time)

21:35:04 Running ZF-IMP ...

21:35:04 ZF-IMP: theory ZF-IMP.Com

21:35:04 ZF-IMP: theory ZF-IMP.Denotation

21:35:04 ZF-IMP: theory ZF-IMP.Equiv

21:35:05 Timing ZF-IMP (2 threads, 1.086s elapsed time, 1.292s cpu time, 0.000s GC time, factor 1.19)

21:35:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

21:35:05 Finished ZF-IMP (0:00:01 elapsed time)

21:35:05 Running CTT ...

21:35:05 CTT: theory CTT.CTT

21:35:06 CTT: theory CTT.Elimination

21:35:06 CTT: theory CTT.Equality

21:35:06 CTT: theory CTT.Synthesis

21:35:06 CTT: theory CTT.Typechecking

21:35:08 Timing CTT (2 threads, 0.807s elapsed time, 1.140s cpu time, 0.000s GC time, factor 1.41)

21:35:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

21:35:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

21:35:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

21:35:08 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)

21:35:08 Running ZF-Coind ...

21:35:08 ZF-Coind: theory ZF-Coind.Language

21:35:08 ZF-Coind: theory ZF-Coind.Map

21:35:08 ZF-Coind: theory ZF-Coind.Types

21:35:08 ZF-Coind: theory ZF-Coind.Values

21:35:08 HOL-Proofs: theory HOL.Nat_Transfer

21:35:08 ZF-Coind: theory ZF-Coind.Dynamic

21:35:08 ZF-Coind: theory ZF-Coind.Static

21:35:08 ZF-Coind: theory ZF-Coind.ECR

21:35:09 Timing ZF-Coind (2 threads, 0.656s elapsed time, 1.288s cpu time, 0.000s GC time, factor 1.96)

21:35:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

21:35:09 Finished ZF-Coind (0:00:00 elapsed time)

21:35:09 Running System ...

21:35:09 System: theory System.Base

21:35:09 System: theory System.Environment

21:35:09 System: theory System.Misc

21:35:09 System: theory System.Presentation

21:35:09 System: theory System.Scala

21:35:09 System: theory System.Sessions

21:35:10 HOL-Proofs: theory HOL.Euclidean_Division

21:35:12 Timing System (2 threads, 0.293s elapsed time, 0.388s cpu time, 0.000s GC time, factor 1.32)

21:35:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

21:35:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

21:35:12 Finished System (0:00:02 elapsed time)

21:35:12 Running Cube ...

21:35:12 Cube: theory Cube.Cube

21:35:12 Cube: theory Cube.Example

21:35:12 Timing Cube (2 threads, 0.284s elapsed time, 0.292s cpu time, 0.000s GC time, factor 1.03)

21:35:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

21:35:12 Finished Cube (0:00:00 elapsed time)

21:35:12 Running Intro ...

21:35:13 HOL: theory HOL.Inequalities

21:35:13 HOL: theory HOL.Limits

21:35:15 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

21:35:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

21:35:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

21:35:15 Finished Intro (0:00:02 elapsed time)

21:35:15 Running Logics ...

21:35:15 HOL-Proofs: theory HOL.Parity

21:35:17 HOL: theory HOL.Deriv

21:35:17 HOL: theory HOL.Series

21:35:18 Timing Logics (2 threads, 0.001s elapsed time, 0.004s cpu time, 0.000s GC time, factor 6.42)

21:35:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics

21:35:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf

21:35:18 Finished Logics (0:00:02 elapsed time)

21:35:18 Running Logics_ZF ...

21:35:18 HOL-Proofs: theory HOL.Divides

21:35:18 Logics_ZF: theory Logics_ZF.FOL_examples

21:35:18 Logics_ZF: theory Logics_ZF.If

21:35:18 Logics_ZF: theory Logics_ZF.ZF_Isar

21:35:18 Logics_ZF: theory Logics_ZF.ZF_examples

21:35:18 Logics_ZF: theory Logics_ZF.IFOL_examples

21:35:18 HOL: theory HOL.NthRoot

21:35:19 HOL: theory HOL.Transcendental

21:35:21 Timing Logics_ZF (2 threads, 0.273s elapsed time, 0.544s cpu time, 0.000s GC time, factor 1.99)

21:35:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

21:35:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

21:35:21 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)

21:35:21 Running Nitpick ...

21:35:24 HOL: theory HOL.Complex

21:35:24 HOL: theory HOL.MacLaurin

21:35:24 Timing Nitpick (2 threads, 0.001s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

21:35:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

21:35:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

21:35:24 Finished Nitpick (0:00:02 elapsed time)

21:35:24 Running SML ...

21:35:24 SML: theory SML.Examples

21:35:25 Warning: missing document directory

21:35:25 Timing SML (2 threads, 0.012s elapsed time, 0.012s cpu time, 0.000s GC time, factor 1.04)

21:35:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

21:35:25 Finished SML (0:00:00 elapsed time)

21:35:25 Running Sledgehammer ...

21:35:26 HOL: theory Complex_Main

21:35:27 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

21:35:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

21:35:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

21:35:27 Finished Sledgehammer (0:00:02 elapsed time)

21:35:41 HOL-Proofs: theory HOL.Code_Numeral

21:35:46 HOL-Proofs: theory HOL.Numeral_Simprocs

21:35:47 HOL-Proofs: theory HOL.SMT

21:35:49 HOL-Proofs: theory HOL.Semiring_Normalization

21:35:52 HOL-Proofs: theory HOL.Groebner_Basis

21:35:53 HOL-Proofs: theory HOL.Set_Interval

21:36:06 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices

21:36:06 HOL-Proofs: theory HOL.Filter

21:36:12 HOL-Proofs: theory HOL.Presburger

21:36:25 HOL-Proofs: theory HOL.Sledgehammer

21:36:27 HOL-Proofs: theory HOL.List

21:37:31 HOL-Proofs: theory HOL.Groups_List

21:37:33 HOL-Proofs: theory HOL.Factorial

21:37:35 HOL-Proofs: theory HOL.Binomial

21:37:57 HOL-Proofs: theory HOL.GCD

21:38:22 HOL-Proofs: theory HOL.Map

21:38:26 HOL-Proofs: theory HOL.Enum

21:38:58 Timing HOL (2 threads, 272.407s elapsed time, 515.828s cpu time, 57.768s GC time, factor 1.89)

21:38:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL

21:38:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf

21:38:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf

21:38:58 Finished HOL (0:06:22 elapsed time, 0:11:34 cpu time, factor 1.82)

21:39:00 Building HOL-Library ...

21:39:00 Building HOLCF ...

21:39:02 HOLCF: theory HOLCF.Nat_Bijection

21:39:02 HOLCF: theory HOLCF.Old_Datatype

21:39:03 HOL-Library: theory HOL-Library.Preorder

21:39:03 HOL-Library: theory HOL-Library.Adhoc_Overloading

21:39:03 HOL-Library: theory HOL-Library.Lattice_Syntax

21:39:03 HOL-Library: theory HOL-Library.AList

21:39:03 HOL-Library: theory HOL-Library.BNF_Axiomatization

21:39:03 HOL-Library: theory HOL-Library.BNF_Corec

21:39:04 HOLCF: theory HOLCF.Countable

21:39:05 HOL-Library: theory HOL-Library.DAList

21:39:06 HOLCF: theory HOLCF.Porder

21:39:06 HOL-Library: theory HOL-Library.Bit

21:39:06 HOLCF: theory HOLCF.Pcpo

21:39:07 HOL-Library: theory HOL-Library.Boolean_Algebra

21:39:07 HOL-Library: theory HOL-Library.Cancellation

21:39:08 HOLCF: theory HOLCF.Cont

21:39:08 HOL-Library: theory HOL-Library.Multiset

21:39:09 HOLCF: theory HOLCF.Adm

21:39:09 HOLCF: theory HOLCF.Discrete

21:39:09 HOLCF: theory HOLCF.Cpodef

21:39:10 HOLCF: theory HOLCF.Fun_Cpo

21:39:10 HOLCF: theory HOLCF.Product_Cpo

21:39:10 HOLCF: theory HOLCF.Cfun

21:39:10 HOL-Library: theory HOL-Library.Cardinal_Notations

21:39:10 HOL-Library: theory HOL-Library.Char_ord

21:39:11 HOL-Library: theory HOL-Library.Code_Abstract_Nat

21:39:11 HOL-Library: theory HOL-Library.Code_Binary_Nat

21:39:11 HOL-Library: theory HOL-Library.Code_Target_Nat

21:39:11 HOLCF: theory HOLCF.Cprod

21:39:11 HOLCF: theory HOLCF.Completion

21:39:11 HOL-Library: theory HOL-Library.Code_Char

21:39:11 HOLCF: theory HOLCF.Deflation

21:39:12 HOL-Library: theory HOL-Library.Code_Prolog

21:39:12 HOLCF: theory HOLCF.Fix

21:39:12 HOLCF: theory HOLCF.Sfun

21:39:12 HOLCF: theory HOLCF.Sprod

21:39:12 HOLCF: theory HOLCF.Up

21:39:12 HOL-Library: theory HOL-Library.Code_Target_Int

21:39:12 HOL-Library: theory HOL-Library.Code_Target_Numeral

21:39:12 HOL-Library: theory HOL-Library.Code_Test

21:39:13 HOLCF: theory HOLCF.Lift

21:39:13 HOL-Proofs: theory HOL.Random

21:39:13 HOLCF: theory HOLCF.One

21:39:13 HOLCF: theory HOLCF.Tr

21:39:13 HOL-Library: theory HOL-Library.Combine_PER

21:39:13 HOLCF: theory HOLCF.Ssum

21:39:14 HOL-Library: theory HOL-Library.Complete_Partial_Order2

21:39:14 HOLCF: theory HOLCF.Fixrec

21:39:14 HOLCF: theory HOLCF.Map_Functions

21:39:14 HOL-Library: theory HOL-Library.DAList_Multiset

21:39:15 HOLCF: theory HOLCF.Bifinite

21:39:15 HOL-Library: theory HOL-Library.Multiset_Order

21:39:15 HOL-Library: theory HOL-Library.Permutation

21:39:15 HOLCF: theory HOLCF.Domain_Aux

21:39:16 HOL-Library: theory HOL-Library.Debug

21:39:16 HOL-Library: theory HOL-Library.Disjoint_Sets

21:39:16 HOL-Proofs: theory HOL.String

21:39:16 HOL-Library: theory HOL-Library.Permutations

21:39:16 HOLCF: theory HOLCF.Universal

21:39:17 HOL-Library: theory HOL-Library.Dlist

21:39:17 HOL-Library: theory HOL-Library.FSet

21:39:18 HOLCF: theory HOLCF.Algebraic

21:39:18 HOLCF: theory HOLCF.Compact_Basis

21:39:18 HOLCF: theory HOLCF.LowerPD

21:39:18 HOL-Library: theory HOL-Library.Fun_Lexorder

21:39:18 HOLCF: theory HOLCF.UpperPD

21:39:18 HOL-Library: theory HOL-Library.FuncSet

21:39:19 HOLCF: theory HOLCF.Representable

21:39:19 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint

21:39:19 HOL-Library: theory HOL-Library.Function_Algebras

21:39:19 HOLCF: theory HOLCF.ConvexPD

21:39:19 HOL-Library: theory HOL-Library.Function_Division

21:39:19 HOL-Library: theory HOL-Library.Groups_Big_Fun

21:39:20 HOL-Library: theory HOL-Library.IArray

21:39:21 HOL-Library: theory HOL-Library.Finite_Map

21:39:21 HOL-Library: theory HOL-Library.Infinite_Set

21:39:22 HOL-Library: theory HOL-Library.Omega_Words_Fun

21:39:22 HOLCF: theory HOLCF.Domain

21:39:22 HOL-Library: theory HOL-Library.Ramsey

21:39:22 HOL-Library: theory HOL-Library.LaTeXsugar

21:39:23 HOL-Library: theory HOL-Library.Lattice_Constructions

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

21:39:24 HOLCF: theory HOLCF.Powerdomains

21:39:24 HOL-Proofs: theory HOL.Predicate

21:39:24 HOL-Library: theory HOL-Library.List_lexord

21:39:24 HOL-Library: theory HOL-Library.Mapping

21:39:25 HOLCF: theory HOLCF

21:39:25 HOL-Library: theory HOL-Library.AList_Mapping

21:39:25 HOL-Library: theory HOL-Library.Monad_Syntax

21:39:26 HOL-Library: theory HOL-Library.More_List

21:39:26 HOL-Library: theory HOL-Library.Nat_Bijection

21:39:26 HOL-Library: theory HOL-Library.Old_Datatype

21:39:26 HOL-Library: theory HOL-Library.Stream

21:39:27 HOL-Proofs: theory HOL.Lazy_Sequence

21:39:27 HOL-Library: theory HOL-Library.Old_Recdef

21:39:28 HOL-Library: theory HOL-Library.Option_ord

21:39:28 HOL-Proofs: theory HOL.Limited_Sequence

21:39:28 HOL-Library: theory HOL-Library.Parallel

21:39:28 HOL-Library: theory HOL-Library.Perm

21:39:29 HOL-Proofs: theory HOL.Typerep

21:39:29 HOL-Library: theory HOL-Library.Phantom_Type

21:39:30 HOL-Library: theory HOL-Library.Cardinality

21:39:30 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

21:39:30 HOL-Proofs: theory HOL.Code_Evaluation

21:39:30 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

21:39:30 HOL-Library: theory HOL-Library.Product_Lexorder

21:39:31 HOL-Library: theory HOL-Library.Product_Plus

21:39:31 HOL-Library: theory HOL-Library.Product_Order

21:39:31 HOL-Library: theory HOL-Library.Numeral_Type

21:39:31 HOL-Library: theory HOL-Library.Finite_Lattice

21:39:32 HOL-Proofs: theory HOL.Quickcheck_Random

21:39:32 HOL-Library: theory HOL-Library.Type_Length

21:39:32 HOL-Library: theory HOL-Library.Saturated

21:39:33 HOL-Library: theory HOL-Library.Quotient_Syntax

21:39:33 HOL-Library: theory HOL-Library.Quotient_Option

21:39:33 HOL-Library: theory HOL-Library.Quotient_Product

21:39:33 HOL-Library: theory HOL-Library.Quotient_Set

21:39:33 HOL-Library: theory HOL-Library.Quotient_List

21:39:34 HOL-Library: theory HOL-Library.Quotient_Sum

21:39:34 HOL-Library: theory HOL-Library.Quotient_Type

21:39:34 HOL-Library: theory HOL-Library.RBT_Impl

21:39:35 HOL-Proofs: theory HOL.Quickcheck_Exhaustive

21:39:35 HOL-Library: theory HOL-Library.Reflection

21:39:35 HOL-Library: theory HOL-Library.Refute

21:39:36 HOL-Library: theory HOL-Library.Rewrite

21:39:36 HOL-Library: theory HOL-Library.Set_Algebras

21:39:36 HOL-Library: theory HOL-Library.Simps_Case_Conv

21:39:37 HOL-Library: theory HOL-Library.Extended

21:39:39 HOL-Library: theory HOL-Library.State_Monad

21:39:39 HOL-Library: theory HOL-Library.Stirling

21:39:40 HOL-Library: theory HOL-Library.Sublist

21:39:41 HOL-Library: theory HOL-Library.Prefix_Order

21:39:41 HOL-Library: theory HOL-Library.Subseq_Order

21:39:41 HOL-Proofs: theory HOL.Record

21:39:41 HOL-Library: theory HOL-Library.Transitive_Closure_Table

21:39:42 HOL-Library: theory HOL-Library.Tree

21:39:44 HOL-Proofs: theory HOL.Nitpick

21:39:46 HOL-Library: theory HOL-Library.Tree_Multiset

21:39:46 HOL-Library: theory HOL-Library.While_Combinator

21:39:47 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

21:39:47 HOL-Library: theory HOL-Library.Countable

21:39:49 HOL-Library: theory HOL-Library.Countable_Set

21:39:50 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

21:39:51 HOL-Proofs: theory HOL.Quickcheck_Narrowing

21:39:51 Timing HOLCF (2 threads, 22.663s elapsed time, 41.004s cpu time, 2.212s GC time, factor 1.81)

21:39:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF

21:39:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

21:39:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

21:39:51 Finished HOLCF (0:00:50 elapsed time, 0:01:23 cpu time, factor 1.64)

21:39:52 Building IOA ...

21:39:53 HOL-Library: theory HOL-Library.Countable_Set_Type

21:39:54 IOA: theory IOA.Asig

21:39:54 IOA: theory IOA.Seq

21:39:55 IOA: theory IOA.Automata

21:39:55 HOL-Library: theory HOL-Library.BigO

21:39:56 IOA: theory IOA.Sequence

21:39:56 IOA: theory IOA.Pred

21:39:56 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

21:39:57 IOA: theory IOA.Traces

21:39:57 IOA: theory IOA.TL

21:39:57 HOL-Library: theory HOL-Library.Diagonal_Subsequence

21:39:57 HOL-Library: theory HOL-Library.Discrete

21:39:57 HOL-Proofs: theory HOL.Random_Pred

21:39:58 HOL-Library: theory HOL-Library.Function_Growth

21:39:58 IOA: theory IOA.CompoExecs

21:39:58 IOA: theory IOA.RefMappings

21:39:58 IOA: theory IOA.RefCorrectness

21:39:58 HOL-Proofs: theory HOL.Random_Sequence

21:39:58 IOA: theory IOA.CompoScheds

21:39:59 IOA: theory IOA.Simulations

21:39:59 IOA: theory IOA.SimCorrectness

21:39:59 HOL-Library: theory HOL-Library.Indicator_Function

21:39:59 HOL-Proofs: theory HOL.Predicate_Compile

21:39:59 IOA: theory IOA.Deadlock

21:39:59 HOL-Library: theory HOL-Library.Lattice_Algebras

21:39:59 IOA: theory IOA.ShortExecutions

21:40:00 IOA: theory IOA.CompoTraces

21:40:01 IOA: theory IOA.Compositionality

21:40:01 IOA: theory IOA.IOA

21:40:02 IOA: theory IOA.TLS

21:40:02 HOL-Proofs: theory Main

21:40:02 IOA: theory IOA.LiveIOA

21:40:03 IOA: theory IOA.Abstraction

21:40:04 HOL-Proofs: theory HOL-Library.Old_Datatype

21:40:06 HOL-Library: theory HOL-Library.Liminf_Limsup

21:40:07 HOL-Library: theory HOL-Library.Log_Nat

21:40:07 HOL-Library: theory HOL-Library.Float

21:40:09 HOL-Library: theory HOL-Library.RBT

21:40:10 HOL-Library: theory HOL-Library.Lub_Glb

21:40:10 HOL-Library: theory HOL-Library.RBT_Mapping

21:40:10 HOL-Library: theory HOL-Library.RBT_Set

21:40:10 HOL-Library: theory HOL-Library.Multiset_Permutations

21:40:11 HOL-Library: theory HOL-Library.Nonpos_Ints

21:40:11 HOL-Library: theory HOL-Library.OptionalSugar

21:40:11 HOL-Library: theory HOL-Library.Order_Continuity

21:40:12 HOL-Library: theory HOL-Library.Periodic_Fun

21:40:12 HOL-Library: theory HOL-Library.Quadratic_Discriminant

21:40:12 HOL-Library: theory HOL-Library.Sum_of_Squares

21:40:12 HOL-Library: theory HOL-Library.Extended_Nat

21:40:13 HOL-Library: theory HOL-Library.Extended_Real

21:40:15 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

21:40:18 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

21:40:20 HOL-Library: theory HOL-Library.Library

21:40:30 Timing IOA (2 threads, 17.260s elapsed time, 32.928s cpu time, 1.116s GC time, factor 1.91)

21:40:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA

21:40:30 Finished IOA (0:00:37 elapsed time, 0:01:02 cpu time, factor 1.65)

21:40:30 Building HOL-Word ...

21:40:32 HOL-Word: theory HOL-Word.Bits

21:40:32 HOL-Word: theory HOL-Word.Bit

21:40:32 HOL-Word: theory HOL-Word.Boolean_Algebra

21:40:33 HOL-Word: theory HOL-Word.Misc_Numeric

21:40:33 HOL-Word: theory HOL-Word.Bits_Bit

21:40:33 HOL-Word: theory HOL-Word.Bit_Representation

21:40:33 HOL-Word: theory HOL-Word.Word_Miscellaneous

21:40:34 HOL-Word: theory HOL-Word.Bits_Int

21:40:34 HOL-Word: theory HOL-Word.Misc_Typedef

21:40:34 HOL-Word: theory HOL-Word.Phantom_Type

21:40:35 HOL-Word: theory HOL-Word.Cardinality

21:40:35 HOL-Word: theory HOL-Word.Bool_List_Representation

21:40:36 HOL-Word: theory HOL-Word.Numeral_Type

21:40:37 HOL-Word: theory HOL-Word.Type_Length

21:40:37 HOL-Word: theory HOL-Word.Word

21:41:18 Timing HOL-Word (2 threads, 22.591s elapsed time, 44.232s cpu time, 1.804s GC time, factor 1.96)

21:41:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word

21:41:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf

21:41:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf

21:41:18 Finished HOL-Word (0:00:47 elapsed time, 0:01:21 cpu time, factor 1.74)

21:41:18 Building HOL-TLA ...

21:41:20 HOL-TLA: theory HOL-TLA.Intensional

21:41:20 HOL-TLA: theory HOL-TLA.Stfun

21:41:20 HOL-TLA: theory HOL-TLA.Action

21:41:21 HOL-TLA: theory HOL-TLA.Init

21:41:21 HOL-TLA: theory HOL-TLA.TLA

21:41:36 Timing HOL-TLA (2 threads, 2.031s elapsed time, 3.060s cpu time, 0.000s GC time, factor 1.51)

21:41:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA

21:41:36 Finished HOL-TLA (0:00:17 elapsed time, 0:00:25 cpu time, factor 1.45)

21:41:36 Building HOLCF-Library ...

21:41:39 HOLCF-Library: theory HOLCF-Library.Infinite_Set

21:41:39 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

21:41:39 HOLCF-Library: theory HOLCF-Library.Char_Discrete

21:41:39 HOLCF-Library: theory HOLCF-Library.Countable_Set

21:41:39 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

21:41:40 HOLCF-Library: theory HOLCF-Library.Countable_Complete_Lattices

21:41:40 HOLCF-Library: theory HOLCF-Library.Int_Discrete

21:41:40 HOLCF-Library: theory HOLCF-Library.List_Cpo

21:41:41 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

21:41:41 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

21:41:42 HOLCF-Library: theory HOLCF-Library.List_Predomain

21:41:43 HOLCF-Library: theory HOLCF-Library.Option_Cpo

21:41:43 HOLCF-Library: theory HOLCF-Library.Order_Continuity

21:41:43 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

21:41:44 HOLCF-Library: theory HOLCF-Library.Extended_Nat

21:41:45 HOLCF-Library: theory HOLCF-Library.Stream

21:41:47 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

21:42:11 Timing HOLCF-Library (2 threads, 15.498s elapsed time, 30.572s cpu time, 1.096s GC time, factor 1.97)

21:42:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library

21:42:11 Finished HOLCF-Library (0:00:35 elapsed time, 0:00:59 cpu time, factor 1.68)

21:42:12 Building HOL-SPARK ...

21:42:14 HOL-SPARK: theory HOL-SPARK.Bit_Comparison

21:42:14 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

21:42:16 HOL-SPARK: theory SPARK

21:42:31 Timing HOL-SPARK (2 threads, 2.537s elapsed time, 4.276s cpu time, 0.136s GC time, factor 1.69)

21:42:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK

21:42:31 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:27 cpu time, factor 1.45)

21:42:31 Building HOL-Nominal ...

21:42:33 HOL-Nominal: theory HOL-Nominal.Infinite_Set

21:42:33 HOL-Nominal: theory HOL-Nominal.Old_Datatype

21:42:34 HOL-Nominal: theory HOL-Nominal.Nominal

21:42:57 Timing HOL-Nominal (2 threads, 8.533s elapsed time, 16.748s cpu time, 0.772s GC time, factor 1.96)

21:42:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal

21:42:57 Finished HOL-Nominal (0:00:26 elapsed time, 0:00:42 cpu time, factor 1.63)

21:42:57 Building HOL-Eisbach ...

21:42:59 HOL-Eisbach: theory HOL-Eisbach.Eisbach

21:42:59 HOL-Eisbach: theory IFOL

21:43:00 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

21:43:00 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

21:43:00 HOL-Eisbach: theory HOL-Eisbach.Examples

21:43:00 HOL-Eisbach: theory HOL-Eisbach.Tests

21:43:01 HOL-Eisbach: theory FOL

21:43:02 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

21:43:16 Warning: missing document directory

21:43:16 Timing HOL-Eisbach (2 threads, 3.407s elapsed time, 6.320s cpu time, 0.172s GC time, factor 1.85)

21:43:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

21:43:16 Finished HOL-Eisbach (0:00:18 elapsed time, 0:00:28 cpu time, factor 1.51)

21:43:17 Building HOL-Mirabelle ...

21:43:18 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle

21:43:19 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test

21:43:32 Timing HOL-Mirabelle (2 threads, 0.600s elapsed time, 0.656s cpu time, 0.000s GC time, factor 1.09)

21:43:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

21:43:32 Finished HOL-Mirabelle (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.42)

21:43:32 Running HOL-Nominal-Examples ...

21:43:35 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine

21:43:35 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi

21:43:38 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1

21:43:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile

21:43:56 Timing HOL-Library (2 threads, 199.469s elapsed time, 373.924s cpu time, 18.192s GC time, factor 1.87)

21:43:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library

21:43:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf

21:43:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf

21:43:56 Finished HOL-Library (0:04:55 elapsed time, 0:08:47 cpu time, factor 1.79)

21:43:58 Building HOL-Computational_Algebra ...

21:44:03 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

21:44:03 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

21:44:05 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

21:44:07 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts

21:44:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

21:44:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

21:44:13 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary

21:44:19 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub

21:44:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

21:44:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

21:44:22 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

21:44:22 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

21:44:24 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

21:44:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

21:44:26 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height

21:44:27 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

21:44:29 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs

21:44:32 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR

21:44:33 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN

21:44:34 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu

21:44:39 HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening

21:44:42 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern

21:44:53 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS

21:44:57 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization

21:45:01 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support

21:45:02 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation

21:45:06 HOL-Nominal-Examples: theory HOL-Nominal-Examples.W

21:45:13 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening

21:45:43 Warning: missing document directory

21:45:43 Timing HOL-Computational_Algebra (2 threads, 63.756s elapsed time, 116.072s cpu time, 4.444s GC time, factor 1.82)

21:45:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Computational_Algebra

21:45:43 Finished HOL-Computational_Algebra (0:01:45 elapsed time, 0:02:57 cpu time, factor 1.69)

21:45:43 Building HOL-Analysis ...

21:45:52 HOL-Analysis: theory HOL-Analysis.L2_Norm

21:45:52 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

21:45:52 HOL-Analysis: theory HOL-Analysis.Inner_Product

21:45:52 HOL-Analysis: theory HOL-Analysis.Operator_Norm

21:45:53 HOL-Analysis: theory HOL-Analysis.Poly_Roots

21:45:53 HOL-Analysis: theory HOL-Analysis.Summation_Tests

21:45:53 HOL-Analysis: theory HOL-Analysis.Product_Vector

21:45:54 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

21:45:54 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

21:45:56 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

21:45:58 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

21:45:58 HOL-Analysis: theory HOL-Analysis.Measurable

21:45:59 HOL-Analysis: theory HOL-Analysis.Measure_Space

21:46:01 HOL-Analysis: theory HOL-Analysis.Norm_Arith

21:46:02 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

21:46:02 HOL-Analysis: theory HOL-Analysis.Caratheodory

21:46:13 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

21:46:13 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

21:46:15 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

21:46:16 HOL-Analysis: theory HOL-Analysis.Tagged_Division

21:46:17 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

21:46:19 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

21:46:20 HOL-Analysis: theory HOL-Analysis.Path_Connected

21:46:25 HOL-Analysis: theory HOL-Analysis.Homeomorphism

21:46:26 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

21:46:29 HOL-Analysis: theory HOL-Analysis.Derivative

21:46:32 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

21:46:33 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

21:46:35 HOL-Analysis: theory HOL-Analysis.Determinants

21:46:35 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2

21:46:36 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

21:46:37 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

21:46:39 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3

21:46:39 HOL-Analysis: theory HOL-Analysis.Polytope

21:46:43 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

21:46:44 HOL-Analysis: theory HOL-Analysis.Borel_Space

21:46:47 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

21:46:48 HOL-Analysis: theory HOL-Analysis.Regularity

21:46:50 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

21:46:51 HOL-Analysis: theory HOL-Analysis.Embed_Measure

21:46:52 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

21:46:53 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

21:46:54 HOL-Analysis: theory HOL-Analysis.Function_Topology

21:46:56 HOL-Analysis: theory HOL-Analysis.Complete_Measure

21:46:57 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

21:46:57 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

21:46:57 HOL-Analysis: theory HOL-Analysis.Set_Integral

21:46:59 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

21:47:03 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

21:47:03 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

21:47:04 HOL-Analysis: theory HOL-Analysis.Integral_Test

21:47:05 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

21:47:05 HOL-Analysis: theory HOL-Analysis.Interval_Integral

21:47:06 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

21:47:07 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

21:47:09 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

21:47:09 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

21:47:10 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

21:47:10 HOL-Analysis: theory HOL-Analysis.Further_Topology

21:47:13 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

21:47:14 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

21:47:14 HOL-Analysis: theory HOL-Analysis.Gamma_Function

21:47:16 HOL-Analysis: theory HOL-Analysis.Great_Picard

21:47:17 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

21:47:19 HOL-Analysis: theory HOL-Analysis.Analysis

21:54:02 Timing HOL-Proofs (2 threads, 1129.651s elapsed time, 1877.356s cpu time, 338.168s GC time, factor 1.66)

21:54:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

21:54:02 Finished HOL-Proofs (0:21:26 elapsed time, 0:35:32 cpu time, factor 1.66)

21:54:04 Building HOL-Algebra ...

21:54:11 HOL-Algebra: theory HOL-Algebra.Congruence

21:54:11 HOL-Algebra: theory HOL-Algebra.Exponent

21:54:13 HOL-Algebra: theory HOL-Algebra.Order

21:54:14 HOL-Algebra: theory HOL-Algebra.Lattice

21:54:15 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

21:54:17 HOL-Algebra: theory HOL-Algebra.Galois_Connection

21:54:17 HOL-Algebra: theory HOL-Algebra.Group

21:54:18 HOL-Algebra: theory HOL-Algebra.Bij

21:54:18 HOL-Algebra: theory HOL-Algebra.Coset

21:54:19 HOL-Algebra: theory HOL-Algebra.FiniteProduct

21:54:20 HOL-Algebra: theory HOL-Algebra.Sylow

21:54:20 HOL-Algebra: theory HOL-Algebra.Divisibility

21:54:20 HOL-Algebra: theory HOL-Algebra.Ring

21:54:25 HOL-Algebra: theory HOL-Algebra.AbelCoset

21:54:26 HOL-Algebra: theory HOL-Algebra.Module

21:54:29 HOL-Algebra: theory HOL-Algebra.More_Group

21:54:29 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

21:54:29 HOL-Algebra: theory HOL-Algebra.More_Ring

21:54:32 HOL-Algebra: theory HOL-Algebra.Ideal

21:54:37 HOL-Algebra: theory HOL-Algebra.RingHom

21:54:39 HOL-Algebra: theory HOL-Algebra.QuotRing

21:54:39 HOL-Algebra: theory HOL-Algebra.UnivPoly

21:54:40 HOL-Algebra: theory HOL-Algebra.IntRing

21:54:55 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

21:56:27 Timing HOL-Algebra (2 threads, 88.961s elapsed time, 168.304s cpu time, 8.632s GC time, factor 1.89)

21:56:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

21:56:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

21:56:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

21:56:27 Finished HOL-Algebra (0:02:22 elapsed time, 0:04:07 cpu time, factor 1.74)

21:56:28 Building HOL-Auth ...

21:56:33 HOL-Auth: theory HOL-Auth.Message

21:56:36 HOL-Auth: theory HOL-Auth.All_Symmetric

21:56:37 HOL-Auth: theory HOL-Auth.Event

21:56:37 HOL-Auth: theory HOL-Auth.EventSC

21:56:38 HOL-Auth: theory HOL-Auth.Extensions

21:56:39 HOL-Auth: theory HOL-Auth.Analz

21:56:39 HOL-Auth: theory HOL-Auth.List_Msg

21:56:39 HOL-Auth: theory HOL-Auth.Guard

21:56:40 HOL-Auth: theory HOL-Auth.GuardK

21:56:41 HOL-Auth: theory HOL-Auth.Public

21:56:41 HOL-Auth: theory HOL-Auth.Shared

21:56:41 HOL-Auth: theory HOL-Auth.CertifiedEmail

21:56:41 HOL-Auth: theory HOL-Auth.Guard_Public

21:56:42 HOL-Auth: theory HOL-Auth.Guard_NS_Public

21:56:42 HOL-Auth: theory HOL-Auth.P2

21:56:42 HOL-Auth: theory HOL-Auth.Proto

21:56:44 HOL-Auth: theory HOL-Auth.KerberosIV

21:56:46 HOL-Auth: theory HOL-Auth.KerberosIV_Gets

21:56:46 HOL-Auth: theory HOL-Auth.KerberosV

21:56:47 HOL-Auth: theory HOL-Auth.Kerberos_BAN

21:56:48 HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets

21:56:48 HOL-Auth: theory HOL-Auth.NS_Public

21:56:49 HOL-Auth: theory HOL-Auth.NS_Public_Bad

21:56:49 HOL-Auth: theory HOL-Auth.NS_Shared

21:56:49 HOL-Auth: theory HOL-Auth.OtwayRees

21:56:50 HOL-Auth: theory HOL-Auth.OtwayReesBella

21:56:50 HOL-Auth: theory HOL-Auth.OtwayRees_AN

21:56:50 HOL-Auth: theory HOL-Auth.OtwayRees_Bad

21:56:51 HOL-Auth: theory HOL-Auth.P1

21:56:51 HOL-Auth: theory HOL-Auth.Recur

21:56:52 HOL-Auth: theory HOL-Auth.WooLam

21:56:53 HOL-Auth: theory HOL-Auth.Yahalom

21:56:54 HOL-Auth: theory HOL-Auth.Yahalom2

21:56:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition

21:56:55 HOL-Auth: theory HOL-Auth.Yahalom_Bad

21:56:55 HOL-Auth: theory HOL-Auth.ZhouGollmann

21:56:56 HOL-Auth: theory HOL-Auth.Auth_Shared

21:56:57 HOL-Auth: theory HOL-Auth.Auth_Guard_Public

21:56:57 HOL-Auth: theory HOL-Auth.Guard_Shared

21:56:58 HOL-Auth: theory HOL-Auth.Guard_OtwayRees

21:56:58 Timing HOL-Nominal-Examples (2 threads, 802.451s elapsed time, 1546.884s cpu time, 117.300s GC time, factor 1.93)

21:56:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples

21:56:58 Finished HOL-Nominal-Examples (0:13:25 elapsed time, 0:25:49 cpu time, factor 1.92)

21:56:58 Building HOL-Number_Theory ...

21:56:58 HOL-Auth: theory HOL-Auth.Guard_Yahalom

21:56:58 HOL-Auth: theory HOL-Auth.TLS

21:56:59 HOL-Auth: theory HOL-Auth.Auth_Guard_Shared

21:56:59 HOL-Auth: theory HOL-Auth.Smartcard

21:56:59 HOL-Auth: theory HOL-Auth.ShoupRubin

21:57:00 HOL-Auth: theory HOL-Auth.Auth_Public

21:57:01 HOL-Auth: theory HOL-Auth.ShoupRubinBella

21:57:03 HOL-Auth: theory HOL-Auth.Auth_Smartcard

21:57:05 HOL-Number_Theory: theory HOL-Number_Theory.Congruence

21:57:06 HOL-Number_Theory: theory HOL-Number_Theory.Order

21:57:07 HOL-Number_Theory: theory HOL-Number_Theory.Lattice

21:57:08 HOL-Number_Theory: theory HOL-Number_Theory.Complete_Lattice

21:57:10 HOL-Number_Theory: theory HOL-Number_Theory.Group

21:57:11 HOL-Number_Theory: theory HOL-Number_Theory.FiniteProduct

21:57:12 HOL-Number_Theory: theory HOL-Number_Theory.Ring

21:57:40 HOL-Number_Theory: theory HOL-Number_Theory.Cong

21:57:40 HOL-Number_Theory: theory HOL-Number_Theory.Coset

21:57:41 HOL-Number_Theory: theory HOL-Number_Theory.Module

21:57:41 HOL-Number_Theory: theory HOL-Number_Theory.AbelCoset

21:57:43 HOL-Number_Theory: theory HOL-Number_Theory.More_Group

21:57:44 HOL-Number_Theory: theory HOL-Number_Theory.More_Finite_Product

21:57:44 HOL-Number_Theory: theory HOL-Number_Theory.More_Ring

21:57:45 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

21:57:45 HOL-Number_Theory: theory HOL-Number_Theory.Fib

21:57:45 HOL-Number_Theory: theory HOL-Number_Theory.Totient

21:57:49 HOL-Number_Theory: theory HOL-Number_Theory.Ideal

21:57:55 HOL-Number_Theory: theory HOL-Number_Theory.RingHom

21:57:57 HOL-Number_Theory: theory HOL-Number_Theory.UnivPoly

21:58:13 HOL-Number_Theory: theory HOL-Number_Theory.Multiplicative_Group

21:58:16 HOL-Number_Theory: theory HOL-Number_Theory.Residues

21:58:20 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

21:58:20 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

21:58:21 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

21:58:21 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

21:58:21 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

21:59:42 Timing HOL-Number_Theory (2 threads, 112.776s elapsed time, 215.012s cpu time, 9.220s GC time, factor 1.91)

21:59:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory

21:59:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf

21:59:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf

21:59:42 Finished HOL-Number_Theory (0:02:43 elapsed time, 0:04:50 cpu time, factor 1.77)

21:59:42 Building HOL-Nonstandard_Analysis ...

21:59:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter

21:59:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef

21:59:50 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat

21:59:51 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef

21:59:52 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA

21:59:54 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex

21:59:54 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star

21:59:55 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim

21:59:55 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar

21:59:56 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv

21:59:56 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ

21:59:57 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries

21:59:58 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental

21:59:58 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog

21:59:58 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA

21:59:59 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal

21:59:59 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar

22:00:00 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim

22:00:00 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex

22:00:01 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis

22:00:03 Timing HOL-Auth (2 threads, 168.273s elapsed time, 303.612s cpu time, 10.052s GC time, factor 1.80)

22:00:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

22:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

22:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

22:00:03 Finished HOL-Auth (0:03:35 elapsed time, 0:06:16 cpu time, factor 1.75)

22:00:04 Building Codegen_Basics ...

22:00:04 Timing HOL-Analysis (2 threads, 738.249s elapsed time, 1264.924s cpu time, 86.408s GC time, factor 1.71)

22:00:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

22:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

22:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf

22:00:04 Finished HOL-Analysis (0:14:20 elapsed time, 0:24:07 cpu time, factor 1.68)

22:00:06 Building HOL-Probability ...

22:00:09 Codegen_Basics: theory Codegen_Basics.Setup

22:00:16 HOL-Probability: theory HOL-Probability.Fin_Map

22:00:16 HOL-Probability: theory HOL-Probability.Discrete_Topology

22:00:17 HOL-Probability: theory HOL-Probability.Essential_Supremum

22:00:17 HOL-Probability: theory HOL-Probability.Probability_Measure

22:00:19 HOL-Probability: theory HOL-Probability.Stopping_Time

22:00:19 HOL-Probability: theory HOL-Probability.Tree_Space

22:00:19 HOL-Probability: theory HOL-Probability.Conditional_Expectation

22:00:20 HOL-Probability: theory HOL-Probability.Distribution_Functions

22:00:20 HOL-Probability: theory HOL-Probability.Giry_Monad

22:00:21 HOL-Probability: theory HOL-Probability.Weak_Convergence

22:00:21 HOL-Probability: theory HOL-Probability.Helly_Selection

22:00:23 HOL-Probability: theory HOL-Probability.Probability_Mass_Function

22:00:23 HOL-Probability: theory HOL-Probability.Projective_Family

22:00:24 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure

22:00:26 HOL-Probability: theory HOL-Probability.PMF_Impl

22:00:26 HOL-Probability: theory HOL-Probability.Random_Permutations

22:00:27 HOL-Probability: theory HOL-Probability.SPMF

22:00:28 HOL-Probability: theory HOL-Probability.Independent_Family

22:00:29 HOL-Probability: theory HOL-Probability.Convolution

22:00:30 HOL-Probability: theory HOL-Probability.Information

22:00:30 HOL-Probability: theory HOL-Probability.Projective_Limit

22:00:31 Timing HOL-Nonstandard_Analysis (2 threads, 14.555s elapsed time, 27.520s cpu time, 1.036s GC time, factor 1.89)

22:00:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

22:00:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

22:00:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

22:00:31 Finished HOL-Nonstandard_Analysis (0:00:47 elapsed time, 0:01:15 cpu time, factor 1.58)

22:00:31 Timing Codegen_Basics (2 threads, 1.572s elapsed time, 1.652s cpu time, 0.000s GC time, factor 1.05)

22:00:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

22:00:31 Finished Codegen_Basics (0:00:26 elapsed time, 0:00:36 cpu time, factor 1.37)

22:00:31 Building Typeclass_Hierarchy_Basics ...

22:00:31 Running HOL-Codegenerator_Test ...

22:00:33 HOL-Probability: theory HOL-Probability.Distributions

22:00:33 HOL-Probability: theory HOL-Probability.Stream_Space

22:00:34 HOL-Probability: theory HOL-Probability.Characteristic_Functions

22:00:35 HOL-Probability: theory HOL-Probability.Sinc_Integral

22:00:35 HOL-Probability: theory HOL-Probability.Levy

22:00:36 Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup

22:00:36 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem

22:00:37 HOL-Probability: theory Probability

22:00:39 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Less_False

22:00:39 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Cmp

22:00:39 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Sorted_Less

22:00:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.AList_Upd_Del

22:00:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.List_Ins_Del

22:00:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Set_by_Ordered

22:00:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Map_by_Ordered

22:00:41 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Records

22:00:41 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML

22:00:41 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala

22:00:41 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Tree_Set

22:00:42 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Tree_Map

22:00:45 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates

22:00:50 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate

22:00:54 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat

22:00:58 Timing Typeclass_Hierarchy_Basics (2 threads, 0.949s elapsed time, 1.048s cpu time, 0.000s GC time, factor 1.10)

22:00:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

22:00:58 Finished Typeclass_Hierarchy_Basics (0:00:26 elapsed time, 0:00:35 cpu time, factor 1.33)

22:00:58 Running HOL-Data_Structures ...

22:01:00 HOL-Data_Structures: theory HOL-Data_Structures.Less_False

22:01:00 HOL-Data_Structures: theory HOL-Data_Structures.Cancellation

22:01:00 HOL-Data_Structures: theory HOL-Data_Structures.Fib

22:01:01 HOL-Data_Structures: theory HOL-Data_Structures.Multiset

22:01:10 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less

22:01:10 HOL-Data_Structures: theory HOL-Data_Structures.Cmp

22:01:10 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del

22:01:11 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del

22:01:11 HOL-Data_Structures: theory HOL-Data_Structures.Map_by_Ordered

22:01:11 HOL-Data_Structures: theory HOL-Data_Structures.Set_by_Ordered

22:01:11 HOL-Data_Structures: theory HOL-Data_Structures.Tree

22:01:11 HOL-Data_Structures: theory HOL-Data_Structures.Tree2

22:01:12 HOL-Data_Structures: theory HOL-Data_Structures.Isin2

22:01:13 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set

22:01:15 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2

22:01:15 HOL-Data_Structures: theory HOL-Data_Structures.Splay_Set

22:01:15 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set

22:01:17 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map

22:01:17 HOL-Data_Structures: theory HOL-Data_Structures.Splay_Map

22:01:17 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map

22:01:18 HOL-Data_Structures: theory HOL-Data_Structures.RBT

22:01:19 HOL-Data_Structures: theory HOL-Data_Structures.Tree23

22:01:21 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set

22:01:22 HOL-Data_Structures: theory HOL-Data_Structures.Tree234

22:01:24 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set

22:01:28 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map

22:01:32 HOL-Data_Structures: theory HOL-Data_Structures.Balance

22:01:33 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set

22:01:35 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map

22:01:36 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set

22:01:54 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map

22:02:21 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap

22:02:23 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set

22:02:27 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map

22:02:56 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map

22:03:33 Timing HOL-Probability (2 threads, 141.613s elapsed time, 263.780s cpu time, 7.584s GC time, factor 1.86)

22:03:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

22:03:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

22:03:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

22:03:33 Finished HOL-Probability (0:03:26 elapsed time, 0:05:50 cpu time, factor 1.69)

22:03:33 Running HOL-ex ...

22:03:39 HOL-ex: theory HOL-ex.Computations

22:03:39 HOL-ex: theory HOL-ex.Groebner_Examples

22:03:39 HOL-ex: theory HOL-ex.PresburgerEx

22:03:39 HOL-ex: theory HOL-ex.Bubblesort

22:03:40 HOL-ex: theory HOL-ex.MergeSort

22:03:40 HOL-ex: theory HOL-ex.Quicksort

22:03:41 HOL-ex: theory HOL-ex.IArray_Examples

22:03:41 HOL-ex: theory HOL-ex.Perm_Fragments

22:03:41 HOL-ex: theory HOL-ex.Refute_Examples

22:03:42 HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples

22:03:42 HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex

22:03:43 HOL-ex: theory HOL-ex.While_Combinator_Example

22:03:43 HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples

22:03:45 HOL-ex: theory HOL-ex.Antiquote

22:03:45 HOL-ex: theory HOL-ex.Arith_Examples

22:03:45 HOL-ex: theory HOL-ex.Birthday_Paradox

22:03:45 HOL-ex: theory HOL-ex.CTL

22:03:45 HOL-ex: theory HOL-ex.Cartouche_Examples

22:03:45 HOL-ex: theory HOL-ex.Case_Product

22:03:45 HOL-ex: theory HOL-ex.Chinese

22:03:45 HOL-ex: theory HOL-ex.Classical

22:03:47 HOL-ex: theory HOL-ex.Coercion_Examples

22:03:47 HOL-ex: theory HOL-ex.Coherent

22:03:47 HOL-ex: theory HOL-ex.Commands

22:03:48 HOL-ex: theory HOL-ex.Erdoes_Szekeres

22:03:48 HOL-ex: theory HOL-ex.Executable_Relation

22:03:48 HOL-ex: theory HOL-ex.Execute_Choice

22:03:48 HOL-ex: theory HOL-ex.Factorial_Ring

22:03:49 HOL-ex: theory HOL-ex.Functions

22:03:55 HOL-ex: theory HOL-ex.Guess

22:03:55 HOL-ex: theory HOL-ex.Hebrew

22:03:57 HOL-ex: theory HOL-ex.Euclidean_Algorithm

22:03:58 HOL-ex: theory HOL-ex.Hex_Bin_Examples

22:03:58 HOL-ex: theory HOL-ex.Iff_Oracle

22:03:58 HOL-ex: theory HOL-ex.Induction_Schema

22:03:58 HOL-ex: theory HOL-ex.Intuitionistic

22:03:58 HOL-ex: theory HOL-ex.Lagrange

22:03:58 HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples

22:03:59 HOL-ex: theory HOL-ex.LocaleTest2

22:04:00 HOL-ex: theory HOL-ex.ML

22:04:01 HOL-ex: theory HOL-ex.MonoidGroup

22:04:01 HOL-ex: theory HOL-ex.Multiquote

22:04:01 HOL-ex: theory HOL-ex.NatSum

22:04:02 HOL-ex: theory HOL-ex.PER

22:04:02 HOL-ex: theory HOL-ex.Peano_Axioms

22:04:02 HOL-ex: theory HOL-ex.Primrec

22:04:02 HOL-ex: theory HOL-ex.Records

22:04:05 HOL-ex: theory HOL-ex.Primes

22:04:05 HOL-ex: theory HOL-ex.Eratosthenes

22:04:06 HOL-ex: theory HOL-ex.Code_Timing

22:04:07 HOL-ex: theory HOL-ex.Rewrite_Examples

22:04:07 HOL-ex: theory HOL-ex.SAT_Examples

22:04:07 HOL-ex: theory HOL-ex.Seq

22:04:07 HOL-ex: theory HOL-ex.Serbian

22:04:08 HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples

22:04:09 HOL-ex: theory HOL-ex.Set_Theory

22:04:09 HOL-ex: theory HOL-ex.Simproc_Tests

22:04:14 HOL-ex: theory HOL-ex.Sudoku

22:04:14 HOL-ex: theory HOL-ex.Tarski

22:04:15 HOL-ex: theory HOL-ex.Termination

22:04:15 HOL-ex: theory HOL-ex.ThreeDivides

22:04:16 HOL-ex: theory HOL-ex.Transfer_Debug

22:04:16 HOL-ex: theory HOL-ex.Transfer_Int_Nat

22:04:16 HOL-ex: theory HOL-ex.Transfer_Ex

22:04:16 HOL-ex: theory HOL-ex.Tree23

22:04:22 HOL-ex: theory HOL-ex.Unification

22:04:25 HOL-ex: theory HOL-ex.Word_Type

22:04:27 HOL-ex: theory HOL-ex.veriT_Preprocessing

22:04:28 HOL-ex: theory HOL-ex.SOS

22:04:28 HOL-ex: theory HOL-ex.SOS_Cert

22:04:29 HOL-ex: theory HOL-ex.Argo_Examples

22:04:31 HOL-ex: theory HOL-ex.Ballot

22:04:32 HOL-ex: theory HOL-ex.BinEx

22:04:33 HOL-ex: theory HOL-ex.Code_Binary_Nat_examples

22:04:34 HOL-ex: theory HOL-ex.Cubic_Quartic

22:04:34 HOL-ex: theory HOL-ex.Dedekind_Real

22:04:36 HOL-ex: theory HOL-ex.Eval_Examples

22:04:39 HOL-ex: theory HOL-ex.Gauge_Integration

22:04:40 HOL-ex: theory HOL-ex.HarmonicSeries

22:04:40 HOL-ex: theory HOL-ex.Normalization_by_Evaluation

22:04:41 HOL-ex: theory HOL-ex.Parallel_Example

22:04:42 HOL-ex: theory HOL-ex.Pythagoras

22:04:43 HOL-ex: theory HOL-ex.Reflection_Examples

22:05:04 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures

22:05:09 HOL-ex: theory HOL-ex.Sqrt

22:05:10 HOL-ex: theory HOL-ex.Sqrt_Script

22:05:11 HOL-ex: theory HOL-ex.Sum_of_Powers

22:05:14 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Pretty_Char

22:08:37 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat

22:12:13 Timing HOL-Data_Structures (2 threads, 669.667s elapsed time, 1017.072s cpu time, 53.896s GC time, factor 1.52)

22:12:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures

22:12:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf

22:12:13 Finished HOL-Data_Structures (0:11:14 elapsed time, 0:17:02 cpu time, factor 1.51)

22:12:13 Running HOL-Decision_Procs ...

22:12:22 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions

22:12:22 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library

22:12:22 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order

22:12:23 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux

22:12:24 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring

22:12:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex

22:12:25 HOL-ex: theory HOL-ex.Meson_Test

22:12:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper

22:12:38 Timing HOL-ex (2 threads, 538.361s elapsed time, 998.804s cpu time, 57.848s GC time, factor 1.86)

22:12:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex

22:12:38 Finished HOL-ex (0:09:04 elapsed time, 0:17:08 cpu time, factor 1.89)

22:12:38 Running HOL-Corec_Examples ...

22:12:39 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete

22:12:40 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field

22:12:44 HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV

22:12:44 HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter

22:12:49 HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting

22:12:52 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex

22:12:54 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack

22:12:57 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC

22:12:58 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor

22:12:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton

22:13:03 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml

22:13:04 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ

22:13:05 Timing HOL-Codegenerator_Test (2 threads, 745.125s elapsed time, 568.860s cpu time, 14.164s GC time, factor 0.76)

22:13:05 Finished HOL-Codegenerator_Test (0:12:33 elapsed time, 0:26:39 cpu time, factor 2.12)

22:13:05 Running HOL-Nitpick_Examples ...

22:13:11 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Core_Nits

22:13:11 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Datatype_Nits

22:13:11 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Hotel_Nits

22:13:12 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Induct_Nits

22:13:12 HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples

22:13:13 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Integer_Nits

22:13:13 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mini_Nits

22:13:14 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mono_Nits

22:13:15 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Pattern_Nits

22:13:15 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Record_Nits

22:13:17 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Refute_Nits

22:13:23 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR

22:13:29 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Special_Nits

22:13:30 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Tests_Nits

22:13:31 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Manual_Nits

22:13:38 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Typedef_Nits

22:13:53 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Nitpick_Examples

22:14:05 HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones

22:14:05 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A

22:14:09 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List

22:14:10 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B

22:14:14 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair

22:14:14 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C

22:14:15 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds

22:14:17 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly

22:14:20 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D

22:14:20 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation

22:14:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial

22:14:29 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono

22:14:41 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff

22:15:11 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly

22:15:19 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex

22:15:20 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex

22:15:20 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs

22:16:27 HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete

22:17:06 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends

22:17:15 HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends

22:17:36 HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class

22:18:07 Timing HOL-Nitpick_Examples (2 threads, 296.043s elapsed time, 146.980s cpu time, 2.808s GC time, factor 0.50)

22:18:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples

22:18:07 Finished HOL-Nitpick_Examples (0:05:01 elapsed time, 0:10:48 cpu time, factor 2.15)

22:18:07 Running HOL-MicroJava ...

22:18:08 Timing HOL-Corec_Examples (2 threads, 323.324s elapsed time, 574.956s cpu time, 58.312s GC time, factor 1.78)

22:18:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples

22:18:08 Finished HOL-Corec_Examples (0:05:29 elapsed time, 0:09:41 cpu time, factor 1.76)

22:18:08 Running HOL-Hoare_Parallel ...

22:18:10 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com

22:18:10 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph

22:18:11 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote

22:18:11 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com

22:18:13 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran

22:18:13 HOL-MicroJava: theory HOL-MicroJava.Eisbach

22:18:13 HOL-MicroJava: theory HOL-MicroJava.Semilat

22:18:13 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran

22:18:14 HOL-MicroJava: theory HOL-MicroJava.JBasis

22:18:14 HOL-MicroJava: theory HOL-MicroJava.Err

22:18:14 HOL-MicroJava: theory HOL-MicroJava.AuxLemmas

22:18:14 HOL-MicroJava: theory HOL-MicroJava.Type

22:18:15 HOL-MicroJava: theory HOL-MicroJava.Listn

22:18:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare

22:18:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare

22:18:15 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework

22:18:16 HOL-MicroJava: theory HOL-MicroJava.Opt

22:18:16 HOL-MicroJava: theory HOL-MicroJava.Product

22:18:16 HOL-MicroJava: theory HOL-MicroJava.SemilatAlg

22:18:16 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics

22:18:16 HOL-MicroJava: theory HOL-MicroJava.Kildall

22:18:16 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax

22:18:17 HOL-MicroJava: theory HOL-MicroJava.Decl

22:18:17 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples

22:18:17 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax

22:18:17 HOL-MicroJava: theory HOL-MicroJava.SystemClasses

22:18:17 HOL-MicroJava: theory HOL-MicroJava.TypeRel

22:18:17 HOL-MicroJava: theory HOL-MicroJava.Value

22:18:17 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll

22:18:18 HOL-MicroJava: theory HOL-MicroJava.WellForm

22:18:18 HOL-MicroJava: theory HOL-MicroJava.State

22:18:18 HOL-MicroJava: theory HOL-MicroJava.Exceptions

22:18:19 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll

22:18:19 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples

22:18:19 HOL-MicroJava: theory HOL-MicroJava.Term

22:18:19 HOL-MicroJava: theory HOL-MicroJava.LBVSpec

22:18:20 HOL-MicroJava: theory HOL-MicroJava.LBVComplete

22:18:20 HOL-MicroJava: theory HOL-MicroJava.LBVCorrect

22:18:21 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err

22:18:21 HOL-MicroJava: theory HOL-MicroJava.Abstract_BV

22:18:21 HOL-MicroJava: theory HOL-MicroJava.Semilattices

22:18:22 HOL-MicroJava: theory HOL-MicroJava.JType

22:18:22 HOL-MicroJava: theory HOL-MicroJava.JVMType

22:18:23 HOL-MicroJava: theory HOL-MicroJava.WellType

22:18:23 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel

22:18:24 HOL-MicroJava: theory HOL-MicroJava.Conform

22:18:25 HOL-MicroJava: theory HOL-MicroJava.JVMState

22:18:25 HOL-MicroJava: theory HOL-MicroJava.JVMInstructions

22:18:27 HOL-MicroJava: theory HOL-MicroJava.JVMExceptions

22:18:27 HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr

22:18:27 HOL-MicroJava: theory HOL-MicroJava.Eval

22:18:27 HOL-MicroJava: theory HOL-MicroJava.JVMExec

22:18:28 HOL-MicroJava: theory HOL-MicroJava.DefsComp

22:18:28 HOL-MicroJava: theory HOL-MicroJava.Index

22:18:29 HOL-MicroJava: theory HOL-MicroJava.JVMDefensive

22:18:30 HOL-MicroJava: theory HOL-MicroJava.JVMListExample

22:18:31 HOL-MicroJava: theory HOL-MicroJava.TypeInf

22:18:31 HOL-MicroJava: theory HOL-MicroJava.Effect

22:18:31 HOL-MicroJava: theory HOL-MicroJava.Example

22:18:33 HOL-MicroJava: theory HOL-MicroJava.JListExample

22:18:34 HOL-MicroJava: theory HOL-MicroJava.JTypeSafe

22:18:35 HOL-MicroJava: theory HOL-MicroJava.TranslCompTp

22:18:36 HOL-MicroJava: theory HOL-MicroJava.TranslComp

22:18:36 HOL-MicroJava: theory HOL-MicroJava.LemmasComp

22:18:36 HOL-MicroJava: theory HOL-MicroJava.CorrComp

22:18:56 HOL-MicroJava: theory HOL-MicroJava.BVSpec

22:18:56 HOL-MicroJava: theory HOL-MicroJava.EffectMono

22:18:57 HOL-MicroJava: theory HOL-MicroJava.Altern

22:18:57 HOL-MicroJava: theory HOL-MicroJava.Correct

22:18:57 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM

22:18:57 HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe

22:18:58 HOL-MicroJava: theory HOL-MicroJava.JVM

22:18:58 HOL-MicroJava: theory HOL-MicroJava.CorrCompTp

22:18:58 HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError

22:18:59 HOL-MicroJava: theory HOL-MicroJava.BVExample

22:19:00 HOL-MicroJava: theory HOL-MicroJava.LBVJVM

22:19:00 HOL-MicroJava: theory HOL-MicroJava.MicroJava

22:20:34 Timing HOL-Decision_Procs (2 threads, 491.407s elapsed time, 898.072s cpu time, 57.576s GC time, factor 1.83)

22:20:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs

22:20:34 Finished HOL-Decision_Procs (0:08:20 elapsed time, 0:15:07 cpu time, factor 1.81)

22:20:34 Running HOL-Datatype_Examples ...

22:20:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte

22:20:40 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF

22:20:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI

22:20:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term

22:20:44 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype

22:20:45 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim

22:20:45 HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree

22:20:46 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition

22:20:46 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI

22:20:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang

22:20:48 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig

22:20:48 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process

22:20:53 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor

22:21:00 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat

22:21:21 Timing HOL-Hoare_Parallel (2 threads, 186.407s elapsed time, 360.896s cpu time, 4.868s GC time, factor 1.94)

22:21:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel

22:21:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf

22:21:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf

22:21:21 Finished HOL-Hoare_Parallel (0:03:12 elapsed time, 0:06:08 cpu time, factor 1.92)

22:21:21 Running HOL-IMP ...

22:21:27 HOL-IMP: theory HOL-IMP.AExp

22:21:27 HOL-IMP: theory HOL-IMP.C_like

22:21:28 HOL-IMP: theory HOL-IMP.ASM

22:21:29 Timing HOL-MicroJava (2 threads, 191.455s elapsed time, 319.352s cpu time, 9.804s GC time, factor 1.67)

22:21:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava

22:21:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf

22:21:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf

22:21:29 Finished HOL-MicroJava (0:03:21 elapsed time, 0:05:31 cpu time, factor 1.65)

22:21:29 Running HOL-Proofs-Lambda ...

22:21:29 HOL-IMP: theory HOL-IMP.BExp

22:21:31 HOL-IMP: theory HOL-IMP.Complete_Lattice

22:21:31 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation

22:21:31 HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int

22:21:31 HOL-IMP: theory HOL-IMP.OO

22:21:32 HOL-IMP: theory HOL-IMP.Com

22:21:32 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda

22:21:32 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder

22:21:32 HOL-IMP: theory HOL-IMP.ACom

22:21:35 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication

22:21:35 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType

22:21:36 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype

22:21:36 HOL-IMP: theory HOL-IMP.Abs_Int_Tests

22:21:36 HOL-IMP: theory HOL-IMP.Big_Step

22:21:36 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed

22:21:37 HOL-IMP: theory HOL-IMP.Denotational

22:21:37 HOL-IMP: theory HOL-IMP.Hoare

22:21:37 HOL-IMP: theory HOL-IMP.Hoare_Examples

22:21:37 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta

22:21:38 HOL-IMP: theory HOL-IMP.Hoare_Total

22:21:38 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta

22:21:38 HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete

22:21:38 HOL-IMP: theory HOL-IMP.Hoare_Total_EX

22:21:38 HOL-IMP: theory HOL-IMP.VCG_Total_EX

22:21:39 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi

22:21:39 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm

22:21:40 HOL-IMP: theory HOL-IMP.VCG

22:21:41 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm

22:21:41 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization

22:21:41 HOL-IMP: theory HOL-IMP.Sec_Type_Expr

22:21:42 HOL-IMP: theory HOL-IMP.Sec_Typing

22:21:42 HOL-IMP: theory HOL-IMP.Sec_TypingT

22:21:42 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm

22:21:42 HOL-IMP: theory HOL-IMP.Sem_Equiv

22:21:43 HOL-IMP: theory HOL-IMP.Vars

22:21:43 HOL-IMP: theory HOL-IMP.Procs

22:21:43 HOL-IMP: theory HOL-IMP.Def_Init

22:21:43 HOL-IMP: theory HOL-IMP.Def_Init_Exp

22:21:44 HOL-IMP: theory HOL-IMP.Def_Init_Big

22:21:44 HOL-IMP: theory HOL-IMP.Fold

22:21:45 HOL-IMP: theory HOL-IMP.Live

22:21:45 HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn

22:21:46 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn

22:21:46 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat

22:21:47 HOL-IMP: theory HOL-IMP.Collecting

22:21:48 HOL-IMP: theory HOL-IMP.Collecting1

22:21:48 HOL-IMP: theory HOL-IMP.Collecting_Examples

22:21:48 HOL-IMP: theory HOL-IMP.Star

22:21:49 HOL-IMP: theory HOL-IMP.Compiler

22:21:52 HOL-IMP: theory HOL-IMP.Def_Init_Small

22:21:52 HOL-IMP: theory HOL-IMP.Small_Step

22:21:53 HOL-IMP: theory HOL-IMP.Finite_Reachable

22:21:53 HOL-IMP: theory HOL-IMP.Compiler2

22:21:54 HOL-IMP: theory HOL-IMP.Abs_Int_init

22:21:54 HOL-IMP: theory HOL-IMP.Live_True

22:21:55 HOL-IMP: theory HOL-IMP.Abs_Int0

22:21:55 HOL-IMP: theory HOL-IMP.Types

22:21:56 HOL-IMP: theory HOL-IMP.Abs_State

22:21:57 HOL-IMP: theory HOL-IMP.Abs_Int1

22:21:58 HOL-IMP: theory HOL-IMP.Abs_Int1_const

22:21:59 HOL-IMP: theory HOL-IMP.Abs_Int1_parity

22:22:00 HOL-IMP: theory HOL-IMP.Abs_Int2

22:22:01 HOL-IMP: theory HOL-IMP.Poly_Types

22:22:02 HOL-IMP: theory HOL-IMP.Abs_Int2_ivl

22:22:03 HOL-IMP: theory HOL-IMP.Abs_Int3

22:22:03 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec

22:23:07 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec

22:23:39 Timing HOL-Datatype_Examples (2 threads, 178.077s elapsed time, 345.556s cpu time, 42.232s GC time, factor 1.94)

22:23:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

22:23:39 Finished HOL-Datatype_Examples (0:03:04 elapsed time, 0:06:03 cpu time, factor 1.97)

22:23:39 Running HOL-Quickcheck_Examples ...

22:23:45 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness

22:23:45 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces

22:23:45 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples

22:23:46 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting

22:23:46 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples

22:23:46 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example

22:24:14 Timing HOL-Proofs-Lambda (2 threads, 159.733s elapsed time, 180.556s cpu time, 5.552s GC time, factor 1.13)

22:24:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda

22:24:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/document.pdf

22:24:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf

22:24:14 Finished HOL-Proofs-Lambda (0:02:45 elapsed time, 0:03:07 cpu time, factor 1.13)

22:24:14 Running HOL-Proofs-Extraction ...

22:24:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Adhoc_Overloading

22:24:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Cancellation

22:24:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Code_Abstract_Nat

22:24:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Code_Target_Nat

22:24:18 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Code_Target_Int

22:24:18 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Multiset

22:24:18 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Code_Target_Numeral

22:24:18 Timing HOL-IMP (2 threads, 167.335s elapsed time, 319.616s cpu time, 15.036s GC time, factor 1.91)

22:24:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP

22:24:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf

22:24:18 Finished HOL-IMP (0:02:57 elapsed time, 0:05:30 cpu time, factor 1.87)

22:24:19 Running HOL-Bali ...

22:24:19 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Monad_Syntax

22:24:19 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.State_Monad

22:24:24 HOL-Bali: theory HOL-Bali.Basis

22:24:26 HOL-Bali: theory HOL-Bali.Name

22:24:26 HOL-Bali: theory HOL-Bali.Table

22:24:28 HOL-Bali: theory HOL-Bali.Type

22:24:30 HOL-Bali: theory HOL-Bali.Value

22:24:31 HOL-Bali: theory HOL-Bali.Term

22:24:41 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Factorial_Ring

22:24:51 HOL-Bali: theory HOL-Bali.Decl

22:24:56 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclidean_Algorithm

22:24:56 HOL-Bali: theory HOL-Bali.TypeRel

22:24:57 HOL-Bali: theory HOL-Bali.DeclConcepts

22:25:00 HOL-Bali: theory HOL-Bali.State

22:25:00 HOL-Bali: theory HOL-Bali.WellType

22:25:01 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example

22:25:01 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples

22:25:02 HOL-Bali: theory HOL-Bali.Conform

22:25:02 HOL-Bali: theory HOL-Bali.Eval

22:25:05 HOL-Bali: theory HOL-Bali.DefiniteAssignment

22:25:07 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Primes

22:25:12 HOL-Bali: theory HOL-Bali.WellForm

22:25:13 HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect

22:25:14 HOL-Bali: theory HOL-Bali.Example

22:25:14 HOL-Bali: theory HOL-Bali.TypeSafe

22:25:17 HOL-Bali: theory HOL-Bali.Evaln

22:25:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman

22:25:17 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util

22:25:18 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem

22:25:19 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall

22:25:20 HOL-Bali: theory HOL-Bali.AxSem

22:25:20 HOL-Bali: theory HOL-Bali.Trans

22:25:23 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor

22:25:23 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole

22:25:24 HOL-Bali: theory HOL-Bali.AxCompl

22:25:25 HOL-Bali: theory HOL-Bali.AxSound

22:25:25 HOL-Bali: theory HOL-Bali.AxExample

22:25:36 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid

22:26:07 Timing HOL-Quickcheck_Examples (2 threads, 140.877s elapsed time, 181.448s cpu time, 4.872s GC time, factor 1.29)

22:26:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples

22:26:07 Finished HOL-Quickcheck_Examples (0:02:26 elapsed time, 0:04:42 cpu time, factor 1.92)

22:26:07 Running HOL-Predicate_Compile_Examples ...

22:26:11 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction

22:26:12 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1

22:26:12 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2

22:26:13 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3

22:26:13 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4

22:26:15 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples

22:26:15 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests

22:26:21 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples

22:26:26 Timing HOL-Proofs-Extraction (2 threads, 126.829s elapsed time, 211.016s cpu time, 8.364s GC time, factor 1.66)

22:26:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction

22:26:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

22:26:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

22:26:26 Finished HOL-Proofs-Extraction (0:02:11 elapsed time, 0:03:36 cpu time, factor 1.65)

22:26:26 Running HOL-Imperative_HOL ...

22:26:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List

22:26:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist

22:26:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap

22:26:34 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad

22:26:35 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples

22:26:37 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array

22:26:38 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref

22:26:38 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL

22:26:38 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists

22:26:40 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview

22:26:40 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker

22:26:44 Timing HOL-Bali (2 threads, 127.802s elapsed time, 225.856s cpu time, 12.156s GC time, factor 1.77)

22:26:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali

22:26:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf

22:26:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf

22:26:44 Finished HOL-Bali (0:02:25 elapsed time, 0:04:07 cpu time, factor 1.71)

22:26:44 Running HOL-Word-SMT_Examples ...

22:26:48 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie

22:26:48 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples

22:26:48 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples

22:26:51 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests

22:26:59 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray

22:27:00 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort

22:27:12 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse

22:27:36 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex

22:28:03 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples

22:28:03 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example

22:28:05 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example

22:28:06 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example

22:28:07 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples

22:28:09 Timing HOL-Imperative_HOL (2 threads, 95.090s elapsed time, 82.716s cpu time, 2.572s GC time, factor 0.87)

22:28:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL

22:28:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf

22:28:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

22:28:09 Finished HOL-Imperative_HOL (0:01:42 elapsed time, 0:03:55 cpu time, factor 2.30)

22:28:09 Running HOL-UNITY ...

22:28:09 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog

22:28:13 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example

22:28:16 HOL-UNITY: theory HOL-UNITY.ListOrder

22:28:16 HOL-UNITY: theory HOL-UNITY.UNITY

22:28:17 HOL-UNITY: theory HOL-UNITY.Constrains

22:28:17 HOL-UNITY: theory HOL-UNITY.Deadlock

22:28:17 HOL-UNITY: theory HOL-UNITY.FP

22:28:17 Timing HOL-Word-SMT_Examples (2 threads, 88.380s elapsed time, 96.332s cpu time, 0.792s GC time, factor 1.09)

22:28:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples

22:28:17 Finished HOL-Word-SMT_Examples (0:01:32 elapsed time, 0:01:42 cpu time, factor 1.11)

22:28:17 Running Corec ...

22:28:17 HOL-UNITY: theory HOL-UNITY.Network

22:28:17 HOL-UNITY: theory HOL-UNITY.WFair

22:28:18 HOL-UNITY: theory HOL-UNITY.SubstAx

22:28:18 HOL-UNITY: theory HOL-UNITY.Token

22:28:19 HOL-UNITY: theory HOL-UNITY.Detects

22:28:19 HOL-UNITY: theory HOL-UNITY.Follows

22:28:19 HOL-UNITY: theory HOL-UNITY.Union

22:28:20 HOL-UNITY: theory HOL-UNITY.Comp

22:28:20 HOL-UNITY: theory HOL-UNITY.Guar

22:28:21 HOL-UNITY: theory HOL-UNITY.Extend

22:28:21 HOL-UNITY: theory HOL-UNITY.Transformers

22:28:22 Timing HOL-Predicate_Compile_Examples (2 threads, 128.423s elapsed time, 196.356s cpu time, 10.344s GC time, factor 1.53)

22:28:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples

22:28:22 Finished HOL-Predicate_Compile_Examples (0:02:14 elapsed time, 0:04:38 cpu time, factor 2.07)

22:28:22 Running HOL-SET_Protocol ...

22:28:22 HOL-UNITY: theory HOL-UNITY.ProgressSets

22:28:22 HOL-UNITY: theory HOL-UNITY.Project

22:28:22 HOL-UNITY: theory HOL-UNITY.Rename

22:28:22 HOL-UNITY: theory HOL-UNITY.ELT

22:28:23 HOL-UNITY: theory HOL-UNITY.Lift_prog

22:28:23 Corec: theory Corec.Setup

22:28:23 Corec: theory Corec.Corec

22:28:23 HOL-UNITY: theory HOL-UNITY.PPROD

22:28:23 HOL-UNITY: theory HOL-UNITY.UNITY_Main

22:28:24 HOL-UNITY: theory HOL-UNITY.AllocBase

22:28:24 HOL-UNITY: theory HOL-UNITY.Channel

22:28:24 HOL-UNITY: theory HOL-UNITY.Common

22:28:24 HOL-UNITY: theory HOL-UNITY.Alloc

22:28:24 HOL-UNITY: theory HOL-UNITY.AllocImpl

22:28:27 HOL-UNITY: theory HOL-UNITY.Client

22:28:27 HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET

22:28:27 HOL-UNITY: theory HOL-UNITY.Counter

22:28:28 HOL-UNITY: theory HOL-UNITY.Counterc

22:28:28 HOL-UNITY: theory HOL-UNITY.Handshake

22:28:28 HOL-UNITY: theory HOL-UNITY.Lift

22:28:29 HOL-UNITY: theory HOL-UNITY.Mutex

22:28:29 HOL-UNITY: theory HOL-UNITY.NSP_Bad

22:28:30 HOL-UNITY: theory HOL-UNITY.PriorityAux

22:28:30 HOL-UNITY: theory HOL-UNITY.Priority

22:28:30 HOL-UNITY: theory HOL-UNITY.Progress

22:28:31 HOL-UNITY: theory HOL-UNITY.Reach

22:28:31 HOL-UNITY: theory HOL-UNITY.TimerArray

22:28:31 HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET

22:28:31 HOL-UNITY: theory HOL-UNITY.Reachability

22:28:32 HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET

22:28:32 HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration

22:28:32 HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration

22:28:34 HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase

22:28:36 HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol

22:29:20 Timing HOL-UNITY (2 threads, 59.838s elapsed time, 102.080s cpu time, 4.636s GC time, factor 1.71)

22:29:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY

22:29:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf

22:29:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf

22:29:20 Finished HOL-UNITY (0:01:10 elapsed time, 0:01:54 cpu time, factor 1.63)

22:29:20 Running Datatypes ...

22:29:23 Timing Corec (2 threads, 57.927s elapsed time, 83.844s cpu time, 5.420s GC time, factor 1.45)

22:29:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec

22:29:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf

22:29:23 Finished Corec (0:01:06 elapsed time, 0:01:31 cpu time, factor 1.39)

22:29:23 Running HOL-Metis_Examples ...

22:29:24 Timing HOL-SET_Protocol (2 threads, 54.318s elapsed time, 101.028s cpu time, 2.368s GC time, factor 1.86)

22:29:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol

22:29:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf

22:29:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf

22:29:24 Finished HOL-SET_Protocol (0:01:02 elapsed time, 0:01:49 cpu time, factor 1.77)

22:29:24 Running HOL-Probability-ex ...

22:29:25 Datatypes: theory Datatypes.Setup

22:29:26 Datatypes: theory Datatypes.Datatypes

22:29:29 HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree

22:29:29 HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction

22:29:29 HOL-Metis_Examples: theory HOL-Metis_Examples.Dense_Linear_Order

22:29:30 HOL-Metis_Examples: theory HOL-Metis_Examples.Message

22:29:32 HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O

22:29:32 HOL-Metis_Examples: theory HOL-Metis_Examples.Sets

22:29:33 HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski

22:29:33 HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure

22:29:34 HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings

22:29:34 HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies

22:29:34 HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification

22:29:36 HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure

22:29:36 HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers

22:29:37 HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC

22:30:12 Timing HOL-Metis_Examples (2 threads, 42.116s elapsed time, 66.220s cpu time, 2.992s GC time, factor 1.57)

22:30:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples

22:30:12 Finished HOL-Metis_Examples (0:00:48 elapsed time, 0:01:25 cpu time, factor 1.79)

22:30:12 Warning: missing document directory

22:30:12 Timing HOL-Probability-ex (2 threads, 34.906s elapsed time, 55.332s cpu time, 1.376s GC time, factor 1.59)

22:30:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex

22:30:12 Finished HOL-Probability-ex (0:00:47 elapsed time, 0:01:08 cpu time, factor 1.43)

22:30:12 Running Tutorial ...

22:30:12 Running HOL-Quotient_Examples ...

22:30:14 Tutorial: theory Tutorial.ToyList_Test

22:30:15 Tutorial: theory Tutorial.AB

22:30:15 Tutorial: theory Tutorial.ABexpr

22:30:16 Tutorial: theory Tutorial.AdvancedInd

22:30:16 Tutorial: theory Tutorial.Base

22:30:16 Tutorial: theory Tutorial.CTL

22:30:17 Timing Datatypes (2 threads, 48.174s elapsed time, 68.700s cpu time, 5.044s GC time, factor 1.43)

22:30:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

22:30:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

22:30:17 Finished Datatypes (0:00:57 elapsed time, 0:01:17 cpu time, factor 1.35)

22:30:17 Running HOL-Analysis-ex ...

22:30:17 Tutorial: theory Tutorial.CTLind

22:30:18 Tutorial: theory Tutorial.PDL

22:30:18 Tutorial: theory Tutorial.CodeGen

22:30:19 Tutorial: theory Tutorial.Nested

22:30:20 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int

22:30:20 HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList

22:30:21 Tutorial: theory Tutorial.Even

22:30:21 Tutorial: theory Tutorial.Fundata

22:30:21 Tutorial: theory Tutorial.Advanced

22:30:21 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet

22:30:21 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow

22:30:22 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList

22:30:22 Tutorial: theory Tutorial.Ifexpr

22:30:22 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet

22:30:23 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun

22:30:23 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set

22:30:23 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test

22:30:23 Tutorial: theory Tutorial.Itrev

22:30:23 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message

22:30:23 Tutorial: theory Tutorial.Mutual

22:30:24 Tutorial: theory Tutorial.Option2

22:30:24 Tutorial: theory Tutorial.Plus

22:30:24 Tutorial: theory Tutorial.Star

22:30:24 Tutorial: theory Tutorial.ToyList

22:30:24 Tutorial: theory Tutorial.Tree

22:30:25 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat

22:30:25 Tutorial: theory Tutorial.Tree2

22:30:25 Tutorial: theory Tutorial.Trie

22:30:25 Tutorial: theory Tutorial.appendix

22:30:25 Tutorial: theory Tutorial.case_exprs

22:30:25 Tutorial: theory Tutorial.fakenat

22:30:26 Tutorial: theory Tutorial.fun0

22:30:27 Tutorial: theory Tutorial.natsum

22:30:27 Tutorial: theory Tutorial.pairs2

22:30:27 Tutorial: theory Tutorial.prime_def

22:30:27 Tutorial: theory Tutorial.simp

22:30:27 Tutorial: theory Tutorial.simp2

22:30:28 Tutorial: theory Tutorial.types

22:30:28 Tutorial: theory Tutorial.unfoldnested

22:30:28 HOL-Analysis-ex: theory HOL-Analysis-ex.Circle_Area

22:30:28 HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations

22:30:39 Tutorial: theory Tutorial.Message

22:30:39 Tutorial: theory Tutorial.Documents

22:30:41 Tutorial: theory Tutorial.Event

22:30:42 Tutorial: theory Tutorial.Public

22:30:43 Tutorial: theory Tutorial.NS_Public

22:30:44 Tutorial: theory Tutorial.Setup

22:30:44 Tutorial: theory Tutorial.Basic

22:30:44 Tutorial: theory Tutorial.Numbers

22:30:44 Tutorial: theory Tutorial.Blast

22:30:44 Tutorial: theory Tutorial.Force

22:30:44 Tutorial: theory Tutorial.Pairs

22:30:44 Tutorial: theory Tutorial.Records

22:30:44 Tutorial: theory Tutorial.Overloading

22:30:45 Tutorial: theory Tutorial.Axioms

22:30:45 Tutorial: theory Tutorial.Typedefs

22:30:46 Tutorial: theory Tutorial.Examples

22:30:46 Tutorial: theory Tutorial.Functions

22:30:46 Tutorial: theory Tutorial.Recur

22:30:46 Tutorial: theory Tutorial.Relations

22:30:46 Tutorial: theory Tutorial.TPrimes

22:30:47 Tutorial: theory Tutorial.Tacticals

22:30:47 Tutorial: theory Tutorial.Forward

22:30:47 Tutorial: theory Tutorial.find2

22:30:53 Timing Tutorial (2 threads, 33.428s elapsed time, 64.692s cpu time, 7.940s GC time, factor 1.94)

22:30:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial

22:30:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf

22:30:53 Finished Tutorial (0:00:40 elapsed time, 0:01:10 cpu time, factor 1.76)

22:30:53 Running HOL-Hoare ...

22:30:54 Timing HOL-Quotient_Examples (2 threads, 32.456s elapsed time, 46.188s cpu time, 2.584s GC time, factor 1.42)

22:30:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples

22:30:54 Finished HOL-Quotient_Examples (0:00:41 elapsed time, 0:01:18 cpu time, factor 1.90)

22:30:54 Running HOL-Cardinals ...

22:30:55 HOL-Hoare: theory HOL-Hoare.Heap

22:30:55 HOL-Hoare: theory HOL-Hoare.Arith2

22:30:55 HOL-Hoare: theory HOL-Hoare.Hoare_Logic

22:30:55 HOL-Hoare: theory HOL-Hoare.Hoare_Logic_Abort

22:30:57 HOL-Hoare: theory HOL-Hoare.Examples

22:30:57 HOL-Hoare: theory HOL-Hoare.HeapSyntax

22:30:57 Warning: missing document directory

22:30:57 Timing HOL-Analysis-ex (2 threads, 28.592s elapsed time, 50.944s cpu time, 0.376s GC time, factor 1.78)

22:30:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

22:30:57 Finished HOL-Analysis-ex (0:00:39 elapsed time, 0:01:01 cpu time, factor 1.56)

22:30:57 Running HOL-Induct ...

22:30:57 HOL-Hoare: theory HOL-Hoare.Pointer_Examples

22:30:57 HOL-Hoare: theory HOL-Hoare.SchorrWaite

22:30:58 HOL-Hoare: theory HOL-Hoare.Pointers0

22:30:59 HOL-Hoare: theory HOL-Hoare.ExamplesAbort

22:30:59 HOL-Hoare: theory HOL-Hoare.HeapSyntaxAbort

22:30:59 HOL-Cardinals: theory HOL-Cardinals.Order_Union

22:30:59 HOL-Cardinals: theory HOL-Cardinals.Fun_More

22:30:59 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More

22:30:59 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension

22:31:00 HOL-Hoare: theory HOL-Hoare.SepLogHeap

22:31:00 HOL-Hoare: theory HOL-Hoare.Pointer_ExamplesAbort

22:31:00 HOL-Hoare: theory HOL-Hoare.Separation

22:31:00 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More

22:31:00 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation

22:31:00 HOL-Hoare: theory HOL-Hoare.Hoare

22:31:00 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding

22:31:01 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions

22:31:02 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation

22:31:02 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic

22:31:03 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic

22:31:03 HOL-Induct: theory HOL-Induct.Common_Patterns

22:31:03 HOL-Cardinals: theory HOL-Cardinals.Cardinals

22:31:04 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set

22:31:05 HOL-Induct: theory HOL-Induct.ABexp

22:31:05 HOL-Induct: theory HOL-Induct.Com

22:31:08 HOL-Induct: theory HOL-Induct.Comb

22:31:08 HOL-Induct: theory HOL-Induct.Infinitely_Branching_Tree

22:31:10 HOL-Induct: theory HOL-Induct.Nested_Datatype

22:31:11 HOL-Induct: theory HOL-Induct.Ordinals

22:31:11 HOL-Induct: theory HOL-Induct.PropLog

22:31:12 HOL-Induct: theory HOL-Induct.QuoDataType

22:31:12 HOL-Induct: theory HOL-Induct.QuoNestedDataType

22:31:13 HOL-Induct: theory HOL-Induct.Sigma_Algebra

22:31:13 HOL-Induct: theory HOL-Induct.Term

22:31:15 HOL-Induct: theory HOL-Induct.Sexp

22:31:15 HOL-Induct: theory HOL-Induct.SList

22:31:22 Timing HOL-Cardinals (2 threads, 21.805s elapsed time, 41.556s cpu time, 1.516s GC time, factor 1.91)

22:31:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals

22:31:22 Finished HOL-Cardinals (0:00:27 elapsed time, 0:00:47 cpu time, factor 1.71)

22:31:22 Running HOL-Statespace ...

22:31:22 Timing HOL-Hoare (2 threads, 25.322s elapsed time, 50.388s cpu time, 1.324s GC time, factor 1.99)

22:31:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare

22:31:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf

22:31:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf

22:31:22 Finished HOL-Hoare (0:00:29 elapsed time, 0:00:55 cpu time, factor 1.89)

22:31:22 Running HOL-SPARK-Examples ...

22:31:24 HOL-Statespace: theory HOL-Statespace.DistinctTreeProver

22:31:24 Timing HOL-Induct (2 threads, 18.333s elapsed time, 32.908s cpu time, 2.812s GC time, factor 1.80)

22:31:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct

22:31:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf

22:31:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf

22:31:24 Finished HOL-Induct (0:00:26 elapsed time, 0:00:42 cpu time, factor 1.60)

22:31:24 Running HOL-Matrix_LP ...

22:31:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas

22:31:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD

22:31:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor

22:31:25 HOL-Statespace: theory HOL-Statespace.StateFun

22:31:25 HOL-Statespace: theory HOL-Statespace.StateSpaceLocale

22:31:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence

22:31:26 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification

22:31:26 HOL-Statespace: theory HOL-Statespace.StateSpaceSyntax

22:31:26 HOL-Statespace: theory HOL-Statespace.StateSpaceEx

22:31:26 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F

22:31:29 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash

22:31:29 HOL-Matrix_LP: theory HOL-Matrix_LP.Compute_Oracle

22:31:29 HOL-Matrix_LP: theory HOL-Matrix_LP.LP

22:31:30 HOL-Matrix_LP: theory HOL-Matrix_LP.Matrix

22:31:30 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeFloat

22:31:30 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L

22:31:31 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeHOL

22:31:31 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R

22:31:31 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeNumeral

22:31:31 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L

22:31:32 HOL-Matrix_LP: theory HOL-Matrix_LP.SparseMatrix

22:31:32 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R

22:31:32 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round

22:31:33 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L

22:31:34 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R

22:31:35 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt

22:31:35 HOL-Matrix_LP: theory HOL-Matrix_LP.Cplex

22:31:44 Timing HOL-SPARK-Examples (2 threads, 18.710s elapsed time, 32.952s cpu time, 0.856s GC time, factor 1.76)

22:31:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples

22:31:44 Finished HOL-SPARK-Examples (0:00:21 elapsed time, 0:00:35 cpu time, factor 1.66)

22:31:44 Running HOLCF-Tutorial ...

22:31:44 Timing HOL-Statespace (2 threads, 18.670s elapsed time, 21.364s cpu time, 0.696s GC time, factor 1.14)

22:31:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace

22:31:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf

22:31:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf

22:31:44 Finished HOL-Statespace (0:00:22 elapsed time, 0:00:25 cpu time, factor 1.15)

22:31:44 Running HOL-TLA-Memory ...

22:31:46 HOLCF-Tutorial: theory HOLCF-Tutorial.Domain_ex

22:31:46 HOLCF-Tutorial: theory HOLCF-Tutorial.Fixrec_ex

22:31:46 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCMemoryParams

22:31:47 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryParameters

22:31:47 HOL-TLA-Memory: theory HOL-TLA-Memory.ProcedureInterface

22:31:47 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCParameters

22:31:47 HOL-TLA-Memory: theory HOL-TLA-Memory.Memory

22:31:47 Timing HOL-Matrix_LP (2 threads, 15.188s elapsed time, 29.468s cpu time, 1.240s GC time, factor 1.94)

22:31:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP

22:31:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf

22:31:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf

22:31:47 Finished HOL-Matrix_LP (0:00:23 elapsed time, 0:00:38 cpu time, factor 1.66)

22:31:47 Running Isar_Ref ...

22:31:48 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerkParameters

22:31:48 HOL-TLA-Memory: theory HOL-TLA-Memory.RPC

22:31:49 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerk

22:31:49 HOLCF-Tutorial: theory HOLCF-Tutorial.New_Domain

22:31:49 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryImplementation

22:31:53 Isar_Ref: theory Isar_Ref.Base

22:31:53 Isar_Ref: theory Isar_Ref.Document_Preparation

22:31:53 Isar_Ref: theory Isar_Ref.First_Order_Logic

22:31:53 Isar_Ref: theory Isar_Ref.Framework

22:31:54 Isar_Ref: theory Isar_Ref.Generic

22:31:54 Isar_Ref: theory Isar_Ref.HOL_Specific

22:31:54 Isar_Ref: theory Isar_Ref.Inner_Syntax

22:31:55 Isar_Ref: theory Isar_Ref.Outer_Syntax

22:31:55 Isar_Ref: theory Isar_Ref.Preface

22:31:55 Isar_Ref: theory Isar_Ref.Proof

22:31:56 Isar_Ref: theory Isar_Ref.Proof_Script

22:31:56 Isar_Ref: theory Isar_Ref.Quick_Reference

22:31:56 Isar_Ref: theory Isar_Ref.Spec

22:31:57 Isar_Ref: theory Isar_Ref.Symbols

22:31:57 Isar_Ref: theory Isar_Ref.Synopsis

22:31:59 Timing HOL-TLA-Memory (2 threads, 12.328s elapsed time, 23.972s cpu time, 0.636s GC time, factor 1.94)

22:31:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory

22:31:59 Finished HOL-TLA-Memory (0:00:14 elapsed time, 0:00:26 cpu time, factor 1.79)

22:32:00 Running Codegen ...

22:32:04 Timing HOLCF-Tutorial (2 threads, 15.118s elapsed time, 19.436s cpu time, 0.488s GC time, factor 1.29)

22:32:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial

22:32:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf

22:32:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf

22:32:04 Finished HOLCF-Tutorial (0:00:19 elapsed time, 0:00:24 cpu time, factor 1.25)

22:32:04 Running IOA-NTP ...

22:32:05 Codegen: theory Codegen.Adaptation

22:32:05 Codegen: theory Codegen.Computations

22:32:06 Codegen: theory Codegen.Evaluation

22:32:06 Codegen: theory Codegen.Further

22:32:06 IOA-NTP: theory IOA-NTP.Lemmas

22:32:06 Codegen: theory Codegen.Inductive_Predicate

22:32:06 IOA-NTP: theory IOA-NTP.Multiset

22:32:07 IOA-NTP: theory IOA-NTP.Packet

22:32:07 IOA-NTP: theory IOA-NTP.Action

22:32:07 Codegen: theory Codegen.Introduction

22:32:09 Codegen: theory Codegen.Foundations

22:32:09 IOA-NTP: theory IOA-NTP.Abschannel

22:32:09 IOA-NTP: theory IOA-NTP.Receiver

22:32:09 Codegen: theory Codegen.Refinement

22:32:10 IOA-NTP: theory IOA-NTP.Sender

22:32:10 IOA-NTP: theory IOA-NTP.Spec

22:32:10 IOA-NTP: theory IOA-NTP.Impl

22:32:11 IOA-NTP: theory IOA-NTP.Correctness

22:32:12 Timing Isar_Ref (2 threads, 10.385s elapsed time, 16.612s cpu time, 1.072s GC time, factor 1.60)

22:32:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref

22:32:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf

22:32:12 Finished Isar_Ref (0:00:24 elapsed time, 0:00:30 cpu time, factor 1.25)

22:32:12 Running HOL-Unix ...

22:32:15 Timing IOA-NTP (2 threads, 8.298s elapsed time, 15.248s cpu time, 0.588s GC time, factor 1.84)

22:32:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP

22:32:15 Finished IOA-NTP (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.60)

22:32:15 Running HOL-NanoJava ...

22:32:17 HOL-NanoJava: theory HOL-NanoJava.Term

22:32:18 Timing Codegen (2 threads, 8.976s elapsed time, 17.684s cpu time, 0.704s GC time, factor 1.97)

22:32:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

22:32:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

22:32:18 Finished Codegen (0:00:18 elapsed time, 0:00:26 cpu time, factor 1.47)

22:32:18 Running HOLCF-IMP ...

22:32:18 HOL-Unix: theory HOL-Unix.Nested_Environment

22:32:19 HOL-Unix: theory HOL-Unix.Unix

22:32:19 HOL-NanoJava: theory HOL-NanoJava.Decl

22:32:20 HOL-NanoJava: theory HOL-NanoJava.TypeRel

22:32:20 HOLCF-IMP: theory HOLCF-IMP.AExp

22:32:20 HOL-NanoJava: theory HOL-NanoJava.State

22:32:21 HOL-NanoJava: theory HOL-NanoJava.AxSem

22:32:21 HOL-NanoJava: theory HOL-NanoJava.OpSem

22:32:22 HOLCF-IMP: theory HOLCF-IMP.BExp

22:32:22 HOL-NanoJava: theory HOL-NanoJava.Equivalence

22:32:22 HOL-NanoJava: theory HOL-NanoJava.Example

22:32:24 HOLCF-IMP: theory HOLCF-IMP.Com

22:32:25 HOLCF-IMP: theory HOLCF-IMP.Big_Step

22:32:26 HOLCF-IMP: theory HOLCF-IMP.Denotational

22:32:26 Timing HOL-NanoJava (2 threads, 6.829s elapsed time, 12.044s cpu time, 0.668s GC time, factor 1.76)

22:32:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava

22:32:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf

22:32:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf

22:32:26 Finished HOL-NanoJava (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.57)

22:32:26 Running IOA-ABP ...

22:32:26 HOLCF-IMP: theory HOLCF-IMP.HoareEx

22:32:27 Timing HOL-Unix (2 threads, 6.879s elapsed time, 11.476s cpu time, 0.656s GC time, factor 1.67)

22:32:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix

22:32:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf

22:32:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf

22:32:27 Finished HOL-Unix (0:00:14 elapsed time, 0:00:19 cpu time, factor 1.37)

22:32:27 Running Prog_Prove ...

22:32:28 Timing HOLCF-IMP (2 threads, 7.110s elapsed time, 13.472s cpu time, 0.448s GC time, factor 1.89)

22:32:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP

22:32:28 Finished HOLCF-IMP (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.63)

22:32:28 Running HOL-Isar_Examples ...

22:32:29 Prog_Prove: theory Prog_Prove.Basics

22:32:29 Prog_Prove: theory Prog_Prove.Bool_nat_list

22:32:29 Prog_Prove: theory Prog_Prove.LaTeXsugar

22:32:29 IOA-ABP: theory IOA-ABP.Lemmas

22:32:29 IOA-ABP: theory IOA-ABP.Packet

22:32:29 Prog_Prove: theory Prog_Prove.Isar

22:32:29 IOA-ABP: theory IOA-ABP.Action

22:32:30 Prog_Prove: theory Prog_Prove.Logic

22:32:31 Prog_Prove: theory Prog_Prove.MyList

22:32:31 IOA-ABP: theory IOA-ABP.Abschannel

22:32:31 IOA-ABP: theory IOA-ABP.Env

22:32:31 Prog_Prove: theory Prog_Prove.Types_and_funs

22:32:32 IOA-ABP: theory IOA-ABP.Receiver

22:32:32 IOA-ABP: theory IOA-ABP.Sender

22:32:33 IOA-ABP: theory IOA-ABP.Abschannel_finite

22:32:33 IOA-ABP: theory IOA-ABP.Spec

22:32:33 IOA-ABP: theory IOA-ABP.Impl

22:32:33 IOA-ABP: theory IOA-ABP.Impl_finite

22:32:34 IOA-ABP: theory IOA-ABP.Correctness

22:32:34 HOL-Isar_Examples: theory HOL-Isar_Examples.First_Order_Logic

22:32:34 HOL-Isar_Examples: theory HOL-Isar_Examples.Higher_Order_Logic

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Basic_Logic

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Cantor

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Drinker

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Expr_Compiler

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Group

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Context

22:32:35 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Notepad

22:32:36 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare

22:32:36 Timing IOA-ABP (2 threads, 6.671s elapsed time, 11.856s cpu time, 0.240s GC time, factor 1.78)

22:32:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP

22:32:36 Finished IOA-ABP (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.52)

22:32:36 Running HOL-Mirabelle-ex ...

22:32:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Knaster_Tarski

22:32:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Mutilated_Checkerboard

22:32:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare_Ex

22:32:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Peirce

22:32:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Puzzle

22:32:38 HOL-Isar_Examples: theory HOL-Isar_Examples.Structured_Statements

22:32:38 HOL-Isar_Examples: theory HOL-Isar_Examples.Summation

22:32:38 HOL-Isar_Examples: theory HOL-Isar_Examples.Fibonacci

22:32:38 Timing Prog_Prove (2 threads, 6.210s elapsed time, 11.996s cpu time, 0.752s GC time, factor 1.93)

22:32:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove

22:32:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf

22:32:38 Finished Prog_Prove (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.50)

22:32:38 Running HOLCF-ex ...

22:32:38 HOL-Mirabelle-ex: theory HOL-Mirabelle-ex.Ex

22:32:41 HOLCF-ex: theory HOLCF-ex.Dagstuhl

22:32:41 HOLCF-ex: theory HOLCF-ex.Focus_ex

22:32:41 HOLCF-ex: theory HOLCF-ex.Concurrency_Monad

22:32:41 HOLCF-ex: theory HOLCF-ex.Dnat

22:32:42 HOLCF-ex: theory HOLCF-ex.Domain_Proofs

22:32:43 HOLCF-ex: theory HOLCF-ex.Fix2

22:32:43 HOLCF-ex: theory HOLCF-ex.Hoare

22:32:43 Timing HOL-Isar_Examples (2 threads, 6.286s elapsed time, 12.260s cpu time, 0.692s GC time, factor 1.95)

22:32:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples

22:32:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf

22:32:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf

22:32:43 Finished HOL-Isar_Examples (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.46)

22:32:43 Running HOLCF-FOCUS ...

22:32:44 HOLCF-ex: theory HOLCF-ex.Letrec

22:32:44 HOLCF-ex: theory HOLCF-ex.Loop

22:32:44 HOLCF-ex: theory HOLCF-ex.Pattern_Match

22:32:44 HOLCF-ex: theory HOLCF-ex.Powerdomain_ex

22:32:45 Timing HOL-Mirabelle-ex (2 threads, 6.097s elapsed time, 0.032s cpu time, 0.000s GC time, factor 0.01)

22:32:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex

22:32:45 Finished HOL-Mirabelle-ex (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.21)

22:32:45 Running HOL-SPARK-Manual ...

22:32:46 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstream

22:32:46 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstreams

22:32:47 HOLCF-FOCUS: theory HOLCF-FOCUS.FOCUS

22:32:47 HOLCF-FOCUS: theory HOLCF-FOCUS.Stream_adm

22:32:47 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer

22:32:47 Timing HOLCF-ex (2 threads, 6.152s elapsed time, 12.288s cpu time, 0.496s GC time, factor 2.00)

22:32:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex

22:32:47 Finished HOLCF-ex (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.65)

22:32:47 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Complex_Types

22:32:47 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Greatest_Common_Divisor

22:32:48 Running HOL-Hahn_Banach ...

22:32:48 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc1

22:32:48 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2

22:32:48 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles

22:32:48 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer_adm

22:32:49 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference

22:32:49 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor

22:32:49 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification

22:32:53 Timing HOLCF-FOCUS (2 threads, 5.529s elapsed time, 9.164s cpu time, 0.208s GC time, factor 1.66)

22:32:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS

22:32:53 Finished HOLCF-FOCUS (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.41)

22:32:53 Running HOL-IMPP ...

22:32:53 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Zorn_Lemma

22:32:53 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Continuum_Not_Denumerable

22:32:54 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Bounds

22:32:54 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Vector_Space

22:32:54 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Linearform

22:32:54 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Subspace

22:32:54 HOL-IMPP: theory HOL-IMPP.Com

22:32:55 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Order

22:32:55 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Normed_Space

22:32:56 Timing HOL-SPARK-Manual (2 threads, 4.710s elapsed time, 8.944s cpu time, 0.240s GC time, factor 1.90)

22:32:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual

22:32:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf

22:32:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf

22:32:56 Finished HOL-SPARK-Manual (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.57)

22:32:56 Running HOL-TPTP ...

22:32:56 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Norm

22:32:56 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas

22:32:56 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas

22:32:56 HOL-IMPP: theory HOL-IMPP.Natural

22:32:57 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Lemmas

22:32:57 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach

22:32:57 HOL-IMPP: theory HOL-IMPP.Hoare

22:32:58 HOL-IMPP: theory HOL-IMPP.Misc

22:32:58 HOL-IMPP: theory HOL-IMPP.EvenOdd

22:33:00 Timing HOL-IMPP (2 threads, 4.455s elapsed time, 7.476s cpu time, 0.184s GC time, factor 1.68)

22:33:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP

22:33:00 Finished HOL-IMPP (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.45)

22:33:00 Running HOL-ZF ...

22:33:01 Timing HOL-Hahn_Banach (2 threads, 4.660s elapsed time, 8.948s cpu time, 0.244s GC time, factor 1.92)

22:33:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

22:33:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

22:33:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

22:33:01 Finished HOL-Hahn_Banach (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.42)

22:33:01 Running Implementation ...

22:33:01 HOL-TPTP: theory HOL-TPTP.TPTP_Parser

22:33:01 HOL-TPTP: theory HOL-TPTP.MaSh_Export_Base

22:33:01 HOL-TPTP: theory HOL-TPTP.MaSh_Eval

22:33:02 HOL-TPTP: theory HOL-TPTP.ATP_Theory_Export

22:33:02 HOL-TPTP: theory HOL-TPTP.THF_Arith

22:33:03 Implementation: theory Implementation.Base

22:33:03 Implementation: theory Implementation.Eq

22:33:03 Implementation: theory Implementation.Integration

22:33:03 Implementation: theory Implementation.Isar

22:33:03 Implementation: theory Implementation.Local_Theory

22:33:03 Implementation: theory Implementation.ML

22:33:03 Implementation: theory Implementation.Prelim

22:33:04 HOL-TPTP: theory HOL-TPTP.TPTP_Interpret

22:33:04 Implementation: theory Implementation.Proof

22:33:04 Implementation: theory Implementation.Syntax

22:33:04 Implementation: theory Implementation.Tactic

22:33:04 HOL-TPTP: theory HOL-TPTP.TPTP_Proof_Reconstruction

22:33:05 HOL-TPTP: theory HOL-TPTP.ATP_Problem_Import

22:33:05 HOL-ZF: theory HOL-ZF.LProd

22:33:05 HOL-ZF: theory HOL-ZF.HOLZF

22:33:06 Implementation: theory Implementation.Logic

22:33:06 HOL-ZF: theory HOL-ZF.Zet

22:33:06 Timing HOL-TPTP (2 threads, 4.480s elapsed time, 5.752s cpu time, 0.112s GC time, factor 1.28)

22:33:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP

22:33:06 Finished HOL-TPTP (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.12)

22:33:06 Running Functions ...

22:33:06 HOL-ZF: theory HOL-ZF.MainZF

22:33:07 HOL-ZF: theory HOL-ZF.Games

22:33:08 Functions: theory Functions.Functions

22:33:10 Timing Implementation (2 threads, 3.798s elapsed time, 6.576s cpu time, 0.084s GC time, factor 1.73)

22:33:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation

22:33:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf

22:33:10 Finished Implementation (0:00:09 elapsed time, 0:00:11 cpu time, factor 1.27)

22:33:10 Running HOL-Nonstandard_Analysis-Examples ...

22:33:12 Timing HOL-ZF (2 threads, 4.229s elapsed time, 8.076s cpu time, 0.220s GC time, factor 1.91)

22:33:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF

22:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf

22:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf

22:33:12 Finished HOL-ZF (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.38)

22:33:12 Running HOL-IOA ...

22:33:13 Timing Functions (2 threads, 3.063s elapsed time, 4.240s cpu time, 0.192s GC time, factor 1.38)

22:33:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions

22:33:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

22:33:13 Finished Functions (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.13)

22:33:13 Running HOL-Lattice ...

22:33:14 HOL-IOA: theory HOL-IOA.Asig

22:33:14 HOL-IOA: theory HOL-IOA.IOA

22:33:15 HOL-IOA: theory HOL-IOA.Solve

22:33:15 HOL-Lattice: theory HOL-Lattice.Orders

22:33:16 HOL-Lattice: theory HOL-Lattice.Bounds

22:33:17 HOL-Lattice: theory HOL-Lattice.Lattice

22:33:17 Timing HOL-IOA (2 threads, 2.590s elapsed time, 4.216s cpu time, 0.116s GC time, factor 1.63)

22:33:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA

22:33:17 Finished HOL-IOA (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.32)

22:33:17 Running Classes ...

22:33:17 HOL-Lattice: theory HOL-Lattice.CompleteLattice

22:33:17 HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes

22:33:19 Classes: theory Classes.Setup

22:33:19 Classes: theory Classes.Classes

22:33:20 Timing HOL-Lattice (2 threads, 2.537s elapsed time, 3.976s cpu time, 0.000s GC time, factor 1.57)

22:33:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice

22:33:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf

22:33:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf

22:33:20 Finished HOL-Lattice (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.34)

22:33:20 Running HOL-TLA-Inc ...

22:33:21 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 3.077s elapsed time, 4.012s cpu time, 0.160s GC time, factor 1.30)

22:33:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples

22:33:21 Finished HOL-Nonstandard_Analysis-Examples (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.08)

22:33:21 Running Locales ...

22:33:22 HOL-TLA-Inc: theory HOL-TLA-Inc.Inc

22:33:23 Locales: theory Locales.Examples

22:33:24 Timing Classes (2 threads, 2.368s elapsed time, 2.644s cpu time, 0.000s GC time, factor 1.12)

22:33:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes

22:33:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf

22:33:24 Finished Classes (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00)

22:33:24 Running HOL-Word-Examples ...

22:33:24 Locales: theory Locales.Examples1

22:33:24 Locales: theory Locales.Examples2

22:33:24 Locales: theory Locales.Examples3

22:33:25 Timing HOL-TLA-Inc (2 threads, 2.274s elapsed time, 4.060s cpu time, 0.076s GC time, factor 1.79)

22:33:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc

22:33:25 Finished HOL-TLA-Inc (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.39)

22:33:25 Running IOA-Storage ...

22:33:26 HOL-Word-Examples: theory HOL-Word-Examples.WordBitwise

22:33:27 HOL-Word-Examples: theory HOL-Word-Examples.WordExamples

22:33:27 IOA-Storage: theory IOA-Storage.Action

22:33:28 Timing Locales (2 threads, 2.021s elapsed time, 3.164s cpu time, 0.000s GC time, factor 1.57)

22:33:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales

22:33:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf

22:33:28 Finished Locales (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.14)

22:33:28 Running Eisbach ...

22:33:28 IOA-Storage: theory IOA-Storage.Impl

22:33:28 IOA-Storage: theory IOA-Storage.Spec

22:33:28 IOA-Storage: theory IOA-Storage.Correctness

22:33:29 Timing HOL-Word-Examples (2 threads, 2.001s elapsed time, 3.736s cpu time, 0.076s GC time, factor 1.87)

22:33:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-Examples

22:33:29 Finished HOL-Word-Examples (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.35)

22:33:29 Running Main ...

22:33:30 Eisbach: theory Eisbach.Base

22:33:30 Timing IOA-Storage (2 threads, 1.727s elapsed time, 2.568s cpu time, 0.000s GC time, factor 1.49)

22:33:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage

22:33:30 Finished IOA-Storage (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.16)

22:33:30 Running HOL-Proofs-ex ...

22:33:30 Eisbach: theory Eisbach.Preface

22:33:30 Eisbach: theory Eisbach.Manual

22:33:31 Main: theory Main.Main_Doc

22:33:32 HOL-Proofs-ex: theory HOL-Proofs-ex.Hilbert_Classical

22:33:32 HOL-Proofs-ex: theory HOL-Proofs-ex.Drinker

22:33:32 HOL-Proofs-ex: theory HOL-Proofs-ex.Proof_Terms

22:33:32 HOL-Proofs-ex: theory HOL-Proofs-ex.XML_Data

22:33:33 Timing Main (2 threads, 1.380s elapsed time, 1.460s cpu time, 0.000s GC time, factor 1.06)

22:33:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main

22:33:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf

22:33:33 Finished Main (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.97)

22:33:33 Running HOL-Import ...

22:33:34 Timing Eisbach (2 threads, 1.659s elapsed time, 2.232s cpu time, 0.000s GC time, factor 1.35)

22:33:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach

22:33:34 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf

22:33:34 Finished Eisbach (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.05)

22:33:34 Running HOL-Nunchaku ...

22:33:34 Timing HOL-Proofs-ex (2 threads, 1.366s elapsed time, 2.360s cpu time, 0.000s GC time, factor 1.73)

22:33:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex

22:33:34 Finished HOL-Proofs-ex (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.21)

22:33:34 Running HOL-Types_To_Sets ...

22:33:35 HOL-Import: theory HOL-Import.Import_Setup

22:33:35 HOL-Import: theory HOL-Import.HOL_Light_Maps

22:33:36 HOL-Nunchaku: theory HOL-Nunchaku.Nunchaku

22:33:36 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites

22:33:36 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets

22:33:36 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite

22:33:36 HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces

22:33:37 Warning: missing document directory

22:33:37 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

22:33:37 Timing HOL-Import (2 threads, 1.127s elapsed time, 1.816s cpu time, 0.000s GC time, factor 1.61)

22:33:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import

22:33:37 Finished HOL-Import (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.19)

22:33:37 Running Sugar ...

22:33:37 Timing HOL-Nunchaku (2 threads, 1.170s elapsed time, 1.236s cpu time, 0.000s GC time, factor 1.06)

22:33:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nunchaku

22:33:37 Finished HOL-Nunchaku (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.99)

22:33:37 Running IOA-ex ...

22:33:38 Timing HOL-Types_To_Sets (2 threads, 1.193s elapsed time, 1.828s cpu time, 0.000s GC time, factor 1.53)

22:33:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets

22:33:38 Finished HOL-Types_To_Sets (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.18)

22:33:38 Running HOL-TLA-Buffer ...

22:33:39 Sugar: theory Sugar.LaTeXsugar

22:33:39 Sugar: theory Sugar.OptionalSugar

22:33:39 Sugar: theory Sugar.Sugar

22:33:40 HOL-TLA-Buffer: theory HOL-TLA-Buffer.Buffer

22:33:40 HOL-TLA-Buffer: theory HOL-TLA-Buffer.DBuffer

22:33:40 IOA-ex: theory IOA-ex.TrivEx2

22:33:40 IOA-ex: theory IOA-ex.TrivEx

22:33:41 Timing HOL-TLA-Buffer (2 threads, 0.756s elapsed time, 1.224s cpu time, 0.000s GC time, factor 1.62)

22:33:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer

22:33:41 Finished HOL-TLA-Buffer (0:00:02 elapsed time, 0:00:03 cpu time)

22:33:41 Running JEdit ...

22:33:41 Timing Sugar (2 threads, 1.106s elapsed time, 1.304s cpu time, 0.000s GC time, factor 1.18)

22:33:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar

22:33:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

22:33:41 Finished Sugar (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.98)

22:33:41 Timing IOA-ex (2 threads, 0.896s elapsed time, 1.848s cpu time, 0.000s GC time, factor 2.06)

22:33:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex

22:33:41 Finished IOA-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.24)

22:33:41 Running HOL-Mutabelle ...

22:33:41 Running How_to_Prove_it ...

22:33:43 JEdit: theory JEdit.Base

22:33:43 JEdit: theory JEdit.JEdit

22:33:43 How_to_Prove_it: theory How_to_Prove_it.How_to_Prove_it

22:33:45 Timing How_to_Prove_it (2 threads, 0.496s elapsed time, 0.640s cpu time, 0.000s GC time, factor 1.29)

22:33:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it

22:33:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

22:33:45 Finished How_to_Prove_it (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.98)

22:33:45 Running Typeclass_Hierarchy ...

22:33:47 HOL-Mutabelle: theory HOL-Mutabelle.MutabelleExtra

22:33:48 Timing HOL-Mutabelle (2 threads, 0.610s elapsed time, 0.688s cpu time, 0.000s GC time, factor 1.13)

22:33:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle

22:33:48 Finished HOL-Mutabelle (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.00)

22:33:48 Running HOL-Prolog ...

22:33:50 HOL-Prolog: theory HOL-Prolog.HOHH

22:33:50 HOL-Prolog: theory HOL-Prolog.Func

22:33:50 HOL-Prolog: theory HOL-Prolog.Test

22:33:50 HOL-Prolog: theory HOL-Prolog.Type

22:33:51 Timing HOL-Prolog (2 threads, 0.235s elapsed time, 0.408s cpu time, 0.000s GC time, factor 1.74)

22:33:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog

22:33:51 Finished HOL-Prolog (0:00:02 elapsed time)

22:33:51 Typeclass_Hierarchy: theory Typeclass_Hierarchy.Typeclass_Hierarchy

22:33:53 Timing JEdit (2 threads, 0.758s elapsed time, 0.804s cpu time, 0.000s GC time, factor 1.06)

22:33:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit

22:33:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

22:33:53 Finished JEdit (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.97)

22:33:54 Timing Typeclass_Hierarchy (2 threads, 0.324s elapsed time, 0.412s cpu time, 0.000s GC time, factor 1.27)

22:33:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy

22:33:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

22:33:54 Finished Typeclass_Hierarchy (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.98)

22:33:54

22:33:54 === TIMING ===

22:33:54

22:33:54 Group doc: 0:04:54 elapsed time, 0:06:33 cpu time, factor 1.34

22:33:54 Group timing: 2:17:26 elapsed time, 3:57:39 cpu time, factor 1.73

22:33:54 Group ZF: 0:01:50 elapsed time, 0:03:06 cpu time, factor 1.69

22:33:54 Group main: 0:33:59 elapsed time, 0:58:42 cpu time, factor 1.73

22:33:54 Overall: 1:01:45 elapsed time, 5:14:27 cpu time, factor 5.09

22:33:54 Archiving artifacts

22:33:54 Started calculate disk usage of build

22:33:54 Finished Calculation of disk usage of build in 0 seconds

22:33:56 Started calculate disk usage of workspace

22:33:56 Finished Calculation of disk usage of workspace in 0 seconds

22:33:56 No emails were triggered.

22:33:56 Finished: SUCCESS