15:16:16 Started by upstream project "isabelle-repo" build number 492

15:16:16 originally caused by:

15:16:16 Started by an SCM change

15:16:16 [EnvInject] - Loading node environment variables.

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

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

15:16:16 [isabelle-repo-makeall] $ hg pull --rev 041cda506fb22860dd10263f930e204ea0188509

15:16:16 pulling from http://isabelle.in.tum.de/repos/isabelle/

15:16:16 searching for changes

15:16:16 adding changesets

15:16:16 adding manifests

15:16:16 adding file changes

15:16:16 added 2 changesets with 5 changes to 5 files

15:16:16 (run 'hg update' to get a working copy)

15:16:17 [isabelle-repo-makeall] $ hg update --clean --rev 041cda506fb22860dd10263f930e204ea0188509

15:16:17 5 files updated, 0 files merged, 0 files removed, 0 files unresolved

15:16:17 [isabelle-repo-makeall] $ hg --config extensions.purge= clean --all

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

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

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

15:16:17 No emails were triggered.

15:16:17 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson864029155773707812.sh

15:16:17 + Admin/jenkins/run_build makeall

15:16:17 + set -e

15:16:17 + PROFILE=makeall

15:16:17 + shift

15:16:17 + bin/isabelle components -a

15:16:17 + bin/isabelle jedit -bf

15:16:17 ### Building graph browser ...

15:16:18 warning: [options] bootstrap class path not set in conjunction with -source 1.4

15:16:18 warning: [options] source value 1.4 is obsolete and will be removed in a future release

15:16:18 warning: [options] target value 1.4 is obsolete and will be removed in a future release

15:16:18 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.

15:16:19 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.

15:16:19 Note: Recompile with -Xlint:deprecation for details.

15:16:19 4 warnings

15:16:19 ### Building Isabelle/Scala ...

15:16:57 ### Building Isabelle/jEdit ...

15:17:25 + bin/isabelle ci_build_makeall

15:17:30

15:17:30 === CONFIGURATION ===

15:17:30

15:17:30 ML_PLATFORM="x86_64-linux"

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

15:17:30 ML_SYSTEM="polyml-5.6"

15:17:30 ML_OPTIONS="-H 4000 --gcthreads 2 --maxheap 8G"

15:17:30

15:17:30 === BUILD ===

15:17:30

15:17:30 Build started at Mon, 3 Oct 2016 13:17:29 GMT

15:17:30 Isabelle id 041cda506fb2

15:17:30

15:17:30 === LOG ===

15:17:30

15:17:31 Session Pure/Pure

15:17:31 Session CCL/CCL

15:17:31 Session CTT/CTT

15:17:31 Session Cube/Cube

15:17:31 Session FOL/FOL

15:17:31 Session FOL/FOL-ex

15:17:31 Session FOLP/FOLP

15:17:31 Session FOLP/FOLP-ex

15:17:31 Session HOL/HOL (main)

15:17:32 Session Doc/Classes (doc)

15:17:32 Session Doc/Codegen_Basics

15:17:32 Session Doc/Codegen (doc)

15:17:32 Session Doc/Corec (doc)

15:17:32 Session Doc/Datatypes (doc)

15:17:32 Session Doc/Functions (doc)

15:17:32 Session HOL/HOL-Algebra (main timing)

15:17:32 Session HOL/HOL-Analysis (main timing)

15:17:32 Session HOL/HOL-Analysis-ex

15:17:32 Session HOL/HOL-Probability (timing)

15:17:33 Session HOL/HOL-Probability-ex (timing)

15:17:33 Session HOL/HOL-Auth (timing)

15:17:33 Session HOL/HOL-UNITY (timing)

15:17:33 Session HOL/HOL-Bali (timing)

15:17:33 Session HOL/HOL-Cardinals (timing)

15:17:33 Session HOL/HOL-Corec_Examples (timing)

15:17:33 Session HOL/HOL-Data_Structures (timing)

15:17:33 Session HOL/HOL-Datatype_Examples (timing)

15:17:33 Session HOL/HOL-Decision_Procs (timing)

15:17:34 Session HOL/HOL-Eisbach

15:17:34 Session Doc/Eisbach (doc)

15:17:34 Session HOL/HOL-Hahn_Banach

15:17:34 Session HOL/HOL-Hoare

15:17:34 Session HOL/HOL-Hoare_Parallel (timing)

15:17:34 Session HOL/HOL-IMP (timing)

15:17:34 Session HOL/HOL-IMPP

15:17:34 Session HOL/HOL-IOA

15:17:34 Session HOL/HOL-Imperative_HOL

15:17:34 Session HOL/HOL-Import

15:17:34 Session HOL/HOL-Induct

15:17:34 Session HOL/HOL-Isar_Examples

15:17:34 Session HOL/HOL-Lattice

15:17:34 Session HOL/HOL-Library (main timing)

15:17:35 Session HOL/HOL-Codegenerator_Test

15:17:35 Session HOL/HOL-Matrix_LP

15:17:35 Session HOL/HOL-Metis_Examples (timing)

15:17:35 Session HOL/HOL-MicroJava (timing)

15:17:35 Session HOL/HOL-Mirabelle

15:17:35 Session HOL/HOL-Mirabelle-ex

15:17:35 Session HOL/HOL-Mutabelle

15:17:35 Session HOL/HOL-NanoJava

15:17:35 Session HOL/HOL-Nitpick_Examples

15:17:35 Session HOL/HOL-Nominal

15:17:35 Session HOL/HOL-Nominal-Examples (timing)

15:17:35 Session HOL/HOL-Nonstandard_Analysis (timing)

15:17:35 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

15:17:35 Session HOL/HOL-Number_Theory (timing)

15:17:36 Session HOL/HOL-Old_Number_Theory

15:17:36 Session HOL/HOL-Predicate_Compile_Examples (timing)

15:17:36 Session HOL/HOL-Prolog

15:17:36 Session HOL/HOL-Quickcheck_Examples (timing)

15:17:36 Session HOL/HOL-Quotient_Examples (timing)

15:17:36 Session HOL/HOL-SET_Protocol (timing)

15:17:36 Session HOL/HOL-Statespace

15:17:36 Session HOL/HOL-TLA

15:17:36 Session HOL/HOL-TLA-Buffer

15:17:36 Session HOL/HOL-TLA-Inc

15:17:36 Session HOL/HOL-TLA-Memory

15:17:36 Session HOL/HOL-TPTP

15:17:36 Session HOL/HOL-Unix

15:17:36 Session HOL/HOL-Word (main timing)

15:17:36 Session HOL/HOL-SPARK (main)

15:17:36 Session HOL/HOL-SPARK-Examples

15:17:36 Session HOL/HOL-SPARK-Manual

15:17:36 Session HOL/HOL-Word-Examples

15:17:36 Session HOL/HOL-Word-SMT_Examples (timing)

15:17:36 Session HOL/HOL-ZF

15:17:37 Session HOL/HOL-ex

15:17:37 Session HOL/HOLCF (main timing)

15:17:37 Session HOL/HOLCF-FOCUS

15:17:37 Session HOL/HOLCF-IMP

15:17:37 Session HOL/HOLCF-Library

15:17:37 Session HOL/HOLCF-Tutorial

15:17:37 Session HOL/HOLCF-ex

15:17:37 Session HOL/IOA (timing)

15:17:37 Session HOL/IOA-ABP

15:17:37 Session HOL/IOA-NTP

15:17:37 Session HOL/IOA-Storage

15:17:37 Session HOL/IOA-ex

15:17:37 Session Doc/How_to_Prove_it

15:17:37 Session Doc/Implementation (doc)

15:17:37 Session Doc/Isar_Ref (doc)

15:17:37 Session Doc/JEdit (doc)

15:17:37 Session Doc/Locales (doc)

15:17:37 Session Doc/Main (doc)

15:17:37 Session Doc/Prog_Prove (doc)

15:17:37 Session Doc/Sugar (doc)

15:17:37 Session Doc/Tutorial (doc)

15:17:37 Session Doc/Typeclass_Hierarchy_Basics

15:17:37 Session Doc/Typeclass_Hierarchy (doc)

15:17:37 Session HOL/HOL-Proofs (timing)

15:17:38 Session HOL/HOL-Proofs-Extraction (timing)

15:17:38 Session HOL/HOL-Proofs-Lambda (timing)

15:17:38 Session HOL/HOL-Proofs-ex

15:17:38 Session Doc/Intro (doc)

15:17:38 Session LCF/LCF

15:17:38 Session Doc/Logics (doc)

15:17:38 Session Doc/Nitpick (doc)

15:17:38 Session Unsorted/SML

15:17:38 Session Sequents/Sequents

15:17:38 Session Doc/Sledgehammer (doc)

15:17:38 Session Unsorted/Spec_Check

15:17:38 Session Doc/System (doc)

15:17:38 Session ZF/ZF (main timing ZF)

15:17:38 Session Doc/Logics_ZF (doc)

15:17:38 Session ZF/ZF-AC (ZF)

15:17:38 Session ZF/ZF-Coind (ZF)

15:17:38 Session ZF/ZF-Constructible (ZF)

15:17:38 Session ZF/ZF-IMP (ZF)

15:17:38 Session ZF/ZF-Induct (ZF)

15:17:38 Session ZF/ZF-Resid (ZF)

15:17:38 Session ZF/ZF-UNITY (timing ZF)

15:17:38 Session ZF/ZF-ex (ZF)

15:17:38 Building Pure ...

15:17:49 Pure: theory Pure

15:17:50 Pure: theory ML_Bootstrap

15:17:53 Warning: missing document directory

15:17:53 Timing Pure (2 threads, 0.757s elapsed time, 0.788s cpu time, 0.000s GC time, factor 1.04)

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

15:17:53 Finished Pure (0:00:13 elapsed time, 0:00:14 cpu time, factor 1.08)

15:17:53 Building HOL ...

15:17:53 Building ZF ...

15:17:53 Building HOL-Proofs ...

15:17:53 ZF: theory IFOL

15:17:53 HOL-Proofs: theory Proofs

15:17:54 HOL-Proofs: theory Code_Generator

15:17:54 HOL: theory Code_Generator

15:17:54 ZF: theory FOL

15:17:56 ZF: theory ZF

15:17:56 ZF: theory upair

15:17:56 ZF: theory pair

15:17:56 HOL-Proofs: theory HOL

15:17:56 ZF: theory Bool

15:17:56 ZF: theory equalities

15:17:56 HOL: theory HOL

15:17:57 ZF: theory Fixedpt

15:17:57 ZF: theory Sum

15:17:57 ZF: theory func

15:17:58 ZF: theory Perm

15:17:58 ZF: theory QPair

15:17:58 ZF: theory Trancl

15:17:58 ZF: theory EquivClass

15:17:58 ZF: theory WF

15:17:58 ZF: theory Order

15:17:58 ZF: theory Ordinal

15:17:59 ZF: theory OrdQuant

15:17:59 ZF: theory OrderArith

15:17:59 ZF: theory Nat_ZF

15:17:59 ZF: theory Epsilon

15:17:59 ZF: theory OrderType

15:17:59 ZF: theory Inductive_ZF

15:18:00 ZF: theory Finite

15:18:00 ZF: theory Cardinal

