Skip to content
[Jenkins]Jenkins
log in
Aborted

Console Output

01:33:13 Started by an SCM change


01:33:13 [EnvInject] - Loading node environment variables.


01:33:13 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow


01:33:13 [isabelle-nightly-slow] $ hg showconfig paths.default


01:33:13 [isabelle-nightly-slow] $ hg pull --rev default


01:33:14 pulling from http://isabelle.in.tum.de/repos/isabelle/


01:33:14 searching for changes


01:33:14 no changes found


01:33:14 [isabelle-nightly-slow] $ hg update --clean --rev default


01:33:14 4 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:33:14 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all


01:33:14 [isabelle-nightly-slow] $ hg log --rev . --template {node}


01:33:14 [isabelle-nightly-slow] $ hg log --rev . --template {rev}


01:33:15 [isabelle-nightly-slow] $ hg log --rev b9a5805d1d702252f3732787a48e8902b82fffff --template exists\n


01:33:15 exists


01:33:15 [isabelle-nightly-slow] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(b9a5805d1d702252f3732787a48e8902b82fffff)" --encoding UTF-8 --encodingmode replace


01:33:15 [afp] $ hg showconfig paths.default


01:33:15 [afp] $ hg pull --rev default


01:33:16 pulling from https://bitbucket.org/isa-afp/afp-devel/


01:33:16 no changes found


01:33:16 [afp] $ hg update --clean --rev default


01:33:16 0 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:33:16 [afp] $ hg --config extensions.purge= clean --all


01:33:16 [afp] $ hg log --rev . --template {node}


01:33:17 [afp] $ hg log --rev . --template {rev}


01:33:17 [afp] $ hg log --rev c380272ea50c12a8f6e19eb6741ef19f45de8345 --template exists\n


01:33:17 exists


01:33:17 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(c380272ea50c12a8f6e19eb6741ef19f45de8345)" --encoding UTF-8 --encodingmode replace


01:33:17 No emails were triggered.


01:33:17 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins7425650349080565792.sh


01:33:17 + Admin/jenkins/run_build slow


01:33:17 + set -e


01:33:17 + PROFILE=slow


01:33:17 + shift


01:33:17 + bin/isabelle components -a


01:33:17 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/polyml-test-b68438d33c69"


01:33:17 Getting "https://isabelle.in.tum.de/components/polyml-test-b68438d33c69.tar.gz"


01:33:18 Unpacking "/media/data/jenkins/.isabelle/contrib/polyml-test-b68438d33c69.tar.gz"


01:33:19 + bin/isabelle jedit -bf


01:33:19 ### Building graph browser ...


01:33:19 warning: [options] bootstrap class path not set in conjunction with -source 6


01:33:19 warning: [options] source value 6 is obsolete and will be removed in a future release


01:33:19 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.


01:33:21 Note: Some input files use or override a deprecated API.


01:33:21 Note: Recompile with -Xlint:deprecation for details.


01:33:21 Note: Some input files use unchecked or unsafe operations.


01:33:21 Note: Recompile with -Xlint:unchecked for details.


01:33:21 3 warnings


01:33:21 ### Building Isabelle/Scala ...


01:34:20 ### Building Isabelle/jEdit ...


01:34:54 + bin/isabelle ocaml_setup


01:34:55 # To setup the new switch in the current shell, you need to run:


01:34:55 eval `opam config env`


01:34:55 + bin/isabelle ghc_setup


01:34:56 stack will use a sandboxed GHC it installed


01:34:56 For more information on paths, see 'stack path' and 'stack exec env'


01:34:56 To use this GHC and packages outside of a project, consider using:


01:34:56 stack ghc, stack ghci, stack runghc, or stack exec


01:34:56 The Glorious Glasgow Haskell Compilation System, version 8.4.4


01:34:56 + bin/isabelle ci_build_slow


01:35:03 

01:35:03 === CONFIGURATION ===


01:35:03 

01:35:03 ISABELLE_BUILD_OPTIONS=""


01:35:03 

01:35:03 ML_PLATFORM="x86_64-linux"


01:35:03 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-b68438d33c69/x86_64-linux"


01:35:03 ML_SYSTEM="polyml-5.7.1"


01:35:03 ML_OPTIONS="-H 4000 --maxheap 20G"


01:35:04 jobs = 1, threads = 8, numa = false


01:35:04 

01:35:04 === BUILD ===


01:35:04 

01:35:04 Build started at Sat, 2 Feb 2019 01:35:03 +0100


01:35:04 Isabelle id 76f2d492627e


01:35:04 Build for AFP id c380272ea50c


01:35:04 

01:35:04 === LOG ===


01:35:04 

01:35:06 Session Pure/Pure


01:35:07 Session FOL/FOL


01:35:07 Session HOL/HOL (main)


01:35:08 Session AFP/AWN (AFP)


01:35:08 Session AFP/AODV (AFP slow)


01:35:09 Session HOL/HOL-Eisbach


01:35:09 Session HOL/HOL-Library (main timing)


01:35:10 Session AFP/Binomial-Heaps (AFP)


01:35:10 Session AFP/ConcurrentIMP (AFP)


01:35:10 Session AFP/ConcurrentGC (AFP slow)


01:35:10 Session AFP/FinFun (AFP)


01:35:10 Session AFP/Finger-Trees (AFP)


01:35:10 Session HOL/HOL-Computational_Algebra (main timing)


01:35:10 Session HOL/HOL-Algebra (main timing)


01:35:11 Session HOL/HOL-Analysis (main timing)


01:35:11 Session AFP/Coinductive (AFP)


01:35:12 Session HOL/HOL-Number_Theory (main timing)


01:35:12 Session HOL/HOL-ex (timing)


01:35:12 Session AFP/Automatic_Refinement (AFP)


01:35:13 Session HOL/HOL-Imperative_HOL (timing)


01:35:13 Session AFP/Trie (AFP)


01:35:13 Session AFP/Flyspeck-Tame (AFP slow very_slow)


01:35:13 Session HOL/HOL-Word (main timing)


01:35:14 Session AFP/Native_Word (AFP)


01:35:14 Session AFP/Refine_Monadic (AFP)


01:35:14 Session AFP/Collections (AFP)


01:35:15 Session AFP/Word_Lib (AFP)


01:35:15 Session AFP/IP_Addresses (AFP)


01:35:16 Session AFP/Simple_Firewall (AFP)


01:35:16 Session AFP/Routing (AFP)


01:35:16 Session AFP/Iptables_Semantics (AFP)


01:35:16 Session AFP/Iptables_Semantics_Examples (AFP)


01:35:17 Session AFP/Iptables_Semantics_Examples_Big (AFP large slow very_slow)


01:35:17 Session AFP/JinjaThreads (AFP slow)


01:35:20 Building Pure ...


01:35:50 Pure: theory Pure


01:35:51 Pure: theory ML_Bootstrap


01:35:51 Pure: theory Pure.Sessions


01:35:54 Timing Pure (1 threads, 1.546s elapsed time, 1.504s cpu time, 0.000s GC time, factor 0.97)


01:35:54 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure


01:35:54 Finished Pure (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00)


01:35:54 Building HOL ...


01:35:58 HOL: theory HOL.Code_Generator


01:36:05 HOL: theory HOL.HOL


01:36:11 HOL: theory HOL.Argo


01:36:11 HOL: theory HOL.Ctr_Sugar


01:36:11 HOL: theory HOL.Orderings


01:36:13 HOL: theory HOL.Groups


01:36:14 HOL: theory HOL.SAT


01:36:17 HOL: theory HOL.Lattices


01:36:19 HOL: theory HOL.Set


01:36:21 HOL: theory HOL.Fun


01:36:21 HOL: theory HOL.Typedef


01:36:22 HOL: theory HOL.Complete_Lattices


01:36:22 HOL: theory HOL.Rings


01:36:26 HOL: theory HOL.Inductive


01:36:29 HOL: theory HOL.Product_Type


01:36:29 HOL: theory HOL.Sum_Type


01:36:31 HOL: theory HOL.Complete_Partial_Order


01:36:37 HOL: theory HOL.Nat


01:36:40 HOL: theory HOL.Fields


01:36:40 HOL: theory HOL.Meson


01:36:41 HOL: theory HOL.ATP


01:36:46 HOL: theory HOL.Metis


01:36:47 HOL: theory HOL.Finite_Set


01:36:50 HOL: theory HOL.Relation


01:36:52 HOL: theory HOL.Transitive_Closure


01:36:53 HOL: theory HOL.Wellfounded


01:36:54 HOL: theory HOL.Fun_Def_Base


01:36:54 HOL: theory HOL.Hilbert_Choice


01:36:54 HOL: theory HOL.Wfrec


01:36:54 HOL: theory HOL.Order_Relation


01:36:55 HOL: theory HOL.BNF_Wellorder_Relation


01:36:56 HOL: theory HOL.BNF_Wellorder_Embedding


01:36:56 HOL: theory HOL.Zorn


01:36:57 HOL: theory HOL.BNF_Wellorder_Constructions


01:36:58 HOL: theory HOL.BNF_Cardinal_Order_Relation


01:36:59 HOL: theory HOL.BNF_Cardinal_Arithmetic


01:37:00 HOL: theory HOL.BNF_Def


01:37:04 HOL: theory HOL.BNF_Composition


