Skip to content
Success

Console Output

17:56:16 Started by upstream project "isabelle-repo" build number 664

17:56:16 originally caused by:

17:56:16 Started by an SCM change

17:56:16 [EnvInject] - Loading node environment variables.

17:56:16 Building remotely on workermta4 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

17:56:16 [isabelle-repo-makeall] $ hg showconfig paths.default

17:56:16 [isabelle-repo-makeall] $ hg pull --rev 3b33d2fc5fc01a66d96f0d914168f0061bb89e8e

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

17:56:17 searching for changes

17:56:17 adding changesets

17:56:17 adding manifests

17:56:17 adding file changes

17:56:17 added 1 changesets with 8 changes to 8 files

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

17:56:17 [isabelle-repo-makeall] $ hg update --clean --rev 3b33d2fc5fc01a66d96f0d914168f0061bb89e8e

17:56:17 8 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

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

17:56:17 No emails were triggered.

17:56:17 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson4424050818805799764.sh

17:56:17 + Admin/jenkins/run_build makeall

17:56:17 + set -e

17:56:17 + PROFILE=makeall

17:56:17 + shift

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

17:56:17 + bin/isabelle jedit -bf

17:56:17 ### Building Isabelle/Scala ...

17:58:35 ### Building Isabelle/jEdit ...

17:59:02 + bin/isabelle ci_build_makeall

17:59:06

17:59:06 === CONFIGURATION ===

17:59:06

17:59:06 ISABELLE_BUILD_OPTIONS=""

17:59:06

17:59:06 ML_PLATFORM="x86_64-linux"

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

17:59:06 ML_SYSTEM="polyml-5.6"

17:59:06 ML_OPTIONS="-H 4000 --maxheap 8G"

17:59:07

17:59:07 === BUILD ===

17:59:07

17:59:07 Build started at Tue, 3 Jan 2017 16:59:06 GMT

17:59:07 Isabelle id 3b33d2fc5fc0

17:59:07

17:59:07 === LOG ===

17:59:07

17:59:07 Session Pure/Pure

17:59:07 Session CCL/CCL

17:59:08 Session CTT/CTT

17:59:08 Session Cube/Cube

17:59:08 Session FOL/FOL

17:59:08 Session FOL/FOL-ex

17:59:08 Session FOLP/FOLP

17:59:08 Session FOLP/FOLP-ex

17:59:08 Session HOL/HOL (main)

17:59:08 Session Doc/Classes (doc)

17:59:08 Session Doc/Codegen_Basics

17:59:08 Session Doc/Codegen (doc)

17:59:08 Session Doc/Corec (doc)

17:59:08 Session Doc/Datatypes (doc)

17:59:08 Session Doc/Functions (doc)

17:59:08 Session HOL/HOL-Algebra (main timing)

17:59:09 Session HOL/HOL-Analysis (main timing)

17:59:09 Session HOL/HOL-Analysis-ex

17:59:09 Session HOL/HOL-Probability (timing)

17:59:09 Session HOL/HOL-Probability-ex (timing)

17:59:09 Session HOL/HOL-Auth (timing)

17:59:09 Session HOL/HOL-UNITY (timing)

17:59:09 Session HOL/HOL-Bali (timing)

17:59:09 Session HOL/HOL-Cardinals (timing)

17:59:09 Session HOL/HOL-Corec_Examples (timing)

17:59:09 Session HOL/HOL-Data_Structures (timing)

17:59:10 Session HOL/HOL-Datatype_Examples (timing)

17:59:10 Session HOL/HOL-Decision_Procs (timing)

17:59:10 Session HOL/HOL-Eisbach

17:59:10 Session Doc/Eisbach (doc)

17:59:10 Session HOL/HOL-Hahn_Banach

17:59:10 Session HOL/HOL-Hoare

17:59:10 Session HOL/HOL-Hoare_Parallel (timing)

17:59:10 Session HOL/HOL-IMP (timing)

17:59:10 Session HOL/HOL-IMPP

17:59:10 Session HOL/HOL-IOA

17:59:10 Session HOL/HOL-Imperative_HOL

17:59:10 Session HOL/HOL-Import

17:59:10 Session HOL/HOL-Induct

17:59:10 Session HOL/HOL-Isar_Examples

17:59:10 Session HOL/HOL-Lattice

17:59:10 Session HOL/HOL-Library (main timing)

17:59:11 Session HOL/HOL-Codegenerator_Test

17:59:11 Session HOL/HOL-Matrix_LP

17:59:11 Session HOL/HOL-Metis_Examples (timing)

17:59:11 Session HOL/HOL-MicroJava (timing)

17:59:11 Session HOL/HOL-Mirabelle

17:59:11 Session HOL/HOL-Mirabelle-ex

17:59:11 Session HOL/HOL-Mutabelle

17:59:11 Session HOL/HOL-NanoJava

17:59:11 Session HOL/HOL-Nitpick_Examples

17:59:11 Session HOL/HOL-Nominal

17:59:11 Session HOL/HOL-Nominal-Examples (timing)

17:59:11 Session HOL/HOL-Nonstandard_Analysis (timing)

17:59:11 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

17:59:11 Session HOL/HOL-Number_Theory (timing)

17:59:12 Session HOL/HOL-Nunchaku

17:59:12 Session HOL/HOL-Predicate_Compile_Examples (timing)

17:59:12 Session HOL/HOL-Prolog

17:59:12 Session HOL/HOL-Quickcheck_Examples (timing)

17:59:12 Session HOL/HOL-Quotient_Examples (timing)

17:59:12 Session HOL/HOL-SET_Protocol (timing)

17:59:12 Session HOL/HOL-Statespace

17:59:12 Session HOL/HOL-TLA

17:59:12 Session HOL/HOL-TLA-Buffer

17:59:12 Session HOL/HOL-TLA-Inc

17:59:12 Session HOL/HOL-TLA-Memory

17:59:12 Session HOL/HOL-TPTP

17:59:12 Session HOL/HOL-Types_To_Sets

17:59:12 Session HOL/HOL-Unix

17:59:12 Session HOL/HOL-Word (main timing)

17:59:12 Session HOL/HOL-SPARK (main)

17:59:12 Session HOL/HOL-SPARK-Examples

17:59:12 Session HOL/HOL-SPARK-Manual

17:59:12 Session HOL/HOL-Word-Examples

17:59:12 Session HOL/HOL-Word-SMT_Examples (timing)

17:59:12 Session HOL/HOL-ZF

17:59:13 Session HOL/HOL-ex

17:59:13 Session HOL/HOLCF (main timing)

17:59:13 Session HOL/HOLCF-FOCUS

17:59:13 Session HOL/HOLCF-IMP

17:59:13 Session HOL/HOLCF-Library

17:59:13 Session HOL/HOLCF-Tutorial

17:59:13 Session HOL/HOLCF-ex

17:59:13 Session HOL/IOA (timing)

17:59:13 Session HOL/IOA-ABP

17:59:13 Session HOL/IOA-NTP

17:59:13 Session HOL/IOA-Storage

17:59:13 Session HOL/IOA-ex

17:59:13 Session Doc/How_to_Prove_it

17:59:13 Session Doc/Implementation (doc)

17:59:13 Session Doc/Isar_Ref (doc)

17:59:13 Session Doc/JEdit (doc)

17:59:13 Session Doc/Locales (doc)

17:59:13 Session Doc/Main (doc)

17:59:13 Session Doc/Prog_Prove (doc)

17:59:13 Session Doc/Sugar (doc)

17:59:13 Session Doc/Tutorial (doc)

17:59:13 Session Doc/Typeclass_Hierarchy_Basics

17:59:13 Session Doc/Typeclass_Hierarchy (doc)

17:59:13 Session HOL/HOL-Proofs (timing)

17:59:14 Session HOL/HOL-Proofs-Extraction (timing)

17:59:14 Session HOL/HOL-Proofs-Lambda (timing)

17:59:14 Session HOL/HOL-Proofs-ex

17:59:14 Session Doc/Intro (doc)

17:59:14 Session LCF/LCF

17:59:14 Session Doc/Logics (doc)

17:59:14 Session Doc/Nitpick (doc)

17:59:14 Session Unsorted/SML

17:59:14 Session Sequents/Sequents

17:59:14 Session Doc/Sledgehammer (doc)

17:59:14 Session Unsorted/Spec_Check

17:59:14 Session Doc/System (doc)

17:59:14 Session ZF/ZF (main timing ZF)

17:59:14 Session Doc/Logics_ZF (doc)

17:59:14 Session ZF/ZF-AC (ZF)

17:59:14 Session ZF/ZF-Coind (ZF)

17:59:14 Session ZF/ZF-Constructible (ZF)

17:59:14 Session ZF/ZF-IMP (ZF)

17:59:14 Session ZF/ZF-Induct (ZF)

17:59:14 Session ZF/ZF-Resid (ZF)

17:59:14 Session ZF/ZF-UNITY (timing ZF)

17:59:14 Session ZF/ZF-ex (ZF)

17:59:15 Cleaning Pure ...

17:59:15 Cleaning SML ...

17:59:15 Cleaning Sequents ...

17:59:15 Cleaning Sledgehammer ...

17:59:15 Cleaning Spec_Check ...

17:59:15 Cleaning System ...

17:59:15 Cleaning ZF ...

17:59:15 Cleaning ZF-AC ...

17:59:15 Cleaning ZF-Coind ...

17:59:15 Cleaning ZF-Constructible ...

17:59:15 Cleaning ZF-IMP ...

17:59:15 Cleaning ZF-Induct ...

17:59:15 Cleaning ZF-Resid ...

17:59:15 Cleaning ZF-UNITY ...

17:59:15 Cleaning ZF-ex ...

17:59:15 Cleaning Nitpick ...

17:59:15 Cleaning Logics_ZF ...

17:59:15 Cleaning Logics ...

17:59:15 Cleaning LCF ...

17:59:15 Cleaning Intro ...

17:59:15 Cleaning HOL-Proofs ...

17:59:15 Cleaning HOL-Proofs-Extraction ...

17:59:15 Cleaning HOL-Proofs-Lambda ...

17:59:15 Cleaning HOL-Proofs-ex ...

17:59:15 Cleaning HOL ...

17:59:15 Cleaning HOL-Algebra ...

17:59:15 Cleaning HOL-Analysis ...

17:59:15 Cleaning HOL-Analysis-ex ...

17:59:15 Cleaning HOL-Probability ...

17:59:15 Cleaning HOL-Probability-ex ...

17:59:15 Cleaning HOL-Auth ...

17:59:15 Cleaning HOL-UNITY ...

17:59:15 Cleaning HOL-Bali ...

17:59:15 Cleaning HOL-Cardinals ...

17:59:15 Cleaning HOL-Corec_Examples ...

17:59:15 Cleaning HOL-Data_Structures ...

17:59:15 Cleaning HOL-Datatype_Examples ...

17:59:15 Cleaning HOL-Decision_Procs ...

17:59:15 Cleaning HOL-Eisbach ...

17:59:15 Cleaning HOL-Hahn_Banach ...

17:59:15 Cleaning HOL-Hoare ...

17:59:15 Cleaning HOL-Hoare_Parallel ...

17:59:15 Cleaning HOL-IMP ...

17:59:15 Cleaning HOL-IMPP ...

17:59:15 Cleaning HOL-IOA ...

17:59:15 Cleaning HOL-Imperative_HOL ...

17:59:15 Cleaning HOL-Import ...

17:59:15 Cleaning HOL-Induct ...

17:59:15 Cleaning HOL-Isar_Examples ...

17:59:15 Cleaning HOL-Lattice ...

17:59:15 Cleaning HOL-Library ...

17:59:16 Cleaning HOL-Codegenerator_Test ...

17:59:16 Cleaning HOL-Matrix_LP ...

17:59:16 Cleaning HOL-Metis_Examples ...

17:59:16 Cleaning HOL-MicroJava ...

17:59:16 Cleaning HOL-Mirabelle ...

17:59:16 Cleaning HOL-Mirabelle-ex ...

17:59:16 Cleaning HOL-Mutabelle ...

17:59:16 Cleaning HOL-NanoJava ...

17:59:16 Cleaning HOL-Nitpick_Examples ...

17:59:16 Cleaning HOL-Nominal ...

17:59:16 Cleaning HOL-Nominal-Examples ...

17:59:16 Cleaning HOL-Nonstandard_Analysis ...

17:59:16 Cleaning HOL-Nonstandard_Analysis-Examples ...

17:59:16 Cleaning HOL-Number_Theory ...

17:59:16 Cleaning HOL-Nunchaku ...

17:59:16 Cleaning HOL-Predicate_Compile_Examples ...

17:59:16 Cleaning HOL-Prolog ...

17:59:16 Cleaning HOL-Quickcheck_Examples ...

17:59:16 Cleaning HOL-Quotient_Examples ...

17:59:16 Cleaning HOL-SET_Protocol ...

17:59:16 Cleaning HOL-Statespace ...

17:59:16 Cleaning HOL-TLA ...

17:59:16 Cleaning HOL-TLA-Buffer ...

17:59:16 Cleaning HOL-TLA-Inc ...

17:59:16 Cleaning HOL-TLA-Memory ...

17:59:16 Cleaning HOL-TPTP ...

17:59:16 Cleaning HOL-Types_To_Sets ...

17:59:16 Cleaning HOL-Unix ...

17:59:16 Cleaning HOL-Word ...

17:59:16 Cleaning HOL-SPARK ...

17:59:16 Cleaning HOL-SPARK-Examples ...

17:59:16 Cleaning HOL-SPARK-Manual ...

17:59:16 Cleaning HOL-Word-Examples ...

17:59:16 Cleaning HOL-Word-SMT_Examples ...

17:59:16 Cleaning HOL-ZF ...

17:59:16 Cleaning HOL-ex ...

17:59:16 Cleaning HOLCF ...

17:59:16 Cleaning HOLCF-FOCUS ...

17:59:16 Cleaning HOLCF-IMP ...

17:59:16 Cleaning HOLCF-Library ...

17:59:16 Cleaning HOLCF-Tutorial ...

17:59:16 Cleaning HOLCF-ex ...

17:59:16 Cleaning IOA ...

17:59:16 Cleaning IOA-ABP ...

17:59:16 Cleaning IOA-NTP ...

17:59:16 Cleaning IOA-Storage ...

17:59:16 Cleaning IOA-ex ...

17:59:16 Cleaning How_to_Prove_it ...

17:59:16 Cleaning Implementation ...

17:59:16 Cleaning Isar_Ref ...

17:59:16 Cleaning JEdit ...

17:59:16 Cleaning Locales ...

17:59:16 Cleaning Main ...

17:59:16 Cleaning Prog_Prove ...

17:59:16 Cleaning Sugar ...

17:59:16 Cleaning Tutorial ...

17:59:16 Cleaning Typeclass_Hierarchy_Basics ...

17:59:16 Cleaning Typeclass_Hierarchy ...

17:59:16 Cleaning Functions ...

17:59:16 Cleaning FOLP ...

17:59:16 Cleaning FOLP-ex ...

17:59:16 Cleaning FOL ...

17:59:16 Cleaning FOL-ex ...

17:59:16 Cleaning Eisbach ...

17:59:16 Cleaning Datatypes ...

17:59:16 Cleaning Cube ...

17:59:16 Cleaning Corec ...

17:59:16 Cleaning Codegen_Basics ...

17:59:16 Cleaning Codegen ...

17:59:16 Cleaning Classes ...

17:59:16 Cleaning CTT ...

17:59:16 Cleaning CCL ...

17:59:16 Building Pure ...

17:59:27 Pure: theory Pure

17:59:28 Pure: theory ML_Bootstrap

17:59:31 Warning: missing document directory

17:59:31 Timing Pure (1 threads, 0.524s elapsed time, 0.524s cpu time, 0.000s GC time, factor 1.00)

17:59:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

17:59:31 Finished Pure (0:00:14 elapsed time, 0:00:14 cpu time, factor 0.99)

17:59:31 Building HOL ...

17:59:31 Building ZF ...

17:59:31 Building HOL-Proofs ...

17:59:32 ZF: theory IFOL

17:59:32 HOL-Proofs: theory Proofs

17:59:32 HOL-Proofs: theory Code_Generator

17:59:32 HOL: theory Code_Generator

17:59:33 ZF: theory FOL

17:59:34 ZF: theory ZF

17:59:34 ZF: theory upair

17:59:35 HOL-Proofs: theory HOL

17:59:35 ZF: theory pair

17:59:35 HOL: theory HOL

17:59:35 ZF: theory Bool

17:59:35 ZF: theory equalities

17:59:35 ZF: theory Fixedpt

17:59:35 ZF: theory Sum

17:59:35 ZF: theory func

17:59:36 ZF: theory Perm

17:59:36 ZF: theory QPair

17:59:36 ZF: theory Trancl

17:59:36 ZF: theory EquivClass

17:59:36 ZF: theory WF

17:59:37 ZF: theory Order

17:59:37 ZF: theory Ordinal

17:59:37 ZF: theory OrdQuant

17:59:37 ZF: theory OrderArith

17:59:37 ZF: theory Nat_ZF

17:59:37 ZF: theory Epsilon

17:59:37 ZF: theory OrderType

17:59:37 ZF: theory Inductive_ZF

17:59:38 ZF: theory Finite

17:59:38 ZF: theory Cardinal

17:59:38 HOL: theory Argo

17:59:38 HOL: theory Ctr_Sugar

17:59:38 ZF: theory Univ

17:59:39 HOL-Proofs: theory Argo

17:59:39 HOL-Proofs: theory Ctr_Sugar

17:59:39 ZF: theory Arith

17:59:39 ZF: theory QUniv

17:59:39 ZF: theory Datatype_ZF

17:59:39 HOL: theory Orderings

17:59:39 ZF: theory ArithSimp

17:59:39 HOL-Proofs: theory Orderings

17:59:39 ZF: theory Int_ZF

17:59:39 ZF: theory CardinalArith

17:59:40 ZF: theory List_ZF

17:59:40 HOL: theory SAT

17:59:40 ZF: theory Bin

17:59:40 HOL-Proofs: theory SAT

17:59:40 ZF: theory IntDiv_ZF

17:59:41 HOL: theory Groups

17:59:41 ZF: theory Main_ZF

17:59:41 ZF: theory AC

17:59:41 ZF: theory Zorn

17:59:41 HOL-Proofs: theory Groups

17:59:41 ZF: theory Cardinal_AC

17:59:41 ZF: theory Main

17:59:42 ZF: theory InfDatatype

17:59:42 ZF: theory Main_ZFC

17:59:43 HOL: theory Lattices

17:59:45 HOL-Proofs: theory Lattices

17:59:45 HOL: theory Set

17:59:47 HOL: theory Fun

17:59:47 HOL: theory Typedef

17:59:47 HOL: theory Rings

17:59:47 HOL: theory Complete_Lattices

17:59:48 HOL-Proofs: theory Set

17:59:50 HOL: theory Inductive

17:59:51 HOL: theory Product_Type

17:59:53 HOL: theory Complete_Partial_Order

17:59:53 HOL: theory Sum_Type

17:59:53 HOL-Proofs: theory Fun

17:59:54 HOL-Proofs: theory Typedef

17:59:54 HOL-Proofs: theory Rings

17:59:56 HOL-Proofs: theory Complete_Lattices

17:59:56 HOL: theory Nat

17:59:58 HOL: theory Fields

17:59:59 HOL: theory Meson

17:59:59 HOL: theory ATP

18:00:00 HOL-Proofs: theory Inductive

18:00:01 HOL: theory Metis

18:00:02 HOL-Proofs: theory Product_Type

18:00:04 HOL: theory Finite_Set

18:00:04 HOL-Proofs: theory Complete_Partial_Order

18:00:04 HOL: theory Relation

18:00:05 HOL-Proofs: theory Sum_Type

18:00:05 Timing ZF (2 threads, 21.118s elapsed time, 34.348s cpu time, 2.356s GC time, factor 1.63)

18:00:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF

18:00:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf

18:00:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf

18:00:05 Finished ZF (0:00:33 elapsed time, 0:00:55 cpu time, factor 1.65)

18:00:05 Building FOL ...

18:00:05 HOL: theory Transitive_Closure

18:00:05 FOL: theory IFOL

18:00:06 FOL: theory FOL

18:00:06 HOL: theory Wellfounded

18:00:07 HOL: theory Fun_Def_Base

18:00:07 HOL: theory Hilbert_Choice

18:00:07 HOL: theory Wfrec

18:00:07 HOL: theory Order_Relation

18:00:08 HOL: theory BNF_Wellorder_Relation

18:00:08 HOL: theory Zorn

18:00:08 HOL-Proofs: theory Nat

18:00:08 HOL: theory BNF_Wellorder_Embedding

18:00:08 HOL: theory BNF_Wellorder_Constructions

18:00:09 HOL: theory BNF_Cardinal_Order_Relation