15:18:00 HOL-Proofs: theory Argo

15:18:00 HOL-Proofs: theory Ctr_Sugar

15:18:00 HOL: theory Argo

15:18:00 HOL: theory Ctr_Sugar

15:18:00 ZF: theory Univ

15:18:01 ZF: theory Arith

15:18:01 ZF: theory QUniv

15:18:01 ZF: theory Datatype_ZF

15:18:01 ZF: theory ArithSimp

15:18:01 ZF: theory Int_ZF

15:18:01 ZF: theory CardinalArith

15:18:01 HOL: theory Orderings

15:18:01 HOL-Proofs: theory Orderings

15:18:02 ZF: theory List_ZF

15:18:02 ZF: theory Bin

15:18:02 HOL-Proofs: theory SAT

15:18:02 HOL: theory SAT

15:18:03 ZF: theory IntDiv_ZF

15:18:03 HOL: theory Groups

15:18:03 HOL-Proofs: theory Groups

15:18:03 ZF: theory Main_ZF

15:18:04 ZF: theory AC

15:18:04 ZF: theory Zorn

15:18:04 ZF: theory Main

15:18:04 ZF: theory Cardinal_AC

15:18:04 ZF: theory InfDatatype

15:18:04 ZF: theory Main_ZFC

15:18:06 HOL: theory Lattices

15:18:07 HOL-Proofs: theory Lattices

15:18:08 HOL: theory Set

15:18:09 HOL: theory Fun

15:18:09 HOL: theory Typedef

15:18:09 HOL-Proofs: theory Set

15:18:10 HOL: theory Rings

15:18:10 HOL: theory Complete_Lattices

15:18:11 HOL-Proofs: theory Fun

15:18:11 HOL-Proofs: theory Typedef

15:18:11 HOL-Proofs: theory Rings

15:18:12 HOL-Proofs: theory Complete_Lattices

15:18:13 HOL: theory Inductive

15:18:14 HOL: theory Product_Type

15:18:15 HOL-Proofs: theory Inductive

15:18:16 HOL: theory Complete_Partial_Order

15:18:16 HOL: theory Sum_Type

15:18:17 HOL-Proofs: theory Product_Type

15:18:19 HOL-Proofs: theory Complete_Partial_Order

15:18:19 HOL: theory Nat

15:18:19 HOL-Proofs: theory Sum_Type

15:18:21 HOL: theory Fields

15:18:21 HOL: theory Meson

15:18:21 HOL: theory ATP

15:18:22 HOL-Proofs: theory Nat

15:18:24 HOL: theory Metis

15:18:24 Timing ZF (2 threads, 18.407s elapsed time, 34.244s cpu time, 2.144s GC time, factor 1.86)

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

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

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

15:18:24 Finished ZF (0:00:30 elapsed time, 0:00:54 cpu time, factor 1.78)

15:18:24 Building FOL ...

15:18:24 HOL-Proofs: theory Fields

15:18:24 FOL: theory IFOL

15:18:25 HOL: theory Finite_Set

15:18:26 FOL: theory FOL

15:18:26 HOL: theory Relation

15:18:27 HOL-Proofs: theory Meson

15:18:27 HOL-Proofs: theory ATP

15:18:28 HOL: theory Transitive_Closure

15:18:29 HOL: theory Wellfounded

15:18:29 HOL-Proofs: theory Finite_Set

15:18:30 HOL: theory Fun_Def_Base

15:18:30 HOL: theory Hilbert_Choice

15:18:30 HOL: theory Wfrec

15:18:30 HOL: theory Order_Relation

15:18:30 HOL: theory BNF_Wellorder_Relation

15:18:30 HOL: theory Zorn

15:18:30 HOL-Proofs: theory Metis

15:18:30 Timing FOL (2 threads, 2.901s elapsed time, 3.200s cpu time, 0.140s GC time, factor 1.10)

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

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

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

15:18:30 Finished FOL (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.24)

15:18:30 Building FOLP ...

15:18:31 HOL: theory BNF_Wellorder_Embedding

15:18:31 FOLP: theory IFOLP

15:18:31 HOL-Proofs: theory Relation

15:18:31 HOL: theory BNF_Wellorder_Constructions

15:18:31 FOLP: theory FOLP

15:18:32 HOL: theory BNF_Cardinal_Order_Relation

15:18:32 HOL-Proofs: theory Transitive_Closure

15:18:32 Timing FOLP (2 threads, 1.006s elapsed time, 1.012s cpu time, 0.000s GC time, factor 1.01)

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

15:18:32 Finished FOLP (0:00:01 elapsed time)

15:18:33 Running CCL ...

15:18:33 HOL: theory BNF_Cardinal_Arithmetic

15:18:33 CCL: theory IFOL

15:18:33 HOL: theory BNF_Def

15:18:34 HOL-Proofs: theory Wellfounded

15:18:34 CCL: theory FOL

15:18:35 HOL-Proofs: theory Fun_Def_Base

15:18:35 HOL-Proofs: theory Hilbert_Choice

15:18:35 HOL-Proofs: theory Wfrec

15:18:35 HOL: theory BNF_Composition

15:18:35 HOL: theory Basic_BNFs

15:18:35 HOL-Proofs: theory Order_Relation

15:18:35 HOL-Proofs: theory BNF_Wellorder_Relation

15:18:35 HOL-Proofs: theory Zorn

15:18:35 HOL-Proofs: theory BNF_Wellorder_Embedding

15:18:36 CCL: theory Set

15:18:36 CCL: theory Lfp

15:18:36 CCL: theory Gfp

15:18:36 CCL: theory CCL

15:18:36 HOL: theory BNF_Fixpoint_Base

15:18:36 HOL-Proofs: theory BNF_Wellorder_Constructions

15:18:36 CCL: theory Term

15:18:36 CCL: theory Trancl

15:18:37 CCL: theory Type

15:18:37 HOL-Proofs: theory BNF_Cardinal_Order_Relation

15:18:37 CCL: theory Fix

15:18:37 CCL: theory Hered

15:18:37 CCL: theory Wfd

15:18:38 HOL-Proofs: theory BNF_Cardinal_Arithmetic

15:18:38 CCL: theory Nat

15:18:38 CCL: theory List

15:18:38 CCL: theory Flag

15:18:38 CCL: theory Stream

15:18:38 HOL-Proofs: theory BNF_Def

15:18:39 HOL: theory BNF_Least_Fixpoint

15:18:39 Timing CCL (2 threads, 5.689s elapsed time, 8.132s cpu time, 0.500s GC time, factor 1.43)

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

15:18:39 Finished CCL (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.39)

15:18:39 Running CTT ...

15:18:39 CTT: theory CTT

15:18:40 CTT: theory Bool

15:18:40 CTT: theory Elimination

15:18:40 CTT: theory Arith

15:18:40 CTT: theory Equality

15:18:40 CTT: theory Typechecking

15:18:40 CTT: theory Synthesis

15:18:40 CTT: theory Main

15:18:40 HOL-Proofs: theory BNF_Composition

15:18:41 HOL-Proofs: theory Basic_BNFs

15:18:41 HOL: theory Basic_BNF_LFPs

15:18:41 HOL: theory Num

15:18:41 HOL-Proofs: theory BNF_Fixpoint_Base

15:18:42 HOL: theory Transfer

15:18:42 Timing CTT (2 threads, 0.913s elapsed time, 1.320s cpu time, 0.000s GC time, factor 1.45)

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

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

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

15:18:42 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)

15:18:42 Running Cube ...

15:18:42 Cube: theory Cube

15:18:42 Cube: theory Example

15:18:43 Timing Cube (2 threads, 0.366s elapsed time, 0.372s cpu time, 0.000s GC time, factor 1.02)

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

15:18:43 Finished Cube (0:00:00 elapsed time)

15:18:43 Running FOL-ex ...

15:18:43 FOL-ex: theory Classical

15:18:43 FOL-ex: theory If

15:18:43 FOL-ex: theory Intro

15:18:43 FOL-ex: theory Miniscope

15:18:43 FOL-ex: theory Nat

15:18:44 FOL-ex: theory Nat_Class

15:18:44 FOL-ex: theory Natural_Numbers

15:18:44 FOL-ex: theory Prolog

15:18:44 FOL-ex: theory Propositional_Cla

15:18:44 FOL-ex: theory Quantifiers_Cla

15:18:44 FOL-ex: theory Foundation

15:18:44 FOL-ex: theory Intuitionistic

15:18:44 FOL-ex: theory Propositional_Int

15:18:44 HOL: theory Power

15:18:44 FOL-ex: theory Quantifiers_Int

15:18:44 HOL-Proofs: theory BNF_Least_Fixpoint

15:18:46 HOL: theory Groups_Big

15:18:46 FOL-ex: theory Locale_Test1

15:18:47 HOL-Proofs: theory Basic_BNF_LFPs

15:18:47 HOL-Proofs: theory Num

15:18:47 HOL-Proofs: theory Transfer

15:18:48 HOL: theory Equiv_Relations

15:18:48 HOL: theory Lifting

15:18:49 FOL-ex: theory Locale_Test2

15:18:49 FOL-ex: theory Locale_Test3

15:18:49 FOL-ex: theory Locale_Test

15:18:50 HOL: theory Lifting_Set

15:18:50 HOL: theory Option

15:18:50 HOL: theory Quotient

15:18:51 HOL-Proofs: theory Power

15:18:51 HOL: theory Extraction

15:18:51 Timing FOL-ex (2 threads, 5.705s elapsed time, 8.080s cpu time, 0.184s GC time, factor 1.42)

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

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

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

15:18:51 Finished FOL-ex (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.43)

15:18:51 Running FOLP-ex ...

15:18:51 FOLP-ex: theory Classical

15:18:51 FOLP-ex: theory If

15:18:51 HOL: theory Lattices_Big

15:18:51 FOLP-ex: theory Intro

15:18:52 FOLP-ex: theory Nat

15:18:52 FOLP-ex: theory Propositional_Cla

15:18:52 FOLP-ex: theory Quantifiers_Cla

15:18:52 FOLP-ex: theory Foundation

15:18:52 FOLP-ex: theory Intuitionistic

15:18:53 HOL: theory Partial_Function

15:18:53 HOL-Proofs: theory Groups_Big

15:18:53 HOL: theory Fun_Def

15:18:54 FOLP-ex: theory Propositional_Int

15:18:54 FOLP-ex: theory Quantifiers_Int

15:18:55 HOL: theory Int

15:18:56 Timing FOLP-ex (2 threads, 3.671s elapsed time, 6.280s cpu time, 0.132s GC time, factor 1.71)

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

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

15:18:56 Running Intro ...

15:18:56 HOL-Proofs: theory Equiv_Relations

15:18:57 HOL-Proofs: theory Lifting

15:18:57 HOL: theory Nat_Transfer

15:18:58 HOL: theory Parity

15:18:58 HOL-Proofs: theory Lifting_Set

15:18:58 HOL-Proofs: theory Option

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

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

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

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

15:18:58 Running LCF ...

15:18:58 LCF: theory IFOL

15:18:58 HOL-Proofs: theory Quotient

15:18:59 HOL-Proofs: theory Lattices_Big

15:18:59 LCF: theory FOL

15:18:59 HOL: theory Divides

