00:34:17 Started by upstream project "isabelle-repo" build number 774

00:34:17 originally caused by:

00:34:17 Started by an SCM change

00:34:17 [EnvInject] - Loading node environment variables.

00:34:17 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

00:34:17 [isabelle-repo-makeall] $ hg showconfig paths.default

00:34:17 [isabelle-repo-makeall] $ hg pull --rev 002b4c8c366ebbb75db83b7890560c7a77c263b3

00:34:18 pulling from http://isabelle.in.tum.de/repos/isabelle/

00:34:18 searching for changes

00:34:18 adding changesets

00:34:18 adding manifests

00:34:18 adding file changes

00:34:18 added 6 changesets with 9 changes to 7 files

00:34:18 (run 'hg update' to get a working copy)

00:34:18 [isabelle-repo-makeall] $ hg update --clean --rev 002b4c8c366ebbb75db83b7890560c7a77c263b3

00:34:18 7 files updated, 0 files merged, 0 files removed, 0 files unresolved

00:34:18 [isabelle-repo-makeall] $ hg log --rev . --template {node}

00:34:18 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

00:34:18 [isabelle-repo-makeall] $ hg id --branch

00:34:18 No emails were triggered.

00:34:18 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson6929690366703596402.sh

00:34:18 + Admin/jenkins/run_build makeall

00:34:18 + set -e

00:34:18 + PROFILE=makeall

00:34:18 + shift

00:34:18 + bin/isabelle components -a

00:34:19 + bin/isabelle jedit -bf

00:34:19 ### Building Isabelle/Scala ...

00:36:39 ### Building Isabelle/jEdit ...

00:37:04 + bin/isabelle ci_build_makeall

00:37:08

00:37:08 === CONFIGURATION ===

00:37:08

00:37:08 ISABELLE_BUILD_OPTIONS=""

00:37:08

00:37:08 ML_PLATFORM="x86_64-linux"

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

00:37:08 ML_SYSTEM="polyml-5.6"

00:37:08 ML_OPTIONS="-H 4000 --maxheap 8G"

00:37:09

00:37:09 === BUILD ===

00:37:09

00:37:09 Build started at Sun, 26 Feb 2017 23:37:08 GMT

00:37:09 Isabelle id 002b4c8c366e

00:37:09

00:37:09 === LOG ===

00:37:09

00:37:09 Session Pure/Pure

00:37:09 Session CCL/CCL

00:37:10 Session CTT/CTT

00:37:10 Session Cube/Cube

00:37:10 Session FOL/FOL

00:37:10 Session FOL/FOL-ex

00:37:10 Session FOLP/FOLP

00:37:10 Session FOLP/FOLP-ex

00:37:10 Session HOL/HOL (main)

00:37:10 Session Doc/Classes (doc)

00:37:10 Session Doc/Codegen_Basics

00:37:10 Session Doc/Codegen (doc)

00:37:10 Session Doc/Corec (doc)

00:37:10 Session Doc/Datatypes (doc)

00:37:10 Session Doc/Functions (doc)

00:37:10 Session HOL/HOL-Algebra (main timing)

00:37:11 Session HOL/HOL-Analysis (main timing)

00:37:11 Session HOL/HOL-Analysis-ex

00:37:11 Session HOL/HOL-Probability (timing)

00:37:11 Session HOL/HOL-Probability-ex (timing)

00:37:11 Session HOL/HOL-Auth (timing)

00:37:11 Session HOL/HOL-UNITY (timing)

00:37:11 Session HOL/HOL-Bali (timing)

00:37:11 Session HOL/HOL-Cardinals (timing)

00:37:11 Session HOL/HOL-Corec_Examples (timing)

00:37:11 Session HOL/HOL-Data_Structures (timing)

00:37:12 Session HOL/HOL-Datatype_Examples (timing)

00:37:12 Session HOL/HOL-Decision_Procs (timing)

00:37:12 Session HOL/HOL-Eisbach

00:37:12 Session Doc/Eisbach (doc)

00:37:12 Session HOL/HOL-Hahn_Banach

00:37:12 Session HOL/HOL-Hoare

00:37:12 Session HOL/HOL-Hoare_Parallel (timing)

00:37:12 Session HOL/HOL-IMP (timing)

00:37:12 Session HOL/HOL-IMPP

00:37:12 Session HOL/HOL-IOA

00:37:12 Session HOL/HOL-Imperative_HOL

00:37:12 Session HOL/HOL-Import

00:37:12 Session HOL/HOL-Induct

00:37:12 Session HOL/HOL-Isar_Examples

00:37:13 Session HOL/HOL-Lattice

00:37:13 Session HOL/HOL-Library (main timing)

00:37:13 Session HOL/HOL-Codegenerator_Test

00:37:13 Session HOL/HOL-Matrix_LP

00:37:13 Session HOL/HOL-Metis_Examples (timing)

00:37:13 Session HOL/HOL-MicroJava (timing)

00:37:13 Session HOL/HOL-Mirabelle

00:37:13 Session HOL/HOL-Mirabelle-ex

00:37:13 Session HOL/HOL-Mutabelle

00:37:13 Session HOL/HOL-NanoJava

00:37:13 Session HOL/HOL-Nitpick_Examples

00:37:13 Session HOL/HOL-Nominal

00:37:13 Session HOL/HOL-Nominal-Examples (timing)

00:37:14 Session HOL/HOL-Nonstandard_Analysis (timing)

00:37:14 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

00:37:14 Session HOL/HOL-Number_Theory (timing)

00:37:14 Session HOL/HOL-Nunchaku

00:37:14 Session HOL/HOL-Predicate_Compile_Examples (timing)

00:37:14 Session HOL/HOL-Prolog

00:37:14 Session HOL/HOL-Quickcheck_Examples (timing)

00:37:14 Session HOL/HOL-Quotient_Examples (timing)

00:37:14 Session HOL/HOL-SET_Protocol (timing)

00:37:14 Session HOL/HOL-Statespace

00:37:14 Session HOL/HOL-TLA

00:37:14 Session HOL/HOL-TLA-Buffer

00:37:14 Session HOL/HOL-TLA-Inc

00:37:14 Session HOL/HOL-TLA-Memory

00:37:14 Session HOL/HOL-TPTP

00:37:14 Session HOL/HOL-Types_To_Sets

00:37:14 Session HOL/HOL-Unix

00:37:14 Session HOL/HOL-Word (main timing)

00:37:15 Session HOL/HOL-SPARK (main)

00:37:15 Session HOL/HOL-SPARK-Examples

00:37:15 Session HOL/HOL-SPARK-Manual

00:37:15 Session HOL/HOL-Word-Examples

00:37:15 Session HOL/HOL-Word-SMT_Examples (timing)

00:37:15 Session HOL/HOL-ZF

00:37:15 Session HOL/HOL-ex

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

00:37:15 Session HOL/HOLCF-FOCUS

00:37:15 Session HOL/HOLCF-IMP

00:37:15 Session HOL/HOLCF-Library

00:37:15 Session HOL/HOLCF-Tutorial

00:37:15 Session HOL/HOLCF-ex

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

00:37:15 Session HOL/IOA-ABP

00:37:15 Session HOL/IOA-NTP

00:37:15 Session HOL/IOA-Storage

00:37:15 Session HOL/IOA-ex

00:37:15 Session Doc/How_to_Prove_it

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

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

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

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

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

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

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

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

00:37:16 Session Doc/Typeclass_Hierarchy_Basics

00:37:16 Session Doc/Typeclass_Hierarchy (doc)

00:37:16 Session HOL/HOL-Proofs (timing)

00:37:16 Session HOL/HOL-Proofs-Extraction (timing)

00:37:16 Session HOL/HOL-Proofs-Lambda (timing)

00:37:16 Session HOL/HOL-Proofs-ex

00:37:16 Session Doc/Intro (doc)

00:37:16 Session LCF/LCF

00:37:16 Session Doc/Logics (doc)

00:37:16 Session Doc/Nitpick (doc)

00:37:16 Session Unsorted/SML

00:37:16 Session Sequents/Sequents

00:37:16 Session Doc/Sledgehammer (doc)

00:37:16 Session Unsorted/Spec_Check

00:37:16 Session Doc/System (doc)

00:37:16 Session ZF/ZF (main timing ZF)

00:37:16 Session Doc/Logics_ZF (doc)

00:37:16 Session ZF/ZF-AC (ZF)

00:37:17 Session ZF/ZF-Coind (ZF)

00:37:17 Session ZF/ZF-Constructible (ZF)

00:37:17 Session ZF/ZF-IMP (ZF)

00:37:17 Session ZF/ZF-Induct (ZF)

00:37:17 Session ZF/ZF-Resid (ZF)

00:37:17 Session ZF/ZF-UNITY (timing ZF)

00:37:17 Session ZF/ZF-ex (ZF)

00:37:18 Cleaning Pure ...

00:37:18 Cleaning SML ...

00:37:18 Cleaning Sequents ...

00:37:18 Cleaning Sledgehammer ...

00:37:18 Cleaning Spec_Check ...

00:37:18 Cleaning System ...

00:37:18 Cleaning ZF ...

00:37:18 Cleaning ZF-AC ...

00:37:18 Cleaning ZF-Coind ...

00:37:18 Cleaning ZF-Constructible ...

00:37:18 Cleaning ZF-IMP ...

00:37:18 Cleaning ZF-Induct ...

00:37:18 Cleaning ZF-Resid ...

00:37:18 Cleaning ZF-UNITY ...

00:37:18 Cleaning ZF-ex ...

00:37:18 Cleaning Nitpick ...

00:37:18 Cleaning Logics_ZF ...

00:37:18 Cleaning Logics ...

00:37:18 Cleaning LCF ...

00:37:18 Cleaning Intro ...

00:37:18 Cleaning HOL-Proofs ...

00:37:18 Cleaning HOL-Proofs-Extraction ...

00:37:18 Cleaning HOL-Proofs-Lambda ...

00:37:18 Cleaning HOL-Proofs-ex ...

00:37:18 Cleaning HOL ...

00:37:18 Cleaning HOL-Algebra ...

00:37:18 Cleaning HOL-Analysis ...

00:37:18 Cleaning HOL-Analysis-ex ...

00:37:18 Cleaning HOL-Probability ...

00:37:18 Cleaning HOL-Probability-ex ...

00:37:18 Cleaning HOL-Auth ...

00:37:18 Cleaning HOL-UNITY ...

00:37:18 Cleaning HOL-Bali ...

00:37:18 Cleaning HOL-Cardinals ...

00:37:18 Cleaning HOL-Corec_Examples ...

00:37:18 Cleaning HOL-Data_Structures ...

00:37:18 Cleaning HOL-Datatype_Examples ...

00:37:18 Cleaning HOL-Decision_Procs ...

00:37:18 Cleaning HOL-Eisbach ...

00:37:18 Cleaning HOL-Hahn_Banach ...

00:37:18 Cleaning HOL-Hoare ...

00:37:18 Cleaning HOL-Hoare_Parallel ...