18:00:09 HOL: theory BNF_Cardinal_Arithmetic

18:00:10 HOL: theory BNF_Def

18:00:10 Timing FOL (2 threads, 2.520s elapsed time, 2.884s cpu time, 0.160s GC time, factor 1.14)

18:00:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL

18:00:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf

18:00:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf

18:00:10 Finished FOL (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.26)

18:00:10 Building FOLP ...

18:00:10 FOLP: theory IFOLP

18:00:11 FOLP: theory FOLP

18:00:11 HOL-Proofs: theory Fields

18:00:11 HOL-Proofs: theory Meson

18:00:12 HOL-Proofs: theory ATP

18:00:12 HOL: theory BNF_Composition

18:00:12 HOL: theory Basic_BNFs

18:00:12 Timing FOLP (2 threads, 0.857s elapsed time, 0.868s cpu time, 0.000s GC time, factor 1.01)

18:00:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP

18:00:12 Finished FOLP (0:00:01 elapsed time)

18:00:12 Running ZF-UNITY ...

18:00:12 HOL: theory BNF_Fixpoint_Base

18:00:13 ZF-UNITY: theory Acc

18:00:13 ZF-UNITY: theory FoldSet

18:00:13 ZF-UNITY: theory GenPrefix

18:00:13 ZF-UNITY: theory Multiset

18:00:13 ZF-UNITY: theory State

18:00:13 ZF-UNITY: theory UNITY

18:00:14 ZF-UNITY: theory Constrains

18:00:14 ZF-UNITY: theory MultisetSum

18:00:14 ZF-UNITY: theory Monotonicity

18:00:14 ZF-UNITY: theory FP

18:00:14 HOL-Proofs: theory Metis

18:00:14 ZF-UNITY: theory WFair

18:00:14 ZF-UNITY: theory Increasing

18:00:14 ZF-UNITY: theory SubstAx

18:00:15 ZF-UNITY: theory Follows

18:00:15 ZF-UNITY: theory Mutex

18:00:15 ZF-UNITY: theory Union

18:00:15 HOL: theory BNF_Least_Fixpoint

18:00:15 ZF-UNITY: theory Comp

18:00:16 ZF-UNITY: theory Guar

18:00:16 ZF-UNITY: theory AllocBase

18:00:16 ZF-UNITY: theory ClientImpl

18:00:16 ZF-UNITY: theory Distributor

18:00:17 ZF-UNITY: theory Merge

18:00:17 ZF-UNITY: theory AllocImpl

18:00:17 HOL: theory Basic_BNF_LFPs

18:00:17 HOL: theory Transfer

18:00:18 HOL: theory Num

18:00:18 HOL-Proofs: theory Finite_Set

18:00:21 HOL: theory Power

18:00:24 HOL: theory Groups_Big

18:00:26 HOL: theory Equiv_Relations

18:00:26 HOL-Proofs: theory Relation

18:00:26 HOL: theory Lifting

18:00:27 HOL: theory Lifting_Set

18:00:27 HOL: theory Option

18:00:28 HOL: theory Quotient

18:00:28 HOL: theory Extraction

18:00:29 HOL-Proofs: theory Transitive_Closure

18:00:29 HOL: theory Lattices_Big

18:00:30 HOL: theory Partial_Function

18:00:31 HOL: theory Fun_Def

18:00:32 Timing ZF-UNITY (2 threads, 18.800s elapsed time, 33.856s cpu time, 1.204s GC time, factor 1.80)

18:00:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

18:00:32 Finished ZF-UNITY (0:00:19 elapsed time, 0:00:34 cpu time, factor 1.78)

18:00:32 Running ZF-Constructible ...

18:00:32 HOL: theory Int

18:00:32 ZF-Constructible: theory Formula

18:00:32 ZF-Constructible: theory MetaExists

18:00:32 ZF-Constructible: theory Normal

18:00:32 ZF-Constructible: theory Reflection

18:00:33 ZF-Constructible: theory Relative

18:00:33 HOL-Proofs: theory Wellfounded

18:00:34 HOL: theory Nat_Transfer

18:00:35 ZF-Constructible: theory L_axioms

18:00:35 ZF-Constructible: theory Wellorderings

18:00:35 HOL: theory Parity

18:00:35 ZF-Constructible: theory WFrec

18:00:35 HOL-Proofs: theory Fun_Def_Base

18:00:35 ZF-Constructible: theory WF_absolute

18:00:36 HOL-Proofs: theory Hilbert_Choice

18:00:36 ZF-Constructible: theory Datatype_absolute

18:00:36 ZF-Constructible: theory Rank

18:00:37 HOL: theory Divides

18:00:37 ZF-Constructible: theory Separation

18:00:37 HOL-Proofs: theory Wfrec

18:00:37 ZF-Constructible: theory Internalize

18:00:37 ZF-Constructible: theory AC_in_L

18:00:38 HOL-Proofs: theory Order_Relation

18:00:39 HOL-Proofs: theory BNF_Wellorder_Relation

18:00:39 HOL-Proofs: theory Zorn

18:00:39 ZF-Constructible: theory Rec_Separation

18:00:39 ZF-Constructible: theory Rank_Separation

18:00:39 ZF-Constructible: theory Satisfies_absolute

18:00:40 HOL-Proofs: theory BNF_Wellorder_Embedding

18:00:40 ZF-Constructible: theory DPow_absolute

18:00:42 HOL-Proofs: theory BNF_Wellorder_Constructions

18:00:43 HOL: theory Code_Numeral

18:00:43 HOL: theory Numeral_Simprocs

18:00:44 HOL: theory SMT

18:00:44 HOL: theory Semiring_Normalization

18:00:46 HOL: theory Set_Interval

18:00:46 HOL: theory Groebner_Basis

18:00:47 HOL-Proofs: theory BNF_Cardinal_Order_Relation

18:00:48 HOL: theory Conditionally_Complete_Lattices

18:00:48 HOL: theory Filter

18:00:49 HOL: theory Presburger

18:00:51 HOL-Proofs: theory BNF_Cardinal_Arithmetic

18:00:51 Timing ZF-Constructible (2 threads, 15.136s elapsed time, 28.700s cpu time, 5.368s GC time, factor 1.90)

18:00:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

18:00:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

18:00:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

18:00:51 Finished ZF-Constructible (0:00:19 elapsed time, 0:00:35 cpu time, factor 1.85)

18:00:52 Running ZF-ex ...

18:00:52 HOL: theory Sledgehammer

18:00:52 ZF-ex: theory BinEx

18:00:52 ZF-ex: theory CoUnit

18:00:52 ZF-ex: theory Commutation

18:00:52 ZF-ex: theory Group

18:00:52 ZF-ex: theory LList

18:00:52 ZF-ex: theory Limit

18:00:53 ZF-ex: theory Ring

18:00:53 HOL-Proofs: theory BNF_Def

18:00:53 ZF-ex: theory NatSum

18:00:53 ZF-ex: theory Primes

18:00:53 HOL: theory List

18:00:53 ZF-ex: theory Ramsey

18:00:53 ZF-ex: theory misc

18:00:59 HOL-Proofs: theory BNF_Composition

18:00:59 HOL-Proofs: theory Basic_BNFs

18:01:00 HOL-Proofs: theory BNF_Fixpoint_Base

18:01:01 HOL: theory Groups_List

18:01:01 HOL: theory Map

18:01:01 HOL: theory Random

18:01:01 HOL: theory Enum

18:01:03 HOL-Proofs: theory BNF_Least_Fixpoint

18:01:03 Timing ZF-ex (2 threads, 10.742s elapsed time, 15.204s cpu time, 0.696s GC time, factor 1.42)

18:01:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

18:01:03 Finished ZF-ex (0:00:11 elapsed time, 0:00:15 cpu time, factor 1.39)

18:01:03 Running ZF-Induct ...

18:01:03 ZF-Induct: theory Binary_Trees

18:01:03 ZF-Induct: theory Acc

18:01:03 ZF-Induct: theory Comb

18:01:03 ZF-Induct: theory Datatypes

18:01:04 ZF-Induct: theory FoldSet

18:01:04 HOL: theory String

18:01:04 ZF-Induct: theory ListN

18:01:04 ZF-Induct: theory Mutil

18:01:04 ZF-Induct: theory Multiset

18:01:04 ZF-Induct: theory Ntree

18:01:04 ZF-Induct: theory Primrec

18:01:04 ZF-Induct: theory PropLog

18:01:04 HOL: theory BNF_Greatest_Fixpoint

18:01:04 ZF-Induct: theory Rmap

18:01:04 HOL: theory Predicate

18:01:04 ZF-Induct: theory Term

18:01:05 ZF-Induct: theory Tree_Forest

18:01:05 ZF-Induct: theory Brouwer

18:01:06 HOL: theory Lazy_Sequence

18:01:06 HOL-Proofs: theory Basic_BNF_LFPs

18:01:06 HOL-Proofs: theory Transfer

18:01:06 HOL: theory Limited_Sequence

18:01:07 HOL: theory Typerep

18:01:08 HOL: theory Code_Evaluation

18:01:08 HOL-Proofs: theory Num

18:01:09 HOL: theory Quickcheck_Random

18:01:11 HOL: theory Quickcheck_Exhaustive

18:01:11 HOL: theory Quickcheck_Narrowing

18:01:12 HOL-Proofs: theory Power

18:01:13 Timing ZF-Induct (2 threads, 6.805s elapsed time, 11.048s cpu time, 0.416s GC time, factor 1.62)

18:01:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

18:01:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

18:01:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

18:01:13 Finished ZF-Induct (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.58)

18:01:13 Running ZF-AC ...

18:01:13 ZF-AC: theory AC_Equiv

18:01:14 ZF-AC: theory AC18_AC19

18:01:14 ZF-AC: theory AC7_AC9

18:01:14 ZF-AC: theory Cardinal_aux

18:01:14 ZF-AC: theory Hartog

18:01:14 ZF-AC: theory WO6_WO1

18:01:14 ZF-AC: theory AC16_lemmas

18:01:14 ZF-AC: theory AC16_WO4

18:01:14 ZF-AC: theory DC

18:01:14 ZF-AC: theory HH

18:01:14 ZF-AC: theory AC15_WO6

18:01:14 ZF-AC: theory AC17_AC1

18:01:14 ZF-AC: theory WO1_AC

18:01:14 ZF-AC: theory WO1_WO7

18:01:14 ZF-AC: theory WO2_AC16

18:01:15 HOL: theory Random_Pred

18:01:15 HOL: theory Record

18:01:15 HOL: theory Random_Sequence

18:01:15 HOL-Proofs: theory Groups_Big

18:01:16 HOL: theory Predicate_Compile

18:01:17 HOL: theory Nitpick

18:01:21 Timing ZF-AC (2 threads, 5.716s elapsed time, 9.664s cpu time, 0.488s GC time, factor 1.69)

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

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

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

18:01:21 Finished ZF-AC (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.61)

18:01:21 Running FOL-ex ...

18:01:21 HOL: theory Main

18:01:21 FOL-ex: theory If

18:01:21 FOL-ex: theory Classical

18:01:21 FOL-ex: theory Intro

18:01:21 FOL-ex: theory Miniscope

18:01:21 FOL-ex: theory Nat

18:01:21 FOL-ex: theory Nat_Class

18:01:22 FOL-ex: theory Natural_Numbers

18:01:22 FOL-ex: theory Prolog

18:01:22 FOL-ex: theory Propositional_Cla

18:01:22 FOL-ex: theory Quantifiers_Cla

18:01:22 HOL-Proofs: theory Equiv_Relations

18:01:22 FOL-ex: theory Foundation

18:01:22 FOL-ex: theory Intuitionistic

18:01:22 FOL-ex: theory Propositional_Int

18:01:22 FOL-ex: theory Quantifiers_Int

18:01:23 HOL: theory Archimedean_Field

18:01:23 HOL: theory Binomial

18:01:24 HOL: theory GCD

18:01:24 FOL-ex: theory Locale_Test1

18:01:24 HOL-Proofs: theory Lifting

18:01:27 FOL-ex: theory Locale_Test2

18:01:27 FOL-ex: theory Locale_Test3

18:01:27 FOL-ex: theory Locale_Test

18:01:27 HOL: theory Topological_Spaces

18:01:28 HOL-Proofs: theory Lifting_Set

18:01:29 HOL: theory Rat

18:01:29 HOL-Proofs: theory Option

18:01:29 Timing FOL-ex (2 threads, 5.435s elapsed time, 7.644s cpu time, 0.212s GC time, factor 1.41)

18:01:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

18:01:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

18:01:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

18:01:29 Finished FOL-ex (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.41)

18:01:29 Running CCL ...

18:01:29 CCL: theory IFOL

18:01:30 CCL: theory FOL

18:01:31 HOL: theory Real

18:01:32 CCL: theory Set

18:01:32 CCL: theory Lfp

18:01:32 CCL: theory Gfp

18:01:32 CCL: theory CCL

18:01:32 CCL: theory Term

18:01:32 CCL: theory Trancl

18:01:33 CCL: theory Type

18:01:33 CCL: theory Fix

18:01:33 CCL: theory Hered

18:01:33 HOL-Proofs: theory Quotient

18:01:33 CCL: theory Wfd

18:01:34 CCL: theory Nat

18:01:34 CCL: theory List

18:01:34 CCL: theory Flag

18:01:34 CCL: theory Stream

18:01:34 HOL-Proofs: theory Extraction

18:01:34 HOL: theory Real_Vector_Spaces

18:01:35 Timing CCL (2 threads, 4.787s elapsed time, 6.824s cpu time, 0.148s GC time, factor 1.43)

18:01:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL

18:01:35 Finished CCL (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.39)

18:01:35 Running Sequents ...

18:01:35 Sequents: theory Sequents

18:01:35 Sequents: theory ILL

18:01:35 Sequents: theory LK0

18:01:35 Sequents: theory ILL_predlog

18:01:35 Sequents: theory Washing

18:01:35 Sequents: theory LK

18:01:35 Sequents: theory Modal0

18:01:35 Sequents: theory S4

18:01:35 Sequents: theory S43

18:01:35 Sequents: theory Hard_Quantifiers

18:01:36 Sequents: theory Nat

18:01:36 Sequents: theory Propositional

18:01:36 Sequents: theory Quantifiers

18:01:36 Sequents: theory T

18:01:36 HOL-Proofs: theory Lattices_Big

18:01:37 HOL-Proofs: theory Partial_Function

18:01:39 Timing Sequents (2 threads, 3.530s elapsed time, 6.796s cpu time, 0.132s GC time, factor 1.93)

18:01:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

18:01:39 Finished Sequents (0:00:03 elapsed time, 0:00:07 cpu time, factor 1.82)

18:01:39 Running FOLP-ex ...

18:01:39 FOLP-ex: theory Classical

18:01:39 FOLP-ex: theory If

18:01:39 FOLP-ex: theory Intro

18:01:39 FOLP-ex: theory Nat

18:01:39 HOL-Proofs: theory Fun_Def

18:01:39 FOLP-ex: theory Propositional_Cla

18:01:40 FOLP-ex: theory Quantifiers_Cla

18:01:40 FOLP-ex: theory Foundation

18:01:40 FOLP-ex: theory Intuitionistic

18:01:41 HOL-Proofs: theory Int

18:01:41 FOLP-ex: theory Propositional_Int

18:01:41 FOLP-ex: theory Quantifiers_Int

18:01:43 Timing FOLP-ex (2 threads, 3.473s elapsed time, 5.964s cpu time, 0.096s GC time, factor 1.72)

18:01:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex

18:01:43 Finished FOLP-ex (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.62)

18:01:43 Running LCF ...

18:01:43 LCF: theory IFOL

18:01:44 LCF: theory FOL

18:01:45 LCF: theory LCF

18:01:46 HOL: theory Inequalities

18:01:46 HOL: theory Limits

18:01:46 LCF: theory Ex1

18:01:46 LCF: theory Ex2

18:01:46 LCF: theory Ex3

18:01:46 LCF: theory Ex4

18:01:46 HOL-Proofs: theory Nat_Transfer

18:01:46 Timing LCF (2 threads, 2.802s elapsed time, 3.236s cpu time, 0.152s GC time, factor 1.15)

18:01:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

18:01:46 Finished LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.12)

18:01:46 Running Spec_Check ...

18:01:46 Spec_Check: theory Spec_Check

18:01:47 Spec_Check: theory Examples

18:01:47 HOL-Proofs: theory Parity

18:01:49 HOL: theory Deriv

18:01:49 HOL: theory Series

18:01:49 Warning: missing document directory

18:01:49 Timing Spec_Check (2 threads, 1.812s elapsed time, 3.280s cpu time, 0.024s GC time, factor 1.81)

18:01:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

18:01:49 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

18:01:49 Running ZF-Resid ...

18:01:49 ZF-Resid: theory Redex

18:01:49 ZF-Resid: theory Substitution

18:01:49 ZF-Resid: theory Residuals

18:01:50 ZF-Resid: theory Reduction

18:01:50 HOL-Proofs: theory Divides

18:01:50 ZF-Resid: theory Confluence

18:01:50 HOL: theory NthRoot

18:01:51 Timing ZF-Resid (2 threads, 1.475s elapsed time, 2.460s cpu time, 0.000s GC time, factor 1.67)

18:01:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

18:01:51 Finished ZF-Resid (0:00:01 elapsed time)

18:01:51 Running ZF-IMP ...

18:01:51 HOL: theory Transcendental

18:01:51 ZF-IMP: theory Com

18:01:51 ZF-IMP: theory Denotation

18:01:51 ZF-IMP: theory Equiv

18:01:52 Timing ZF-IMP (2 threads, 0.991s elapsed time, 1.152s cpu time, 0.000s GC time, factor 1.16)

18:01:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

18:01:52 Finished ZF-IMP (0:00:01 elapsed time)

18:01:52 Running CTT ...

18:01:53 CTT: theory CTT

18:01:53 CTT: theory Bool

18:01:53 CTT: theory Elimination

18:01:53 CTT: theory Arith

18:01:53 CTT: theory Equality

18:01:53 CTT: theory Typechecking

18:01:53 CTT: theory Synthesis

18:01:53 CTT: theory Main

18:01:55 HOL: theory Complex

18:01:55 Timing CTT (2 threads, 0.689s elapsed time, 1.052s cpu time, 0.000s GC time, factor 1.53)

18:01:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

18:01:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

18:01:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

18:01:55 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)

18:01:55 Running Logics_ZF ...

18:01:55 Logics_ZF: theory FOL_examples

18:01:55 Logics_ZF: theory If

18:01:55 Logics_ZF: theory ZF_Isar

18:01:55 Logics_ZF: theory ZF_examples

18:01:55 Logics_ZF: theory IFOL_examples

18:01:56 HOL: theory MacLaurin

18:01:57 HOL: theory Complex_Main

18:01:58 Timing Logics_ZF (2 threads, 0.269s elapsed time, 0.536s cpu time, 0.000s GC time, factor 1.99)

18:01:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

18:01:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

18:01:58 Finished Logics_ZF (0:00:03 elapsed time)

18:01:58 Running Cube ...

18:01:59 Cube: theory Cube

18:01:59 Cube: theory Example

18:01:59 Timing Cube (2 threads, 0.294s elapsed time, 0.296s cpu time, 0.000s GC time, factor 1.01)

18:01:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

18:01:59 Finished Cube (0:00:00 elapsed time)

18:01:59 Running Intro ...