15:19:00 HOL-Proofs: theory Partial_Function

15:19:01 HOL-Proofs: theory Fun_Def

15:19:01 LCF: theory LCF

15:19:01 LCF: theory Ex1

15:19:01 LCF: theory Ex2

15:19:01 LCF: theory Ex3

15:19:01 LCF: theory Ex4

15:19:02 Timing LCF (2 threads, 2.982s elapsed time, 3.376s cpu time, 0.136s GC time, factor 1.13)

15:19:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

15:19:02 Finished LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.09)

15:19:02 Running Logics ...

15:19:02 HOL-Proofs: theory Int

15:19:04 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

15:19:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics

15:19:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf

15:19:04 Finished Logics (0:00:02 elapsed time)

15:19:04 Running Logics_ZF ...

15:19:04 Logics_ZF: theory FOL_examples

15:19:04 Logics_ZF: theory If

15:19:04 Logics_ZF: theory ZF_Isar

15:19:04 HOL: theory Code_Numeral

15:19:05 Logics_ZF: theory ZF_examples

15:19:05 Logics_ZF: theory IFOL_examples

15:19:05 HOL-Proofs: theory Nat_Transfer

15:19:05 HOL-Proofs: theory Parity

15:19:05 HOL: theory Numeral_Simprocs

15:19:06 HOL: theory SMT

15:19:08 HOL-Proofs: theory Divides

15:19:08 Timing Logics_ZF (2 threads, 0.413s elapsed time, 0.724s cpu time, 0.000s GC time, factor 1.75)

15:19:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

15:19:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

15:19:08 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)

15:19:08 Running Nitpick ...

15:19:08 HOL: theory Semiring_Normalization

15:19:10 HOL: theory Groebner_Basis

15:19:10 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

15:19:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

15:19:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

15:19:10 Finished Nitpick (0:00:02 elapsed time)

15:19:10 Running SML ...

15:19:10 SML: theory Examples

15:19:11 HOL: theory Set_Interval

15:19:11 Warning: missing document directory

15:19:11 Timing SML (2 threads, 0.018s elapsed time, 0.020s cpu time, 0.000s GC time, factor 1.11)

15:19:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

15:19:11 Finished SML (0:00:00 elapsed time)

15:19:11 Running Sequents ...

15:19:11 Sequents: theory Sequents

15:19:11 Sequents: theory ILL

15:19:11 Sequents: theory LK0

15:19:11 Sequents: theory ILL_predlog

15:19:12 Sequents: theory Washing

15:19:12 Sequents: theory LK

15:19:12 Sequents: theory Modal0

15:19:12 Sequents: theory S4

15:19:12 Sequents: theory S43

15:19:12 Sequents: theory Hard_Quantifiers

15:19:12 Sequents: theory Nat

15:19:12 Sequents: theory Propositional

15:19:12 Sequents: theory Quantifiers

15:19:12 Sequents: theory T

15:19:13 HOL-Proofs: theory Code_Numeral

15:19:13 HOL: theory Conditionally_Complete_Lattices

15:19:14 HOL: theory Filter

15:19:14 HOL-Proofs: theory Numeral_Simprocs

15:19:15 HOL: theory Presburger

15:19:15 HOL-Proofs: theory SMT

15:19:15 Timing Sequents (2 threads, 3.829s elapsed time, 7.368s cpu time, 0.152s GC time, factor 1.92)

15:19:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

15:19:15 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.79)

15:19:15 Running Sledgehammer ...

15:19:17 HOL-Proofs: theory Semiring_Normalization

15:19:17 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

15:19:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

15:19:17 Finished Sledgehammer (0:00:01 elapsed time)

15:19:17 Running Spec_Check ...

15:19:17 HOL: theory Sledgehammer

15:19:17 Spec_Check: theory Spec_Check

15:19:18 Spec_Check: theory Examples

15:19:19 HOL: theory List

15:19:20 HOL-Proofs: theory Groebner_Basis

15:19:20 Warning: missing document directory

15:19:20 Timing Spec_Check (2 threads, 1.990s elapsed time, 3.376s cpu time, 0.016s GC time, factor 1.70)

15:19:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

15:19:20 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

15:19:20 Running System ...

15:19:20 System: theory Base

15:19:20 System: theory Environment

15:19:20 System: theory Misc

15:19:20 System: theory Presentation

15:19:20 System: theory Scala

15:19:20 System: theory Sessions

15:19:21 HOL-Proofs: theory Set_Interval

15:19:23 Timing System (2 threads, 0.314s elapsed time, 0.440s cpu time, 0.000s GC time, factor 1.40)

15:19:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

15:19:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

15:19:23 Finished System (0:00:02 elapsed time)

15:19:23 Running ZF-AC ...

15:19:23 ZF-AC: theory AC_Equiv

15:19:23 ZF-AC: theory AC18_AC19

15:19:23 ZF-AC: theory AC7_AC9

15:19:23 ZF-AC: theory Cardinal_aux

15:19:24 ZF-AC: theory Hartog

15:19:24 ZF-AC: theory WO6_WO1

15:19:24 ZF-AC: theory AC16_lemmas

15:19:24 HOL-Proofs: theory Presburger

15:19:24 ZF-AC: theory AC16_WO4

15:19:24 ZF-AC: theory DC

15:19:24 ZF-AC: theory HH

15:19:24 ZF-AC: theory AC15_WO6

15:19:24 ZF-AC: theory AC17_AC1

15:19:24 ZF-AC: theory WO1_AC

15:19:25 ZF-AC: theory WO1_WO7

15:19:25 ZF-AC: theory WO2_AC16

15:19:26 HOL-Proofs: theory Sledgehammer

15:19:27 HOL: theory Groups_List

15:19:27 HOL: theory Map

15:19:28 HOL: theory Random

15:19:28 HOL: theory Enum

15:19:28 HOL-Proofs: theory List

15:19:30 HOL: theory String

15:19:30 Timing ZF-AC (2 threads, 5.087s elapsed time, 9.828s cpu time, 0.472s GC time, factor 1.93)

15:19:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

15:19:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

15:19:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

15:19:30 Finished ZF-AC (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.77)

15:19:31 Running ZF-Coind ...

15:19:31 ZF-Coind: theory Language

15:19:31 ZF-Coind: theory Map

15:19:31 HOL: theory BNF_Greatest_Fixpoint

15:19:31 HOL: theory Predicate

15:19:31 ZF-Coind: theory Types

15:19:31 ZF-Coind: theory Values

15:19:31 ZF-Coind: theory Dynamic

15:19:31 ZF-Coind: theory Static

15:19:31 ZF-Coind: theory ECR

15:19:32 Timing ZF-Coind (2 threads, 0.796s elapsed time, 1.460s cpu time, 0.000s GC time, factor 1.83)

15:19:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

15:19:32 Finished ZF-Coind (0:00:01 elapsed time)

15:19:32 Running ZF-Constructible ...

15:19:32 HOL: theory Lazy_Sequence

15:19:32 ZF-Constructible: theory Formula

15:19:32 ZF-Constructible: theory MetaExists

15:19:32 ZF-Constructible: theory Normal

15:19:33 ZF-Constructible: theory Reflection

15:19:33 HOL: theory Limited_Sequence

15:19:33 ZF-Constructible: theory Relative

15:19:34 HOL: theory Typerep

15:19:35 HOL: theory Code_Evaluation

15:19:35 ZF-Constructible: theory L_axioms

15:19:35 ZF-Constructible: theory Wellorderings

15:19:35 ZF-Constructible: theory WFrec

15:19:36 HOL: theory Quickcheck_Random

15:19:36 ZF-Constructible: theory WF_absolute

15:19:37 ZF-Constructible: theory Datatype_absolute

15:19:37 ZF-Constructible: theory Rank

15:19:38 ZF-Constructible: theory Separation

15:19:38 ZF-Constructible: theory Internalize

15:19:38 HOL: theory Quickcheck_Exhaustive

15:19:38 HOL: theory Quickcheck_Narrowing

15:19:38 ZF-Constructible: theory AC_in_L

15:19:39 ZF-Constructible: theory Rec_Separation

15:19:40 ZF-Constructible: theory Rank_Separation

15:19:40 ZF-Constructible: theory Satisfies_absolute

15:19:41 ZF-Constructible: theory DPow_absolute

15:19:42 HOL: theory Record

15:19:42 HOL: theory Random_Pred

15:19:43 HOL: theory Random_Sequence

15:19:44 HOL: theory Nitpick

15:19:44 HOL: theory Predicate_Compile

15:19:49 HOL: theory Main

15:19:51 HOL: theory Archimedean_Field

15:19:51 HOL: theory Binomial

15:19:52 Timing ZF-Constructible (2 threads, 14.825s elapsed time, 29.680s cpu time, 5.328s GC time, factor 2.00)

15:19:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

15:19:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

15:19:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

15:19:52 Finished ZF-Constructible (0:00:19 elapsed time, 0:00:36 cpu time, factor 1.92)

15:19:52 Running ZF-IMP ...

15:19:52 ZF-IMP: theory Com

15:19:52 HOL: theory GCD

15:19:52 ZF-IMP: theory Denotation

15:19:52 ZF-IMP: theory Equiv

15:19:53 Timing ZF-IMP (2 threads, 1.124s elapsed time, 1.388s cpu time, 0.000s GC time, factor 1.24)

15:19:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

15:19:53 Finished ZF-IMP (0:00:01 elapsed time)

15:19:53 Running ZF-Induct ...

15:19:53 ZF-Induct: theory Acc

15:19:53 ZF-Induct: theory Binary_Trees

15:19:53 ZF-Induct: theory Comb

15:19:54 ZF-Induct: theory Datatypes

15:19:54 ZF-Induct: theory FoldSet

15:19:54 ZF-Induct: theory ListN

15:19:54 ZF-Induct: theory Mutil

15:19:54 ZF-Induct: theory Multiset

15:19:54 ZF-Induct: theory Ntree

15:19:54 ZF-Induct: theory Primrec

15:19:54 ZF-Induct: theory PropLog

15:19:55 ZF-Induct: theory Rmap

15:19:55 ZF-Induct: theory Term

15:19:55 ZF-Induct: theory Tree_Forest

15:19:55 ZF-Induct: theory Brouwer

15:19:55 HOL: theory Topological_Spaces

15:19:57 HOL: theory Rat

15:19:59 HOL: theory Real

15:20:03 HOL: theory Real_Vector_Spaces

15:20:03 Timing ZF-Induct (2 threads, 6.078s elapsed time, 11.164s cpu time, 0.492s GC time, factor 1.84)

15:20:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

15:20:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

15:20:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

15:20:03 Finished ZF-Induct (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.72)

15:20:03 Running ZF-Resid ...

15:20:03 ZF-Resid: theory Redex

15:20:03 ZF-Resid: theory Substitution

15:20:03 ZF-Resid: theory Residuals

15:20:04 ZF-Resid: theory Reduction

15:20:04 ZF-Resid: theory Confluence

15:20:05 Timing ZF-Resid (2 threads, 1.612s elapsed time, 2.928s cpu time, 0.128s GC time, factor 1.82)

15:20:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

15:20:05 Finished ZF-Resid (0:00:02 elapsed time, 0:00:03 cpu time)

15:20:05 Running ZF-UNITY ...

