20:59:20 Started by upstream project "isabelle-repo" build number 1276

20:59:20 originally caused by:

20:59:20 Started by an SCM change

20:59:20 [EnvInject] - Loading node environment variables.

20:59:20 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

20:59:20 [isabelle-repo-makeall] $ hg showconfig paths.default

20:59:20 [isabelle-repo-makeall] $ hg pull --rev 978c584609ded0d1a36246b83aeb8630d14034f9

20:59:20 pulling from http://isabelle.in.tum.de/repos/isabelle/

20:59:20 searching for changes

20:59:20 adding changesets

20:59:20 adding manifests

20:59:20 adding file changes

20:59:20 added 1 changesets with 1 changes to 1 files

20:59:20 (run 'hg update' to get a working copy)

20:59:20 [isabelle-repo-makeall] $ hg update --clean --rev 978c584609ded0d1a36246b83aeb8630d14034f9

20:59:20 1 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

20:59:20 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

20:59:20 [isabelle-repo-makeall] $ hg id --branch

20:59:21 No emails were triggered.

20:59:21 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/jenkins3354187583624592740.sh

20:59:21 + Admin/jenkins/run_build makeall

20:59:21 + set -e

20:59:21 + PROFILE=makeall

20:59:21 + shift

20:59:21 + bin/isabelle components -a

20:59:21 + bin/isabelle jedit -bf

20:59:22 ### Building Isabelle/Scala ...

20:59:49 ### Building Isabelle/jEdit ...

21:00:05 + bin/isabelle ci_build_makeall

21:00:09

21:00:09 === CONFIGURATION ===

21:00:09

21:00:09 ISABELLE_BUILD_OPTIONS=""

21:00:09

21:00:09 ML_PLATFORM="x86_64-linux"

21:00:09 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"

21:00:09 ML_SYSTEM="polyml-5.7.1"

21:00:09 ML_OPTIONS="-H 4000 --maxheap 8G"

21:00:10

21:00:10 === BUILD ===

21:00:10

21:00:10 Build started at Sat, 4 Nov 2017 20:00:09 GMT

21:00:10 Isabelle id 978c584609de

21:00:10

21:00:10 === LOG ===

21:00:10

21:00:10 Session Pure/Pure

21:00:10 Session CTT/CTT

21:00:10 Session Cube/Cube

21:00:10 Session FOL/FOL

21:00:10 Session CCL/CCL

21:00:10 Session FOL/FOL-ex

21:00:11 Session FOLP/FOLP

21:00:11 Session FOLP/FOLP-ex

21:00:11 Session HOL/HOL (main)

21:00:11 Session Doc/Classes (doc)

21:00:11 Session Doc/Functions (doc)

21:00:11 Session HOL/HOL-Eisbach

21:00:11 Session Doc/Eisbach (doc)

21:00:11 Session HOL/HOL-Hoare

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

21:00:12 Session HOL/HOL-IMPP

21:00:12 Session HOL/HOL-IOA

21:00:12 Session HOL/HOL-Import

21:00:12 Session HOL/HOL-Lattice

21:00:12 Session HOL/HOL-Library (main timing)

21:00:12 Session Doc/Codegen_Basics

21:00:12 Session Doc/Codegen (doc)

21:00:12 Session Doc/Datatypes (doc)

21:00:12 Session Doc/Corec (doc)

21:00:12 Session HOL/HOL-Auth (timing)

21:00:12 Session HOL/HOL-UNITY (timing)

21:00:13 Session HOL/HOL-Bali (timing)

21:00:13 Session HOL/HOL-Cardinals (timing)

21:00:13 Session HOL/HOL-Computational_Algebra (timing)

21:00:13 Session HOL/HOL-Algebra (main timing)

21:00:13 Session HOL/HOL-Decision_Procs (timing)

21:00:13 Session HOL/HOL-Quotient_Examples (timing)

21:00:14 Session HOL/HOL-Analysis (main timing)

21:00:14 Session HOL/HOL-Analysis-ex

21:00:14 Session HOL/HOL-Probability (main timing)

21:00:14 Session HOL/HOL-Probability-ex (timing)

21:00:15 Session HOL/HOL-Isar_Examples

21:00:15 Session HOL/HOL-Nonstandard_Analysis (timing)

21:00:15 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

21:00:15 Session HOL/HOL-Number_Theory (timing)

21:00:15 Session HOL/HOL-Data_Structures (timing)

21:00:15 Session HOL/HOL-ex (timing)

21:00:16 Session HOL/HOL-Codegenerator_Test

21:00:16 Session HOL/HOL-Corec_Examples (timing)

21:00:16 Session HOL/HOL-Datatype_Examples (timing)

21:00:16 Session HOL/HOL-Hahn_Banach

21:00:16 Session HOL/HOL-IMP (timing)

21:00:16 Session HOL/HOL-Imperative_HOL (timing)

21:00:16 Session HOL/HOL-Induct

21:00:16 Session HOL/HOL-Matrix_LP

21:00:16 Session HOL/HOL-Metis_Examples (timing)

21:00:16 Session HOL/HOL-MicroJava (timing)

21:00:17 Session HOL/HOL-Mutabelle

21:00:17 Session HOL/HOL-Nitpick_Examples

21:00:17 Session HOL/HOL-Nominal

21:00:17 Session HOL/HOL-Nominal-Examples (timing)

21:00:17 Session HOL/HOL-Predicate_Compile_Examples (timing)

21:00:17 Session HOL/HOL-Quickcheck_Examples (timing)

21:00:17 Session HOL/HOL-SET_Protocol (timing)

21:00:17 Session HOL/HOL-TPTP

21:00:17 Session HOL/HOL-Unix

21:00:17 Session HOL/HOL-ZF

21:00:17 Session Doc/Isar_Ref (doc)

21:00:17 Session Doc/Typeclass_Hierarchy_Basics

21:00:17 Session Doc/Typeclass_Hierarchy (doc)

21:00:18 Session HOL/HOL-Mirabelle

21:00:18 Session HOL/HOL-Mirabelle-ex

21:00:18 Session HOL/HOL-NanoJava

21:00:18 Session HOL/HOL-Prolog

21:00:18 Session HOL/HOL-Statespace

21:00:18 Session HOL/HOL-TLA

21:00:18 Session HOL/HOL-TLA-Buffer

21:00:18 Session HOL/HOL-TLA-Inc

21:00:18 Session HOL/HOL-TLA-Memory

21:00:18 Session HOL/HOL-Types_To_Sets

21:00:18 Session HOL/HOL-Word (main timing)

21:00:18 Session HOL/HOL-SPARK (main)

21:00:18 Session HOL/HOL-SPARK-Examples

21:00:18 Session HOL/HOL-SPARK-Manual

21:00:18 Session HOL/HOL-Word-Examples

21:00:18 Session HOL/HOL-Word-SMT_Examples (timing)

21:00:18 Session HOL/HOLCF (main timing)

21:00:19 Session HOL/HOLCF-IMP

21:00:19 Session HOL/HOLCF-Library

21:00:19 Session HOL/HOLCF-FOCUS

21:00:19 Session HOL/HOLCF-ex

21:00:19 Session HOL/HOLCF-Tutorial

21:00:19 Session HOL/IOA (timing)

21:00:19 Session HOL/IOA-ABP

21:00:19 Session HOL/IOA-NTP

21:00:19 Session HOL/IOA-Storage

21:00:19 Session HOL/IOA-ex

21:00:19 Session Doc/How_to_Prove_it

21:00:19 Session Doc/Implementation (doc)

21:00:19 Session Doc/JEdit (doc)

21:00:19 Session Doc/Locales (doc)

21:00:19 Session Doc/Main (doc)

21:00:19 Session Doc/Prog_Prove (doc)

21:00:19 Session Doc/Sugar (doc)

21:00:20 Session Doc/Tutorial (doc)

21:00:20 Session HOL/HOL-Proofs (timing)

21:00:20 Session HOL/HOL-Proofs-Extraction (timing)

21:00:20 Session HOL/HOL-Proofs-Lambda (timing)

21:00:20 Session HOL/HOL-Proofs-ex

21:00:20 Session Doc/Intro (doc)

21:00:20 Session LCF/LCF

21:00:20 Session Doc/Logics (doc)

21:00:20 Session Doc/Nitpick (doc)

21:00:20 Session Unsorted/SML

21:00:20 Session Sequents/Sequents

21:00:20 Session Doc/Sledgehammer (doc)

21:00:20 Session Unsorted/Spec_Check

21:00:20 Session Doc/System (doc)

21:00:20 Session ZF/ZF (main timing)

21:00:20 Session Doc/Logics_ZF (doc)

21:00:20 Session ZF/ZF-AC

21:00:20 Session ZF/ZF-Coind

21:00:20 Session ZF/ZF-Constructible

21:00:21 Session ZF/ZF-IMP

21:00:21 Session ZF/ZF-Induct

21:00:21 Session ZF/ZF-UNITY (timing)

21:00:21 Session ZF/ZF-Resid

21:00:21 Session ZF/ZF-ex

21:00:22 Cleaning Pure ...

21:00:22 Cleaning SML ...

21:00:22 Cleaning Sequents ...

21:00:22 Cleaning Sledgehammer ...

21:00:22 Cleaning Spec_Check ...

21:00:22 Cleaning System ...

21:00:22 Cleaning ZF ...

21:00:22 Cleaning ZF-AC ...

21:00:22 Cleaning ZF-Coind ...

21:00:22 Cleaning ZF-Constructible ...

21:00:22 Cleaning ZF-IMP ...

21:00:22 Cleaning ZF-Induct ...

21:00:22 Cleaning ZF-UNITY ...

21:00:22 Cleaning ZF-Resid ...

21:00:22 Cleaning ZF-ex ...

21:00:22 Cleaning Nitpick ...

21:00:22 Cleaning Logics_ZF ...

21:00:22 Cleaning Logics ...

21:00:22 Cleaning LCF ...

21:00:22 Cleaning Intro ...

21:00:22 Cleaning HOL-Proofs ...

21:00:22 Cleaning HOL-Proofs-Extraction ...

21:00:22 Cleaning HOL-Proofs-Lambda ...

21:00:22 Cleaning HOL-Proofs-ex ...

21:00:22 Cleaning HOL ...

21:00:22 Cleaning HOL-Analysis ...

21:00:22 Cleaning HOL-Analysis-ex ...

21:00:22 Cleaning HOL-Probability ...

21:00:22 Cleaning HOL-Probability-ex ...

21:00:22 Cleaning HOL-Data_Structures ...

21:00:22 Cleaning HOL-Eisbach ...

21:00:22 Cleaning HOL-Hoare ...

21:00:22 Cleaning HOL-Hoare_Parallel ...

21:00:22 Cleaning HOL-IMPP ...

21:00:22 Cleaning HOL-IOA ...

21:00:22 Cleaning HOL-Import ...

21:00:22 Cleaning HOL-Lattice ...

21:00:22 Cleaning HOL-Library ...

21:00:22 Cleaning HOL-Auth ...

21:00:22 Cleaning HOL-UNITY ...

21:00:22 Cleaning HOL-Bali ...

21:00:22 Cleaning HOL-Cardinals ...

21:00:22 Cleaning HOL-Computational_Algebra ...

21:00:22 Cleaning HOL-Algebra ...

21:00:22 Cleaning HOL-Decision_Procs ...

21:00:22 Cleaning HOL-Quotient_Examples ...

21:00:22 Cleaning HOL-Isar_Examples ...