00:37:18 Cleaning HOL-IMP ...

00:37:18 Cleaning HOL-IMPP ...

00:37:18 Cleaning HOL-IOA ...

00:37:18 Cleaning HOL-Imperative_HOL ...

00:37:18 Cleaning HOL-Import ...

00:37:18 Cleaning HOL-Induct ...

00:37:18 Cleaning HOL-Isar_Examples ...

00:37:18 Cleaning HOL-Lattice ...

00:37:18 Cleaning HOL-Library ...

00:37:18 Cleaning HOL-Codegenerator_Test ...

00:37:18 Cleaning HOL-Matrix_LP ...

00:37:18 Cleaning HOL-Metis_Examples ...

00:37:18 Cleaning HOL-MicroJava ...

00:37:18 Cleaning HOL-Mirabelle ...

00:37:18 Cleaning HOL-Mirabelle-ex ...

00:37:18 Cleaning HOL-Mutabelle ...

00:37:18 Cleaning HOL-NanoJava ...

00:37:18 Cleaning HOL-Nitpick_Examples ...

00:37:18 Cleaning HOL-Nominal ...

00:37:18 Cleaning HOL-Nominal-Examples ...

00:37:18 Cleaning HOL-Nonstandard_Analysis ...

00:37:18 Cleaning HOL-Nonstandard_Analysis-Examples ...

00:37:18 Cleaning HOL-Number_Theory ...

00:37:18 Cleaning HOL-Nunchaku ...

00:37:18 Cleaning HOL-Predicate_Compile_Examples ...

00:37:18 Cleaning HOL-Prolog ...

00:37:18 Cleaning HOL-Quickcheck_Examples ...

00:37:18 Cleaning HOL-Quotient_Examples ...

00:37:18 Cleaning HOL-SET_Protocol ...

00:37:18 Cleaning HOL-Statespace ...

00:37:18 Cleaning HOL-TLA ...

00:37:18 Cleaning HOL-TLA-Buffer ...

00:37:18 Cleaning HOL-TLA-Inc ...

00:37:18 Cleaning HOL-TLA-Memory ...

00:37:18 Cleaning HOL-TPTP ...

00:37:18 Cleaning HOL-Types_To_Sets ...

00:37:18 Cleaning HOL-Unix ...

00:37:18 Cleaning HOL-Word ...

00:37:18 Cleaning HOL-SPARK ...

00:37:18 Cleaning HOL-SPARK-Examples ...

00:37:18 Cleaning HOL-SPARK-Manual ...

00:37:18 Cleaning HOL-Word-Examples ...

00:37:18 Cleaning HOL-Word-SMT_Examples ...

00:37:18 Cleaning HOL-ZF ...

00:37:18 Cleaning HOL-ex ...

00:37:18 Cleaning HOLCF ...

00:37:18 Cleaning HOLCF-FOCUS ...

00:37:18 Cleaning HOLCF-IMP ...

00:37:18 Cleaning HOLCF-Library ...

00:37:18 Cleaning HOLCF-Tutorial ...

00:37:18 Cleaning HOLCF-ex ...

00:37:18 Cleaning IOA ...

00:37:18 Cleaning IOA-ABP ...

00:37:18 Cleaning IOA-NTP ...

00:37:18 Cleaning IOA-Storage ...

00:37:18 Cleaning IOA-ex ...

00:37:18 Cleaning How_to_Prove_it ...

00:37:18 Cleaning Implementation ...

00:37:18 Cleaning Isar_Ref ...

00:37:18 Cleaning JEdit ...

00:37:18 Cleaning Locales ...

00:37:18 Cleaning Main ...

00:37:18 Cleaning Prog_Prove ...

00:37:18 Cleaning Sugar ...

00:37:18 Cleaning Tutorial ...

00:37:18 Cleaning Typeclass_Hierarchy_Basics ...

00:37:18 Cleaning Typeclass_Hierarchy ...

00:37:18 Cleaning Functions ...

00:37:18 Cleaning FOLP ...

00:37:18 Cleaning FOLP-ex ...

00:37:18 Cleaning FOL ...

00:37:18 Cleaning FOL-ex ...

00:37:18 Cleaning Eisbach ...

00:37:18 Cleaning Datatypes ...

00:37:18 Cleaning Cube ...

00:37:18 Cleaning Corec ...

00:37:18 Cleaning Codegen_Basics ...

00:37:18 Cleaning Codegen ...

00:37:18 Cleaning Classes ...

00:37:18 Cleaning CTT ...

00:37:18 Cleaning CCL ...

00:37:18 Building Pure ...

00:37:30 Pure: theory Pure

00:37:30 Pure: theory ML_Bootstrap

00:37:33 Warning: missing document directory

00:37:33 Timing Pure (1 threads, 0.539s elapsed time, 0.540s cpu time, 0.000s GC time, factor 1.00)

00:37:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

00:37:33 Finished Pure (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)

00:37:34 Building HOL ...

00:37:34 Building ZF ...

00:37:34 Building HOL-Proofs ...

00:37:34 HOL-Proofs: theory Proofs

00:37:34 ZF: theory IFOL

00:37:35 HOL-Proofs: theory Code_Generator

00:37:35 HOL: theory Code_Generator

00:37:35 ZF: theory FOL

00:37:36 ZF: theory ZF

00:37:37 ZF: theory upair

00:37:37 ZF: theory pair

00:37:37 ZF: theory Bool

00:37:37 ZF: theory equalities

00:37:37 HOL-Proofs: theory HOL

00:37:37 HOL: theory HOL

00:37:38 ZF: theory Fixedpt

00:37:38 ZF: theory Sum

00:37:38 ZF: theory func

00:37:38 ZF: theory Perm

00:37:38 ZF: theory QPair

00:37:38 ZF: theory Trancl

00:37:39 ZF: theory EquivClass

00:37:39 ZF: theory WF

00:37:39 ZF: theory Order

00:37:39 ZF: theory Ordinal

00:37:39 ZF: theory OrdQuant

00:37:39 ZF: theory OrderArith

00:37:40 ZF: theory Nat_ZF

00:37:40 ZF: theory Epsilon

00:37:40 ZF: theory OrderType

00:37:40 ZF: theory Inductive_ZF

00:37:40 ZF: theory Finite

00:37:40 ZF: theory Cardinal

00:37:41 ZF: theory Univ

00:37:41 HOL: theory Argo

00:37:41 HOL: theory Ctr_Sugar

00:37:41 HOL-Proofs: theory Argo

00:37:41 HOL-Proofs: theory Ctr_Sugar

00:37:41 ZF: theory Arith

00:37:41 ZF: theory QUniv

00:37:41 ZF: theory Datatype_ZF

00:37:42 ZF: theory ArithSimp

00:37:42 HOL: theory Orderings

00:37:42 ZF: theory Int_ZF

00:37:42 ZF: theory CardinalArith

00:37:42 HOL-Proofs: theory Orderings

00:37:42 ZF: theory List_ZF

00:37:42 ZF: theory Bin

00:37:43 HOL: theory SAT

00:37:43 HOL-Proofs: theory SAT

00:37:43 ZF: theory IntDiv_ZF

00:37:44 HOL: theory Groups

00:37:44 ZF: theory Main_ZF

00:37:44 ZF: theory AC

00:37:44 ZF: theory Zorn

00:37:44 ZF: theory Cardinal_AC

00:37:44 ZF: theory Main

00:37:44 ZF: theory InfDatatype

00:37:44 ZF: theory Main_ZFC

00:37:45 HOL-Proofs: theory Groups

00:37:46 HOL: theory Lattices

00:37:48 HOL: theory Set

00:37:49 HOL-Proofs: theory Lattices

00:37:50 HOL: theory Fun

00:37:50 HOL: theory Typedef

00:37:50 HOL: theory Rings

00:37:50 HOL: theory Complete_Lattices

00:37:52 HOL-Proofs: theory Set

00:37:53 HOL: theory Inductive

00:37:55 HOL: theory Product_Type

00:37:56 HOL: theory Complete_Partial_Order

00:37:56 HOL: theory Sum_Type

00:37:56 HOL-Proofs: theory Fun

00:37:57 HOL-Proofs: theory Typedef

00:37:58 HOL-Proofs: theory Rings

00:37:59 HOL-Proofs: theory Complete_Lattices

00:38:00 HOL: theory Nat

00:38:02 HOL: theory Fields

00:38:02 HOL: theory Meson

00:38:03 HOL: theory ATP

00:38:03 HOL-Proofs: theory Inductive

00:38:05 HOL: theory Metis

00:38:05 HOL-Proofs: theory Product_Type

00:38:07 HOL: theory Finite_Set

00:38:07 HOL-Proofs: theory Complete_Partial_Order

00:38:08 HOL: theory Relation

00:38:08 HOL-Proofs: theory Sum_Type

00:38:09 HOL: theory Transitive_Closure

00:38:10 Timing ZF (2 threads, 23.163s elapsed time, 38.508s cpu time, 5.004s GC time, factor 1.66)

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

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

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

00:38:10 Finished ZF (0:00:35 elapsed time, 0:00:59 cpu time, factor 1.66)

00:38:10 HOL: theory Wellfounded

00:38:10 Building FOL ...

00:38:10 FOL: theory IFOL

00:38:11 HOL: theory Fun_Def_Base

00:38:11 HOL: theory Hilbert_Choice

00:38:11 HOL: theory Wfrec

00:38:11 HOL: theory Order_Relation

00:38:11 FOL: theory FOL

00:38:11 HOL: theory BNF_Wellorder_Relation

00:38:11 HOL: theory Zorn

00:38:12 HOL: theory BNF_Wellorder_Embedding

00:38:12 HOL-Proofs: theory Nat

00:38:12 HOL: theory BNF_Wellorder_Constructions

00:38:13 HOL: theory BNF_Cardinal_Order_Relation

00:38:13 HOL: theory BNF_Cardinal_Arithmetic

00:38:14 HOL: theory BNF_Def

00:38:15 HOL: theory BNF_Composition

00:38:16 HOL: theory Basic_BNFs

00:38:16 HOL-Proofs: theory Fields

00:38:16 Timing FOL (2 threads, 2.552s elapsed time, 2.828s cpu time, 0.156s GC time, factor 1.11)

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

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

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

00:38:16 Finished FOL (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.25)

00:38:16 Building FOLP ...

00:38:16 FOLP: theory IFOLP

00:38:16 HOL: theory BNF_Fixpoint_Base

00:38:17 FOLP: theory FOLP

00:38:17 HOL-Proofs: theory Meson

00:38:17 HOL-Proofs: theory ATP

00:38:18 Timing FOLP (2 threads, 1.024s elapsed time, 0.896s cpu time, 0.000s GC time, factor 0.87)

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

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

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

00:38:18 ZF-UNITY: theory FoldSet

00:38:18 ZF-UNITY: theory Acc

00:38:18 ZF-UNITY: theory GenPrefix

00:38:18 ZF-UNITY: theory Multiset

00:38:19 ZF-UNITY: theory State