15:20:06 ZF-UNITY: theory Acc

15:20:06 ZF-UNITY: theory FoldSet

15:20:06 ZF-UNITY: theory GenPrefix

15:20:06 ZF-UNITY: theory Multiset

15:20:06 ZF-UNITY: theory State

15:20:06 ZF-UNITY: theory UNITY

15:20:07 ZF-UNITY: theory Constrains

15:20:07 ZF-UNITY: theory MultisetSum

15:20:07 ZF-UNITY: theory Monotonicity

15:20:07 ZF-UNITY: theory FP

15:20:07 ZF-UNITY: theory WFair

15:20:07 ZF-UNITY: theory Increasing

15:20:07 ZF-UNITY: theory SubstAx

15:20:08 ZF-UNITY: theory Follows

15:20:08 ZF-UNITY: theory Mutex

15:20:08 ZF-UNITY: theory Union

15:20:09 ZF-UNITY: theory Comp

15:20:09 ZF-UNITY: theory Guar

15:20:10 ZF-UNITY: theory AllocBase

15:20:10 ZF-UNITY: theory ClientImpl

15:20:10 ZF-UNITY: theory Distributor

15:20:10 ZF-UNITY: theory Merge

15:20:10 ZF-UNITY: theory AllocImpl

15:20:14 HOL: theory Inequalities

15:20:14 HOL: theory Limits

15:20:17 HOL: theory Deriv

15:20:18 HOL: theory Series

15:20:19 HOL: theory NthRoot

15:20:20 HOL: theory Transcendental

15:20:23 Timing ZF-UNITY (2 threads, 16.972s elapsed time, 32.860s cpu time, 1.224s GC time, factor 1.94)

15:20:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

15:20:23 Finished ZF-UNITY (0:00:17 elapsed time, 0:00:33 cpu time, factor 1.91)

15:20:23 Running ZF-ex ...

15:20:23 ZF-ex: theory BinEx

15:20:23 ZF-ex: theory CoUnit

15:20:23 ZF-ex: theory Commutation

15:20:23 ZF-ex: theory Group

15:20:23 ZF-ex: theory LList

15:20:23 ZF-ex: theory Limit

15:20:24 ZF-ex: theory Ring

15:20:24 HOL: theory Complex

15:20:25 ZF-ex: theory NatSum

15:20:25 HOL: theory MacLaurin

15:20:25 ZF-ex: theory Primes

15:20:25 ZF-ex: theory Ramsey

15:20:25 ZF-ex: theory misc

15:20:26 HOL: theory Complex_Main

15:20:31 Timing ZF-ex (2 threads, 7.942s elapsed time, 15.544s cpu time, 0.640s GC time, factor 1.96)

15:20:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

15:20:31 Finished ZF-ex (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.89)

15:24:08 Timing HOL (2 threads, 275.327s elapsed time, 539.484s cpu time, 47.716s GC time, factor 1.96)

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

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

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

15:24:08 Finished HOL (0:06:15 elapsed time, 0:11:40 cpu time, factor 1.87)

15:24:10 Building HOLCF ...

15:24:11 Building HOL-TLA ...

15:24:12 HOLCF: theory Nat_Bijection

15:24:12 HOLCF: theory Old_Datatype

15:24:12 HOL-TLA: theory Intensional

15:24:12 HOL-TLA: theory Stfun

15:24:12 HOL-TLA: theory Action

15:24:13 HOL-TLA: theory Init

15:24:13 HOL-TLA: theory TLA

15:24:14 HOLCF: theory Countable

15:24:16 HOLCF: theory Porder

15:24:16 HOLCF: theory Pcpo

15:24:18 HOLCF: theory Cont

15:24:18 HOLCF: theory Adm

15:24:18 HOLCF: theory Discrete

15:24:18 HOLCF: theory Cpodef

15:24:19 HOLCF: theory Fun_Cpo

15:24:19 HOLCF: theory Product_Cpo

15:24:19 HOLCF: theory Cfun

15:24:20 HOLCF: theory Cprod

15:24:20 HOLCF: theory Fix

15:24:20 HOLCF: theory Sfun

15:24:20 HOLCF: theory Sprod

15:24:20 HOLCF: theory Up

15:24:21 HOLCF: theory Lift

15:24:22 HOLCF: theory One

15:24:22 HOLCF: theory Tr

15:24:22 HOLCF: theory Ssum

15:24:22 HOLCF: theory Plain_HOLCF

15:24:23 HOLCF: theory Completion

15:24:23 HOLCF: theory Deflation

15:24:23 HOLCF: theory Map_Functions

15:24:23 HOLCF: theory Fixrec

15:24:24 HOLCF: theory Bifinite

15:24:24 HOLCF: theory Domain_Aux

15:24:25 HOLCF: theory Universal

15:24:26 HOLCF: theory Algebraic

15:24:26 HOLCF: theory Compact_Basis

15:24:26 HOLCF: theory LowerPD

15:24:27 HOLCF: theory UpperPD

15:24:27 HOLCF: theory Representable

15:24:27 Timing HOL-TLA (2 threads, 2.378s elapsed time, 4.088s cpu time, 0.148s GC time, factor 1.72)

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

15:24:27 Finished HOL-TLA (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.47)

15:24:27 Building HOL-Word ...

15:24:27 HOLCF: theory ConvexPD

15:24:28 HOL-Word: theory Bit

15:24:28 HOL-Word: theory Bits

15:24:29 HOL-Word: theory Boolean_Algebra

15:24:29 HOL-Word: theory Bits_Bit

15:24:29 HOL-Word: theory Misc_Numeric

15:24:30 HOL-Word: theory Bit_Representation

15:24:30 HOL-Word: theory Misc_Typedef

15:24:30 HOLCF: theory Domain

15:24:30 HOL-Word: theory Phantom_Type

15:24:30 HOL-Word: theory Bits_Int

15:24:31 HOL-Word: theory Cardinality

15:24:31 HOLCF: theory Powerdomains

15:24:32 HOL-Word: theory Bool_List_Representation

15:24:32 HOL-Word: theory Numeral_Type

15:24:32 HOLCF: theory HOLCF

15:24:33 HOL-Word: theory Type_Length

15:24:34 HOL-Word: theory Word_Miscellaneous

15:24:34 HOL-Word: theory Word

15:25:03 Timing HOLCF (2 threads, 25.079s elapsed time, 49.080s cpu time, 2.176s GC time, factor 1.96)

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

15:25:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

15:25:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

15:25:03 Finished HOLCF (0:00:52 elapsed time, 0:01:30 cpu time, factor 1.73)

15:25:03 Building IOA ...

15:25:05 IOA: theory Seq

15:25:05 IOA: theory Asig

15:25:05 IOA: theory Automata

15:25:07 IOA: theory Sequence

15:25:07 IOA: theory Pred

15:25:08 IOA: theory Traces

15:25:08 IOA: theory TL

15:25:09 IOA: theory CompoExecs

15:25:09 IOA: theory RefMappings

15:25:09 IOA: theory RefCorrectness

15:25:09 IOA: theory CompoScheds

15:25:10 IOA: theory Simulations

15:25:10 IOA: theory SimCorrectness

15:25:11 IOA: theory Deadlock

15:25:11 IOA: theory ShortExecutions

15:25:11 IOA: theory CompoTraces

15:25:12 IOA: theory Compositionality

15:25:12 IOA: theory IOA

15:25:13 IOA: theory TLS

15:25:14 IOA: theory LiveIOA

15:25:14 IOA: theory Abstraction

15:25:16 Timing HOL-Word (2 threads, 23.588s elapsed time, 46.960s cpu time, 1.632s GC time, factor 1.99)

15:25:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word

15:25:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf

15:25:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf

15:25:16 Finished HOL-Word (0:00:48 elapsed time, 0:01:24 cpu time, factor 1.75)

15:25:16 Building HOL-Analysis ...

15:25:19 HOL-Analysis: theory Disjoint_Sets

15:25:19 HOL-Analysis: theory FuncSet

15:25:20 HOL-Analysis: theory Infinite_Set

15:25:20 HOL-Analysis: theory Multiset

15:25:20 HOL-Analysis: theory Nat_Bijection

15:25:21 HOL-Analysis: theory Old_Datatype

15:25:23 HOL-Analysis: theory Countable

15:25:24 HOL-Analysis: theory Countable_Set

15:25:25 HOL-Analysis: theory Countable_Complete_Lattices

15:25:25 HOL-Analysis: theory Permutations

15:25:27 HOL-Analysis: theory Phantom_Type

15:25:28 HOL-Analysis: theory Cardinality

15:25:28 HOL-Analysis: theory Product_Plus

15:25:28 HOL-Analysis: theory Product_Order

15:25:29 HOL-Analysis: theory Set_Algebras

15:25:29 HOL-Analysis: theory Numeral_Type

15:25:29 HOL-Analysis: theory L2_Norm

15:25:29 HOL-Analysis: theory Continuum_Not_Denumerable

15:25:30 HOL-Analysis: theory Indicator_Function

15:25:30 HOL-Analysis: theory Inner_Product

15:25:30 HOL-Analysis: theory Liminf_Limsup

15:25:31 HOL-Analysis: theory Product_Vector

15:25:31 HOL-Analysis: theory Nonpos_Ints

15:25:32 HOL-Analysis: theory Operator_Norm

15:25:32 HOL-Analysis: theory Euclidean_Space

15:25:32 HOL-Analysis: theory Order_Continuity

15:25:33 HOL-Analysis: theory Extended_Nat

15:25:34 HOL-Analysis: theory Extended_Real

15:25:34 HOL-Analysis: theory Finite_Cartesian_Product

15:25:35 HOL-Analysis: theory Linear_Algebra

15:25:38 HOL-Analysis: theory Extended_Nonnegative_Real

15:25:38 HOL-Analysis: theory Periodic_Fun

15:25:39 HOL-Analysis: theory Poly_Roots

15:25:39 HOL-Analysis: theory Sum_of_Squares

15:25:41 HOL-Analysis: theory Sigma_Algebra

15:25:42 HOL-Analysis: theory Norm_Arith

15:25:42 HOL-Analysis: theory Topology_Euclidean_Space

15:25:44 Timing IOA (2 threads, 18.944s elapsed time, 37.376s cpu time, 1.288s GC time, factor 1.97)

15:25:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA

15:25:44 Finished IOA (0:00:40 elapsed time, 0:01:08 cpu time, factor 1.72)

15:25:44 Building HOL-SPARK ...

15:25:44 HOL-Analysis: theory Measurable

15:25:45 HOL-Analysis: theory Measure_Space

15:25:46 HOL-SPARK: theory Bit_Comparison

15:25:46 HOL-SPARK: theory SPARK_Setup

15:25:48 HOL-Analysis: theory Caratheodory

15:25:49 HOL-Analysis: theory Summation_Tests

15:25:49 HOL-SPARK: theory SPARK

15:25:52 HOL-Analysis: theory Bounded_Linear_Function

15:25:52 HOL-Analysis: theory Convex_Euclidean_Space

15:25:54 HOL-Analysis: theory Extended_Real_Limits

15:25:55 HOL-Analysis: theory Tagged_Division

15:25:57 HOL-Analysis: theory Uniform_Limit