21:00:22 Cleaning HOL-Nonstandard_Analysis ...

21:00:22 Cleaning HOL-Nonstandard_Analysis-Examples ...

21:00:22 Cleaning HOL-Number_Theory ...

21:00:22 Cleaning HOL-Codegenerator_Test ...

21:00:22 Cleaning HOL-ex ...

21:00:22 Cleaning HOL-Corec_Examples ...

21:00:22 Cleaning HOL-Datatype_Examples ...

21:00:22 Cleaning HOL-Hahn_Banach ...

21:00:22 Cleaning HOL-IMP ...

21:00:22 Cleaning HOL-Imperative_HOL ...

21:00:22 Cleaning HOL-Induct ...

21:00:22 Cleaning HOL-Matrix_LP ...

21:00:22 Cleaning HOL-Metis_Examples ...

21:00:22 Cleaning HOL-MicroJava ...

21:00:22 Cleaning HOL-Mutabelle ...

21:00:22 Cleaning HOL-Nitpick_Examples ...

21:00:22 Cleaning HOL-Nominal ...

21:00:22 Cleaning HOL-Nominal-Examples ...

21:00:22 Cleaning HOL-Predicate_Compile_Examples ...

21:00:22 Cleaning HOL-Quickcheck_Examples ...

21:00:22 Cleaning HOL-SET_Protocol ...

21:00:22 Cleaning HOL-TPTP ...

21:00:22 Cleaning HOL-Unix ...

21:00:22 Cleaning HOL-ZF ...

21:00:22 Cleaning Isar_Ref ...

21:00:22 Cleaning Typeclass_Hierarchy_Basics ...

21:00:22 Cleaning Typeclass_Hierarchy ...

21:00:22 Cleaning HOL-Mirabelle ...

21:00:22 Cleaning HOL-Mirabelle-ex ...

21:00:22 Cleaning HOL-NanoJava ...

21:00:22 Cleaning HOL-Prolog ...

21:00:22 Cleaning HOL-Statespace ...

21:00:22 Cleaning HOL-TLA ...

21:00:22 Cleaning HOL-TLA-Buffer ...

21:00:22 Cleaning HOL-TLA-Inc ...

21:00:22 Cleaning HOL-TLA-Memory ...

21:00:22 Cleaning HOL-Types_To_Sets ...

21:00:22 Cleaning HOL-Word ...

21:00:22 Cleaning HOL-SPARK ...

21:00:22 Cleaning HOL-SPARK-Examples ...

21:00:22 Cleaning HOL-SPARK-Manual ...

21:00:22 Cleaning HOL-Word-Examples ...

21:00:22 Cleaning HOL-Word-SMT_Examples ...

21:00:22 Cleaning HOLCF ...

21:00:22 Cleaning HOLCF-IMP ...

21:00:22 Cleaning HOLCF-Library ...

21:00:22 Cleaning HOLCF-FOCUS ...

21:00:22 Cleaning HOLCF-ex ...

21:00:22 Cleaning HOLCF-Tutorial ...

21:00:22 Cleaning IOA ...

21:00:22 Cleaning IOA-ABP ...

21:00:22 Cleaning IOA-NTP ...

21:00:22 Cleaning IOA-Storage ...

21:00:22 Cleaning IOA-ex ...

21:00:22 Cleaning How_to_Prove_it ...

21:00:22 Cleaning Implementation ...

21:00:22 Cleaning JEdit ...

21:00:22 Cleaning Locales ...

21:00:22 Cleaning Main ...

21:00:22 Cleaning Prog_Prove ...

21:00:22 Cleaning Sugar ...

21:00:22 Cleaning Tutorial ...

21:00:22 Cleaning Functions ...

21:00:22 Cleaning FOLP ...

21:00:22 Cleaning FOLP-ex ...

21:00:22 Cleaning FOL ...

21:00:22 Cleaning FOL-ex ...

21:00:22 Cleaning Eisbach ...

21:00:22 Cleaning Datatypes ...

21:00:22 Cleaning Cube ...

21:00:22 Cleaning Corec ...

21:00:23 Cleaning Codegen_Basics ...

21:00:23 Cleaning Codegen ...

21:00:23 Cleaning Classes ...

21:00:23 Cleaning CTT ...

21:00:23 Cleaning CCL ...

21:00:23 Building Pure ...

21:00:37 Pure: theory Pure

21:00:38 Pure: theory ML_Bootstrap

21:00:41 Timing Pure (1 threads, 0.717s elapsed time, 0.720s cpu time, 0.000s GC time, factor 1.00)

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

21:00:41 Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.97)

21:00:41 Building HOL ...

21:00:41 Building ZF ...

21:00:41 Building HOL-Proofs ...

21:00:41 ZF: theory IFOL

21:00:42 HOL-Proofs: theory HOL.Code_Generator

21:00:42 HOL: theory HOL.Code_Generator

21:00:42 ZF: theory FOL

21:00:44 ZF: theory ZF.ZF_Base

21:00:45 ZF: theory ZF.upair

21:00:45 ZF: theory ZF.pair

21:00:45 HOL-Proofs: theory HOL.HOL

21:00:45 ZF: theory ZF.Bool

21:00:45 ZF: theory ZF.equalities

21:00:45 HOL: theory HOL.HOL

21:00:46 ZF: theory ZF.Sum

21:00:46 ZF: theory ZF.Fixedpt

21:00:46 ZF: theory ZF.func

21:00:47 ZF: theory ZF.Perm

21:00:47 ZF: theory ZF.QPair

21:00:47 ZF: theory ZF.Trancl

21:00:47 ZF: theory ZF.EquivClass

21:00:47 ZF: theory ZF.WF

21:00:47 ZF: theory ZF.Order

21:00:47 ZF: theory ZF.Ordinal

21:00:47 ZF: theory ZF.OrdQuant

21:00:47 ZF: theory ZF.OrderArith

21:00:48 ZF: theory ZF.Nat_ZF

21:00:48 ZF: theory ZF.Epsilon

21:00:48 ZF: theory ZF.OrderType

21:00:48 ZF: theory ZF.Inductive_ZF

21:00:49 ZF: theory ZF.Finite

21:00:49 ZF: theory ZF.Cardinal

21:00:49 HOL: theory HOL.Argo

21:00:49 HOL: theory HOL.Ctr_Sugar

21:00:49 ZF: theory ZF.Univ

21:00:50 HOL-Proofs: theory HOL.Argo

21:00:50 HOL-Proofs: theory HOL.Ctr_Sugar

21:00:50 ZF: theory ZF.Arith

21:00:50 ZF: theory ZF.QUniv

21:00:50 ZF: theory ZF.Datatype_ZF

21:00:50 ZF: theory ZF.ArithSimp

21:00:50 ZF: theory ZF.Int_ZF

21:00:50 ZF: theory ZF.CardinalArith

21:00:51 HOL: theory HOL.Orderings

21:00:51 ZF: theory ZF.List_ZF

21:00:51 HOL-Proofs: theory HOL.Orderings

21:00:51 HOL: theory HOL.SAT

21:00:51 ZF: theory ZF.Bin

21:00:51 HOL-Proofs: theory HOL.SAT

21:00:52 ZF: theory ZF.IntDiv_ZF

21:00:52 HOL: theory HOL.Groups

21:00:53 ZF: theory ZF

21:00:53 ZF: theory ZF.AC

21:00:53 ZF: theory ZF.Zorn

21:00:53 ZF: theory ZF.Cardinal_AC

21:00:53 ZF: theory ZF.InfDatatype

21:00:53 ZF: theory ZFC

21:00:53 HOL-Proofs: theory HOL.Groups

21:00:55 HOL: theory HOL.Lattices

21:00:58 HOL: theory HOL.Set

21:00:58 HOL-Proofs: theory HOL.Lattices

21:00:59 HOL: theory HOL.Fun

21:00:59 HOL: theory HOL.Typedef

21:01:00 HOL: theory HOL.Rings

21:01:00 HOL: theory HOL.Complete_Lattices

21:01:01 HOL-Proofs: theory HOL.Set

21:01:02 HOL: theory HOL.Inductive

21:01:04 HOL: theory HOL.Product_Type

21:01:06 HOL: theory HOL.Complete_Partial_Order

21:01:06 HOL: theory HOL.Sum_Type

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

21:01:07 HOL-Proofs: theory HOL.Typedef

21:01:07 HOL-Proofs: theory HOL.Rings

21:01:09 HOL-Proofs: theory HOL.Complete_Lattices

21:01:11 HOL: theory HOL.Nat

21:01:13 HOL: theory HOL.Fields

21:01:13 HOL: theory HOL.Meson

21:01:14 HOL: theory HOL.ATP

21:01:15 HOL-Proofs: theory HOL.Inductive

21:01:17 Timing ZF (2 threads, 23.448s elapsed time, 38.000s cpu time, 2.268s GC time, factor 1.62)

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

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

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

21:01:17 Finished ZF (0:00:35 elapsed time, 0:00:56 cpu time, factor 1.60)

21:01:17 Building ZF-Induct ...

21:01:17 ZF-Induct: theory ZF-Induct.Acc

21:01:17 ZF-Induct: theory ZF-Induct.Binary_Trees

21:01:17 ZF-Induct: theory ZF-Induct.Comb

21:01:17 HOL: theory HOL.Metis

21:01:17 ZF-Induct: theory ZF-Induct.Datatypes

21:01:18 ZF-Induct: theory ZF-Induct.FoldSet

21:01:18 ZF-Induct: theory ZF-Induct.ListN

21:01:18 ZF-Induct: theory ZF-Induct.Mutil

21:01:18 HOL-Proofs: theory HOL.Product_Type

21:01:18 ZF-Induct: theory ZF-Induct.Ntree

21:01:18 ZF-Induct: theory ZF-Induct.Multiset

21:01:18 ZF-Induct: theory ZF-Induct.Primrec

21:01:18 ZF-Induct: theory ZF-Induct.PropLog

21:01:19 ZF-Induct: theory ZF-Induct.Rmap

21:01:19 ZF-Induct: theory ZF-Induct.Term

21:01:19 ZF-Induct: theory ZF-Induct.Tree_Forest

21:01:19 ZF-Induct: theory ZF-Induct.Brouwer

21:01:20 HOL: theory HOL.Finite_Set

21:01:21 HOL-Proofs: theory HOL.Complete_Partial_Order

21:01:22 HOL: theory HOL.Relation

21:01:22 HOL-Proofs: theory HOL.Sum_Type

21:01:23 HOL: theory HOL.Transitive_Closure

21:01:25 HOL: theory HOL.Wellfounded

21:01:26 HOL: theory HOL.Fun_Def_Base

21:01:26 HOL: theory HOL.Hilbert_Choice

21:01:26 HOL: theory HOL.Wfrec

21:01:26 HOL: theory HOL.Order_Relation

21:01:27 HOL: theory HOL.BNF_Wellorder_Relation

21:01:27 HOL: theory HOL.Zorn

21:01:27 HOL: theory HOL.BNF_Wellorder_Embedding

21:01:27 HOL-Proofs: theory HOL.Nat

21:01:27 HOL: theory HOL.BNF_Wellorder_Constructions

21:01:28 HOL: theory HOL.BNF_Cardinal_Order_Relation

21:01:29 HOL: theory HOL.BNF_Cardinal_Arithmetic

21:01:30 HOL: theory HOL.BNF_Def

21:01:32 Timing ZF-Induct (2 threads, 8.296s elapsed time, 13.160s cpu time, 0.548s GC time, factor 1.59)

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

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

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