18:02:02 Timing Intro (2 threads, 0.001s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:02:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

18:02:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

18:02:02 Finished Intro (0:00:02 elapsed time)

18:02:02 Running SML ...

18:02:02 SML: theory Examples

18:02:02 Warning: missing document directory

18:02:02 Timing SML (2 threads, 0.015s elapsed time, 0.016s cpu time, 0.000s GC time, factor 1.05)

18:02:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

18:02:02 Finished SML (0:00:00 elapsed time)

18:02:02 Running Logics ...

18:02:05 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

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

18:02:05 Finished Logics (0:00:02 elapsed time)

18:02:05 Running Nitpick ...

18:02:08 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:02:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

18:02:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

18:02:08 Finished Nitpick (0:00:02 elapsed time)

18:02:08 Running Sledgehammer ...

18:02:09 HOL-Proofs: theory Code_Numeral

18:02:10 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:02:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

18:02:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

18:02:10 Finished Sledgehammer (0:00:02 elapsed time)

18:02:10 Running ZF-Coind ...

18:02:10 ZF-Coind: theory Language

18:02:10 ZF-Coind: theory Map

18:02:10 ZF-Coind: theory Types

18:02:10 ZF-Coind: theory Values

18:02:10 ZF-Coind: theory Dynamic

18:02:11 ZF-Coind: theory Static

18:02:11 ZF-Coind: theory ECR

18:02:11 Timing ZF-Coind (2 threads, 0.670s elapsed time, 1.248s cpu time, 0.000s GC time, factor 1.86)

18:02:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

18:02:11 Finished ZF-Coind (0:00:00 elapsed time)

18:02:11 Running System ...

18:02:11 System: theory Base

18:02:11 System: theory Environment

18:02:11 System: theory Misc

18:02:11 System: theory Presentation

18:02:11 System: theory Scala

18:02:11 System: theory Sessions

18:02:13 HOL-Proofs: theory Numeral_Simprocs

18:02:14 HOL-Proofs: theory SMT

18:02:14 Timing System (2 threads, 0.319s elapsed time, 0.420s cpu time, 0.000s GC time, factor 1.32)

18:02:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

18:02:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

18:02:14 Finished System (0:00:02 elapsed time)

18:02:15 HOL-Proofs: theory Semiring_Normalization

18:02:18 HOL-Proofs: theory Groebner_Basis

18:02:18 HOL-Proofs: theory Set_Interval

18:02:29 HOL-Proofs: theory Conditionally_Complete_Lattices

18:02:29 HOL-Proofs: theory Filter

18:02:33 HOL-Proofs: theory Presburger

18:02:45 HOL-Proofs: theory Sledgehammer

18:02:46 HOL-Proofs: theory List

18:03:22 HOL-Proofs: theory Groups_List

18:03:24 HOL-Proofs: theory Map

18:03:26 HOL-Proofs: theory Enum

18:03:40 HOL-Proofs: theory Random

18:04:35 HOL-Proofs: theory String

18:04:37 HOL-Proofs: theory BNF_Greatest_Fixpoint

18:04:42 HOL-Proofs: theory Predicate

18:04:44 HOL-Proofs: theory Lazy_Sequence

18:04:46 HOL-Proofs: theory Limited_Sequence

18:04:46 HOL-Proofs: theory Typerep

18:04:48 HOL-Proofs: theory Code_Evaluation

18:04:49 HOL-Proofs: theory Quickcheck_Random

18:04:52 HOL-Proofs: theory Quickcheck_Exhaustive

18:04:58 HOL-Proofs: theory Record

18:05:01 HOL-Proofs: theory Nitpick

18:05:08 HOL-Proofs: theory Quickcheck_Narrowing

18:05:14 HOL-Proofs: theory Random_Pred

18:05:15 HOL-Proofs: theory Random_Sequence

18:05:16 HOL-Proofs: theory Predicate_Compile

18:05:18 HOL-Proofs: theory Main

18:05:20 HOL-Proofs: theory Old_Datatype

18:05:27 Timing HOL (2 threads, 235.747s elapsed time, 440.328s cpu time, 29.440s GC time, factor 1.87)

18:05:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL

18:05:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf

18:05:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf

18:05:27 Finished HOL (0:05:55 elapsed time, 0:10:34 cpu time, factor 1.78)

18:05:29 Building HOLCF ...

18:05:30 Building HOL-Word ...

18:05:32 HOLCF: theory Nat_Bijection

18:05:32 HOLCF: theory Old_Datatype

18:05:32 HOL-Word: theory Bit

18:05:32 HOL-Word: theory Bits

18:05:32 HOL-Word: theory Boolean_Algebra

18:05:33 HOL-Word: theory Bits_Bit

18:05:33 HOL-Word: theory Misc_Numeric

18:05:33 HOL-Word: theory Bit_Representation

18:05:33 HOL-Word: theory Misc_Typedef

18:05:33 HOL-Word: theory Phantom_Type

18:05:33 HOLCF: theory Countable

18:05:33 HOL-Word: theory Bits_Int

18:05:34 HOL-Word: theory Cardinality

18:05:35 HOLCF: theory Porder

18:05:35 HOL-Word: theory Bool_List_Representation

18:05:35 HOL-Word: theory Numeral_Type

18:05:36 HOLCF: theory Pcpo

18:05:37 HOL-Word: theory Type_Length

18:05:37 HOL-Word: theory Word_Miscellaneous

18:05:37 HOLCF: theory Cont

18:05:37 HOL-Word: theory Word

18:05:37 HOLCF: theory Adm

18:05:37 HOLCF: theory Discrete

18:05:38 HOLCF: theory Cpodef

18:05:38 HOLCF: theory Fun_Cpo

18:05:38 HOLCF: theory Product_Cpo

18:05:39 HOLCF: theory Cfun

18:05:39 HOLCF: theory Cprod

18:05:39 HOLCF: theory Fix

18:05:40 HOLCF: theory Sfun

18:05:40 HOLCF: theory Sprod

18:05:40 HOLCF: theory Up

18:05:41 HOLCF: theory Lift

18:05:41 HOLCF: theory One

18:05:41 HOLCF: theory Tr

18:05:41 HOLCF: theory Ssum

18:05:42 HOLCF: theory Plain_HOLCF

18:05:42 HOLCF: theory Completion

18:05:42 HOLCF: theory Deflation

18:05:43 HOLCF: theory Map_Functions

18:05:43 HOLCF: theory Fixrec

18:05:43 HOLCF: theory Bifinite

18:05:43 HOLCF: theory Domain_Aux

18:05:45 HOLCF: theory Universal

18:05:46 HOLCF: theory Algebraic

18:05:46 HOLCF: theory Compact_Basis

18:05:46 HOLCF: theory LowerPD

18:05:46 HOLCF: theory UpperPD

18:05:47 HOLCF: theory Representable

18:05:47 HOLCF: theory ConvexPD

18:05:50 HOLCF: theory Domain

18:05:51 HOLCF: theory Powerdomains

18:05:52 HOLCF: theory HOLCF

18:06:18 Timing HOL-Word (2 threads, 22.539s elapsed time, 43.580s cpu time, 1.804s GC time, factor 1.93)

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

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

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

18:06:18 Finished HOL-Word (0:00:48 elapsed time, 0:01:22 cpu time, factor 1.71)

18:06:18 Building HOL-TLA ...

18:06:20 Timing HOLCF (2 threads, 20.977s elapsed time, 37.900s cpu time, 2.192s GC time, factor 1.81)

18:06:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF

18:06:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

18:06:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

18:06:20 Finished HOLCF (0:00:49 elapsed time, 0:01:21 cpu time, factor 1.63)

18:06:20 Building IOA ...

18:06:21 HOL-TLA: theory Intensional

18:06:21 HOL-TLA: theory Stfun

18:06:21 HOL-TLA: theory Action

18:06:22 HOL-TLA: theory Init

18:06:22 HOL-TLA: theory TLA

18:06:23 IOA: theory Asig

18:06:23 IOA: theory Seq

18:06:24 IOA: theory Automata

18:06:25 IOA: theory Sequence

18:06:25 IOA: theory Pred

18:06:26 IOA: theory Traces

18:06:26 IOA: theory TL

18:06:27 IOA: theory CompoExecs

18:06:27 IOA: theory RefMappings

18:06:27 IOA: theory RefCorrectness

18:06:27 IOA: theory CompoScheds

18:06:28 IOA: theory Simulations

18:06:28 IOA: theory SimCorrectness

18:06:28 IOA: theory Deadlock

18:06:28 IOA: theory ShortExecutions

18:06:29 IOA: theory CompoTraces

18:06:30 IOA: theory Compositionality

18:06:30 IOA: theory IOA

18:06:31 IOA: theory TLS

18:06:31 IOA: theory LiveIOA

18:06:32 IOA: theory Abstraction

18:06:38 Timing HOL-TLA (2 threads, 1.918s elapsed time, 3.004s cpu time, 0.000s GC time, factor 1.57)

18:06:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA

18:06:38 Finished HOL-TLA (0:00:19 elapsed time, 0:00:27 cpu time, factor 1.42)

18:06:38 Building HOL-Analysis ...

18:06:42 HOL-Analysis: theory Disjoint_Sets

18:06:42 HOL-Analysis: theory FuncSet

18:06:42 HOL-Analysis: theory Infinite_Set

18:06:43 HOL-Analysis: theory Multiset

18:06:43 HOL-Analysis: theory Nat_Bijection

18:06:43 HOL-Analysis: theory Old_Datatype

18:06:45 HOL-Analysis: theory Countable

18:06:47 HOL-Analysis: theory Countable_Set

18:06:47 HOL-Analysis: theory Countable_Complete_Lattices

18:06:48 HOL-Analysis: theory Permutations

18:06:50 HOL-Analysis: theory Phantom_Type

18:06:51 HOL-Analysis: theory Cardinality

18:06:51 HOL-Analysis: theory Product_Plus

18:06:51 HOL-Analysis: theory Product_Order

18:06:51 HOL-Analysis: theory Set_Algebras

18:06:52 HOL-Analysis: theory Numeral_Type

18:06:52 HOL-Analysis: theory L2_Norm

18:06:52 HOL-Analysis: theory Continuum_Not_Denumerable

18:06:52 HOL-Analysis: theory Discrete

18:06:53 HOL-Analysis: theory Indicator_Function

18:06:53 HOL-Analysis: theory Inner_Product

18:06:53 HOL-Analysis: theory Liminf_Limsup

18:06:54 HOL-Analysis: theory Nonpos_Ints

18:06:54 HOL-Analysis: theory Product_Vector

18:06:54 HOL-Analysis: theory Operator_Norm

18:06:55 HOL-Analysis: theory Euclidean_Space

18:06:55 HOL-Analysis: theory Order_Continuity

18:06:56 HOL-Analysis: theory Extended_Nat

18:06:57 HOL-Analysis: theory Finite_Cartesian_Product

18:06:57 HOL-Analysis: theory Linear_Algebra

18:06:58 HOL-Analysis: theory Extended_Real

18:07:00 HOL-Analysis: theory Periodic_Fun

18:07:01 HOL-Analysis: theory Poly_Roots

18:07:01 HOL-Analysis: theory Sum_of_Squares

18:07:03 HOL-Analysis: theory Extended_Nonnegative_Real

18:07:03 Timing IOA (2 threads, 18.233s elapsed time, 34.348s cpu time, 1.272s GC time, factor 1.88)

18:07:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA

18:07:03 Finished IOA (0:00:41 elapsed time, 0:01:09 cpu time, factor 1.66)

18:07:03 Building HOL-SPARK ...

18:07:04 HOL-Analysis: theory Norm_Arith

18:07:05 HOL-Analysis: theory Topology_Euclidean_Space

18:07:05 HOL-Analysis: theory Sigma_Algebra

18:07:06 HOL-SPARK: theory Bit_Comparison

18:07:06 HOL-SPARK: theory SPARK_Setup

18:07:08 HOL-SPARK: theory SPARK

18:07:09 HOL-Analysis: theory Measurable

18:07:10 HOL-Analysis: theory Measure_Space

18:07:16 HOL-Analysis: theory Caratheodory

18:07:17 HOL-Analysis: theory Summation_Tests

18:07:19 HOL-Analysis: theory Bounded_Linear_Function

18:07:19 HOL-Analysis: theory Convex_Euclidean_Space

18:07:20 HOL-Analysis: theory Extended_Real_Limits

18:07:22 HOL-Analysis: theory Tagged_Division

18:07:23 HOL-Analysis: theory Uniform_Limit

18:07:26 HOL-Analysis: theory Continuous_Extension

18:07:26 HOL-Analysis: theory Path_Connected

18:07:26 Timing HOL-SPARK (2 threads, 2.662s elapsed time, 4.432s cpu time, 0.208s GC time, factor 1.66)

18:07:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK

18:07:26 Finished HOL-SPARK (0:00:23 elapsed time, 0:00:33 cpu time, factor 1.45)

18:07:26 Building HOL-Library ...

18:07:30 HOL-Library: theory Adhoc_Overloading

18:07:30 HOL-Library: theory Lattice_Syntax

18:07:30 HOL-Library: theory AList

18:07:30 HOL-Library: theory BNF_Axiomatization

18:07:30 HOL-Library: theory BNF_Corec

18:07:31 HOL-Analysis: theory Homeomorphism

18:07:32 HOL-Library: theory DAList

18:07:32 HOL-Analysis: theory Brouwer_Fixpoint

18:07:33 HOL-Library: theory Stirling

18:07:33 HOL-Library: theory Bit

18:07:34 HOL-Analysis: theory Derivative

18:07:34 HOL-Library: theory Bits

18:07:34 HOL-Library: theory Bits_Bit

18:07:35 HOL-Library: theory Boolean_Algebra

18:07:35 HOL-Library: theory Cardinal_Notations

18:07:36 HOL-Library: theory Char_ord

18:07:36 HOL-Library: theory Code_Abstract_Nat

18:07:36 HOL-Library: theory Code_Binary_Nat

18:07:36 HOL-Library: theory Code_Target_Nat

18:07:36 HOL-Library: theory Code_Char

18:07:36 HOL-Library: theory Code_Prolog

18:07:37 HOL-Analysis: theory Cartesian_Euclidean_Space

18:07:37 HOL-Library: theory Code_Test

18:07:37 HOL-Analysis: theory Weierstrass_Theorems

18:07:37 HOL-Library: theory Combine_PER

18:07:37 HOL-Library: theory Complete_Partial_Order2

18:07:38 HOL-Library: theory Debug

18:07:38 HOL-Library: theory Disjoint_Sets

18:07:38 HOL-Library: theory Dlist

18:07:39 HOL-Library: theory FSet

18:07:40 HOL-Analysis: theory Determinants

18:07:40 HOL-Analysis: theory Fashoda_Theorem

18:07:41 HOL-Analysis: theory Ordered_Euclidean_Space

18:07:41 HOL-Analysis: theory Polytope

18:07:41 HOL-Library: theory Fraction_Field

18:07:43 HOL-Library: theory Fun_Lexorder

18:07:43 HOL-Library: theory FuncSet

18:07:43 HOL-Library: theory Finite_Map

18:07:43 HOL-Library: theory Function_Algebras

18:07:44 HOL-Library: theory Function_Division

18:07:44 HOL-Library: theory Code_Target_Int

18:07:44 HOL-Library: theory Code_Target_Numeral

18:07:45 HOL-Library: theory Groups_Big_Fun

18:07:45 HOL-Library: theory IArray

18:07:45 HOL-Library: theory Infinite_Set

18:07:46 HOL-Library: theory Omega_Words_Fun

18:07:46 HOL-Library: theory LaTeXsugar

18:07:46 HOL-Library: theory Lattice_Constructions

18:07:46 HOL-Library: theory ListVector

18:07:47 HOL-Analysis: theory Borel_Space

18:07:47 HOL-Library: theory List_lexord

18:07:47 HOL-Library: theory Mapping

18:07:49 HOL-Library: theory AList_Mapping

18:07:49 HOL-Library: theory Misc_Numeric

18:07:49 HOL-Library: theory Bit_Representation

18:07:50 HOL-Library: theory Misc_Typedef

18:07:50 HOL-Library: theory Bits_Int

18:07:50 HOL-Library: theory Monad_Syntax

18:07:50 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

18:07:50 HOL-Library: theory More_List

18:07:51 HOL-Library: theory Multiset

18:07:52 HOL-Library: theory Bool_List_Representation

18:07:53 HOL-Analysis: theory Regularity

18:07:53 HOL-Library: theory Nat_Bijection

18:07:53 HOL-Analysis: theory Binary_Product_Measure

18:07:54 HOL-Library: theory Stream

18:07:54 HOL-Analysis: theory Embed_Measure

18:07:54 HOL-Analysis: theory Finite_Product_Measure

18:07:56 HOL-Analysis: theory Bochner_Integration

18:07:57 HOL-Analysis: theory Function_Topology

18:07:58 HOL-Library: theory Old_Datatype

18:07:59 HOL-Library: theory Countable

18:07:59 HOL-Analysis: theory Complete_Measure

18:08:00 HOL-Library: theory DAList_Multiset

18:08:00 HOL-Analysis: theory Radon_Nikodym

18:08:00 HOL-Analysis: theory Lebesgue_Measure

18:08:00 HOL-Analysis: theory Set_Integral

18:08:01 HOL-Library: theory Factorial_Ring

18:08:02 HOL-Library: theory Multiset_Order

18:08:02 HOL-Library: theory Permutation

18:08:02 HOL-Library: theory Permutations

18:08:03 HOL-Analysis: theory Henstock_Kurzweil_Integration

18:08:03 HOL-Library: theory Countable_Set

18:08:04 HOL-Library: theory Countable_Complete_Lattices

18:08:07 HOL-Analysis: theory Bounded_Continuous_Function

18:08:07 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

18:08:07 HOL-Library: theory Countable_Set_Type

18:08:08 HOL-Analysis: theory Integral_Test

18:08:08 HOL-Analysis: theory Complex_Analysis_Basics

18:08:09 HOL-Analysis: theory Interval_Integral

18:08:10 HOL-Analysis: theory Lebesgue_Integral_Substitution

18:08:10 HOL-Library: theory Old_Recdef

18:08:10 HOL-Library: theory Euclidean_Algorithm

18:08:10 HOL-Analysis: theory Complex_Transcendental

18:08:11 HOL-Library: theory Option_ord

18:08:11 HOL-Library: theory Parallel

18:08:12 HOL-Library: theory Perm

18:08:13 HOL-Analysis: theory Generalised_Binomial_Theorem

18:08:13 HOL-Analysis: theory Harmonic_Numbers

18:08:13 HOL-Analysis: theory Cauchy_Integral_Theorem

18:08:14 HOL-Library: theory Phantom_Type

18:08:14 HOL-Analysis: theory Gamma_Function

18:08:14 HOL-Library: theory Cardinality

18:08:16 HOL-Library: theory FinFun

18:08:18 HOL-Analysis: theory Further_Topology

18:08:19 HOL-Analysis: theory Conformal_Mappings

18:08:19 HOL-Library: theory Numeral_Type

18:08:20 HOL-Library: theory Type_Length

18:08:20 HOL-Library: theory Saturated

18:08:20 HOL-Library: theory Predicate_Compile_Alternative_Defs

18:08:21 HOL-Library: theory Predicate_Compile_Quickcheck

18:08:21 HOL-Library: theory Normalized_Fraction

18:08:21 HOL-Library: theory Product_Lexorder

18:08:21 HOL-Library: theory Product_Plus

18:08:21 HOL-Analysis: theory Analysis

18:08:21 HOL-Library: theory Product_Order

18:08:22 HOL-Library: theory Quotient_Syntax

18:08:22 HOL-Library: theory Quotient_Option

18:08:22 HOL-Library: theory Finite_Lattice

18:08:22 HOL-Library: theory Quotient_Product

18:08:22 HOL-Library: theory Quotient_Set

18:08:22 HOL-Library: theory Quotient_List

18:08:23 HOL-Library: theory Quotient_Sum

18:08:23 HOL-Library: theory Quotient_Type

18:08:23 HOL-Library: theory RBT_Impl

18:08:25 HOL-Library: theory Ramsey

18:08:26 HOL-Library: theory Reflection

18:08:26 HOL-Library: theory Refute

18:08:27 HOL-Library: theory Rewrite

18:08:27 HOL-Library: theory Set_Algebras

18:08:28 HOL-Library: theory Simps_Case_Conv

18:08:28 HOL-Library: theory Extended

18:08:31 HOL-Library: theory State_Monad

18:08:31 HOL-Library: theory Sublist

18:08:32 HOL-Library: theory Prefix_Order

18:08:32 HOL-Library: theory Sublist_Order

18:08:32 HOL-Library: theory Polynomial

18:08:39 HOL-Library: theory BigO

18:08:41 HOL-Library: theory Code_Real_Approx_By_Float

18:08:42 HOL-Library: theory Diagonal_Subsequence

18:08:42 HOL-Library: theory Discrete

18:08:43 HOL-Library: theory Field_as_Ring

18:08:45 HOL-Library: theory Formal_Power_Series

18:08:50 HOL-Library: theory Polynomial_FPS

18:08:51 HOL-Library: theory Fundamental_Theorem_Algebra

18:08:52 HOL-Library: theory Indicator_Function

18:08:53 HOL-Library: theory Lattice_Algebras

18:08:59 HOL-Library: theory Liminf_Limsup

18:09:00 HOL-Library: theory Log_Nat

18:09:00 HOL-Library: theory Float

18:09:03 HOL-Library: theory Lub_Glb

18:09:04 HOL-Library: theory Multiset_Permutations

18:09:04 HOL-Library: theory RBT

18:09:04 HOL-Library: theory RBT_Mapping

18:09:05 HOL-Library: theory RBT_Set

18:09:05 HOL-Library: theory Nonpos_Ints

18:09:05 HOL-Library: theory OptionalSugar

18:09:05 HOL-Library: theory Order_Continuity

18:09:06 HOL-Library: theory Periodic_Fun

18:09:06 HOL-Library: theory Polynomial_Factorial

18:09:07 HOL-Library: theory Extended_Nat

18:09:08 HOL-Library: theory Extended_Real

18:09:12 HOL-Library: theory Extended_Nonnegative_Real

18:09:15 HOL-Library: theory Linear_Temporal_Logic_on_Streams

18:09:17 HOL-Library: theory Quadratic_Discriminant

18:09:17 HOL-Library: theory Sum_of_Squares

18:09:19 HOL-Library: theory Transitive_Closure_Table

18:09:19 HOL-Library: theory Tree

18:09:20 HOL-Library: theory While_Combinator

18:09:21 HOL-Library: theory Bourbaki_Witt_Fixpoint

18:09:21 HOL-Library: theory Word_Miscellaneous

18:09:22 HOL-Library: theory Word

18:09:23 HOL-Library: theory Tree_Multiset

18:09:24 HOL-Library: theory Preorder

18:09:24 HOL-Library: theory Function_Growth

18:09:26 HOL-Library: theory Library

18:09:28 HOL-Library: theory Old_SMT

18:11:09 Timing HOL-Proofs (2 threads, 540.826s elapsed time, 970.696s cpu time, 100.904s GC time, factor 1.79)

18:11:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

18:11:09 Finished HOL-Proofs (0:11:36 elapsed time, 0:20:24 cpu time, factor 1.76)

18:11:11 Building HOL-Auth ...

18:11:13 HOL-Auth: theory Message

18:11:13 HOL-Auth: theory Nat_Bijection

18:11:14 HOL-Auth: theory Simps_Case_Conv

18:11:17 HOL-Auth: theory All_Symmetric

18:11:17 HOL-Auth: theory Event

18:11:17 HOL-Auth: theory EventSC

18:11:18 HOL-Auth: theory Extensions

18:11:19 HOL-Auth: theory Analz

18:11:19 HOL-Auth: theory List_Msg

18:11:19 HOL-Auth: theory Guard

18:11:20 HOL-Auth: theory GuardK

18:11:21 HOL-Auth: theory Public

18:11:22 HOL-Auth: theory Shared

18:11:22 HOL-Auth: theory CertifiedEmail

18:11:22 HOL-Auth: theory Guard_Public

18:11:23 HOL-Auth: theory Guard_NS_Public

18:11:23 HOL-Auth: theory P2

18:11:23 HOL-Auth: theory Proto

18:11:25 HOL-Auth: theory KerberosIV

18:11:27 HOL-Auth: theory KerberosIV_Gets

18:11:27 HOL-Auth: theory KerberosV

18:11:29 HOL-Auth: theory Kerberos_BAN

18:11:29 HOL-Auth: theory Kerberos_BAN_Gets

18:11:30 HOL-Auth: theory NS_Public

18:11:31 HOL-Auth: theory NS_Public_Bad

18:11:31 HOL-Auth: theory NS_Shared

18:11:31 HOL-Auth: theory OtwayRees

18:11:31 HOL-Auth: theory OtwayReesBella

18:11:32 HOL-Auth: theory OtwayRees_AN

18:11:32 HOL-Auth: theory OtwayRees_Bad

18:11:33 HOL-Auth: theory P1

18:11:33 HOL-Auth: theory Recur

18:11:34 HOL-Auth: theory WooLam

18:11:34 HOL-Auth: theory Yahalom

18:11:35 HOL-Auth: theory Yahalom2

18:11:36 HOL-Auth: theory Yahalom_Bad

18:11:37 HOL-Auth: theory ZhouGollmann

18:11:38 HOL-Auth: theory Auth_Shared

18:11:39 HOL-Auth: theory Auth_Guard_Public

18:11:39 HOL-Auth: theory Guard_Shared

18:11:39 HOL-Auth: theory Guard_OtwayRees

18:11:39 HOL-Auth: theory Guard_Yahalom

18:11:40 HOL-Auth: theory TLS

18:11:40 HOL-Auth: theory Auth_Guard_Shared

18:11:40 HOL-Auth: theory Smartcard

18:11:41 HOL-Auth: theory ShoupRubin

18:11:42 HOL-Auth: theory Auth_Public

18:11:43 HOL-Auth: theory ShoupRubinBella

18:11:45 HOL-Auth: theory Auth_Smartcard

18:14:48 Timing HOL-Library (2 threads, 303.872s elapsed time, 564.336s cpu time, 31.824s GC time, factor 1.86)

18:14:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library

18:14:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf

18:14:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf

18:14:48 Finished HOL-Library (0:07:20 elapsed time, 0:13:05 cpu time, factor 1.78)

18:14:49 Building Codegen_Basics ...

18:14:52 Codegen_Basics: theory Dlist

18:14:52 Codegen_Basics: theory IArray

18:14:53 Codegen_Basics: theory Mapping

18:14:53 Codegen_Basics: theory RBT_Impl

18:15:24 Timing HOL-Auth (2 threads, 205.853s elapsed time, 324.192s cpu time, 11.144s GC time, factor 1.57)

18:15:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

18:15:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

18:15:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

18:15:24 Finished HOL-Auth (0:04:13 elapsed time, 0:06:38 cpu time, factor 1.57)

18:15:25 Building HOL-Nonstandard_Analysis ...

18:15:27 HOL-Nonstandard_Analysis: theory Lub_Glb

18:15:27 HOL-Nonstandard_Analysis: theory Infinite_Set

18:15:28 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

18:15:28 HOL-Nonstandard_Analysis: theory StarDef

18:15:29 HOL-Nonstandard_Analysis: theory HyperNat

18:15:30 HOL-Nonstandard_Analysis: theory HyperDef

18:15:31 HOL-Nonstandard_Analysis: theory NSA

18:15:32 Codegen_Basics: theory RBT

18:15:33 Codegen_Basics: theory Setup

18:15:34 HOL-Nonstandard_Analysis: theory NSComplex

18:15:34 HOL-Nonstandard_Analysis: theory Star

18:15:34 HOL-Nonstandard_Analysis: theory HLim

18:15:35 HOL-Nonstandard_Analysis: theory NatStar

18:15:35 HOL-Nonstandard_Analysis: theory HDeriv

18:15:35 HOL-Nonstandard_Analysis: theory HSEQ

18:15:36 HOL-Nonstandard_Analysis: theory HSeries

18:15:37 HOL-Nonstandard_Analysis: theory HTranscendental

18:15:38 HOL-Nonstandard_Analysis: theory HLog

18:15:38 HOL-Nonstandard_Analysis: theory NSCA

18:15:39 HOL-Nonstandard_Analysis: theory Hyperreal

18:15:39 HOL-Nonstandard_Analysis: theory CStar

18:15:39 HOL-Nonstandard_Analysis: theory CLim

18:15:40 HOL-Nonstandard_Analysis: theory Hypercomplex

18:15:40 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

18:16:07 Timing HOL-Nonstandard_Analysis (2 threads, 17.351s elapsed time, 34.060s cpu time, 1.448s GC time, factor 1.96)

18:16:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

18:16:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

18:16:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

18:16:07 Finished HOL-Nonstandard_Analysis (0:00:42 elapsed time, 0:01:11 cpu time, factor 1.70)

18:16:08 Building Typeclass_Hierarchy_Basics ...

18:16:10 Typeclass_Hierarchy_Basics: theory Lattice_Syntax

18:16:10 Typeclass_Hierarchy_Basics: theory Multiset

18:16:15 Typeclass_Hierarchy_Basics: theory Setup

18:16:33 Timing Codegen_Basics (2 threads, 65.352s elapsed time, 116.692s cpu time, 4.780s GC time, factor 1.79)

18:16:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

18:16:33 Finished Codegen_Basics (0:01:42 elapsed time, 0:02:55 cpu time, factor 1.70)

18:16:33 Building HOL-Nominal ...

18:16:35 HOL-Nominal: theory Infinite_Set

18:16:35 HOL-Nominal: theory Old_Datatype

18:16:36 Timing Typeclass_Hierarchy_Basics (2 threads, 9.024s elapsed time, 17.184s cpu time, 0.788s GC time, factor 1.90)

18:16:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

18:16:36 Finished Typeclass_Hierarchy_Basics (0:00:28 elapsed time, 0:00:45 cpu time, factor 1.62)

18:16:36 Building HOL-Eisbach ...

18:16:37 HOL-Nominal: theory Nominal

18:16:38 HOL-Eisbach: theory Eisbach

18:16:38 HOL-Eisbach: theory IFOL

18:16:39 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax

18:16:39 HOL-Eisbach: theory Eisbach_Tools

18:16:39 HOL-Eisbach: theory Examples

18:16:39 HOL-Eisbach: theory Tests

18:16:39 HOL-Eisbach: theory FOL

18:16:41 HOL-Eisbach: theory Examples_FOL

18:16:57 Warning: missing document directory

18:16:57 Timing HOL-Eisbach (2 threads, 3.460s elapsed time, 6.528s cpu time, 0.228s GC time, factor 1.89)

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

18:16:57 Finished HOL-Eisbach (0:00:20 elapsed time, 0:00:30 cpu time, factor 1.53)

18:16:57 Building HOL-Mirabelle ...

18:16:59 HOL-Mirabelle: theory Mirabelle

18:16:59 HOL-Mirabelle: theory Mirabelle_Test

18:17:01 Timing HOL-Nominal (2 threads, 8.929s elapsed time, 17.424s cpu time, 0.984s GC time, factor 1.95)

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

18:17:01 Finished HOL-Nominal (0:00:27 elapsed time, 0:00:45 cpu time, factor 1.64)

18:17:01 Running HOL-Nominal-Examples ...

18:17:04 HOL-Nominal-Examples: theory CK_Machine

18:17:04 HOL-Nominal-Examples: theory CR_Takahashi

18:17:07 HOL-Nominal-Examples: theory Class1

18:17:14 Timing HOL-Mirabelle (2 threads, 0.562s elapsed time, 0.640s cpu time, 0.000s GC time, factor 1.14)

18:17:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

18:17:14 Finished HOL-Mirabelle (0:00:16 elapsed time, 0:00:23 cpu time, factor 1.42)

18:17:14 Running HOL-Data_Structures ...

18:17:16 HOL-Data_Structures: theory Multiset

18:17:16 HOL-Data_Structures: theory Less_False

18:17:16 HOL-Data_Structures: theory Fib

18:17:17 HOL-Nominal-Examples: theory Compile

18:17:26 HOL-Data_Structures: theory Cmp

18:17:26 HOL-Data_Structures: theory Sorted_Less

18:17:27 HOL-Data_Structures: theory AList_Upd_Del

18:17:27 HOL-Data_Structures: theory List_Ins_Del

18:17:27 HOL-Data_Structures: theory Map_by_Ordered

18:17:27 HOL-Data_Structures: theory Tree

18:17:27 HOL-Data_Structures: theory Set_by_Ordered

18:17:28 HOL-Data_Structures: theory Brother12_Set

18:17:32 HOL-Data_Structures: theory Balance

18:17:33 HOL-Data_Structures: theory Splay_Set

18:17:35 HOL-Data_Structures: theory Splay_Map

18:17:37 HOL-Data_Structures: theory Tree_Set

18:17:37 HOL-Nominal-Examples: theory Contexts

18:17:38 HOL-Data_Structures: theory Tree_Map

18:17:39 HOL-Data_Structures: theory Tree2

18:17:40 HOL-Data_Structures: theory Isin2

18:17:41 HOL-Data_Structures: theory AA_Set

18:17:43 HOL-Data_Structures: theory AVL_Set

18:17:44 HOL-Data_Structures: theory Leftist_Heap

18:17:45 HOL-Nominal-Examples: theory Crary

18:17:46 HOL-Data_Structures: theory Lookup2

18:17:47 HOL-Data_Structures: theory AA_Map

18:17:48 HOL-Data_Structures: theory AVL_Map

18:17:48 HOL-Data_Structures: theory RBT

18:17:50 HOL-Nominal-Examples: theory Fsub

18:17:58 HOL-Nominal-Examples: theory Height

18:17:59 HOL-Data_Structures: theory RBT_Set

18:18:01 HOL-Nominal-Examples: theory Lam_Funs

18:18:03 HOL-Data_Structures: theory RBT_Map

18:18:05 HOL-Nominal-Examples: theory CR

18:18:05 HOL-Nominal-Examples: theory SN

18:18:07 HOL-Nominal-Examples: theory Lambda_mu

18:18:07 HOL-Data_Structures: theory Tree23

18:18:09 HOL-Data_Structures: theory Tree23_Set

18:18:12 HOL-Nominal-Examples: theory LocalWeakening

18:18:15 HOL-Nominal-Examples: theory Pattern

18:18:17 HOL-Data_Structures: theory Tree23_Map

18:18:22 HOL-Data_Structures: theory Tree234

18:18:24 HOL-Data_Structures: theory Tree234_Set

18:18:26 HOL-Nominal-Examples: theory SOS

18:18:29 HOL-Nominal-Examples: theory Standardization

18:18:33 HOL-Nominal-Examples: theory Support

18:18:34 HOL-Nominal-Examples: theory Type_Preservation

18:18:38 HOL-Nominal-Examples: theory W

18:18:45 HOL-Nominal-Examples: theory Weakening

18:18:57 HOL-Data_Structures: theory Tree234_Map

18:19:18 HOL-Data_Structures: theory Brother12_Map

18:20:09 HOL-Nominal-Examples: theory Class2

18:20:12 HOL-Nominal-Examples: theory Class3

18:20:49 Timing HOL-Analysis (2 threads, 706.068s elapsed time, 1238.704s cpu time, 43.760s GC time, factor 1.75)

18:20:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

18:20:49 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

18:20:49 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf

18:20:49 Finished HOL-Analysis (0:14:10 elapsed time, 0:24:23 cpu time, factor 1.72)

18:20:50 Building HOL-Probability ...

18:20:57 HOL-Probability: theory AList

18:20:57 HOL-Probability: theory FSet

18:20:59 HOL-Probability: theory Permutation

18:20:59 HOL-Probability: theory Diagonal_Subsequence

18:21:01 HOL-Probability: theory Finite_Map

18:21:11 HOL-Probability: theory Lattice_Syntax

18:21:11 HOL-Probability: theory Adhoc_Overloading

18:21:11 HOL-Probability: theory Complete_Partial_Order2

18:21:11 HOL-Probability: theory Mapping

18:21:12 HOL-Probability: theory AList_Mapping

18:21:13 HOL-Probability: theory Monad_Syntax

18:21:13 HOL-Probability: theory Stream

18:21:14 HOL-Probability: theory Rewrite

18:21:14 HOL-Probability: theory Sublist

18:21:15 HOL-Probability: theory Multiset_Permutations

18:21:16 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

18:21:16 HOL-Probability: theory Fin_Map

18:21:18 HOL-Probability: theory Discrete_Topology

18:21:18 HOL-Probability: theory Essential_Supremum

18:21:18 HOL-Probability: theory Probability_Measure

18:21:19 HOL-Probability: theory Stopping_Time

18:21:21 HOL-Probability: theory Conditional_Expectation

18:21:21 HOL-Probability: theory Distribution_Functions

18:21:21 HOL-Probability: theory Weak_Convergence

18:21:22 HOL-Probability: theory Giry_Monad

18:21:22 HOL-Probability: theory Helly_Selection

18:21:24 HOL-Probability: theory Probability_Mass_Function

18:21:24 HOL-Probability: theory Projective_Family

18:21:25 HOL-Probability: theory Infinite_Product_Measure

18:21:27 HOL-Probability: theory PMF_Impl

18:21:27 HOL-Probability: theory Random_Permutations

18:21:28 HOL-Probability: theory SPMF

18:21:29 HOL-Probability: theory Independent_Family

18:21:31 HOL-Probability: theory Convolution

18:21:31 HOL-Probability: theory Information

18:21:32 HOL-Probability: theory Projective_Limit

18:21:34 HOL-Probability: theory Stream_Space

18:21:34 HOL-Probability: theory Distributions

18:21:36 HOL-Probability: theory Characteristic_Functions

18:21:37 HOL-Probability: theory Sinc_Integral

18:21:37 HOL-Probability: theory Levy

18:21:39 HOL-Probability: theory Central_Limit_Theorem

18:21:39 HOL-Probability: theory Probability

18:24:57 Timing HOL-Probability (2 threads, 179.909s elapsed time, 326.348s cpu time, 13.600s GC time, factor 1.81)

18:24:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

18:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

18:24:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

18:24:57 Finished HOL-Probability (0:04:06 elapsed time, 0:07:06 cpu time, factor 1.73)

18:24:58 Running HOL-Codegenerator_Test ...

18:25:05 HOL-Codegenerator_Test: theory Cmp

18:25:05 HOL-Codegenerator_Test: theory Code_Test_PolyML

18:25:05 HOL-Codegenerator_Test: theory Code_Test_Scala

18:25:06 HOL-Codegenerator_Test: theory Less_False

18:25:06 HOL-Codegenerator_Test: theory Sorted_Less

18:25:06 HOL-Codegenerator_Test: theory Primes

18:25:06 HOL-Codegenerator_Test: theory AList_Upd_Del

18:25:07 HOL-Codegenerator_Test: theory List_Ins_Del

18:25:07 HOL-Codegenerator_Test: theory Map_by_Ordered

18:25:07 HOL-Codegenerator_Test: theory Eratosthenes

18:25:07 HOL-Codegenerator_Test: theory Set_by_Ordered

18:25:08 HOL-Codegenerator_Test: theory Records

18:25:08 HOL-Codegenerator_Test: theory Tree_Set

18:25:08 HOL-Codegenerator_Test: theory Tree_Map

18:25:12 HOL-Codegenerator_Test: theory Candidates

18:25:15 HOL-Codegenerator_Test: theory Generate

18:25:17 HOL-Codegenerator_Test: theory Generate_Binary_Nat

18:30:11 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures

18:30:12 HOL-Codegenerator_Test: theory Generate_Pretty_Char

18:31:14 Timing HOL-Data_Structures (2 threads, 834.503s elapsed time, 1142.076s cpu time, 62.940s GC time, factor 1.37)

18:31:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures

18:31:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf

18:31:14 Finished HOL-Data_Structures (0:13:59 elapsed time, 0:19:07 cpu time, factor 1.37)

18:31:14 Running HOL-ex ...

18:31:16 HOL-ex: theory Adhoc_Overloading

18:31:16 HOL-ex: theory Cartouche_Examples

18:31:17 HOL-ex: theory Chinese

18:31:17 HOL-ex: theory Code_Abstract_Nat

18:31:17 HOL-ex: theory Code_Binary_Nat

18:31:17 HOL-ex: theory FuncSet

18:31:18 HOL-ex: theory Hebrew

18:31:18 HOL-ex: theory Monad_Syntax

18:31:18 HOL-ex: theory Refute

18:31:19 HOL-ex: theory Serbian

18:31:20 HOL-ex: theory State_Monad

18:31:20 HOL-ex: theory Code_Binary_Nat_examples

18:31:21 HOL-ex: theory Eval_Examples

18:31:24 HOL-ex: theory Normalization_by_Evaluation

18:31:25 HOL-ex: theory Transitive_Closure_Table

18:31:48 HOL-ex: theory PresburgerEx

18:31:48 HOL-ex: theory Groebner_Examples

18:31:48 HOL-ex: theory AList

18:31:48 HOL-ex: theory Abstract_NAT

18:31:48 HOL-ex: theory Antiquote

18:31:49 HOL-ex: theory Arith_Examples

18:31:49 HOL-ex: theory CTL

18:31:49 HOL-ex: theory Classical

18:31:50 HOL-ex: theory Code_Target_Nat

18:31:50 HOL-ex: theory Coercion_Examples

18:31:50 HOL-ex: theory Coherent

18:31:51 HOL-ex: theory Commands

18:31:51 HOL-ex: theory Debug

18:31:51 HOL-ex: theory Dlist

18:31:52 HOL-ex: theory Erdoes_Szekeres

18:31:52 HOL-ex: theory Executable_Relation

18:31:52 HOL-ex: theory FSet

18:31:52 HOL-ex: theory Birthday_Paradox

18:31:53 HOL-ex: theory Code_Target_Int

18:31:53 HOL-ex: theory Code_Target_Numeral

18:31:53 HOL-ex: theory Transfer_Int_Nat

18:31:53 HOL-ex: theory Guess

18:31:53 HOL-ex: theory Hex_Bin_Examples

18:31:54 HOL-ex: theory IArray

18:31:55 HOL-ex: theory IArray_Examples

18:31:56 HOL-ex: theory Iff_Oracle

18:31:56 HOL-ex: theory Induction_Schema

18:31:56 HOL-ex: theory Infinite_Set

18:31:56 HOL-ex: theory Intuitionistic

18:31:56 HOL-ex: theory Adhoc_Overloading_Examples

18:31:56 HOL-ex: theory LaTeXsugar

18:31:57 HOL-ex: theory Lagrange

18:31:57 HOL-ex: theory List_to_Set_Comprehension_Examples

18:31:57 HOL-ex: theory LocaleTest2

18:31:57 HOL-ex: theory ML

18:31:58 HOL-ex: theory Mapping

18:31:59 HOL-ex: theory Functions

18:31:59 HOL-ex: theory AList_Mapping

18:31:59 HOL-ex: theory Execute_Choice

18:31:59 HOL-ex: theory MonoidGroup

18:32:00 HOL-ex: theory Multiquote

18:32:00 HOL-ex: theory Multiset

18:32:04 HOL-ex: theory NatSum

18:32:05 HOL-ex: theory PER

18:32:05 HOL-ex: theory Parallel

18:32:05 HOL-ex: theory Bubblesort

18:32:06 HOL-ex: theory Factorial_Ring

18:32:06 HOL-ex: theory MergeSort

18:32:08 HOL-ex: theory Quicksort

18:32:08 HOL-ex: theory Perm

18:32:09 HOL-ex: theory Perm_Fragments

18:32:10 HOL-ex: theory Phantom_Type

18:32:11 HOL-ex: theory Cardinality

18:32:12 HOL-ex: theory FinFun

18:32:14 HOL-ex: theory Euclidean_Algorithm

18:32:15 HOL-ex: theory FinFunPred

18:32:16 HOL-ex: theory Numeral_Type

18:32:17 HOL-ex: theory Type_Length

18:32:17 HOL-ex: theory Primrec

18:32:17 HOL-ex: theory Records

18:32:23 HOL-ex: theory Reflection

18:32:23 HOL-ex: theory Refute_Examples

18:32:24 HOL-ex: theory Primes

18:32:25 HOL-ex: theory Eratosthenes

18:32:26 HOL-ex: theory Code_Timing

18:32:27 HOL-ex: theory Rewrite

18:32:27 HOL-ex: theory Rewrite_Examples

18:32:27 HOL-ex: theory SAT_Examples

18:32:27 HOL-ex: theory Seq

18:32:28 HOL-ex: theory Set_Comprehension_Pointfree_Examples

18:32:28 HOL-ex: theory Set_Theory

18:32:29 HOL-Nominal-Examples: theory VC_Condition

18:32:29 HOL-ex: theory Simproc_Tests

18:32:29 HOL-ex: theory Simps_Case_Conv

18:32:29 HOL-ex: theory Simps_Case_Conv_Examples

18:32:30 HOL-ex: theory Sudoku

18:32:32 HOL-ex: theory Tarski

18:32:33 Timing HOL-Nominal-Examples (2 threads, 927.967s elapsed time, 1619.428s cpu time, 135.848s GC time, factor 1.75)

18:32:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples

18:32:33 Finished HOL-Nominal-Examples (0:15:31 elapsed time, 0:27:02 cpu time, factor 1.74)

18:32:33 Running HOL-Decision_Procs ...

18:32:34 HOL-ex: theory Termination

18:32:36 HOL-ex: theory ThreeDivides

18:32:36 HOL-Decision_Procs: theory Code_Abstract_Nat

18:32:36 HOL-Decision_Procs: theory Commutative_Ring

18:32:36 HOL-ex: theory Argo_Examples

18:32:36 HOL-Decision_Procs: theory Code_Target_Nat

18:32:37 HOL-Decision_Procs: theory DP_Library

18:32:37 HOL-Decision_Procs: theory Dense_Linear_Order

18:32:40 HOL-ex: theory Ballot

18:32:40 HOL-Decision_Procs: theory Dense_Linear_Order_Ex

18:32:41 HOL-ex: theory BinEx

18:32:41 HOL-Decision_Procs: theory Code_Target_Int

18:32:41 HOL-Decision_Procs: theory Code_Target_Numeral

18:32:42 HOL-Decision_Procs: theory Old_Recdef

18:32:42 HOL-ex: theory Cubic_Quartic

18:32:43 HOL-ex: theory Dedekind_Real

18:32:43 HOL-ex: theory Gauge_Integration

18:32:44 HOL-Decision_Procs: theory Cooper

18:32:44 HOL-ex: theory HarmonicSeries

18:32:44 HOL-ex: theory Parallel_Example

18:32:45 HOL-ex: theory Pythagoras

18:32:45 HOL-ex: theory Reflection_Examples

18:32:45 HOL-Decision_Procs: theory Commutative_Ring_Complete

18:32:46 HOL-ex: theory Sqrt

18:32:46 HOL-Decision_Procs: theory Commutative_Ring_Ex

18:32:46 HOL-Decision_Procs: theory Ferrack

18:32:47 HOL-ex: theory Sqrt_Script

18:32:48 HOL-ex: theory Sum_of_Powers

18:32:49 HOL-ex: theory Sum_of_Squares

18:32:52 HOL-ex: theory SOS

18:32:54 HOL-ex: theory SOS_Cert

18:32:55 HOL-ex: theory Transfer_Debug

18:32:55 HOL-ex: theory Transfer_Ex

18:32:55 HOL-ex: theory Transitive_Closure_Table_Ex

18:32:57 HOL-ex: theory Tree23

18:33:20 HOL-Decision_Procs: theory Lattice_Algebras

18:33:21 HOL-Codegenerator_Test: theory Generate_Target_Nat

18:33:26 HOL-Decision_Procs: theory Log_Nat

18:33:26 HOL-Decision_Procs: theory Float

18:33:27 HOL-Decision_Procs: theory MIR

18:33:28 HOL-ex: theory Unification

18:33:29 HOL-Decision_Procs: theory Approximation

18:33:29 HOL-ex: theory While_Combinator

18:33:30 HOL-ex: theory While_Combinator_Example

18:33:30 HOL-ex: theory Word_Type

18:34:18 HOL-Decision_Procs: theory Polynomial_List

18:34:33 HOL-Decision_Procs: theory Approximation_Ex

18:34:33 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex

18:34:34 HOL-Decision_Procs: theory Rat_Pair

18:34:39 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial

18:34:55 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff

18:35:38 HOL-Decision_Procs: theory Decision_Procs

18:38:29 HOL-Codegenerator_Test: theory Code_Test_GHC

18:38:31 HOL-Codegenerator_Test: theory Code_Test_MLton

18:38:35 HOL-Codegenerator_Test: theory Code_Test_OCaml

18:38:36 HOL-Codegenerator_Test: theory Code_Test_SMLNJ

18:38:38 Timing HOL-Codegenerator_Test (2 threads, 811.533s elapsed time, 697.428s cpu time, 18.212s GC time, factor 0.86)

18:38:38 Finished HOL-Codegenerator_Test (0:13:39 elapsed time, 0:37:34 cpu time, factor 2.75)

18:38:38 Running HOL-Nitpick_Examples ...

18:38:40 HOL-Nitpick_Examples: theory Core_Nits

18:38:40 HOL-Nitpick_Examples: theory Datatype_Nits

18:38:41 HOL-Nitpick_Examples: theory Hotel_Nits

18:38:41 HOL-Nitpick_Examples: theory Induct_Nits

18:38:42 HOL-Nitpick_Examples: theory Integer_Nits

18:38:42 HOL-Nitpick_Examples: theory Mini_Nits

18:38:43 HOL-Nitpick_Examples: theory Mono_Nits

18:38:43 HOL-Nitpick_Examples: theory Pattern_Nits

18:38:43 HOL-Nitpick_Examples: theory Quotient_Syntax

18:38:44 HOL-Nitpick_Examples: theory Quotient_Product

18:38:44 HOL-Nitpick_Examples: theory Record_Nits

18:38:44 HOL-Nitpick_Examples: theory Manual_Nits

18:38:45 HOL-Nitpick_Examples: theory Refute_Nits

18:38:50 HOL-Nitpick_Examples: theory Special_Nits

18:38:51 HOL-Nitpick_Examples: theory Tests_Nits

18:38:52 HOL-Nitpick_Examples: theory Typedef_Nits

18:38:57 HOL-Nitpick_Examples: theory Nitpick_Examples

18:41:32 Timing HOL-Decision_Procs (2 threads, 535.978s elapsed time, 827.340s cpu time, 55.056s GC time, factor 1.54)

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

18:41:32 Finished HOL-Decision_Procs (0:08:58 elapsed time, 0:13:49 cpu time, factor 1.54)

18:41:32 Running HOL-Corec_Examples ...

18:41:34 HOL-Corec_Examples: theory BNF_Corec

18:41:34 HOL-Corec_Examples: theory BNF_Axiomatization

18:41:35 HOL-Corec_Examples: theory FSet

18:41:39 HOL-Corec_Examples: theory Nat_Bijection

18:41:41 HOL-Corec_Examples: theory Stream

18:41:43 HOL-Corec_Examples: theory Iterate_GPV

18:41:43 HOL-Corec_Examples: theory LFilter

18:41:48 HOL-Corec_Examples: theory Simple_Nesting

18:41:54 HOL-Corec_Examples: theory Stream_Processor

18:42:09 HOL-Corec_Examples: theory Paper_Examples

18:43:06 HOL-Corec_Examples: theory Merge_A

18:43:06 HOL-Corec_Examples: theory GPV_Bare_Bones

18:43:12 HOL-Corec_Examples: theory Merge_B

18:43:17 HOL-Corec_Examples: theory Merge_C

18:43:21 HOL-Corec_Examples: theory Merge_Poly

18:43:23 HOL-Corec_Examples: theory Merge_D

18:43:33 HOL-Corec_Examples: theory Misc_Mono

18:43:42 HOL-ex: theory Meson_Test

18:44:09 Timing HOL-ex (2 threads, 756.115s elapsed time, 1166.644s cpu time, 91.452s GC time, factor 1.54)

18:44:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex

18:44:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/document.pdf

18:44:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/outline.pdf

18:44:09 Finished HOL-ex (0:12:54 elapsed time, 0:20:30 cpu time, factor 1.59)

18:44:09 Timing HOL-Nitpick_Examples (2 threads, 328.443s elapsed time, 134.324s cpu time, 2.648s GC time, factor 0.41)

18:44:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples

18:44:09 Finished HOL-Nitpick_Examples (0:05:30 elapsed time, 0:11:55 cpu time, factor 2.16)

18:44:09 Running HOL-Hoare_Parallel ...

18:44:09 Running HOL-MicroJava ...

18:44:11 HOL-MicroJava: theory While_Combinator

18:44:11 HOL-Hoare_Parallel: theory OG_Com

18:44:11 HOL-Hoare_Parallel: theory Graph

18:44:12 HOL-Hoare_Parallel: theory Quote_Antiquote

18:44:12 HOL-Hoare_Parallel: theory RG_Com

18:44:13 HOL-MicroJava: theory Eisbach

18:44:13 HOL-MicroJava: theory Transitive_Closure_Table

18:44:13 HOL-MicroJava: theory Semilat

18:44:14 HOL-Hoare_Parallel: theory RG_Tran

18:44:14 HOL-MicroJava: theory JBasis

18:44:14 HOL-MicroJava: theory AuxLemmas

18:44:14 HOL-MicroJava: theory Type

18:44:14 HOL-MicroJava: theory Err

18:44:14 HOL-Corec_Examples: theory Misc_Poly

18:44:14 HOL-Hoare_Parallel: theory OG_Tran

18:44:15 HOL-MicroJava: theory Listn

18:44:15 HOL-MicroJava: theory Typing_Framework

18:44:16 HOL-MicroJava: theory Opt

18:44:16 HOL-MicroJava: theory Product

18:44:16 HOL-Hoare_Parallel: theory RG_Hoare

18:44:16 HOL-MicroJava: theory SemilatAlg

18:44:16 HOL-Hoare_Parallel: theory OG_Hoare

18:44:17 HOL-MicroJava: theory Kildall

18:44:17 HOL-MicroJava: theory Decl

18:44:17 HOL-MicroJava: theory SystemClasses

18:44:17 HOL-Hoare_Parallel: theory OG_Tactics

18:44:17 HOL-Hoare_Parallel: theory RG_Syntax

18:44:17 HOL-MicroJava: theory TypeRel

18:44:17 HOL-MicroJava: theory Value

18:44:17 HOL-Hoare_Parallel: theory RG_Examples

18:44:17 HOL-Hoare_Parallel: theory OG_Syntax

18:44:18 HOL-MicroJava: theory WellForm

18:44:18 HOL-Hoare_Parallel: theory Gar_Coll

18:44:18 HOL-MicroJava: theory State

18:44:18 HOL-MicroJava: theory Term

18:44:18 HOL-MicroJava: theory Exceptions

18:44:18 HOL-MicroJava: theory LBVSpec

18:44:19 HOL-MicroJava: theory LBVComplete

18:44:19 HOL-Hoare_Parallel: theory Mul_Gar_Coll

18:44:20 HOL-MicroJava: theory LBVCorrect

18:44:20 HOL-Hoare_Parallel: theory OG_Examples

18:44:20 HOL-MicroJava: theory Typing_Framework_err

18:44:20 HOL-MicroJava: theory Abstract_BV

18:44:21 HOL-MicroJava: theory Semilattices

18:44:21 HOL-MicroJava: theory JType

18:44:22 HOL-MicroJava: theory JVMType

18:44:22 HOL-MicroJava: theory WellType

18:44:23 HOL-MicroJava: theory Conform

18:44:23 HOL-MicroJava: theory Eval

18:44:24 HOL-Hoare_Parallel: theory Hoare_Parallel

18:44:24 HOL-MicroJava: theory JVMState

18:44:24 HOL-MicroJava: theory JVMInstructions

18:44:25 HOL-MicroJava: theory JVMExceptions

18:44:25 HOL-MicroJava: theory JVMExecInstr

18:44:26 HOL-MicroJava: theory JVMExec

18:44:26 HOL-MicroJava: theory DefsComp

18:44:27 HOL-MicroJava: theory Index

18:44:27 HOL-MicroJava: theory JVMDefensive

18:44:27 HOL-MicroJava: theory JVMListExample

18:44:28 HOL-MicroJava: theory Example

18:44:28 HOL-MicroJava: theory JListExample

18:44:29 HOL-MicroJava: theory JTypeSafe

18:44:30 HOL-MicroJava: theory TypeInf

18:44:30 HOL-MicroJava: theory Effect

18:44:30 HOL-MicroJava: theory TranslCompTp

18:44:31 HOL-MicroJava: theory TranslComp

18:44:31 HOL-MicroJava: theory LemmasComp

18:44:31 HOL-MicroJava: theory CorrComp

18:44:54 HOL-MicroJava: theory BVSpec

18:44:54 HOL-MicroJava: theory Altern

18:44:55 HOL-MicroJava: theory Correct

18:44:55 HOL-MicroJava: theory BVSpecTypeSafe

18:44:56 HOL-MicroJava: theory EffectMono

18:44:56 HOL-MicroJava: theory Typing_Framework_JVM

18:44:56 HOL-MicroJava: theory BVNoTypeError

18:44:57 HOL-MicroJava: theory JVM

18:44:57 HOL-MicroJava: theory LBVJVM

18:44:57 HOL-MicroJava: theory BVExample

18:44:57 HOL-MicroJava: theory CorrCompTp

18:44:59 HOL-MicroJava: theory MicroJava

18:45:17 HOL-Corec_Examples: theory Small_Concrete

18:45:52 HOL-Corec_Examples: theory Stream_Friends

18:46:02 HOL-Corec_Examples: theory TLList_Friends

18:46:22 HOL-Corec_Examples: theory Type_Class

18:46:55 Timing HOL-Corec_Examples (2 threads, 319.931s elapsed time, 580.124s cpu time, 57.640s GC time, factor 1.81)

18:46:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples

18:46:55 Finished HOL-Corec_Examples (0:05:22 elapsed time, 0:09:42 cpu time, factor 1.81)

18:46:55 Running HOL-Datatype_Examples ...

18:46:57 HOL-Datatype_Examples: theory BNF_Axiomatization

18:46:57 HOL-Datatype_Examples: theory FSet

18:46:58 HOL-Datatype_Examples: theory Infinite_Set

18:46:58 HOL-Datatype_Examples: theory Lift_BNF

18:47:01 HOL-Datatype_Examples: theory Milner_Tofte

18:47:01 HOL-Datatype_Examples: theory Lambda_Term

18:47:03 HOL-Datatype_Examples: theory Misc_Codatatype

18:47:04 HOL-Datatype_Examples: theory Prelim

18:47:04 HOL-Datatype_Examples: theory DTree

18:47:05 HOL-Datatype_Examples: theory Parallel

18:47:05 HOL-Datatype_Examples: theory TreeFsetI

18:47:06 HOL-Datatype_Examples: theory Gram_Lang

18:47:07 HOL-Datatype_Examples: theory Nat_Bijection

18:47:08 HOL-Datatype_Examples: theory Stream

18:47:10 HOL-Datatype_Examples: theory Process

18:47:14 HOL-Datatype_Examples: theory Stream_Processor

18:47:21 Timing HOL-MicroJava (2 threads, 185.597s elapsed time, 323.172s cpu time, 9.340s GC time, factor 1.74)

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

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

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

18:47:21 Finished HOL-MicroJava (0:03:11 elapsed time, 0:05:31 cpu time, factor 1.73)

18:47:21 Running HOL-IMP ...

18:47:21 HOL-Datatype_Examples: theory Old_Datatype

18:47:23 HOL-Datatype_Examples: theory Compat

18:47:23 HOL-IMP: theory Char_ord

18:47:23 HOL-IMP: theory List_lexord

18:47:24 HOL-IMP: theory Quotient_Syntax

18:47:24 HOL-IMP: theory Simps_Case_Conv

18:47:24 HOL-IMP: theory Quotient_Option

18:47:24 HOL-IMP: theory Quotient_Product

18:47:24 HOL-IMP: theory Quotient_Set

18:47:24 HOL-IMP: theory Extended

18:47:24 HOL-IMP: theory Quotient_List

18:47:25 HOL-IMP: theory While_Combinator

18:47:31 HOL-IMP: theory AExp

18:47:31 HOL-IMP: theory C_like

18:47:33 HOL-IMP: theory ASM

18:47:34 HOL-IMP: theory BExp

18:47:36 HOL-IMP: theory Complete_Lattice

18:47:36 HOL-IMP: theory Com

18:47:36 HOL-IMP: theory Procs

18:47:37 HOL-IMP: theory ACom

18:47:38 HOL-IMP: theory Abs_Int_Tests

18:47:38 HOL-IMP: theory Big_Step

18:47:39 HOL-IMP: theory Denotational

18:47:39 HOL-IMP: theory Hoare

18:47:40 HOL-IMP: theory Hoare_Examples

18:47:40 HOL-IMP: theory Hoare_Total

18:47:40 HOL-IMP: theory Hoare_Sound_Complete

18:47:40 HOL-IMP: theory Hoare_Total_EX

18:47:41 HOL-IMP: theory VCG

18:47:41 HOL-IMP: theory VCG_Total_EX

18:47:43 HOL-IMP: theory Sec_Type_Expr

18:47:43 HOL-IMP: theory Sem_Equiv

18:47:43 Timing HOL-Hoare_Parallel (2 threads, 207.182s elapsed time, 368.784s cpu time, 5.000s GC time, factor 1.78)

18:47:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel

18:47:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf

18:47:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf

18:47:43 Finished HOL-Hoare_Parallel (0:03:33 elapsed time, 0:06:17 cpu time, factor 1.77)

18:47:43 Running HOL-Imperative_HOL ...

18:47:43 HOL-IMP: theory Sec_Typing

18:47:43 HOL-IMP: theory Sec_TypingT

18:47:43 HOL-IMP: theory Vars

18:47:43 HOL-IMP: theory Procs_Dyn_Vars_Dyn

18:47:44 HOL-IMP: theory Def_Init

18:47:44 HOL-IMP: theory Def_Init_Exp

18:47:44 HOL-IMP: theory Fold

18:47:45 HOL-IMP: theory Def_Init_Big

18:47:45 HOL-IMP: theory Live

18:47:45 HOL-Imperative_HOL: theory Adhoc_Overloading

18:47:45 HOL-Imperative_HOL: theory LaTeXsugar

18:47:45 HOL-IMP: theory Procs_Stat_Vars_Dyn

18:47:45 HOL-Imperative_HOL: theory Monad_Syntax

18:47:45 HOL-Imperative_HOL: theory Nat_Bijection

18:47:45 HOL-Imperative_HOL: theory Old_Datatype

18:47:46 HOL-IMP: theory Procs_Stat_Vars_Stat

18:47:46 HOL-IMP: theory Collecting

18:47:47 HOL-Imperative_HOL: theory Countable

18:47:49 HOL-Imperative_HOL: theory Code_Target_Int

18:47:49 HOL-Imperative_HOL: theory Code_Abstract_Nat

18:47:49 HOL-Imperative_HOL: theory Code_Target_Nat

18:47:49 HOL-Imperative_HOL: theory Multiset

18:47:49 HOL-Imperative_HOL: theory Code_Target_Numeral

18:47:49 HOL-IMP: theory Collecting1

18:47:49 HOL-Imperative_HOL: theory Heap

18:47:49 HOL-IMP: theory Collecting_Examples

18:47:50 HOL-IMP: theory OO

18:47:52 HOL-Imperative_HOL: theory Heap_Monad

18:47:54 HOL-Imperative_HOL: theory Array

18:47:54 HOL-IMP: theory Star

18:47:55 HOL-IMP: theory Compiler

18:47:55 HOL-Imperative_HOL: theory List_Sublist

18:47:55 HOL-Imperative_HOL: theory Ref

18:47:55 HOL-Imperative_HOL: theory Subarray

18:47:55 HOL-Imperative_HOL: theory Imperative_HOL

18:47:55 HOL-Imperative_HOL: theory Linked_Lists

18:47:56 HOL-Imperative_HOL: theory Overview

18:47:56 HOL-Imperative_HOL: theory Imperative_Quicksort

18:48:00 HOL-IMP: theory Compiler2

18:48:01 HOL-IMP: theory Def_Init_Small

18:48:02 HOL-IMP: theory Small_Step

18:48:03 HOL-IMP: theory Finite_Reachable

18:48:03 HOL-IMP: theory Types

18:48:03 HOL-IMP: theory Abs_Int_init

18:48:03 HOL-Datatype_Examples: theory Countable

18:48:04 HOL-IMP: theory Abs_Int0

18:48:05 HOL-Datatype_Examples: theory Misc_Datatype

18:48:06 HOL-IMP: theory Abs_State

18:48:07 HOL-IMP: theory Abs_Int1

18:48:08 HOL-IMP: theory Abs_Int1_const

18:48:11 HOL-IMP: theory Poly_Types

18:48:11 HOL-IMP: theory Abs_Int1_parity

18:48:14 HOL-IMP: theory Abs_Int2

18:48:14 HOL-IMP: theory Live_True

18:48:18 HOL-IMP: theory Abs_Int2_ivl

18:48:21 HOL-IMP: theory Abs_Int3

18:48:31 HOL-Imperative_HOL: theory Imperative_Reverse

18:48:36 HOL-Imperative_HOL: theory RBT_Impl

18:48:51 HOL-Datatype_Examples: theory Misc_Primcorec

18:48:56 HOL-Datatype_Examples: theory TreeFI

18:48:57 HOL-Datatype_Examples: theory Koenig

18:49:05 HOL-Imperative_HOL: theory Sorted_List

18:49:20 HOL-Imperative_HOL: theory SatChecker

18:49:31 HOL-Imperative_HOL: theory Imperative_HOL_ex

18:50:17 HOL-Datatype_Examples: theory Misc_Primrec

18:50:54 Timing HOL-Imperative_HOL (2 threads, 187.528s elapsed time, 206.288s cpu time, 7.656s GC time, factor 1.10)

18:50:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL

18:50:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf

18:50:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

18:50:54 Finished HOL-Imperative_HOL (0:03:11 elapsed time, 0:08:24 cpu time, factor 2.64)

18:50:54 Running HOL-Proofs-Lambda ...

18:50:56 Timing HOL-Datatype_Examples (2 threads, 238.004s elapsed time, 388.480s cpu time, 47.612s GC time, factor 1.63)

18:50:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

18:50:56 Finished HOL-Datatype_Examples (0:04:00 elapsed time, 0:06:55 cpu time, factor 1.72)

18:50:56 Running HOL-Quickcheck_Examples ...

18:50:57 HOL-Proofs-Lambda: theory GCD

18:50:59 HOL-Quickcheck_Examples: theory Completeness

18:50:59 HOL-Quickcheck_Examples: theory AList

18:50:59 HOL-Quickcheck_Examples: theory Dlist

18:51:00 HOL-Quickcheck_Examples: theory Multiset

18:51:01 HOL-Quickcheck_Examples: theory DAList

18:51:02 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces

18:51:02 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples

18:51:03 HOL-Quickcheck_Examples: theory Quickcheck_Nesting

18:51:03 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example

18:51:06 HOL-Quickcheck_Examples: theory DAList_Multiset

18:51:07 HOL-Quickcheck_Examples: theory Quickcheck_Examples

18:51:15 HOL-Proofs-Lambda: theory Code_Target_Int

18:51:16 HOL-Proofs-Lambda: theory Lambda

18:51:16 HOL-Proofs-Lambda: theory Commutation

18:51:16 HOL-Proofs-Lambda: theory ListOrder

18:51:19 HOL-Proofs-Lambda: theory ListApplication

18:51:19 HOL-Proofs-Lambda: theory ParRed

18:51:19 HOL-Proofs-Lambda: theory LambdaType

18:51:20 HOL-Proofs-Lambda: theory Eta

18:51:21 Timing HOL-IMP (2 threads, 233.391s elapsed time, 353.016s cpu time, 16.196s GC time, factor 1.51)

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

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

18:51:21 Finished HOL-IMP (0:04:00 elapsed time, 0:06:00 cpu time, factor 1.50)

18:51:21 Running HOL-Proofs-Extraction ...

18:51:22 HOL-Proofs-Lambda: theory ListBeta

18:51:23 HOL-Proofs-Lambda: theory InductTermi

18:51:23 HOL-Proofs-Lambda: theory StrongNorm

18:51:24 HOL-Proofs-Extraction: theory Adhoc_Overloading

18:51:24 HOL-Proofs-Extraction: theory Binomial

18:51:24 HOL-Proofs-Extraction: theory Code_Abstract_Nat

18:51:24 HOL-Proofs-Extraction: theory Code_Target_Nat

18:51:25 HOL-Proofs-Lambda: theory NormalForm

18:51:25 HOL-Proofs-Extraction: theory GCD

18:51:25 HOL-Proofs-Lambda: theory Standardization

18:51:26 HOL-Proofs-Lambda: theory WeakNorm

18:51:42 HOL-Proofs-Extraction: theory Monad_Syntax

18:51:42 HOL-Proofs-Extraction: theory Multiset

18:51:42 HOL-Proofs-Extraction: theory Code_Target_Int

18:51:43 HOL-Proofs-Extraction: theory Code_Target_Numeral

18:51:43 HOL-Proofs-Extraction: theory State_Monad

18:52:05 HOL-Proofs-Extraction: theory Factorial_Ring

18:52:22 HOL-Proofs-Extraction: theory Euclidean_Algorithm

18:52:36 HOL-Proofs-Extraction: theory Primes

18:52:41 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples

18:52:41 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs

18:52:41 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck

18:52:42 HOL-Quickcheck_Examples: theory Hotel_Example

18:52:47 HOL-Proofs-Extraction: theory Higman

18:52:47 HOL-Proofs-Extraction: theory Util

18:52:47 HOL-Proofs-Extraction: theory Euclid

18:52:48 HOL-Proofs-Extraction: theory Pigeonhole

18:53:32 HOL-Proofs-Extraction: theory QuotRem

18:53:37 HOL-Proofs-Extraction: theory Greatest_Common_Divisor

18:53:41 HOL-Proofs-Extraction: theory Warshall

18:53:45 HOL-Proofs-Extraction: theory Higman_Extraction

18:53:52 Timing HOL-Quickcheck_Examples (2 threads, 172.277s elapsed time, 234.488s cpu time, 7.636s GC time, factor 1.36)

18:53:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples

18:53:52 Finished HOL-Quickcheck_Examples (0:02:54 elapsed time, 0:05:38 cpu time, factor 1.93)

18:53:52 Running HOL-Bali ...

18:53:54 HOL-Bali: theory Old_Recdef

18:53:55 HOL-Bali: theory Basis

18:53:57 HOL-Bali: theory Name

18:53:57 HOL-Bali: theory Table

18:53:59 HOL-Bali: theory Type

18:54:01 HOL-Bali: theory Value

18:54:01 HOL-Bali: theory Term

18:54:02 Timing HOL-Proofs-Extraction (2 threads, 155.160s elapsed time, 273.280s cpu time, 15.000s GC time, factor 1.76)

18:54:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction

18:54:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

18:54:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

18:54:02 Finished HOL-Proofs-Extraction (0:02:39 elapsed time, 0:04:38 cpu time, factor 1.74)

18:54:02 Running HOL-Predicate_Compile_Examples ...

18:54:04 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs

18:54:04 HOL-Predicate_Compile_Examples: theory Examples

18:54:04 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck

18:54:05 HOL-Predicate_Compile_Examples: theory IMP_1

18:54:05 HOL-Predicate_Compile_Examples: theory IMP_2

18:54:07 Timing HOL-Proofs-Lambda (2 threads, 186.480s elapsed time, 215.588s cpu time, 8.272s GC time, factor 1.16)

18:54:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda

18:54:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/document.pdf

18:54:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf

18:54:07 Finished HOL-Proofs-Lambda (0:03:12 elapsed time, 0:03:42 cpu time, factor 1.16)

18:54:07 Running HOL-Number_Theory ...

18:54:07 HOL-Predicate_Compile_Examples: theory IMP_3

18:54:08 HOL-Predicate_Compile_Examples: theory IMP_4

18:54:09 HOL-Number_Theory: theory Congruence

18:54:09 HOL-Number_Theory: theory FuncSet

18:54:10 HOL-Number_Theory: theory Multiset

18:54:10 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples

18:54:10 HOL-Number_Theory: theory Lattice

18:54:13 HOL-Number_Theory: theory Group

18:54:15 HOL-Number_Theory: theory FiniteProduct

18:54:16 HOL-Number_Theory: theory Ring

18:54:17 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests

18:54:21 HOL-Predicate_Compile_Examples: theory Specialisation_Examples

18:54:26 HOL-Bali: theory Decl

18:54:31 HOL-Bali: theory TypeRel

18:54:32 HOL-Bali: theory DeclConcepts

18:54:35 HOL-Bali: theory State

18:54:35 HOL-Bali: theory WellType

18:54:39 HOL-Bali: theory Conform

18:54:40 HOL-Bali: theory Eval

18:54:44 HOL-Bali: theory DefiniteAssignment

18:54:49 HOL-Number_Theory: theory MiscAlgebra

18:54:49 HOL-Number_Theory: theory Factorial_Ring

18:54:52 HOL-Number_Theory: theory Fib

18:54:59 HOL-Bali: theory WellForm

18:55:02 HOL-Bali: theory DefiniteAssignmentCorrect

18:55:02 HOL-Bali: theory Example

18:55:04 HOL-Number_Theory: theory Euclidean_Algorithm

18:55:04 HOL-Bali: theory TypeSafe

18:55:07 HOL-Bali: theory Evaln

18:55:11 HOL-Bali: theory AxSem

18:55:11 HOL-Bali: theory Trans

18:55:16 HOL-Number_Theory: theory Primes

18:55:16 HOL-Bali: theory AxCompl

18:55:16 HOL-Bali: theory AxSound

18:55:17 HOL-Number_Theory: theory Cong

18:55:17 HOL-Number_Theory: theory Eratosthenes

18:55:17 HOL-Bali: theory AxExample

18:55:17 HOL-Number_Theory: theory Residues

18:55:20 HOL-Number_Theory: theory Euler_Criterion

18:55:21 HOL-Number_Theory: theory Gauss

18:55:21 HOL-Number_Theory: theory Pocklington

18:55:21 HOL-Number_Theory: theory Quadratic_Reciprocity

18:55:22 HOL-Number_Theory: theory Number_Theory

18:56:02 HOL-Predicate_Compile_Examples: theory Code_Prolog

18:56:02 HOL-Predicate_Compile_Examples: theory Hotel_Example

18:56:02 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples

18:56:04 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example

18:56:05 HOL-Predicate_Compile_Examples: theory Lambda_Example

18:56:06 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog

18:56:07 HOL-Predicate_Compile_Examples: theory List_Examples

18:56:12 Timing HOL-Number_Theory (2 threads, 118.525s elapsed time, 178.916s cpu time, 6.156s GC time, factor 1.51)

18:56:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory

18:56:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf

18:56:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf

18:56:12 Finished HOL-Number_Theory (0:02:04 elapsed time, 0:03:06 cpu time, factor 1.50)

18:56:12 Running HOL-Algebra ...

18:56:13 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example

18:56:14 HOL-Algebra: theory Multiset

18:56:14 HOL-Algebra: theory FuncSet

18:56:19 HOL-Algebra: theory Factorial_Ring

18:56:19 HOL-Algebra: theory Permutation

18:56:21 Timing HOL-Predicate_Compile_Examples (2 threads, 136.673s elapsed time, 229.896s cpu time, 14.216s GC time, factor 1.68)

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

18:56:21 Finished HOL-Predicate_Compile_Examples (0:02:19 elapsed time, 0:05:25 cpu time, factor 2.33)

18:56:21 Running HOL-UNITY ...

18:56:25 HOL-UNITY: theory ListOrder

18:56:25 HOL-UNITY: theory Multiset

18:56:25 HOL-UNITY: theory UNITY

18:56:26 HOL-UNITY: theory Constrains

18:56:27 HOL-UNITY: theory Deadlock

18:56:27 HOL-UNITY: theory FP

18:56:27 HOL-UNITY: theory Network

18:56:28 HOL-Algebra: theory Euclidean_Algorithm

18:56:28 HOL-UNITY: theory WFair

18:56:29 HOL-UNITY: theory SubstAx

18:56:30 HOL-UNITY: theory Detects

18:56:30 HOL-UNITY: theory Union

18:56:31 HOL-UNITY: theory Comp

18:56:31 HOL-UNITY: theory Multiset_Order

18:56:31 HOL-UNITY: theory Follows

18:56:31 HOL-UNITY: theory Guar

18:56:32 HOL-UNITY: theory Transformers

18:56:32 HOL-UNITY: theory Extend

18:56:32 HOL-UNITY: theory ProgressSets

18:56:32 HOL-UNITY: theory Project

18:56:33 HOL-UNITY: theory Rename

18:56:33 HOL-UNITY: theory Lift_prog

18:56:34 HOL-UNITY: theory ELT

18:56:34 HOL-UNITY: theory PPROD

18:56:34 HOL-UNITY: theory UNITY_Main

18:56:34 HOL-UNITY: theory Token

18:56:35 HOL-UNITY: theory AllocBase

18:56:35 HOL-UNITY: theory Alloc

18:56:35 HOL-UNITY: theory AllocImpl

18:56:38 HOL-UNITY: theory Client

18:56:38 HOL-Algebra: theory Primes

18:56:38 HOL-UNITY: theory Channel

18:56:38 HOL-UNITY: theory Common

18:56:38 HOL-UNITY: theory Counter

18:56:39 HOL-UNITY: theory Counterc

18:56:39 HOL-UNITY: theory Handshake

18:56:39 HOL-UNITY: theory Lift

18:56:40 HOL-UNITY: theory Mutex

18:56:40 HOL-UNITY: theory NSP_Bad

18:56:41 HOL-UNITY: theory PriorityAux

18:56:41 HOL-UNITY: theory Priority

18:56:41 HOL-UNITY: theory Progress

18:56:41 HOL-UNITY: theory Reach

18:56:41 HOL-UNITY: theory TimerArray

18:56:41 HOL-UNITY: theory Reachability

18:56:43 HOL-Algebra: theory Congruence

18:56:43 HOL-Algebra: theory Exponent

18:56:44 HOL-Algebra: theory Lattice

18:56:47 HOL-Algebra: theory Group

18:56:48 Timing HOL-Bali (2 threads, 161.968s elapsed time, 267.628s cpu time, 18.948s GC time, factor 1.65)

18:56:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali

18:56:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf

18:56:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf

18:56:48 Finished HOL-Bali (0:02:55 elapsed time, 0:04:46 cpu time, factor 1.63)

18:56:48 Running HOL-Word-SMT_Examples ...

18:56:49 HOL-Algebra: theory Bij

18:56:49 HOL-Algebra: theory Coset

18:56:50 HOL-Algebra: theory FiniteProduct

18:56:51 HOL-Word-SMT_Examples: theory Boogie

18:56:51 HOL-Word-SMT_Examples: theory SMT_Examples

18:56:51 HOL-Algebra: theory Ring

18:56:51 HOL-Algebra: theory Sylow

18:56:52 HOL-Word-SMT_Examples: theory SMT_Tests

18:56:52 HOL-Algebra: theory Divisibility

18:56:53 HOL-Word-SMT_Examples: theory SMT_Word_Examples

18:56:56 HOL-Algebra: theory AbelCoset

18:56:57 HOL-Algebra: theory Module

18:57:04 HOL-Algebra: theory Ideal

18:57:09 HOL-Algebra: theory RingHom

18:57:12 HOL-Algebra: theory QuotRing

18:57:12 HOL-Algebra: theory UnivPoly

18:57:13 HOL-Algebra: theory IntRing

18:57:54 Timing HOL-UNITY (2 threads, 84.813s elapsed time, 129.548s cpu time, 5.664s GC time, factor 1.53)

18:57:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY

18:57:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf

18:57:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf

18:57:54 Finished HOL-UNITY (0:01:32 elapsed time, 0:02:19 cpu time, factor 1.51)

18:57:54 Running HOL-SET_Protocol ...

18:57:56 Timing HOL-Algebra (2 threads, 97.275s elapsed time, 185.360s cpu time, 11.460s GC time, factor 1.91)

18:57:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

18:57:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

18:57:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

18:57:56 Finished HOL-Algebra (0:01:43 elapsed time, 0:03:14 cpu time, factor 1.87)

18:57:56 Running Corec ...

18:57:56 HOL-SET_Protocol: theory Nat_Bijection

18:57:57 HOL-SET_Protocol: theory Message_SET

18:57:58 Corec: theory Setup

18:57:58 Corec: theory FSet

18:57:58 Corec: theory BNF_Corec

18:58:01 HOL-SET_Protocol: theory Event_SET

18:58:02 HOL-SET_Protocol: theory Public_SET

18:58:02 HOL-SET_Protocol: theory Cardholder_Registration

18:58:02 HOL-SET_Protocol: theory Merchant_Registration

18:58:04 HOL-SET_Protocol: theory Purchase

18:58:06 Corec: theory Corec

18:58:06 HOL-SET_Protocol: theory SET_Protocol

18:58:07 Timing HOL-Word-SMT_Examples (2 threads, 75.332s elapsed time, 99.868s cpu time, 0.996s GC time, factor 1.33)

18:58:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples

18:58:07 Finished HOL-Word-SMT_Examples (0:01:18 elapsed time, 0:01:46 cpu time, factor 1.36)

18:58:07 Running HOL-Quotient_Examples ...

18:58:09 HOL-Quotient_Examples: theory Congruence

18:58:09 HOL-Quotient_Examples: theory FuncSet

18:58:10 HOL-Quotient_Examples: theory Lift_DList

18:58:10 HOL-Quotient_Examples: theory Lattice

18:58:10 HOL-Quotient_Examples: theory Lift_FSet

18:58:11 HOL-Quotient_Examples: theory Lift_Set

18:58:11 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test

18:58:12 HOL-Quotient_Examples: theory Group

18:58:15 HOL-Quotient_Examples: theory Int_Pow

18:58:15 HOL-Quotient_Examples: theory Multiset

18:58:21 HOL-Quotient_Examples: theory Quotient_Syntax

18:58:21 HOL-Quotient_Examples: theory Lift_Fun

18:58:21 HOL-Quotient_Examples: theory Quotient_Message

18:58:23 HOL-Quotient_Examples: theory Quotient_Option

18:58:23 HOL-Quotient_Examples: theory Quotient_Product

18:58:23 HOL-Quotient_Examples: theory Quotient_Rat

18:58:24 HOL-Quotient_Examples: theory Quotient_Set

18:58:24 HOL-Quotient_Examples: theory Quotient_List

18:58:24 HOL-Quotient_Examples: theory DList

18:58:25 HOL-Quotient_Examples: theory Quotient_FSet

18:58:26 HOL-Quotient_Examples: theory Quotient_Int

18:59:10 Timing HOL-SET_Protocol (2 threads, 71.317s elapsed time, 108.324s cpu time, 2.308s GC time, factor 1.52)

18:59:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol

18:59:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf

18:59:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf

18:59:10 Finished HOL-SET_Protocol (0:01:15 elapsed time, 0:01:53 cpu time, factor 1.50)

18:59:10 Running Datatypes ...

18:59:12 Timing HOL-Quotient_Examples (2 threads, 62.790s elapsed time, 95.116s cpu time, 9.060s GC time, factor 1.51)

18:59:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples

18:59:12 Finished HOL-Quotient_Examples (0:01:05 elapsed time, 0:02:47 cpu time, factor 2.56)

18:59:12 Running HOL-Analysis-ex ...

18:59:12 Datatypes: theory Setup

18:59:13 Datatypes: theory Cardinal_Notations

18:59:13 Datatypes: theory BNF_Axiomatization

18:59:13 Datatypes: theory FSet

18:59:13 Datatypes: theory Nat_Bijection

18:59:13 Datatypes: theory Old_Datatype

18:59:15 Datatypes: theory Countable

18:59:16 Datatypes: theory Simps_Case_Conv

18:59:16 Datatypes: theory Datatypes

18:59:18 Timing Corec (2 threads, 76.378s elapsed time, 106.368s cpu time, 6.836s GC time, factor 1.39)

18:59:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec

18:59:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf

18:59:18 Finished Corec (0:01:21 elapsed time, 0:01:50 cpu time, factor 1.37)

18:59:18 Running HOL-Metis_Examples ...

18:59:18 HOL-Analysis-ex: theory Approximations

18:59:20 HOL-Metis_Examples: theory Binary_Tree

18:59:20 HOL-Metis_Examples: theory Dense_Linear_Order

18:59:21 HOL-Metis_Examples: theory FuncSet

18:59:22 HOL-Metis_Examples: theory Abstraction

18:59:22 HOL-Metis_Examples: theory Function_Algebras

18:59:22 HOL-Metis_Examples: theory Message

18:59:22 HOL-Metis_Examples: theory Set_Algebras

18:59:22 HOL-Metis_Examples: theory Big_O

18:59:23 HOL-Metis_Examples: theory Sets

18:59:23 HOL-Metis_Examples: theory Tarski

18:59:25 HOL-Metis_Examples: theory Clausification

18:59:25 HOL-Metis_Examples: theory Trans_Closure

18:59:25 HOL-Metis_Examples: theory Type_Encodings

18:59:25 HOL-Metis_Examples: theory Proxies

19:00:02 Warning: missing document directory

19:00:02 Timing HOL-Analysis-ex (2 threads, 43.383s elapsed time, 51.220s cpu time, 0.480s GC time, factor 1.18)

19:00:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

19:00:02 Finished HOL-Analysis-ex (0:00:49 elapsed time, 0:00:57 cpu time, factor 1.16)

19:00:02 Running HOL-Probability-ex ...

19:00:03 Timing HOL-Metis_Examples (2 threads, 42.794s elapsed time, 67.828s cpu time, 2.764s GC time, factor 1.58)

19:00:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples

19:00:03 Finished HOL-Metis_Examples (0:00:45 elapsed time, 0:01:24 cpu time, factor 1.86)

19:00:03 Running Tutorial ...

19:00:05 Timing Datatypes (2 threads, 49.259s elapsed time, 79.556s cpu time, 5.916s GC time, factor 1.62)

19:00:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

19:00:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

19:00:05 Finished Datatypes (0:00:54 elapsed time, 0:01:24 cpu time, factor 1.55)

19:00:05 Running HOL-Isar_Examples ...

19:00:05 Tutorial: theory ToyList_Test

19:00:06 Tutorial: theory ABexpr

19:00:06 Tutorial: theory AB

19:00:07 Tutorial: theory AdvancedInd

19:00:07 HOL-Isar_Examples: theory Lattice_Syntax

19:00:07 HOL-Isar_Examples: theory Multiset

19:00:07 Tutorial: theory Base

19:00:08 Tutorial: theory CTL

19:00:08 Tutorial: theory CTLind

19:00:09 Tutorial: theory PDL

19:00:09 Tutorial: theory CodeGen

19:00:10 Tutorial: theory Nested

19:00:11 HOL-Probability-ex: theory Dining_Cryptographers

19:00:11 HOL-Probability-ex: theory Koepf_Duermuth_Countermeasure

19:00:12 Tutorial: theory Even

19:00:12 Tutorial: theory Fundata

19:00:12 HOL-Probability-ex: theory Measure_Not_CCC

19:00:12 Tutorial: theory Advanced

19:00:13 Tutorial: theory Ifexpr

19:00:13 HOL-Isar_Examples: theory Factorial_Ring

19:00:14 Tutorial: theory Itrev

19:00:14 Tutorial: theory Mutual

19:00:15 Tutorial: theory Option2

19:00:15 Tutorial: theory Plus

19:00:15 Tutorial: theory Star

19:00:15 Tutorial: theory ToyList

19:00:15 Tutorial: theory Tree

19:00:16 Tutorial: theory Trie

19:00:16 Tutorial: theory Tree2

19:00:16 Tutorial: theory appendix

19:00:16 Tutorial: theory case_exprs

19:00:16 Tutorial: theory fakenat

19:00:17 Tutorial: theory fun0

19:00:18 Tutorial: theory natsum

19:00:18 Tutorial: theory pairs2

19:00:18 Tutorial: theory prime_def

19:00:18 Tutorial: theory simp

19:00:18 Tutorial: theory simp2

19:00:18 Tutorial: theory types

19:00:18 Tutorial: theory unfoldnested

19:00:21 HOL-Isar_Examples: theory Euclidean_Algorithm

19:00:31 HOL-Isar_Examples: theory Primes

19:00:33 Tutorial: theory Message

19:00:33 Tutorial: theory Documents

19:00:35 Tutorial: theory Event

19:00:36 Tutorial: theory Public

19:00:36 Tutorial: theory NS_Public

19:00:37 HOL-Isar_Examples: theory First_Order_Logic

19:00:37 HOL-Isar_Examples: theory Basic_Logic

19:00:37 HOL-Isar_Examples: theory Cantor

19:00:37 HOL-Isar_Examples: theory Drinker

19:00:37 HOL-Isar_Examples: theory Expr_Compiler

19:00:37 HOL-Isar_Examples: theory Group

19:00:37 HOL-Isar_Examples: theory Group_Context

19:00:38 HOL-Isar_Examples: theory Group_Notepad

19:00:38 HOL-Isar_Examples: theory Hoare

19:00:38 Tutorial: theory Setup

19:00:38 Tutorial: theory Basic

19:00:38 Tutorial: theory Blast

19:00:38 Tutorial: theory Force

19:00:38 Tutorial: theory Pairs

19:00:38 Tutorial: theory Records

19:00:39 Tutorial: theory Overloading

19:00:39 HOL-Isar_Examples: theory Knaster_Tarski

19:00:39 Tutorial: theory Axioms

19:00:39 HOL-Isar_Examples: theory Fibonacci

19:00:39 HOL-Isar_Examples: theory Hoare_Ex

19:00:39 HOL-Isar_Examples: theory Mutilated_Checkerboard

19:00:39 Tutorial: theory Numbers

19:00:39 HOL-Isar_Examples: theory Peirce

19:00:40 HOL-Isar_Examples: theory Puzzle

19:00:40 Tutorial: theory Typedefs

19:00:40 HOL-Isar_Examples: theory Structured_Statements

19:00:40 HOL-Isar_Examples: theory Summation

19:00:40 HOL-Isar_Examples: theory Higher_Order_Logic

19:00:40 Tutorial: theory Recur

19:00:40 Tutorial: theory Functions

19:00:40 Tutorial: theory Relations

19:00:40 Tutorial: theory TPrimes

19:00:41 Tutorial: theory Tacticals

19:00:41 Tutorial: theory Forward

19:00:41 Tutorial: theory Examples

19:00:41 Tutorial: theory find2

19:00:46 Timing HOL-Isar_Examples (2 threads, 35.479s elapsed time, 63.980s cpu time, 2.860s GC time, factor 1.80)

19:00:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples

19:00:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf

19:00:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf

19:00:46 Finished HOL-Isar_Examples (0:00:40 elapsed time, 0:01:09 cpu time, factor 1.74)

19:00:46 Running HOL-Nonstandard_Analysis-Examples ...

19:00:47 Timing Tutorial (2 threads, 36.180s elapsed time, 66.864s cpu time, 9.276s GC time, factor 1.85)

19:00:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial

19:00:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf

19:00:47 Finished Tutorial (0:00:43 elapsed time, 0:01:13 cpu time, factor 1.70)

19:00:47 Running HOL-Hoare ...

19:00:48 HOL-Nonstandard_Analysis-Examples: theory Multiset

19:00:49 HOL-Hoare: theory Heap

19:00:49 HOL-Hoare: theory Arith2

19:00:49 HOL-Hoare: theory Hoare_Logic

19:00:50 HOL-Hoare: theory Hoare_Logic_Abort

19:00:51 HOL-Hoare: theory Examples

19:00:51 HOL-Hoare: theory HeapSyntax

19:00:52 HOL-Hoare: theory Pointer_Examples

19:00:52 HOL-Hoare: theory SchorrWaite

19:00:53 HOL-Hoare: theory Pointers0

19:00:53 Warning: missing document directory

19:00:53 Timing HOL-Probability-ex (2 threads, 41.606s elapsed time, 52.836s cpu time, 1.148s GC time, factor 1.27)

19:00:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex

19:00:53 Finished HOL-Probability-ex (0:00:51 elapsed time, 0:01:02 cpu time, factor 1.22)

19:00:53 Running HOL-Cardinals ...

19:00:53 HOL-Hoare: theory ExamplesAbort

19:00:54 HOL-Hoare: theory HeapSyntaxAbort

19:00:54 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring

19:00:54 HOL-Hoare: theory Pointer_ExamplesAbort

19:00:54 HOL-Hoare: theory SepLogHeap

19:00:54 HOL-Hoare: theory Separation

19:00:55 HOL-Hoare: theory Hoare

19:00:55 HOL-Cardinals: theory Cardinal_Notations

19:00:55 HOL-Cardinals: theory Order_Union

19:00:56 HOL-Cardinals: theory Fun_More

19:00:56 HOL-Cardinals: theory Order_Relation_More

19:00:56 HOL-Cardinals: theory Wellorder_Extension

19:00:56 HOL-Cardinals: theory Wellfounded_More

19:00:56 HOL-Cardinals: theory Wellorder_Relation

19:00:57 HOL-Cardinals: theory Wellorder_Embedding

19:00:57 HOL-Cardinals: theory Wellorder_Constructions

19:00:59 HOL-Cardinals: theory Cardinal_Order_Relation

19:00:59 HOL-Cardinals: theory Ordinal_Arithmetic

19:01:00 HOL-Cardinals: theory Cardinal_Arithmetic

19:01:00 HOL-Cardinals: theory Cardinals

19:01:01 HOL-Cardinals: theory Bounded_Set

19:01:03 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm

19:01:12 HOL-Nonstandard_Analysis-Examples: theory Primes

19:01:13 HOL-Nonstandard_Analysis-Examples: theory NSPrimes

19:01:19 Timing HOL-Hoare (2 threads, 27.148s elapsed time, 49.852s cpu time, 1.516s GC time, factor 1.84)

19:01:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare

19:01:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf

19:01:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf

19:01:19 Finished HOL-Hoare (0:00:31 elapsed time, 0:00:55 cpu time, factor 1.75)

19:01:19 Running HOL-Induct ...

19:01:20 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 31.342s elapsed time, 55.608s cpu time, 2.284s GC time, factor 1.77)