15:25:59 HOL-Analysis: theory Continuous_Extension

15:25:59 HOL-Analysis: theory Path_Connected

15:26:03 HOL-Analysis: theory Homeomorphism

15:26:03 Timing HOL-SPARK (2 threads, 3.705s elapsed time, 7.140s cpu time, 0.052s GC time, factor 1.93)

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

15:26:03 Finished HOL-SPARK (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.53)

15:26:03 Building Codegen_Basics ...

15:26:03 HOL-Analysis: theory Brouwer_Fixpoint

15:26:05 Codegen_Basics: theory Dlist

15:26:05 Codegen_Basics: theory IArray

15:26:05 HOL-Analysis: theory Derivative

15:26:06 Codegen_Basics: theory Mapping

15:26:07 Codegen_Basics: theory RBT_Impl

15:26:08 HOL-Analysis: theory Cartesian_Euclidean_Space

15:26:08 HOL-Analysis: theory Weierstrass_Theorems

15:26:11 HOL-Analysis: theory Determinants

15:26:11 HOL-Analysis: theory Fashoda_Theorem

15:26:11 HOL-Analysis: theory Ordered_Euclidean_Space

15:26:12 HOL-Analysis: theory Polytope

15:26:17 HOL-Analysis: theory Borel_Space

15:26:19 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

15:26:19 HOL-Analysis: theory Regularity

15:26:22 HOL-Analysis: theory Binary_Product_Measure

15:26:23 HOL-Analysis: theory Embed_Measure

15:26:23 HOL-Analysis: theory Finite_Product_Measure

15:26:25 HOL-Analysis: theory Bochner_Integration

15:26:27 HOL-Analysis: theory Complete_Measure

15:26:27 HOL-Analysis: theory Radon_Nikodym

15:26:28 HOL-Analysis: theory Set_Integral

15:26:28 HOL-Analysis: theory Lebesgue_Measure

15:26:30 HOL-Analysis: theory Henstock_Kurzweil_Integration

15:26:34 HOL-Analysis: theory Bounded_Continuous_Function

15:26:34 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

15:26:34 HOL-Analysis: theory Integral_Test

15:26:35 HOL-Analysis: theory Complex_Analysis_Basics

15:26:35 HOL-Analysis: theory Interval_Integral

15:26:36 HOL-Analysis: theory Lebesgue_Integral_Substitution

15:26:37 HOL-Analysis: theory FurtherTopology

15:26:37 HOL-Analysis: theory Complex_Transcendental

15:26:39 HOL-Analysis: theory Generalised_Binomial_Theorem

15:26:39 HOL-Analysis: theory Harmonic_Numbers

15:26:39 HOL-Analysis: theory Cauchy_Integral_Theorem

15:26:40 HOL-Analysis: theory Gamma_Function

15:26:42 Codegen_Basics: theory RBT

15:26:43 Codegen_Basics: theory Setup

15:26:44 HOL-Analysis: theory Conformal_Mappings

15:26:46 HOL-Analysis: theory Analysis

15:27:41 Timing Codegen_Basics (2 threads, 58.050s elapsed time, 114.800s cpu time, 3.968s GC time, factor 1.98)

15:27:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

15:27:41 Finished Codegen_Basics (0:01:37 elapsed time, 0:02:57 cpu time, factor 1.81)

15:27:42 Building HOL-Auth ...

15:27:43 HOL-Auth: theory Message

15:27:43 HOL-Auth: theory Nat_Bijection

15:27:44 HOL-Auth: theory Simps_Case_Conv

15:27:47 HOL-Auth: theory All_Symmetric

15:27:47 HOL-Auth: theory Event

15:27:47 HOL-Auth: theory EventSC

15:27:48 HOL-Auth: theory Extensions

15:27:49 HOL-Auth: theory Analz

15:27:49 HOL-Auth: theory List_Msg

15:27:49 HOL-Auth: theory Guard

15:27:50 HOL-Auth: theory GuardK

15:27:51 HOL-Auth: theory Public

15:27:51 HOL-Auth: theory Shared

15:27:51 HOL-Auth: theory CertifiedEmail

15:27:52 HOL-Auth: theory Guard_Public

15:27:52 HOL-Auth: theory Guard_NS_Public

15:27:52 HOL-Auth: theory P2

15:27:52 HOL-Auth: theory Proto

15:27:54 HOL-Auth: theory KerberosIV

15:27:56 HOL-Auth: theory KerberosIV_Gets

15:27:56 HOL-Auth: theory KerberosV

15:27:58 HOL-Auth: theory Kerberos_BAN

15:27:58 HOL-Auth: theory Kerberos_BAN_Gets

15:27:58 HOL-Auth: theory NS_Public

15:27:59 HOL-Auth: theory NS_Public_Bad

15:27:59 HOL-Auth: theory NS_Shared

15:27:59 HOL-Auth: theory OtwayRees

15:28:00 HOL-Auth: theory OtwayReesBella

15:28:00 HOL-Auth: theory OtwayRees_AN

15:28:00 HOL-Auth: theory OtwayRees_Bad

15:28:01 HOL-Auth: theory P1

15:28:01 HOL-Auth: theory Recur

15:28:02 HOL-Auth: theory WooLam

15:28:03 HOL-Auth: theory Yahalom

15:28:04 HOL-Auth: theory Yahalom2

15:28:05 HOL-Auth: theory Yahalom_Bad

15:28:05 HOL-Auth: theory ZhouGollmann

15:28:06 HOL-Auth: theory Auth_Shared

15:28:07 HOL-Auth: theory Auth_Guard_Public

15:28:07 HOL-Auth: theory Guard_Shared

15:28:08 HOL-Auth: theory Guard_OtwayRees

15:28:08 HOL-Auth: theory Guard_Yahalom

15:28:08 HOL-Auth: theory TLS

15:28:08 HOL-Auth: theory Auth_Guard_Shared

15:28:09 HOL-Auth: theory Smartcard

15:28:09 HOL-Auth: theory ShoupRubin

15:28:10 HOL-Auth: theory Auth_Public

15:28:11 HOL-Auth: theory ShoupRubinBella

15:28:13 HOL-Auth: theory Auth_Smartcard

15:30:55 Timing HOL-Auth (2 threads, 153.427s elapsed time, 303.548s cpu time, 8.572s GC time, factor 1.98)

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

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

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

15:30:55 Finished HOL-Auth (0:03:13 elapsed time, 0:06:06 cpu time, factor 1.90)

15:30:56 Building HOL-Eisbach ...

15:30:57 HOL-Eisbach: theory Eisbach

15:30:57 HOL-Eisbach: theory IFOL

15:30:58 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax

15:30:58 HOL-Eisbach: theory Eisbach_Tools

15:30:58 HOL-Eisbach: theory Examples

15:30:59 HOL-Eisbach: theory Tests

15:30:59 HOL-Eisbach: theory FOL

15:31:01 HOL-Eisbach: theory Examples_FOL

15:31:15 Warning: missing document directory

15:31:15 Timing HOL-Eisbach (2 threads, 4.761s elapsed time, 8.660s cpu time, 0.084s GC time, factor 1.82)

15:31:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

15:31:15 Finished HOL-Eisbach (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.54)

15:31:15 Building HOL-Library ...

15:31:18 HOL-Library: theory Adhoc_Overloading

15:31:18 HOL-Library: theory Lattice_Syntax

15:31:18 HOL-Library: theory AList

15:31:18 HOL-Library: theory BNF_Axiomatization

15:31:18 HOL-Library: theory BNF_Corec

15:31:20 HOL-Library: theory DAList

15:31:22 HOL-Library: theory Stirling

15:31:22 HOL-Library: theory Bit

15:31:23 HOL-Library: theory Bits

15:31:23 HOL-Library: theory Bits_Bit

15:31:24 HOL-Library: theory Boolean_Algebra

15:31:24 HOL-Library: theory Cardinal_Notations

15:31:24 HOL-Library: theory Char_ord

15:31:24 HOL-Library: theory Code_Abstract_Nat

15:31:24 HOL-Library: theory Code_Binary_Nat

15:31:25 HOL-Library: theory Code_Target_Nat

15:31:25 HOL-Library: theory Code_Char

15:31:25 HOL-Library: theory Code_Prolog

15:31:26 HOL-Library: theory Code_Test

15:31:26 HOL-Library: theory Combine_PER

15:31:26 HOL-Library: theory Complete_Partial_Order2

15:31:26 HOL-Library: theory Debug

15:31:26 HOL-Library: theory Discrete

15:31:27 HOL-Library: theory Disjoint_Sets

15:31:27 HOL-Library: theory Dlist

15:31:28 HOL-Library: theory FSet

15:31:29 HOL-Library: theory Fraction_Field

15:31:31 HOL-Library: theory Fun_Lexorder

15:31:31 HOL-Library: theory FuncSet

15:31:31 HOL-Library: theory Function_Algebras

15:31:31 HOL-Library: theory Function_Division

15:31:32 HOL-Library: theory Finite_Map

15:31:32 HOL-Library: theory Code_Target_Int

15:31:32 HOL-Library: theory Code_Target_Numeral

15:31:32 HOL-Library: theory Groups_Big_Fun

15:31:33 HOL-Library: theory IArray

15:31:33 HOL-Library: theory Infinite_Set

15:31:34 HOL-Library: theory LaTeXsugar

15:31:34 HOL-Library: theory Lattice_Constructions

15:31:34 HOL-Library: theory Omega_Words_Fun

15:31:34 HOL-Library: theory ListVector

15:31:35 HOL-Library: theory List_lexord

15:31:35 HOL-Library: theory Mapping

15:31:36 HOL-Library: theory AList_Mapping

15:31:37 HOL-Library: theory Misc_Numeric

15:31:37 HOL-Library: theory Bit_Representation

15:31:37 HOL-Library: theory Misc_Typedef

15:31:37 HOL-Library: theory Monad_Syntax

15:31:37 HOL-Library: theory More_List

15:31:37 HOL-Library: theory Bits_Int

15:31:37 HOL-Library: theory Multiset

15:31:39 HOL-Library: theory Nat_Bijection

15:31:39 HOL-Library: theory Stream

15:31:41 HOL-Library: theory Old_Datatype

15:31:42 HOL-Library: theory DAList_Multiset

15:31:43 HOL-Library: theory Factorial_Ring

15:31:43 HOL-Library: theory Multiset_Order

15:31:44 HOL-Library: theory Permutation

15:31:44 HOL-Library: theory Permutations

15:31:45 HOL-Library: theory Countable

15:31:47 HOL-Library: theory Countable_Set

15:31:47 HOL-Library: theory Countable_Complete_Lattices

15:31:50 HOL-Library: theory Countable_Set_Type

15:31:51 HOL-Library: theory Euclidean_Algorithm

15:31:53 HOL-Library: theory Old_Recdef

15:31:54 HOL-Library: theory Option_ord

15:31:54 HOL-Library: theory Parallel

15:31:55 HOL-Library: theory Perm

15:31:56 HOL-Library: theory Phantom_Type

15:31:57 HOL-Library: theory Cardinality

15:31:58 HOL-Library: theory FinFun

15:32:00 HOL-Library: theory Normalized_Fraction

15:32:00 HOL-Library: theory Numeral_Type