21:01:32 Finished ZF-Induct (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.53)

21:01:32 Building FOL ...

21:01:32 FOL: theory IFOL

21:01:32 HOL-Proofs: theory HOL.Fields

21:01:32 HOL-Proofs: theory HOL.Meson

21:01:33 FOL: theory FOL

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

21:01:33 HOL: theory HOL.BNF_Composition

21:01:33 HOL: theory HOL.Basic_BNFs

21:01:34 HOL: theory HOL.BNF_Fixpoint_Base

21:01:36 HOL-Proofs: theory HOL.Metis

21:01:38 Timing FOL (2 threads, 3.487s elapsed time, 3.864s cpu time, 0.164s GC time, factor 1.11)

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

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

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

21:01:38 Finished FOL (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16)

21:01:38 Building FOLP ...

21:01:38 FOLP: theory IFOLP

21:01:39 HOL: theory HOL.BNF_Least_Fixpoint

21:01:39 FOLP: theory FOLP

21:01:41 Timing FOLP (2 threads, 1.245s elapsed time, 1.248s cpu time, 0.000s GC time, factor 1.00)

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

21:01:41 Finished FOLP (0:00:02 elapsed time)

21:01:41 Running ZF-Constructible ...

21:01:41 ZF-Constructible: theory ZF-Constructible.Formula

21:01:41 ZF-Constructible: theory ZF-Constructible.MetaExists

21:01:41 ZF-Constructible: theory ZF-Constructible.Normal

21:01:41 ZF-Constructible: theory ZF-Constructible.Reflection

21:01:42 HOL-Proofs: theory HOL.Finite_Set

21:01:42 ZF-Constructible: theory ZF-Constructible.Relative

21:01:42 HOL: theory HOL.Basic_BNF_LFPs

21:01:43 HOL: theory HOL.Transfer

21:01:44 HOL: theory HOL.Num

21:01:44 ZF-Constructible: theory ZF-Constructible.L_axioms

21:01:44 ZF-Constructible: theory ZF-Constructible.Wellorderings

21:01:45 ZF-Constructible: theory ZF-Constructible.WFrec

21:01:45 ZF-Constructible: theory ZF-Constructible.WF_absolute

21:01:46 ZF-Constructible: theory ZF-Constructible.Datatype_absolute

21:01:46 ZF-Constructible: theory ZF-Constructible.Rank

21:01:48 ZF-Constructible: theory ZF-Constructible.Separation

21:01:48 ZF-Constructible: theory ZF-Constructible.Internalize

21:01:48 HOL: theory HOL.Power

21:01:48 ZF-Constructible: theory ZF-Constructible.AC_in_L

21:01:50 ZF-Constructible: theory ZF-Constructible.Rec_Separation

21:01:50 ZF-Constructible: theory ZF-Constructible.Rank_Separation

21:01:50 ZF-Constructible: theory ZF-Constructible.Satisfies_absolute

21:01:51 ZF-Constructible: theory ZF-Constructible.DPow_absolute

21:01:51 HOL-Proofs: theory HOL.Relation

21:01:51 HOL: theory HOL.Groups_Big

21:01:55 HOL: theory HOL.Equiv_Relations

21:01:55 HOL-Proofs: theory HOL.Transitive_Closure

21:01:55 HOL: theory HOL.Lifting

21:01:57 HOL: theory HOL.Lifting_Set

21:01:57 HOL: theory HOL.Option

21:01:57 HOL: theory HOL.Quotient

21:01:58 HOL: theory HOL.Extraction

21:01:59 HOL: theory HOL.Lattices_Big

21:02:00 HOL-Proofs: theory HOL.Wellfounded

21:02:01 HOL: theory HOL.Partial_Function

21:02:02 HOL: theory HOL.Fun_Def

21:02:03 HOL-Proofs: theory HOL.Fun_Def_Base

21:02:03 HOL: theory HOL.Int

21:02:03 HOL-Proofs: theory HOL.Hilbert_Choice

21:02:05 Timing ZF-Constructible (2 threads, 18.781s elapsed time, 35.964s cpu time, 6.792s GC time, factor 1.91)

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

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

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

21:02:05 Finished ZF-Constructible (0:00:23 elapsed time, 0:00:43 cpu time, factor 1.83)

21:02:05 Running ZF-UNITY ...

21:02:05 ZF-UNITY: theory ZF-UNITY.MultisetSum

21:02:05 ZF-UNITY: theory ZF-UNITY.GenPrefix

21:02:06 ZF-UNITY: theory ZF-UNITY.State

21:02:06 ZF-UNITY: theory ZF-UNITY.UNITY

21:02:06 ZF-UNITY: theory ZF-UNITY.Monotonicity

21:02:06 ZF-UNITY: theory ZF-UNITY.Constrains

21:02:06 ZF-UNITY: theory ZF-UNITY.FP

21:02:06 ZF-UNITY: theory ZF-UNITY.WFair

21:02:06 HOL-Proofs: theory HOL.Wfrec

21:02:07 ZF-UNITY: theory ZF-UNITY.Increasing

21:02:07 HOL-Proofs: theory HOL.Order_Relation

21:02:07 ZF-UNITY: theory ZF-UNITY.SubstAx

21:02:07 HOL: theory HOL.Euclidean_Division

21:02:07 ZF-UNITY: theory ZF-UNITY.Follows

21:02:07 ZF-UNITY: theory ZF-UNITY.Mutex

21:02:08 ZF-UNITY: theory ZF-UNITY.Union

21:02:08 HOL-Proofs: theory HOL.BNF_Wellorder_Relation

21:02:08 HOL-Proofs: theory HOL.Zorn

21:02:08 ZF-UNITY: theory ZF-UNITY.Comp

21:02:08 ZF-UNITY: theory ZF-UNITY.Guar

21:02:09 ZF-UNITY: theory ZF-UNITY.AllocBase

21:02:09 ZF-UNITY: theory ZF-UNITY.ClientImpl

21:02:09 ZF-UNITY: theory ZF-UNITY.Distributor

21:02:09 ZF-UNITY: theory ZF-UNITY.Merge

21:02:09 ZF-UNITY: theory ZF-UNITY.AllocImpl

21:02:10 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding

21:02:12 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions

21:02:15 HOL: theory HOL.Parity

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

21:02:19 HOL: theory HOL.Divides

21:02:23 HOL: theory HOL.Code_Numeral

21:02:23 HOL: theory HOL.Numeral_Simprocs

21:02:24 HOL: theory HOL.SMT

21:02:24 HOL: theory HOL.Semiring_Normalization

21:02:25 Timing ZF-UNITY (2 threads, 18.680s elapsed time, 33.948s cpu time, 1.268s GC time, factor 1.82)

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

21:02:25 Finished ZF-UNITY (0:00:19 elapsed time, 0:00:34 cpu time, factor 1.75)

21:02:25 Running ZF-ex ...

21:02:25 ZF-ex: theory ZF-ex.BinEx

21:02:25 ZF-ex: theory ZF-ex.CoUnit

21:02:25 ZF-ex: theory ZF-ex.Commutation

21:02:25 ZF-ex: theory ZF-ex.Group

21:02:26 ZF-ex: theory ZF-ex.LList

21:02:26 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic

21:02:26 ZF-ex: theory ZF-ex.Limit

21:02:27 HOL: theory HOL.Set_Interval

21:02:27 ZF-ex: theory ZF-ex.Ring

21:02:27 HOL: theory HOL.Groebner_Basis

21:02:27 ZF-ex: theory ZF-ex.NatSum

21:02:27 ZF-ex: theory ZF-ex.Primes

21:02:27 ZF-ex: theory ZF-ex.Ramsey

21:02:28 ZF-ex: theory ZF-ex.misc

21:02:28 HOL-Proofs: theory HOL.BNF_Def

21:02:31 HOL: theory HOL.Conditionally_Complete_Lattices

21:02:31 HOL: theory HOL.Filter

21:02:32 HOL-Proofs: theory HOL.BNF_Composition

21:02:33 HOL-Proofs: theory HOL.Basic_BNFs

21:02:33 HOL: theory HOL.Presburger

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

21:02:37 HOL: theory HOL.Sledgehammer

21:02:40 HOL-Proofs: theory HOL.BNF_Least_Fixpoint

21:02:40 Timing ZF-ex (2 threads, 13.930s elapsed time, 19.620s cpu time, 0.940s GC time, factor 1.41)

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

21:02:40 Finished ZF-ex (0:00:14 elapsed time, 0:00:20 cpu time, factor 1.35)

21:02:40 Running ZF-AC ...

21:02:40 HOL: theory HOL.List

21:02:40 ZF-AC: theory ZF-AC.AC_Equiv

21:02:41 ZF-AC: theory ZF-AC.AC18_AC19

21:02:41 ZF-AC: theory ZF-AC.AC7_AC9

21:02:41 ZF-AC: theory ZF-AC.Cardinal_aux

21:02:41 ZF-AC: theory ZF-AC.Hartog

21:02:41 ZF-AC: theory ZF-AC.HH

21:02:41 ZF-AC: theory ZF-AC.WO6_WO1

21:02:41 ZF-AC: theory ZF-AC.AC16_lemmas

21:02:41 ZF-AC: theory ZF-AC.AC16_WO4

21:02:41 ZF-AC: theory ZF-AC.DC

21:02:42 ZF-AC: theory ZF-AC.AC15_WO6

21:02:42 ZF-AC: theory ZF-AC.AC17_AC1

21:02:42 ZF-AC: theory ZF-AC.WO1_AC

21:02:42 ZF-AC: theory ZF-AC.WO1_WO7

21:02:42 ZF-AC: theory ZF-AC.WO2_AC16

21:02:45 HOL-Proofs: theory HOL.Basic_BNF_LFPs

21:02:45 HOL-Proofs: theory HOL.Transfer

21:02:48 HOL-Proofs: theory HOL.Num

21:02:50 Timing ZF-AC (2 threads, 7.089s elapsed time, 11.544s cpu time, 0.548s GC time, factor 1.63)

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

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

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

21:02:50 Finished ZF-AC (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.50)

21:02:50 Running CCL ...

21:02:50 CCL: theory IFOL

21:02:51 HOL: theory HOL.Groups_List

21:02:51 HOL: theory HOL.Map

21:02:52 CCL: theory FOL

21:02:52 HOL: theory HOL.Factorial

21:02:52 HOL: theory HOL.GCD

21:02:53 HOL: theory HOL.Binomial

21:02:53 HOL-Proofs: theory HOL.Power

21:02:53 HOL: theory HOL.Enum

21:02:54 CCL: theory CCL.Set

21:02:54 CCL: theory CCL.Lfp

21:02:54 CCL: theory CCL.Gfp

21:02:54 CCL: theory CCL.CCL

21:02:55 CCL: theory CCL.Term

21:02:55 CCL: theory CCL.Trancl

21:02:55 CCL: theory CCL.Type

21:02:56 CCL: theory CCL.Fix

21:02:56 CCL: theory CCL.Hered

21:02:56 CCL: theory CCL.Wfd

21:02:56 HOL: theory HOL.String

21:02:56 CCL: theory CCL.Nat

21:02:56 CCL: theory CCL.List

21:02:57 CCL: theory CCL.Flag

21:02:57 CCL: theory CCL.Stream

21:02:57 HOL: theory HOL.BNF_Greatest_Fixpoint

21:02:58 HOL-Proofs: theory HOL.Groups_Big