19:01:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples

19:01:20 Finished HOL-Nonstandard_Analysis-Examples (0:00:34 elapsed time, 0:00:58 cpu time, factor 1.71)

19:01:20 Timing HOL-Cardinals (2 threads, 24.135s elapsed time, 44.400s cpu time, 1.912s GC time, factor 1.84)

19:01:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals

19:01:20 Finished HOL-Cardinals (0:00:26 elapsed time, 0:00:46 cpu time, factor 1.76)

19:01:20 Running HOL-Matrix_LP ...

19:01:20 Running HOL-SPARK-Examples ...

19:01:21 HOL-Induct: theory Old_Datatype

19:01:23 HOL-Induct: theory Common_Patterns

19:01:23 HOL-Matrix_LP: theory Compute_Oracle

19:01:23 HOL-Matrix_LP: theory Lattice_Algebras

19:01:23 HOL-SPARK-Examples: theory RMD_Lemmas

19:01:23 HOL-SPARK-Examples: theory RMD

19:01:23 HOL-Matrix_LP: theory ComputeHOL

19:01:23 HOL-SPARK-Examples: theory Greatest_Common_Divisor

19:01:24 HOL-SPARK-Examples: theory Longest_Increasing_Subsequence

19:01:24 HOL-SPARK-Examples: theory RMD_Specification