01:37:04 HOL: theory HOL.Basic_BNFs


01:37:06 HOL: theory HOL.BNF_Fixpoint_Base


01:37:11 HOL: theory HOL.BNF_Least_Fixpoint


01:37:17 HOL: theory HOL.Basic_BNF_LFPs


01:37:17 HOL: theory HOL.Transfer


01:37:19 HOL: theory HOL.Num


01:37:23 HOL: theory HOL.Power


01:37:27 HOL: theory HOL.Groups_Big


01:37:30 HOL: theory HOL.Equiv_Relations


01:37:31 HOL: theory HOL.Lifting


01:37:33 HOL: theory HOL.Lifting_Set


01:37:33 HOL: theory HOL.Option


01:37:33 HOL: theory HOL.Quotient


01:37:34 HOL: theory HOL.Extraction


01:37:34 HOL: theory HOL.Lattices_Big


01:37:34 HOL: theory HOL.Partial_Function


01:37:36 HOL: theory HOL.Fun_Def


01:37:39 HOL: theory HOL.Int


01:37:44 HOL: theory HOL.Euclidean_Division


01:37:52 HOL: theory HOL.Parity


01:37:56 HOL: theory HOL.Divides


01:38:00 HOL: theory HOL.Code_Numeral


01:38:00 HOL: theory HOL.Numeral_Simprocs


01:38:00 HOL: theory HOL.SMT


01:38:00 HOL: theory HOL.Set_Interval


01:38:02 HOL: theory HOL.Semiring_Normalization


01:38:06 HOL: theory HOL.Groebner_Basis


01:38:08 HOL: theory HOL.Conditionally_Complete_Lattices


01:38:08 HOL: theory HOL.Filter


01:38:09 HOL: theory HOL.Presburger


01:38:15 HOL: theory HOL.Sledgehammer


01:38:20 HOL: theory HOL.List


01:38:35 HOL: theory HOL.Groups_List


01:38:35 HOL: theory HOL.Map


01:38:37 HOL: theory HOL.Factorial


01:38:37 HOL: theory HOL.GCD


01:38:37 HOL: theory HOL.Enum


01:38:37 HOL: theory HOL.Random


01:38:39 HOL: theory HOL.Binomial


01:38:45 HOL: theory HOL.String


01:38:48 HOL: theory HOL.BNF_Greatest_Fixpoint


01:38:49 HOL: theory HOL.Predicate


01:38:49 HOL: theory HOL.Typerep


01:38:51 HOL: theory HOL.Lazy_Sequence


01:38:53 HOL: theory HOL.Limited_Sequence


01:38:54 HOL: theory HOL.Code_Evaluation


01:38:58 HOL: theory HOL.Quickcheck_Random


01:39:05 HOL: theory HOL.Quickcheck_Exhaustive


01:39:05 HOL: theory HOL.Quickcheck_Narrowing


01:39:05 HOL: theory HOL.Random_Pred


01:39:06 HOL: theory HOL.Random_Sequence


01:39:14 HOL: theory HOL.Record


01:39:14 HOL: theory HOL.Predicate_Compile


01:39:17 HOL: theory HOL.Nitpick


01:39:27 HOL: theory HOL.Nunchaku


01:39:29 HOL: theory Main


01:39:31 HOL: theory HOL.Archimedean_Field


01:39:31 HOL: theory HOL.Hull


01:39:31 HOL: theory HOL.Topological_Spaces


01:39:31 HOL: theory HOL.Modules


01:39:33 HOL: theory HOL.Vector_Spaces


01:39:45 HOL: theory HOL.Rat


01:39:49 HOL: theory HOL.Real


01:39:52 HOL: theory HOL.Real_Vector_Spaces


01:40:10 HOL: theory HOL.Inequalities


01:40:10 HOL: theory HOL.Limits


01:40:19 HOL: theory HOL.Deriv


01:40:19 HOL: theory HOL.Series


01:40:23 HOL: theory HOL.NthRoot


01:40:23 HOL: theory HOL.Transcendental


01:40:32 HOL: theory HOL.Complex


01:40:34 HOL: theory HOL.MacLaurin


01:40:34 HOL: theory Complex_Main


01:42:23 Timing HOL (8 threads, 290.005s elapsed time, 1002.072s cpu time, 97.512s GC time, factor 3.46)


01:42:23 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL


01:42:23 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf


01:42:23 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf


01:42:23 Finished HOL (0:06:24 elapsed time, 0:19:43 cpu time, factor 3.07)


01:42:23 Running Flyspeck-Tame ...


01:42:24 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order


01:42:24 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl


01:42:24 Flyspeck-Tame: theory HOL-Library.AList


01:42:24 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat


01:42:24 Flyspeck-Tame: theory Flyspeck-Tame.ListAux


01:42:24 Flyspeck-Tame: theory HOL-Library.Code_Target_Int


01:42:24 Flyspeck-Tame: theory HOL-Library.IArray


01:42:24 Flyspeck-Tame: theory HOL-Library.While_Combinator


01:42:24 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat


01:42:24 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso


01:42:25 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral


01:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Arch


01:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Worklist


01:42:25 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax


01:42:26 Flyspeck-Tame: theory Flyspeck-Tame.ListSum


01:42:26 Flyspeck-Tame: theory Flyspeck-Tame.Rotation


01:42:27 Flyspeck-Tame: theory Flyspeck-Tame.Graph


01:42:27 Flyspeck-Tame: theory Flyspeck-Tame.Maps


01:42:27 Flyspeck-Tame: theory Trie.Trie


01:42:29 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision


01:42:29 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps


01:42:30 Flyspeck-Tame: theory Flyspeck-Tame.Tame


01:42:30 Flyspeck-Tame: theory Trie.Tries


01:42:31 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator


01:42:32 Flyspeck-Tame: theory Flyspeck-Tame.TameProps


01:42:32 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps


01:42:32 Flyspeck-Tame: theory Flyspeck-Tame.Plane


01:42:33 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps


01:42:33 Flyspeck-Tame: theory Flyspeck-Tame.Plane1


01:42:34 Flyspeck-Tame: theory Flyspeck-Tame.Generator


01:42:34 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum


01:42:41 Flyspeck-Tame: theory Flyspeck-Tame.Invariants


01:42:43 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux


01:42:44 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps


01:42:44 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps


01:42:44 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props


01:42:45 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound


01:42:45 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps


01:42:46 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps


01:42:46 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps


01:42:47 Flyspeck-Tame: theory Flyspeck-Tame.ArchComp


01:42:47 Flyspeck-Tame: theory Flyspeck-Tame.Completeness


15:42:29 *** Timeout


15:42:29 Flyspeck-Tame FAILED


15:42:29 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7.1_x86_64-linux/log/Flyspeck-Tame)


15:42:29 ###           ("_position" v))))))


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("_applC"


15:42:29 ###     ("\<^const>Graph.nextFace"


15:42:29 ###       ("\<^const>HOL.eq" ("_position" u) ("_position" f)))


15:42:29 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###         ("_position" v)))))


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("\<^const>HOL.eq" ("_position" u)


15:42:29 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f))


15:42:29 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###         ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###           ("_position" v))))))


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("\<^const>HOL.eq" ("_position" u)


15:42:29 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###         ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###           ("_position" v))))))


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("_applC"


15:42:29 ###     ("\<^const>Graph.nextFace"


15:42:29 ###       ("\<^const>HOL.eq" ("_position" u) ("_position" f)))


15:42:29 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f))


15:42:29 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))


15:42:29 ###         ("_position" v)))))


15:42:29 ### Fortunately, only one parse tree is well-formed and type-correct,


15:42:29 ### but you may still want to disambiguate your grammar or your input.


15:42:29 ### Ambiguous input (line 234 of "~~/afp/thys/Flyspeck-Tame/GeneratorProps.thy") produces 2 parse trees:


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("\<^const>HOL.eq"


15:42:29 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f)) ("_position" u))


15:42:29 ###     ("_position" v)))


15:42:29 ### ("\<^const>HOL.Trueprop"


15:42:29 ###   ("\<^const>HOL.eq"


15:42:29 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f)) ("_position" u))


15:42:29 ###     ("_position" v)))


15:42:29 ### Fortunately, only one parse tree is well-formed and type-correct,


15:42:29 ### but you may still want to disambiguate your grammar or your input.


15:42:29 Running JinjaThreads ...


15:42:32 JinjaThreads: theory HOL-Eisbach.Eisbach


15:42:32 JinjaThreads: theory Automatic_Refinement.Foldi


15:42:32 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1


15:42:32 JinjaThreads: theory Automatic_Refinement.Prio_List


15:42:32 JinjaThreads: theory Collections.ICF_Tools


15:42:32 JinjaThreads: theory Finger-Trees.FingerTree


15:42:32 JinjaThreads: theory HOL-Library.AList


15:42:32 JinjaThreads: theory HOL-Library.Adhoc_Overloading


15:42:32 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot


15:42:32 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot


15:42:32 JinjaThreads: theory HOL-Library.Monad_Syntax


15:42:32 JinjaThreads: theory Collections.Ord_Code_Preproc


15:42:32 JinjaThreads: theory HOL-Library.Bit


15:42:33 JinjaThreads: theory HOL-Library.Boolean_Algebra


15:42:33 JinjaThreads: theory HOL-Library.Cancellation