00:38:19 ZF-UNITY: theory UNITY

00:38:19 HOL: theory BNF_Least_Fixpoint

00:38:19 ZF-UNITY: theory Constrains

00:38:19 ZF-UNITY: theory MultisetSum

00:38:19 HOL-Proofs: theory Metis

00:38:19 ZF-UNITY: theory Monotonicity

00:38:19 ZF-UNITY: theory FP

00:38:20 ZF-UNITY: theory WFair

00:38:20 ZF-UNITY: theory Increasing

00:38:20 ZF-UNITY: theory SubstAx

00:38:20 ZF-UNITY: theory Follows

00:38:20 ZF-UNITY: theory Mutex

00:38:20 ZF-UNITY: theory Union

00:38:21 HOL: theory Basic_BNF_LFPs

00:38:21 ZF-UNITY: theory Comp

00:38:21 HOL: theory Transfer

00:38:21 ZF-UNITY: theory Guar

00:38:22 ZF-UNITY: theory AllocBase

00:38:22 ZF-UNITY: theory ClientImpl

00:38:22 ZF-UNITY: theory Distributor

00:38:22 ZF-UNITY: theory Merge

00:38:22 HOL: theory Num

00:38:22 ZF-UNITY: theory AllocImpl

00:38:23 HOL-Proofs: theory Finite_Set

00:38:25 HOL: theory Power

00:38:27 HOL: theory Groups_Big

00:38:29 HOL: theory Equiv_Relations

00:38:30 HOL: theory Lifting

00:38:30 HOL-Proofs: theory Relation

00:38:31 HOL: theory Lifting_Set

00:38:31 HOL: theory Option

00:38:31 HOL: theory Quotient

00:38:32 HOL: theory Extraction

00:38:33 HOL: theory Lattices_Big

00:38:33 HOL-Proofs: theory Transitive_Closure

00:38:34 HOL: theory Partial_Function

00:38:35 HOL: theory Fun_Def

00:38:36 HOL: theory Int

00:38:37 HOL-Proofs: theory Wellfounded

00:38:37 Timing ZF-UNITY (2 threads, 18.663s elapsed time, 33.772s cpu time, 1.212s GC time, factor 1.81)

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

00:38:37 Finished ZF-UNITY (0:00:19 elapsed time, 0:00:34 cpu time, factor 1.79)

00:38:37 Running ZF-Constructible ...

00:38:38 ZF-Constructible: theory Formula

00:38:38 ZF-Constructible: theory MetaExists

00:38:38 ZF-Constructible: theory Normal

00:38:38 ZF-Constructible: theory Reflection

00:38:38 ZF-Constructible: theory Relative

00:38:38 HOL: theory Nat_Transfer

00:38:39 HOL: theory Euclidean_Division

00:38:39 HOL-Proofs: theory Fun_Def_Base

00:38:40 HOL-Proofs: theory Hilbert_Choice

00:38:40 ZF-Constructible: theory L_axioms

00:38:40 ZF-Constructible: theory Wellorderings

00:38:41 ZF-Constructible: theory WFrec

00:38:41 ZF-Constructible: theory WF_absolute

00:38:42 HOL-Proofs: theory Wfrec

00:38:42 ZF-Constructible: theory Datatype_absolute

00:38:42 ZF-Constructible: theory Rank

00:38:42 HOL-Proofs: theory Order_Relation

00:38:43 HOL: theory Parity

00:38:43 ZF-Constructible: theory Separation

00:38:43 ZF-Constructible: theory Internalize

00:38:43 ZF-Constructible: theory AC_in_L

00:38:43 HOL-Proofs: theory BNF_Wellorder_Relation

00:38:43 HOL-Proofs: theory Zorn

00:38:44 HOL-Proofs: theory BNF_Wellorder_Embedding

00:38:45 ZF-Constructible: theory Rec_Separation

00:38:45 HOL: theory Divides

00:38:45 ZF-Constructible: theory Rank_Separation

00:38:45 ZF-Constructible: theory Satisfies_absolute

00:38:46 ZF-Constructible: theory DPow_absolute

00:38:46 HOL-Proofs: theory BNF_Wellorder_Constructions

00:38:52 HOL-Proofs: theory BNF_Cardinal_Order_Relation

00:38:52 HOL: theory Code_Numeral

00:38:52 HOL: theory Numeral_Simprocs

00:38:53 HOL: theory SMT

00:38:53 HOL: theory Semiring_Normalization

00:38:55 HOL: theory Set_Interval

00:38:55 HOL: theory Groebner_Basis

00:38:57 HOL-Proofs: theory BNF_Cardinal_Arithmetic

00:38:57 HOL: theory Conditionally_Complete_Lattices

00:38:57 HOL: theory Filter

00:38:58 Timing ZF-Constructible (2 threads, 15.753s elapsed time, 29.596s cpu time, 5.408s GC time, factor 1.88)

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

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

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

00:38:58 Finished ZF-Constructible (0:00:20 elapsed time, 0:00:36 cpu time, factor 1.83)

00:38:58 Running ZF-ex ...

00:38:58 ZF-ex: theory BinEx

00:38:58 ZF-ex: theory CoUnit

00:38:58 ZF-ex: theory Commutation

00:38:58 ZF-ex: theory Group

00:38:58 ZF-ex: theory LList

00:38:58 ZF-ex: theory Limit

00:38:58 HOL: theory Presburger

00:38:59 HOL-Proofs: theory BNF_Def

00:38:59 ZF-ex: theory Ring

00:39:00 ZF-ex: theory NatSum

00:39:00 ZF-ex: theory Primes

00:39:00 ZF-ex: theory Ramsey

00:39:00 ZF-ex: theory misc

00:39:01 HOL: theory Sledgehammer

00:39:02 HOL: theory List

00:39:04 HOL-Proofs: theory BNF_Composition

00:39:04 HOL-Proofs: theory Basic_BNFs

00:39:06 HOL-Proofs: theory BNF_Fixpoint_Base

00:39:08 HOL-Proofs: theory BNF_Least_Fixpoint

00:39:10 HOL: theory Groups_List

00:39:10 HOL: theory Map

00:39:10 Timing ZF-ex (2 threads, 11.043s elapsed time, 15.552s cpu time, 0.728s GC time, factor 1.41)

00:39:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

00:39:10 Finished ZF-ex (0:00:11 elapsed time, 0:00:15 cpu time, factor 1.38)

00:39:10 Running ZF-Induct ...

00:39:10 ZF-Induct: theory Binary_Trees

00:39:10 ZF-Induct: theory Acc

00:39:10 ZF-Induct: theory Comb

00:39:10 HOL: theory Enum

00:39:10 ZF-Induct: theory Datatypes

00:39:10 HOL: theory Random

00:39:11 ZF-Induct: theory FoldSet

00:39:11 ZF-Induct: theory ListN

00:39:11 ZF-Induct: theory Mutil

00:39:11 ZF-Induct: theory Multiset

00:39:11 ZF-Induct: theory Ntree

00:39:11 ZF-Induct: theory Primrec

00:39:11 ZF-Induct: theory PropLog

00:39:11 HOL-Proofs: theory Basic_BNF_LFPs

00:39:11 ZF-Induct: theory Rmap

00:39:11 ZF-Induct: theory Term

00:39:12 ZF-Induct: theory Tree_Forest

00:39:12 HOL-Proofs: theory Transfer

00:39:12 ZF-Induct: theory Brouwer

00:39:13 HOL: theory String

00:39:13 HOL-Proofs: theory Num

00:39:14 HOL: theory BNF_Greatest_Fixpoint

00:39:14 HOL: theory Predicate

00:39:15 HOL: theory Lazy_Sequence

00:39:16 HOL: theory Limited_Sequence

00:39:16 HOL: theory Typerep

00:39:17 HOL: theory Code_Evaluation

00:39:18 HOL-Proofs: theory Power

00:39:19 HOL: theory Quickcheck_Random

00:39:20 Timing ZF-Induct (2 threads, 6.889s elapsed time, 11.088s cpu time, 0.420s GC time, factor 1.61)

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

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

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

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

00:39:20 Running ZF-AC ...

00:39:20 ZF-AC: theory AC_Equiv

00:39:21 ZF-AC: theory AC18_AC19

00:39:21 ZF-AC: theory AC7_AC9

00:39:21 ZF-AC: theory Cardinal_aux

00:39:21 HOL: theory Quickcheck_Exhaustive

00:39:21 ZF-AC: theory Hartog

00:39:21 ZF-AC: theory HH

00:39:21 ZF-AC: theory WO6_WO1

00:39:21 ZF-AC: theory AC16_lemmas

00:39:21 ZF-AC: theory AC16_WO4

00:39:21 ZF-AC: theory DC

00:39:21 HOL: theory Quickcheck_Narrowing

00:39:21 HOL-Proofs: theory Groups_Big

00:39:21 ZF-AC: theory AC15_WO6

00:39:21 ZF-AC: theory AC17_AC1

00:39:22 ZF-AC: theory WO1_AC

00:39:22 ZF-AC: theory WO1_WO7

00:39:22 ZF-AC: theory WO2_AC16

00:39:25 HOL: theory Record

00:39:25 HOL: theory Random_Pred

00:39:25 HOL: theory Random_Sequence

00:39:26 HOL: theory Predicate_Compile

00:39:26 HOL: theory Nitpick

00:39:28 HOL-Proofs: theory Equiv_Relations

00:39:29 Timing ZF-AC (2 threads, 5.953s elapsed time, 10.056s cpu time, 0.500s GC time, factor 1.69)

00:39:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

00:39:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

00:39:29 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

00:39:29 Finished ZF-AC (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.60)

00:39:29 Running FOL-ex ...

00:39:29 FOL-ex: theory Classical

00:39:29 FOL-ex: theory If

00:39:29 FOL-ex: theory Intro

00:39:29 FOL-ex: theory Miniscope

00:39:29 FOL-ex: theory Nat

00:39:29 FOL-ex: theory Nat_Class

00:39:29 FOL-ex: theory Natural_Numbers

00:39:29 FOL-ex: theory Prolog

00:39:29 FOL-ex: theory Propositional_Cla

00:39:29 FOL-ex: theory Quantifiers_Cla

00:39:29 FOL-ex: theory Foundation

00:39:29 FOL-ex: theory Intuitionistic

00:39:29 FOL-ex: theory Propositional_Int

00:39:29 FOL-ex: theory Quantifiers_Int

00:39:30 HOL-Proofs: theory Lifting

00:39:31 HOL: theory Main

00:39:32 FOL-ex: theory Locale_Test1

00:39:33 HOL: theory Archimedean_Field

00:39:33 HOL: theory Binomial

00:39:34 HOL: theory GCD

00:39:34 HOL-Proofs: theory Lifting_Set

00:39:34 FOL-ex: theory Locale_Test2

00:39:34 FOL-ex: theory Locale_Test3

00:39:34 FOL-ex: theory Locale_Test

00:39:35 HOL-Proofs: theory Option

00:39:35 HOL-Proofs: theory Quotient