15:32:01 HOL-Library: theory Predicate_Compile_Alternative_Defs

15:32:01 HOL-Library: theory Predicate_Compile_Quickcheck

15:32:01 HOL-Library: theory Type_Length

15:32:02 HOL-Library: theory Saturated

15:32:02 HOL-Library: theory Product_Lexorder

15:32:02 HOL-Library: theory Product_Plus

15:32:02 HOL-Library: theory Quotient_Syntax

15:32:02 HOL-Library: theory Product_Order

15:32:02 HOL-Library: theory Quotient_Option

15:32:02 HOL-Library: theory Quotient_Product

15:32:02 HOL-Library: theory Finite_Lattice

15:32:02 HOL-Library: theory Quotient_Set

15:32:02 HOL-Library: theory Quotient_List

15:32:03 HOL-Library: theory Quotient_Sum

15:32:03 HOL-Library: theory Quotient_Type

15:32:03 HOL-Library: theory RBT_Impl

15:32:06 HOL-Library: theory Ramsey

15:32:06 HOL-Library: theory Reflection

15:32:06 HOL-Library: theory Refute

15:32:07 HOL-Library: theory Rewrite

15:32:07 HOL-Library: theory Set_Algebras

15:32:07 HOL-Library: theory Simps_Case_Conv

15:32:08 HOL-Library: theory Extended

15:32:09 HOL-Library: theory State_Monad

15:32:10 HOL-Library: theory Sublist

15:32:11 HOL-Library: theory Prefix_Order

15:32:11 HOL-Library: theory Sublist_Order

15:32:11 HOL-Library: theory Polynomial

15:32:16 HOL-Library: theory BigO

15:32:17 HOL-Library: theory Bool_List_Representation

15:32:19 HOL-Library: theory Code_Real_Approx_By_Float

15:32:19 HOL-Library: theory Diagonal_Subsequence

15:32:20 HOL-Library: theory Formal_Power_Series

15:32:24 HOL-Library: theory Polynomial_FPS

15:32:25 HOL-Library: theory Fundamental_Theorem_Algebra

15:32:26 HOL-Library: theory Indicator_Function

15:32:26 HOL-Library: theory Lattice_Algebras

15:32:32 HOL-Library: theory Liminf_Limsup

15:32:33 HOL-Library: theory Log_Nat

15:32:33 HOL-Library: theory Float

15:32:36 HOL-Library: theory Lub_Glb

15:32:37 HOL-Library: theory Multiset_Permutations

15:32:38 HOL-Library: theory Nonpos_Ints

15:32:38 HOL-Library: theory OptionalSugar

15:32:39 HOL-Library: theory Order_Continuity

15:32:40 HOL-Library: theory Extended_Nat

15:32:41 HOL-Library: theory RBT

15:32:41 HOL-Library: theory Extended_Real

15:32:42 HOL-Library: theory RBT_Mapping

15:32:42 HOL-Library: theory RBT_Set

15:32:44 HOL-Library: theory Linear_Temporal_Logic_on_Streams

15:32:45 HOL-Library: theory Periodic_Fun

15:32:45 HOL-Library: theory Extended_Nonnegative_Real

15:32:46 HOL-Library: theory Polynomial_Factorial

15:32:48 HOL-Library: theory Quadratic_Discriminant

15:32:48 HOL-Library: theory Sum_of_Squares

15:32:49 HOL-Library: theory Transitive_Closure_Table

15:32:50 HOL-Library: theory Tree

15:32:51 HOL-Library: theory While_Combinator

15:32:52 HOL-Library: theory Bourbaki_Witt_Fixpoint

15:32:53 HOL-Library: theory Word_Miscellaneous

15:32:53 HOL-Library: theory Word

15:32:53 HOL-Library: theory Tree_Multiset

15:32:54 HOL-Library: theory Preorder

15:32:54 HOL-Library: theory Function_Growth

15:32:55 HOL-Library: theory Library

15:32:59 HOL-Library: theory Old_SMT

15:33:51 HOL-Proofs: theory Conditionally_Complete_Lattices

15:33:51 HOL-Proofs: theory Extraction

15:33:55 HOL-Proofs: theory Filter

15:33:56 HOL-Proofs: theory Groups_List

15:33:56 HOL-Proofs: theory Map

15:33:57 HOL-Proofs: theory Enum

15:33:57 HOL-Proofs: theory Random

15:34:00 HOL-Proofs: theory String

15:34:01 HOL-Proofs: theory BNF_Greatest_Fixpoint

15:34:01 HOL-Proofs: theory Predicate

15:34:03 HOL-Proofs: theory Lazy_Sequence

15:34:04 HOL-Proofs: theory Limited_Sequence

15:34:06 HOL-Proofs: theory Typerep

15:34:07 HOL-Proofs: theory Code_Evaluation

15:34:09 HOL-Proofs: theory Quickcheck_Random

15:34:11 HOL-Proofs: theory Quickcheck_Exhaustive

15:34:11 HOL-Proofs: theory Quickcheck_Narrowing

15:34:17 HOL-Proofs: theory Random_Pred

15:34:17 HOL-Proofs: theory Record

15:34:18 HOL-Proofs: theory Random_Sequence

15:34:20 HOL-Proofs: theory Nitpick

15:34:20 HOL-Proofs: theory Predicate_Compile

15:34:27 HOL-Proofs: theory Main

15:34:29 HOL-Proofs: theory Old_Datatype

15:39:44 Timing HOL-Library (2 threads, 370.186s elapsed time, 727.552s cpu time, 52.812s GC time, factor 1.97)

15:39:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library

15:39:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf

15:39:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf

15:39:44 Finished HOL-Library (0:08:27 elapsed time, 0:15:52 cpu time, factor 1.87)

15:39:46 Building HOL-Mirabelle ...

15:39:47 HOL-Mirabelle: theory Mirabelle

15:39:47 HOL-Mirabelle: theory Mirabelle_Test

15:39:55 Timing HOL-Proofs (2 threads, 1250.899s elapsed time, 2289.068s cpu time, 128.172s GC time, factor 1.83)

15:39:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

15:39:55 Finished HOL-Proofs (0:22:01 elapsed time, 0:40:03 cpu time, factor 1.82)

15:39:58 Building HOL-Nominal ...

15:39:59 HOL-Nominal: theory Infinite_Set

15:39:59 HOL-Nominal: theory Old_Datatype

15:40:00 HOL-Nominal: theory Nominal

15:40:02 Timing HOL-Mirabelle (2 threads, 1.129s elapsed time, 1.716s cpu time, 0.000s GC time, factor 1.52)

15:40:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

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

15:40:02 Building HOL-Nonstandard_Analysis ...

15:40:03 HOL-Nonstandard_Analysis: theory Infinite_Set

15:40:03 HOL-Nonstandard_Analysis: theory Lub_Glb

15:40:04 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

15:40:04 HOL-Nonstandard_Analysis: theory StarDef

15:40:06 HOL-Nonstandard_Analysis: theory HyperNat

15:40:06 HOL-Nonstandard_Analysis: theory HyperDef

15:40:08 HOL-Nonstandard_Analysis: theory NSA

15:40:10 HOL-Nonstandard_Analysis: theory NSComplex

15:40:10 HOL-Nonstandard_Analysis: theory Star

15:40:11 HOL-Nonstandard_Analysis: theory HLim

15:40:11 HOL-Nonstandard_Analysis: theory NatStar

15:40:12 HOL-Nonstandard_Analysis: theory HDeriv

15:40:12 HOL-Nonstandard_Analysis: theory HSEQ

15:40:13 HOL-Nonstandard_Analysis: theory HSeries

15:40:13 HOL-Nonstandard_Analysis: theory HTranscendental

15:40:14 HOL-Nonstandard_Analysis: theory HLog

15:40:14 HOL-Nonstandard_Analysis: theory NSCA

15:40:15 HOL-Nonstandard_Analysis: theory Hyperreal

15:40:15 HOL-Nonstandard_Analysis: theory CStar

15:40:15 HOL-Nonstandard_Analysis: theory CLim

15:40:16 HOL-Nonstandard_Analysis: theory Hypercomplex

15:40:16 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

15:40:28 Timing HOL-Nominal (2 threads, 13.067s elapsed time, 26.108s cpu time, 1.032s GC time, factor 2.00)

15:40:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal

15:40:28 Finished HOL-Nominal (0:00:29 elapsed time, 0:00:50 cpu time, factor 1.70)

15:40:28 Building Typeclass_Hierarchy_Basics ...

15:40:29 Typeclass_Hierarchy_Basics: theory Lattice_Syntax

15:40:29 Typeclass_Hierarchy_Basics: theory Multiset

15:40:35 Typeclass_Hierarchy_Basics: theory Setup

15:40:43 Timing HOL-Nonstandard_Analysis (2 threads, 19.609s elapsed time, 37.416s cpu time, 1.252s GC time, factor 1.91)

15:40:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

15:40:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

15:40:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

15:40:43 Finished HOL-Nonstandard_Analysis (0:00:40 elapsed time, 0:01:09 cpu time, factor 1.70)

15:40:43 Running HOL-Mirabelle-ex ...

15:40:44 HOL-Mirabelle-ex: theory Ex

15:40:52 Timing HOL-Mirabelle-ex (2 threads, 7.182s elapsed time, 0.044s cpu time, 0.000s GC time, factor 0.01)

15:40:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex

15:40:52 Finished HOL-Mirabelle-ex (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.31)

15:40:52 Running Classes ...

15:40:53 Classes: theory Setup

15:40:54 Classes: theory Classes

15:40:58 Timing Classes (2 threads, 3.018s elapsed time, 4.500s cpu time, 0.048s GC time, factor 1.49)

15:40:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes

15:40:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf

15:40:58 Finished Classes (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.19)

15:40:58 Running Codegen ...

15:40:59 Timing Typeclass_Hierarchy_Basics (2 threads, 13.939s elapsed time, 27.860s cpu time, 0.836s GC time, factor 2.00)

15:40:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

15:40:59 Finished Typeclass_Hierarchy_Basics (0:00:30 elapsed time, 0:00:53 cpu time, factor 1.73)

15:40:59 Running Corec ...

15:41:00 Codegen: theory Adaptation

15:41:00 Codegen: theory Evaluation

15:41:00 Corec: theory Setup

15:41:01 Codegen: theory Further

15:41:01 Codegen: theory Inductive_Predicate

15:41:02 Corec: theory BNF_Corec

15:41:02 Corec: theory FSet

15:41:02 Codegen: theory Introduction

15:41:03 Codegen: theory Refinement

15:41:04 Codegen: theory Foundations

15:41:09 Corec: theory Corec

15:41:11 Timing Codegen (2 threads, 7.050s elapsed time, 15.016s cpu time, 0.604s GC time, factor 2.13)

15:41:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

15:41:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

15:41:11 Finished Codegen (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.65)

15:41:11 Running Datatypes ...

15:41:12 Datatypes: theory Setup

15:41:13 Datatypes: theory BNF_Axiomatization

15:41:13 Datatypes: theory Cardinal_Notations

15:41:13 Datatypes: theory FSet

15:41:13 Datatypes: theory Nat_Bijection

15:41:14 Datatypes: theory Old_Datatype

15:41:15 Datatypes: theory Countable