15:42:33 JinjaThreads: theory Collections.Locale_Code


15:42:33 JinjaThreads: theory Automatic_Refinement.Refine_Util


15:42:33 JinjaThreads: theory Collections.Record_Intf


15:42:33 JinjaThreads: theory HOL-Library.Case_Converter


15:42:33 JinjaThreads: theory HOL-Library.Code_Abstract_Nat


15:42:33 JinjaThreads: theory HOL-Library.Code_Target_Nat


15:42:33 JinjaThreads: theory HOL-Library.Code_Target_Int


15:42:33 JinjaThreads: theory HOL-Library.Simps_Case_Conv


15:42:34 JinjaThreads: theory HOL-Library.Dlist


15:42:34 JinjaThreads: theory Automatic_Refinement.Anti_Unification


15:42:34 JinjaThreads: theory Automatic_Refinement.Attr_Comb


15:42:34 JinjaThreads: theory Automatic_Refinement.Autoref_Data


15:42:34 JinjaThreads: theory Automatic_Refinement.Indep_Vars


15:42:34 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp


15:42:34 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms


15:42:34 JinjaThreads: theory Automatic_Refinement.Tagged_Solver


15:42:34 JinjaThreads: theory Automatic_Refinement.Select_Solve


15:42:34 JinjaThreads: theory HOL-Library.Multiset


15:42:34 JinjaThreads: theory HOL-Library.Infinite_Set


15:42:34 JinjaThreads: theory HOL-Library.Code_Target_Numeral


15:42:34 JinjaThreads: theory HOL-Library.Lattice_Syntax


15:42:34 JinjaThreads: theory HOL-Library.Complete_Partial_Order2


15:42:34 JinjaThreads: theory HOL-Library.Nat_Bijection


15:42:34 JinjaThreads: theory HOL-Library.Old_Datatype


15:42:35 JinjaThreads: theory HOL-Library.Option_ord


15:42:35 JinjaThreads: theory HOL-Library.Phantom_Type


15:42:35 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs


15:42:35 JinjaThreads: theory HOL-Library.RBT_Impl


15:42:35 JinjaThreads: theory Trie.Trie


15:42:35 JinjaThreads: theory HOL-Library.Sublist


15:42:36 JinjaThreads: theory HOL-Library.Transitive_Closure_Table


15:42:36 JinjaThreads: theory HOL-Library.Cardinality


15:42:36 JinjaThreads: theory HOL-Library.While_Combinator


15:42:37 JinjaThreads: theory Collections.DatRef


15:42:38 JinjaThreads: theory HOL-Word.Bits


15:42:38 JinjaThreads: theory FinFun.FinFun


15:42:38 JinjaThreads: theory HOL-Library.Numeral_Type


15:42:39 JinjaThreads: theory HOL-Word.Bits_Bit


15:42:40 JinjaThreads: theory HOL-Word.Misc_Numeric


15:42:40 JinjaThreads: theory HOL-Word.Bit_Representation


15:42:40 JinjaThreads: theory HOL-Word.Word_Miscellaneous


15:42:40 JinjaThreads: theory HOL-Word.Misc_Typedef


15:42:40 JinjaThreads: theory HOL-Library.Countable


15:42:40 JinjaThreads: theory JinjaThreads.Set_Monad


15:42:40 JinjaThreads: theory JinjaThreads.Set_without_equal


15:42:41 JinjaThreads: theory Refine_Monadic.Refine_Chapter


15:42:41 JinjaThreads: theory HOL-Word.Bits_Int


15:42:41 JinjaThreads: theory HOL-Library.Type_Length


15:42:42 JinjaThreads: theory HOL-Library.Countable_Set


15:42:42 JinjaThreads: theory Binomial-Heaps.BinomialHeap


15:42:42 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap


15:42:43 JinjaThreads: theory HOL-ex.Quicksort


15:42:43 JinjaThreads: theory HOL-Word.Bool_List_Representation


15:42:43 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices


15:42:43 JinjaThreads: theory Automatic_Refinement.Misc


15:42:44 JinjaThreads: theory JinjaThreads.Auxiliary


15:42:45 JinjaThreads: theory Native_Word.More_Bits_Int


15:42:48 JinjaThreads: theory HOL-Word.Word


15:42:49 JinjaThreads: theory HOL-Library.Order_Continuity


15:42:50 JinjaThreads: theory Native_Word.Bits_Integer


15:42:50 JinjaThreads: theory HOL-Library.Extended_Nat


15:42:51 JinjaThreads: theory Coinductive.Coinductive_Nat


15:42:53 JinjaThreads: theory Coinductive.Coinductive_List


15:42:55 JinjaThreads: theory Automatic_Refinement.Refine_Lib


15:42:55 JinjaThreads: theory Collections.SetIterator


15:42:55 JinjaThreads: theory Collections.Sorted_List_Operations


15:42:56 JinjaThreads: theory Automatic_Refinement.Autoref_Phases


15:42:57 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging


15:42:57 JinjaThreads: theory Automatic_Refinement.Relators


15:42:57 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover


15:42:57 JinjaThreads: theory Native_Word.Word_Misc


15:42:57 JinjaThreads: theory Collections.SetIteratorOperations


15:42:59 JinjaThreads: theory Automatic_Refinement.Param_Tool


15:42:59 JinjaThreads: theory Automatic_Refinement.Param_HOL


15:43:01 JinjaThreads: theory Collections.Assoc_List


15:43:01 JinjaThreads: theory Automatic_Refinement.Parametricity


15:43:01 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops


15:43:01 JinjaThreads: theory Collections.Dlist_add


15:43:01 JinjaThreads: theory Collections.Proper_Iterator


15:43:02 JinjaThreads: theory Collections.SetIteratorGA


15:43:02 JinjaThreads: theory Collections.Diff_Array


15:43:02 JinjaThreads: theory Collections.Trie_Impl


15:43:03 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel


15:43:03 JinjaThreads: theory Collections.Trie2


15:43:04 JinjaThreads: theory Collections.It_to_It


15:43:04 JinjaThreads: theory Automatic_Refinement.Autoref_Translate


15:43:04 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface


15:43:04 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo


15:43:05 JinjaThreads: theory Automatic_Refinement.Autoref_Tool


15:43:07 JinjaThreads: theory Coinductive.Lazy_LList


15:43:07 JinjaThreads: theory Coinductive.TLList


15:43:07 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL


15:43:14 JinjaThreads: theory Coinductive.Lazy_TLList


15:43:15 JinjaThreads: theory Native_Word.Code_Target_Bits_Int


15:43:15 JinjaThreads: theory Native_Word.Uint32


15:43:15 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement


15:43:15 JinjaThreads: theory Collections.Idx_Iterator


15:43:15 JinjaThreads: theory Refine_Monadic.Refine_Misc


15:43:15 JinjaThreads: theory Collections.Code_Target_ICF


15:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Domain


15:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Transfer


15:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Assert


15:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Recursion


15:43:18 JinjaThreads: theory Refine_Monadic.RefineG_While


15:43:18 JinjaThreads: theory Refine_Monadic.Refine_Basic


15:43:19 JinjaThreads: theory Collections.HashCode


15:43:19 JinjaThreads: theory Refine_Monadic.Refine_Det


15:43:24 JinjaThreads: theory Refine_Monadic.Refine_Heuristics


15:43:24 JinjaThreads: theory Refine_Monadic.Refine_Leof


15:43:24 JinjaThreads: theory Refine_Monadic.Refine_Pfun


15:43:24 JinjaThreads: theory Refine_Monadic.Refine_More_Comb


15:43:24 JinjaThreads: theory Refine_Monadic.Refine_While


15:43:27 JinjaThreads: theory Refine_Monadic.Refine_Transfer


15:43:28 JinjaThreads: theory Refine_Monadic.Autoref_Monadic


15:43:28 JinjaThreads: theory Refine_Monadic.Refine_Automation


15:43:28 JinjaThreads: theory Refine_Monadic.Refine_Foreach


15:43:32 JinjaThreads: theory Refine_Monadic.Refine_Monadic


15:43:33 JinjaThreads: theory Collections.Gen_Iterator


15:43:33 JinjaThreads: theory Collections.Intf_Map


15:43:33 JinjaThreads: theory Collections.Intf_Set


15:43:34 JinjaThreads: theory Collections.Iterator


15:43:35 JinjaThreads: theory Collections.Array_Iterator


15:43:35 JinjaThreads: theory Collections.ICF_Spec_Base


15:43:36 JinjaThreads: theory Collections.AnnotatedListSpec


15:43:36 JinjaThreads: theory Collections.ListSpec


15:43:36 JinjaThreads: theory Collections.MapSpec


15:43:36 JinjaThreads: theory Collections.PrioSpec


15:43:36 JinjaThreads: theory Collections.PrioUniqueSpec


15:43:36 JinjaThreads: theory Collections.SetSpec


15:43:38 JinjaThreads: theory Collections.BinoPrioImpl


15:43:38 JinjaThreads: theory Collections.SkewPrioImpl


15:43:38 JinjaThreads: theory Collections.ListGA


15:43:40 JinjaThreads: theory Collections.Fifo


15:43:40 JinjaThreads: theory Collections.FTAnnotatedListImpl


15:43:40 JinjaThreads: theory Collections.PrioByAnnotatedList