19:01:24 HOL-SPARK-Examples: theory F

19:01:25 HOL-Induct: theory Com

19:01:25 HOL-Induct: theory ABexp

19:01:27 HOL-SPARK-Examples: theory Hash

19:01:28 HOL-Induct: theory Comb

19:01:28 HOL-Induct: theory Nested_Datatype

19:01:29 HOL-SPARK-Examples: theory K_L

19:01:29 HOL-Induct: theory Sexp

19:01:29 HOL-Matrix_LP: theory ComputeFloat

19:01:29 HOL-SPARK-Examples: theory K_R

19:01:29 HOL-Induct: theory SList

19:01:30 HOL-Matrix_LP: theory ComputeNumeral

19:01:30 HOL-Induct: theory Ordinals

19:01:30 HOL-SPARK-Examples: theory R_L

19:01:30 HOL-Induct: theory PropLog

19:01:30 HOL-Matrix_LP: theory LP

19:01:30 HOL-Matrix_LP: theory Matrix

19:01:31 HOL-SPARK-Examples: theory R_R

19:01:31 HOL-Induct: theory QuoDataType

19:01:31 HOL-SPARK-Examples: theory Round

19:01:31 HOL-Induct: theory QuoNestedDataType

19:01:31 HOL-SPARK-Examples: theory S_L