21:02:58 Timing CCL (2 threads, 6.671s elapsed time, 9.484s cpu time, 0.696s GC time, factor 1.42)

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

21:02:58 Finished CCL (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.31)

21:02:58 Running FOL-ex ...

21:02:59 FOL-ex: theory FOL-ex.If

21:02:59 FOL-ex: theory FOL-ex.Classical

21:02:59 FOL-ex: theory FOL-ex.Intro

21:02:59 FOL-ex: theory FOL-ex.Miniscope

21:02:59 FOL-ex: theory FOL-ex.Nat

21:02:59 FOL-ex: theory FOL-ex.Nat_Class

21:02:59 FOL-ex: theory FOL-ex.Natural_Numbers

21:02:59 FOL-ex: theory FOL-ex.Prolog

21:02:59 FOL-ex: theory FOL-ex.Propositional_Cla

21:02:59 FOL-ex: theory FOL-ex.Quantifiers_Cla

21:02:59 FOL-ex: theory FOL-ex.Foundation

21:02:59 FOL-ex: theory FOL-ex.Intuitionistic

21:02:59 FOL-ex: theory FOL-ex.Propositional_Int

21:02:59 FOL-ex: theory FOL-ex.Quantifiers_Int

21:03:00 HOL: theory HOL.Predicate

21:03:01 HOL: theory HOL.Lazy_Sequence

21:03:02 FOL-ex: theory FOL-ex.Locale_Test1

21:03:02 HOL: theory HOL.Limited_Sequence

21:03:02 HOL: theory HOL.Typerep

21:03:04 HOL: theory HOL.Code_Evaluation

21:03:05 FOL-ex: theory FOL-ex.Locale_Test2

21:03:05 FOL-ex: theory FOL-ex.Locale_Test3

21:03:05 FOL-ex: theory FOL-ex.Locale_Test

21:03:05 HOL: theory HOL.Random

21:03:06 HOL: theory HOL.Quickcheck_Random

21:03:07 HOL-Proofs: theory HOL.Equiv_Relations

21:03:07 Timing FOL-ex (2 threads, 6.230s elapsed time, 9.040s cpu time, 0.216s GC time, factor 1.45)

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

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

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

21:03:07 Finished FOL-ex (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.39)

21:03:07 Running Sequents ...

21:03:08 Sequents: theory Sequents.Sequents

21:03:08 Sequents: theory Sequents.ILL

21:03:08 Sequents: theory Sequents.LK0

21:03:08 Sequents: theory Sequents.ILL_predlog

21:03:08 Sequents: theory Sequents.Washing

21:03:08 Sequents: theory Sequents.LK

21:03:08 Sequents: theory Sequents.Modal0

21:03:08 Sequents: theory Sequents.S4

21:03:08 Sequents: theory Sequents.S43

21:03:08 Sequents: theory Sequents.Hard_Quantifiers

21:03:08 HOL: theory HOL.Quickcheck_Exhaustive

21:03:08 HOL: theory HOL.Quickcheck_Narrowing

21:03:08 Sequents: theory Sequents.Nat

21:03:08 Sequents: theory Sequents.Propositional

21:03:08 Sequents: theory Sequents.Quantifiers

21:03:09 Sequents: theory Sequents.T

21:03:10 HOL-Proofs: theory HOL.Lifting

21:03:12 Timing Sequents (2 threads, 3.860s elapsed time, 7.444s cpu time, 0.148s GC time, factor 1.93)

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

21:03:12 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.65)

21:03:12 Running FOLP-ex ...

21:03:13 FOLP-ex: theory FOLP-ex.Classical

21:03:13 FOLP-ex: theory FOLP-ex.If

21:03:13 FOLP-ex: theory FOLP-ex.Intro

21:03:13 FOLP-ex: theory FOLP-ex.Nat

21:03:13 FOLP-ex: theory FOLP-ex.Propositional_Cla

21:03:13 HOL: theory HOL.Random_Pred

21:03:13 HOL: theory HOL.Record

21:03:13 FOLP-ex: theory FOLP-ex.Quantifiers_Cla

21:03:14 HOL: theory HOL.Random_Sequence

21:03:14 FOLP-ex: theory FOLP-ex.Foundation

21:03:14 FOLP-ex: theory FOLP-ex.Intuitionistic

21:03:14 HOL: theory HOL.Predicate_Compile

21:03:15 FOLP-ex: theory FOLP-ex.Propositional_Int

21:03:16 HOL: theory HOL.Nitpick

21:03:16 FOLP-ex: theory FOLP-ex.Quantifiers_Int

21:03:18 Timing FOLP-ex (2 threads, 4.402s elapsed time, 7.048s cpu time, 0.128s GC time, factor 1.60)

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

21:03:18 Finished FOLP-ex (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.41)

21:03:18 Running LCF ...

21:03:18 LCF: theory IFOL

21:03:19 LCF: theory FOL

21:03:19 HOL-Proofs: theory HOL.Lifting_Set

21:03:20 HOL-Proofs: theory HOL.Option

21:03:21 HOL-Proofs: theory HOL.Quotient

21:03:21 HOL-Proofs: theory HOL.Extraction

21:03:22 LCF: theory LCF.LCF

21:03:22 LCF: theory LCF.Ex1

21:03:22 LCF: theory LCF.Ex2

21:03:22 LCF: theory LCF.Ex3

21:03:22 LCF: theory LCF.Ex4

21:03:23 Timing LCF (2 threads, 3.593s elapsed time, 4.080s cpu time, 0.152s GC time, factor 1.14)

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

21:03:23 Finished LCF (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00)

21:03:23 Running Spec_Check ...

21:03:23 Spec_Check: theory Spec_Check.Spec_Check

21:03:23 HOL: theory HOL.Nunchaku

21:03:23 Spec_Check: theory Spec_Check.Examples

21:03:24 HOL: theory Main

21:03:24 HOL-Proofs: theory HOL.Lattices_Big

21:03:26 HOL-Proofs: theory HOL.Partial_Function

21:03:26 Timing Spec_Check (2 threads, 2.004s elapsed time, 3.332s cpu time, 0.016s GC time, factor 1.66)

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

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

21:03:26 Running ZF-Resid ...

21:03:26 HOL: theory HOL.Archimedean_Field

21:03:26 HOL: theory HOL.Topological_Spaces

21:03:26 ZF-Resid: theory ZF-Resid.Redex

21:03:26 ZF-Resid: theory ZF-Resid.Substitution

21:03:26 ZF-Resid: theory ZF-Resid.Residuals

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

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

21:03:28 HOL-Proofs: theory HOL.Fun_Def

21:03:28 Timing ZF-Resid (2 threads, 1.692s elapsed time, 2.684s cpu time, 0.000s GC time, factor 1.59)

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

21:03:28 Finished ZF-Resid (0:00:02 elapsed time)

21:03:28 Running ZF-IMP ...

21:03:28 ZF-IMP: theory ZF-IMP.Com

21:03:29 ZF-IMP: theory ZF-IMP.Denotation

21:03:29 ZF-IMP: theory ZF-IMP.Equiv

21:03:30 HOL-Proofs: theory HOL.Int

21:03:32 Timing ZF-IMP (2 threads, 1.145s elapsed time, 1.320s cpu time, 0.000s GC time, factor 1.15)

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

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

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

21:03:32 Finished ZF-IMP (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.10)

21:03:32 Running CTT ...

21:03:32 CTT: theory CTT.CTT

21:03:32 HOL: theory HOL.Rat

21:03:33 CTT: theory CTT.Elimination

21:03:33 CTT: theory CTT.Equality

21:03:33 CTT: theory CTT.Synthesis

21:03:33 CTT: theory CTT.Typechecking

21:03:35 HOL: theory HOL.Real

21:03:35 Timing CTT (2 threads, 0.972s elapsed time, 1.348s cpu time, 0.000s GC time, factor 1.39)

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

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

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

21:03:35 Finished CTT (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.23)

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

21:03:36 ZF-Coind: theory ZF-Coind.Language

21:03:36 ZF-Coind: theory ZF-Coind.Map

21:03:36 ZF-Coind: theory ZF-Coind.Types

21:03:36 ZF-Coind: theory ZF-Coind.Values

21:03:36 ZF-Coind: theory ZF-Coind.Dynamic

21:03:36 ZF-Coind: theory ZF-Coind.Static

21:03:36 ZF-Coind: theory ZF-Coind.ECR

21:03:36 HOL: theory HOL.Real_Vector_Spaces

21:03:37 Timing ZF-Coind (2 threads, 0.764s elapsed time, 1.432s cpu time, 0.000s GC time, factor 1.87)

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

21:03:37 Finished ZF-Coind (0:00:01 elapsed time)

21:03:37 Running Cube ...

21:03:37 Cube: theory Cube.Cube

21:03:38 HOL-Proofs: theory HOL.Euclidean_Division

21:03:38 Cube: theory Cube.Example

21:03:38 Timing Cube (2 threads, 0.351s elapsed time, 0.356s cpu time, 0.000s GC time, factor 1.01)

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

21:03:38 Finished Cube (0:00:00 elapsed time)

21:03:38 Running Intro ...

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

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

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

21:03:41 Finished Intro (0:00:02 elapsed time)

21:03:41 Running Logics ...

21:03:45 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

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

21:03:45 Finished Logics (0:00:03 elapsed time)

21:03:45 Running Logics_ZF ...

21:03:45 Logics_ZF: theory Logics_ZF.FOL_examples

21:03:45 Logics_ZF: theory Logics_ZF.If

21:03:45 Logics_ZF: theory Logics_ZF.ZF_Isar

21:03:45 Logics_ZF: theory Logics_ZF.ZF_examples

21:03:45 Logics_ZF: theory Logics_ZF.IFOL_examples

21:03:49 Timing Logics_ZF (2 threads, 0.299s elapsed time, 0.592s cpu time, 0.000s GC time, factor 1.98)

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

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

21:03:49 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.90)

21:03:49 Running Nitpick ...

21:03:50 HOL: theory HOL.Inequalities

21:03:50 HOL: theory HOL.Limits

21:03:50 HOL-Proofs: theory HOL.Parity

21:03:52 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

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

21:03:52 Finished Nitpick (0:00:02 elapsed time)

21:03:52 Running System ...

21:03:52 System: theory System.Base

21:03:52 System: theory System.Environment

21:03:52 System: theory System.Misc

21:03:52 System: theory System.Presentation

21:03:52 System: theory System.Scala

21:03:52 System: theory System.Sessions

21:03:54 HOL: theory HOL.Deriv

21:03:54 HOL: theory HOL.Series

21:03:55 HOL: theory HOL.NthRoot

21:03:56 Timing System (2 threads, 0.426s elapsed time, 0.572s cpu time, 0.000s GC time, factor 1.34)

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

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

21:03:56 Finished System (0:00:03 elapsed time)

21:03:56 Running SML ...

21:03:56 SML: theory SML.Examples

21:03:56 HOL-Proofs: theory HOL.Divides

21:03:56 HOL: theory HOL.Transcendental

21:03:57 Timing SML (2 threads, 0.014s elapsed time, 0.016s cpu time, 0.000s GC time, factor 1.11)

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

21:03:57 Finished SML (0:00:00 elapsed time)

21:03:57 Running Sledgehammer ...

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

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

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

21:04:00 Finished Sledgehammer (0:00:02 elapsed time)

21:04:02 HOL: theory HOL.Complex

21:04:02 HOL: theory HOL.MacLaurin