15:43:42 JinjaThreads: theory HOL-Library.RBT


15:43:43 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList


15:43:43 JinjaThreads: theory Collections.Algos


15:43:44 JinjaThreads: theory Collections.SetIndex


15:43:44 JinjaThreads: theory Collections.SetIteratorCollectionsGA


15:43:45 JinjaThreads: theory Collections.RBT_add


15:43:45 JinjaThreads: theory Collections.MapGA


15:43:45 JinjaThreads: theory Collections.SetGA


15:43:49 JinjaThreads: theory Collections.FTPrioImpl


15:43:49 JinjaThreads: theory Collections.FTPrioUniqueImpl


15:43:50 JinjaThreads: theory Collections.ArrayMapImpl


15:43:50 JinjaThreads: theory Collections.ListMapImpl


15:43:50 JinjaThreads: theory Collections.ListMapImpl_Invar


15:43:50 JinjaThreads: theory Collections.TrieMapImpl


15:43:50 JinjaThreads: theory Collections.RBTMapImpl


15:43:54 JinjaThreads: theory Collections.ListSetImpl


15:43:56 JinjaThreads: theory Collections.ListSetImpl_Invar


15:43:56 JinjaThreads: theory Collections.ListSetImpl_NotDist


15:43:58 JinjaThreads: theory Collections.ArrayHashMap_Impl


15:43:59 JinjaThreads: theory Collections.ListSetImpl_Sorted


15:44:01 JinjaThreads: theory Collections.SetByMap


15:44:04 JinjaThreads: theory Collections.HashMap_Impl


15:44:04 JinjaThreads: theory Collections.ArraySetImpl


15:44:04 JinjaThreads: theory Collections.TrieSetImpl


15:44:05 JinjaThreads: theory Collections.RBTSetImpl


15:44:06 JinjaThreads: theory Collections.ArrayHashMap


15:44:08 JinjaThreads: theory Collections.HashMap


15:44:16 JinjaThreads: theory Collections.ArrayHashSet


15:44:18 JinjaThreads: theory Collections.HashSet


15:44:18 JinjaThreads: theory Collections.MapStdImpl


15:44:28 JinjaThreads: theory Collections.SetStdImpl


15:44:33 JinjaThreads: theory Collections.ICF_Impl


15:44:41 JinjaThreads: theory Collections.ICF_Refine_Monadic


15:44:41 JinjaThreads: theory Collections.ICF_Autoref


15:44:46 JinjaThreads: theory Collections.Collections


15:44:47 JinjaThreads: theory Collections.CollectionsV1


15:44:58 JinjaThreads: theory JinjaThreads.JT_ICF


15:44:58 JinjaThreads: theory JinjaThreads.Basic_Main


15:45:44 JinjaThreads: theory HOL-Library.Prefix_Order


15:45:44 JinjaThreads: theory JinjaThreads.FWState


15:45:44 JinjaThreads: theory JinjaThreads.LTS


15:45:44 JinjaThreads: theory HOL-Library.Mapping


15:45:44 JinjaThreads: theory JinjaThreads.Type


15:45:44 JinjaThreads: theory JinjaThreads.ListIndex


15:45:44 JinjaThreads: theory JinjaThreads.Orders


15:45:44 JinjaThreads: theory JinjaThreads.Semilat


15:45:45 JinjaThreads: theory JinjaThreads.Err


15:45:46 JinjaThreads: theory HOL-Library.AList_Mapping


15:45:47 JinjaThreads: theory JinjaThreads.Listn


15:45:47 JinjaThreads: theory JinjaThreads.Opt


15:45:47 JinjaThreads: theory JinjaThreads.Product


15:45:48 JinjaThreads: theory JinjaThreads.Semilattices


15:45:48 JinjaThreads: theory JinjaThreads.Typing_Framework


15:45:48 JinjaThreads: theory JinjaThreads.SemilatAlg


15:45:49 JinjaThreads: theory JinjaThreads.Decl


15:45:49 JinjaThreads: theory JinjaThreads.Kildall


15:45:49 JinjaThreads: theory JinjaThreads.LBVSpec


15:45:49 JinjaThreads: theory JinjaThreads.Bisimulation


15:45:50 JinjaThreads: theory JinjaThreads.LBVComplete


15:45:50 JinjaThreads: theory JinjaThreads.LBVCorrect


15:45:50 JinjaThreads: theory JinjaThreads.Typing_Framework_err


15:45:51 JinjaThreads: theory JinjaThreads.Abstract_BV


15:45:52 JinjaThreads: theory JinjaThreads.TypeRel


15:45:57 JinjaThreads: theory JinjaThreads.TypeRelRefine


15:45:57 JinjaThreads: theory JinjaThreads.Value


15:46:02 JinjaThreads: theory JinjaThreads.Exceptions


15:46:02 JinjaThreads: theory JinjaThreads.Heap


15:46:03 JinjaThreads: theory JinjaThreads.SystemClasses


15:46:05 JinjaThreads: theory JinjaThreads.MM


15:46:05 JinjaThreads: theory JinjaThreads.State


15:46:13 JinjaThreads: theory JinjaThreads.FWCondAction


15:46:13 JinjaThreads: theory JinjaThreads.FWInterrupt


15:46:13 JinjaThreads: theory JinjaThreads.FWLock


15:46:13 JinjaThreads: theory JinjaThreads.FWThread


15:46:13 JinjaThreads: theory JinjaThreads.FWWait


15:46:13 JinjaThreads: theory JinjaThreads.Observable_Events


15:46:17 JinjaThreads: theory JinjaThreads.FWLocking


15:46:18 JinjaThreads: theory JinjaThreads.FWLockingThread


15:46:18 JinjaThreads: theory JinjaThreads.FWWellform


15:46:19 JinjaThreads: theory JinjaThreads.FWSemantics


15:46:19 JinjaThreads: theory JinjaThreads.FWLifting


15:46:22 JinjaThreads: theory JinjaThreads.JVMState


15:46:22 JinjaThreads: theory JinjaThreads.StartConfig


15:46:22 JinjaThreads: theory JinjaThreads.JMM_Spec


15:46:23 JinjaThreads: theory JinjaThreads.FWLiftingSem


15:46:23 JinjaThreads: theory JinjaThreads.FWProgressAux


15:46:24 JinjaThreads: theory JinjaThreads.Conform


15:46:24 JinjaThreads: theory JinjaThreads.State_Refinement


15:46:25 JinjaThreads: theory JinjaThreads.FWDeadlock


15:46:26 JinjaThreads: theory JinjaThreads.FWLTS


15:46:27 JinjaThreads: theory JinjaThreads.ConformThreaded


15:46:29 JinjaThreads: theory JinjaThreads.ExternalCall


15:46:29 JinjaThreads: theory JinjaThreads.FWProgress


15:46:29 JinjaThreads: theory JinjaThreads.SC


15:46:30 JinjaThreads: theory JinjaThreads.SC_Collections


15:46:38 JinjaThreads: theory JinjaThreads.JMM_DRF


15:46:38 JinjaThreads: theory JinjaThreads.SC_Legal


15:46:40 JinjaThreads: theory JinjaThreads.FWBisimulation


15:46:41 JinjaThreads: theory JinjaThreads.FWInitFinLift


15:46:41 JinjaThreads: theory JinjaThreads.Non_Speculative


15:46:42 JinjaThreads: theory JinjaThreads.Scheduler


15:46:45 JinjaThreads: theory JinjaThreads.HB_Completion


15:46:46 JinjaThreads: theory JinjaThreads.SC_Completion


15:47:23 JinjaThreads: theory JinjaThreads.WellForm


15:47:24 JinjaThreads: theory JinjaThreads.ExternalCall_Execute


15:47:31 JinjaThreads: theory JinjaThreads.BinOp


15:47:31 JinjaThreads: theory JinjaThreads.ExternalCallWF


15:47:31 JinjaThreads: theory JinjaThreads.JMM_Heap


15:47:39 JinjaThreads: theory JinjaThreads.SemiType


15:47:45 JinjaThreads: theory JinjaThreads.JVM_SemiType


15:47:45 JinjaThreads: theory JinjaThreads.JMM_Type


15:47:45 JinjaThreads: theory JinjaThreads.JMM_Type2


15:47:47 JinjaThreads: theory JinjaThreads.JMM_Framework


15:47:49 JinjaThreads: theory JinjaThreads.Random_Scheduler


15:47:50 JinjaThreads: theory JinjaThreads.Round_Robin


15:48:04 JinjaThreads: theory JinjaThreads.SC_Schedulers


15:48:08 JinjaThreads: theory JinjaThreads.Expr


15:48:13 JinjaThreads: theory JinjaThreads.JVMInstructions


15:48:14 JinjaThreads: theory JinjaThreads.PCompiler


15:48:16 JinjaThreads: theory JinjaThreads.PCompilerRefine


15:48:30 JinjaThreads: theory JinjaThreads.JVMExceptions


15:48:30 JinjaThreads: theory JinjaThreads.JVMHeap


15:48:31 JinjaThreads: theory JinjaThreads.Effect


15:48:37 JinjaThreads: theory JinjaThreads.CallExpr


15:48:37 JinjaThreads: theory JinjaThreads.DefAss


15:48:37 JinjaThreads: theory JinjaThreads.WWellForm