19:01:32 HOL-Matrix_LP: theory SparseMatrix

19:01:32 HOL-Induct: theory Sigma_Algebra

19:01:32 HOL-SPARK-Examples: theory S_R

19:01:32 HOL-Induct: theory Term

19:01:33 HOL-SPARK-Examples: theory Sqrt

19:01:34 HOL-Induct: theory Tree

19:01:36 HOL-Matrix_LP: theory Cplex

19:01:44 Timing HOL-SPARK-Examples (2 threads, 20.150s elapsed time, 34.480s cpu time, 1.064s GC time, factor 1.71)

19:01:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples

19:01:44 Finished HOL-SPARK-Examples (0:00:23 elapsed time, 0:00:37 cpu time, factor 1.61)

19:01:44 Running HOL-Statespace ...

19:01:46 Timing HOL-Induct (2 threads, 22.430s elapsed time, 41.200s cpu time, 7.112s GC time, factor 1.84)

19:01:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct

19:01:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf

19:01:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf

19:01:46 Finished HOL-Induct (0:00:26 elapsed time, 0:00:46 cpu time, factor 1.74)

19:01:46 Running HOLCF-ex ...

19:01:46 HOL-Statespace: theory DistinctTreeProver

19:01:47 Timing HOL-Matrix_LP (2 threads, 22.277s elapsed time, 39.512s cpu time, 1.544s GC time, factor 1.77)