21:04:04 HOL: theory Complex_Main

21:04:04 HOL-Proofs: theory HOL.Code_Numeral

21:04:05 HOL-Proofs: theory HOL.Numeral_Simprocs

21:04:06 HOL-Proofs: theory HOL.Semiring_Normalization

21:04:09 HOL-Proofs: theory HOL.SMT

21:04:09 HOL-Proofs: theory HOL.Set_Interval

21:04:12 HOL-Proofs: theory HOL.Groebner_Basis

21:04:24 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices

21:04:24 HOL-Proofs: theory HOL.Filter

21:04:31 HOL-Proofs: theory HOL.Presburger

21:04:46 HOL-Proofs: theory HOL.Sledgehammer

21:04:49 HOL-Proofs: theory HOL.List

21:06:05 HOL-Proofs: theory HOL.Groups_List

21:06:07 HOL-Proofs: theory HOL.Factorial

21:06:17 HOL-Proofs: theory HOL.Binomial

21:06:29 HOL-Proofs: theory HOL.GCD

21:06:49 HOL-Proofs: theory HOL.Map

21:06:53 HOL-Proofs: theory HOL.Enum

21:07:19 Timing HOL (2 threads, 308.953s elapsed time, 580.076s cpu time, 59.808s GC time, factor 1.88)

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

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

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

21:07:19 Finished HOL (0:06:35 elapsed time, 0:11:50 cpu time, factor 1.80)

21:07:19 Building HOL-Library ...

21:07:19 Building HOLCF ...

21:07:20 HOLCF: theory HOL-Library.Nat_Bijection

21:07:20 HOLCF: theory HOL-Library.Old_Datatype

21:07:21 HOL-Library: theory HOL-Library.Adhoc_Overloading

21:07:21 HOL-Library: theory HOL-Library.Lattice_Syntax

21:07:21 HOL-Library: theory HOL-Library.AList

21:07:21 HOL-Library: theory HOL-Library.BNF_Axiomatization

21:07:21 HOLCF: theory HOLCF.Porder

21:07:21 HOL-Library: theory HOL-Library.BNF_Corec

21:07:21 HOLCF: theory HOLCF.Pcpo

21:07:22 HOLCF: theory HOL-Library.Countable

21:07:23 HOL-Library: theory HOL-Library.DAList

21:07:23 HOLCF: theory HOLCF.Cont

21:07:23 HOLCF: theory HOLCF.Adm

21:07:23 HOLCF: theory HOLCF.Cpodef

21:07:23 HOLCF: theory HOLCF.Fun_Cpo

21:07:24 HOLCF: theory HOLCF.Product_Cpo

21:07:24 HOLCF: theory HOLCF.Discrete

21:07:24 HOLCF: theory HOLCF.Cfun

21:07:24 HOL-Library: theory HOL-Library.Bit

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

21:07:25 HOLCF: theory HOLCF.Completion

21:07:25 HOLCF: theory HOLCF.Cprod

21:07:25 HOLCF: theory HOLCF.Deflation

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

21:07:25 HOLCF: theory HOLCF.Fix

21:07:25 HOLCF: theory HOLCF.Sfun

21:07:25 HOLCF: theory HOLCF.Sprod

21:07:25 HOLCF: theory HOLCF.Up

21:07:26 HOL-Library: theory HOL-Library.Multiset

21:07:26 HOLCF: theory HOLCF.Lift

21:07:27 HOLCF: theory HOLCF.One

21:07:27 HOLCF: theory HOLCF.Tr

21:07:27 HOLCF: theory HOLCF.Ssum

21:07:27 HOLCF: theory HOLCF.Fixrec

21:07:27 HOLCF: theory HOLCF.Map_Functions

21:07:28 HOLCF: theory HOLCF.Bifinite

21:07:28 HOLCF: theory HOLCF.Domain_Aux

21:07:29 HOL-Proofs: theory HOL.Random

21:07:29 HOLCF: theory HOLCF.Universal

21:07:29 HOL-Library: theory HOL-Library.Cardinal_Notations

21:07:29 HOL-Library: theory HOL-Library.Char_ord

21:07:30 HOL-Library: theory HOL-Library.Code_Abstract_Nat

21:07:30 HOL-Library: theory HOL-Library.Code_Binary_Nat

21:07:30 HOL-Library: theory HOL-Library.Code_Target_Nat

21:07:30 HOL-Library: theory HOL-Library.Code_Char

21:07:30 HOL-Library: theory HOL-Library.Code_Prolog

21:07:30 HOL-Library: theory HOL-Library.Code_Target_Int

21:07:31 HOL-Library: theory HOL-Library.Code_Target_Numeral

21:07:31 HOL-Library: theory HOL-Library.Code_Test

21:07:31 HOLCF: theory HOLCF.Algebraic

21:07:31 HOLCF: theory HOLCF.Compact_Basis

21:07:31 HOLCF: theory HOLCF.LowerPD

21:07:31 HOLCF: theory HOLCF.UpperPD

21:07:32 HOLCF: theory HOLCF.Representable

21:07:32 HOL-Library: theory HOL-Library.DAList_Multiset

21:07:32 HOLCF: theory HOLCF.ConvexPD

21:07:32 HOL-Library: theory HOL-Library.Multiset_Order

21:07:32 HOL-Library: theory HOL-Library.Permutation

21:07:32 HOL-Library: theory HOL-Library.Combine_PER

21:07:32 HOL-Library: theory HOL-Library.Complete_Partial_Order2

21:07:33 HOL-Library: theory HOL-Library.Debug

21:07:33 HOL-Library: theory HOL-Library.Disjoint_Sets

21:07:33 HOL-Library: theory HOL-Library.Permutations

21:07:34 HOL-Library: theory HOL-Library.Dlist

21:07:35 HOLCF: theory HOLCF.Domain

21:07:35 HOL-Library: theory HOL-Library.Fun_Lexorder

21:07:35 HOL-Library: theory HOL-Library.FuncSet

21:07:36 HOL-Library: theory HOL-Library.Function_Algebras

21:07:36 HOLCF: theory HOLCF.Powerdomains

21:07:36 HOL-Library: theory HOL-Library.Function_Division

21:07:36 HOL-Library: theory HOL-Library.Groups_Big_Fun

21:07:37 HOL-Library: theory HOL-Library.IArray

21:07:37 HOL-Library: theory HOL-Library.Infinite_Set

21:07:37 HOL-Library: theory HOL-Library.Omega_Words_Fun

21:07:37 HOLCF: theory HOLCF

21:07:37 HOL-Library: theory HOL-Library.Ramsey

21:07:38 HOL-Library: theory HOL-Library.LaTeXsugar

21:07:38 HOL-Library: theory HOL-Library.Lattice_Constructions

21:07:38 HOL-Library: theory HOL-Library.ListVector

21:07:38 HOL-Library: theory HOL-Library.List_lexord

21:07:38 HOL-Library: theory HOL-Library.Mapping

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

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

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

21:07:41 HOL-Library: theory HOL-Library.More_List

21:07:41 HOL-Library: theory HOL-Library.Nat_Bijection

21:07:41 HOL-Library: theory HOL-Library.Old_Datatype

21:07:41 HOL-Library: theory HOL-Library.Stream

21:07:43 HOL-Library: theory HOL-Library.Old_Recdef

21:07:43 HOL-Library: theory HOL-Library.Open_State_Syntax

21:07:43 HOL-Library: theory HOL-Library.Option_ord

21:07:43 HOL-Library: theory HOL-Library.Parallel

21:07:44 HOL-Library: theory HOL-Library.Pattern_Aliases

21:07:44 HOL-Library: theory HOL-Library.Perm

21:07:44 HOL-Library: theory HOL-Library.Phantom_Type

21:07:45 HOL-Library: theory HOL-Library.Cardinality

21:07:45 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

21:07:45 HOL-Proofs: theory HOL.String

21:07:46 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

21:07:46 HOL-Library: theory HOL-Library.Preorder

21:07:46 HOL-Library: theory HOL-Library.Product_Lexorder

21:07:46 HOL-Library: theory HOL-Library.Numeral_Type

21:07:46 HOL-Library: theory HOL-Library.Product_Plus

21:07:46 HOL-Library: theory HOL-Library.Product_Order

21:07:47 HOL-Library: theory HOL-Library.Finite_Lattice

21:07:47 HOL-Library: theory HOL-Library.Type_Length

21:07:48 HOL-Library: theory HOL-Library.Saturated

21:07:48 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint

21:07:48 HOL-Library: theory HOL-Library.Quotient_Syntax

21:07:48 HOL-Library: theory HOL-Library.Quotient_Option

21:07:48 HOL-Library: theory HOL-Library.Quotient_Product

21:07:48 HOL-Library: theory HOL-Library.Quotient_Set

21:07:48 HOL-Library: theory HOL-Library.Quotient_List

21:07:49 HOL-Library: theory HOL-Library.Quotient_Sum

21:07:49 HOL-Library: theory HOL-Library.Quotient_Type

21:07:49 HOL-Library: theory HOL-Library.RBT_Impl

21:07:50 HOL-Library: theory HOL-Library.Reflection

21:07:50 HOL-Library: theory HOL-Library.Refute

21:07:51 HOL-Library: theory HOL-Library.Rewrite

21:07:51 HOL-Library: theory HOL-Library.Set_Algebras

21:07:51 HOL-Library: theory HOL-Library.Simps_Case_Conv

21:07:51 HOL-Library: theory HOL-Library.Extended

21:07:54 HOL-Library: theory HOL-Library.Stirling

21:07:54 HOL-Library: theory HOL-Library.Sublist

21:07:56 HOL-Library: theory HOL-Library.Prefix_Order

21:07:56 HOL-Library: theory HOL-Library.Subseq_Order

21:07:56 HOL-Library: theory HOL-Library.Transitive_Closure_Table

21:07:56 HOL-Proofs: theory HOL.Predicate

21:07:56 HOL-Library: theory HOL-Library.Tree

21:07:59 Timing HOLCF (2 threads, 19.078s elapsed time, 37.460s cpu time, 2.092s GC time, factor 1.96)

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

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

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

21:07:59 Finished HOLCF (0:00:39 elapsed time, 0:01:04 cpu time, factor 1.64)

21:07:59 Building IOA ...

21:07:59 HOL-Proofs: theory HOL.Lazy_Sequence

21:07:59 HOL-Library: theory HOL-Library.Tree_Multiset

21:08:00 HOL-Library: theory HOL-Library.Uprod

21:08:00 IOA: theory IOA.Asig

21:08:00 IOA: theory IOA.Seq

21:08:00 IOA: theory IOA.Automata

21:08:00 HOL-Proofs: theory HOL.Limited_Sequence

21:08:01 HOL-Library: theory HOL-Library.While_Combinator

21:08:01 HOL-Proofs: theory HOL.Typerep

21:08:01 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

21:08:01 IOA: theory IOA.Sequence

21:08:02 HOL-Library: theory HOL-Library.Countable

21:08:02 IOA: theory IOA.Pred

21:08:02 HOL-Proofs: theory HOL.Code_Evaluation

21:08:02 IOA: theory IOA.TL

21:08:02 IOA: theory IOA.Traces

21:08:03 HOL-Library: theory HOL-Library.Countable_Set

21:08:03 IOA: theory IOA.CompoExecs

21:08:04 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

21:08:04 IOA: theory IOA.RefMappings

21:08:04 IOA: theory IOA.RefCorrectness

21:08:04 IOA: theory IOA.CompoScheds