15:48:37 JinjaThreads: theory JinjaThreads.JHeap


15:48:37 JinjaThreads: theory JinjaThreads.WellType


15:48:39 JinjaThreads: theory JinjaThreads.ToString


15:48:40 JinjaThreads: theory JinjaThreads.JVMExecInstr


15:48:46 JinjaThreads: theory JinjaThreads.JVMExec


15:48:47 JinjaThreads: theory JinjaThreads.Annotate


15:48:47 JinjaThreads: theory JinjaThreads.J1State


15:48:48 JinjaThreads: theory JinjaThreads.SmallStep


15:48:51 JinjaThreads: theory JinjaThreads.JVMDefensive


15:48:53 JinjaThreads: theory JinjaThreads.Compiler2


15:48:53 JinjaThreads: theory JinjaThreads.J1Heap


15:49:04 JinjaThreads: theory JinjaThreads.Compiler1


15:49:08 JinjaThreads: theory JinjaThreads.JMM_Typesafe


15:49:09 JinjaThreads: theory JinjaThreads.JVMThreaded


15:49:14 JinjaThreads: theory JinjaThreads.J1WellType


15:49:19 JinjaThreads: theory JinjaThreads.Exception_Tables


15:49:19 JinjaThreads: theory JinjaThreads.Compiler


15:49:19 JinjaThreads: theory JinjaThreads.J1WellForm


15:49:20 JinjaThreads: theory JinjaThreads.JWellForm


15:49:21 JinjaThreads: theory JinjaThreads.WellTypeRT


15:49:22 JinjaThreads: theory JinjaThreads.JVMExec_Execute


15:49:23 JinjaThreads: theory JinjaThreads.JJ1WellForm


15:49:24 JinjaThreads: theory JinjaThreads.Preprocessor


15:49:28 JinjaThreads: theory JinjaThreads.JMM_Common


15:49:28 JinjaThreads: theory JinjaThreads.JVM_Main


15:49:28 JinjaThreads: theory JinjaThreads.JMM_JVM


15:49:38 JinjaThreads: theory JinjaThreads.FWBisimDeadlock


15:49:38 JinjaThreads: theory JinjaThreads.FWBisimLift


15:49:39 JinjaThreads: theory JinjaThreads.J1


15:49:40 JinjaThreads: theory JinjaThreads.JMM_Typesafe2


15:49:58 JinjaThreads: theory JinjaThreads.BVSpec


15:49:59 JinjaThreads: theory JinjaThreads.BVConform


15:50:00 JinjaThreads: theory JinjaThreads.TypeComp


15:50:00 JinjaThreads: theory JinjaThreads.EffectMono


15:50:01 JinjaThreads: theory JinjaThreads.TF_JVM


15:50:08 JinjaThreads: theory JinjaThreads.BVExec


15:50:10 JinjaThreads: theory JinjaThreads.LBVJVM


15:50:22 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe


15:50:22 JinjaThreads: theory JinjaThreads.Common_Main


15:50:39 JinjaThreads: theory JinjaThreads.BVNoTypeError


15:50:43 JinjaThreads: theory JinjaThreads.BVProgressThreaded


15:50:43 JinjaThreads: theory JinjaThreads.J1Deadlock


15:50:43 JinjaThreads: theory JinjaThreads.BCVExec


15:50:44 JinjaThreads: theory JinjaThreads.JVMExec_Execute2


15:50:51 JinjaThreads: theory JinjaThreads.JVMTau


15:51:29 JinjaThreads: theory JinjaThreads.Execs


15:51:52 JinjaThreads: theory JinjaThreads.DefAssPreservation


15:51:54 JinjaThreads: theory JinjaThreads.Threaded


15:51:55 JinjaThreads: theory JinjaThreads.Progress


15:52:03 JinjaThreads: theory JinjaThreads.TypeSafe


15:52:27 JinjaThreads: theory JinjaThreads.J0


15:52:27 JinjaThreads: theory JinjaThreads.JMM_J


15:52:39 JinjaThreads: theory JinjaThreads.J1JVMBisim


15:52:39 JinjaThreads: theory JinjaThreads.ProgressThreaded


15:52:39 JinjaThreads: theory JinjaThreads.J_Execute


15:52:56 JinjaThreads: theory JinjaThreads.DRF_JVM


15:52:57 JinjaThreads: theory JinjaThreads.JVMDeadlocked


15:53:00 JinjaThreads: theory JinjaThreads.JVM_Execute


15:53:01 JinjaThreads: theory JinjaThreads.JVM_Execute2


15:53:34 JinjaThreads: theory JinjaThreads.DRF_J


15:53:40 JinjaThreads: theory JinjaThreads.J0Bisim


15:53:44 JinjaThreads: theory JinjaThreads.J0J1Bisim


15:53:51 JinjaThreads: theory JinjaThreads.Deadlocked


15:53:52 JinjaThreads: theory JinjaThreads.BV_Main


15:53:54 JinjaThreads: theory JinjaThreads.Code_Generation


15:54:06 JinjaThreads: theory JinjaThreads.J_Main


15:54:08 JinjaThreads: theory JinjaThreads.ApprenticeChallenge


15:54:08 JinjaThreads: theory JinjaThreads.BufferExample


15:54:15 JinjaThreads: theory JinjaThreads.Java2Jinja


15:54:35 JinjaThreads: theory JinjaThreads.Examples_Main


15:54:54 JinjaThreads: theory JinjaThreads.Correctness1


15:54:55 JinjaThreads: theory JinjaThreads.Correctness1Threaded


16:04:31 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe


16:04:50 JinjaThreads: theory JinjaThreads.Execute_Main


16:05:20 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe


16:05:43 JinjaThreads: theory JinjaThreads.J1JVM


16:05:45 JinjaThreads: theory JinjaThreads.JVMJ1


16:07:34 JinjaThreads: theory JinjaThreads.Correctness2


16:10:19 JinjaThreads: theory JinjaThreads.Correctness


16:20:14 JinjaThreads: theory JinjaThreads.Compiler_Main


16:20:16 JinjaThreads: theory JinjaThreads.JMM_Compiler


16:20:21 JinjaThreads: theory JinjaThreads.SC_Interp


16:27:20 JinjaThreads: theory JinjaThreads.JMM_Interp


16:27:31 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2


16:27:36 JinjaThreads: theory JinjaThreads.JMM


16:27:43 JinjaThreads: theory JinjaThreads.MM_Main


16:28:04 JinjaThreads: theory JinjaThreads.JinjaThreads


16:43:54 Timing JinjaThreads (8 threads, 3619.648s elapsed time, 16376.412s cpu time, 5418.716s GC time, factor 4.52)


16:43:54 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads


16:43:54 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf


16:43:54 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf


16:43:54 Finished JinjaThreads (1:01:22 elapsed time, 4:39:06 cpu time, factor 4.55)


16:43:54 Building AWN ...


16:43:55 AWN: theory AWN.Lib


16:43:55 AWN: theory AWN.TransitionSystems


16:43:55 AWN: theory AWN.AWN


16:43:56 AWN: theory AWN.Invariants


16:43:57 AWN: theory AWN.OInvariants


16:44:11 AWN: theory AWN.AWN_Cterms


16:44:11 AWN: theory AWN.AWN_SOS


16:44:11 AWN: theory AWN.OAWN_SOS


16:44:15 AWN: theory AWN.AWN_Labels


16:44:17 AWN: theory AWN.Pnet


16:44:17 AWN: theory AWN.Inv_Cterms


16:44:17 AWN: theory AWN.AWN_Invariants


16:44:18 AWN: theory AWN.Closed


16:44:18 AWN: theory AWN.AWN_SOS_Labels


16:44:19 AWN: theory AWN.Qmsg


16:44:20 AWN: theory AWN.OAWN_Invariants


16:44:20 AWN: theory AWN.ONode_Lifting


16:44:20 AWN: theory AWN.OPnet


16:44:20 AWN: theory AWN.OAWN_SOS_Labels


16:44:21 AWN: theory AWN.OPnet_Lifting


16:44:22 AWN: theory AWN.OClosed_Lifting


16:44:22 AWN: theory AWN.OClosed_Transfer


16:44:22 AWN: theory AWN.OAWN_Convert


16:44:22 AWN: theory AWN.Qmsg_Lifting


16:44:23 AWN: theory AWN.AWN_Main


16:44:24 AWN: theory AWN.Toy


16:44:40 AWN: theory AWN.AWN_Term_Graph


16:45:16 Timing AWN (8 threads, 49.208s elapsed time, 243.800s cpu time, 8.912s GC time, factor 4.95)


16:45:16 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN


16:45:16 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf


16:45:16 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf


16:45:16 Finished AWN (0:01:21 elapsed time, 0:05:09 cpu time, factor 3.82)


16:45:16 Running AODV ...


16:45:18 AODV: theory AODV.Aodv_Basic


16:45:20 AODV: theory AODV.A_Norreqid


16:45:20 AODV: theory AODV.Aodv_Data


16:45:20 AODV: theory AODV.Aodv_Message


16:45:20 AODV: theory AODV.B_Fwdrreps


16:45:20 AODV: theory AODV.C_Gtobcast


16:45:20 AODV: theory AODV.D_Fwdrreqs


16:45:20 AODV: theory AODV.E_All_ABCD


16:45:20 AODV: theory AODV.A_Aodv_Data