19:01:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP

19:01:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf

19:01:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf

19:01:47 Finished HOL-Matrix_LP (0:00:27 elapsed time, 0:00:45 cpu time, factor 1.68)

19:01:47 Running Isar_Ref ...

19:01:47 HOL-Statespace: theory StateFun

19:01:48 HOL-Statespace: theory StateSpaceLocale

19:01:48 HOL-Statespace: theory StateSpaceSyntax

19:01:49 HOL-Statespace: theory StateSpaceEx

19:01:49 HOLCF-ex: theory Infinite_Set

19:01:49 HOLCF-ex: theory Concurrency_Monad

19:01:50 HOLCF-ex: theory Countable_Set

19:01:50 Isar_Ref: theory Adhoc_Overloading

19:01:50 Isar_Ref: theory Base

19:01:50 HOLCF-ex: theory Countable_Complete_Lattices

19:01:50 Isar_Ref: theory Dlist

19:01:50 Isar_Ref: theory First_Order_Logic

19:01:50 Isar_Ref: theory Document_Preparation

19:01:51 Isar_Ref: theory FSet

19:01:51 HOLCF-ex: theory Dnat

19:01:51 Isar_Ref: theory Framework

19:01:52 HOLCF-ex: theory Domain_Proofs

19:01:52 Isar_Ref: theory Generic

19:01:52 Isar_Ref: theory Inner_Syntax

19:01:53 Isar_Ref: theory Old_Datatype

19:01:53 HOLCF-ex: theory Fix2

19:01:54 HOLCF-ex: theory Hoare

19:01:54 HOLCF-ex: theory Letrec

19:01:54 HOLCF-ex: theory Loop

19:01:54 HOLCF-ex: theory Pattern_Match

19:01:54 HOLCF-ex: theory Powerdomain_ex

19:01:54 Isar_Ref: theory Old_Recdef

19:01:54 Isar_Ref: theory Outer_Syntax

19:01:55 HOLCF-ex: theory Order_Continuity

19:01:55 Isar_Ref: theory Preface

19:01:55 Isar_Ref: theory Proof

19:01:56 Isar_Ref: theory Proof_Script

19:01:56 Isar_Ref: theory HOL_Specific

19:01:56 HOLCF-ex: theory Extended_Nat

19:01:56 Isar_Ref: theory Quick_Reference

19:01:56 Isar_Ref: theory Spec

19:01:57 Isar_Ref: theory Symbols

19:01:57 Isar_Ref: theory Synopsis

19:01:57 HOLCF-ex: theory Stream

19:01:59 HOLCF-ex: theory Dagstuhl

19:01:59 HOLCF-ex: theory Focus_ex

19:02:08 Timing HOL-Statespace (2 threads, 19.656s elapsed time, 22.412s cpu time, 0.828s GC time, factor 1.14)

19:02:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace

19:02:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf

19:02:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf

19:02:08 Finished HOL-Statespace (0:00:23 elapsed time, 0:00:27 cpu time, factor 1.15)

19:02:08 Timing HOLCF-ex (2 threads, 18.061s elapsed time, 33.304s cpu time, 1.396s GC time, factor 1.84)

19:02:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex

19:02:08 Finished HOLCF-ex (0:00:21 elapsed time, 0:00:36 cpu time, factor 1.69)

19:02:08 Running HOLCF-Library ...

19:02:08 Running HOLCF-FOCUS ...

19:02:11 HOLCF-FOCUS: theory Infinite_Set

19:02:11 HOLCF-Library: theory Infinite_Set

19:02:11 HOLCF-Library: theory Bool_Discrete

19:02:11 HOLCF-Library: theory Char_Discrete

19:02:11 HOLCF-Library: theory Countable_Set

19:02:11 HOLCF-Library: theory Defl_Bifinite

19:02:11 HOLCF-FOCUS: theory Countable_Set

19:02:12 HOLCF-Library: theory Countable_Complete_Lattices

19:02:12 HOLCF-FOCUS: theory Countable_Complete_Lattices

19:02:12 HOLCF-Library: theory Int_Discrete

19:02:12 HOLCF-Library: theory List_Cpo

19:02:13 HOLCF-Library: theory Nat_Discrete

19:02:13 HOLCF-Library: theory Sum_Cpo

19:02:14 HOLCF-Library: theory List_Predomain

19:02:15 HOLCF-Library: theory Option_Cpo

19:02:15 HOLCF-Library: theory Order_Continuity

19:02:15 HOLCF-FOCUS: theory Order_Continuity

19:02:16 HOLCF-Library: theory Extended_Nat

19:02:16 HOLCF-FOCUS: theory Extended_Nat

19:02:17 Timing Isar_Ref (2 threads, 17.831s elapsed time, 33.128s cpu time, 2.016s GC time, factor 1.86)

19:02:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref

19:02:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf

19:02:17 Finished Isar_Ref (0:00:28 elapsed time, 0:00:43 cpu time, factor 1.53)

19:02:17 Running HOLCF-Tutorial ...

19:02:17 HOLCF-Library: theory Stream

19:02:17 HOLCF-FOCUS: theory Stream

19:02:19 HOLCF-Library: theory HOLCF_Library

19:02:19 HOLCF-FOCUS: theory Fstream

19:02:19 HOLCF-FOCUS: theory Fstreams

19:02:19 HOLCF-FOCUS: theory FOCUS

19:02:19 HOLCF-Tutorial: theory Domain_ex

19:02:19 HOLCF-Tutorial: theory Fixrec_ex

19:02:19 HOLCF-FOCUS: theory Stream_adm

19:02:20 HOLCF-FOCUS: theory Buffer

19:02:21 HOLCF-FOCUS: theory Buffer_adm

19:02:22 HOLCF-Tutorial: theory New_Domain

19:02:27 Timing HOLCF-FOCUS (2 threads, 15.045s elapsed time, 29.440s cpu time, 0.992s GC time, factor 1.96)

19:02:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS

19:02:27 Finished HOLCF-FOCUS (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.79)

19:02:27 Running HOL-TLA-Memory ...

19:02:28 Timing HOLCF-Library (2 threads, 15.909s elapsed time, 29.504s cpu time, 1.212s GC time, factor 1.85)

19:02:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library

19:02:28 Finished HOLCF-Library (0:00:19 elapsed time, 0:00:32 cpu time, factor 1.71)

19:02:28 Running HOL-ZF ...

19:02:29 HOL-TLA-Memory: theory RPCMemoryParams

19:02:29 HOL-TLA-Memory: theory MemoryParameters

19:02:29 HOL-TLA-Memory: theory ProcedureInterface

19:02:29 HOL-TLA-Memory: theory RPCParameters

19:02:29 HOL-TLA-Memory: theory Memory

19:02:30 HOL-ZF: theory Multiset