15:41:17 Datatypes: theory Simps_Case_Conv

15:41:17 Datatypes: theory Datatypes

15:42:08 Timing Datatypes (2 threads, 52.388s elapsed time, 83.704s cpu time, 5.968s GC time, factor 1.60)

15:42:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

15:42:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

15:42:08 Finished Datatypes (0:00:57 elapsed time, 0:01:28 cpu time, factor 1.54)

15:42:08 Running Eisbach ...

15:42:10 Eisbach: theory Base

15:42:11 Eisbach: theory Manual

15:42:11 Eisbach: theory Preface

15:42:11 Timing Corec (2 threads, 67.254s elapsed time, 101.544s cpu time, 6.844s GC time, factor 1.51)

15:42:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec

15:42:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf

15:42:11 Finished Corec (0:01:11 elapsed time, 0:01:45 cpu time, factor 1.48)

15:42:11 Running Functions ...

15:42:12 Functions: theory Functions

15:42:15 Timing Eisbach (2 threads, 2.446s elapsed time, 4.080s cpu time, 0.036s GC time, factor 1.67)

15:42:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach

15:42:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf

15:42:15 Finished Eisbach (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.22)

15:42:15 Running HOL-Algebra ...

15:42:16 HOL-Algebra: theory FuncSet

15:42:16 HOL-Algebra: theory Multiset

15:42:17 Timing Functions (2 threads, 2.997s elapsed time, 5.380s cpu time, 0.144s GC time, factor 1.80)

15:42:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions

15:42:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

15:42:17 Finished Functions (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33)

15:42:17 Running HOL-Bali ...

15:42:19 HOL-Bali: theory Old_Recdef

15:42:20 HOL-Bali: theory Basis

15:42:21 HOL-Algebra: theory Factorial_Ring

15:42:21 HOL-Bali: theory Name

15:42:21 HOL-Bali: theory Table

15:42:21 HOL-Algebra: theory Permutation

15:42:24 HOL-Bali: theory Type

15:42:25 HOL-Bali: theory Value

15:42:26 HOL-Bali: theory Term

15:42:30 HOL-Algebra: theory Euclidean_Algorithm

15:42:39 HOL-Algebra: theory Primes

15:42:48 HOL-Bali: theory Decl

15:42:53 HOL-Bali: theory TypeRel

15:42:54 HOL-Algebra: theory Congruence

15:42:54 HOL-Algebra: theory Exponent

15:42:54 HOL-Bali: theory DeclConcepts

15:42:55 HOL-Algebra: theory Lattice

15:42:56 HOL-Bali: theory State

15:42:57 HOL-Bali: theory WellType

15:42:57 HOL-Algebra: theory Group

15:42:58 HOL-Bali: theory Conform

15:42:59 HOL-Algebra: theory Bij

15:42:59 HOL-Algebra: theory Coset

15:42:59 HOL-Bali: theory Eval

15:43:00 HOL-Algebra: theory FiniteProduct

15:43:01 HOL-Algebra: theory Ring

15:43:01 HOL-Bali: theory DefiniteAssignment

15:43:02 HOL-Algebra: theory Sylow

15:43:03 HOL-Algebra: theory Divisibility

15:43:05 HOL-Algebra: theory AbelCoset

15:43:06 HOL-Algebra: theory Module

15:43:08 HOL-Bali: theory WellForm

15:43:10 HOL-Bali: theory DefiniteAssignmentCorrect

15:43:10 HOL-Bali: theory Example

15:43:11 HOL-Bali: theory TypeSafe

15:43:11 HOL-Algebra: theory Ideal

15:43:14 HOL-Bali: theory Evaln

15:43:16 HOL-Algebra: theory RingHom

15:43:17 HOL-Bali: theory AxSem

15:43:18 HOL-Bali: theory Trans

15:43:18 HOL-Algebra: theory QuotRing

15:43:18 HOL-Algebra: theory UnivPoly

15:43:19 HOL-Algebra: theory IntRing

15:43:22 HOL-Bali: theory AxCompl

15:43:22 HOL-Bali: theory AxSound

15:43:23 HOL-Bali: theory AxExample

15:44:10 Timing HOL-Analysis (2 threads, 999.151s elapsed time, 1971.492s cpu time, 125.424s GC time, factor 1.97)

15:44:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

15:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

15:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf

15:44:10 Finished HOL-Analysis (0:18:53 elapsed time, 0:36:19 cpu time, factor 1.92)

15:44:11 Building HOL-Probability ...

15:44:12 Timing HOL-Algebra (2 threads, 111.510s elapsed time, 223.532s cpu time, 9.208s GC time, factor 2.00)

15:44:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

15:44:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

15:44:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

15:44:12 Finished HOL-Algebra (0:01:57 elapsed time, 0:03:51 cpu time, factor 1.97)

15:44:12 Running HOL-Analysis-ex ...

15:44:15 HOL-Probability: theory AList

15:44:15 HOL-Probability: theory FSet

15:44:16 HOL-Analysis-ex: theory Approximations

15:44:16 HOL-Probability: theory Permutation

15:44:17 HOL-Probability: theory Diagonal_Subsequence

15:44:19 HOL-Probability: theory Finite_Map

15:44:27 HOL-Probability: theory Adhoc_Overloading

15:44:27 HOL-Probability: theory Lattice_Syntax

15:44:27 HOL-Probability: theory Complete_Partial_Order2

15:44:27 HOL-Probability: theory Mapping

15:44:29 HOL-Probability: theory AList_Mapping

15:44:29 HOL-Probability: theory Monad_Syntax

15:44:29 HOL-Probability: theory Stream

15:44:31 HOL-Probability: theory Rewrite

15:44:31 HOL-Probability: theory Sublist

15:44:31 HOL-Probability: theory Multiset_Permutations

15:44:32 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

15:44:32 HOL-Probability: theory Fin_Map

15:44:34 HOL-Probability: theory Discrete_Topology

15:44:34 HOL-Probability: theory Probability_Measure

15:44:36 HOL-Probability: theory Distribution_Functions

15:44:36 HOL-Probability: theory Giry_Monad

15:44:37 HOL-Probability: theory Weak_Convergence

15:44:37 HOL-Probability: theory Helly_Selection

15:44:38 HOL-Probability: theory Probability_Mass_Function

15:44:39 HOL-Probability: theory Projective_Family

15:44:40 HOL-Probability: theory Infinite_Product_Measure

15:44:41 HOL-Probability: theory PMF_Impl

15:44:41 HOL-Probability: theory Random_Permutations

15:44:42 HOL-Probability: theory SPMF

15:44:43 HOL-Probability: theory Independent_Family

15:44:44 HOL-Probability: theory Convolution

15:44:45 HOL-Probability: theory Information

15:44:47 HOL-Probability: theory Projective_Limit

15:44:48 HOL-Probability: theory Distributions

15:44:49 HOL-Probability: theory Stream_Space

15:44:49 Warning: missing document directory

15:44:49 Timing HOL-Analysis-ex (2 threads, 32.490s elapsed time, 55.772s cpu time, 0.252s GC time, factor 1.72)

15:44:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

15:44:49 Finished HOL-Analysis-ex (0:00:36 elapsed time, 0:00:59 cpu time, factor 1.64)

15:44:49 Running HOL-Cardinals ...

15:44:50 HOL-Probability: theory Characteristic_Functions

15:44:50 HOL-Probability: theory Sinc_Integral

15:44:50 HOL-Cardinals: theory Order_Union

15:44:50 HOL-Cardinals: theory Cardinal_Notations

15:44:51 HOL-Cardinals: theory Fun_More

15:44:51 HOL-Cardinals: theory Order_Relation_More

15:44:51 HOL-Cardinals: theory Wellorder_Extension

15:44:51 HOL-Probability: theory Levy

15:44:51 HOL-Cardinals: theory Wellfounded_More

15:44:51 HOL-Cardinals: theory Wellorder_Relation

15:44:51 HOL-Cardinals: theory Wellorder_Embedding

15:44:52 HOL-Cardinals: theory Wellorder_Constructions

15:44:52 HOL-Probability: theory Central_Limit_Theorem

15:44:52 HOL-Probability: theory Probability

15:44:53 HOL-Cardinals: theory Cardinal_Order_Relation

15:44:53 HOL-Cardinals: theory Ordinal_Arithmetic

15:44:54 HOL-Cardinals: theory Cardinal_Arithmetic

15:44:54 HOL-Cardinals: theory Cardinals

15:44:55 HOL-Cardinals: theory Bounded_Set

15:45:20 Timing HOL-Bali (2 threads, 169.336s elapsed time, 333.276s cpu time, 16.132s GC time, factor 1.97)

15:45:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali

15:45:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf

15:45:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf

15:45:20 Finished HOL-Bali (0:03:02 elapsed time, 0:05:51 cpu time, factor 1.93)

15:45:20 Running HOL-Codegenerator_Test ...

15:45:24 HOL-Codegenerator_Test: theory Less_False

15:45:24 HOL-Codegenerator_Test: theory Cmp

15:45:24 HOL-Codegenerator_Test: theory Sorted_Less

15:45:25 HOL-Codegenerator_Test: theory AList_Upd_Del

15:45:25 HOL-Codegenerator_Test: theory List_Ins_Del

15:45:26 HOL-Codegenerator_Test: theory Map_by_Ordered

15:45:26 HOL-Codegenerator_Test: theory Set_by_Ordered

15:45:26 HOL-Codegenerator_Test: theory Primes

15:45:26 HOL-Codegenerator_Test: theory Records

15:45:27 HOL-Codegenerator_Test: theory Eratosthenes

15:45:27 HOL-Codegenerator_Test: theory Tree_Set

15:45:29 HOL-Codegenerator_Test: theory Tree_Map

15:45:31 HOL-Codegenerator_Test: theory Candidates

15:45:34 HOL-Codegenerator_Test: theory Generate

15:45:35 HOL-Codegenerator_Test: theory Generate_Binary_Nat

15:49:05 Timing HOL-Probability (2 threads, 229.048s elapsed time, 429.932s cpu time, 10.036s GC time, factor 1.88)

15:49:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

15:49:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

15:49:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

15:49:05 Finished HOL-Probability (0:04:53 elapsed time, 0:08:40 cpu time, factor 1.77)

15:49:06 Running HOL-Corec_Examples ...

15:49:07 HOL-Corec_Examples: theory BNF_Corec

15:49:07 HOL-Corec_Examples: theory FSet

15:49:12 HOL-Corec_Examples: theory Nat_Bijection

15:49:12 HOL-Corec_Examples: theory Stream

15:49:15 HOL-Corec_Examples: theory LFilter

15:49:15 HOL-Corec_Examples: theory Simple_Nesting

15:49:19 HOL-Corec_Examples: theory Stream_Processor

15:49:40 HOL-Corec_Examples: theory Paper_Examples

15:50:17 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures

15:50:21 HOL-Codegenerator_Test: theory Generate_Pretty_Char

15:50:52 HOL-Corec_Examples: theory Merge_A

15:50:52 HOL-Corec_Examples: theory GPV_Bare_Bones

15:50:57 HOL-Corec_Examples: theory Merge_B

15:51:00 HOL-Corec_Examples: theory Merge_C

15:51:04 HOL-Corec_Examples: theory Merge_Poly