16:45:20 AODV: theory AODV.A_Aodv_Message


16:45:20 AODV: theory AODV.E_Aodv_Data


16:45:20 AODV: theory AODV.B_Aodv_Data


16:45:20 AODV: theory AODV.B_Aodv_Message


16:45:20 AODV: theory AODV.C_Aodv_Data


16:45:22 AODV: theory AODV.C_Fresher


16:45:22 AODV: theory AODV.C_Aodv_Message


16:45:22 AODV: theory AODV.A_Fresher


16:45:22 AODV: theory AODV.B_Fresher


16:45:22 AODV: theory AODV.D_Aodv_Data


16:45:22 AODV: theory AODV.D_Aodv_Message


16:45:22 AODV: theory AODV.E_Fresher


16:45:22 AODV: theory AODV.Fresher


16:45:23 AODV: theory AODV.E_Aodv_Message


16:45:23 AODV: theory AODV.A_Aodv


16:45:23 AODV: theory AODV.Aodv


16:45:23 AODV: theory AODV.B_Aodv


16:45:24 AODV: theory AODV.C_Aodv


16:45:24 AODV: theory AODV.D_Fresher


16:45:24 AODV: theory AODV.D_Aodv


16:45:24 AODV: theory AODV.E_Aodv


16:46:32 AODV: theory AODV.Aodv_Predicates


16:46:32 AODV: theory AODV.OAodv


16:46:32 AODV: theory AODV.Loop_Freedom


16:46:32 AODV: theory AODV.Quality_Increases


16:46:32 AODV: theory AODV.Seq_Invariants


16:46:33 AODV: theory AODV.Global_Invariants


16:46:34 AODV: theory AODV.Aodv_Loop_Freedom


16:46:39 AODV: theory AODV.C_Aodv_Predicates


16:46:39 AODV: theory AODV.C_Loop_Freedom


16:46:40 AODV: theory AODV.C_Quality_Increases


16:46:41 AODV: theory AODV.C_Seq_Invariants


16:46:41 AODV: theory AODV.C_OAodv


16:46:42 AODV: theory AODV.C_Global_Invariants


16:46:43 AODV: theory AODV.C_Aodv_Loop_Freedom


16:46:57 AODV: theory AODV.A_Aodv_Predicates


16:46:57 AODV: theory AODV.A_OAodv


16:46:57 AODV: theory AODV.A_Loop_Freedom


16:46:58 AODV: theory AODV.A_Quality_Increases


16:46:58 AODV: theory AODV.A_Seq_Invariants


16:46:59 AODV: theory AODV.A_Global_Invariants


16:47:00 AODV: theory AODV.E_Aodv_Predicates


16:47:00 AODV: theory AODV.E_OAodv


16:47:00 AODV: theory AODV.E_Loop_Freedom


16:47:01 AODV: theory AODV.E_Quality_Increases


16:47:01 AODV: theory AODV.E_Seq_Invariants


16:47:01 AODV: theory AODV.B_Aodv_Predicates


16:47:01 AODV: theory AODV.B_OAodv


16:47:02 AODV: theory AODV.E_Global_Invariants


16:47:02 AODV: theory AODV.B_Loop_Freedom


16:47:02 AODV: theory AODV.B_Quality_Increases


16:47:02 AODV: theory AODV.B_Seq_Invariants


16:47:03 AODV: theory AODV.A_Aodv_Loop_Freedom


16:47:03 AODV: theory AODV.E_Aodv_Loop_Freedom


16:47:03 AODV: theory AODV.B_Global_Invariants


16:47:04 AODV: theory AODV.B_Aodv_Loop_Freedom


16:47:10 AODV: theory AODV.D_Aodv_Predicates


16:47:11 AODV: theory AODV.D_OAodv


16:47:11 AODV: theory AODV.D_Loop_Freedom


16:47:11 AODV: theory AODV.D_Quality_Increases


16:47:11 AODV: theory AODV.D_Seq_Invariants


16:47:12 AODV: theory AODV.D_Global_Invariants


16:47:13 AODV: theory AODV.D_Aodv_Loop_Freedom


16:47:20 AODV: theory AODV.All


19:36:25 Timing AODV (8 threads, 10251.125s elapsed time, 56218.508s cpu time, 4906.204s GC time, factor 5.48)


19:36:25 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV


19:36:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf


19:36:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf


19:36:25 Finished AODV (2:51:06 elapsed time, 15:37:25 cpu time, factor 5.48)


19:36:25 Building HOL-Library ...


19:36:27 HOL-Library: theory HOL-Library.AList


19:36:27 HOL-Library: theory HOL-Library.Adhoc_Overloading


19:36:27 HOL-Library: theory HOL-Library.BNF_Corec


19:36:27 HOL-Library: theory HOL-Library.Bit


19:36:27 HOL-Library: theory HOL-Library.Boolean_Algebra


19:36:27 HOL-Library: theory HOL-Library.BNF_Axiomatization


19:36:27 HOL-Library: theory HOL-Library.Cardinal_Notations


19:36:27 HOL-Library: theory HOL-Library.Cancellation


19:36:27 HOL-Library: theory HOL-Library.Case_Converter


19:36:28 HOL-Library: theory HOL-Library.Monad_Syntax


19:36:28 HOL-Library: theory HOL-Library.State_Monad


19:36:28 HOL-Library: theory HOL-Library.Char_ord


19:36:28 HOL-Library: theory HOL-Library.Code_Abstract_Nat


19:36:28 HOL-Library: theory HOL-Library.Code_Binary_Nat


19:36:28 HOL-Library: theory HOL-Library.Code_Target_Nat


19:36:28 HOL-Library: theory HOL-Library.Code_Prolog


19:36:28 HOL-Library: theory HOL-Library.Code_Target_Int


19:36:28 HOL-Library: theory HOL-Library.Code_Lazy


19:36:29 HOL-Library: theory HOL-Library.Multiset


19:36:29 HOL-Library: theory HOL-Library.Simps_Case_Conv


19:36:29 HOL-Library: theory HOL-Library.Code_Target_Numeral


19:36:29 HOL-Library: theory HOL-Library.Extended


19:36:29 HOL-Library: theory HOL-Library.Code_Test


19:36:30 HOL-Library: theory HOL-Library.Comparator


19:36:30 HOL-Library: theory HOL-Library.Conditional_Parametricity


19:36:30 HOL-Library: theory HOL-Library.Datatype_Records


19:36:30 HOL-Library: theory HOL-Library.Debug


19:36:30 HOL-Library: theory HOL-Library.Disjoint_Sets


19:36:31 HOL-Library: theory HOL-Library.DAList


19:36:31 HOL-Library: theory HOL-Library.Dlist


19:36:31 HOL-Library: theory HOL-Library.Fun_Lexorder


19:36:31 HOL-Library: theory HOL-Library.FuncSet


19:36:31 HOL-Library: theory HOL-Library.Function_Algebras


19:36:31 HOL-Library: theory HOL-Library.Groups_Big_Fun


19:36:31 HOL-Library: theory HOL-Library.Function_Division


19:36:31 HOL-Library: theory HOL-Library.IArray


19:36:31 HOL-Library: theory HOL-Library.Infinite_Set


19:36:32 HOL-Library: theory HOL-Library.Equipollence


19:36:32 HOL-Library: theory HOL-Library.LaTeXsugar


19:36:32 HOL-Library: theory HOL-Library.Lattice_Constructions


19:36:32 HOL-Library: theory HOL-Library.Omega_Words_Fun


19:36:32 HOL-Library: theory HOL-Library.Ramsey


19:36:32 HOL-Library: theory HOL-Library.Lattice_Syntax


19:36:32 HOL-Library: theory HOL-Library.Combine_PER


19:36:32 HOL-Library: theory HOL-Library.Complete_Partial_Order2


19:36:32 HOL-Library: theory HOL-Library.ListVector


19:36:32 HOL-Library: theory HOL-Library.List_Lexorder


19:36:32 HOL-Library: theory HOL-Library.Mapping


19:36:32 HOL-Library: theory HOL-Library.More_List


19:36:32 HOL-Library: theory HOL-Library.Nat_Bijection


19:36:33 HOL-Library: theory HOL-Library.Old_Datatype


19:36:33 HOL-Library: theory HOL-Library.Old_Recdef


19:36:33 HOL-Library: theory HOL-Library.Stream


19:36:35 HOL-Library: theory HOL-Library.Open_State_Syntax


19:36:35 HOL-Library: theory HOL-Library.Option_ord


19:36:35 HOL-Library: theory HOL-Library.AList_Mapping


19:36:35 HOL-Library: theory HOL-Library.Parallel


19:36:36 HOL-Library: theory HOL-Library.Pattern_Aliases


19:36:36 HOL-Library: theory HOL-Library.Perm


19:36:36 HOL-Library: theory HOL-Library.Phantom_Type


19:36:36 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs


19:36:36 HOL-Library: theory HOL-Library.Preorder


19:36:37 HOL-Library: theory HOL-Library.Product_Lexorder


19:36:37 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck


19:36:37 HOL-Library: theory HOL-Library.Product_Plus


19:36:37 HOL-Library: theory HOL-Library.Cardinality


19:36:37 HOL-Library: theory HOL-Library.Quotient_Syntax


19:36:37 HOL-Library: theory HOL-Library.Quotient_Option