19:02:30 HOL-ZF: theory HOLZF

19:02:30 HOL-TLA-Memory: theory MemClerkParameters

19:02:30 HOL-TLA-Memory: theory RPC

19:02:30 HOL-ZF: theory Zet

19:02:31 HOL-TLA-Memory: theory MemClerk

19:02:31 HOL-TLA-Memory: theory MemoryImplementation

19:02:35 Timing HOLCF-Tutorial (2 threads, 13.872s elapsed time, 18.052s cpu time, 0.540s GC time, factor 1.30)

19:02:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial

19:02:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf

19:02:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf

19:02:35 Finished HOLCF-Tutorial (0:00:18 elapsed time, 0:00:22 cpu time, factor 1.26)

19:02:35 Running HOL-Hahn_Banach ...

19:02:35 HOL-ZF: theory LProd

19:02:35 HOL-ZF: theory MainZF

19:02:36 HOL-ZF: theory Games

19:02:37 HOL-Hahn_Banach: theory Infinite_Set

19:02:37 HOL-Hahn_Banach: theory Nat_Bijection

19:02:38 HOL-Hahn_Banach: theory Old_Datatype

19:02:38 HOL-Hahn_Banach: theory Set_Algebras

19:02:38 HOL-Hahn_Banach: theory Zorn_Lemma

19:02:39 HOL-Hahn_Banach: theory Countable

19:02:41 HOL-Hahn_Banach: theory Countable_Set

19:02:42 HOL-Hahn_Banach: theory Continuum_Not_Denumerable

19:02:42 HOL-Hahn_Banach: theory Bounds

19:02:42 HOL-Hahn_Banach: theory Vector_Space

19:02:43 Timing HOL-TLA-Memory (2 threads, 13.415s elapsed time, 23.604s cpu time, 0.680s GC time, factor 1.76)

19:02:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory

19:02:43 Finished HOL-TLA-Memory (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.64)

19:02:43 Running HOL-Unix ...

19:02:43 HOL-Hahn_Banach: theory Linearform

19:02:43 HOL-Hahn_Banach: theory Subspace

19:02:43 HOL-Hahn_Banach: theory Function_Order

19:02:43 HOL-Hahn_Banach: theory Normed_Space

19:02:44 HOL-Hahn_Banach: theory Function_Norm

19:02:44 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas

19:02:44 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas

19:02:45 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas

19:02:45 HOL-Unix: theory Sublist

19:02:45 HOL-Unix: theory Nested_Environment

19:02:45 HOL-Hahn_Banach: theory Hahn_Banach

19:02:45 Timing HOL-ZF (2 threads, 12.109s elapsed time, 23.212s cpu time, 1.120s GC time, factor 1.92)

19:02:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF

19:02:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf

19:02:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf

19:02:45 Finished HOL-ZF (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.72)

19:02:45 Running IOA-NTP ...

19:02:47 HOL-Unix: theory Unix

19:02:48 IOA-NTP: theory Lemmas

19:02:48 IOA-NTP: theory Multiset

19:02:48 IOA-NTP: theory Packet

19:02:48 IOA-NTP: theory Action

19:02:51 IOA-NTP: theory Abschannel

19:02:51 IOA-NTP: theory Receiver

19:02:51 Timing HOL-Hahn_Banach (2 threads, 11.000s elapsed time, 21.576s cpu time, 1.096s GC time, factor 1.96)

19:02:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

19:02:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

19:02:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

19:02:51 Finished HOL-Hahn_Banach (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.75)

19:02:51 Running HOL-NanoJava ...

19:02:51 IOA-NTP: theory Sender

19:02:52 IOA-NTP: theory Spec

19:02:52 IOA-NTP: theory Impl

19:02:53 HOL-NanoJava: theory Term

19:02:53 IOA-NTP: theory Correctness

19:02:55 HOL-NanoJava: theory Decl

19:02:56 HOL-NanoJava: theory TypeRel

19:02:56 HOL-NanoJava: theory State

19:02:57 HOL-NanoJava: theory AxSem

19:02:57 HOL-NanoJava: theory OpSem

19:02:57 Timing HOL-Unix (2 threads, 9.556s elapsed time, 18.044s cpu time, 0.920s GC time, factor 1.89)

19:02:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix

19:02:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf

19:02:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf

19:02:57 Finished HOL-Unix (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.68)

19:02:57 Running HOL-Mirabelle-ex ...

19:02:57 Timing IOA-NTP (2 threads, 8.355s elapsed time, 14.624s cpu time, 0.644s GC time, factor 1.75)

19:02:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP

19:02:57 Finished IOA-NTP (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.53)

19:02:57 Running HOLCF-IMP ...

19:02:57 HOL-NanoJava: theory Equivalence

19:02:58 HOL-NanoJava: theory Example

19:02:59 HOL-Mirabelle-ex: theory Ex

19:03:00 HOLCF-IMP: theory AExp

19:03:02 HOLCF-IMP: theory BExp

19:03:02 Timing HOL-NanoJava (2 threads, 6.624s elapsed time, 11.456s cpu time, 0.640s GC time, factor 1.73)

19:03:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava

19:03:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf

19:03:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf

19:03:02 Finished HOL-NanoJava (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.50)

19:03:02 Running Codegen ...

19:03:03 HOLCF-IMP: theory Com

19:03:04 HOLCF-IMP: theory Big_Step

19:03:05 Codegen: theory Adaptation

19:03:05 Codegen: theory Evaluation

19:03:05 Codegen: theory Further

19:03:05 HOLCF-IMP: theory Denotational

19:03:05 Codegen: theory Inductive_Predicate

19:03:06 HOLCF-IMP: theory HoareEx

19:03:06 Timing HOL-Mirabelle-ex (2 threads, 6.383s elapsed time, 0.032s cpu time, 0.000s GC time, factor 0.01)

19:03:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex

19:03:06 Finished HOL-Mirabelle-ex (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.27)

19:03:06 Running IOA-ABP ...

19:03:06 Codegen: theory Introduction

19:03:07 Timing HOLCF-IMP (2 threads, 6.594s elapsed time, 12.116s cpu time, 0.504s GC time, factor 1.84)

19:03:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP

19:03:07 Finished HOLCF-IMP (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.56)

19:03:07 Running Prog_Prove ...

19:03:07 Codegen: theory Refinement

19:03:07 Codegen: theory Foundations

19:03:09 IOA-ABP: theory Lemmas

19:03:09 IOA-ABP: theory Packet

19:03:09 IOA-ABP: theory Action

19:03:09 Prog_Prove: theory Basics

19:03:09 Prog_Prove: theory Bool_nat_list

19:03:10 Prog_Prove: theory LaTeXsugar

19:03:10 Prog_Prove: theory Isar

19:03:10 Prog_Prove: theory Logic

19:03:11 IOA-ABP: theory Abschannel

19:03:11 IOA-ABP: theory Env

19:03:11 Prog_Prove: theory MyList

19:03:11 IOA-ABP: theory Receiver

19:03:12 Prog_Prove: theory Types_and_funs

19:03:12 IOA-ABP: theory Sender

19:03:12 IOA-ABP: theory Abschannel_finite

19:03:12 IOA-ABP: theory Spec

19:03:13 IOA-ABP: theory Impl

19:03:13 IOA-ABP: theory Impl_finite

19:03:13 IOA-ABP: theory Correctness

19:03:14 Timing Codegen (2 threads, 6.187s elapsed time, 12.084s cpu time, 0.536s GC time, factor 1.95)

19:03:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

19:03:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

19:03:14 Finished Codegen (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.47)

19:03:14 Running HOL-TPTP ...

19:03:16 Timing IOA-ABP (2 threads, 6.409s elapsed time, 11.340s cpu time, 0.236s GC time, factor 1.77)

19:03:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP

19:03:16 Finished IOA-ABP (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.50)

19:03:16 Running HOL-SPARK-Manual ...

19:03:16 HOL-TPTP: theory MaSh_Export_Base

19:03:16 HOL-TPTP: theory ATP_Theory_Export

19:03:17 HOL-TPTP: theory MaSh_Eval

19:03:17 HOL-TPTP: theory THF_Arith

19:03:17 HOL-TPTP: theory TPTP_Parser

19:03:18 Timing Prog_Prove (2 threads, 5.813s elapsed time, 11.280s cpu time, 0.756s GC time, factor 1.94)

19:03:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove

19:03:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf

19:03:18 Finished Prog_Prove (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.48)

19:03:18 Running HOL-IMPP ...

19:03:19 HOL-SPARK-Manual: theory Greatest_Common_Divisor

19:03:19 HOL-SPARK-Manual: theory Complex_Types

19:03:19 HOL-TPTP: theory TPTP_Interpret

19:03:19 HOL-SPARK-Manual: theory Proc1

19:03:19 HOL-SPARK-Manual: theory Proc2

19:03:19 HOL-TPTP: theory TPTP_Proof_Reconstruction

19:03:20 HOL-SPARK-Manual: theory VC_Principles

19:03:20 HOL-SPARK-Manual: theory Reference

19:03:20 HOL-SPARK-Manual: theory Simple_Greatest_Common_Divisor

19:03:20 HOL-IMPP: theory Com

19:03:20 HOL-SPARK-Manual: theory Example_Verification

19:03:21 HOL-TPTP: theory Refute

19:03:21 HOL-TPTP: theory ATP_Problem_Import

19:03:22 HOL-IMPP: theory Natural

19:03:22 Timing HOL-TPTP (2 threads, 5.334s elapsed time, 6.300s cpu time, 0.092s GC time, factor 1.18)

19:03:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP

19:03:22 Finished HOL-TPTP (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.12)

19:03:22 Running Implementation ...

19:03:23 HOL-IMPP: theory Hoare

19:03:24 HOL-IMPP: theory Misc

19:03:24 HOL-IMPP: theory EvenOdd

19:03:25 Implementation: theory Base

19:03:25 Implementation: theory Eq

19:03:25 Implementation: theory Integration

19:03:25 Implementation: theory Isar

19:03:25 Implementation: theory Local_Theory

19:03:25 Implementation: theory ML

19:03:25 Implementation: theory Prelim

19:03:25 Timing HOL-IMPP (2 threads, 4.449s elapsed time, 7.488s cpu time, 0.208s GC time, factor 1.68)

19:03:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP

19:03:25 Finished HOL-IMPP (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.43)

19:03:25 Running Functions ...

19:03:26 Implementation: theory Proof

19:03:26 Implementation: theory Syntax

19:03:26 Implementation: theory Tactic

19:03:27 Timing HOL-SPARK-Manual (2 threads, 5.169s elapsed time, 9.168s cpu time, 0.220s GC time, factor 1.77)

19:03:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual

19:03:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf

19:03:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf

19:03:27 Finished HOL-SPARK-Manual (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.51)

19:03:27 Running HOL-IOA ...

19:03:27 Functions: theory Functions

19:03:27 Implementation: theory Logic

19:03:29 HOL-IOA: theory Asig

19:03:29 HOL-IOA: theory IOA

19:03:30 HOL-IOA: theory Solve

19:03:32 Timing Implementation (2 threads, 3.655s elapsed time, 6.332s cpu time, 0.076s GC time, factor 1.73)

19:03:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation

19:03:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf

19:03:32 Finished Implementation (0:00:09 elapsed time, 0:00:11 cpu time, factor 1.25)

19:03:32 Running HOL-Lattice ...

19:03:32 Timing Functions (2 threads, 3.067s elapsed time, 4.280s cpu time, 0.244s GC time, factor 1.40)

19:03:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions

19:03:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

19:03:32 Finished Functions (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.13)

19:03:32 Timing HOL-IOA (2 threads, 2.853s elapsed time, 4.112s cpu time, 0.132s GC time, factor 1.44)

19:03:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA

19:03:32 Finished HOL-IOA (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.23)

19:03:32 Running HOL-TLA-Inc ...

19:03:32 Running HOL-Word-Examples ...

19:03:34 HOL-Lattice: theory Orders

19:03:35 HOL-TLA-Inc: theory Inc

19:03:35 HOL-Lattice: theory Bounds

19:03:35 HOL-Word-Examples: theory WordBitwise

19:03:35 HOL-Lattice: theory Lattice

19:03:36 HOL-Lattice: theory CompleteLattice

19:03:36 HOL-Word-Examples: theory WordExamples

19:03:37 Timing HOL-TLA-Inc (2 threads, 2.404s elapsed time, 4.116s cpu time, 0.108s GC time, factor 1.71)

19:03:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc

19:03:37 Finished HOL-TLA-Inc (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.35)

19:03:37 Running Classes ...

19:03:38 Timing HOL-Word-Examples (2 threads, 2.171s elapsed time, 3.616s cpu time, 0.072s GC time, factor 1.67)

19:03:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-Examples

19:03:38 Finished HOL-Word-Examples (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.28)

19:03:38 Running Locales ...

19:03:38 Timing HOL-Lattice (2 threads, 2.301s elapsed time, 3.900s cpu time, 0.000s GC time, factor 1.70)

19:03:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice

19:03:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf

19:03:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf

19:03:38 Finished HOL-Lattice (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.37)

19:03:38 Running IOA-Storage ...

19:03:40 Classes: theory Setup

19:03:40 Classes: theory Classes

19:03:40 Locales: theory Examples

19:03:41 Locales: theory Examples1

19:03:41 Locales: theory Examples2

19:03:41 Locales: theory Examples3

19:03:42 IOA-Storage: theory Action

19:03:42 IOA-Storage: theory Impl

19:03:42 IOA-Storage: theory Spec

19:03:43 IOA-Storage: theory Correctness

19:03:44 Timing IOA-Storage (2 threads, 1.676s elapsed time, 2.472s cpu time, 0.000s GC time, factor 1.47)

19:03:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage

19:03:44 Finished IOA-Storage (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.15)

19:03:44 Running Eisbach ...

19:03:44 Timing Classes (2 threads, 2.190s elapsed time, 2.532s cpu time, 0.000s GC time, factor 1.16)

19:03:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes

19:03:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf

19:03:44 Finished Classes (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.01)

19:03:44 Timing Locales (2 threads, 1.783s elapsed time, 3.048s cpu time, 0.000s GC time, factor 1.71)

19:03:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales

19:03:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf

19:03:44 Finished Locales (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.17)

19:03:44 Running HOL-Mutabelle ...

19:03:44 Running Main ...

19:03:46 Eisbach: theory Base

19:03:46 Eisbach: theory Manual

19:03:46 Eisbach: theory Preface

19:03:46 HOL-Mutabelle: theory Refute

19:03:46 Main: theory Main_Doc

19:03:47 HOL-Mutabelle: theory MutabelleExtra

19:03:49 Timing HOL-Mutabelle (2 threads, 1.747s elapsed time, 1.844s cpu time, 0.000s GC time, factor 1.06)

19:03:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle

19:03:49 Finished HOL-Mutabelle (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.01)

19:03:49 Timing Main (2 threads, 1.259s elapsed time, 1.320s cpu time, 0.000s GC time, factor 1.05)

19:03:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main

19:03:49 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf

19:03:49 Finished Main (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.97)

19:03:49 Running HOL-Proofs-ex ...

19:03:49 Running HOL-Import ...

19:03:50 Timing Eisbach (2 threads, 1.491s elapsed time, 2.000s cpu time, 0.000s GC time, factor 1.34)

19:03:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach

19:03:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf

19:03:50 Finished Eisbach (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.04)

19:03:50 Running Sugar ...

19:03:51 HOL-Proofs-ex: theory Hilbert_Classical

19:03:51 HOL-Proofs-ex: theory Drinker

19:03:51 HOL-Proofs-ex: theory Proof_Terms

19:03:51 HOL-Import: theory Import_Setup

19:03:51 HOL-Proofs-ex: theory XML_Data

19:03:52 HOL-Import: theory HOL_Light_Maps

19:03:52 Sugar: theory LaTeXsugar

19:03:52 Sugar: theory OptionalSugar

19:03:53 Timing HOL-Proofs-ex (2 threads, 1.190s elapsed time, 2.212s cpu time, 0.000s GC time, factor 1.86)

19:03:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex

19:03:53 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.25)

19:03:53 Warning: missing document directory

19:03:53 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

19:03:53 Timing HOL-Import (2 threads, 1.052s elapsed time, 1.868s cpu time, 0.000s GC time, factor 1.77)

19:03:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import

19:03:53 Finished HOL-Import (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.20)

19:03:53 Running HOL-Nunchaku ...

19:03:53 Running HOL-Types_To_Sets ...

19:03:53 Sugar: theory Sugar

19:03:55 HOL-Types_To_Sets: theory Prerequisites

19:03:55 HOL-Types_To_Sets: theory Types_To_Sets

19:03:55 HOL-Nunchaku: theory Nunchaku

19:03:55 HOL-Types_To_Sets: theory Finite

19:03:55 HOL-Types_To_Sets: theory T2_Spaces

19:03:55 Timing Sugar (2 threads, 1.038s elapsed time, 1.208s cpu time, 0.000s GC time, factor 1.16)

19:03:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar

19:03:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

19:03:55 Finished Sugar (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.98)

19:03:55 Running IOA-ex ...

19:03:56 Timing HOL-Nunchaku (2 threads, 1.125s elapsed time, 1.196s cpu time, 0.000s GC time, factor 1.06)

19:03:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nunchaku

19:03:56 Finished HOL-Nunchaku (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)

19:03:56 Timing HOL-Types_To_Sets (2 threads, 1.057s elapsed time, 1.656s cpu time, 0.000s GC time, factor 1.57)

19:03:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets

19:03:56 Finished HOL-Types_To_Sets (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.15)

19:03:56 Running HOL-TLA-Buffer ...

19:03:56 Running JEdit ...

19:03:58 IOA-ex: theory TrivEx2

19:03:58 IOA-ex: theory TrivEx

19:03:58 JEdit: theory Base

19:03:58 HOL-TLA-Buffer: theory Buffer

19:03:59 HOL-TLA-Buffer: theory DBuffer

19:03:59 JEdit: theory JEdit

19:04:00 Timing IOA-ex (2 threads, 0.866s elapsed time, 1.800s cpu time, 0.000s GC time, factor 2.08)

19:04:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex

19:04:00 Finished IOA-ex (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.21)

19:04:00 Timing HOL-TLA-Buffer (2 threads, 0.744s elapsed time, 1.228s cpu time, 0.000s GC time, factor 1.65)

19:04:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer

19:04:00 Finished HOL-TLA-Buffer (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.14)

19:04:00 Running How_to_Prove_it ...

19:04:00 Running HOL-Prolog ...

19:04:02 HOL-Prolog: theory HOHH

19:04:02 How_to_Prove_it: theory How_to_Prove_it

19:04:02 HOL-Prolog: theory Func

19:04:02 HOL-Prolog: theory Test

19:04:02 HOL-Prolog: theory Type

19:04:02 Timing HOL-Prolog (2 threads, 0.300s elapsed time, 0.488s cpu time, 0.000s GC time, factor 1.63)

19:04:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog

19:04:02 Finished HOL-Prolog (0:00:02 elapsed time)

19:04:02 Running Typeclass_Hierarchy ...

19:04:04 Timing How_to_Prove_it (2 threads, 0.444s elapsed time, 0.576s cpu time, 0.000s GC time, factor 1.30)

19:04:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it

19:04:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

19:04:04 Finished How_to_Prove_it (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.98)

19:04:05 Typeclass_Hierarchy: theory Typeclass_Hierarchy

19:04:08 Timing Typeclass_Hierarchy (2 threads, 0.316s elapsed time, 0.404s cpu time, 0.000s GC time, factor 1.28)

19:04:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy

19:04:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

19:04:08 Finished Typeclass_Hierarchy (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.95)

19:04:08 Timing JEdit (2 threads, 0.734s elapsed time, 0.772s cpu time, 0.000s GC time, factor 1.05)

19:04:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit

19:04:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

19:04:08 Finished JEdit (0:00:11 elapsed time, 0:00:10 cpu time, factor 0.97)

19:04:08

19:04:08 === TIMING ===

19:04:08

19:04:08 Group timing: 2:09:40 elapsed time, 3:36:11 cpu time, factor 1.67

19:04:08 Group doc: 0:05:04 elapsed time, 0:07:03 cpu time, factor 1.39

19:04:08 Group main: 0:31:45 elapsed time, 0:55:30 cpu time, factor 1.75

19:04:08 Group ZF: 0:01:44 elapsed time, 0:02:54 cpu time, factor 1.66

19:04:08 Overall: 1:05:00 elapsed time, 5:33:34 cpu time, factor 5.13

19:04:08 Archiving artifacts

19:04:08 Started calculate disk usage of build

19:04:08 Finished Calculation of disk usage of build in 0 seconds

19:04:16 Started calculate disk usage of workspace

19:04:16 Finished Calculation of disk usage of workspace in 0 seconds

19:04:16 No emails were triggered.

19:04:16 Finished: SUCCESS