15:51:06 HOL-Corec_Examples: theory Merge_D

15:51:14 HOL-Corec_Examples: theory Misc_Mono

15:51:54 HOL-Corec_Examples: theory Misc_Poly

15:52:49 Timing HOL-Cardinals (2 threads, 478.403s elapsed time, 473.088s cpu time, 8.056s GC time, factor 0.99)

15:52:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals

15:52:49 Finished HOL-Cardinals (0:08:00 elapsed time, 0:07:54 cpu time, factor 0.99)

15:52:49 Running HOL-Data_Structures ...

15:52:51 HOL-Data_Structures: theory Less_False

15:52:51 HOL-Data_Structures: theory Multiset

15:52:51 HOL-Data_Structures: theory Lattice_Algebras

15:53:01 HOL-Data_Structures: theory Log_Nat

15:53:02 HOL-Data_Structures: theory Float

15:53:20 HOL-Corec_Examples: theory Small_Concrete

15:53:25 HOL-Codegenerator_Test: theory Generate_Target_Nat

15:53:31 HOL-Data_Structures: theory Fib

15:53:31 HOL-Data_Structures: theory Cmp

15:53:32 HOL-Data_Structures: theory Sorted_Less

15:53:32 HOL-Data_Structures: theory Tree

15:53:32 HOL-Data_Structures: theory AList_Upd_Del

15:53:33 HOL-Data_Structures: theory Map_by_Ordered

15:53:33 HOL-Data_Structures: theory List_Ins_Del

15:53:33 HOL-Data_Structures: theory Set_by_Ordered

15:53:33 HOL-Data_Structures: theory Brother12_Set

15:53:35 HOL-Data_Structures: theory Balance

15:53:36 HOL-Data_Structures: theory Splay_Set

15:53:38 HOL-Data_Structures: theory Splay_Map

15:53:40 HOL-Data_Structures: theory Tree_Set

15:53:41 HOL-Data_Structures: theory Tree_Map

15:53:42 HOL-Data_Structures: theory Tree2

15:53:43 HOL-Data_Structures: theory Isin2

15:53:43 HOL-Data_Structures: theory AA_Set

15:53:45 HOL-Data_Structures: theory AVL_Set

15:53:46 HOL-Data_Structures: theory Leftist_Heap

15:53:48 HOL-Data_Structures: theory Lookup2

15:53:49 HOL-Data_Structures: theory AA_Map

15:53:50 HOL-Data_Structures: theory AVL_Map

15:53:50 HOL-Data_Structures: theory RBT

15:53:54 HOL-Corec_Examples: theory Stream_Friends

15:54:01 HOL-Data_Structures: theory RBT_Set

15:54:03 HOL-Corec_Examples: theory TLList_Friends

15:54:04 HOL-Data_Structures: theory RBT_Map

15:54:08 HOL-Data_Structures: theory Tree23

15:54:10 HOL-Data_Structures: theory Tree23_Set

15:54:18 HOL-Data_Structures: theory Tree23_Map

15:54:23 HOL-Data_Structures: theory Tree234

15:54:27 HOL-Corec_Examples: theory Type_Class

15:54:28 HOL-Data_Structures: theory Tree234_Set

15:55:06 Timing HOL-Corec_Examples (2 threads, 357.271s elapsed time, 576.368s cpu time, 57.720s GC time, factor 1.61)

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

15:55:06 Finished HOL-Corec_Examples (0:05:59 elapsed time, 0:09:38 cpu time, factor 1.61)

15:55:06 Running HOL-Datatype_Examples ...

15:55:06 HOL-Data_Structures: theory Tree234_Map

15:55:07 HOL-Datatype_Examples: theory BNF_Axiomatization

15:55:07 HOL-Datatype_Examples: theory FSet

15:55:07 HOL-Datatype_Examples: theory Infinite_Set

15:55:08 HOL-Datatype_Examples: theory Lift_BNF

15:55:12 HOL-Datatype_Examples: theory Milner_Tofte

15:55:12 HOL-Datatype_Examples: theory Lambda_Term

15:55:13 HOL-Datatype_Examples: theory Misc_Codatatype

15:55:14 HOL-Datatype_Examples: theory Prelim

15:55:15 HOL-Datatype_Examples: theory DTree

15:55:15 HOL-Datatype_Examples: theory Parallel

15:55:16 HOL-Datatype_Examples: theory TreeFsetI

15:55:16 HOL-Datatype_Examples: theory Gram_Lang

15:55:18 HOL-Datatype_Examples: theory Nat_Bijection

15:55:19 HOL-Datatype_Examples: theory Stream

15:55:20 HOL-Datatype_Examples: theory Process

15:55:26 HOL-Datatype_Examples: theory Stream_Processor

15:55:28 HOL-Data_Structures: theory Brother12_Map

15:55:31 HOL-Datatype_Examples: theory Old_Datatype

15:55:33 HOL-Datatype_Examples: theory Compat

15:56:26 HOL-Datatype_Examples: theory Countable

15:56:29 HOL-Datatype_Examples: theory Misc_Datatype

15:56:58 HOL-Datatype_Examples: theory Misc_Primcorec

15:57:01 HOL-Datatype_Examples: theory TreeFI

15:57:01 HOL-Datatype_Examples: theory Koenig

15:58:00 HOL-Codegenerator_Test: theory Code_Test_GHC

15:58:03 HOL-Codegenerator_Test: theory Code_Test_MLton

15:58:07 HOL-Codegenerator_Test: theory Code_Test_OCaml

15:58:08 HOL-Codegenerator_Test: theory Code_Test_PolyML

15:58:09 HOL-Codegenerator_Test: theory Code_Test_Scala

15:58:30 HOL-Datatype_Examples: theory Misc_Primrec

15:58:39 HOL-Codegenerator_Test: theory Code_Test_SMLNJ

15:58:40 Timing HOL-Codegenerator_Test (2 threads, 795.273s elapsed time, 652.480s cpu time, 19.084s GC time, factor 0.82)

15:58:40 Finished HOL-Codegenerator_Test (0:13:19 elapsed time, 0:36:00 cpu time, factor 2.70)

15:58:40 Running HOL-Decision_Procs ...

15:58:42 HOL-Decision_Procs: theory Code_Abstract_Nat

15:58:42 HOL-Decision_Procs: theory Commutative_Ring

15:58:42 HOL-Decision_Procs: theory Code_Target_Nat

15:58:43 HOL-Decision_Procs: theory DP_Library

15:58:43 HOL-Decision_Procs: theory Dense_Linear_Order

15:58:46 HOL-Decision_Procs: theory Dense_Linear_Order_Ex

15:58:46 HOL-Decision_Procs: theory Code_Target_Int

15:58:46 HOL-Decision_Procs: theory Code_Target_Numeral

15:58:47 HOL-Decision_Procs: theory Old_Recdef

15:58:48 HOL-Decision_Procs: theory Cooper

15:58:48 HOL-Decision_Procs: theory Commutative_Ring_Complete

15:58:49 HOL-Decision_Procs: theory Commutative_Ring_Ex

15:58:49 HOL-Decision_Procs: theory Ferrack

15:59:06 Timing HOL-Datatype_Examples (2 threads, 238.671s elapsed time, 366.856s cpu time, 43.628s GC time, factor 1.54)

15:59:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

15:59:06 Finished HOL-Datatype_Examples (0:04:00 elapsed time, 0:06:25 cpu time, factor 1.60)

15:59:06 Running HOL-Hahn_Banach ...

15:59:08 HOL-Hahn_Banach: theory Infinite_Set

15:59:08 HOL-Hahn_Banach: theory Nat_Bijection

15:59:09 HOL-Hahn_Banach: theory Old_Datatype

15:59:09 HOL-Hahn_Banach: theory Set_Algebras

15:59:09 HOL-Decision_Procs: theory Lattice_Algebras

15:59:10 HOL-Hahn_Banach: theory Zorn_Lemma

15:59:10 HOL-Hahn_Banach: theory Countable

15:59:12 HOL-Hahn_Banach: theory Countable_Set

15:59:13 HOL-Hahn_Banach: theory Continuum_Not_Denumerable

15:59:13 HOL-Hahn_Banach: theory Bounds

15:59:13 HOL-Hahn_Banach: theory Vector_Space

15:59:14 HOL-Hahn_Banach: theory Linearform

15:59:14 HOL-Hahn_Banach: theory Subspace

15:59:15 HOL-Hahn_Banach: theory Function_Order

15:59:15 HOL-Hahn_Banach: theory Normed_Space

15:59:15 HOL-Hahn_Banach: theory Function_Norm

15:59:15 HOL-Decision_Procs: theory Log_Nat

15:59:15 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas

15:59:15 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas

15:59:15 HOL-Decision_Procs: theory Float

15:59:16 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas

15:59:16 HOL-Hahn_Banach: theory Hahn_Banach

15:59:16 HOL-Decision_Procs: theory MIR

15:59:18 HOL-Decision_Procs: theory Approximation

15:59:33 Timing HOL-Hahn_Banach (2 threads, 22.439s elapsed time, 44.112s cpu time, 0.920s GC time, factor 1.97)

15:59:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

15:59:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

15:59:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

15:59:33 Finished HOL-Hahn_Banach (0:00:26 elapsed time, 0:00:48 cpu time, factor 1.86)

15:59:33 Running HOL-Hoare ...

15:59:34 HOL-Hoare: theory Arith2

15:59:34 HOL-Hoare: theory Heap

15:59:35 HOL-Hoare: theory Hoare_Logic

15:59:36 HOL-Hoare: theory Hoare_Logic_Abort

15:59:37 HOL-Hoare: theory Examples

15:59:37 HOL-Hoare: theory HeapSyntax

15:59:37 HOL-Hoare: theory Pointer_Examples

15:59:38 HOL-Hoare: theory SchorrWaite

15:59:39 HOL-Hoare: theory Pointers0

15:59:40 HOL-Hoare: theory ExamplesAbort

15:59:40 HOL-Hoare: theory HeapSyntaxAbort

15:59:40 HOL-Hoare: theory Pointer_ExamplesAbort

15:59:40 HOL-Hoare: theory SepLogHeap

15:59:40 HOL-Hoare: theory Separation

15:59:41 HOL-Hoare: theory Hoare

16:00:04 HOL-Decision_Procs: theory Polynomial_List

16:00:04 Timing HOL-Hoare (2 threads, 27.285s elapsed time, 54.412s cpu time, 1.444s GC time, factor 1.99)

16:00:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare

16:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf

16:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf

16:00:04 Finished HOL-Hoare (0:00:31 elapsed time, 0:00:59 cpu time, factor 1.91)

16:00:05 Running HOL-Hoare_Parallel ...

16:00:06 HOL-Hoare_Parallel: theory Graph

16:00:06 HOL-Hoare_Parallel: theory OG_Com

16:00:07 HOL-Hoare_Parallel: theory Quote_Antiquote

16:00:07 HOL-Hoare_Parallel: theory RG_Com

16:00:09 HOL-Hoare_Parallel: theory RG_Tran

16:00:10 HOL-Hoare_Parallel: theory OG_Tran

16:00:11 HOL-Hoare_Parallel: theory RG_Hoare

16:00:12 HOL-Hoare_Parallel: theory OG_Hoare