21:08:04 HOL-Proofs: theory HOL.Quickcheck_Random

21:08:04 IOA: theory IOA.Simulations

21:08:05 IOA: theory IOA.SimCorrectness

21:08:05 IOA: theory IOA.Deadlock

21:08:05 IOA: theory IOA.ShortExecutions

21:08:06 IOA: theory IOA.CompoTraces

21:08:06 HOL-Library: theory HOL-Library.Countable_Set_Type

21:08:07 IOA: theory IOA.Compositionality

21:08:07 IOA: theory IOA.IOA

21:08:07 IOA: theory IOA.TLS

21:08:07 HOL-Proofs: theory HOL.Quickcheck_Exhaustive

21:08:08 IOA: theory IOA.LiveIOA

21:08:08 IOA: theory IOA.Abstraction

21:08:09 HOL-Library: theory HOL-Library.FSet

21:08:13 HOL-Library: theory HOL-Library.Finite_Map

21:08:14 HOL-Proofs: theory HOL.Record

21:08:16 HOL-Library: theory HOL-Library.BigO

21:08:17 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

21:08:17 HOL-Proofs: theory HOL.Nitpick

21:08:17 HOL-Library: theory HOL-Library.Diagonal_Subsequence

21:08:18 HOL-Library: theory HOL-Library.Discrete

21:08:18 HOL-Library: theory HOL-Library.Going_To_Filter

21:08:18 HOL-Library: theory HOL-Library.Indicator_Function

21:08:18 HOL-Library: theory HOL-Library.Lattice_Algebras

21:08:24 HOL-Library: theory HOL-Library.Liminf_Limsup

21:08:25 HOL-Library: theory HOL-Library.Log_Nat

21:08:26 HOL-Library: theory HOL-Library.Float

21:08:27 HOL-Proofs: theory HOL.Nunchaku

21:08:27 HOL-Library: theory HOL-Library.RBT

21:08:28 HOL-Library: theory HOL-Library.RBT_Mapping

21:08:28 HOL-Proofs: theory HOL.Quickcheck_Narrowing

21:08:28 HOL-Library: theory HOL-Library.RBT_Set

21:08:28 HOL-Library: theory HOL-Library.Lub_Glb

21:08:29 HOL-Library: theory HOL-Library.Multiset_Permutations

21:08:29 HOL-Library: theory HOL-Library.Nonpos_Ints

21:08:30 HOL-Library: theory HOL-Library.OptionalSugar

21:08:30 HOL-Library: theory HOL-Library.Order_Continuity

21:08:30 HOL-Library: theory HOL-Library.Periodic_Fun

21:08:30 HOL-Library: theory HOL-Library.Quadratic_Discriminant

21:08:30 HOL-Library: theory HOL-Library.Sum_of_Squares

21:08:31 HOL-Library: theory HOL-Library.Extended_Nat

21:08:32 HOL-Library: theory HOL-Library.Extended_Real

21:08:33 Timing IOA (2 threads, 18.033s elapsed time, 33.504s cpu time, 1.268s GC time, factor 1.86)

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

21:08:33 Finished IOA (0:00:33 elapsed time, 0:00:52 cpu time, factor 1.58)

21:08:33 Building HOL-Word ...

21:08:33 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

21:08:34 HOL-Word: theory HOL-Library.Boolean_Algebra

21:08:34 HOL-Word: theory HOL-Library.Bit

21:08:34 HOL-Word: theory HOL-Library.Phantom_Type

21:08:34 HOL-Word: theory HOL-Word.Bits

21:08:35 HOL-Word: theory HOL-Word.Bits_Bit

21:08:35 HOL-Word: theory HOL-Word.Misc_Numeric

21:08:35 HOL-Library: theory HOL-Library.Tree_Real

21:08:35 HOL-Word: theory HOL-Word.Bit_Representation

21:08:35 HOL-Word: theory HOL-Library.Cardinality

21:08:36 HOL-Word: theory HOL-Word.Bits_Int

21:08:36 HOL-Proofs: theory HOL.Random_Pred

21:08:37 HOL-Word: theory HOL-Library.Numeral_Type

21:08:37 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

21:08:38 HOL-Proofs: theory HOL.Random_Sequence

21:08:38 HOL-Word: theory HOL-Library.Type_Length

21:08:38 HOL-Word: theory HOL-Word.Bit_Comparison

21:08:38 HOL-Word: theory HOL-Word.Bool_List_Representation

21:08:38 HOL-Word: theory HOL-Word.Word_Miscellaneous

21:08:38 HOL-Word: theory HOL-Word.Misc_Typedef

21:08:39 HOL-Word: theory HOL-Word.Word

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

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

21:08:44 HOL-Proofs: theory Main

21:08:46 HOL-Word: theory HOL-Word.WordBitwise

21:08:47 HOL-Proofs: theory HOL-Library.Old_Datatype

21:09:17 Timing HOL-Word (2 threads, 24.541s elapsed time, 46.732s cpu time, 1.868s GC time, factor 1.90)

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

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

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

21:09:17 Finished HOL-Word (0:00:43 elapsed time, 0:01:12 cpu time, factor 1.67)

21:09:17 Building HOL-TLA ...

21:09:17 HOL-TLA: theory HOL-TLA.Intensional

21:09:18 HOL-TLA: theory HOL-TLA.Stfun

21:09:18 HOL-TLA: theory HOL-TLA.Action

21:09:18 HOL-TLA: theory HOL-TLA.Init

21:09:18 HOL-TLA: theory HOL-TLA.TLA

21:09:29 Timing HOL-TLA (2 threads, 1.813s elapsed time, 2.932s cpu time, 0.000s GC time, factor 1.62)

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

21:09:29 Finished HOL-TLA (0:00:11 elapsed time, 0:00:15 cpu time, factor 1.27)

21:09:29 Building HOL-Analysis ...

21:09:32 HOL-Analysis: theory HOL-Library.Cancellation

21:09:32 HOL-Analysis: theory HOL-Library.Disjoint_Sets

21:09:32 HOL-Analysis: theory HOL-Library.FuncSet

21:09:32 HOL-Analysis: theory HOL-Library.Multiset

21:09:32 HOL-Analysis: theory HOL-Library.Infinite_Set

21:09:33 HOL-Analysis: theory HOL-Library.Nat_Bijection

21:09:33 HOL-Analysis: theory HOL-Library.Old_Datatype

21:09:36 HOL-Analysis: theory HOL-Library.Phantom_Type

21:09:36 HOL-Analysis: theory HOL-Library.Cardinality

21:09:37 HOL-Analysis: theory HOL-Library.Numeral_Type

21:09:39 HOL-Analysis: theory HOL-Library.Product_Plus

21:09:39 HOL-Analysis: theory HOL-Library.Product_Order

21:09:39 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

21:09:39 HOL-Analysis: theory HOL-Library.Permutations

21:09:40 HOL-Analysis: theory HOL-Library.Set_Algebras

21:09:41 HOL-Analysis: theory HOL-Library.Countable

21:09:42 HOL-Analysis: theory HOL-Library.Countable_Set

21:09:43 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

21:09:47 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

21:09:48 HOL-Analysis: theory HOL-Analysis.Infinite_Products

21:09:48 HOL-Analysis: theory HOL-Analysis.Inner_Product

21:09:49 HOL-Analysis: theory HOL-Analysis.Product_Vector

21:09:50 HOL-Analysis: theory HOL-Analysis.L2_Norm

21:09:50 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

21:09:51 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

21:09:52 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

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

21:09:57 HOL-Analysis: theory HOL-Analysis.Operator_Norm

21:09:57 HOL-Analysis: theory HOL-Analysis.Poly_Roots

21:09:58 HOL-Analysis: theory HOL-Library.Discrete

21:09:58 HOL-Analysis: theory HOL-Library.Indicator_Function

21:09:58 HOL-Analysis: theory HOL-Library.Liminf_Limsup

21:09:59 HOL-Analysis: theory HOL-Library.Nonpos_Ints

21:09:59 HOL-Analysis: theory HOL-Library.Order_Continuity

21:10:00 HOL-Analysis: theory HOL-Computational_Algebra.Primes

21:10:00 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

21:10:00 HOL-Analysis: theory HOL-Library.Extended_Nat

21:10:01 HOL-Analysis: theory HOL-Library.Extended_Real

21:10:04 HOL-Analysis: theory HOL-Library.Periodic_Fun

21:10:05 HOL-Analysis: theory HOL-Library.Sum_of_Squares

21:10:06 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

21:10:07 HOL-Analysis: theory HOL-Analysis.Norm_Arith

21:10:08 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

21:10:08 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

21:10:12 HOL-Analysis: theory HOL-Analysis.Measurable

21:10:13 HOL-Analysis: theory HOL-Analysis.Measure_Space

21:10:15 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

21:10:16 HOL-Analysis: theory HOL-Analysis.Caratheodory

21:10:17 HOL-Analysis: theory HOL-Analysis.Connected

21:10:17 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

21:10:18 HOL-Analysis: theory HOL-Analysis.Summation_Tests

21:10:20 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

21:10:20 HOL-Analysis: theory HOL-Analysis.Tagged_Division

21:10:21 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

21:10:23 HOL-Analysis: theory HOL-Analysis.Starlike

21:10:26 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

21:10:27 HOL-Analysis: theory HOL-Analysis.Path_Connected

21:10:31 HOL-Analysis: theory HOL-Analysis.Homeomorphism

21:10:32 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

21:10:35 HOL-Analysis: theory HOL-Analysis.Derivative

21:10:37 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

21:10:37 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

21:10:40 HOL-Analysis: theory HOL-Analysis.Determinants

21:10:40 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

21:10:40 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

21:10:41 HOL-Analysis: theory HOL-Analysis.Polytope

21:10:45 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

21:10:45 HOL-Analysis: theory HOL-Analysis.Borel_Space

21:10:48 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

21:10:48 HOL-Analysis: theory HOL-Analysis.Regularity

21:10:50 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

21:10:51 HOL-Analysis: theory HOL-Analysis.Embed_Measure

21:10:51 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

21:10:53 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

21:10:53 HOL-Analysis: theory HOL-Analysis.Function_Topology

21:10:55 HOL-Analysis: theory HOL-Analysis.Complete_Measure

21:10:55 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

21:10:56 HOL-Analysis: theory HOL-Analysis.Set_Integral

21:10:56 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

21:10:57 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

21:10:58 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

21:11:02 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

21:11:02 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

21:11:03 HOL-Analysis: theory HOL-Analysis.Integral_Test

21:11:04 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

21:11:04 HOL-Analysis: theory HOL-Analysis.Improper_Integral

21:11:04 HOL-Analysis: theory HOL-Analysis.Interval_Integral

21:11:05 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

21:11:05 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

21:11:08 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

21:11:08 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

21:11:09 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

21:11:11 HOL-Analysis: theory HOL-Analysis.Further_Topology

21:11:14 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

21:11:15 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

21:11:16 HOL-Analysis: theory HOL-Analysis.FPS_Convergence

21:11:16 HOL-Analysis: theory HOL-Analysis.Gamma_Function

21:11:18 HOL-Analysis: theory HOL-Analysis.Great_Picard

21:11:19 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping

21:11:20 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

21:11:21 HOL-Analysis: theory HOL-Analysis.Analysis

21:12:04 Timing HOL-Library (2 threads, 209.712s elapsed time, 388.244s cpu time, 18.800s GC time, factor 1.85)

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

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

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