00:39:37 HOL-Proofs: theory Extraction

00:39:37 Timing FOL-ex (2 threads, 5.528s elapsed time, 7.720s cpu time, 0.196s GC time, factor 1.40)

00:39:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

00:39:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

00:39:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

00:39:37 Finished FOL-ex (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.42)

00:39:37 Running CCL ...

00:39:37 CCL: theory IFOL

00:39:37 HOL: theory Topological_Spaces

00:39:38 CCL: theory FOL

00:39:39 HOL-Proofs: theory Lattices_Big

00:39:39 CCL: theory Set

00:39:40 HOL: theory Rat

00:39:40 CCL: theory Lfp

00:39:40 CCL: theory Gfp

00:39:40 CCL: theory CCL

00:39:40 CCL: theory Term

00:39:40 CCL: theory Trancl

00:39:40 CCL: theory Type

00:39:40 CCL: theory Fix

00:39:41 CCL: theory Hered

00:39:41 CCL: theory Wfd

00:39:41 CCL: theory Nat

00:39:41 CCL: theory List

00:39:41 CCL: theory Flag

00:39:41 CCL: theory Stream

00:39:42 HOL: theory Real

00:39:42 Timing CCL (2 threads, 4.851s elapsed time, 7.088s cpu time, 0.168s GC time, factor 1.46)

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

00:39:42 Finished CCL (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.41)

00:39:42 Running Sequents ...

00:39:42 Sequents: theory Sequents

00:39:43 Sequents: theory ILL

00:39:43 Sequents: theory LK0

00:39:43 Sequents: theory ILL_predlog

00:39:43 Sequents: theory Washing

00:39:43 Sequents: theory Modal0

00:39:43 Sequents: theory LK

00:39:43 Sequents: theory S4

00:39:43 Sequents: theory S43

00:39:43 Sequents: theory Hard_Quantifiers

00:39:43 Sequents: theory Nat

00:39:43 Sequents: theory Propositional

00:39:43 Sequents: theory Quantifiers

00:39:43 Sequents: theory T

00:39:44 HOL: theory Real_Vector_Spaces

00:39:45 HOL-Proofs: theory Partial_Function

00:39:47 Timing Sequents (2 threads, 4.028s elapsed time, 6.896s cpu time, 0.116s GC time, factor 1.71)

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

00:39:47 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.62)

00:39:47 Running FOLP-ex ...

00:39:47 FOLP-ex: theory Classical

00:39:47 FOLP-ex: theory If

00:39:47 HOL-Proofs: theory Fun_Def

00:39:47 FOLP-ex: theory Intro

00:39:47 FOLP-ex: theory Nat

00:39:47 FOLP-ex: theory Propositional_Cla

00:39:48 FOLP-ex: theory Quantifiers_Cla

00:39:48 FOLP-ex: theory Foundation

00:39:48 FOLP-ex: theory Intuitionistic

00:39:49 HOL-Proofs: theory Int

00:39:49 FOLP-ex: theory Propositional_Int

00:39:49 FOLP-ex: theory Quantifiers_Int

00:39:51 Timing FOLP-ex (2 threads, 3.372s elapsed time, 5.856s cpu time, 0.088s GC time, factor 1.74)

00:39:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex

00:39:51 Finished FOLP-ex (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.65)

00:39:51 Running LCF ...

00:39:51 LCF: theory IFOL

00:39:52 LCF: theory FOL

00:39:53 LCF: theory LCF

00:39:54 LCF: theory Ex1

00:39:54 LCF: theory Ex2

00:39:54 LCF: theory Ex3

00:39:54 LCF: theory Ex4

00:39:54 HOL-Proofs: theory Nat_Transfer

00:39:54 Timing LCF (2 threads, 2.746s elapsed time, 3.192s cpu time, 0.156s GC time, factor 1.16)

00:39:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

00:39:54 Finished LCF (0:00:02 elapsed time, 0:00:03 cpu time)

00:39:54 Running Spec_Check ...

00:39:54 Spec_Check: theory Spec_Check

00:39:55 Spec_Check: theory Examples

00:39:56 HOL-Proofs: theory Euclidean_Division

00:39:56 HOL: theory Inequalities

00:39:56 HOL: theory Limits

00:39:57 Warning: missing document directory

00:39:57 Timing Spec_Check (2 threads, 1.800s elapsed time, 3.260s cpu time, 0.012s GC time, factor 1.81)

00:39:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

00:39:57 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

00:39:57 Running ZF-Resid ...

00:39:57 ZF-Resid: theory Redex

00:39:57 ZF-Resid: theory Substitution

00:39:57 ZF-Resid: theory Residuals

00:39:58 ZF-Resid: theory Reduction

00:39:58 ZF-Resid: theory Confluence

00:39:59 Timing ZF-Resid (2 threads, 1.535s elapsed time, 2.520s cpu time, 0.000s GC time, factor 1.64)

00:39:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

00:39:59 Finished ZF-Resid (0:00:01 elapsed time)

00:39:59 Running ZF-IMP ...

00:39:59 ZF-IMP: theory Com

00:39:59 ZF-IMP: theory Denotation

00:39:59 HOL: theory Deriv

00:39:59 ZF-IMP: theory Equiv

00:40:00 HOL: theory Series

00:40:00 Timing ZF-IMP (2 threads, 0.996s elapsed time, 1.144s cpu time, 0.000s GC time, factor 1.15)

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

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

00:40:00 Running CTT ...

00:40:01 CTT: theory CTT

00:40:01 HOL-Proofs: theory Parity

00:40:01 CTT: theory Elimination

00:40:01 CTT: theory Bool

00:40:01 CTT: theory Arith

00:40:01 CTT: theory Equality

00:40:01 CTT: theory Typechecking

00:40:01 HOL: theory NthRoot

00:40:01 CTT: theory Synthesis

00:40:01 CTT: theory Main

00:40:02 HOL: theory Transcendental

00:40:03 Timing CTT (2 threads, 0.711s elapsed time, 1.076s cpu time, 0.000s GC time, factor 1.51)

00:40:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

00:40:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

00:40:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

00:40:03 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)

00:40:03 Running ZF-Coind ...

00:40:03 ZF-Coind: theory Map

00:40:03 ZF-Coind: theory Language

00:40:03 ZF-Coind: theory Types

00:40:03 ZF-Coind: theory Values

00:40:03 ZF-Coind: theory Dynamic

00:40:03 ZF-Coind: theory Static

00:40:04 ZF-Coind: theory ECR

00:40:04 HOL-Proofs: theory Divides

00:40:04 Timing ZF-Coind (2 threads, 0.686s elapsed time, 1.288s cpu time, 0.000s GC time, factor 1.88)

00:40:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

00:40:04 Finished ZF-Coind (0:00:00 elapsed time)

00:40:04 Running Cube ...

00:40:04 Cube: theory Cube

00:40:04 Cube: theory Example

00:40:04 Timing Cube (2 threads, 0.280s elapsed time, 0.288s cpu time, 0.000s GC time, factor 1.03)

00:40:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

00:40:04 Finished Cube (0:00:00 elapsed time)

00:40:04 Running System ...

00:40:05 System: theory Base

00:40:05 System: theory Environment

00:40:05 System: theory Misc

00:40:05 System: theory Presentation

00:40:05 System: theory Scala

00:40:05 System: theory Sessions

00:40:06 HOL: theory Complex

00:40:06 HOL: theory MacLaurin

00:40:07 Timing System (2 threads, 0.307s elapsed time, 0.412s cpu time, 0.000s GC time, factor 1.34)

00:40:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

00:40:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

00:40:07 Finished System (0:00:02 elapsed time)

00:40:07 Running Logics_ZF ...

00:40:07 HOL: theory Complex_Main

00:40:08 Logics_ZF: theory FOL_examples

00:40:08 Logics_ZF: theory If

00:40:08 Logics_ZF: theory ZF_Isar

00:40:08 Logics_ZF: theory ZF_examples

00:40:08 Logics_ZF: theory IFOL_examples

00:40:11 Timing Logics_ZF (2 threads, 0.275s elapsed time, 0.548s cpu time, 0.000s GC time, factor 1.99)

00:40:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

00:40:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

00:40:11 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.99)

00:40:11 Running SML ...

00:40:11 SML: theory Examples

00:40:12 Warning: missing document directory

00:40:12 Timing SML (2 threads, 0.015s elapsed time, 0.016s cpu time, 0.000s GC time, factor 1.05)

00:40:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

00:40:12 Finished SML (0:00:00 elapsed time)

00:40:12 Running Intro ...