19:36:37 HOL-Library: theory HOL-Library.Quotient_Product


19:36:37 HOL-Library: theory HOL-Library.Quotient_Set


19:36:37 HOL-Library: theory HOL-Library.Product_Order


19:36:37 HOL-Library: theory HOL-Library.Quotient_Sum


19:36:37 HOL-Library: theory HOL-Library.Quotient_List


19:36:37 HOL-Library: theory HOL-Library.Quotient_Type


19:36:37 HOL-Library: theory HOL-Library.RBT_Impl


19:36:38 HOL-Library: theory HOL-Library.Realizers


19:36:38 HOL-Library: theory HOL-Library.Finite_Lattice


19:36:38 HOL-Library: theory HOL-Library.DAList_Multiset


19:36:38 HOL-Library: theory HOL-Library.Multiset_Order


19:36:38 HOL-Library: theory HOL-Library.Permutation


19:36:38 HOL-Library: theory HOL-Library.Permutations


19:36:39 HOL-Library: theory HOL-Library.Reflection


19:36:39 HOL-Library: theory HOL-Library.Refute


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


19:36:39 HOL-Library: theory HOL-Library.Numeral_Type


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


19:36:39 HOL-Library: theory HOL-Library.Sorting_Algorithms


19:36:41 HOL-Library: theory HOL-Library.Stirling


19:36:41 HOL-Library: theory HOL-Library.Sublist


19:36:42 HOL-Library: theory HOL-Library.Transitive_Closure_Table


19:36:42 HOL-Library: theory HOL-Library.Tree


19:36:42 HOL-Library: theory HOL-Library.Uprod


19:36:42 HOL-Library: theory HOL-Library.While_Combinator


19:36:42 HOL-Library: theory HOL-Library.Countable


19:36:42 HOL-Library: theory HOL-Library.Type_Length


19:36:43 HOL-Library: theory HOL-Library.Saturated


19:36:43 HOL-Library: theory HOL-Library.BigO


19:36:43 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float


19:36:43 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint


19:36:44 HOL-Library: theory HOL-Library.Diagonal_Subsequence


19:36:44 HOL-Library: theory HOL-Library.Prefix_Order


19:36:44 HOL-Library: theory HOL-Library.Subseq_Order


19:36:44 HOL-Library: theory HOL-Library.Discrete


19:36:44 HOL-Library: theory HOL-Library.Going_To_Filter


19:36:44 HOL-Library: theory HOL-Library.Indicator_Function


19:36:44 HOL-Library: theory HOL-Library.Landau_Symbols


19:36:44 HOL-Library: theory HOL-Library.Lattice_Algebras


19:36:44 HOL-Library: theory HOL-Library.Liminf_Limsup


19:36:44 HOL-Library: theory HOL-Library.Countable_Set


19:36:44 HOL-Library: theory HOL-Library.FSet


19:36:45 HOL-Library: theory HOL-Library.Log_Nat


19:36:45 HOL-Library: theory HOL-Library.Lub_Glb


19:36:45 HOL-Library: theory HOL-Library.Multiset_Permutations


19:36:45 HOL-Library: theory HOL-Library.Countable_Complete_Lattices


19:36:45 HOL-Library: theory HOL-Library.Countable_Set_Type


19:36:46 HOL-Library: theory HOL-Library.Tree_Multiset


19:36:47 HOL-Library: theory HOL-Library.Set_Idioms


19:36:47 HOL-Library: theory HOL-Library.Nonpos_Ints


19:36:48 HOL-Library: theory HOL-Library.OptionalSugar


19:36:48 HOL-Library: theory HOL-Library.Periodic_Fun


19:36:48 HOL-Library: theory HOL-Library.Quadratic_Discriminant


19:36:48 HOL-Library: theory HOL-Library.Sum_of_Squares


19:36:48 HOL-Library: theory HOL-Library.Tree_Real


19:36:49 HOL-Library: theory HOL-Library.Order_Continuity


19:36:50 HOL-Library: theory HOL-Library.Extended_Nat


19:36:50 HOL-Library: theory HOL-Library.Float


19:36:50 HOL-Library: theory HOL-Library.Finite_Map


19:36:51 HOL-Library: theory HOL-Library.Extended_Real


19:36:51 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams


19:36:57 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real


19:37:14 HOL-Library: theory HOL-Library.Library


19:37:34 HOL-Library: theory HOL-Library.RBT


19:37:35 HOL-Library: theory HOL-Library.RBT_Mapping


19:37:35 HOL-Library: theory HOL-Library.RBT_Set


19:39:24 Timing HOL-Library (8 threads, 103.922s elapsed time, 649.728s cpu time, 41.160s GC time, factor 6.25)


19:39:24 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library


19:39:24 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf


19:39:24 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf


19:39:24 Finished HOL-Library (0:02:55 elapsed time, 0:13:56 cpu time, factor 4.76)


19:39:24 Building ConcurrentIMP ...


19:39:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred


19:39:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang


19:39:40 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg


19:39:42 ConcurrentIMP: theory ConcurrentIMP.CIMP


19:39:42 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex


19:39:42 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex


19:40:13 Timing ConcurrentIMP (8 threads, 21.852s elapsed time, 53.120s cpu time, 2.780s GC time, factor 2.43)


19:40:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP


19:40:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf


19:40:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf


19:40:13 Finished ConcurrentIMP (0:00:48 elapsed time, 0:01:47 cpu time, factor 2.23)


19:40:13 Running ConcurrentGC ...


19:40:14 ConcurrentGC: theory ConcurrentGC.Model


19:40:35 ConcurrentGC: theory ConcurrentGC.Tactics


19:40:44 ConcurrentGC: theory ConcurrentGC.Proofs_basis


19:40:48 ConcurrentGC: theory ConcurrentGC.TSO


19:41:07 ConcurrentGC: theory ConcurrentGC.Handshakes


19:45:13 ConcurrentGC: theory ConcurrentGC.MarkObject


19:48:57 ConcurrentGC: theory ConcurrentGC.StrongTricolour


19:50:09 ConcurrentGC: theory ConcurrentGC.Proofs


19:50:11 ConcurrentGC: theory ConcurrentGC.Concrete_heap


19:50:13 ConcurrentGC: theory ConcurrentGC.Concrete


22:11:09 Timing ConcurrentGC (8 threads, 9047.119s elapsed time, 32781.896s cpu time, 1732.144s GC time, factor 3.62)


22:11:09 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC


22:11:09 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf


22:11:09 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf


22:11:09 Finished ConcurrentGC (2:30:53 elapsed time, 9:06:34 cpu time, factor 3.62)


22:11:09 Building HOL-Word ...


22:11:10 HOL-Word: theory HOL-Library.Bit


22:11:10 HOL-Word: theory HOL-Library.Boolean_Algebra


22:11:10 HOL-Word: theory HOL-Library.Phantom_Type


22:11:10 HOL-Word: theory HOL-Word.Bits


22:11:10 HOL-Word: theory HOL-Word.Misc_Numeric


22:11:10 HOL-Word: theory HOL-Word.Misc_Typedef


22:11:10 HOL-Word: theory HOL-Word.Bit_Representation


22:11:11 HOL-Word: theory HOL-Word.Bits_Bit


22:11:11 HOL-Word: theory HOL-Word.Word_Miscellaneous


22:11:11 HOL-Word: theory HOL-Word.Bits_Int


22:11:11 HOL-Word: theory HOL-Library.Cardinality


22:11:13 HOL-Word: theory HOL-Library.Numeral_Type


22:11:13 HOL-Word: theory HOL-Word.Bit_Comparison


22:11:13 HOL-Word: theory HOL-Word.Bool_List_Representation


22:11:15 HOL-Word: theory HOL-Library.Type_Length


22:11:15 HOL-Word: theory HOL-Word.Word


22:11:21 HOL-Word: theory HOL-Word.WordBitwise


22:11:22 HOL-Word: theory HOL-Word.WordExamples


22:11:43 Timing HOL-Word (8 threads, 13.410s elapsed time, 66.104s cpu time, 2.248s GC time, factor 4.93)


22:11:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word


22:11:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf


22:11:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf


22:11:43 Finished HOL-Word (0:00:33 elapsed time, 0:01:45 cpu time, factor 3.20)


22:11:43 Building Word_Lib ...


22:11:44 Word_Lib: theory Word_Lib.Hex_Words


22:11:44 Word_Lib: theory Word_Lib.Signed_Words


22:11:44 Word_Lib: theory Word_Lib.Word_Type_Syntax


22:11:44 Word_Lib: theory HOL-Library.Sublist


22:11:44 Word_Lib: theory Word_Lib.More_Divides


22:11:44 Word_Lib: theory Word_Lib.HOL_Lemmas


22:11:44 Word_Lib: theory Word_Lib.Enumeration


22:11:44 Word_Lib: theory Word_Lib.Norm_Words


22:11:44 Word_Lib: theory Word_Lib.WordBitwise_Signed


22:11:44 Word_Lib: theory Word_Lib.Word_Syntax


22:11:45 Word_Lib: theory Word_Lib.Word_Lib


22:11:46 Word_Lib: theory Word_Lib.Word_Enum


22:11:46 Word_Lib: theory Word_Lib.Aligned


22:11:47 Word_Lib: theory Word_Lib.Word_Setup_32