21:12:04 Finished HOL-Library (0:04:43 elapsed time, 0:08:15 cpu time, factor 1.75)

21:12:04 Building HOL-Computational_Algebra ...

21:12:06 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

21:12:06 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

21:12:17 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

21:12:17 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

21:12:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

21:12:27 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

21:12:27 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

21:12:27 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

21:12:28 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers

21:12:28 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree

21:12:28 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

21:12:29 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

21:12:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

21:12:45 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

21:13:45 Timing HOL-Computational_Algebra (2 threads, 71.035s elapsed time, 126.656s cpu time, 5.176s GC time, factor 1.78)

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

21:13:45 Finished HOL-Computational_Algebra (0:01:39 elapsed time, 0:02:42 cpu time, factor 1.63)

21:13:45 Building HOL-Number_Theory ...

21:13:47 HOL-Number_Theory: theory HOL-Number_Theory.Cong

21:13:47 HOL-Number_Theory: theory HOL-Algebra.Congruence

21:13:48 HOL-Number_Theory: theory HOL-Algebra.Order

21:13:49 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

21:13:49 HOL-Number_Theory: theory HOL-Number_Theory.Fib

21:13:49 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers

21:13:49 HOL-Number_Theory: theory HOL-Algebra.Lattice

21:13:50 HOL-Number_Theory: theory HOL-Number_Theory.Totient

21:13:51 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice

21:13:52 HOL-Number_Theory: theory HOL-Algebra.Group

21:13:54 HOL-Number_Theory: theory HOL-Algebra.Coset

21:13:54 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct

21:13:55 HOL-Number_Theory: theory HOL-Algebra.Ring

21:14:01 HOL-Number_Theory: theory HOL-Algebra.AbelCoset

21:14:04 HOL-Number_Theory: theory HOL-Algebra.Module

21:14:07 HOL-Number_Theory: theory HOL-Algebra.More_Group

21:14:07 HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product

21:14:08 HOL-Number_Theory: theory HOL-Algebra.More_Ring

21:14:09 HOL-Number_Theory: theory HOL-Algebra.Ideal

21:14:16 HOL-Number_Theory: theory HOL-Algebra.RingHom

21:14:18 HOL-Number_Theory: theory HOL-Algebra.UnivPoly

21:14:47 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group

21:14:54 HOL-Number_Theory: theory HOL-Number_Theory.Residues

21:14:58 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

21:14:58 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

21:14:59 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

21:15:00 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

21:15:00 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

21:16:44 Timing HOL-Number_Theory (2 threads, 131.948s elapsed time, 242.264s cpu time, 9.796s GC time, factor 1.84)

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

21:16:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf

21:16:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf

21:16:44 Finished HOL-Number_Theory (0:02:58 elapsed time, 0:05:01 cpu time, factor 1.69)

21:16:44 Building HOL-Algebra ...

21:16:46 HOL-Algebra: theory HOL-Algebra.Exponent

21:16:46 HOL-Algebra: theory HOL-Algebra.Congruence

21:16:47 HOL-Algebra: theory HOL-Algebra.Order

21:16:49 HOL-Algebra: theory HOL-Algebra.Lattice

21:16:51 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

21:16:52 HOL-Algebra: theory HOL-Algebra.Galois_Connection

21:16:53 HOL-Algebra: theory HOL-Algebra.Group

21:16:55 HOL-Algebra: theory HOL-Algebra.Bij

21:16:55 HOL-Algebra: theory HOL-Algebra.Coset

21:16:56 HOL-Algebra: theory HOL-Algebra.FiniteProduct

21:16:57 HOL-Algebra: theory HOL-Algebra.Sylow

21:16:57 HOL-Algebra: theory HOL-Algebra.Divisibility

21:16:58 HOL-Algebra: theory HOL-Algebra.Ring

21:17:06 HOL-Algebra: theory HOL-Algebra.AbelCoset

21:17:07 HOL-Algebra: theory HOL-Algebra.Module

21:17:11 HOL-Algebra: theory HOL-Algebra.More_Group

21:17:11 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

21:17:11 HOL-Algebra: theory HOL-Algebra.More_Ring

21:17:15 HOL-Algebra: theory HOL-Algebra.Ideal

21:17:21 HOL-Algebra: theory HOL-Algebra.RingHom

21:17:23 HOL-Algebra: theory HOL-Algebra.QuotRing

21:17:24 HOL-Algebra: theory HOL-Algebra.UnivPoly

21:17:24 HOL-Algebra: theory HOL-Algebra.IntRing

21:17:52 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

21:19:06 Timing HOL-Proofs (2 threads, 998.543s elapsed time, 1756.180s cpu time, 217.176s GC time, factor 1.76)

21:19:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

21:19:06 Finished HOL-Proofs (0:18:21 elapsed time, 0:31:42 cpu time, factor 1.73)

21:19:06 Building HOLCF-Library ...

21:19:07 HOLCF-Library: theory HOL-Library.Infinite_Set

21:19:07 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

21:19:07 HOLCF-Library: theory HOLCF-Library.Char_Discrete

21:19:08 HOLCF-Library: theory HOLCF-Library.Int_Discrete

21:19:08 HOLCF-Library: theory HOL-Library.Countable_Set

21:19:08 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

21:19:08 HOLCF-Library: theory HOL-Library.Countable_Complete_Lattices

21:19:09 HOLCF-Library: theory HOLCF-Library.List_Cpo

21:19:09 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

21:19:09 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

21:19:10 HOLCF-Library: theory HOLCF-Library.List_Predomain

21:19:11 HOLCF-Library: theory HOLCF-Library.Option_Cpo

21:19:11 HOLCF-Library: theory HOL-Library.Order_Continuity

21:19:12 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

21:19:12 HOLCF-Library: theory HOL-Library.Extended_Nat

21:19:13 HOLCF-Library: theory HOLCF-Library.Stream

21:19:15 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

21:19:23 Timing HOL-Algebra (2 threads, 105.528s elapsed time, 197.648s cpu time, 13.524s GC time, factor 1.87)

21:19:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

21:19:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

21:19:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

21:19:23 Finished HOL-Algebra (0:02:37 elapsed time, 0:04:23 cpu time, factor 1.67)

21:19:23 Building HOL-SPARK ...

21:19:24 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

21:19:27 HOL-SPARK: theory HOL-SPARK.SPARK

21:19:37 Timing HOL-SPARK (2 threads, 2.637s elapsed time, 3.480s cpu time, 0.104s GC time, factor 1.32)

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

21:19:37 Finished HOL-SPARK (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.22)

21:19:37 Building HOL-Auth ...

21:19:39 Timing HOLCF-Library (2 threads, 17.077s elapsed time, 31.060s cpu time, 1.088s GC time, factor 1.82)

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

21:19:39 Finished HOLCF-Library (0:00:31 elapsed time, 0:00:50 cpu time, factor 1.57)

21:19:39 Building HOL-Nonstandard_Analysis ...

21:19:39 HOL-Auth: theory HOL-Auth.Message

21:19:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter

21:19:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef

21:19:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat

21:19:42 HOL-Auth: theory HOL-Auth.All_Symmetric

21:19:42 HOL-Auth: theory HOL-Auth.Event

21:19:42 HOL-Auth: theory HOL-Auth.EventSC

21:19:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef

21:19:43 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA

21:19:43 HOL-Auth: theory HOL-Auth.Extensions

21:19:44 HOL-Auth: theory HOL-Auth.Analz

21:19:45 HOL-Auth: theory HOL-Auth.List_Msg

21:19:45 HOL-Auth: theory HOL-Auth.Guard

21:19:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex

21:19:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star

21:19:45 HOL-Auth: theory HOL-Auth.GuardK

21:19:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim

21:19:46 HOL-Auth: theory HOL-Auth.Public

21:19:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar

21:19:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv

21:19:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ

21:19:46 HOL-Auth: theory HOL-Auth.Shared

21:19:47 HOL-Auth: theory HOL-Auth.CertifiedEmail

21:19:47 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries

21:19:47 HOL-Auth: theory HOL-Auth.Guard_Public

21:19:47 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental

21:19:47 HOL-Auth: theory HOL-Auth.Guard_NS_Public

21:19:47 HOL-Auth: theory HOL-Auth.P2

21:19:48 HOL-Auth: theory HOL-Auth.Proto

21:19:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog

21:19:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA

21:19:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal

21:19:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar

21:19:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim

21:19:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex

21:19:49 HOL-Auth: theory HOL-Auth.KerberosIV

21:19:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis

21:19:51 HOL-Auth: theory HOL-Auth.KerberosIV_Gets

21:19:51 HOL-Auth: theory HOL-Auth.KerberosV

21:19:53 HOL-Auth: theory HOL-Auth.Kerberos_BAN

21:19:53 HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets

21:19:54 HOL-Auth: theory HOL-Auth.NS_Public

21:19:55 HOL-Auth: theory HOL-Auth.NS_Public_Bad

21:19:55 HOL-Auth: theory HOL-Auth.NS_Shared

21:19:55 HOL-Auth: theory HOL-Auth.OtwayRees

21:19:55 HOL-Auth: theory HOL-Auth.OtwayReesBella

21:19:56 HOL-Auth: theory HOL-Auth.OtwayRees_AN

21:19:56 HOL-Auth: theory HOL-Auth.OtwayRees_Bad

21:19:56 HOL-Auth: theory HOL-Auth.P1

21:19:57 HOL-Auth: theory HOL-Auth.Recur

21:19:58 HOL-Auth: theory HOL-Auth.WooLam

21:19:58 HOL-Auth: theory HOL-Auth.Yahalom

21:19:59 HOL-Auth: theory HOL-Auth.Yahalom2

21:20:00 HOL-Auth: theory HOL-Auth.Yahalom_Bad

21:20:00 HOL-Auth: theory HOL-Auth.ZhouGollmann

21:20:01 HOL-Auth: theory HOL-Auth.Auth_Shared

21:20:02 HOL-Auth: theory HOL-Auth.Auth_Guard_Public

21:20:03 HOL-Auth: theory HOL-Auth.Guard_Shared

21:20:03 HOL-Auth: theory HOL-Auth.Guard_OtwayRees

21:20:03 HOL-Auth: theory HOL-Auth.Guard_Yahalom

21:20:04 HOL-Auth: theory HOL-Auth.TLS

21:20:04 HOL-Auth: theory HOL-Auth.Auth_Guard_Shared

21:20:04 HOL-Auth: theory HOL-Auth.Smartcard

21:20:04 HOL-Auth: theory HOL-Auth.ShoupRubin

21:20:06 HOL-Auth: theory HOL-Auth.Auth_Public

21:20:06 HOL-Auth: theory HOL-Auth.ShoupRubinBella

21:20:09 HOL-Auth: theory HOL-Auth.Auth_Smartcard

21:20:14 Timing HOL-Nonstandard_Analysis (2 threads, 11.792s elapsed time, 22.032s cpu time, 1.052s GC time, factor 1.87)

21:20:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

21:20:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

21:20:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

21:20:14 Finished HOL-Nonstandard_Analysis (0:00:35 elapsed time, 0:00:54 cpu time, factor 1.53)

21:20:14 Building HOL-Nominal ...

21:20:16 HOL-Nominal: theory HOL-Nominal.Nominal

21:20:40 Timing HOL-Nominal (2 threads, 7.539s elapsed time, 13.500s cpu time, 0.740s GC time, factor 1.79)

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