00:40:14 Timing Intro (2 threads, 0.001s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

00:40:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

00:40:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

00:40:14 Finished Intro (0:00:02 elapsed time)

00:40:14 Running Logics ...

00:40:17 Timing Logics (2 threads, 0.001s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

00:40:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics

00:40:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf

00:40:17 Finished Logics (0:00:02 elapsed time)

00:40:17 Running Nitpick ...

00:40:19 Timing Nitpick (2 threads, 0.001s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

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

00:40:19 Finished Nitpick (0:00:02 elapsed time)

00:40:19 Running Sledgehammer ...

00:40:22 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

00:40:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

00:40:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

00:40:22 Finished Sledgehammer (0:00:02 elapsed time)

00:40:24 HOL-Proofs: theory Code_Numeral

00:40:28 HOL-Proofs: theory Numeral_Simprocs

00:40:29 HOL-Proofs: theory SMT

00:40:30 HOL-Proofs: theory Semiring_Normalization

00:40:33 HOL-Proofs: theory Groebner_Basis

00:40:33 HOL-Proofs: theory Set_Interval

00:40:44 HOL-Proofs: theory Conditionally_Complete_Lattices

00:40:46 HOL-Proofs: theory Filter

00:40:50 HOL-Proofs: theory Presburger

00:41:01 HOL-Proofs: theory Sledgehammer

00:41:03 HOL-Proofs: theory List

00:41:40 HOL-Proofs: theory Groups_List

00:41:41 HOL-Proofs: theory Map

00:41:44 HOL-Proofs: theory Enum

00:41:59 HOL-Proofs: theory Random

00:42:48 HOL-Proofs: theory String

00:42:50 HOL-Proofs: theory BNF_Greatest_Fixpoint

00:42:55 HOL-Proofs: theory Predicate

00:42:57 HOL-Proofs: theory Lazy_Sequence

00:42:58 HOL-Proofs: theory Limited_Sequence

00:42:59 HOL-Proofs: theory Typerep

00:43:00 HOL-Proofs: theory Code_Evaluation

00:43:02 HOL-Proofs: theory Quickcheck_Random

00:43:05 HOL-Proofs: theory Quickcheck_Exhaustive

00:43:10 HOL-Proofs: theory Record

00:43:12 HOL-Proofs: theory Nitpick

00:43:16 Timing HOL (2 threads, 238.596s elapsed time, 443.336s cpu time, 26.432s GC time, factor 1.86)

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

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

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

00:43:16 Finished HOL (0:05:41 elapsed time, 0:10:10 cpu time, factor 1.79)

00:43:18 Building HOLCF ...

00:43:18 Building HOL-Word ...

00:43:19 HOL-Proofs: theory Quickcheck_Narrowing

00:43:20 HOLCF: theory Nat_Bijection

00:43:20 HOLCF: theory Old_Datatype

00:43:20 HOL-Word: theory Bit

00:43:20 HOL-Word: theory Bits

00:43:20 HOL-Word: theory Boolean_Algebra

00:43:21 HOL-Word: theory Bits_Bit

00:43:21 HOL-Word: theory Misc_Numeric

00:43:21 HOL-Word: theory Bit_Representation

00:43:21 HOL-Word: theory Misc_Typedef

00:43:21 HOL-Word: theory Phantom_Type

00:43:21 HOLCF: theory Countable

00:43:21 HOL-Word: theory Bits_Int

00:43:22 HOL-Word: theory Cardinality

00:43:23 HOLCF: theory Porder

00:43:23 HOL-Word: theory Bool_List_Representation

00:43:24 HOL-Word: theory Numeral_Type

00:43:24 HOLCF: theory Pcpo

00:43:24 HOL-Word: theory Word_Miscellaneous

00:43:25 HOL-Word: theory Type_Length

00:43:25 HOL-Word: theory Word

00:43:25 HOLCF: theory Cont

00:43:25 HOL-Proofs: theory Random_Pred

00:43:26 HOLCF: theory Adm

00:43:26 HOLCF: theory Discrete

00:43:26 HOLCF: theory Cpodef

00:43:26 HOL-Proofs: theory Random_Sequence

00:43:26 HOLCF: theory Fun_Cpo

00:43:27 HOLCF: theory Product_Cpo

00:43:27 HOLCF: theory Cfun

00:43:27 HOL-Proofs: theory Predicate_Compile

00:43:28 HOLCF: theory Cprod

00:43:28 HOLCF: theory Fix

00:43:28 HOLCF: theory Sfun

00:43:28 HOLCF: theory Sprod

00:43:28 HOLCF: theory Up

00:43:29 HOLCF: theory Lift

00:43:30 HOLCF: theory One

00:43:30 HOLCF: theory Tr

00:43:30 HOL-Proofs: theory Main

00:43:30 HOLCF: theory Ssum

00:43:30 HOLCF: theory Plain_HOLCF

00:43:31 HOLCF: theory Completion

00:43:31 HOLCF: theory Deflation

00:43:32 HOLCF: theory Map_Functions

00:43:32 HOLCF: theory Fixrec

00:43:32 HOL-Proofs: theory Old_Datatype

00:43:32 HOLCF: theory Bifinite

00:43:32 HOLCF: theory Domain_Aux

00:43:34 HOLCF: theory Universal

00:43:35 HOLCF: theory Algebraic

00:43:35 HOLCF: theory Compact_Basis

00:43:35 HOLCF: theory LowerPD

00:43:36 HOLCF: theory UpperPD

00:43:36 HOLCF: theory Representable

00:43:36 HOLCF: theory ConvexPD

00:43:39 HOLCF: theory Domain

00:43:41 HOLCF: theory Powerdomains

00:43:42 HOLCF: theory HOLCF

00:44:06 Timing HOL-Word (2 threads, 24.252s elapsed time, 46.800s cpu time, 2.036s GC time, factor 1.93)

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

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

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

00:44:06 Finished HOL-Word (0:00:47 elapsed time, 0:01:22 cpu time, factor 1.73)

00:44:06 Building HOL-TLA ...

00:44:07 Timing HOLCF (2 threads, 22.850s elapsed time, 41.344s cpu time, 2.344s GC time, factor 1.81)

00:44:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF

00:44:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

00:44:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

00:44:07 Finished HOLCF (0:00:49 elapsed time, 0:01:21 cpu time, factor 1.66)

00:44:07 Building IOA ...

00:44:08 HOL-TLA: theory Intensional

00:44:08 HOL-TLA: theory Stfun

00:44:09 HOL-TLA: theory Action

00:44:09 HOL-TLA: theory Init

00:44:09 HOL-TLA: theory TLA

00:44:10 IOA: theory Seq

00:44:10 IOA: theory Asig

00:44:10 IOA: theory Automata

00:44:11 IOA: theory Sequence

00:44:11 IOA: theory Pred

00:44:12 IOA: theory Traces

00:44:13 IOA: theory TL

00:44:13 IOA: theory CompoExecs

00:44:13 IOA: theory RefMappings

00:44:14 IOA: theory RefCorrectness

00:44:14 IOA: theory CompoScheds

00:44:14 IOA: theory Simulations

00:44:15 IOA: theory SimCorrectness

00:44:15 IOA: theory Deadlock

00:44:15 IOA: theory ShortExecutions

00:44:15 IOA: theory CompoTraces

00:44:16 IOA: theory Compositionality

00:44:17 IOA: theory IOA

00:44:17 IOA: theory TLS

00:44:18 IOA: theory LiveIOA

00:44:18 IOA: theory Abstraction

00:44:23 Timing HOL-TLA (2 threads, 1.998s elapsed time, 3.120s cpu time, 0.000s GC time, factor 1.56)

00:44:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA

00:44:23 Finished HOL-TLA (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.44)

00:44:24 Building HOL-Analysis ...

00:44:27 HOL-Analysis: theory Cancellation

00:44:27 HOL-Analysis: theory Disjoint_Sets

00:44:28 HOL-Analysis: theory FuncSet

00:44:28 HOL-Analysis: theory Multiset

00:44:28 HOL-Analysis: theory Infinite_Set

00:44:29 HOL-Analysis: theory Nat_Bijection

00:44:29 HOL-Analysis: theory Old_Datatype

00:44:31 HOL-Analysis: theory Countable

00:44:33 HOL-Analysis: theory Countable_Set

00:44:33 HOL-Analysis: theory Permutations

00:44:33 HOL-Analysis: theory Factorial_Ring

00:44:35 HOL-Analysis: theory Countable_Complete_Lattices

00:44:38 HOL-Analysis: theory Phantom_Type

00:44:39 HOL-Analysis: theory Cardinality

00:44:40 HOL-Analysis: theory Numeral_Type

00:44:41 HOL-Analysis: theory Product_Plus

00:44:41 HOL-Analysis: theory Product_Order

00:44:42 HOL-Analysis: theory Set_Algebras

00:44:42 HOL-Analysis: theory L2_Norm

00:44:43 HOL-Analysis: theory Continuum_Not_Denumerable

00:44:43 HOL-Analysis: theory Euclidean_Algorithm

00:44:43 HOL-Analysis: theory Discrete

00:44:43 HOL-Analysis: theory Indicator_Function

00:44:44 HOL-Analysis: theory Inner_Product

00:44:45 HOL-Analysis: theory Product_Vector

00:44:46 HOL-Analysis: theory Euclidean_Space

00:44:47 Timing IOA (2 threads, 17.995s elapsed time, 33.680s cpu time, 1.160s GC time, factor 1.87)

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

00:44:47 Finished IOA (0:00:39 elapsed time, 0:01:04 cpu time, factor 1.64)

00:44:47 Building HOL-SPARK ...

00:44:48 HOL-Analysis: theory Finite_Cartesian_Product

00:44:49 HOL-Analysis: theory Linear_Algebra

00:44:50 HOL-SPARK: theory Bit_Comparison

00:44:50 HOL-SPARK: theory SPARK_Setup

00:44:51 HOL-Analysis: theory Primes

00:44:52 HOL-Analysis: theory Liminf_Limsup

00:44:52 HOL-SPARK: theory SPARK

00:44:52 HOL-Analysis: theory Nonpos_Ints

00:44:52 HOL-Analysis: theory Operator_Norm

00:44:53 HOL-Analysis: theory Order_Continuity

00:44:53 HOL-Analysis: theory Periodic_Fun

00:44:53 HOL-Analysis: theory Poly_Roots

00:44:53 HOL-Analysis: theory Sum_of_Squares

00:44:54 HOL-Analysis: theory Extended_Nat

00:44:55 HOL-Analysis: theory Extended_Real

00:44:56 HOL-Analysis: theory Norm_Arith

00:44:57 HOL-Analysis: theory Topology_Euclidean_Space

00:44:59 HOL-Analysis: theory Extended_Nonnegative_Real

00:45:01 HOL-Analysis: theory Sigma_Algebra

00:45:04 HOL-Analysis: theory Measurable

00:45:05 HOL-Analysis: theory Measure_Space

00:45:06 Timing HOL-SPARK (2 threads, 2.625s elapsed time, 4.368s cpu time, 0.156s GC time, factor 1.66)

00:45:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK

00:45:06 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:26 cpu time, factor 1.44)

00:45:06 Building HOL-Library ...

00:45:07 HOL-Analysis: theory Bounded_Linear_Function

00:45:08 HOL-Analysis: theory Caratheodory

00:45:09 HOL-Analysis: theory Convex_Euclidean_Space

00:45:09 HOL-Analysis: theory Extended_Real_Limits

00:45:09 HOL-Library: theory Adhoc_Overloading

00:45:09 HOL-Library: theory Lattice_Syntax

00:45:09 HOL-Library: theory AList

00:45:10 HOL-Library: theory BNF_Axiomatization

00:45:10 HOL-Library: theory BNF_Corec

00:45:10 HOL-Analysis: theory Tagged_Division

00:45:11 HOL-Library: theory DAList

00:45:12 HOL-Analysis: theory Summation_Tests

00:45:12 HOL-Analysis: theory Uniform_Limit

00:45:13 HOL-Library: theory Stirling

00:45:13 HOL-Library: theory Bit

00:45:14 HOL-Library: theory Bits

00:45:14 HOL-Library: theory Bits_Bit

00:45:15 HOL-Library: theory Boolean_Algebra

00:45:15 HOL-Library: theory Cancellation

00:45:15 HOL-Analysis: theory Continuous_Extension

00:45:15 HOL-Analysis: theory Path_Connected

00:45:16 HOL-Library: theory Multiset

00:45:16 HOL-Library: theory Cardinal_Notations

00:45:16 HOL-Library: theory Char_ord

00:45:16 HOL-Library: theory Code_Abstract_Nat

00:45:17 HOL-Library: theory Code_Binary_Nat

00:45:17 HOL-Library: theory Code_Target_Nat

00:45:17 HOL-Library: theory Code_Char

00:45:17 HOL-Library: theory Code_Prolog

00:45:18 HOL-Library: theory Code_Test

00:45:19 HOL-Library: theory Combine_PER

00:45:19 HOL-Library: theory Complete_Partial_Order2

00:45:20 HOL-Analysis: theory Homeomorphism

00:45:21 HOL-Analysis: theory Brouwer_Fixpoint

00:45:21 HOL-Library: theory DAList_Multiset

00:45:22 HOL-Library: theory Multiset_Order

00:45:22 HOL-Library: theory Permutation

00:45:22 HOL-Library: theory Debug

00:45:23 HOL-Library: theory Disjoint_Sets

00:45:23 HOL-Library: theory Dlist

00:45:23 HOL-Analysis: theory Derivative

00:45:23 HOL-Library: theory Permutations

00:45:24 HOL-Library: theory FSet

00:45:24 HOL-Library: theory Fraction_Field

00:45:25 HOL-Library: theory Fun_Lexorder

00:45:26 HOL-Library: theory FuncSet

00:45:26 HOL-Analysis: theory Cartesian_Euclidean_Space

00:45:26 HOL-Analysis: theory Weierstrass_Theorems

00:45:26 HOL-Library: theory Function_Algebras

00:45:27 HOL-Library: theory Function_Division

00:45:27 HOL-Library: theory Code_Target_Int

00:45:27 HOL-Library: theory Code_Target_Numeral

00:45:27 HOL-Library: theory Factorial_Ring

00:45:28 HOL-Library: theory Finite_Map

00:45:29 HOL-Analysis: theory Determinants

00:45:29 HOL-Analysis: theory Fashoda_Theorem

00:45:29 HOL-Analysis: theory Ordered_Euclidean_Space

00:45:30 HOL-Library: theory Groups_Big_Fun

00:45:30 HOL-Analysis: theory Polytope

00:45:30 HOL-Library: theory IArray

00:45:31 HOL-Library: theory Infinite_Set

00:45:32 HOL-Library: theory Omega_Words_Fun

00:45:32 HOL-Library: theory LaTeXsugar

00:45:32 HOL-Library: theory Lattice_Constructions

00:45:35 HOL-Library: theory ListVector

00:45:35 HOL-Analysis: theory Arcwise_Connected

00:45:35 HOL-Analysis: theory Borel_Space

00:45:35 HOL-Library: theory List_lexord

00:45:36 HOL-Library: theory Mapping

00:45:36 HOL-Library: theory Euclidean_Algorithm

00:45:37 HOL-Library: theory AList_Mapping

00:45:37 HOL-Library: theory Misc_Numeric

00:45:37 HOL-Library: theory Bit_Representation

00:45:38 HOL-Library: theory Bits_Int

00:45:38 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

00:45:39 HOL-Library: theory Bool_List_Representation

00:45:39 HOL-Analysis: theory Regularity

00:45:40 HOL-Library: theory Misc_Typedef

00:45:41 HOL-Library: theory Monad_Syntax

00:45:41 HOL-Library: theory More_List

00:45:41 HOL-Analysis: theory Binary_Product_Measure

00:45:41 HOL-Library: theory Nat_Bijection

00:45:42 HOL-Library: theory Stream

00:45:42 HOL-Analysis: theory Embed_Measure

00:45:42 HOL-Analysis: theory Finite_Product_Measure

00:45:43 HOL-Library: theory Old_Datatype

00:45:44 HOL-Analysis: theory Bochner_Integration

00:45:44 HOL-Analysis: theory Function_Topology

00:45:44 HOL-Library: theory Countable

00:45:45 HOL-Library: theory Normalized_Fraction

00:45:45 HOL-Library: theory Old_Recdef

00:45:46 HOL-Analysis: theory Complete_Measure

00:45:46 HOL-Library: theory Countable_Set

00:45:46 HOL-Analysis: theory Radon_Nikodym

00:45:46 HOL-Library: theory Option_ord

00:45:47 HOL-Library: theory Countable_Complete_Lattices

00:45:47 HOL-Library: theory Countable_Set_Type

00:45:47 HOL-Analysis: theory Set_Integral

00:45:47 HOL-Analysis: theory Lebesgue_Measure

00:45:49 HOL-Analysis: theory Henstock_Kurzweil_Integration

00:45:49 HOL-Library: theory Parallel

00:45:50 HOL-Library: theory Perm

00:45:50 HOL-Library: theory Phantom_Type

00:45:51 HOL-Library: theory Cardinality

00:45:51 HOL-Library: theory Predicate_Compile_Alternative_Defs

00:45:52 HOL-Library: theory Predicate_Compile_Quickcheck

00:45:52 HOL-Library: theory Product_Lexorder

00:45:52 HOL-Library: theory Numeral_Type

00:45:52 HOL-Library: theory Product_Plus

00:45:52 HOL-Library: theory Product_Order

00:45:53 HOL-Library: theory Finite_Lattice

00:45:53 HOL-Analysis: theory Bounded_Continuous_Function

00:45:53 HOL-Library: theory Type_Length

00:45:53 HOL-Library: theory Saturated

00:45:54 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

00:45:54 HOL-Library: theory Quotient_Syntax

00:45:54 HOL-Analysis: theory Integral_Test

00:45:54 HOL-Library: theory Quotient_Option

00:45:54 HOL-Library: theory Quotient_Product

00:45:54 HOL-Library: theory Quotient_Set

00:45:54 HOL-Library: theory Quotient_List

00:45:55 HOL-Library: theory Quotient_Sum

00:45:55 HOL-Library: theory Quotient_Type

00:45:55 HOL-Analysis: theory Complex_Analysis_Basics

00:45:55 HOL-Analysis: theory Interval_Integral

00:45:55 HOL-Library: theory RBT_Impl

00:45:56 HOL-Analysis: theory Lebesgue_Integral_Substitution

00:45:57 HOL-Library: theory Ramsey

00:45:57 HOL-Library: theory Reflection

00:45:57 HOL-Analysis: theory Complex_Transcendental

00:45:57 HOL-Library: theory Refute

00:45:58 HOL-Library: theory Rewrite

00:45:58 HOL-Library: theory Set_Algebras

00:45:59 HOL-Library: theory Simps_Case_Conv

00:45:59 HOL-Library: theory Extended

00:46:00 HOL-Analysis: theory Generalised_Binomial_Theorem

00:46:00 HOL-Analysis: theory Harmonic_Numbers

00:46:00 HOL-Analysis: theory Cauchy_Integral_Theorem

00:46:00 HOL-Analysis: theory Further_Topology

00:46:01 HOL-Library: theory State_Monad

00:46:01 HOL-Library: theory Sublist

00:46:02 HOL-Library: theory Prefix_Order

00:46:02 HOL-Library: theory Sublist_Order

00:46:02 HOL-Library: theory Polynomial

00:46:04 HOL-Analysis: theory Jordan_Curve

00:46:05 HOL-Analysis: theory Conformal_Mappings

00:46:05 HOL-Analysis: theory Gamma_Function

00:46:07 HOL-Analysis: theory Great_Picard

00:46:08 HOL-Analysis: theory Winding_Numbers

00:46:09 HOL-Analysis: theory Analysis

00:46:10 HOL-Library: theory BigO

00:46:11 HOL-Library: theory Code_Real_Approx_By_Float

00:46:12 HOL-Library: theory Diagonal_Subsequence

00:46:12 HOL-Library: theory Discrete

00:46:13 HOL-Library: theory Field_as_Ring

00:46:15 HOL-Library: theory Formal_Power_Series

00:46:20 HOL-Library: theory Polynomial_FPS

00:46:21 HOL-Library: theory Fundamental_Theorem_Algebra

00:46:22 HOL-Library: theory Indicator_Function

00:46:22 HOL-Library: theory Lattice_Algebras

00:46:29 HOL-Library: theory Liminf_Limsup

00:46:30 HOL-Library: theory Log_Nat

00:46:31 HOL-Library: theory Float

00:46:34 HOL-Library: theory Lub_Glb

00:46:34 HOL-Library: theory Multiset_Permutations

00:46:34 HOL-Library: theory RBT

00:46:35 HOL-Library: theory RBT_Mapping

00:46:36 HOL-Library: theory RBT_Set

00:46:36 HOL-Library: theory Nonpos_Ints

00:46:36 HOL-Library: theory OptionalSugar

00:46:36 HOL-Library: theory Order_Continuity

00:46:37 HOL-Library: theory Periodic_Fun

00:46:37 HOL-Library: theory Polynomial_Factorial

00:46:37 HOL-Library: theory Extended_Nat

00:46:38 HOL-Library: theory Extended_Real

00:46:43 HOL-Library: theory Extended_Nonnegative_Real

00:46:46 HOL-Library: theory Linear_Temporal_Logic_on_Streams

00:46:48 HOL-Library: theory Quadratic_Discriminant

00:46:49 HOL-Library: theory Sum_of_Squares

00:46:52 HOL-Library: theory Transitive_Closure_Table

00:46:52 HOL-Library: theory Tree

00:46:52 HOL-Library: theory While_Combinator

00:46:53 HOL-Library: theory Bourbaki_Witt_Fixpoint

00:46:53 HOL-Library: theory Word_Miscellaneous

00:46:54 HOL-Library: theory Word

00:46:56 HOL-Library: theory Tree_Multiset

00:46:56 HOL-Library: theory Preorder

00:46:56 HOL-Library: theory Function_Growth

00:46:58 HOL-Library: theory Library

00:47:00 HOL-Library: theory Old_SMT

00:49:09 Timing HOL-Proofs (2 threads, 543.315s elapsed time, 967.760s cpu time, 100.652s GC time, factor 1.78)

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

00:49:09 Finished HOL-Proofs (0:11:34 elapsed time, 0:20:12 cpu time, factor 1.75)

00:49:11 Building HOL-Auth ...

00:49:13 HOL-Auth: theory Message

00:49:13 HOL-Auth: theory Nat_Bijection

00:49:14 HOL-Auth: theory Simps_Case_Conv

00:49:16 HOL-Auth: theory All_Symmetric

00:49:16 HOL-Auth: theory Event

00:49:16 HOL-Auth: theory EventSC

00:49:17 HOL-Auth: theory Extensions

00:49:18 HOL-Auth: theory Analz

00:49:19 HOL-Auth: theory List_Msg

00:49:19 HOL-Auth: theory Guard

00:49:19 HOL-Auth: theory GuardK

00:49:20 HOL-Auth: theory Public

00:49:21 HOL-Auth: theory Shared

00:49:21 HOL-Auth: theory CertifiedEmail

00:49:21 HOL-Auth: theory Guard_Public

00:49:22 HOL-Auth: theory Guard_NS_Public

00:49:22 HOL-Auth: theory P2

00:49:22 HOL-Auth: theory Proto

00:49:24 HOL-Auth: theory KerberosIV

00:49:26 HOL-Auth: theory KerberosIV_Gets

00:49:26 HOL-Auth: theory KerberosV

00:49:28 HOL-Auth: theory Kerberos_BAN

00:49:28 HOL-Auth: theory Kerberos_BAN_Gets

00:49:29 HOL-Auth: theory NS_Public

00:49:29 HOL-Auth: theory NS_Public_Bad

00:49:29 HOL-Auth: theory NS_Shared

00:49:30 HOL-Auth: theory OtwayRees

00:49:30 HOL-Auth: theory OtwayReesBella

00:49:31 HOL-Auth: theory OtwayRees_AN

00:49:31 HOL-Auth: theory OtwayRees_Bad

00:49:31 HOL-Auth: theory P1

00:49:32 HOL-Auth: theory Recur

00:49:33 HOL-Auth: theory WooLam

00:49:33 HOL-Auth: theory Yahalom

00:49:34 HOL-Auth: theory Yahalom2

00:49:35 HOL-Auth: theory Yahalom_Bad

00:49:35 HOL-Auth: theory ZhouGollmann

00:49:36 HOL-Auth: theory Auth_Shared

00:49:37 HOL-Auth: theory Auth_Guard_Public

00:49:37 HOL-Auth: theory Guard_Shared

00:49:38 HOL-Auth: theory Guard_OtwayRees

00:49:38 HOL-Auth: theory Guard_Yahalom

00:49:38 HOL-Auth: theory TLS

00:49:39 HOL-Auth: theory Auth_Guard_Shared

00:49:39 HOL-Auth: theory Smartcard

00:49:39 HOL-Auth: theory ShoupRubin

00:49:41 HOL-Auth: theory Auth_Public

00:49:41 HOL-Auth: theory ShoupRubinBella

00:49:43 HOL-Auth: theory Auth_Smartcard

00:51:58 Timing HOL-Library (2 threads, 292.998s elapsed time, 535.232s cpu time, 33.316s GC time, factor 1.83)

00:51:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library

00:51:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf

00:51:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf

00:51:58 Finished HOL-Library (0:06:50 elapsed time, 0:12:05 cpu time, factor 1.77)

00:52:00 Building Codegen_Basics ...

00:52:02 Codegen_Basics: theory IArray

00:52:02 Codegen_Basics: theory Dlist

00:52:03 Codegen_Basics: theory Mapping

00:52:03 Codegen_Basics: theory RBT_Impl

00:52:40 Codegen_Basics: theory RBT

00:52:40 Codegen_Basics: theory Setup

00:53:09 Timing HOL-Auth (2 threads, 196.366s elapsed time, 312.736s cpu time, 10.612s GC time, factor 1.59)

00:53:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

00:53:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

00:53:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

00:53:09 Finished HOL-Auth (0:03:57 elapsed time, 0:06:18 cpu time, factor 1.59)

00:53:09 Building HOL-Nonstandard_Analysis ...

00:53:11 HOL-Nonstandard_Analysis: theory Lub_Glb

00:53:11 HOL-Nonstandard_Analysis: theory Infinite_Set

00:53:12 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

00:53:12 HOL-Nonstandard_Analysis: theory StarDef

00:53:13 HOL-Nonstandard_Analysis: theory HyperNat

00:53:14 HOL-Nonstandard_Analysis: theory HyperDef

00:53:15 HOL-Nonstandard_Analysis: theory NSA

00:53:17 HOL-Nonstandard_Analysis: theory NSComplex

00:53:17 HOL-Nonstandard_Analysis: theory Star

00:53:18 HOL-Nonstandard_Analysis: theory HLim

00:53:18 HOL-Nonstandard_Analysis: theory NatStar

00:53:18 HOL-Nonstandard_Analysis: theory HDeriv

00:53:19 HOL-Nonstandard_Analysis: theory HSEQ

00:53:19 HOL-Nonstandard_Analysis: theory HSeries

00:53:20 HOL-Nonstandard_Analysis: theory HTranscendental

00:53:21 HOL-Nonstandard_Analysis: theory HLog

00:53:22 HOL-Nonstandard_Analysis: theory NSCA

00:53:22 HOL-Nonstandard_Analysis: theory Hyperreal

00:53:22 HOL-Nonstandard_Analysis: theory CStar

00:53:23 HOL-Nonstandard_Analysis: theory CLim

00:53:23 HOL-Nonstandard_Analysis: theory Hypercomplex

00:53:24 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

00:53:39 Timing Codegen_Basics (2 threads, 63.240s elapsed time, 111.560s cpu time, 4.172s GC time, factor 1.76)

00:53:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

00:53:39 Finished Codegen_Basics (0:01:38 elapsed time, 0:02:46 cpu time, factor 1.69)

00:53:39 Building Typeclass_Hierarchy_Basics ...

00:53:41 Typeclass_Hierarchy_Basics: theory Lattice_Syntax

00:53:41 Typeclass_Hierarchy_Basics: theory Cancellation

00:53:42 Typeclass_Hierarchy_Basics: theory Multiset

00:53:47 Typeclass_Hierarchy_Basics: theory Setup

00:53:47 Timing HOL-Nonstandard_Analysis (2 threads, 16.240s elapsed time, 31.820s cpu time, 1.264s GC time, factor 1.96)

00:53:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

00:53:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

00:53:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

00:53:47 Finished HOL-Nonstandard_Analysis (0:00:37 elapsed time, 0:01:04 cpu time, factor 1.71)

00:53:47 Building HOL-Nominal ...

00:53:49 HOL-Nominal: theory Infinite_Set

00:53:49 HOL-Nominal: theory Old_Datatype

00:53:51 HOL-Nominal: theory Nominal

00:54:08 Timing Typeclass_Hierarchy_Basics (2 threads, 10.053s elapsed time, 18.184s cpu time, 0.812s GC time, factor 1.81)

00:54:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

00:54:08 Finished Typeclass_Hierarchy_Basics (0:00:28 elapsed time, 0:00:45 cpu time, factor 1.59)

00:54:08 Building HOL-Eisbach ...

00:54:10 HOL-Eisbach: theory Eisbach

00:54:10 HOL-Eisbach: theory IFOL

00:54:11 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax

00:54:11 HOL-Eisbach: theory Eisbach_Tools

00:54:11 HOL-Eisbach: theory Examples

00:54:11 HOL-Eisbach: theory Tests

00:54:12 HOL-Eisbach: theory FOL

00:54:13 HOL-Eisbach: theory Examples_FOL

00:54:15 Timing HOL-Nominal (2 threads, 9.419s elapsed time, 18.252s cpu time, 0.992s GC time, factor 1.94)

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

00:54:15 Finished HOL-Nominal (0:00:27 elapsed time, 0:00:44 cpu time, factor 1.63)

00:54:15 Building HOL-Mirabelle ...

00:54:17 HOL-Mirabelle: theory Mirabelle

00:54:17 HOL-Mirabelle: theory Mirabelle_Test

00:54:28 Warning: missing document directory

00:54:28 Timing HOL-Eisbach (2 threads, 3.249s elapsed time, 6.192s cpu time, 0.164s GC time, factor 1.91)

00:54:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

00:54:28 Finished HOL-Eisbach (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.51)

00:54:28 Running HOL-Nominal-Examples ...

00:54:31 HOL-Nominal-Examples: theory CK_Machine

00:54:31 HOL-Nominal-Examples: theory CR_Takahashi

00:54:31 Timing HOL-Mirabelle (2 threads, 0.544s elapsed time, 0.624s cpu time, 0.000s GC time, factor 1.15)

00:54:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

00:54:31 Finished HOL-Mirabelle (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.42)

00:54:31 Running HOL-Data_Structures ...

00:54:33 HOL-Data_Structures: theory Cancellation

00:54:33 HOL-Data_Structures: theory Less_False

00:54:33 HOL-Data_Structures: theory Fib

00:54:34 HOL-Nominal-Examples: theory Class1

00:54:34 HOL-Data_Structures: theory Multiset

00:54:44 HOL-Data_Structures: theory Cmp

00:54:44 HOL-Data_Structures: theory Sorted_Less

00:54:44 HOL-Nominal-Examples: theory Compile

00:54:45 HOL-Data_Structures: theory AList_Upd_Del

00:54:45 HOL-Data_Structures: theory List_Ins_Del

00:54:45 HOL-Data_Structures: theory Map_by_Ordered

00:54:45 HOL-Data_Structures: theory Set_by_Ordered

00:54:45 HOL-Data_Structures: theory Tree

00:54:46 HOL-Data_Structures: theory Brother12_Set

00:54:50 HOL-Data_Structures: theory Balance

00:54:51 HOL-Data_Structures: theory Splay_Set

00:54:53 HOL-Data_Structures: theory Splay_Map

00:54:54 HOL-Data_Structures: theory Tree_Set

00:54:56 HOL-Data_Structures: theory Tree_Map

00:54:56 HOL-Data_Structures: theory Tree2

00:54:57 HOL-Data_Structures: theory Isin2

00:54:58 HOL-Data_Structures: theory AA_Set

00:55:00 HOL-Data_Structures: theory AVL_Set

00:55:01 HOL-Data_Structures: theory Leftist_Heap

00:55:04 HOL-Nominal-Examples: theory Contexts

00:55:04 HOL-Data_Structures: theory Lookup2

00:55:05 HOL-Data_Structures: theory AA_Map

00:55:05 HOL-Data_Structures: theory AVL_Map

00:55:06 HOL-Data_Structures: theory RBT

00:55:10 HOL-Data_Structures: theory RBT_Set

00:55:10 HOL-Nominal-Examples: theory Crary

00:55:14 HOL-Data_Structures: theory RBT_Map

00:55:16 HOL-Nominal-Examples: theory Fsub

00:55:18 HOL-Data_Structures: theory Tree23

00:55:20 HOL-Data_Structures: theory Tree23_Set

00:55:24 HOL-Nominal-Examples: theory Height

00:55:27 HOL-Nominal-Examples: theory Lam_Funs

00:55:27 HOL-Data_Structures: theory Tree23_Map

00:55:31 HOL-Nominal-Examples: theory CR

00:55:32 HOL-Nominal-Examples: theory SN

00:55:32 HOL-Data_Structures: theory Tree234

00:55:34 HOL-Nominal-Examples: theory Lambda_mu

00:55:35 HOL-Data_Structures: theory Tree234_Set

00:55:38 HOL-Nominal-Examples: theory LocalWeakening

00:55:41 HOL-Nominal-Examples: theory Pattern

00:55:52 HOL-Nominal-Examples: theory SOS

00:55:55 HOL-Nominal-Examples: theory Standardization

00:55:59 HOL-Nominal-Examples: theory Support

00:56:00 HOL-Nominal-Examples: theory Type_Preservation

00:56:04 HOL-Nominal-Examples: theory W

00:56:07 HOL-Data_Structures: theory Tree234_Map

00:56:10 HOL-Nominal-Examples: theory Weakening

00:56:25 HOL-Data_Structures: theory Brother12_Map

00:57:28 HOL-Nominal-Examples: theory Class2

00:57:31 HOL-Nominal-Examples: theory Class3

01:00:15 Timing HOL-Analysis (2 threads, 836.759s elapsed time, 1434.740s cpu time, 79.844s GC time, factor 1.71)

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

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

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

01:00:15 Finished HOL-Analysis (0:15:51 elapsed time, 0:26:47 cpu time, factor 1.69)

01:00:17 Building HOL-Probability ...

01:00:21 HOL-Probability: theory AList

01:00:21 HOL-Probability: theory Permutation

01:00:22 HOL-Probability: theory FSet

01:00:23 HOL-Probability: theory Diagonal_Subsequence

01:00:25 HOL-Probability: theory Finite_Map

01:00:34 HOL-Probability: theory Adhoc_Overloading

01:00:34 HOL-Probability: theory Lattice_Syntax

01:00:34 HOL-Probability: theory Complete_Partial_Order2

01:00:34 HOL-Probability: theory Mapping

01:00:36 HOL-Probability: theory AList_Mapping

01:00:36 HOL-Probability: theory Monad_Syntax

01:00:36 HOL-Probability: theory Stream

01:00:37 HOL-Probability: theory Rewrite

01:00:38 HOL-Probability: theory Sublist

01:00:38 HOL-Probability: theory Multiset_Permutations

01:00:39 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

01:00:39 HOL-Probability: theory Fin_Map

01:00:41 HOL-Probability: theory Discrete_Topology

01:00:41 HOL-Probability: theory Essential_Supremum

01:00:41 HOL-Probability: theory Probability_Measure

01:00:41 HOL-Probability: theory Stopping_Time

01:00:43 HOL-Probability: theory Conditional_Expectation

01:00:43 HOL-Probability: theory Distribution_Functions

01:00:44 HOL-Probability: theory Weak_Convergence

01:00:44 HOL-Probability: theory Giry_Monad

01:00:44 HOL-Probability: theory Helly_Selection

01:00:46 HOL-Probability: theory Probability_Mass_Function

01:00:47 HOL-Probability: theory Projective_Family

01:00:48 HOL-Probability: theory Infinite_Product_Measure

01:00:49 HOL-Probability: theory PMF_Impl

01:00:49 HOL-Probability: theory Random_Permutations

01:00:50 HOL-Probability: theory SPMF

01:00:51 HOL-Probability: theory Independent_Family

01:00:53 HOL-Probability: theory Convolution

01:00:53 HOL-Probability: theory Information

01:00:54 HOL-Probability: theory Projective_Limit

01:00:57 HOL-Probability: theory Distributions

01:00:57 HOL-Probability: theory Stream_Space

01:00:58 HOL-Probability: theory Characteristic_Functions

01:00:58 HOL-Probability: theory Sinc_Integral

01:00:59 HOL-Probability: theory Levy

01:01:00 HOL-Probability: theory Central_Limit_Theorem

01:01:01 HOL-Probability: theory Probability

01:04:13 Timing HOL-Probability (2 threads, 175.817s elapsed time, 314.624s cpu time, 10.904s GC time, factor 1.79)

01:04:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

01:04:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

01:04:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

01:04:13 Finished HOL-Probability (0:03:56 elapsed time, 0:06:45 cpu time, factor 1.72)

01:04:14 Running HOL-Codegenerator_Test ...

01:04:20 HOL-Codegenerator_Test: theory Code_Test_PolyML

01:04:20 HOL-Codegenerator_Test: theory Cmp

01:04:20 HOL-Codegenerator_Test: theory Code_Test_Scala

01:04:21 HOL-Codegenerator_Test: theory Primes

01:04:21 HOL-Codegenerator_Test: theory Less_False

01:04:21 HOL-Codegenerator_Test: theory Sorted_Less

01:04:21 HOL-Codegenerator_Test: theory AList_Upd_Del

01:04:21 HOL-Codegenerator_Test: theory Eratosthenes

01:04:22 HOL-Codegenerator_Test: theory Map_by_Ordered

01:04:22 HOL-Codegenerator_Test: theory List_Ins_Del

01:04:22 HOL-Codegenerator_Test: theory Records

01:04:23 HOL-Codegenerator_Test: theory Set_by_Ordered

01:04:23 HOL-Codegenerator_Test: theory Tree_Set

01:04:24 HOL-Codegenerator_Test: theory Tree_Map

01:04:27 HOL-Codegenerator_Test: theory Candidates

01:04:30 HOL-Codegenerator_Test: theory Generate

01:04:31 HOL-Codegenerator_Test: theory Generate_Binary_Nat

01:07:19 Timing HOL-Data_Structures (2 threads, 762.220s elapsed time, 1069.548s cpu time, 58.624s GC time, factor 1.40)

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

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

01:07:19 Finished HOL-Data_Structures (0:12:47 elapsed time, 0:17:54 cpu time, factor 1.40)

01:07:19 Running HOL-ex ...

01:07:21 HOL-ex: theory Adhoc_Overloading

01:07:21 HOL-ex: theory Computations

01:07:21 HOL-ex: theory Cartouche_Examples

01:07:22 HOL-ex: theory Chinese

01:07:22 HOL-ex: theory Code_Abstract_Nat

01:07:22 HOL-ex: theory Code_Binary_Nat

01:07:22 HOL-ex: theory FuncSet

01:07:23 HOL-ex: theory Hebrew

01:07:23 HOL-ex: theory Monad_Syntax

01:07:23 HOL-ex: theory Refute

01:07:24 HOL-ex: theory Serbian

01:07:25 HOL-ex: theory State_Monad

01:07:26 HOL-ex: theory Code_Binary_Nat_examples

01:07:26 HOL-ex: theory Eval_Examples

01:07:29 HOL-ex: theory Normalization_by_Evaluation

01:07:30 HOL-ex: theory Transitive_Closure_Table

01:07:55 HOL-ex: theory Groebner_Examples

01:07:55 HOL-ex: theory PresburgerEx

01:07:55 HOL-ex: theory AList

01:07:55 HOL-ex: theory Antiquote

01:07:55 HOL-ex: theory Arith_Examples

01:07:55 HOL-ex: theory CTL

01:07:55 HOL-ex: theory Cancellation

01:07:56 HOL-ex: theory Multiset

01:07:56 HOL-ex: theory Classical

01:07:59 HOL-ex: theory Code_Target_Nat

01:08:00 HOL-ex: theory Coercion_Examples

01:08:00 HOL-ex: theory Coherent

01:08:00 HOL-ex: theory Commands

01:08:00 HOL-ex: theory Debug

01:08:00 HOL-ex: theory Dlist

01:08:01 HOL-ex: theory Bubblesort

01:08:01 HOL-ex: theory MergeSort

01:08:02 HOL-ex: theory Quicksort

01:08:02 HOL-ex: theory Erdoes_Szekeres

01:08:02 HOL-ex: theory Executable_Relation

01:08:03 HOL-ex: theory FSet

01:08:03 HOL-ex: theory Birthday_Paradox

01:08:03 HOL-ex: theory Code_Target_Int

01:08:03 HOL-ex: theory Code_Target_Numeral

01:08:03 HOL-ex: theory Factorial_Ring

01:08:06 HOL-ex: theory Transfer_Int_Nat

01:08:07 HOL-ex: theory Guess

01:08:07 HOL-ex: theory Hex_Bin_Examples

01:08:07 HOL-ex: theory IArray

01:08:08 HOL-ex: theory IArray_Examples

01:08:09 HOL-ex: theory Iff_Oracle

01:08:09 HOL-ex: theory Induction_Schema

01:08:09 HOL-ex: theory Infinite_Set

01:08:09 HOL-ex: theory Adhoc_Overloading_Examples

01:08:11 HOL-ex: theory Intuitionistic

01:08:11 HOL-ex: theory LaTeXsugar

01:08:11 HOL-ex: theory Lagrange

01:08:11 HOL-ex: theory List_to_Set_Comprehension_Examples

01:08:12 HOL-ex: theory LocaleTest2

01:08:12 HOL-ex: theory ML

01:08:13 HOL-ex: theory Euclidean_Algorithm

01:08:14 HOL-ex: theory Mapping

01:08:15 HOL-ex: theory AList_Mapping

01:08:15 HOL-ex: theory Execute_Choice

01:08:15 HOL-ex: theory Functions

01:08:24 HOL-ex: theory Primes

01:08:25 HOL-ex: theory MonoidGroup

01:08:26 HOL-ex: theory Eratosthenes

01:08:27 HOL-ex: theory Multiquote

01:08:27 HOL-ex: theory NatSum

01:08:27 HOL-ex: theory Code_Timing

01:08:28 HOL-ex: theory PER

01:08:29 HOL-ex: theory Parallel

01:08:31 HOL-ex: theory Peano_Axioms

01:08:31 HOL-ex: theory Perm

01:08:32 HOL-ex: theory Phantom_Type

01:08:34 HOL-ex: theory Cardinality

01:08:34 HOL-ex: theory Perm_Fragments

01:08:35 HOL-ex: theory Primrec

01:08:36 HOL-ex: theory Records

01:08:36 HOL-ex: theory Numeral_Type

01:08:39 HOL-ex: theory Type_Length

01:08:39 HOL-ex: theory Reflection

01:08:39 HOL-ex: theory Refute_Examples

01:08:45 HOL-ex: theory Rewrite

01:08:45 HOL-ex: theory SAT_Examples

01:08:46 HOL-ex: theory Rewrite_Examples

01:08:47 HOL-ex: theory Seq

01:08:47 HOL-ex: theory Set_Comprehension_Pointfree_Examples

01:08:48 HOL-ex: theory Set_Theory

01:08:48 HOL-ex: theory Simproc_Tests

01:08:49 HOL-ex: theory Simps_Case_Conv

01:08:49 HOL-ex: theory Simps_Case_Conv_Examples

01:08:50 HOL-ex: theory Sudoku

01:08:53 HOL-ex: theory Tarski

01:08:57 HOL-ex: theory Termination

01:09:00 HOL-ex: theory ThreeDivides

01:09:00 HOL-ex: theory Argo_Examples

01:09:03 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures

01:09:05 HOL-ex: theory Ballot

01:09:06 HOL-ex: theory BinEx

01:09:09 HOL-ex: theory Cubic_Quartic

01:09:10 HOL-ex: theory Dedekind_Real

01:09:10 HOL-ex: theory Gauge_Integration

01:09:10 HOL-ex: theory HarmonicSeries

01:09:11 HOL-ex: theory Parallel_Example

01:09:12 HOL-ex: theory Pythagoras

01:09:12 HOL-ex: theory Reflection_Examples

01:09:13 HOL-ex: theory Sqrt

01:09:13 HOL-ex: theory Sqrt_Script

01:09:14 HOL-Codegenerator_Test: theory Generate_Pretty_Char

01:09:14 HOL-ex: theory Sum_of_Powers

01:09:15 HOL-ex: theory Sum_of_Squares

01:09:18 HOL-ex: theory SOS

01:09:18 HOL-ex: theory SOS_Cert

01:09:18 HOL-ex: theory Transfer_Debug

01:09:18 HOL-ex: theory Transfer_Ex

01:09:19 HOL-ex: theory Transitive_Closure_Table_Ex

01:09:19 HOL-ex: theory Tree23

01:09:25 HOL-Nominal-Examples: theory VC_Condition

01:09:28 Timing HOL-Nominal-Examples (2 threads, 897.037s elapsed time, 1549.556s cpu time, 125.580s GC time, factor 1.73)

01:09:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples

01:09:28 Finished HOL-Nominal-Examples (0:14:59 elapsed time, 0:25:52 cpu time, factor 1.73)

01:09:28 Running HOL-Decision_Procs ...

01:09:30 HOL-Decision_Procs: theory Code_Abstract_Nat