22:11:47 Word_Lib: theory Word_Lib.Word_Setup_64


22:11:47 Word_Lib: theory Word_Lib.Word_Next


22:11:47 Word_Lib: theory Word_Lib.Word_Lemmas


22:11:54 Word_Lib: theory Word_Lib.Word_Lemmas_32


22:11:54 Word_Lib: theory Word_Lib.Word_Lemmas_64


22:13:11 Timing Word_Lib (8 threads, 71.006s elapsed time, 188.572s cpu time, 5.644s GC time, factor 2.66)


22:13:11 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib


22:13:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf


22:13:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf


22:13:11 Finished Word_Lib (0:01:28 elapsed time, 0:03:43 cpu time, factor 2.53)


22:13:11 Building IP_Addresses ...


22:13:13 IP_Addresses: theory HOL-Eisbach.Eisbach


22:13:13 IP_Addresses: theory HOL-Library.Cancellation


22:13:13 IP_Addresses: theory HOL-Library.Infinite_Set


22:13:13 IP_Addresses: theory HOL-Library.Option_ord


22:13:13 IP_Addresses: theory IP_Addresses.NumberWang_IPv4


22:13:13 IP_Addresses: theory IP_Addresses.NumberWang_IPv6


22:13:14 IP_Addresses: theory HOL-Library.Multiset


22:13:20 IP_Addresses: theory HOL-ex.Quicksort


22:13:21 IP_Addresses: theory Automatic_Refinement.Misc


22:13:28 IP_Addresses: theory HOL-Library.Code_Abstract_Nat


22:13:28 IP_Addresses: theory HOL-Library.Product_Lexorder


22:13:28 IP_Addresses: theory IP_Addresses.Hs_Compat


22:13:28 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString


22:13:28 IP_Addresses: theory IP_Addresses.WordInterval


22:13:29 IP_Addresses: theory HOL-Library.Code_Target_Nat


22:13:29 IP_Addresses: theory IP_Addresses.Lib_List_toString


22:13:29 IP_Addresses: theory IP_Addresses.Lib_Word_toString


22:13:34 IP_Addresses: theory IP_Addresses.IP_Address


22:13:34 IP_Addresses: theory IP_Addresses.WordInterval_Sorted


22:13:41 IP_Addresses: theory IP_Addresses.IPv4


22:13:41 IP_Addresses: theory IP_Addresses.IPv6


22:13:41 IP_Addresses: theory IP_Addresses.Prefix_Match


22:13:42 IP_Addresses: theory IP_Addresses.CIDR_Split


22:15:27 IP_Addresses: theory IP_Addresses.IP_Address_Parser


22:15:27 IP_Addresses: theory IP_Addresses.IP_Address_toString


22:15:29 IP_Addresses: theory IP_Addresses.Prefix_Match_toString


22:19:13 Timing IP_Addresses (8 threads, 318.289s elapsed time, 968.596s cpu time, 57.644s GC time, factor 3.04)


22:19:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses


22:19:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf


22:19:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf


22:19:13 Finished IP_Addresses (0:06:00 elapsed time, 0:17:48 cpu time, factor 2.97)


22:19:13 Building Simple_Firewall ...


22:19:14 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State


22:19:14 Simple_Firewall: theory Simple_Firewall.GroupF


22:19:14 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries


22:19:14 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString


22:19:14 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString


22:19:14 Simple_Firewall: theory Simple_Firewall.Option_Helpers


22:19:14 Simple_Firewall: theory Simple_Firewall.List_Product_More


22:19:14 Simple_Firewall: theory HOL-Library.Char_ord


22:19:15 Simple_Firewall: theory Simple_Firewall.Iface


22:19:15 Simple_Firewall: theory Simple_Firewall.L4_Protocol


22:19:20 Simple_Firewall: theory Simple_Firewall.Simple_Packet


22:19:20 Simple_Firewall: theory Simple_Firewall.Primitives_toString


22:19:23 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax


22:19:26 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString


22:19:26 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics


22:19:29 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw


22:19:29 Simple_Firewall: theory Simple_Firewall.Shadowed


22:19:30 Simple_Firewall: theory Simple_Firewall.Service_Matrix


22:20:07 Timing Simple_Firewall (8 threads, 25.496s elapsed time, 101.664s cpu time, 4.804s GC time, factor 3.99)


22:20:07 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall


22:20:07 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf


22:20:07 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf


22:20:07 Finished Simple_Firewall (0:00:53 elapsed time, 0:02:48 cpu time, factor 3.11)


22:20:07 Building Routing ...


22:20:09 Routing: theory Routing.Linorder_Helper


22:20:09 Routing: theory HOL-Library.Adhoc_Overloading


22:20:09 Routing: theory HOL-Library.Monad_Syntax


22:20:10 Routing: theory Routing.Routing_Table


22:20:15 Routing: theory Routing.IpRoute_Parser


22:20:15 Routing: theory Routing.Linux_Router


22:20:40 Timing Routing (8 threads, 13.318s elapsed time, 37.396s cpu time, 1.156s GC time, factor 2.81)


22:20:40 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing


22:20:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf


22:20:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf


22:20:40 Finished Routing (0:00:32 elapsed time, 0:01:15 cpu time, factor 2.31)


22:20:40 Building Iptables_Semantics ...


22:20:42 Iptables_Semantics: theory Iptables_Semantics.List_Misc


22:20:42 Iptables_Semantics: theory Iptables_Semantics.Negation_Type


22:20:45 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists


22:20:46 Iptables_Semantics: theory HOL-Library.Code_Target_Int


22:20:46 Iptables_Semantics: theory HOL-Library.LaTeXsugar


22:20:46 Iptables_Semantics: theory Native_Word.More_Bits_Int


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Ternary


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State


22:20:46 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags


22:20:46 Iptables_Semantics: theory Iptables_Semantics.IpAddresses


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Word_Upto


22:20:46 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common


22:20:48 Iptables_Semantics: theory Iptables_Semantics.Ports


22:20:49 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet


22:20:49 Iptables_Semantics: theory Native_Word.Bits_Integer


22:20:50 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax


22:21:08 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary


22:21:08 Iptables_Semantics: theory Iptables_Semantics.Semantics


22:21:09 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto


22:21:10 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int


22:21:10 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics


22:21:11 Iptables_Semantics: theory Iptables_Semantics.Matching


22:21:11 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful


22:21:11 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update


22:21:11 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding


22:21:12 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary


22:21:12 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs


22:21:13 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings


22:21:14 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action


22:21:14 Iptables_Semantics: theory Iptables_Semantics.Optimizing


22:21:14 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic


22:21:15 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches


22:21:16 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching


22:21:18 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization


22:21:21 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher


22:21:23 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold


22:21:23 Iptables_Semantics: theory Iptables_Semantics.Ipassmt


22:21:28 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt


22:22:23 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas


22:22:23 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString


22:22:23 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform


22:22:23 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics


22:22:24 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize


22:22:24 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize


22:22:24 Iptables_Semantics: theory Iptables_Semantics.No_Spoof


22:22:24 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize


22:22:24 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize


22:22:36 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace


22:22:43 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace


22:22:47 Iptables_Semantics: theory Iptables_Semantics.Transform


22:22:53 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract


22:22:55 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance


22:23:03 Iptables_Semantics: theory Iptables_Semantics.Code_Interface


22:23:04 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings


22:23:05 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings


22:23:05 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics


22:23:05 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings


22:23:13 Iptables_Semantics: theory Iptables_Semantics.Parser


22:23:13 Iptables_Semantics: theory Iptables_Semantics.Documentation


22:23:14 Iptables_Semantics: theory Iptables_Semantics.Code_haskell


22:24:43 Timing Iptables_Semantics (8 threads, 181.201s elapsed time, 816.416s cpu time, 61.728s GC time, factor 4.51)


22:24:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics


22:24:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf


22:24:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf


22:24:43 Finished Iptables_Semantics (0:04:00 elapsed time, 0:16:44 cpu time, factor 4.17)


22:24:43 Building Iptables_Semantics_Examples ...


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof


22:24:45 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6


22:24:46 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test


22:24:52 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail


22:24:53 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples


22:24:53 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed


22:24:54 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation


22:31:15 Timing Iptables_Semantics_Examples (8 threads, 363.174s elapsed time, 2349.436s cpu time, 229.708s GC time, factor 6.47)


22:31:15 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples


22:31:15 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf


22:31:15 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf


22:31:15 Finished Iptables_Semantics_Examples (0:06:31 elapsed time, 0:40:08 cpu time, factor 6.15)


22:31:15 Running Iptables_Semantics_Examples_Big ...


22:31:17 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern


22:31:17 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated


22:31:17 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small


22:31:17 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3


22:31:17 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall


22:35:55 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large


00:15:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW


00:53:17 Build timed out (after 1,400 minutes). Marking the build as aborted.


00:53:17 Build was aborted


00:53:17 Archiving artifacts


00:53:17 Started calculate disk usage of build


00:53:17 Finished Calculation of disk usage of build in 0 seconds


00:53:28 Started calculate disk usage of workspace


00:53:29 Finished Calculation of disk usage of workspace in  1 second


00:53:29 No emails were triggered.


00:53:29 Finished: ABORTED