21:20:40 Finished HOL-Nominal (0:00:25 elapsed time, 0:00:37 cpu time, factor 1.44)

21:20:40 Building HOL-Eisbach ...

21:20:41 HOL-Eisbach: theory HOL-Eisbach.Eisbach

21:20:41 HOL-Eisbach: theory IFOL

21:20:42 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

21:20:42 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

21:20:42 HOL-Eisbach: theory HOL-Eisbach.Examples

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

21:20:43 HOL-Eisbach: theory FOL

21:20:45 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

21:20:56 Timing HOL-Eisbach (2 threads, 3.923s elapsed time, 7.832s cpu time, 0.164s GC time, factor 2.00)

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

21:20:56 Finished HOL-Eisbach (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.47)

21:20:56 Building Codegen_Basics ...

21:20:57 Codegen_Basics: theory Codegen_Basics.Setup

21:21:15 Timing Codegen_Basics (2 threads, 1.423s elapsed time, 1.544s cpu time, 0.000s GC time, factor 1.08)

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

21:21:15 Finished Codegen_Basics (0:00:18 elapsed time, 0:00:23 cpu time, factor 1.28)

21:21:15 Building Typeclass_Hierarchy_Basics ...

21:21:16 Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup

21:21:33 Timing Typeclass_Hierarchy_Basics (2 threads, 0.841s elapsed time, 0.956s cpu time, 0.000s GC time, factor 1.14)

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

21:21:33 Finished Typeclass_Hierarchy_Basics (0:00:17 elapsed time, 0:00:21 cpu time, factor 1.28)

21:21:33 Building HOL-Mirabelle ...

21:21:34 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle

21:21:34 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test

21:21:44 Timing HOL-Mirabelle (2 threads, 0.526s elapsed time, 0.604s cpu time, 0.000s GC time, factor 1.15)

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

21:21:44 Finished HOL-Mirabelle (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.23)

21:21:44 Running HOL-Nominal-Examples ...

21:21:46 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine

21:21:46 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi

21:21:49 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1

21:22:00 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile

21:22:23 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts

21:22:27 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary

21:22:32 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub

21:22:41 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height

21:22:43 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs

21:22:47 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR

21:22:47 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN

21:22:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu

21:22:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening

21:22:57 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern

21:23:07 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS

21:23:11 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization

21:23:14 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support

21:23:15 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation

21:23:19 HOL-Nominal-Examples: theory HOL-Nominal-Examples.W

21:23:26 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening

21:23:39 Timing HOL-Auth (2 threads, 209.324s elapsed time, 322.736s cpu time, 10.616s GC time, factor 1.54)

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

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

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

21:23:39 Finished HOL-Auth (0:04:00 elapsed time, 0:06:07 cpu time, factor 1.53)

21:23:39 Running HOL-Decision_Procs ...

21:23:41 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions

21:23:41 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library

21:23:41 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order

21:23:42 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux

21:23:43 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring

21:23:44 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex

21:23:45 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper

21:23:56 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete

21:23:56 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field

21:24:12 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex

21:24:14 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack

21:24:33 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2

21:24:37 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3

21:24:48 Timing HOL-Analysis (2 threads, 821.420s elapsed time, 1438.008s cpu time, 39.936s GC time, factor 1.75)

21:24:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

21:24:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

21:24:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf

21:24:48 Finished HOL-Analysis (0:15:17 elapsed time, 0:26:10 cpu time, factor 1.71)

21:24:48 Building HOL-Probability ...

21:24:49 HOL-Probability: theory HOL-Library.Adhoc_Overloading

21:24:49 HOL-Probability: theory HOL-Library.Lattice_Syntax

21:24:49 HOL-Probability: theory HOL-Library.AList

21:24:49 HOL-Probability: theory HOL-Library.Complete_Partial_Order2

21:24:51 HOL-Probability: theory HOL-Library.Mapping

21:24:52 HOL-Probability: theory HOL-Library.AList_Mapping

21:24:53 HOL-Probability: theory HOL-Library.Monad_Syntax

21:24:53 HOL-Probability: theory HOL-Library.Stream

21:24:53 HOL-Probability: theory HOL-Library.Rewrite

21:24:54 HOL-Probability: theory HOL-Library.Sublist

21:24:55 HOL-Probability: theory HOL-Library.Tree

21:24:56 HOL-Probability: theory HOL-Library.FSet

21:24:58 HOL-Probability: theory HOL-Library.Diagonal_Subsequence

21:24:58 HOL-Probability: theory HOL-Library.Multiset_Permutations

21:24:59 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams

21:25:01 HOL-Probability: theory HOL-Library.Finite_Map

21:25:01 HOL-Probability: theory HOL-Probability.Discrete_Topology

21:25:02 HOL-Probability: theory HOL-Probability.Essential_Supremum

21:25:02 HOL-Probability: theory HOL-Probability.Probability_Measure

21:25:03 HOL-Probability: theory HOL-Probability.Fin_Map

21:25:04 HOL-Probability: theory HOL-Probability.Conditional_Expectation

21:25:05 HOL-Probability: theory HOL-Probability.Distribution_Functions

21:25:05 HOL-Probability: theory HOL-Probability.Giry_Monad

21:25:05 HOL-Probability: theory HOL-Probability.Weak_Convergence

21:25:07 HOL-Probability: theory HOL-Probability.Helly_Selection

21:25:09 HOL-Probability: theory HOL-Probability.Stopping_Time

21:25:09 HOL-Probability: theory HOL-Probability.Probability_Mass_Function

21:25:10 HOL-Probability: theory HOL-Probability.Projective_Family

21:25:11 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure

21:25:12 HOL-Probability: theory HOL-Probability.PMF_Impl

21:25:12 HOL-Probability: theory HOL-Probability.Random_Permutations

21:25:13 HOL-Probability: theory HOL-Probability.SPMF

21:25:14 HOL-Probability: theory HOL-Probability.Independent_Family

21:25:16 HOL-Probability: theory HOL-Probability.Convolution

21:25:16 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR

21:25:16 HOL-Probability: theory HOL-Probability.Information

21:25:18 HOL-Probability: theory HOL-Probability.Projective_Limit

21:25:19 HOL-Probability: theory HOL-Probability.Distributions

21:25:20 HOL-Probability: theory HOL-Probability.Stream_Space

21:25:21 HOL-Probability: theory HOL-Probability.Tree_Space

21:25:21 HOL-Probability: theory HOL-Probability.Characteristic_Functions

21:25:22 HOL-Probability: theory HOL-Probability.Sinc_Integral

21:25:22 HOL-Probability: theory HOL-Probability.Levy

21:25:23 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem

21:25:24 HOL-Probability: theory HOL-Probability.Probability

21:25:57 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List

21:26:15 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair

21:26:15 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial

21:26:27 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff

21:27:38 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds

21:27:43 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation

21:28:31 Timing HOL-Probability (2 threads, 183.897s elapsed time, 331.632s cpu time, 14.144s GC time, factor 1.80)

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

21:28:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

21:28:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

21:28:31 Finished HOL-Probability (0:03:42 elapsed time, 0:06:24 cpu time, factor 1.72)

21:28:31 Running HOL-Data_Structures ...

21:28:32 HOL-Data_Structures: theory HOL-Data_Structures.Less_False

21:28:32 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less

21:28:32 HOL-Data_Structures: theory HOL-Data_Structures.Cmp

21:28:32 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del

21:28:33 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del

21:28:33 HOL-Data_Structures: theory HOL-Data_Structures.Map_by_Ordered

21:28:33 HOL-Data_Structures: theory HOL-Data_Structures.Tree2

21:28:34 HOL-Data_Structures: theory HOL-Data_Structures.Set_by_Ordered

21:28:34 HOL-Data_Structures: theory HOL-Data_Structures.Tree23

21:28:34 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex

21:28:35 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex

21:28:35 HOL-Data_Structures: theory HOL-Data_Structures.Isin2

21:28:35 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set

21:28:36 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2

21:28:36 HOL-Data_Structures: theory HOL-Data_Structures.RBT

21:28:37 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map

21:28:38 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set

21:28:40 HOL-Data_Structures: theory HOL-Data_Structures.Tree234

21:28:43 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set

21:28:46 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map

21:28:53 HOL-Data_Structures: theory HOL-Library.Cancellation

21:28:53 HOL-Data_Structures: theory HOL-Library.Multiset

21:28:54 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs

21:28:59 HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue

21:28:59 HOL-Data_Structures: theory HOL-Library.Pattern_Aliases

21:28:59 HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS

21:28:59 HOL-Data_Structures: theory HOL-Library.Tree

21:29:02 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set

21:29:06 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map

21:29:07 HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap

21:29:11 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap

21:29:13 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set

21:29:15 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map

21:29:19 HOL-Data_Structures: theory HOL-Data_Structures.Sorting

21:29:20 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map

21:29:21 HOL-Data_Structures: theory HOL-Library.Tree_Real

21:29:22 HOL-Data_Structures: theory HOL-Data_Structures.Balance

21:29:22 HOL-Data_Structures: theory HOL-Number_Theory.Fib

21:29:23 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set

21:29:25 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map

21:29:25 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set

21:30:58 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map

21:33:09 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition

21:33:14 Timing HOL-Nominal-Examples (2 threads, 686.657s elapsed time, 1245.008s cpu time, 120.776s GC time, factor 1.81)

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

21:33:14 Finished HOL-Nominal-Examples (0:11:29 elapsed time, 0:20:47 cpu time, factor 1.81)

21:33:14 Running HOL-Codegenerator_Test ...

21:33:16 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp

21:33:16 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False

21:33:16 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less

21:33:16 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del

21:33:16 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del

21:33:17 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_by_Ordered

21:33:17 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML

21:33:17 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala

21:33:17 HOL-Codegenerator_Test: theory HOL-ex.Records

21:33:17 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_by_Ordered

21:33:17 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set

21:33:18 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map

21:33:22 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates

21:33:26 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate

21:33:32 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat

21:34:58 Timing HOL-Decision_Procs (2 threads, 675.263s elapsed time, 1282.440s cpu time, 121.824s GC time, factor 1.90)

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

21:34:58 Finished HOL-Decision_Procs (0:11:18 elapsed time, 0:21:25 cpu time, factor 1.89)

21:34:58 Running HOL-ex ...

21:35:00 HOL-ex: theory HOL-ex.Computations

21:35:00 HOL-ex: theory HOL-ex.Bubblesort

21:35:00 HOL-ex: theory HOL-ex.MergeSort

21:35:02 HOL-ex: theory HOL-ex.Quicksort

21:35:02 HOL-ex: theory HOL-ex.IArray_Examples

21:35:02 HOL-ex: theory HOL-ex.Perm_Fragments

21:35:02 HOL-ex: theory HOL-ex.Refute_Examples

21:35:02 HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples

21:35:03 HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex

21:35:04 HOL-ex: theory HOL-ex.While_Combinator_Example

21:35:04 HOL-ex: theory HOL-ex.Code_Timing

21:35:06 HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples

21:35:06 HOL-ex: theory HOL-ex.Antiquote

21:35:06 HOL-ex: theory HOL-ex.Arith_Examples

21:35:06 HOL-ex: theory HOL-ex.Birthday_Paradox

21:35:06 HOL-ex: theory HOL-ex.CTL

21:35:07 HOL-ex: theory HOL-ex.Cartouche_Examples

21:35:07 HOL-ex: theory HOL-ex.Case_Product