Skipping 130 KB.. Full Log

Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
17:52:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
17:52:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
17:52:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
17:52:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
17:53:03 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
17:53:13 Preparing Automatic_Refinement/document ...
17:53:16 Finished Automatic_Refinement/document (0:00:02 elapsed time)
17:53:16 Preparing Automatic_Refinement/outline ...
17:53:18 Finished Automatic_Refinement/outline (0:00:02 elapsed time)
17:53:18 Timing Automatic_Refinement (8 threads, 25.732s elapsed time, 113.451s cpu time, 3.728s GC time, factor 4.41)
17:53:18 Finished Automatic_Refinement (0:00:35 elapsed time, 0:02:12 cpu time, factor 3.75)
17:53:18 Running AutoCorres2_Test (on lxcisa1/1) ...
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.DataStructures
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.Match_Cterm_Ex
17:53:22 AutoCorres2_Test: theory HOL-Computational_Algebra.Factorial_Ring
17:53:22 AutoCorres2_Test: theory HOL-Library.Product_Lexorder
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.Asm_Labels
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.AC_Rename
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.Alloc_Ex
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.CList
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.ConditionGuard
17:53:22 AutoCorres2_Test: theory AutoCorres2_Test.CustomWordAbs
17:53:23 AutoCorres2_Test: theory AutoCorres2_Test.BinarySearch
17:53:30 AutoCorres2_Test: theory AutoCorres2_Test.EvaluationOrder
17:53:31 AutoCorres2_Test: theory AutoCorres2_Test.Exception_Rewriting
17:53:31 AutoCorres2_Test: theory AutoCorres2_Test.FactorialTest
17:53:34 AutoCorres2_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm
17:53:37 AutoCorres2_Test: theory AutoCorres2_Test.FibProof
17:53:42 AutoCorres2_Test: theory AutoCorres2_Test.FunctionInfoDemo
17:53:42 AutoCorres2_Test: theory AutoCorres2_Test.Global_Structs
17:53:43 AutoCorres2_Test: theory AutoCorres2_Test.Guard_Simp
17:53:44 AutoCorres2_Test: theory AutoCorres2_Test.HeapWrap
17:53:51 AutoCorres2_Test: theory AutoCorres2_Test.In_Out_Parameters_Slow
17:53:52 AutoCorres2_Test: theory HOL-Computational_Algebra.Primes
17:53:52 AutoCorres2_Test: theory AutoCorres2_Test.Incremental
17:54:00 AutoCorres2_Test: theory AutoCorres2_Test.Kmalloc
17:54:03 AutoCorres2_Test: theory AutoCorres2_Test.IsPrime_Ex
17:54:16 AutoCorres2_Test: theory AutoCorres2_Test.ListRev
17:54:26 AutoCorres2_Test: theory AutoCorres2_Test.Memcpy
17:54:29 AutoCorres2_Test: theory AutoCorres2_Test.Memset
17:54:41 AutoCorres2_Test: theory AutoCorres2_Test.MultByAdd
17:54:48 AutoCorres2_Test: theory AutoCorres2_Test.Mutual_Fixed_Points
17:54:49 AutoCorres2_Test: theory AutoCorres2_Test.Plus_Ex
17:54:53 AutoCorres2_Test: theory AutoCorres2_Test.Quicksort_Ex
17:55:03 AutoCorres2_Test: theory AutoCorres2_Test.SchorrWaite_Ex
17:55:07 AutoCorres2_Test: theory AutoCorres2_Test.SignedWordAbsHeap
17:55:16 AutoCorres2_Test: theory AutoCorres2_Test.Simple
17:55:20 AutoCorres2_Test: theory AutoCorres2_Test.Str2Long
17:55:20 AutoCorres2_Test: theory AutoCorres2_Test.Suzuki
17:55:24 AutoCorres2_Test: theory AutoCorres2_Test.Swap_Ex
17:55:27 AutoCorres2_Test: theory AutoCorres2_Test.Test_Spec_Translation
17:55:34 AutoCorres2_Test: theory AutoCorres2_Test.TraceDemo
17:55:35 AutoCorres2_Test: theory AutoCorres2_Test.WhileLoopVarsPreserved
17:55:39 AutoCorres2_Test: theory AutoCorres2_Test.WordAbs
17:55:42 AutoCorres2_Test: theory AutoCorres2_Test.WordAbsFnCall
17:55:44 AutoCorres2_Test: theory AutoCorres2_Test.array_indirect_update
17:55:45 AutoCorres2_Test: theory AutoCorres2_Test.badnames
17:55:47 AutoCorres2_Test: theory AutoCorres2_Test.basic
17:55:53 AutoCorres2_Test: theory AutoCorres2_Test.basic_recursion
17:55:54 AutoCorres2_Test: theory AutoCorres2_Test.big_bit_ops
17:55:56 AutoCorres2_Test: theory AutoCorres2_Test.bit_shuffle
17:56:03 AutoCorres2_Test: theory AutoCorres2_Test.bodyless_function
17:56:08 AutoCorres2_Test: theory AutoCorres2_Test.buffer
17:56:13 AutoCorres2_Test: theory AutoCorres2_Test.explosion
17:56:14 AutoCorres2_Test: theory AutoCorres2_Test.final_autocorres
17:56:18 AutoCorres2_Test: theory AutoCorres2_Test.fnptr_enum0
17:56:22 AutoCorres2_Test: theory AutoCorres2_Test.fnptr_large_array
17:56:26 AutoCorres2_Test: theory AutoCorres2_Test.fnptr_skip_heap_abs
17:56:28 AutoCorres2_Test: theory AutoCorres2_Test.global_array_update
17:56:29 AutoCorres2_Test: theory AutoCorres2_Test.globals
17:56:38 AutoCorres2_Test: theory AutoCorres2_Test.goto
17:56:41 AutoCorres2_Test: theory AutoCorres2_Test.heap_infer
17:56:44 AutoCorres2_Test: theory AutoCorres2_Test.heap_lift_array
17:56:49 AutoCorres2_Test: theory AutoCorres2_Test.heap_lift_force_prevent
17:56:50 AutoCorres2_Test: theory AutoCorres2_Test.int128
17:56:52 AutoCorres2_Test: theory AutoCorres2_Test.l2_opt_invariant
17:56:57 AutoCorres2_Test: theory AutoCorres2_Test.loop_test
17:56:59 AutoCorres2_Test: theory AutoCorres2_Test.loop_test2
17:56:59 AutoCorres2_Test: theory AutoCorres2_Test.mmio
17:57:02 AutoCorres2_Test: theory AutoCorres2_Test.mmio_assume
17:57:08 AutoCorres2_Test: theory AutoCorres2_Test.mutual_recursion
17:57:12 AutoCorres2_Test: theory AutoCorres2_Test.mutual_recursion2
17:57:17 AutoCorres2_Test: theory AutoCorres2_Test.nested_array
17:57:18 AutoCorres2_Test: theory AutoCorres2_Test.nested_break_cont
17:57:22 AutoCorres2_Test: theory AutoCorres2_Test.nested_struct
17:57:25 AutoCorres2_Test: theory AutoCorres2_Test.open_nested
17:57:29 AutoCorres2_Test: theory AutoCorres2_Test.open_nested_array
17:57:35 AutoCorres2_Test: theory AutoCorres2_Test.option_exploration
17:57:42 AutoCorres2_Test: theory AutoCorres2_Test.partial_open_nested
17:57:43 AutoCorres2_Test: theory AutoCorres2_Test.pointers_to_locals_skip_hl
17:57:45 AutoCorres2_Test: theory AutoCorres2_Test.pointers_to_locals_skip_hl_wa
17:57:50 AutoCorres2_Test: theory AutoCorres2_Test.profile_conversion
17:57:51 AutoCorres2_Test: theory AutoCorres2_Test.prototyped_functions
17:57:53 AutoCorres2_Test: theory AutoCorres2_Test.read_global_array
17:58:00 AutoCorres2_Test: theory AutoCorres2_Test.signed_ptr_ptr
17:58:05 AutoCorres2_Test: theory AutoCorres2_Test.simple1
17:58:11 AutoCorres2_Test: theory AutoCorres2_Test.single_auxupd
17:58:11 AutoCorres2_Test: theory AutoCorres2_Test.skip_heap_abs
17:58:12 AutoCorres2_Test: theory AutoCorres2_Test.skip_in_out_parameters
17:58:12 AutoCorres2_Test: theory AutoCorres2_Test.struct
17:58:17 AutoCorres2_Test: theory AutoCorres2_Test.struct1
17:58:18 AutoCorres2_Test: theory AutoCorres2_Test.struct3
17:58:18 AutoCorres2_Test: theory AutoCorres2_Test.struct2
17:58:20 AutoCorres2_Test: theory AutoCorres2_Test.struct_consecutive_init
17:58:23 AutoCorres2_Test: theory AutoCorres2_Test.struct_init
17:58:29 AutoCorres2_Test: theory AutoCorres2_Test.ternary_conditional_operator
17:58:33 AutoCorres2_Test: theory AutoCorres2_Test.try
17:58:35 AutoCorres2_Test: theory AutoCorres2_Test.type_strengthen_tricks
17:58:47 AutoCorres2_Test: theory AutoCorres2_Test.underscore_funs
17:58:54 AutoCorres2_Test: theory AutoCorres2_Test.unfold_bind_options
17:58:59 AutoCorres2_Test: theory AutoCorres2_Test.unliftable_call
17:58:59 AutoCorres2_Test: theory AutoCorres2_Test.voidptrptr
17:59:02 AutoCorres2_Test: theory AutoCorres2_Test.while_loop_no_vars
17:59:09 AutoCorres2_Test: theory AutoCorres2_Test.word_abs_cases
17:59:11 AutoCorres2_Test: theory AutoCorres2_Test.word_abs_exn
17:59:13 AutoCorres2_Test: theory AutoCorres2_Test.word_abs_options
17:59:15 AutoCorres2_Test: theory AutoCorres2_Test.write_to_global_array
17:59:18 AutoCorres2_Test: theory AutoCorres2_Test.CompoundCTypesEx
17:59:20 AutoCorres2_Test: theory AutoCorres2_Test.CompoundCTypesExNew
17:59:21 AutoCorres2_Test: theory AutoCorres2_Test.MachineWords
17:59:21 AutoCorres2_Test: theory AutoCorres2_Test.Plus0
17:59:22 AutoCorres2_Test: theory AutoCorres2_Test.Skip_Asm
17:59:22 AutoCorres2_Test: theory AutoCorres2_Test.aligned
17:59:23 AutoCorres2_Test: theory AutoCorres2_Test.analsignedoverflow
17:59:24 AutoCorres2_Test: theory AutoCorres2_Test.array_of_ptr
17:59:25 AutoCorres2_Test: theory AutoCorres2_Test.arrays
17:59:26 AutoCorres2_Test: theory AutoCorres2_Test.asm_stmt
17:59:26 AutoCorres2_Test: theory AutoCorres2_Test.attributes
17:59:28 AutoCorres2_Test: theory AutoCorres2_Test.basic_char
17:59:29 AutoCorres2_Test: theory AutoCorres2_Test.bigstruct
17:59:29 AutoCorres2_Test: theory AutoCorres2_Test.breakcontinue
17:59:30 AutoCorres2_Test: theory AutoCorres2_Test.bug20060707
17:59:30 AutoCorres2_Test: theory AutoCorres2_Test.bug_mvt20110302
17:59:31 AutoCorres2_Test: theory AutoCorres2_Test.bugzilla180
17:59:32 AutoCorres2_Test: theory AutoCorres2_Test.bugzilla181
17:59:32 AutoCorres2_Test: theory AutoCorres2_Test.bugzilla182
17:59:33 AutoCorres2_Test: theory AutoCorres2_Test.builtins
17:59:35 AutoCorres2_Test: theory AutoCorres2_Test.charlit
17:59:35 AutoCorres2_Test: theory AutoCorres2_Test.codetests
17:59:36 AutoCorres2_Test: theory AutoCorres2_Test.dc_20081211
17:59:36 AutoCorres2_Test: theory AutoCorres2_Test.dc_embbug
17:59:38 AutoCorres2_Test: theory AutoCorres2_Test.decl_only
17:59:39 AutoCorres2_Test: theory AutoCorres2_Test.dont_translate
17:59:39 AutoCorres2_Test: theory AutoCorres2_Test.dupthms
17:59:39 AutoCorres2_Test: theory AutoCorres2_Test.empty
17:59:40 AutoCorres2_Test: theory AutoCorres2_Test.emptystmt
17:59:40 AutoCorres2_Test: theory AutoCorres2_Test.exit
17:59:41 AutoCorres2_Test: theory AutoCorres2_Test.extern_builtin
17:59:42 AutoCorres2_Test: theory AutoCorres2_Test.extern_dups
17:59:43 AutoCorres2_Test: theory AutoCorres2_Test.factorial
17:59:43 AutoCorres2_Test: theory AutoCorres2_Test.fncall
17:59:44 AutoCorres2_Test: theory AutoCorres2_Test.fnptr0
17:59:44 AutoCorres2_Test: theory AutoCorres2_Test.fnptr_enum
17:59:45 AutoCorres2_Test: theory AutoCorres2_Test.gcc_attribs
17:59:46 AutoCorres2_Test: theory AutoCorres2_Test.ghoststate1
17:59:47 AutoCorres2_Test: theory AutoCorres2_Test.ghoststate2
17:59:48 AutoCorres2_Test: theory AutoCorres2_Test.globals_fn
17:59:49 AutoCorres2_Test: theory AutoCorres2_Test.globals_in_record
17:59:49 AutoCorres2_Test: theory AutoCorres2_Test.globinits
17:59:50 AutoCorres2_Test: theory AutoCorres2_Test.goto0
17:59:51 AutoCorres2_Test: theory AutoCorres2_Test.guard_while
17:59:52 AutoCorres2_Test: theory AutoCorres2_Test.hexliteral
17:59:52 AutoCorres2_Test: theory AutoCorres2_Test.init_static
17:59:53 AutoCorres2_Test: theory AutoCorres2_Test.initialised_decls
17:59:53 AutoCorres2_Test: theory AutoCorres2_Test.inner_fncalls
17:59:54 AutoCorres2_Test: theory AutoCorres2_Test.int_promotion
17:59:54 AutoCorres2_Test: theory AutoCorres2_Test.isa2014
17:59:55 AutoCorres2_Test: theory AutoCorres2_Test.jiraver039
17:59:56 AutoCorres2_Test: theory AutoCorres2_Test.jiraver092
17:59:56 AutoCorres2_Test: theory AutoCorres2_Test.jiraver105
17:59:56 AutoCorres2_Test: theory AutoCorres2_Test.jiraver110
17:59:57 AutoCorres2_Test: theory AutoCorres2_Test.jiraver1241
17:59:57 AutoCorres2_Test: theory AutoCorres2_Test.jiraver150
17:59:57 AutoCorres2_Test: theory AutoCorres2_Test.jiraver224
17:59:58 AutoCorres2_Test: theory AutoCorres2_Test.jiraver253
17:59:58 AutoCorres2_Test: theory AutoCorres2_Test.jiraver254
17:59:59 AutoCorres2_Test: theory AutoCorres2_Test.jiraver307
17:59:59 AutoCorres2_Test: theory AutoCorres2_Test.jiraver310
18:00:00 AutoCorres2_Test: theory AutoCorres2_Test.jiraver313
18:00:00 AutoCorres2_Test: theory AutoCorres2_Test.jiraver315
18:00:01 AutoCorres2_Test: theory AutoCorres2_Test.jiraver332
18:00:01 AutoCorres2_Test: theory AutoCorres2_Test.jiraver336
18:00:01 AutoCorres2_Test: theory AutoCorres2_Test.jiraver337
18:00:01 AutoCorres2_Test: theory AutoCorres2_Test.jiraver344
18:00:03 AutoCorres2_Test: theory AutoCorres2_Test.jiraver345
18:00:04 AutoCorres2_Test: theory AutoCorres2_Test.jiraver384
18:00:04 AutoCorres2_Test: theory AutoCorres2_Test.jiraver400
18:00:04 AutoCorres2_Test: theory AutoCorres2_Test.jiraver422
18:00:04 AutoCorres2_Test: theory AutoCorres2_Test.jiraver426
18:00:04 AutoCorres2_Test: theory AutoCorres2_Test.jiraver429
18:00:06 AutoCorres2_Test: theory AutoCorres2_Test.jiraver432
18:00:06 AutoCorres2_Test: theory AutoCorres2_Test.jiraver434
18:00:06 AutoCorres2_Test: theory AutoCorres2_Test.jiraver439
18:00:06 AutoCorres2_Test: theory AutoCorres2_Test.jiraver440
18:00:07 AutoCorres2_Test: theory AutoCorres2_Test.jiraver443
18:00:07 AutoCorres2_Test: theory AutoCorres2_Test.jiraver443a
18:00:07 AutoCorres2_Test: theory AutoCorres2_Test.jiraver456
18:00:09 AutoCorres2_Test: theory AutoCorres2_Test.jiraver464
18:00:11 AutoCorres2_Test: theory AutoCorres2_Test.jiraver473
18:00:11 AutoCorres2_Test: theory AutoCorres2_Test.jiraver54
18:00:11 AutoCorres2_Test: theory AutoCorres2_Test.jiraver550
18:00:12 AutoCorres2_Test: theory AutoCorres2_Test.jiraver808
18:00:12 AutoCorres2_Test: theory AutoCorres2_Test.jiraver881
18:00:13 AutoCorres2_Test: theory AutoCorres2_Test.kmalloc0
18:00:13 AutoCorres2_Test: theory AutoCorres2_Test.list_reverse
18:00:14 AutoCorres2_Test: theory AutoCorres2_Test.list_reverse_norm
18:00:14 AutoCorres2_Test: theory AutoCorres2_Test.locvarfncall
18:00:15 AutoCorres2_Test: theory AutoCorres2_Test.longlong
18:00:16 AutoCorres2_Test: theory AutoCorres2_Test.memcopy
18:00:17 AutoCorres2_Test: theory AutoCorres2_Test.modifies_assumptions
18:00:17 AutoCorres2_Test: theory AutoCorres2_Test.modifies_pointer_to_local
18:00:17 AutoCorres2_Test: theory AutoCorres2_Test.modifies_speed
18:00:17 AutoCorres2_Test: theory AutoCorres2_Test.multi_deref
18:00:18 AutoCorres2_Test: theory AutoCorres2_Test.multidim_arrays
18:00:19 AutoCorres2_Test: theory AutoCorres2_Test.mutrec_modifies
18:00:19 AutoCorres2_Test: theory AutoCorres2_Test.nested
18:00:19 AutoCorres2_Test: theory AutoCorres2_Test.parse_addr
18:00:21 AutoCorres2_Test: theory AutoCorres2_Test.parse_c99block
18:00:22 AutoCorres2_Test: theory AutoCorres2_Test.parse_complit
18:00:24 AutoCorres2_Test: theory AutoCorres2_Test.parse_dowhile
18:00:24 AutoCorres2_Test: theory AutoCorres2_Test.parse_enum
18:00:24 AutoCorres2_Test: theory AutoCorres2_Test.parse_fncall
18:00:24 AutoCorres2_Test: theory AutoCorres2_Test.parse_forloop
18:00:26 AutoCorres2_Test: theory AutoCorres2_Test.parse_include
18:00:27 AutoCorres2_Test: theory AutoCorres2_Test.parse_protos
18:00:27 AutoCorres2_Test: theory AutoCorres2_Test.parse_retfncall
18:00:27 AutoCorres2_Test: theory AutoCorres2_Test.parse_sizeof
18:00:29 AutoCorres2_Test: theory AutoCorres2_Test.parse_someops
18:00:30 AutoCorres2_Test: theory AutoCorres2_Test.parse_struct
18:00:30 AutoCorres2_Test: theory AutoCorres2_Test.parse_struct_array
18:00:30 AutoCorres2_Test: theory AutoCorres2_Test.parse_switch
18:00:30 AutoCorres2_Test: theory AutoCorres2_Test.parse_typecast
18:00:32 AutoCorres2_Test: theory AutoCorres2_Test.parse_voidfn
18:00:33 AutoCorres2_Test: theory AutoCorres2_Test.phantom_mstate
18:00:33 AutoCorres2_Test: theory AutoCorres2_Test.pointers_to_locals0
18:00:33 AutoCorres2_Test: theory AutoCorres2_Test.populate_globals
18:00:34 AutoCorres2_Test: theory AutoCorres2_Test.postfixOps
18:00:36 AutoCorres2_Test: theory AutoCorres2_Test.protoparamshadow
18:00:36 AutoCorres2_Test: theory AutoCorres2_Test.ptr_auxupd
18:00:38 AutoCorres2_Test: theory AutoCorres2_Test.ptr_diff
18:00:39 AutoCorres2_Test: theory AutoCorres2_Test.ptr_modifies
18:00:39 AutoCorres2_Test: theory AutoCorres2_Test.really_simple
18:00:39 AutoCorres2_Test: theory AutoCorres2_Test.relspec
18:00:40 AutoCorres2_Test: theory AutoCorres2_Test.retprefix
18:00:42 AutoCorres2_Test: theory AutoCorres2_Test.selection_sort
18:00:42 AutoCorres2_Test: theory AutoCorres2_Test.shortcircuit
18:00:42 AutoCorres2_Test: theory AutoCorres2_Test.signed_div
18:00:43 AutoCorres2_Test: theory AutoCorres2_Test.signedoverflow
18:00:44 AutoCorres2_Test: theory AutoCorres2_Test.simple_annotated_fn
18:00:45 AutoCorres2_Test: theory AutoCorres2_Test.simple_constexpr_sizeof
18:00:45 AutoCorres2_Test: theory AutoCorres2_Test.simple_fn
18:00:45 AutoCorres2_Test: theory AutoCorres2_Test.sizeof_typedef
18:00:46 AutoCorres2_Test: theory AutoCorres2_Test.spec_annotated_fn
18:00:46 AutoCorres2_Test: theory AutoCorres2_Test.spec_annotated_voidfn
18:00:46 AutoCorres2_Test: theory AutoCorres2_Test.static
18:00:47 AutoCorres2_Test: theory AutoCorres2_Test.struct_init0
18:00:49 AutoCorres2_Test: theory AutoCorres2_Test.struct_names
18:00:49 AutoCorres2_Test: theory AutoCorres2_Test.swap0
18:00:49 AutoCorres2_Test: theory AutoCorres2_Test.switch_unsigned_signed
18:00:50 AutoCorres2_Test: theory AutoCorres2_Test.test_locality
18:00:50 AutoCorres2_Test: theory AutoCorres2_Test.test_shifts
18:00:51 AutoCorres2_Test: theory AutoCorres2_Test.ummbug20100217
18:00:52 AutoCorres2_Test: theory AutoCorres2_Test.union
18:00:52 AutoCorres2_Test: theory AutoCorres2_Test.untouched_globals
18:00:52 AutoCorres2_Test: theory AutoCorres2_Test.variable_munge
18:00:52 AutoCorres2_Test: theory AutoCorres2_Test.varinit
18:00:54 AutoCorres2_Test: theory AutoCorres2_Test.void_ptr_init
18:00:55 AutoCorres2_Test: theory AutoCorres2_Test.volatile_asm
18:02:09 AutoCorres2_Test: theory AutoCorres2_Test.CParserTest
18:02:19 AutoCorres2_Test: theory AutoCorres2_Test.AutoCorresTest
18:06:53 Timing AutoCorres2_Test (8 threads, 805.083s elapsed time, 5432.760s cpu time, 427.294s GC time, factor 6.75)
18:06:53 Finished AutoCorres2_Test (0:13:32 elapsed time, 1:31:02 cpu time, factor 6.72)
18:06:53 Building Core_SC_DOM (on lxcisa1/0) ...
18:07:09 Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
18:07:09 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
18:07:09 Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
18:07:10 Core_SC_DOM: theory Core_SC_DOM.Ref
18:07:10 Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
18:07:11 Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
18:07:11 Core_SC_DOM: theory Core_SC_DOM.BaseClass
18:07:11 Core_SC_DOM: theory Core_SC_DOM.NodePointer
18:07:11 Core_SC_DOM: theory Core_SC_DOM.ObjectClass
18:07:12 Core_SC_DOM: theory Core_SC_DOM.ElementPointer
18:07:13 Core_SC_DOM: theory Core_SC_DOM.NodeClass
18:07:13 Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
18:07:14 Core_SC_DOM: theory Core_SC_DOM.BaseMonad
18:07:14 Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
18:07:15 Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
18:07:16 Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
18:07:16 Core_SC_DOM: theory Core_SC_DOM.ElementClass
18:07:17 Core_SC_DOM: theory Core_SC_DOM.NodeMonad
18:07:18 Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
18:07:18 Core_SC_DOM: theory Core_SC_DOM.ElementMonad
18:07:19 Core_SC_DOM: theory Core_SC_DOM.DocumentClass
18:07:20 Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
18:07:21 Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
18:07:23 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
18:07:43 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
18:08:03 Core_SC_DOM: theory Core_SC_DOM.Core_DOM
18:08:03 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
18:08:11 Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
18:08:11 Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
18:08:11 Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
18:08:11 Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
18:08:13 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
18:10:22 Preparing Core_SC_DOM/document ...
18:10:37 Finished Core_SC_DOM/document (0:00:14 elapsed time)
18:10:37 Preparing Core_SC_DOM/outline ...
18:10:46 Finished Core_SC_DOM/outline (0:00:09 elapsed time)
18:10:47 Timing Core_SC_DOM (8 threads, 155.519s elapsed time, 833.465s cpu time, 61.249s GC time, factor 5.36)
18:10:47 Finished Core_SC_DOM (0:03:27 elapsed time, 0:15:55 cpu time, factor 4.60)
18:10:47 Building Refine_Monadic (on lxcisa1/1) ...
18:10:48 Refine_Monadic: theory Refine_Monadic.Example_Chapter
18:10:48 Refine_Monadic: theory Refine_Monadic.Refine_Chapter
18:10:48 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
18:10:48 Refine_Monadic: theory HOL-Library.Phantom_Type
18:10:48 Refine_Monadic: theory HOL-Library.Adhoc_Overloading
18:10:48 Refine_Monadic: theory HOL-Library.While_Combinator
18:10:49 Refine_Monadic: theory HOL-Library.Monad_Syntax
18:10:49 Refine_Monadic: theory Refine_Monadic.Refine_Misc
18:10:49 Refine_Monadic: theory HOL-Library.Cardinality
18:10:50 Refine_Monadic: theory Refine_Monadic.RefineG_Domain
18:10:50 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
18:10:50 Refine_Monadic: theory Refine_Monadic.RefineG_Assert
18:10:51 Refine_Monadic: theory HOL-Library.Numeral_Type
18:10:51 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
18:10:52 Refine_Monadic: theory Refine_Monadic.RefineG_While
18:10:52 Refine_Monadic: theory Refine_Monadic.Refine_Basic
18:10:52 Refine_Monadic: theory HOL-Library.Type_Length
18:10:52 Refine_Monadic: theory Refine_Monadic.Refine_Det
18:10:53 Refine_Monadic: theory HOL-Library.Word
18:10:56 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
18:10:56 Refine_Monadic: theory Refine_Monadic.Refine_Leof
18:10:56 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
18:10:57 Refine_Monadic: theory Refine_Monadic.Refine_Pfun
18:10:57 Refine_Monadic: theory Refine_Monadic.Refine_While
18:10:59 Refine_Monadic: theory Refine_Monadic.Refine_Transfer
18:10:59 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
18:10:59 Refine_Monadic: theory Refine_Monadic.Refine_Automation
18:10:59 Refine_Monadic: theory Refine_Monadic.Refine_Foreach
18:11:03 Refine_Monadic: theory Refine_Monadic.Refine_Monadic
18:11:03 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
18:11:04 Refine_Monadic: theory Refine_Monadic.WordRefine
18:11:04 Refine_Monadic: theory Refine_Monadic.Examples
18:11:36 Preparing Refine_Monadic/document ...
18:11:46 Finished Refine_Monadic/document (0:00:09 elapsed time)
18:11:46 Preparing Refine_Monadic/outline ...
18:11:52 Finished Refine_Monadic/outline (0:00:06 elapsed time)
18:11:52 Timing Refine_Monadic (8 threads, 37.523s elapsed time, 170.877s cpu time, 8.712s GC time, factor 4.55)
18:11:52 Finished Refine_Monadic (0:00:48 elapsed time, 0:03:13 cpu time, factor 3.99)
18:11:52 Building HOL-Probability (on lxcisa1/0) ...
18:11:55 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
18:11:55 HOL-Probability: theory HOL-Library.Conditional_Parametricity
18:11:55 HOL-Probability: theory HOL-Library.Adhoc_Overloading
18:11:55 HOL-Probability: theory HOL-Library.AList
18:11:55 HOL-Probability: theory HOL-Library.Rewrite
18:11:55 HOL-Probability: theory HOL-Library.Stream
18:11:55 HOL-Probability: theory HOL-Library.Tree
18:11:55 HOL-Probability: theory HOL-Library.Sublist
18:11:55 HOL-Probability: theory HOL-Library.Monad_Syntax
18:11:56 HOL-Probability: theory HOL-Library.FSet
18:11:56 HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
18:11:56 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
18:11:56 HOL-Probability: theory HOL-Probability.Discrete_Topology
18:11:57 HOL-Probability: theory HOL-Probability.Essential_Supremum
18:11:57 HOL-Probability: theory HOL-Probability.Probability_Measure
18:11:58 HOL-Probability: theory HOL-Probability.Stopping_Time
18:11:58 HOL-Probability: theory HOL-Library.Mapping
18:11:59 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
18:12:00 HOL-Probability: theory HOL-Probability.Tree_Space
18:12:01 HOL-Probability: theory HOL-Library.AList_Mapping
18:12:01 HOL-Probability: theory HOL-Probability.Conditional_Expectation
18:12:01 HOL-Probability: theory HOL-Probability.Distribution_Functions
18:12:01 HOL-Probability: theory HOL-Probability.Giry_Monad
18:12:01 HOL-Probability: theory HOL-Probability.Weak_Convergence
18:12:02 HOL-Probability: theory HOL-Probability.Helly_Selection
18:12:03 HOL-Probability: theory HOL-Library.Finite_Map
18:12:04 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
18:12:04 HOL-Probability: theory HOL-Probability.Projective_Family
18:12:05 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
18:12:06 HOL-Probability: theory HOL-Probability.Independent_Family
18:12:06 HOL-Probability: theory HOL-Probability.Stream_Space
18:12:07 HOL-Probability: theory HOL-Probability.PMF_Impl
18:12:07 HOL-Probability: theory HOL-Probability.Random_Permutations
18:12:07 HOL-Probability: theory HOL-Probability.SPMF
18:12:07 HOL-Probability: theory HOL-Probability.Convolution
18:12:07 HOL-Probability: theory HOL-Probability.Information
18:12:07 HOL-Probability: theory HOL-Probability.Product_PMF
18:12:09 HOL-Probability: theory HOL-Probability.Hoeffding
18:12:10 HOL-Probability: theory HOL-Probability.Distributions
18:12:12 HOL-Probability: theory HOL-Probability.Characteristic_Functions
18:12:12 HOL-Probability: theory HOL-Probability.Sinc_Integral
18:12:12 HOL-Probability: theory HOL-Probability.Levy
18:12:12 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
18:12:19 HOL-Probability: theory HOL-Probability.Fin_Map
18:12:21 HOL-Probability: theory HOL-Probability.Projective_Limit
18:12:23 HOL-Probability: theory HOL-Probability.Probability
18:13:31 Preparing HOL-Probability/document ...
18:13:49 Finished HOL-Probability/document (0:00:18 elapsed time)
18:13:49 Preparing HOL-Probability/outline ...
18:13:56 Finished HOL-Probability/outline (0:00:07 elapsed time)
18:13:56 Timing HOL-Probability (8 threads, 73.374s elapsed time, 487.659s cpu time, 21.666s GC time, factor 6.65)
18:13:56 Finished HOL-Probability (0:01:35 elapsed time, 0:08:54 cpu time, factor 5.59)
18:13:57 Building Collections (on lxcisa1/1) ...
18:13:58 Collections: theory Collections.ICF_Tools
18:13:58 Collections: theory Collections.Partial_Equivalence_Relation
18:13:58 Collections: theory Finger-Trees.FingerTree
18:13:58 Collections: theory Binomial-Heaps.BinomialHeap
18:13:58 Collections: theory Binomial-Heaps.SkewBinomialHeap
18:13:58 Collections: theory HOL-Library.AList
18:13:58 Collections: theory HOL-Library.Code_Abstract_Nat
18:13:58 Collections: theory HOL-Library.Code_Target_Int
18:13:59 Collections: theory HOL-Library.Code_Target_Nat
18:13:59 Collections: theory Collections.Ord_Code_Preproc
18:13:59 Collections: theory HOL-Library.Confluence
18:13:59 Collections: theory Collections.Locale_Code
18:13:59 Collections: theory Collections.Record_Intf
18:13:59 Collections: theory HOL-Library.Confluent_Quotient
18:13:59 Collections: theory HOL-Library.Code_Target_Numeral
18:13:59 Collections: theory Collections.SetIterator
18:13:59 Collections: theory Collections.Sorted_List_Operations
18:13:59 Collections: theory Word_Lib.Bit_Comprehension
18:13:59 Collections: theory HOL-Library.Dlist
18:14:00 Collections: theory Word_Lib.More_Divides
18:14:00 Collections: theory HOL-Library.RBT_Impl
18:14:00 Collections: theory HOL-Library.Signed_Division
18:14:01 Collections: theory Collections.DatRef
18:14:01 Collections: theory Collections.Idx_Iterator
18:14:01 Collections: theory Collections.SetAbstractionIterator
18:14:02 Collections: theory Collections.SetIteratorOperations
18:14:02 Collections: theory Native_Word.Code_Int_Integer_Conversion
18:14:02 Collections: theory Word_Lib.Signed_Division_Word
18:14:02 Collections: theory Word_Lib.More_Arithmetic
18:14:02 Collections: theory Word_Lib.More_Bit_Ring
18:14:03 Collections: theory Word_Lib.More_Word
18:14:05 Collections: theory Collections.Assoc_List
18:14:05 Collections: theory Collections.Dlist_add
18:14:05 Collections: theory Collections.Proper_Iterator
18:14:05 Collections: theory Collections.SetIteratorGA
18:14:05 Collections: theory Collections.Diff_Array
18:14:06 Collections: theory Native_Word.Code_Target_Word_Base
18:14:06 Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
18:14:06 Collections: theory Collections.It_to_It
18:14:06 Collections: theory Collections.Gen_Iterator
18:14:06 Collections: theory Word_Lib.Least_significant_bit
18:14:07 Collections: theory Collections.Iterator
18:14:08 Collections: theory Collections.ICF_Spec_Base
18:14:08 Collections: theory Word_Lib.Most_significant_bit
18:14:08 Collections: theory Word_Lib.Generic_set_bit
18:14:08 Collections: theory Collections.MapSpec
18:14:09 Collections: theory Native_Word.Code_Target_Integer_Bit
18:14:09 Collections: theory Native_Word.Word_Type_Copies
18:14:12 Collections: theory Collections.Robdd
18:14:24 Collections: theory Native_Word.Code_Target_Int_Bit
18:14:24 Collections: theory Native_Word.Uint32
18:14:24 Collections: theory Collections.Code_Target_ICF
18:14:25 Collections: theory Collections.Locale_Code_Ex
18:14:26 Collections: theory Collections.HashCode
18:15:06 Collections: theory Collections.RBT_add
18:15:42 Collections: theory Collections.GenCF_Chapter
18:15:42 Collections: theory Collections.GenCF_Gen_Chapter
18:15:42 Collections: theory Collections.GenCF_Impl_Chapter
18:15:42 Collections: theory Collections.GenCF_Intf_Chapter
18:15:43 Collections: theory Collections.Intf_Comp
18:15:43 Collections: theory Collections.Impl_Array_Stack
18:15:43 Collections: theory Collections.Array_Iterator
18:15:43 Collections: theory HOL-Library.Product_Lexorder
18:15:43 Collections: theory Collections.Intf_Map
18:15:43 Collections: theory Collections.Intf_Set
18:15:43 Collections: theory Collections.Intf_Hash
18:15:43 Collections: theory Collections.Gen_Map
18:15:43 Collections: theory Collections.Gen_Set
18:15:43 Collections: theory Collections.Impl_Cfun_Set
18:15:43 Collections: theory Collections.Impl_List_Set
18:15:45 Collections: theory Collections.Gen_Comp
18:15:45 Collections: theory Collections.Impl_Array_Map
18:15:45 Collections: theory Collections.Impl_List_Map
18:15:45 Collections: theory Collections.Impl_RBT_Map
18:15:45 Collections: theory Collections.Gen_Map2Set
18:15:46 Collections: theory Collections.Impl_Array_Hash_Map
18:16:00 Collections: theory Collections.Impl_Bit_Set
18:16:00 Collections: theory Native_Word.Uint
18:16:00 Collections: theory Collections.Gen_Hash
18:16:02 Collections: theory Collections.Impl_Uv_Set
18:16:16 Collections: theory Collections.GenCF
18:16:19 Collections: theory Collections.ICF_Chapter
18:16:19 Collections: theory Collections.ICF_Spec_Chapter
18:16:19 Collections: theory Collections.ICF_Gen_Algo_Chapter
18:16:19 Collections: theory Collections.ICF_Impl_Chapter
18:16:19 Collections: theory Trie.Trie
18:16:19 Collections: theory Collections.AnnotatedListSpec
18:16:19 Collections: theory Collections.ListSpec
18:16:19 Collections: theory HOL-Library.RBT
18:16:19 Collections: theory Collections.PrioSpec
18:16:19 Collections: theory Collections.PrioUniqueSpec
18:16:20 Collections: theory Collections.SetSpec
18:16:21 Collections: theory Collections.BinoPrioImpl
18:16:21 Collections: theory Collections.SkewPrioImpl
18:16:21 Collections: theory Collections.ListGA
18:16:22 Collections: theory Collections.Trie_Impl
18:16:22 Collections: theory Collections.FTAnnotatedListImpl
18:16:22 Collections: theory Collections.PrioByAnnotatedList
18:16:22 Collections: theory Collections.Fifo
18:16:22 Collections: theory Collections.PrioUniqueByAnnotatedList
18:16:22 Collections: theory Collections.Trie2
18:16:24 Collections: theory Collections.Algos
18:16:24 Collections: theory Collections.SetIndex
18:16:25 Collections: theory Collections.SetIteratorCollectionsGA
18:16:25 Collections: theory Collections.MapGA
18:16:25 Collections: theory Collections.SetGA
18:16:28 Collections: theory Collections.FTPrioImpl
18:16:28 Collections: theory Collections.FTPrioUniqueImpl
18:16:30 Collections: theory Collections.ArrayMapImpl
18:16:30 Collections: theory Collections.ListMapImpl
18:16:31 Collections: theory Collections.ListMapImpl_Invar
18:16:31 Collections: theory Collections.TrieMapImpl
18:16:32 Collections: theory Collections.RBTMapImpl
18:16:33 Collections: theory Collections.ListSetImpl
18:16:33 Collections: theory Collections.ListSetImpl_Invar
18:16:35 Collections: theory Collections.ListSetImpl_NotDist
18:16:36 Collections: theory Collections.ListSetImpl_Sorted
18:16:37 Collections: theory Collections.SetByMap
18:16:38 Collections: theory Collections.ArrayHashMap_Impl
18:16:40 Collections: theory Collections.ArraySetImpl
18:16:40 Collections: theory Collections.TrieSetImpl
18:16:40 Collections: theory Collections.RBTSetImpl
18:16:40 Collections: theory Collections.HashMap_Impl
18:16:41 Collections: theory Collections.ArrayHashMap
18:16:42 Collections: theory Collections.HashMap
18:16:48 Collections: theory Collections.ArrayHashSet
18:16:48 Collections: theory Collections.HashSet
18:16:48 Collections: theory Collections.MapStdImpl
18:16:55 Collections: theory Collections.SetStdImpl
18:16:59 Collections: theory Collections.ICF_Impl
18:17:03 Collections: theory Collections.ICF_Refine_Monadic
18:17:03 Collections: theory Collections.ICF_Autoref
18:17:07 Collections: theory Collections.Collections_Entrypoints_Chapter
18:17:07 Collections: theory Collections.ICF_Entrypoints_Chapter
18:17:07 Collections: theory Collections.Userguides_Chapter
18:17:07 Collections: theory Collections.Collections
18:17:07 Collections: theory Collections.Refine_Dflt
18:17:07 Collections: theory Collections.CollectionsV1
18:17:07 Collections: theory Collections.ICF_Userguide
18:17:07 Collections: theory Collections.Refine_Dflt_Only_ICF
18:17:07 Collections: theory Collections.Refine_Dflt_ICF
18:17:08 Collections: theory Collections.Refine_Monadic_Userguide
18:18:26 Preparing Collections/document ...
18:18:43 Finished Collections/document (0:00:17 elapsed time)
18:18:43 Preparing Collections/outline ...
18:18:54 Finished Collections/outline (0:00:10 elapsed time)
18:18:54 Preparing Collections/userguide ...
18:18:57 Finished Collections/userguide (0:00:03 elapsed time)
18:18:58 Timing Collections (8 threads, 212.176s elapsed time, 986.259s cpu time, 66.179s GC time, factor 4.65)
18:18:58 Finished Collections (0:04:26 elapsed time, 0:18:34 cpu time, factor 4.18)
18:18:58 Building Jordan_Normal_Form (on lxcisa1/0) ...
18:19:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
18:19:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
18:19:08 Jordan_Normal_Form: theory Deriving.Comparator
18:19:08 Jordan_Normal_Form: theory Containers.Extend_Partial_Order
18:19:08 Jordan_Normal_Form: theory Containers.List_Fusion
18:19:08 Jordan_Normal_Form: theory Containers.Equal
18:19:08 Jordan_Normal_Form: theory Deriving.Derive_Manager
18:19:08 Jordan_Normal_Form: theory Deriving.Generator_Aux
18:19:08 Jordan_Normal_Form: theory Containers.Containers_Auxiliary
18:19:08 Jordan_Normal_Form: theory Abstract-Rewriting.Seq
18:19:08 Jordan_Normal_Form: theory Containers.Closure_Set
18:19:08 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
18:19:08 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
18:19:09 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
18:19:09 Jordan_Normal_Form: theory Deriving.Equality_Generator
18:19:09 Jordan_Normal_Form: theory Containers.Containers_Generator
18:19:09 Jordan_Normal_Form: theory Regular-Sets.Regular_Set
18:19:10 Jordan_Normal_Form: theory Deriving.Equality_Instances
18:19:10 Jordan_Normal_Form: theory Show.Show
18:19:10 Jordan_Normal_Form: theory Containers.Collection_Enum
18:19:10 Jordan_Normal_Form: theory Deriving.Compare
18:19:10 Jordan_Normal_Form: theory Deriving.Comparator_Generator
18:19:10 Jordan_Normal_Form: theory Containers.Lexicographic_Order
18:19:10 Jordan_Normal_Form: theory Containers.Collection_Eq
18:19:11 Jordan_Normal_Form: theory Containers.RBT_ext
18:19:11 Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl
18:19:11 Jordan_Normal_Form: theory Containers.Set_Linorder
18:19:11 Jordan_Normal_Form: theory Deriving.Compare_Generator
18:19:11 Jordan_Normal_Form: theory Containers.DList_Set
18:19:11 Jordan_Normal_Form: theory Deriving.Compare_Instances
18:19:12 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
18:19:12 Jordan_Normal_Form: theory Show.Show_Instances
18:19:13 Jordan_Normal_Form: theory Regular-Sets.Regular_Exp
18:19:13 Jordan_Normal_Form: theory Show.Shows_Literal
18:19:13 Jordan_Normal_Form: theory VectorSpace.FunctionLemmas
18:19:14 Jordan_Normal_Form: theory VectorSpace.RingModuleFacts
18:19:14 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
18:19:14 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
18:19:14 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
18:19:14 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
18:19:15 Jordan_Normal_Form: theory VectorSpace.MonoidSums
18:19:15 Jordan_Normal_Form: theory VectorSpace.LinearCombinations
18:19:17 Jordan_Normal_Form: theory Regular-Sets.NDerivative
18:19:17 Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation
18:19:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
18:19:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
18:19:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
18:19:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
18:19:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Shows_Literal_Matrix
18:19:22 Jordan_Normal_Form: theory VectorSpace.SumSpaces
18:19:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
18:19:22 Jordan_Normal_Form: theory VectorSpace.VectorSpace
18:19:22 Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking
18:19:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
18:19:23 Jordan_Normal_Form: theory Regular-Sets.Regexp_Method
18:19:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
18:19:23 Jordan_Normal_Form: theory Containers.Collection_Order
18:19:24 Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting
18:19:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
18:19:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
18:19:27 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders
18:19:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
18:19:27 Jordan_Normal_Form: theory Containers.RBT_Mapping2
18:19:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
18:19:28 Jordan_Normal_Form: theory Containers.RBT_Set2
18:19:29 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
18:19:29 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier
18:19:29 Jordan_Normal_Form: theory Matrix.Ordered_Semiring
18:19:30 Jordan_Normal_Form: theory Containers.Set_Impl
18:19:31 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
18:19:33 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
18:19:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
18:19:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
18:19:38 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
18:19:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
18:19:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
18:19:48 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
18:19:50 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
18:19:52 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
18:19:53 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
18:19:55 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
18:19:58 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
18:19:58 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
18:23:12 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
18:23:12 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
18:23:12 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
18:23:12 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
18:23:20 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
18:23:59 Preparing Jordan_Normal_Form/document ...
18:24:22 Finished Jordan_Normal_Form/document (0:00:22 elapsed time)
18:24:22 Preparing Jordan_Normal_Form/outline ...
18:24:31 Finished Jordan_Normal_Form/outline (0:00:09 elapsed time)
18:24:32 Timing Jordan_Normal_Form (8 threads, 261.041s elapsed time, 1545.424s cpu time, 59.660s GC time, factor 5.92)
18:24:32 Finished Jordan_Normal_Form (0:04:58 elapsed time, 0:27:09 cpu time, factor 5.46)
18:24:32 Building Abstract-Rewriting (on lxcisa1/1) ...
18:24:37 Abstract-Rewriting: theory Regular-Sets.Regular_Set
18:24:37 Abstract-Rewriting: theory Abstract-Rewriting.Seq
18:24:41 Abstract-Rewriting: theory Regular-Sets.Regular_Exp
18:24:44 Abstract-Rewriting: theory Regular-Sets.NDerivative
18:24:44 Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
18:24:47 Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
18:24:47 Abstract-Rewriting: theory Regular-Sets.Regexp_Method
18:24:48 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
18:24:51 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
18:24:51 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
18:24:54 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
18:25:10 Preparing Abstract-Rewriting/document ...
18:25:17 Finished Abstract-Rewriting/document (0:00:07 elapsed time)
18:25:17 Preparing Abstract-Rewriting/outline ...
18:25:21 Finished Abstract-Rewriting/outline (0:00:03 elapsed time)
18:25:21 Timing Abstract-Rewriting (8 threads, 24.629s elapsed time, 83.565s cpu time, 2.421s GC time, factor 3.39)
18:25:21 Finished Abstract-Rewriting (0:00:37 elapsed time, 0:01:49 cpu time, factor 2.93)
18:25:21 Building First_Order_Terms (on lxcisa1/0) ...
18:25:23 First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
18:25:23 First_Order_Terms: theory Fresh_Identifiers.Fresh
18:25:24 First_Order_Terms: theory First_Order_Terms.Renaming2
18:25:24 First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
18:25:24 First_Order_Terms: theory First_Order_Terms.Renaming2_String
18:25:24 First_Order_Terms: theory First_Order_Terms.Option_Monad
18:25:24 First_Order_Terms: theory First_Order_Terms.Fun_More
18:25:24 First_Order_Terms: theory First_Order_Terms.Seq_More
18:25:25 First_Order_Terms: theory First_Order_Terms.Term
18:25:27 First_Order_Terms: theory First_Order_Terms.Unifiers
18:25:27 First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
18:25:27 First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
18:25:27 First_Order_Terms: theory First_Order_Terms.Subsumption
18:25:28 First_Order_Terms: theory First_Order_Terms.Abstract_Matching
18:25:28 First_Order_Terms: theory First_Order_Terms.Abstract_Unification
18:25:29 First_Order_Terms: theory First_Order_Terms.Unification
18:25:31 First_Order_Terms: theory First_Order_Terms.Matching
18:25:31 First_Order_Terms: theory First_Order_Terms.Unification_String
18:25:33 First_Order_Terms: theory Deriving.Derive_Manager
18:25:33 First_Order_Terms: theory Matrix.Utility
18:25:33 First_Order_Terms: theory Deriving.Generator_Aux
18:25:33 First_Order_Terms: theory Show.Show
18:25:33 First_Order_Terms: theory Polynomial_Factorization.Missing_List
18:25:34 First_Order_Terms: theory Show.Show_Instances
18:25:35 First_Order_Terms: theory Show.Shows_Literal
18:25:36 First_Order_Terms: theory First_Order_Terms.Position
18:25:38 First_Order_Terms: theory First_Order_Terms.Term_More
18:26:02 Preparing First_Order_Terms/document ...
18:26:11 Finished First_Order_Terms/document (0:00:08 elapsed time)
18:26:11 Preparing First_Order_Terms/outline ...
18:26:16 Finished First_Order_Terms/outline (0:00:05 elapsed time)
18:26:16 Timing First_Order_Terms (8 threads, 24.810s elapsed time, 112.705s cpu time, 3.599s GC time, factor 4.54)
18:26:16 Finished First_Order_Terms (0:00:40 elapsed time, 0:02:25 cpu time, factor 3.59)
18:26:16 Building Expander_Graphs (on lxcisa1/1) ...
18:26:22 Expander_Graphs: theory Digit_Expansions.Bits_Digits
18:26:22 Expander_Graphs: theory Graph_Theory.Rtrancl_On
18:26:22 Expander_Graphs: theory HOL-Eisbach.Eisbach
18:26:22 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
18:26:22 Expander_Graphs: theory HOL-Decision_Procs.Dense_Linear_Order
18:26:22 Expander_Graphs: theory HOL-Library.Code_Target_Int
18:26:22 Expander_Graphs: theory HOL-Library.Code_Abstract_Nat
18:26:22 Expander_Graphs: theory HOL-Algebra.Congruence
18:26:22 Expander_Graphs: theory HOL-Library.Code_Target_Nat
18:26:23 Expander_Graphs: theory Finite_Fields.Finite_Fields_More_Bijections
18:26:23 Expander_Graphs: theory HOL-Combinatorics.List_Permutation
18:26:23 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
18:26:23 Expander_Graphs: theory HOL-Library.Code_Target_Numeral
18:26:23 Expander_Graphs: theory HOL-Library.Function_Algebras
18:26:23 Expander_Graphs: theory Abstract-Rewriting.Seq
18:26:23 Expander_Graphs: theory HOL-Library.More_List
18:26:23 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
18:26:24 Expander_Graphs: theory HOL-Library.While_Combinator
18:26:24 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
18:26:24 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
18:26:24 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
18:26:24 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
18:26:25 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
18:26:25 Expander_Graphs: theory HOL-Algebra.Order
18:26:25 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
18:26:25 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
18:26:25 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
18:26:25 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
18:26:26 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
18:26:26 Expander_Graphs: theory HOL-Library.Lattice_Algebras
18:26:26 Expander_Graphs: theory HOL-Library.Log_Nat
18:26:26 Expander_Graphs: theory HOL-Algebra.Lattice
18:26:26 Expander_Graphs: theory Graph_Theory.Stuff
18:26:26 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families
18:26:26 Expander_Graphs: theory Graph_Theory.Digraph
18:26:26 Expander_Graphs: theory Ergodic_Theory.SG_Library_Complement
18:26:27 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
18:26:27 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
18:26:28 Expander_Graphs: theory Matrix.Utility
18:26:28 Expander_Graphs: theory HOL-Algebra.Complete_Lattice
18:26:28 Expander_Graphs: theory Lp.Functional_Spaces
18:26:28 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
18:26:29 Expander_Graphs: theory Regular-Sets.Regular_Set
18:26:29 Expander_Graphs: theory Graph_Theory.Arc_Walk
18:26:29 Expander_Graphs: theory HOL-Algebra.Group
18:26:31 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
18:26:31 Expander_Graphs: theory VectorSpace.FunctionLemmas
18:26:31 Expander_Graphs: theory Graph_Theory.Pair_Digraph
18:26:32 Expander_Graphs: theory HOL-Algebra.Coset
18:26:32 Expander_Graphs: theory HOL-Algebra.FiniteProduct
18:26:32 Expander_Graphs: theory Lp.Lp
18:26:32 Expander_Graphs: theory HOL-Algebra.Ring
18:26:34 Expander_Graphs: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
18:26:34 Expander_Graphs: theory HOL-Library.Interval
18:26:34 Expander_Graphs: theory HOL-Library.Float
18:26:34 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
18:26:34 Expander_Graphs: theory HOL-Algebra.Generated_Groups
18:26:35 Expander_Graphs: theory HOL-Algebra.Divisibility
18:26:37 Expander_Graphs: theory HOL-Algebra.Elementary_Groups
18:26:38 Expander_Graphs: theory Universal_Hash_Families.Pseudorandom_Objects
18:26:38 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
18:26:38 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
18:26:38 Expander_Graphs: theory HOL-Library.Interval_Float
18:26:38 Expander_Graphs: theory Regular-Sets.Regular_Exp
18:26:39 Expander_Graphs: theory HOL-Algebra.AbelCoset
18:26:39 Expander_Graphs: theory HOL-Algebra.Module
18:26:39 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
18:26:39 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
18:26:40 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
18:26:40 Expander_Graphs: theory HOL-Decision_Procs.Approximation_Bounds
18:26:40 Expander_Graphs: theory Graph_Theory.Digraph_Component
18:26:41 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
18:26:41 Expander_Graphs: theory VectorSpace.RingModuleFacts
18:26:42 Expander_Graphs: theory VectorSpace.MonoidSums
18:26:42 Expander_Graphs: theory Regular-Sets.NDerivative
18:26:42 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
18:26:42 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
18:26:42 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
18:26:42 Expander_Graphs: theory VectorSpace.LinearCombinations
18:26:42 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
18:26:42 Expander_Graphs: theory HOL-Algebra.Ideal
18:26:43 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
18:26:44 Expander_Graphs: theory Jordan_Normal_Form.Matrix
18:26:45 Expander_Graphs: theory HOL-Decision_Procs.Approximation
18:26:45 Expander_Graphs: theory HOL-Algebra.RingHom
18:26:46 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
18:26:47 Expander_Graphs: theory HOL-Algebra.QuotRing
18:26:47 Expander_Graphs: theory HOL-Algebra.UnivPoly
18:26:47 Expander_Graphs: theory Regular-Sets.Regexp_Method
18:26:48 Expander_Graphs: theory VectorSpace.SumSpaces
18:26:48 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
18:26:49 Expander_Graphs: theory VectorSpace.VectorSpace
18:26:50 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
18:26:51 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
18:26:51 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
18:26:52 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
18:26:53 Expander_Graphs: theory Jordan_Normal_Form.Determinant
18:26:54 Expander_Graphs: theory Matrix.Ordered_Semiring
18:26:55 Expander_Graphs: theory Matrix.Matrix_Legacy
18:26:55 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
18:26:55 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
18:26:57 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
18:26:58 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
18:26:58 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
18:26:58 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
18:26:58 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
18:27:00 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
18:27:00 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
18:27:01 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
18:27:02 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
18:27:03 Expander_Graphs: theory HOL-Algebra.Multiplicative_Group
18:27:07 Expander_Graphs: theory HOL-Algebra.Ring_Divisibility
18:27:07 Expander_Graphs: theory HOL-Algebra.Subrings
18:27:11 Expander_Graphs: theory HOL-Algebra.Embedded_Algebras
18:27:13 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
18:27:16 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
18:27:17 Expander_Graphs: theory HOL-Algebra.Polynomials
18:27:20 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
18:27:26 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
18:27:26 Expander_Graphs: theory QHLProver.Complex_Matrix
18:27:26 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
18:27:32 Expander_Graphs: theory QHLProver.Gates
18:27:32 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
18:27:38 Expander_Graphs: theory HOL-Algebra.Polynomial_Divisibility
18:27:40 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
18:27:42 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
18:27:44 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
18:28:08 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
18:28:08 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
18:28:18 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
18:28:21 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
18:28:24 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
18:28:24 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
18:28:26 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
18:28:28 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
18:28:34 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
18:28:34 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
18:28:38 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
18:28:41 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
18:28:47 Expander_Graphs: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
18:37:41 Preparing Expander_Graphs/document ...
18:37:52 Finished Expander_Graphs/document (0:00:10 elapsed time)
18:37:52 Preparing Expander_Graphs/outline ...
18:37:56 Finished Expander_Graphs/outline (0:00:04 elapsed time)
18:37:57 Timing Expander_Graphs (8 threads, 622.059s elapsed time, 2458.153s cpu time, 197.021s GC time, factor 3.95)
18:37:57 Finished Expander_Graphs (0:11:17 elapsed time, 0:43:05 cpu time, factor 3.82)
18:37:57 Building Stateful_Protocol_Composition_and_Typing (on lxcisa1/0) ...
18:38:02 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
18:38:03 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
18:38:05 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
18:38:09 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
18:38:11 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
18:38:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
18:38:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
18:38:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
18:38:22 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
18:38:29 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
18:38:29 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
18:38:34 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
18:38:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
18:38:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
18:38:56 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
18:39:21 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
18:39:36 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
18:42:31 Preparing Stateful_Protocol_Composition_and_Typing/document ...
18:43:07 Finished Stateful_Protocol_Composition_and_Typing/document (0:00:35 elapsed time)
18:43:07 Preparing Stateful_Protocol_Composition_and_Typing/outline ...
18:43:22 Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:14 elapsed time)
18:43:22 Timing Stateful_Protocol_Composition_and_Typing (8 threads, 230.538s elapsed time, 1379.367s cpu time, 45.760s GC time, factor 5.98)
18:43:22 Finished Stateful_Protocol_Composition_and_Typing (0:04:31 elapsed time, 0:24:33 cpu time, factor 5.42)
18:43:22 Building Shadow_SC_DOM (on lxcisa1/1) ...
18:44:06 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
18:44:08 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
18:44:10 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
18:45:25 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
18:45:36 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
18:45:37 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
18:45:38 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
18:45:38 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
18:45:38 Shadow_SC_DOM: theory Shadow_SC_DOM.slots
18:45:38 Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
18:45:47 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
18:51:39 Preparing Shadow_SC_DOM/document ...
18:51:53 Finished Shadow_SC_DOM/document (0:00:14 elapsed time)
18:51:53 Preparing Shadow_SC_DOM/outline ...
18:52:02 Finished Shadow_SC_DOM/outline (0:00:08 elapsed time)
18:52:02 Timing Shadow_SC_DOM (8 threads, 412.446s elapsed time, 2434.215s cpu time, 173.623s GC time, factor 5.90)
18:52:02 Finished Shadow_SC_DOM (0:08:15 elapsed time, 0:43:47 cpu time, factor 5.31)
18:52:02 Running Cook_Levin (on lxcisa1/0) ...
18:52:06 Cook_Levin: theory Cook_Levin.Basics
18:52:06 Cook_Levin: theory HOL-Eisbach.Eisbach
18:52:08 Cook_Levin: theory Cook_Levin.Combinations
18:52:09 Cook_Levin: theory Cook_Levin.Elementary
18:52:11 Cook_Levin: theory Cook_Levin.Composing
18:52:11 Cook_Levin: theory Cook_Levin.Memorizing
18:52:12 Cook_Levin: theory Cook_Levin.Arithmetic
18:52:12 Cook_Levin: theory Cook_Levin.Oblivious
18:52:14 Cook_Levin: theory Cook_Levin.Oblivious_Polynomial
18:52:16 Cook_Levin: theory Cook_Levin.Lists_Lists
18:52:19 Cook_Levin: theory Cook_Levin.Two_Four_Symbols
18:52:20 Cook_Levin: theory Cook_Levin.Symbol_Ops
18:52:22 Cook_Levin: theory Cook_Levin.Wellformed
18:52:22 Cook_Levin: theory Cook_Levin.NP
18:52:22 Cook_Levin: theory Cook_Levin.Oblivious_2_Tape
18:52:24 Cook_Levin: theory Cook_Levin.Satisfiability
18:52:28 Cook_Levin: theory Cook_Levin.Reducing
18:52:29 Cook_Levin: theory Cook_Levin.Aux_TM_Reducing
18:52:33 Cook_Levin: theory Cook_Levin.Sat_TM_CNF
18:52:39 Cook_Levin: theory Cook_Levin.Reduction_TM
19:04:11 Preparing Cook_Levin/document ...
19:05:33 Finished Cook_Levin/document (0:01:22 elapsed time)
19:05:33 Preparing Cook_Levin/outline ...
19:06:06 Finished Cook_Levin/outline (0:00:32 elapsed time)
19:06:06 Timing Cook_Levin (8 threads, 721.321s elapsed time, 3761.286s cpu time, 38.590s GC time, factor 5.21)
19:06:06 Finished Cook_Levin (0:12:04 elapsed time, 1:02:48 cpu time, factor 5.20)
19:06:07 Running Finite_Fields (on lxcisa1/1) ...
19:06:12 Finite_Fields: theory Flow_Networks.Graph
19:06:12 Finite_Fields: theory Digit_Expansions.Bits_Digits
19:06:12 Finite_Fields: theory HOL-Number_Theory.Cong
19:06:12 Finite_Fields: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
19:06:12 Finite_Fields: theory HOL-Number_Theory.Eratosthenes
19:06:12 Finite_Fields: theory HOL-Real_Asymp.Inst_Existentials
19:06:12 Finite_Fields: theory HOL-Types_To_Sets.Types_To_Sets
19:06:12 Finite_Fields: theory HOL-Analysis.Metric_Arith
19:06:12 Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results
19:06:13 Finite_Fields: theory Finite_Fields.Finite_Fields_More_Bijections
19:06:13 Finite_Fields: theory HOL-Analysis.Abstract_Topology
19:06:13 Finite_Fields: theory HOL-Analysis.Continuum_Not_Denumerable
19:06:13 Finite_Fields: theory HOL-Analysis.Inner_Product
19:06:13 Finite_Fields: theory HOL-Analysis.L2_Norm
19:06:13 Finite_Fields: theory HOL-Analysis.Operator_Norm
19:06:13 Finite_Fields: theory HOL-Analysis.Poly_Roots
19:06:14 Finite_Fields: theory HOL-Analysis.Product_Vector
19:06:14 Finite_Fields: theory HOL-Combinatorics.Multiset_Permutations
19:06:14 Finite_Fields: theory HOL-Number_Theory.Mod_Exp
19:06:14 Finite_Fields: theory HOL-Analysis.Sigma_Algebra
19:06:15 Finite_Fields: theory Flow_Networks.Network
19:06:15 Finite_Fields: theory HOL-Analysis.Norm_Arith
19:06:15 Finite_Fields: theory HOL-Number_Theory.Fib
19:06:15 Finite_Fields: theory HOL-Number_Theory.Prime_Powers
19:06:16 Finite_Fields: theory HOL-Number_Theory.Totient
19:06:16 Finite_Fields: theory HOL-Real_Asymp.Eventuallize
19:06:16 Finite_Fields: theory HOL-Real_Asymp.Lazy_Eval
19:06:17 Finite_Fields: theory HOL-Analysis.Elementary_Topology
19:06:17 Finite_Fields: theory Flow_Networks.Residual_Graph
19:06:17 Finite_Fields: theory HOL-Analysis.Euclidean_Space
19:06:17 Finite_Fields: theory HOL-Number_Theory.Residues
19:06:18 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion
19:06:18 Finite_Fields: theory HOL-Analysis.Measurable
19:06:19 Finite_Fields: theory HOL-Analysis.Abstract_Limits
19:06:20 Finite_Fields: theory HOL-Analysis.FSigma
19:06:20 Finite_Fields: theory HOL-Analysis.Sum_Topology
19:06:20 Finite_Fields: theory HOL-Analysis.Measure_Space
19:06:21 Finite_Fields: theory Flow_Networks.Augmenting_Flow
19:06:22 Finite_Fields: theory Flow_Networks.Augmenting_Path
19:06:22 Finite_Fields: theory HOL-Analysis.Finite_Cartesian_Product
19:06:22 Finite_Fields: theory HOL-Analysis.Linear_Algebra
19:06:22 Finite_Fields: theory Flow_Networks.Ford_Fulkerson
19:06:22 Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
19:06:22 Finite_Fields: theory HOL-Analysis.Abstract_Topology_2
19:06:22 Finite_Fields: theory Finite_Fields.Ring_Characteristic
19:06:23 Finite_Fields: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
19:06:24 Finite_Fields: theory HOL-Analysis.Affine
19:06:25 Finite_Fields: theory MFMC_Countable.MFMC_Finite
19:06:26 Finite_Fields: theory HOL-Analysis.Cartesian_Space
19:06:26 Finite_Fields: theory HOL-Analysis.Convex
19:06:26 Finite_Fields: theory HOL-Analysis.Infinite_Sum
19:06:26 Finite_Fields: theory HOL-Analysis.Caratheodory
19:06:26 Finite_Fields: theory HOL-Analysis.Connected
19:06:26 Finite_Fields: theory HOL-Analysis.Elementary_Metric_Spaces
19:06:27 Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
19:06:27 Finite_Fields: theory HOL-Analysis.Function_Topology
19:06:28 Finite_Fields: theory HOL-Number_Theory.Gauss
19:06:29 Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
19:06:29 Finite_Fields: theory HOL-Analysis.Product_Topology
19:06:29 Finite_Fields: theory HOL-Number_Theory.Pocklington
19:06:30 Finite_Fields: theory HOL-Analysis.Determinants
19:06:30 Finite_Fields: theory HOL-Analysis.T1_Spaces
19:06:31 Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
19:06:31 Finite_Fields: theory HOL-Analysis.Lindelof_Spaces
19:06:31 Finite_Fields: theory HOL-Number_Theory.Number_Theory
19:06:32 Finite_Fields: theory HOL-Analysis.Elementary_Normed_Spaces
19:06:32 Finite_Fields: theory HOL-Analysis.Function_Metric
19:06:32 Finite_Fields: theory HOL-Analysis.Isolated
19:06:33 Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
19:06:33 Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
19:06:33 Finite_Fields: theory HOL-Analysis.Topology_Euclidean_Space
19:06:33 Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
19:06:34 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
19:06:34 Finite_Fields: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
19:06:34 Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
19:06:35 Finite_Fields: theory HOL-Analysis.Extended_Real_Limits
19:06:35 Finite_Fields: theory HOL-Analysis.Line_Segment
19:06:35 Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
19:06:36 Finite_Fields: theory HOL-Analysis.Summation_Tests
19:06:36 Finite_Fields: theory HOL-Analysis.Convex_Euclidean_Space
19:06:37 Finite_Fields: theory HOL-Analysis.Tagged_Division
19:06:38 Finite_Fields: theory HOL-Analysis.Ordered_Euclidean_Space
19:06:38 Finite_Fields: theory HOL-Analysis.Starlike
19:06:38 Finite_Fields: theory Dirichlet_Series.Moebius_Mu
19:06:39 Finite_Fields: theory Dirichlet_Series.More_Totient
19:06:39 Finite_Fields: theory Dirichlet_Series.Divisor_Count
19:06:40 Finite_Fields: theory Dirichlet_Series.Liouville_Lambda
19:06:40 Finite_Fields: theory Dirichlet_Series.Arithmetic_Summatory
19:06:41 Finite_Fields: theory HOL-Analysis.Uniform_Limit
19:06:42 Finite_Fields: theory HOL-Analysis.Continuous_Extension
19:06:42 Finite_Fields: theory HOL-Analysis.Path_Connected
19:06:42 Finite_Fields: theory HOL-Analysis.Bounded_Continuous_Function
19:06:42 Finite_Fields: theory HOL-Analysis.Bounded_Linear_Function
19:06:43 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
19:06:44 Finite_Fields: theory HOL-Analysis.Locally
19:06:44 Finite_Fields: theory HOL-Analysis.Uncountable_Sets
19:06:45 Finite_Fields: theory HOL-Analysis.Homotopy
19:06:45 Finite_Fields: theory HOL-Analysis.Arcwise_Connected
19:06:45 Finite_Fields: theory HOL-Analysis.Derivative
19:06:51 Finite_Fields: theory HOL-Analysis.Borel_Space
19:06:51 Finite_Fields: theory HOL-Analysis.Cartesian_Euclidean_Space
19:06:51 Finite_Fields: theory HOL-Analysis.Complex_Analysis_Basics
19:06:51 Finite_Fields: theory HOL-Analysis.Abstract_Euclidean_Space
19:06:52 Finite_Fields: theory HOL-Analysis.Homeomorphism
19:06:52 Finite_Fields: theory HOL-Analysis.Sparse_In
19:06:52 Finite_Fields: theory HOL-Analysis.Cross3
19:06:52 Finite_Fields: theory HOL-Analysis.Polytope
19:06:52 Finite_Fields: theory HOL-Analysis.Abstract_Topological_Spaces
19:06:52 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
19:06:53 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test
19:06:55 Finite_Fields: theory HOL-Analysis.Complex_Transcendental
19:06:55 Finite_Fields: theory HOL-Analysis.Brouwer_Fixpoint
19:06:58 Finite_Fields: theory HOL-Analysis.Weierstrass_Theorems
19:06:58 Finite_Fields: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
19:07:01 Finite_Fields: theory HOL-Analysis.Regularity
19:07:02 Finite_Fields: theory HOL-Analysis.Fashoda_Theorem
19:07:03 Finite_Fields: theory HOL-Analysis.Abstract_Metric_Spaces
19:07:04 Finite_Fields: theory HOL-Analysis.Generalised_Binomial_Theorem
19:07:04 Finite_Fields: theory HOL-Analysis.Harmonic_Numbers
19:07:04 Finite_Fields: theory Executable_Randomized_Algorithms.Tau_Additivity
19:07:04 Finite_Fields: theory HOL-Analysis.FPS_Convergence
19:07:04 Finite_Fields: theory HOL-Analysis.Infinite_Products
19:07:04 Finite_Fields: theory HOL-Analysis.Retracts
19:07:05 Finite_Fields: theory HOL-Analysis.Binary_Product_Measure
19:07:06 Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
19:07:08 Finite_Fields: theory HOL-Analysis.Embed_Measure
19:07:08 Finite_Fields: theory HOL-Analysis.Finite_Product_Measure
19:07:08 Finite_Fields: theory HOL-Analysis.Smooth_Paths
19:07:09 Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test_Code
19:07:10 Finite_Fields: theory HOL-Analysis.Bochner_Integration
19:07:10 Finite_Fields: theory HOL-Probability.Fin_Map
19:07:10 Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
19:07:11 Finite_Fields: theory HOL-Analysis.Lipschitz
19:07:11 Finite_Fields: theory HOL-Analysis.Urysohn
19:07:12 Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
19:07:14 Finite_Fields: theory HOL-Analysis.Multivariate_Analysis
19:07:15 Finite_Fields: theory HOL-Analysis.Complete_Measure
19:07:15 Finite_Fields: theory HOL-Analysis.Radon_Nikodym
19:07:15 Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
19:07:16 Finite_Fields: theory HOL-Analysis.Set_Integral
19:07:16 Finite_Fields: theory HOL-Analysis.Lebesgue_Measure
19:07:18 Finite_Fields: theory HOL-Real_Asymp.Real_Asymp
19:07:19 Finite_Fields: theory HOL-Analysis.Infinite_Set_Sum
19:07:20 Finite_Fields: theory HOL-Analysis.Henstock_Kurzweil_Integration
19:07:23 Finite_Fields: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
19:07:23 Finite_Fields: theory HOL-Analysis.Integral_Test
19:07:23 Finite_Fields: theory HOL-Analysis.Kronecker_Approximation_Theorem
19:07:26 Finite_Fields: theory HOL-Analysis.Further_Topology
19:07:26 Finite_Fields: theory HOL-Analysis.Gamma_Function
19:07:26 Finite_Fields: theory HOL-Analysis.Improper_Integral
19:07:26 Finite_Fields: theory HOL-Analysis.Interval_Integral
19:07:26 Finite_Fields: theory HOL-Analysis.Vitali_Covering_Theorem
19:07:27 Finite_Fields: theory HOL-Analysis.Equivalence_Measurable_On_Borel
19:07:28 Finite_Fields: theory HOL-Analysis.Lebesgue_Integral_Substitution
19:07:28 Finite_Fields: theory HOL-Analysis.Change_Of_Vars
19:07:31 Finite_Fields: theory HOL-Analysis.Simplex_Content
19:07:32 Finite_Fields: theory HOL-Analysis.Jordan_Curve
19:07:33 Finite_Fields: theory HOL-Analysis.Ball_Volume
19:07:33 Finite_Fields: theory HOL-Analysis.Analysis
19:07:35 Finite_Fields: theory Dirichlet_Series.Euler_Products
19:07:35 Finite_Fields: theory Dirichlet_Series.Partial_Summation
19:07:35 Finite_Fields: theory HOL-Complex_Analysis.Contour_Integration
19:07:35 Finite_Fields: theory HOL-Probability.Discrete_Topology
19:07:35 Finite_Fields: theory HOL-Probability.Essential_Supremum
19:07:35 Finite_Fields: theory HOL-Probability.Probability_Measure
19:07:35 Finite_Fields: theory HOL-Probability.Stopping_Time
19:07:35 Finite_Fields: theory HOL-Probability.Tree_Space
19:07:36 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
19:07:37 Finite_Fields: theory HOL-Complex_Analysis.Winding_Numbers
19:07:38 Finite_Fields: theory HOL-Probability.Conditional_Expectation
19:07:38 Finite_Fields: theory HOL-Probability.Distribution_Functions
19:07:38 Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
19:07:38 Finite_Fields: theory HOL-Probability.Weak_Convergence
19:07:38 Finite_Fields: theory HOL-Probability.Giry_Monad
19:07:39 Finite_Fields: theory HOL-Probability.Helly_Selection
19:07:40 Finite_Fields: theory HOL-Complex_Analysis.Conformal_Mappings
19:07:42 Finite_Fields: theory HOL-Complex_Analysis.Complex_Singularities
19:07:42 Finite_Fields: theory HOL-Complex_Analysis.Great_Picard
19:07:42 Finite_Fields: theory HOL-Probability.Probability_Mass_Function
19:07:42 Finite_Fields: theory HOL-Probability.Projective_Family
19:07:42 Finite_Fields: theory HOL-Complex_Analysis.Riemann_Mapping
19:07:44 Finite_Fields: theory HOL-Probability.Infinite_Product_Measure
19:07:44 Finite_Fields: theory HOL-Complex_Analysis.Complex_Residues
19:07:45 Finite_Fields: theory HOL-Complex_Analysis.Residue_Theorem
19:07:45 Finite_Fields: theory HOL-Probability.Independent_Family
19:07:45 Finite_Fields: theory HOL-Probability.Projective_Limit
19:07:45 Finite_Fields: theory HOL-Probability.Stream_Space
19:07:46 Finite_Fields: theory HOL-Complex_Analysis.Laurent_Convergence
19:07:46 Finite_Fields: theory Finite_Fields.Finite_Fields_More_PMF
19:07:46 Finite_Fields: theory HOL-Probability.PMF_Impl
19:07:46 Finite_Fields: theory HOL-Probability.Random_Permutations
19:07:46 Finite_Fields: theory HOL-Probability.SPMF
19:07:47 Finite_Fields: theory HOL-Probability.Convolution
19:07:47 Finite_Fields: theory HOL-Probability.Information
19:07:47 Finite_Fields: theory HOL-Probability.Product_PMF
19:07:48 Finite_Fields: theory HOL-Probability.Hoeffding
19:07:50 Finite_Fields: theory HOL-Complex_Analysis.Meromorphic
19:07:51 Finite_Fields: theory HOL-Probability.Distributions
19:07:51 Finite_Fields: theory HOL-Complex_Analysis.Weierstrass_Factorization
19:07:52 Finite_Fields: theory HOL-Complex_Analysis.Complex_Analysis
19:07:52 Finite_Fields: theory HOL-Probability.Characteristic_Functions
19:07:52 Finite_Fields: theory HOL-Probability.Sinc_Integral
19:07:53 Finite_Fields: theory Dirichlet_Series.Dirichlet_Series_Analysis
19:07:53 Finite_Fields: theory HOL-Probability.Levy
19:07:53 Finite_Fields: theory HOL-Probability.Central_Limit_Theorem
19:07:53 Finite_Fields: theory HOL-Probability.Probability
19:07:54 Finite_Fields: theory Executable_Randomized_Algorithms.Coin_Space
19:07:54 Finite_Fields: theory MFMC_Countable.MFMC_Misc
19:07:54 Finite_Fields: theory MFMC_Countable.Matrix_For_Marginals
19:07:55 Finite_Fields: theory Zeta_Function.Zeta_Library
19:07:56 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
19:07:57 Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm
19:07:59 Finite_Fields: theory MFMC_Countable.Rel_PMF_Characterisation
19:07:59 Finite_Fields: theory Probabilistic_While.While_SPMF
19:08:00 Finite_Fields: theory Finite_Fields.Find_Irreducible_Poly
19:17:39 Preparing Finite_Fields/document ...
19:17:49 Finished Finite_Fields/document (0:00:10 elapsed time)
19:17:49 Preparing Finite_Fields/outline ...
19:17:53 Finished Finite_Fields/outline (0:00:04 elapsed time)
19:17:54 Timing Finite_Fields (8 threads, 668.648s elapsed time, 4523.127s cpu time, 322.809s GC time, factor 6.76)
19:17:54 Finished Finite_Fields (0:11:14 elapsed time, 1:15:44 cpu time, factor 6.74)
19:17:54 Running Modular_arithmetic_LLL_and_HNF_algorithms (on lxcisa1/0) ...
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
19:18:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
19:18:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
19:18:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
19:18:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
19:18:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
19:18:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
19:18:04 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
19:18:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
19:18:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
19:18:06 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
19:18:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
19:18:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
19:18:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
19:18:07 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
19:18:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
19:18:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
19:18:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
19:18:10 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
19:18:11 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
19:18:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
19:18:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
19:18:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
19:18:12 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
19:18:13 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
19:18:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
19:18:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
19:18:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
19:18:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
19:18:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
19:18:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
19:18:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
19:18:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
19:18:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
19:18:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
19:18:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Show.Shows_Literal
19:18:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
19:18:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
19:18:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Shows_Literal_Matrix
19:18:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
19:18:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
19:18:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
19:18:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
19:18:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
19:18:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
19:18:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
19:18:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
19:18:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
19:18:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
19:18:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
19:18:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
19:18:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
19:18:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
19:18:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
19:18:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
19:18:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
19:18:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
19:18:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
19:18:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
19:18:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
19:18:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
19:18:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
19:18:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
19:18:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
19:18:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
19:18:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
19:18:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
19:18:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
19:18:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
19:18:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
19:18:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
19:18:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
19:18:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
19:18:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
19:19:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
19:19:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
19:19:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
19:19:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
19:19:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
19:19:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
19:19:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
19:19:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
19:19:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
19:19:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
19:19:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
19:19:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
19:19:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
19:19:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
19:19:54 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
19:19:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
19:19:55 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
19:20:00 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
19:20:01 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
19:20:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
19:20:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
19:20:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
19:21:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
19:21:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
19:22:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
19:22:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
19:22:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
19:23:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
19:23:02 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
19:23:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
19:23:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
19:23:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
19:23:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
19:29:27 Preparing Modular_arithmetic_LLL_and_HNF_algorithms/document ...
19:29:42 Finished Modular_arithmetic_LLL_and_HNF_algorithms/document (0:00:14 elapsed time)
19:29:42 Preparing Modular_arithmetic_LLL_and_HNF_algorithms/outline ...
19:29:47 Finished Modular_arithmetic_LLL_and_HNF_algorithms/outline (0:00:04 elapsed time)
19:29:47 Timing Modular_arithmetic_LLL_and_HNF_algorithms (8 threads, 681.061s elapsed time, 4310.237s cpu time, 293.870s GC time, factor 6.33)
19:29:47 Finished Modular_arithmetic_LLL_and_HNF_algorithms (0:11:27 elapsed time, 1:12:07 cpu time, factor 6.30)
19:29:47 Running MiniSail (on lxcisa1/1) ...
19:29:49 MiniSail: theory FinFun.FinFun
19:29:49 MiniSail: theory HOL-Eisbach.Eisbach
19:29:51 MiniSail: theory HOL-Eisbach.Eisbach_Tools
19:29:51 MiniSail: theory Nominal2.Nominal2_Base
19:29:57 MiniSail: theory Nominal2.Nominal2_Abs
19:29:59 MiniSail: theory Nominal2.Nominal2_FCB
19:29:59 MiniSail: theory Nominal2.Nominal2
19:30:03 MiniSail: theory MiniSail.Nominal-Utils
19:30:04 MiniSail: theory MiniSail.Syntax
19:30:56 MiniSail: theory MiniSail.BTVSubst
19:30:56 MiniSail: theory MiniSail.IVSubst
19:31:01 MiniSail: theory MiniSail.Wellformed
19:31:02 MiniSail: theory MiniSail.SyntaxL
19:32:43 MiniSail: theory MiniSail.RCLogic
19:32:43 MiniSail: theory MiniSail.WellformedL
19:33:04 MiniSail: theory MiniSail.SubstMethods
19:33:10 MiniSail: theory MiniSail.RCLogicL
19:33:12 MiniSail: theory MiniSail.Typing
19:35:29 MiniSail: theory MiniSail.Operational
19:35:30 MiniSail: theory MiniSail.TypingL
19:35:46 MiniSail: theory MiniSail.ContextSubtypingL
19:35:49 MiniSail: theory MiniSail.BTVSubstTypingL
19:35:50 MiniSail: theory MiniSail.IVSubstTypingL
19:35:51 MiniSail: theory MiniSail.Safety
19:35:53 MiniSail: theory MiniSail.MiniSail
19:41:30 Preparing MiniSail/document ...
19:41:58 Finished MiniSail/document (0:00:27 elapsed time)
19:41:58 Preparing MiniSail/outline ...
19:42:09 Finished MiniSail/outline (0:00:10 elapsed time)
19:42:09 Timing MiniSail (8 threads, 696.750s elapsed time, 3491.010s cpu time, 177.802s GC time, factor 5.01)
19:42:09 Finished MiniSail (0:11:40 elapsed time, 0:58:17 cpu time, factor 5.00)
19:42:09 Building CAVA_Base (on lxcisa1/0) ...
19:42:12 CAVA_Base: theory CAVA_Base.Lexord_List
19:42:12 CAVA_Base: theory CAVA_Base.Statistics
19:42:12 CAVA_Base: theory Deriving.Comparator
19:42:12 CAVA_Base: theory Deriving.Derive_Manager
19:42:12 CAVA_Base: theory Deriving.Generator_Aux
19:42:12 CAVA_Base: theory HOL-Library.Char_ord
19:42:12 CAVA_Base: theory HOL-Library.Old_Datatype
19:42:12 CAVA_Base: theory HOL-Library.Nat_Bijection
19:42:12 CAVA_Base: theory CAVA_Base.Code_String
19:42:12 CAVA_Base: theory CAVA_Base.CAVA_Code_Target
19:42:12 CAVA_Base: theory Deriving.Equality_Generator
19:42:12 CAVA_Base: theory Deriving.Hash_Generator
19:42:12 CAVA_Base: theory CAVA_Base.CAVA_Base
19:42:13 CAVA_Base: theory HOL-Library.Countable
19:42:13 CAVA_Base: theory Deriving.Equality_Instances
19:42:13 CAVA_Base: theory Deriving.Hash_Instances
19:42:13 CAVA_Base: theory Deriving.Compare
19:42:13 CAVA_Base: theory Deriving.Comparator_Generator
19:42:13 CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base
19:42:14 CAVA_Base: theory Deriving.Compare_Generator
19:42:14 CAVA_Base: theory Deriving.Countable_Generator
19:42:15 CAVA_Base: theory Deriving.Compare_Instances
19:42:15 CAVA_Base: theory Deriving.Derive
19:42:28 Timing CAVA_Base (8 threads, 5.435s elapsed time, 23.366s cpu time, 0.522s GC time, factor 4.30)
19:42:28 Finished CAVA_Base (0:00:18 elapsed time, 0:00:49 cpu time, factor 2.70)
19:42:28 Building CAVA_Automata (on lxcisa1/1) ...
19:42:31 CAVA_Automata: theory CAVA_Automata.Step_Conv
19:42:31 CAVA_Automata: theory HOL-Library.Omega_Words_Fun
19:42:31 CAVA_Automata: theory CAVA_Automata.Digraph_Basic
19:42:32 CAVA_Automata: theory CAVA_Automata.Digraph
19:42:34 CAVA_Automata: theory CAVA_Automata.Automata
19:42:34 CAVA_Automata: theory CAVA_Automata.Digraph_Impl
19:42:40 CAVA_Automata: theory CAVA_Automata.Lasso
19:42:40 CAVA_Automata: theory CAVA_Automata.Simulation
19:42:41 CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
19:42:56 CAVA_Automata: theory CAVA_Automata.Automata_Impl
19:43:34 CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
19:43:48 Preparing CAVA_Automata/document ...
19:43:52 Finished CAVA_Automata/document (0:00:03 elapsed time)
19:43:52 Preparing CAVA_Automata/outline ...
19:43:55 Finished CAVA_Automata/outline (0:00:02 elapsed time)
19:43:55 Timing CAVA_Automata (8 threads, 64.638s elapsed time, 116.790s cpu time, 4.302s GC time, factor 1.81)
19:43:55 Finished CAVA_Automata (0:01:19 elapsed time, 0:02:27 cpu time, factor 1.86)
19:43:55 Building CAVA_Setup (on lxcisa1/0) ...
19:43:58 CAVA_Setup: theory Partial_Order_Reduction.Basic_Extensions
19:43:58 CAVA_Setup: theory Partial_Order_Reduction.Set_Extensions
19:43:58 CAVA_Setup: theory HOL-Library.Case_Converter
19:43:58 CAVA_Setup: theory HOL-Library.IArray
19:43:58 CAVA_Setup: theory DFS_Framework.DFS_Framework_Misc
19:43:58 CAVA_Setup: theory HOL-Library.Complete_Partial_Order2
19:43:58 CAVA_Setup: theory HOL-Library.Mapping
19:43:58 CAVA_Setup: theory HOL-Library.Stream
19:43:58 CAVA_Setup: theory HOL-Library.Sublist
19:43:58 CAVA_Setup: theory Partial_Order_Reduction.Functions
19:43:58 CAVA_Setup: theory HOL-Library.Simps_Case_Conv
19:43:58 CAVA_Setup: theory HOL-Library.Countable_Set
19:43:59 CAVA_Setup: theory LTL.LTL
19:43:59 CAVA_Setup: theory Partial_Order_Reduction.Relation_Extensions
19:43:59 CAVA_Setup: theory Promela.PromelaAST
19:43:59 CAVA_Setup: theory DFS_Framework.DFS_Framework_Refine_Aux
19:44:00 CAVA_Setup: theory HOL-Library.Countable_Complete_Lattices
19:44:00 CAVA_Setup: theory SM.SM_Syntax
19:44:00 CAVA_Setup: theory SM.SOS_Misc_Add
19:44:01 CAVA_Setup: theory Stuttering_Equivalence.Samplers
19:44:01 CAVA_Setup: theory HOL-Library.RBT_Mapping
19:44:01 CAVA_Setup: theory Stuttering_Equivalence.StutterEquivalence
19:44:01 CAVA_Setup: theory Transition_Systems_and_Automata.Basic
19:44:01 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence
19:44:01 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton
19:44:02 CAVA_Setup: theory HOL-Library.Prefix_Order
19:44:02 CAVA_Setup: theory Partial_Order_Reduction.List_Prefixes
19:44:02 CAVA_Setup: theory Partial_Order_Reduction.List_Extensions
19:44:02 CAVA_Setup: theory SM.LTS
19:44:02 CAVA_Setup: theory SM.Gen_Scheduler
19:44:02 CAVA_Setup: theory Partial_Order_Reduction.Word_Prefixes
19:44:03 CAVA_Setup: theory Partial_Order_Reduction.Traces
19:44:03 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System
19:44:03 CAVA_Setup: theory DFS_Framework.Impl_Rev_Array_Stack
19:44:03 CAVA_Setup: theory HOL-Library.Order_Continuity
19:44:03 CAVA_Setup: theory DFS_Framework.Param_DFS
19:44:04 CAVA_Setup: theory HOL-Library.Extended_Nat
19:44:05 CAVA_Setup: theory SM.Gen_Scheduler_Refine
19:44:05 CAVA_Setup: theory SM.SM_Cfg
19:44:05 CAVA_Setup: theory Promela.PromelaStatistics
19:44:05 CAVA_Setup: theory Gabow_SCC.Find_Path
19:44:05 CAVA_Setup: theory Gabow_SCC.Find_Path_Impl
19:44:05 CAVA_Setup: theory Coinductive.Coinductive_Nat
19:44:05 CAVA_Setup: theory HOL-Library.Linear_Temporal_Logic_on_Streams
19:44:06 CAVA_Setup: theory Gabow_SCC.Gabow_SCC
19:44:07 CAVA_Setup: theory Coinductive.Coinductive_List
19:44:07 CAVA_Setup: theory Partial_Order_Reduction.ENat_Extensions
19:44:07 CAVA_Setup: theory Partial_Order_Reduction.CCPO_Extensions
19:44:07 CAVA_Setup: theory Transition_Systems_and_Automata.Sequence_LTL
19:44:08 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Construction
19:44:09 CAVA_Setup: theory Partial_Order_Reduction.ESet_Extensions
19:44:09 CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Extra
19:44:09 CAVA_Setup: theory SM.Gen_Cfg_Bisim
19:44:09 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Extensions
19:44:10 CAVA_Setup: theory DFS_Framework.DFS_Invars_Basic
19:44:10 CAVA_Setup: theory DFS_Framework.General_DFS_Structure
19:44:11 CAVA_Setup: theory Gabow_SCC.Gabow_GBG
19:44:12 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Traces
19:44:12 CAVA_Setup: theory SM.Pid_Scheduler
19:44:13 CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton_Code
19:44:15 CAVA_Setup: theory Coinductive.Coinductive_List_Prefix
19:44:16 CAVA_Setup: theory Coinductive.Coinductive_Stream
19:44:16 CAVA_Setup: theory Word_Lib.Bits_Int
19:44:17 CAVA_Setup: theory Partial_Order_Reduction.Coinductive_List_Extensions
19:44:17 CAVA_Setup: theory Stuttering_Equivalence.PLTL
19:44:17 CAVA_Setup: theory DFS_Framework.Rec_Impl
19:44:18 CAVA_Setup: theory DFS_Framework.Tailrec_Impl
19:44:18 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA
19:44:19 CAVA_Setup: theory Partial_Order_Reduction.LList_Prefixes
19:44:20 CAVA_Setup: theory Partial_Order_Reduction.Stuttering
19:44:21 CAVA_Setup: theory Word_Lib.Typedef_Morphisms
19:44:21 CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
19:44:21 CAVA_Setup: theory SM.SM_State
19:44:22 CAVA_Setup: theory Partial_Order_Reduction.Ample_Abstract
19:44:23 CAVA_Setup: theory Partial_Order_Reduction.Ample_Analysis
19:44:23 CAVA_Setup: theory SM.SM_Semantics
19:44:24 CAVA_Setup: theory Promela.PromelaDatastructures
19:44:26 CAVA_Setup: theory DFS_Framework.Simple_Impl
19:44:26 CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA_impl
19:44:28 CAVA_Setup: theory SM.Decide_Locality
19:44:28 CAVA_Setup: theory SM.SM_LTL
19:44:30 CAVA_Setup: theory SM.Type_System
19:44:33 CAVA_Setup: theory DFS_Framework.Restr_Impl
19:44:34 CAVA_Setup: theory SM.SM_Finite_Reachable
19:44:34 CAVA_Setup: theory SM.Rename_Cfg
19:44:35 CAVA_Setup: theory DFS_Framework.DFS_Framework
19:44:36 CAVA_Setup: theory DFS_Framework.Reachable_Nodes
19:44:43 CAVA_Setup: theory SM.SM_Visible
19:44:44 CAVA_Setup: theory Gabow_SCC.Gabow_GBG_Code
19:44:44 CAVA_Setup: theory Gabow_SCC.Gabow_SCC_Code
19:44:46 CAVA_Setup: theory SM.SM_Pid
19:44:50 CAVA_Setup: theory SM.SM_Variables
19:44:51 CAVA_Setup: theory SM.SM_Indep
19:45:21 CAVA_Setup: theory LTL_to_GBA.All_Of_LTL_to_GBA
19:45:29 CAVA_Setup: theory DFS_Framework.Feedback_Arcs
19:45:50 CAVA_Setup: theory Promela.PromelaInvariants
19:45:52 CAVA_Setup: theory Promela.Promela
19:46:09 CAVA_Setup: theory Gabow_SCC.All_Of_Gabow_SCC
19:46:10 CAVA_Setup: theory SM.SM_Datastructures
19:46:10 CAVA_Setup: theory SM.SM_Sticky
19:46:20 CAVA_Setup: theory SM.SM_POR
19:46:35 CAVA_Setup: theory SM.SM_Ample_Impl
19:47:03 CAVA_Setup: theory Promela.PromelaLTL
19:47:05 CAVA_Setup: theory Promela.PromelaLTLConv
19:47:15 CAVA_Setup: theory Promela.All_Of_Promela
19:48:12 CAVA_Setup: theory SM.SM_Wrapup
19:50:23 Timing CAVA_Setup (8 threads, 327.171s elapsed time, 2174.725s cpu time, 122.930s GC time, factor 6.65)
19:50:23 Finished CAVA_Setup (0:06:23 elapsed time, 0:38:26 cpu time, factor 6.01)
19:50:23 Building Subresultants (on lxcisa1/1) ...
19:50:26 Subresultants: theory Subresultants.Coeff_Int
19:50:26 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
19:50:26 Subresultants: theory Subresultants.Dichotomous_Lazard
19:50:26 Subresultants: theory Subresultants.More_Homomorphisms
19:50:26 Subresultants: theory Subresultants.Binary_Exponentiation
19:50:26 Subresultants: theory Subresultants.Resultant_Prelim
19:50:27 Subresultants: theory Subresultants.Subresultant
19:50:32 Subresultants: theory Subresultants.Subresultant_Gcd
19:51:29 Preparing Subresultants/document ...
19:51:35 Finished Subresultants/document (0:00:05 elapsed time)
19:51:35 Preparing Subresultants/outline ...
19:51:38 Finished Subresultants/outline (0:00:03 elapsed time)
19:51:38 Timing Subresultants (8 threads, 47.718s elapsed time, 207.589s cpu time, 2.407s GC time, factor 4.35)
19:51:38 Finished Subresultants (0:01:05 elapsed time, 0:04:04 cpu time, factor 3.72)
19:51:38 Building Sepref_Prereq (on lxcisa1/0) ...
19:51:40 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
19:51:40 Sepref_Prereq: theory HOL-Library.Old_Datatype
19:51:40 Sepref_Prereq: theory HOL-Library.Nat_Bijection
19:51:41 Sepref_Prereq: theory HOL-Library.Countable
19:51:43 Sepref_Prereq: theory HOL-Imperative_HOL.Heap
19:51:45 Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
19:51:47 Sepref_Prereq: theory HOL-Imperative_HOL.Array
19:51:48 Sepref_Prereq: theory HOL-Imperative_HOL.Ref
19:51:48 Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
19:51:48 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
19:51:48 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
19:51:48 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
19:51:51 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
19:51:51 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
19:51:52 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
19:51:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
19:51:54 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
19:51:57 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
19:51:58 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
19:52:03 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
19:52:09 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
19:52:09 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
19:52:09 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
19:52:09 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
19:52:10 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
19:52:13 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
19:52:30 Timing Sepref_Prereq (8 threads, 35.143s elapsed time, 104.938s cpu time, 2.983s GC time, factor 2.99)
19:52:30 Finished Sepref_Prereq (0:00:50 elapsed time, 0:02:17 cpu time, factor 2.70)
19:52:30 Building Syntax_Independent_Logic (on lxcisa1/1) ...
19:52:31 Syntax_Independent_Logic: theory HOL-Eisbach.Eisbach
19:52:32 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Prelim
19:52:35 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax
19:52:39 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction
19:52:40 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax_Arith
19:52:43 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Natural_Deduction
19:52:43 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Standard_Model
19:53:13 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Pseudo_Term
19:53:13 Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction_Q
19:55:27 Preparing Syntax_Independent_Logic/document ...
19:55:36 Finished Syntax_Independent_Logic/document (0:00:09 elapsed time)
19:55:36 Preparing Syntax_Independent_Logic/outline ...
19:55:42 Finished Syntax_Independent_Logic/outline (0:00:05 elapsed time)
19:55:42 Timing Syntax_Independent_Logic (8 threads, 165.316s elapsed time, 946.853s cpu time, 8.761s GC time, factor 5.73)
19:55:42 Finished Syntax_Independent_Logic (0:02:56 elapsed time, 0:16:10 cpu time, factor 5.49)
19:55:42 Building Core_DOM (on lxcisa1/0) ...
19:56:01 Core_DOM: theory Core_DOM.Testing_Utils
19:56:01 Core_DOM: theory Core_DOM.Hiding_Type_Variables
19:56:01 Core_DOM: theory Core_DOM.Core_DOM_Basic_Datatypes
19:56:02 Core_DOM: theory Core_DOM.Ref
19:56:02 Core_DOM: theory Core_DOM.Heap_Error_Monad
19:56:02 Core_DOM: theory Core_DOM.ObjectPointer
19:56:02 Core_DOM: theory Core_DOM.BaseClass
19:56:03 Core_DOM: theory Core_DOM.NodePointer
19:56:03 Core_DOM: theory Core_DOM.ObjectClass
19:56:04 Core_DOM: theory Core_DOM.ElementPointer
19:56:05 Core_DOM: theory Core_DOM.NodeClass
19:56:05 Core_DOM: theory Core_DOM.CharacterDataPointer
19:56:06 Core_DOM: theory Core_DOM.BaseMonad
19:56:06 Core_DOM: theory Core_DOM.DocumentPointer
19:56:07 Core_DOM: theory Core_DOM.ShadowRootPointer
19:56:07 Core_DOM: theory Core_DOM.ObjectMonad
19:56:08 Core_DOM: theory Core_DOM.ElementClass
19:56:08 Core_DOM: theory Core_DOM.NodeMonad
19:56:10 Core_DOM: theory Core_DOM.CharacterDataClass
19:56:10 Core_DOM: theory Core_DOM.ElementMonad
19:56:11 Core_DOM: theory Core_DOM.DocumentClass
19:56:11 Core_DOM: theory Core_DOM.CharacterDataMonad
19:56:13 Core_DOM: theory Core_DOM.DocumentMonad
19:56:14 Core_DOM: theory Core_DOM.Core_DOM_Functions
19:56:35 Core_DOM: theory Core_DOM.Core_DOM_Heap_WF
19:56:56 Core_DOM: theory Core_DOM.Core_DOM
19:56:56 Core_DOM: theory Core_DOM.Core_DOM_BaseTest
19:57:04 Core_DOM: theory Core_DOM.Document_adoptNode
19:57:04 Core_DOM: theory Core_DOM.Document_getElementById
19:57:04 Core_DOM: theory Core_DOM.Node_insertBefore
19:57:04 Core_DOM: theory Core_DOM.Node_removeChild
19:57:07 Core_DOM: theory Core_DOM.Core_DOM_Tests
19:59:37 Preparing Core_DOM/document ...
19:59:51 Finished Core_DOM/document (0:00:14 elapsed time)
19:59:51 Preparing Core_DOM/outline ...
20:00:01 Finished Core_DOM/outline (0:00:09 elapsed time)
20:00:01 Timing Core_DOM (8 threads, 178.531s elapsed time, 977.066s cpu time, 59.811s GC time, factor 5.47)
20:00:01 Finished Core_DOM (0:03:53 elapsed time, 0:18:24 cpu time, factor 4.74)
20:00:02 Running CoCon (on lxcisa1/1) ...
20:00:03 CoCon: theory Fresh_Identifiers.Fresh
20:00:03 CoCon: theory Fresh_Identifiers.Fresh_String
20:00:04 CoCon: theory CoCon.Prelim
20:00:12 CoCon: theory CoCon.System_Specification
20:00:32 CoCon: theory CoCon.Automation_Setup
20:00:32 CoCon: theory CoCon.Safety_Properties
20:00:33 CoCon: theory CoCon.Decision_Intro
20:00:33 CoCon: theory CoCon.Discussion_Intro
20:00:33 CoCon: theory CoCon.Observation_Setup
20:00:33 CoCon: theory CoCon.Decision_Value_Setup
20:00:33 CoCon: theory CoCon.Paper_Intro
20:00:33 CoCon: theory CoCon.Review_Intro
20:00:33 CoCon: theory CoCon.Discussion_Value_Setup
20:00:33 CoCon: theory CoCon.Paper_Value_Setup
20:00:34 CoCon: theory CoCon.Review_Value_Setup
20:00:34 CoCon: theory CoCon.Reviewer_Assignment_Intro
20:00:34 CoCon: theory CoCon.Reviewer_Assignment_Value_Setup
20:00:34 CoCon: theory CoCon.Traceback_Properties
20:00:35 CoCon: theory CoCon.Discussion_NCPC
20:00:35 CoCon: theory CoCon.Decision_NCPC
20:00:35 CoCon: theory CoCon.Decision_NCPC_Aut
20:00:35 CoCon: theory CoCon.Paper_Aut
20:00:35 CoCon: theory CoCon.Paper_Aut_PC
20:00:36 CoCon: theory CoCon.Discussion_All
20:00:36 CoCon: theory CoCon.Review_RAut
20:00:36 CoCon: theory CoCon.Review_RAut_NCPC
20:00:36 CoCon: theory CoCon.Review_RAut_NCPC_PAut
20:00:36 CoCon: theory CoCon.Decision_All
20:00:37 CoCon: theory CoCon.Paper_All
20:00:37 CoCon: theory CoCon.Reviewer_Assignment_NCPC
20:00:37 CoCon: theory CoCon.Reviewer_Assignment_NCPC_Aut
20:00:38 CoCon: theory CoCon.Reviewer_Assignment_All
20:00:39 CoCon: theory CoCon.Review_All
20:01:05 CoCon: theory CoCon.All_BD_Security_Instances_for_CoCon
20:08:48 Preparing CoCon/document ...
20:08:59 Finished CoCon/document (0:00:10 elapsed time)
20:08:59 Preparing CoCon/outline ...
20:09:05 Finished CoCon/outline (0:00:05 elapsed time)
20:09:05 Timing CoCon (8 threads, 523.026s elapsed time, 3703.812s cpu time, 34.734s GC time, factor 7.08)
20:09:05 Finished CoCon (0:08:45 elapsed time, 1:01:48 cpu time, factor 7.06)
20:09:05 Running Automated_Stateful_Protocol_Verification (on lxcisa1/0) ...
20:09:08 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
20:09:08 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
20:09:08 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
20:09:08 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
20:09:08 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
20:09:09 Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
20:09:09 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
20:09:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
20:09:10 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
20:09:12 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
20:09:20 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
20:09:26 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
20:09:54 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
20:10:39 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
20:14:22 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
20:14:23 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
20:14:23 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
20:14:23 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
20:19:56 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
20:20:54 Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
20:21:25 Preparing Automated_Stateful_Protocol_Verification/document ...
20:22:02 Finished Automated_Stateful_Protocol_Verification/document (0:00:37 elapsed time)
20:22:02 Preparing Automated_Stateful_Protocol_Verification/outline ...
20:22:18 Finished Automated_Stateful_Protocol_Verification/outline (0:00:16 elapsed time)
20:22:18 Timing Automated_Stateful_Protocol_Verification (8 threads, 727.678s elapsed time, 2827.515s cpu time, 1028.254s GC time, factor 3.89)
20:22:18 Finished Automated_Stateful_Protocol_Verification (0:12:14 elapsed time, 0:47:30 cpu time, factor 3.88)
20:22:18 Building Berlekamp_Zassenhaus (on lxcisa1/1) ...
20:22:22 Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
20:22:22 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
20:22:22 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
20:22:22 Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
20:22:22 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
20:22:22 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
20:22:22 Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
20:22:22 Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
20:22:23 Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
20:22:23 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
20:22:23 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
20:22:23 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
20:22:23 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
20:22:23 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
20:22:23 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
20:22:23 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
20:22:23 Berlekamp_Zassenhaus: theory Matrix.Utility
20:22:24 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
20:22:24 Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
20:22:24 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
20:22:24 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
20:22:24 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
20:22:24 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
20:22:24 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
20:22:25 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
20:22:25 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
20:22:25 Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
20:22:26 Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
20:22:26 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
20:22:26 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
20:22:26 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
20:22:26 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
20:22:26 Berlekamp_Zassenhaus: theory Show.Show_Poly
20:22:26 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
20:22:27 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
20:22:27 Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
20:22:27 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
20:22:27 Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
20:22:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
20:22:27 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
20:22:27 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
20:22:28 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
20:22:28 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
20:22:28 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
20:22:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
20:22:29 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
20:22:29 Berlekamp_Zassenhaus: theory Word_Lib.More_Word
20:22:31 Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
20:22:31 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
20:22:31 Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:22:31 Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
20:22:33 Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
20:22:33 Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
20:22:33 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
20:22:34 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
20:22:34 Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
20:22:35 Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
20:22:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
20:22:41 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
20:22:43 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
20:22:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
20:22:48 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
20:22:48 Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
20:22:48 Berlekamp_Zassenhaus: theory Native_Word.Uint32
20:22:49 Berlekamp_Zassenhaus: theory Native_Word.Uint64
20:22:51 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
20:22:55 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
20:22:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
20:22:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
20:22:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
20:22:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
20:22:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
20:22:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
20:23:00 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
20:23:01 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
20:23:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
20:23:05 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
20:23:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
20:23:06 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
20:23:10 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
20:23:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
20:23:12 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
20:23:13 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorization_External_Interface
20:25:01 Preparing Berlekamp_Zassenhaus/document ...
20:25:22 Finished Berlekamp_Zassenhaus/document (0:00:21 elapsed time)
20:25:22 Preparing Berlekamp_Zassenhaus/outline ...
20:25:32 Finished Berlekamp_Zassenhaus/outline (0:00:09 elapsed time)
20:25:32 Timing Berlekamp_Zassenhaus (8 threads, 129.284s elapsed time, 760.321s cpu time, 20.934s GC time, factor 5.88)
20:25:32 Finished Berlekamp_Zassenhaus (0:02:39 elapsed time, 0:13:47 cpu time, factor 5.19)
20:25:32 Building Refine_Imperative_HOL (on lxcisa1/0) ...
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.User_Smashing
20:25:35 Refine_Imperative_HOL: theory Isar_Ref.Base
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.PO_Normalizer
20:25:35 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Misc
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Add
20:25:35 Refine_Imperative_HOL: theory List-Index.List_Index
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Concl_Pres_Clarification
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Named_Theorems_Rev
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Structured_Apply
20:25:35 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Mono_Prover
20:25:35 Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Refine_Aux
20:25:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Misc
20:25:37 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Term_Synth
20:25:38 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_IICF
20:25:38 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Setup
20:25:38 Refine_Imperative_HOL: theory HOL-Library.Rewrite
20:25:38 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Tool
20:25:38 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Id_Op
20:25:38 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Userguides
20:25:38 Refine_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
20:25:39 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Basic
20:25:40 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Constraints
20:25:40 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Monadify
20:25:41 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Frame
20:25:41 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Rules
20:25:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
20:25:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Definition
20:25:45 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Translate
20:25:47 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Intf_Util
20:25:49 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Tool
20:25:50 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
20:25:53 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Foreach
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Improper
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Map
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Matrix
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Multiset
20:25:55 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Set
20:25:56 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Map
20:25:56 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_Mset
20:25:56 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Bag
20:25:56 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_MsetO
20:25:56 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_SetO
20:25:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array
20:25:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_List
20:25:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_HOL_List
20:25:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_MS_Array_List
20:25:57 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heap
20:25:58 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Sepl_Binding
20:25:59 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
20:25:59 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
20:25:59 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heap
20:26:00 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_Matrix
20:26:01 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
20:26:18 Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF
20:26:19 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_General_Util
20:26:20 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
20:26:20 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Reference
20:27:04 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc
20:27:04 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph
20:27:04 Refine_Imperative_HOL: theory HOL-Library.Omega_Words_Fun
20:27:04 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight
20:27:04 Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph
20:27:04 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
20:27:04 Refine_Imperative_HOL: theory CAVA_Automata.Digraph_Basic
20:27:05 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec
20:27:06 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph
20:27:07 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra
20:27:09 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA
20:27:10 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap
20:27:13 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl
20:27:13 Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS
20:27:16 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
20:27:56 Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator
20:28:02 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype
20:28:05 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
20:28:07 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS
20:28:07 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS
20:28:07 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests
20:28:23 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark
20:28:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark
20:28:36 Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples
20:29:27 Preparing Refine_Imperative_HOL/document ...
20:29:39 Finished Refine_Imperative_HOL/document (0:00:12 elapsed time)
20:29:39 Preparing Refine_Imperative_HOL/outline ...
20:29:47 Finished Refine_Imperative_HOL/outline (0:00:07 elapsed time)
20:29:48 Timing Refine_Imperative_HOL (8 threads, 208.191s elapsed time, 564.230s cpu time, 22.772s GC time, factor 2.71)
20:29:48 Finished Refine_Imperative_HOL (0:03:53 elapsed time, 0:10:19 cpu time, factor 2.66)
20:29:48 Building LEM (on lxcisa1/1) ...
20:29:49 LEM: theory LEM.Lem_bool
20:29:49 LEM: theory HOL-Library.Cancellation
20:29:49 LEM: theory HOL-Library.FuncSet
20:29:49 LEM: theory HOL-Combinatorics.Transposition
20:29:49 LEM: theory HOL-Library.Phantom_Type
20:29:49 LEM: theory Word_Lib.Even_More_List
20:29:49 LEM: theory HOL-Library.While_Combinator
20:29:49 LEM: theory HOL-Library.Sublist
20:29:50 LEM: theory LEM.Lem_basic_classes
20:29:50 LEM: theory Word_Lib.More_Bit_Ring
20:29:51 LEM: theory HOL-Library.Disjoint_Sets
20:29:51 LEM: theory HOL-Library.Multiset
20:29:51 LEM: theory HOL-Library.Cardinality
20:29:52 LEM: theory HOL-Library.Numeral_Type
20:29:53 LEM: theory HOL-Library.Type_Length
20:29:54 LEM: theory HOL-Library.Word
20:29:54 LEM: theory Word_Lib.More_Arithmetic
20:29:56 LEM: theory LEM.Lem_function
20:29:56 LEM: theory LEM.Lem_tuple
20:29:56 LEM: theory LEM.Lem_maybe
20:29:57 LEM: theory HOL-Combinatorics.Permutations
20:29:58 LEM: theory HOL-Combinatorics.List_Permutation
20:29:59 LEM: theory LEM.LemExtraDefs
20:30:04 LEM: theory Word_Lib.Bit_Comprehension
20:30:04 LEM: theory Word_Lib.Legacy_Aliases
20:30:04 LEM: theory Word_Lib.More_Divides
20:30:04 LEM: theory LEM.Lem_num
20:30:04 LEM: theory Word_Lib.More_Word
20:30:06 LEM: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:30:06 LEM: theory Word_Lib.Least_significant_bit
20:30:08 LEM: theory Word_Lib.Aligned
20:30:08 LEM: theory Word_Lib.Singleton_Bit_Shifts
20:30:08 LEM: theory Word_Lib.Most_significant_bit
20:30:08 LEM: theory Word_Lib.Generic_set_bit
20:30:09 LEM: theory Word_Lib.Bits_Int
20:30:12 LEM: theory LEM.Lem_set_helpers
20:30:13 LEM: theory Word_Lib.Typedef_Morphisms
20:30:14 LEM: theory Word_Lib.Reversed_Bit_Lists
20:30:17 LEM: theory LEM.Lem
20:30:17 LEM: theory LEM.Lem_assert_extra
20:30:17 LEM: theory LEM.Lem_function_extra
20:30:18 LEM: theory LEM.Lem_list
20:30:18 LEM: theory LEM.Lem_maybe_extra
20:30:22 LEM: theory LEM.Lem_either
20:30:22 LEM: theory LEM.Lem_list_extra
20:30:22 LEM: theory LEM.Lem_string
20:30:22 LEM: theory LEM.Lem_word
20:30:22 LEM: theory LEM.Lem_set
20:30:22 LEM: theory LEM.Lem_sorting
20:30:23 LEM: theory LEM.Lem_num_extra
20:30:23 LEM: theory LEM.Lem_show
20:30:23 LEM: theory LEM.Lem_map
20:30:23 LEM: theory LEM.Lem_relation
20:30:23 LEM: theory LEM.Lem_set_extra
20:30:23 LEM: theory LEM.Lem_map_extra
20:30:24 LEM: theory LEM.Lem_machine_word
20:30:24 LEM: theory LEM.Lem_string_extra
20:30:25 LEM: theory LEM.Lem_show_extra
20:30:28 LEM: theory LEM.Lem_pervasives
20:30:30 LEM: theory LEM.Lem_pervasives_extra
20:30:52 Timing LEM (8 threads, 44.883s elapsed time, 283.408s cpu time, 9.174s GC time, factor 6.31)
20:30:52 Finished LEM (0:01:01 elapsed time, 0:05:20 cpu time, factor 5.17)
20:30:52 Building Word_Lib (on lxcisa1/0) ...
20:30:53 Word_Lib: theory Word_Lib.Enumeration
20:30:53 Word_Lib: theory Word_Lib.Even_More_List
20:30:53 Word_Lib: theory Word_Lib.More_Bit_Ring
20:30:53 Word_Lib: theory Word_Lib.More_Misc
20:30:53 Word_Lib: theory HOL-Library.Phantom_Type
20:30:53 Word_Lib: theory HOL-Library.Sublist
20:30:54 Word_Lib: theory HOL-Library.Cardinality
20:30:55 Word_Lib: theory HOL-Library.Numeral_Type
20:30:56 Word_Lib: theory Word_Lib.More_Sublist
20:30:56 Word_Lib: theory HOL-Library.Type_Length
20:30:57 Word_Lib: theory HOL-Library.Word
20:30:57 Word_Lib: theory Word_Lib.More_Arithmetic
20:31:06 Word_Lib: theory Word_Lib.Legacy_Aliases
20:31:06 Word_Lib: theory Word_Lib.More_Divides
20:31:06 Word_Lib: theory Word_Lib.More_Word
20:31:08 Word_Lib: theory Word_Lib.Strict_part_mono
20:31:13 Word_Lib: theory Word_Lib.Bit_Comprehension
20:31:13 Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:31:13 Word_Lib: theory Word_Lib.Least_significant_bit
20:31:13 Word_Lib: theory HOL-Library.Signed_Division
20:31:14 Word_Lib: theory Word_Lib.Signed_Division_Word
20:31:14 Word_Lib: theory Word_Lib.Aligned
20:31:14 Word_Lib: theory Word_Lib.Most_significant_bit
20:31:15 Word_Lib: theory Word_Lib.Generic_set_bit
20:31:15 Word_Lib: theory Word_Lib.Next_and_Prev
20:31:16 Word_Lib: theory Word_Lib.Bits_Int
20:31:20 Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
20:31:20 Word_Lib: theory Word_Lib.Many_More
20:31:20 Word_Lib: theory Word_Lib.Typedef_Morphisms
20:31:22 Word_Lib: theory HOL-Eisbach.Eisbach
20:31:22 Word_Lib: theory Word_Lib.Bit_Comprehension_Int
20:31:22 Word_Lib: theory Word_Lib.Hex_Words
20:31:22 Word_Lib: theory Word_Lib.Signed_Words
20:31:22 Word_Lib: theory Word_Lib.Syntax_Bundles
20:31:22 Word_Lib: theory Word_Lib.Type_Syntax
20:31:22 Word_Lib: theory Word_Lib.Word_Syntax
20:31:22 Word_Lib: theory Word_Lib.Enumeration_Word
20:31:22 Word_Lib: theory Word_Lib.Sgn_Abs
20:31:22 Word_Lib: theory Word_Lib.Rsplit
20:31:22 Word_Lib: theory Word_Lib.Reversed_Bit_Lists
20:31:22 Word_Lib: theory Word_Lib.Norm_Words
20:31:22 Word_Lib: theory Word_Lib.Word_Names
20:31:22 Word_Lib: theory Word_Lib.Word_16
20:31:23 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
20:31:23 Word_Lib: theory Word_Lib.Word_EqI
20:31:25 Word_Lib: theory Word_Lib.Bitwise
20:31:26 Word_Lib: theory Word_Lib.Bitwise_Signed
20:31:26 Word_Lib: theory Word_Lib.Boolean_Inequalities
20:31:29 Word_Lib: theory Word_Lib.Word_Lemmas
20:31:31 Word_Lib: theory Word_Lib.Word_8
20:31:31 Word_Lib: theory Word_Lib.More_Word_Operations
20:31:32 Word_Lib: theory Word_Lib.Word_32
20:31:32 Word_Lib: theory Word_Lib.Word_64
20:31:33 Word_Lib: theory Word_Lib.Machine_Word_64_Basics
20:31:33 Word_Lib: theory Word_Lib.Machine_Word_64
20:31:34 Word_Lib: theory Word_Lib.Machine_Word_32_Basics
20:31:34 Word_Lib: theory Word_Lib.Word_Lib_Sumo
20:31:34 Word_Lib: theory Word_Lib.Machine_Word_32
20:31:36 Word_Lib: theory Word_Lib.Guide
20:31:39 Word_Lib: theory Word_Lib.Examples
20:31:52 Preparing Word_Lib/document ...
20:32:00 Finished Word_Lib/document (0:00:07 elapsed time)
20:32:00 Preparing Word_Lib/outline ...
20:32:05 Finished Word_Lib/outline (0:00:05 elapsed time)
20:32:06 Timing Word_Lib (8 threads, 47.356s elapsed time, 264.625s cpu time, 6.776s GC time, factor 5.59)
20:32:06 Finished Word_Lib (0:00:58 elapsed time, 0:04:48 cpu time, factor 4.90)
20:32:06 Building CakeML (on lxcisa1/1) ...
20:32:08 CakeML: theory CakeML.Doc_Generated
20:32:08 CakeML: theory CakeML.Doc_Proofs
20:32:08 CakeML: theory Deriving.Derive_Manager
20:32:08 CakeML: theory HOL-Eisbach.Eisbach
20:32:08 CakeML: theory Deriving.Generator_Aux
20:32:08 CakeML: theory HOL-Library.Case_Converter
20:32:08 CakeML: theory HOL-Library.Complete_Partial_Order2
20:32:08 CakeML: theory HOL-Library.Datatype_Records
20:32:08 CakeML: theory HOL-Library.Infinite_Set
20:32:08 CakeML: theory HOL-Library.Nat_Bijection
20:32:08 CakeML: theory HOL-Library.Old_Datatype
20:32:08 CakeML: theory Word_Lib.Signed_Words
20:32:09 CakeML: theory HOL-Library.Simps_Case_Conv
20:32:09 CakeML: theory Word_Lib.Type_Syntax
20:32:09 CakeML: theory Word_Lib.Word_Syntax
20:32:09 CakeML: theory Word_Lib.Word_Names
20:32:09 CakeML: theory HOL-Library.Signed_Division
20:32:09 CakeML: theory HOL-Library.Lattice_Algebras
20:32:09 CakeML: theory HOL-Library.Log_Nat
20:32:09 CakeML: theory Show.Show
20:32:10 CakeML: theory HOL-Library.Countable
20:32:10 CakeML: theory HOL-Eisbach.Eisbach_Tools
20:32:10 CakeML: theory Word_Lib.Enumeration
20:32:10 CakeML: theory Word_Lib.Many_More
20:32:10 CakeML: theory Word_Lib.Rsplit
20:32:10 CakeML: theory Word_Lib.Word_EqI
20:32:11 CakeML: theory Word_Lib.Enumeration_Word
20:32:11 CakeML: theory Word_Lib.More_Misc
20:32:11 CakeML: theory CakeML.Namespace
20:32:11 CakeML: theory Word_Lib.Signed_Division_Word
20:32:12 CakeML: theory Show.Show_Instances
20:32:12 CakeML: theory CakeML.Tokens
20:32:12 CakeML: theory HOL-Library.Countable_Set
20:32:13 CakeML: theory HOL-Library.Countable_Complete_Lattices
20:32:13 CakeML: theory Word_Lib.Boolean_Inequalities
20:32:15 CakeML: theory HOL-Library.Order_Continuity
20:32:15 CakeML: theory Word_Lib.Word_Lemmas
20:32:16 CakeML: theory CakeML.NamespaceAuxiliary
20:32:16 CakeML: theory HOL-Library.Extended_Nat
20:32:16 CakeML: theory HOL-Library.Float
20:32:17 CakeML: theory Coinductive.Coinductive_Nat
20:32:18 CakeML: theory Word_Lib.More_Word_Operations
20:32:18 CakeML: theory Coinductive.Coinductive_List
20:32:19 CakeML: theory IEEE_Floating_Point.IEEE
20:32:19 CakeML: theory Word_Lib.Word_64
20:32:22 CakeML: theory IEEE_Floating_Point.FP64
20:32:26 CakeML: theory CakeML.Lib
20:32:29 CakeML: theory CakeML.LibAuxiliary
20:32:30 CakeML: theory CakeML.Ffi
20:32:30 CakeML: theory CakeML.FpSem
20:32:34 CakeML: theory CakeML.Ast
20:32:38 CakeML: theory CakeML.SimpleIO
20:33:05 CakeML: theory CakeML.CakeML_Compiler
20:33:05 CakeML: theory CakeML.AstAuxiliary
20:33:05 CakeML: theory CakeML.SemanticPrimitives
20:33:36 CakeML: theory CakeML.CakeML_Quickcheck
20:33:36 CakeML: theory CakeML.SemanticPrimitivesAuxiliary
20:33:36 CakeML: theory CakeML.Evaluate
20:33:36 CakeML: theory CakeML.SmallStep
20:33:36 CakeML: theory CakeML.TypeSystem
20:33:41 CakeML: theory CakeML.BigStep
20:33:42 CakeML: theory CakeML.PrimTypes
20:33:47 CakeML: theory CakeML.BigSmallInvariants
20:33:47 CakeML: theory CakeML.Semantic_Extras
20:33:58 CakeML: theory CakeML.TypeSystemAuxiliary
20:34:01 CakeML: theory CakeML.Big_Step_Determ
20:34:01 CakeML: theory CakeML.Big_Step_Total
20:34:01 CakeML: theory CakeML.Big_Step_Clocked
20:34:01 CakeML: theory CakeML.Big_Step_Unclocked
20:34:02 CakeML: theory CakeML.Evaluate_Termination
20:34:02 CakeML: theory CakeML.Matching
20:34:03 CakeML: theory CakeML.Evaluate_Clock
20:34:03 CakeML: theory CakeML.Big_Step_Fun_Equiv
20:34:03 CakeML: theory CakeML.Evaluate_Single
20:34:06 CakeML: theory CakeML.Big_Step_Unclocked_Single
20:34:13 CakeML: theory CakeML.CakeML_Code
20:35:16 CakeML: theory CakeML.Compiler_Test
20:35:24 CakeML: theory CakeML.Code_Test_Haskell
20:36:13 Preparing CakeML/document ...
20:36:19 Finished CakeML/document (0:00:05 elapsed time)
20:36:19 Preparing CakeML/outline ...
20:36:23 Finished CakeML/outline (0:00:04 elapsed time)
20:36:24 Timing CakeML (8 threads, 215.439s elapsed time, 1088.451s cpu time, 87.732s GC time, factor 5.05)
20:36:24 Finished CakeML (0:04:05 elapsed time, 0:19:15 cpu time, factor 4.71)
20:36:24 Running X86_Semantics (on lxcisa1/0) ...
20:36:25 X86_Semantics: theory HOL-Eisbach.Eisbach
20:36:25 X86_Semantics: theory Word_Lib.Even_More_List
20:36:25 X86_Semantics: theory HOL-Library.Phantom_Type
20:36:25 X86_Semantics: theory Word_Lib.More_Bit_Ring
20:36:25 X86_Semantics: theory HOL-Library.Sublist
20:36:27 X86_Semantics: theory HOL-Library.Cardinality
20:36:27 X86_Semantics: theory HOL-Library.Numeral_Type
20:36:28 X86_Semantics: theory HOL-Library.Type_Length
20:36:29 X86_Semantics: theory Word_Lib.More_Arithmetic
20:36:29 X86_Semantics: theory HOL-Library.Word
20:36:38 X86_Semantics: theory Word_Lib.Bit_Comprehension
20:36:38 X86_Semantics: theory Word_Lib.Legacy_Aliases
20:36:38 X86_Semantics: theory Word_Lib.More_Divides
20:36:38 X86_Semantics: theory Word_Lib.Syntax_Bundles
20:36:39 X86_Semantics: theory Word_Lib.More_Word
20:36:40 X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:36:40 X86_Semantics: theory Word_Lib.Least_significant_bit
20:36:42 X86_Semantics: theory Word_Lib.Aligned
20:36:42 X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
20:36:42 X86_Semantics: theory Word_Lib.Most_significant_bit
20:36:43 X86_Semantics: theory Word_Lib.Generic_set_bit
20:36:44 X86_Semantics: theory Word_Lib.Bits_Int
20:36:47 X86_Semantics: theory Word_Lib.Typedef_Morphisms
20:36:48 X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
20:36:50 X86_Semantics: theory Word_Lib.Bitwise
20:36:51 X86_Semantics: theory X86_Semantics.BitByte
20:36:51 X86_Semantics: theory X86_Semantics.Memory
20:36:52 X86_Semantics: theory X86_Semantics.State
20:36:59 X86_Semantics: theory X86_Semantics.StateCleanUp
20:36:59 X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
20:37:10 X86_Semantics: theory X86_Semantics.SymbolicExecution
20:37:10 X86_Semantics: theory X86_Semantics.X86_Parse
20:37:12 X86_Semantics: theory X86_Semantics.Examples
20:37:12 X86_Semantics: theory X86_Semantics.Example_WC
20:48:21 Preparing X86_Semantics/document ...
20:48:29 Finished X86_Semantics/document (0:00:07 elapsed time)
20:48:29 Preparing X86_Semantics/outline ...
20:48:35 Finished X86_Semantics/outline (0:00:06 elapsed time)
20:48:35 Timing X86_Semantics (8 threads, 714.360s elapsed time, 904.061s cpu time, 11.359s GC time, factor 1.27)
20:48:35 Finished X86_Semantics (0:11:56 elapsed time, 0:15:08 cpu time, factor 1.27)
20:48:35 Running AutoCorres2 (on lxcisa1/1) ...
20:48:37 AutoCorres2: theory AutoCorres2.MkTermAntiquote
20:48:37 AutoCorres2: theory AutoCorres2.ML_Fun_Cache
20:48:37 AutoCorres2: theory AutoCorres2.TermPatternAntiquote
20:48:37 AutoCorres2: theory HOL-Eisbach.Eisbach
20:48:37 AutoCorres2: theory AutoCorres2.Apply_Trace
20:48:37 AutoCorres2: theory AutoCorres2.Introduction_AutoCorres2
20:48:37 AutoCorres2: theory AutoCorres2.ML_Infer_Instantiate
20:48:37 AutoCorres2: theory AutoCorres2.ML_Record_Antiquotation
20:48:37 AutoCorres2: theory AutoCorres2.MapExtra
20:48:37 AutoCorres2: theory AutoCorres2.Misc_Antiquotation
20:48:37 AutoCorres2: theory AutoCorres2.MkTermAntiquote_Tests
20:48:37 AutoCorres2: theory AutoCorres2.Named_Rules
20:48:38 AutoCorres2: theory AutoCorres2.Padding
20:48:38 AutoCorres2: theory AutoCorres2.Option_Scanner
20:48:38 AutoCorres2: theory AutoCorres2.Print_Annotated
20:48:38 AutoCorres2: theory AutoCorres2.StaticFun
20:48:38 AutoCorres2: theory AutoCorres2.Apply_Trace_Cmd
20:48:38 AutoCorres2: theory AutoCorres2.AutoCorres_Utils
20:48:38 AutoCorres2: theory AutoCorres2.Subgoal_Methods
20:48:39 AutoCorres2: theory AutoCorres2.Subgoals
20:48:39 AutoCorres2: theory AutoCorres2.Target_Architecture
20:48:39 AutoCorres2: theory AutoCorres2.TermPatternAntiquote_Tests
20:48:39 AutoCorres2: theory AutoCorres2.MapExtraTrans
20:48:39 AutoCorres2: theory AutoCorres2.Tuple_Tools
20:48:39 AutoCorres2: theory HOL-Library.Adhoc_Overloading
20:48:39 AutoCorres2: theory HOL-Library.Code_Abstract_Nat
20:48:39 AutoCorres2: theory HOL-Library.Complete_Partial_Order2
20:48:39 AutoCorres2: theory HOL-Library.Monad_Syntax
20:48:39 AutoCorres2: theory HOL-Library.Code_Binary_Nat
20:48:39 AutoCorres2: theory HOL-Eisbach.Eisbach_Tools
20:48:40 AutoCorres2: theory AutoCorres2.Tagging
20:48:40 AutoCorres2: theory AutoCorres2.Less_Monad_Syntax
20:48:40 AutoCorres2: theory AutoCorres2.Cong_Tactic
20:48:40 AutoCorres2: theory AutoCorres2.Rule_By_Method
20:48:40 AutoCorres2: theory HOL-Library.Phantom_Type
20:48:40 AutoCorres2: theory HOL-Library.Signed_Division
20:48:40 AutoCorres2: theory AutoCorres2.Match_Cterm
20:48:41 AutoCorres2: theory AutoCorres2.Simp_Trace
20:48:41 AutoCorres2: theory AutoCorres2.Basic_Runs_To_VCG
20:48:41 AutoCorres2: theory AutoCorres2.Eisbach_Methods
20:48:41 AutoCorres2: theory HOL-Library.Sublist
20:48:41 AutoCorres2: theory AutoCorres2.PrettyProgs
20:48:41 AutoCorres2: theory HOL-Library.Cardinality
20:48:42 AutoCorres2: theory AutoCorres2.IndirectCalls
20:48:42 AutoCorres2: theory Word_Lib.Enumeration
20:48:43 AutoCorres2: theory Word_Lib.Even_More_List
20:48:43 AutoCorres2: theory Word_Lib.More_Bit_Ring
20:48:43 AutoCorres2: theory Word_Lib.More_Misc
20:48:43 AutoCorres2: theory HOL-Library.Numeral_Type
20:48:43 AutoCorres2: theory AutoCorres2.Runs_To_VCG
20:48:44 AutoCorres2: theory AutoCorres2.Arrays
20:48:44 AutoCorres2: theory HOL-Library.Type_Length
20:48:44 AutoCorres2: theory HOL-Library.Prefix_Order
20:48:44 AutoCorres2: theory Word_Lib.More_Sublist
20:48:45 AutoCorres2: theory AutoCorres2.Mutual_CCPO_Recursion
20:48:45 AutoCorres2: theory AutoCorres2.Spec_Monad
20:48:45 AutoCorres2: theory HOL-Library.Word
20:48:45 AutoCorres2: theory Word_Lib.More_Arithmetic
20:48:52 AutoCorres2: theory AutoCorres2.Synthesize
20:48:55 AutoCorres2: theory Word_Lib.Bit_Comprehension
20:48:55 AutoCorres2: theory Word_Lib.Hex_Words
20:48:55 AutoCorres2: theory Word_Lib.Legacy_Aliases
20:48:55 AutoCorres2: theory Word_Lib.More_Divides
20:48:55 AutoCorres2: theory AutoCorres2.Reaches
20:48:55 AutoCorres2: theory Word_Lib.Signed_Words
20:48:55 AutoCorres2: theory Word_Lib.Syntax_Bundles
20:48:55 AutoCorres2: theory Word_Lib.Type_Syntax
20:48:55 AutoCorres2: theory Word_Lib.Word_Syntax
20:48:55 AutoCorres2: theory Word_Lib.Norm_Words
20:48:56 AutoCorres2: theory Word_Lib.Word_Names
20:48:56 AutoCorres2: theory Word_Lib.Signed_Division_Word
20:48:56 AutoCorres2: theory Word_Lib.More_Word
20:48:57 AutoCorres2: theory Word_Lib.Bit_Comprehension_Int
20:48:58 AutoCorres2: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:48:58 AutoCorres2: theory Word_Lib.Enumeration_Word
20:48:58 AutoCorres2: theory Word_Lib.Least_significant_bit
20:48:58 AutoCorres2: theory Word_Lib.Many_More
20:48:58 AutoCorres2: theory Word_Lib.Strict_part_mono
20:48:58 AutoCorres2: theory Word_Lib.Word_16
20:48:59 AutoCorres2: theory AutoCorres2.Distinct_Prop
20:48:59 AutoCorres2: theory AutoCorres2.Lens
20:48:59 AutoCorres2: theory Word_Lib.Aligned
20:48:59 AutoCorres2: theory Word_Lib.Singleton_Bit_Shifts
20:48:59 AutoCorres2: theory Word_Lib.Most_significant_bit
20:48:59 AutoCorres2: theory Word_Lib.Generic_set_bit
20:48:59 AutoCorres2: theory Word_Lib.Sgn_Abs
20:49:00 AutoCorres2: theory Word_Lib.Next_and_Prev
20:49:00 AutoCorres2: theory Word_Lib.Word_EqI
20:49:00 AutoCorres2: theory Word_Lib.Bits_Int
20:49:02 AutoCorres2: theory Word_Lib.Boolean_Inequalities
20:49:04 AutoCorres2: theory Word_Lib.Rsplit
20:49:04 AutoCorres2: theory Word_Lib.Typedef_Morphisms
20:49:05 AutoCorres2: theory Word_Lib.Reversed_Bit_Lists
20:49:06 AutoCorres2: theory Word_Lib.Word_Lemmas
20:49:08 AutoCorres2: theory Word_Lib.Bitwise
20:49:08 AutoCorres2: theory Word_Lib.Word_8
20:49:08 AutoCorres2: theory Word_Lib.More_Word_Operations
20:49:09 AutoCorres2: theory Word_Lib.Bitwise_Signed
20:49:10 AutoCorres2: theory AutoCorres2.Word_Lemmas_Internal
20:49:10 AutoCorres2: theory Word_Lib.Word_32
20:49:10 AutoCorres2: theory Word_Lib.Word_64
20:49:11 AutoCorres2: theory Word_Lib.Machine_Word_64_Basics
20:49:11 AutoCorres2: theory Word_Lib.Machine_Word_64
20:49:11 AutoCorres2: theory Word_Lib.Machine_Word_32_Basics
20:49:11 AutoCorres2: theory Word_Lib.Word_Lib_Sumo
20:49:11 AutoCorres2: theory Word_Lib.Machine_Word_32
20:49:14 AutoCorres2: theory AutoCorres2.More_Lib
20:49:14 AutoCorres2: theory AutoCorres2.Word_Lemmas_32_Internal
20:49:14 AutoCorres2: theory AutoCorres2.Word_Lemmas_64_Internal
20:49:14 AutoCorres2: theory AutoCorres2.WordSetup
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type_ARM
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type_ARM64
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type_ARM_HYP
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type_RISCV64
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type_X64
20:49:15 AutoCorres2: theory AutoCorres2.Addr_Type
20:49:16 AutoCorres2: theory AutoCorres2.CTypesBase
20:49:17 AutoCorres2: theory AutoCorres2.NatBitwise
20:49:17 AutoCorres2: theory AutoCorres2.Reader_Monad
20:49:18 AutoCorres2: theory AutoCorres2.Option_MonadND
20:49:19 AutoCorres2: theory AutoCorres2.CTypesDefs
20:49:33 AutoCorres2: theory AutoCorres2.CTypes
20:49:36 AutoCorres2: theory AutoCorres2.HeapRawState
20:49:37 AutoCorres2: theory AutoCorres2.Vanilla32_Preliminaries
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM64
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_RISCV64
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_X64
20:49:37 AutoCorres2: theory AutoCorres2.Word_Mem_Encoding
20:49:38 AutoCorres2: theory AutoCorres2.Vanilla32
20:49:39 AutoCorres2: theory AutoCorres2.CompoundCTypes
20:49:44 AutoCorres2: theory AutoCorres2.ArraysMemInstance
20:49:46 AutoCorres2: theory AutoCorres2.ArchArraysMemInstance
20:49:48 AutoCorres2: theory AutoCorres2.TypHeap
20:49:56 AutoCorres2: theory AutoCorres2.Separation_UMM
20:49:57 AutoCorres2: theory AutoCorres2.SepCode
20:49:59 AutoCorres2: theory AutoCorres2.SepInv
20:50:00 AutoCorres2: theory AutoCorres2.SepTactic
20:50:01 AutoCorres2: theory AutoCorres2.SepFrame
20:50:02 AutoCorres2: theory AutoCorres2.StructSupport
20:50:04 AutoCorres2: theory AutoCorres2.ArrayAssertion
20:50:04 AutoCorres2: theory AutoCorres2.CProof
20:50:12 AutoCorres2: theory AutoCorres2.CLanguage
20:50:12 AutoCorres2: theory AutoCorres2.Padding_Equivalence
20:50:12 AutoCorres2: theory AutoCorres2.PackedTypes
20:50:19 AutoCorres2: theory AutoCorres2.ModifiesProofs
20:50:22 AutoCorres2: theory AutoCorres2.UMM
20:50:29 AutoCorres2: theory AutoCorres2.CLocals
20:50:32 AutoCorres2: theory AutoCorres2.CTranslationSetup
20:50:56 AutoCorres2: theory AutoCorres2.Array_Selectors
20:50:56 AutoCorres2: theory AutoCorres2.CTranslation
20:50:57 AutoCorres2: theory AutoCorres2.CTranslationInfrastructure
20:50:57 AutoCorres2: theory AutoCorres2.TypHeapLib
20:50:58 AutoCorres2: theory AutoCorres2.AbstractArrays
20:50:58 AutoCorres2: theory AutoCorres2.LemmaBucket_C
20:50:58 AutoCorres2: theory AutoCorres2.AutoCorres_Base
20:51:02 AutoCorres2: theory AutoCorres2.SimplBucket
20:51:02 AutoCorres2: theory AutoCorres2.TypHeapSimple
20:51:02 AutoCorres2: theory AutoCorres2.AutoCorresSimpset
20:51:02 AutoCorres2: theory AutoCorres2.CCorresE
20:51:03 AutoCorres2: theory AutoCorres2.CorresXF
20:51:04 AutoCorres2: theory AutoCorres2.L1Defs
20:51:07 AutoCorres2: theory AutoCorres2.L1Peephole
20:51:07 AutoCorres2: theory AutoCorres2.L1Valid
20:51:07 AutoCorres2: theory AutoCorres2.ExceptionRewrite
20:51:07 AutoCorres2: theory AutoCorres2.SimplConv
20:51:08 AutoCorres2: theory AutoCorres2.L2Defs
20:51:11 AutoCorres2: theory AutoCorres2.Split_Heap
20:51:15 AutoCorres2: theory AutoCorres2.L2ExceptionRewrite
20:51:15 AutoCorres2: theory AutoCorres2.L2Peephole
20:51:15 AutoCorres2: theory AutoCorres2.LocalVarExtract
20:51:15 AutoCorres2: theory AutoCorres2.Stack_Typing
20:51:16 AutoCorres2: theory AutoCorres2.WordAbstract
20:51:18 AutoCorres2: theory AutoCorres2.Refines_Spec
20:51:18 AutoCorres2: theory AutoCorres2.In_Out_Parameters
20:51:19 AutoCorres2: theory AutoCorres2.WordPolish
20:51:34 AutoCorres2: theory AutoCorres2.HeapLift
20:51:35 AutoCorres2: theory AutoCorres2.TypeStrengthen
20:51:55 AutoCorres2: theory AutoCorres2.Polish
20:51:55 AutoCorres2: theory AutoCorres2.Runs_To_VCG_StackPointer
20:52:03 AutoCorres2: theory AutoCorres2.AutoCorres
20:52:27 AutoCorres2: theory AutoCorres2.AutoCorresInfrastructure
20:52:27 AutoCorres2: theory AutoCorres2.Chapter1_MinMax
20:52:27 AutoCorres2: theory AutoCorres2.Chapter2_HoareHeap
20:52:28 AutoCorres2: theory AutoCorres2.Chapter3_HoareHeap
20:52:28 AutoCorres2: theory AutoCorres2.In_Out_Parameters_Ex
20:52:28 AutoCorres2: theory AutoCorres2.fnptr
20:52:31 AutoCorres2: theory AutoCorres2.open_struct
20:52:33 AutoCorres2: theory AutoCorres2.pointers_to_locals
20:52:36 AutoCorres2: theory AutoCorres2.union_ac
20:55:59 AutoCorres2: theory AutoCorres2.AutoCorres_Documentation
20:56:37 Preparing AutoCorres2/document ...
20:58:03 Finished AutoCorres2/document (0:01:25 elapsed time)
20:58:03 Preparing AutoCorres2/outline ...
20:58:51 Finished AutoCorres2/outline (0:00:48 elapsed time)
20:58:52 Timing AutoCorres2 (8 threads, 465.197s elapsed time, 3176.943s cpu time, 101.966s GC time, factor 6.83)
20:58:52 Finished AutoCorres2 (0:07:50 elapsed time, 0:53:19 cpu time, factor 6.80)
20:58:52 Building Category3 (on lxcisa1/0) ...
20:58:54 Category3: theory Category3.Category
20:58:54 Category3: theory HOL-Cardinals.Order_Union
20:58:54 Category3: theory HOL-Cardinals.Order_Relation_More
20:58:54 Category3: theory HOL-Cardinals.Fun_More
20:58:54 Category3: theory HereditarilyFinite.HF
20:58:55 Category3: theory HOL-Cardinals.Wellorder_Extension
20:58:55 Category3: theory HOL-Cardinals.Wellfounded_More
20:58:55 Category3: theory HOL-Cardinals.Wellorder_Relation
20:58:55 Category3: theory Category3.ConcreteCategory
20:58:55 Category3: theory Category3.DiscreteCategory
20:58:55 Category3: theory Category3.EpiMonoIso
20:58:55 Category3: theory HOL-Cardinals.Wellorder_Embedding
20:58:56 Category3: theory HOL-Cardinals.Wellorder_Constructions
20:58:56 Category3: theory Category3.DualCategory
20:58:56 Category3: theory Category3.InitialTerminal
20:58:56 Category3: theory Category3.ProductCategory
20:58:57 Category3: theory HOL-Cardinals.Cardinal_Order_Relation
20:58:57 Category3: theory HOL-Cardinals.Ordinal_Arithmetic
20:58:58 Category3: theory Category3.FreeCategory
20:58:58 Category3: theory Category3.Functor
20:58:58 Category3: theory HOL-Cardinals.Cardinal_Arithmetic
20:58:58 Category3: theory HOL-Cardinals.Cardinals
20:58:59 Category3: theory ZFC_in_HOL.ZFC_Library
20:58:59 Category3: theory ZFC_in_HOL.ZFC_in_HOL
20:58:59 Category3: theory ZFC_in_HOL.ZFC_Cardinals
20:59:03 Category3: theory Category3.NaturalTransformation
20:59:03 Category3: theory Category3.Subcategory
20:59:06 Category3: theory Category3.SetCategory
20:59:07 Category3: theory Category3.BinaryFunctor
20:59:09 Category3: theory Category3.SetCat
20:59:13 Category3: theory Category3.FunctorCategory
20:59:26 Category3: theory Category3.Yoneda
20:59:51 Category3: theory Category3.Adjunction
21:00:45 Category3: theory Category3.EquivalenceOfCategories
21:00:45 Category3: theory Category3.Limit
21:02:25 Category3: theory Category3.CategoryWithPullbacks
21:02:25 Category3: theory Category3.ZFC_SetCat
21:02:39 Category3: theory Category3.ZFC_SetCat_Interp
21:02:40 Category3: theory Category3.CartesianCategory
21:03:00 Category3: theory Category3.CartesianClosedCategory
21:03:01 Category3: theory Category3.CategoryWithFiniteLimits
21:03:02 Category3: theory Category3.HF_SetCat
21:03:05 Category3: theory Category3.HF_SetCat_Interp
21:04:45 Preparing Category3/document ...
21:05:12 Finished Category3/document (0:00:26 elapsed time)
21:05:12 Preparing Category3/outline ...
21:05:22 Finished Category3/outline (0:00:09 elapsed time)
21:05:22 Timing Category3 (8 threads, 319.979s elapsed time, 1820.893s cpu time, 103.339s GC time, factor 5.69)
21:05:22 Finished Category3 (0:05:50 elapsed time, 0:31:30 cpu time, factor 5.39)
21:05:22 Building Complex_Bounded_Operators_Dependencies (on lxcisa1/1) ...
21:05:25 Complex_Bounded_Operators_Dependencies: theory Containers.List_Fusion
21:05:25 Complex_Bounded_Operators_Dependencies: theory Containers.Extend_Partial_Order
21:05:25 Complex_Bounded_Operators_Dependencies: theory Containers.Equal
21:05:25 Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator
21:05:25 Complex_Bounded_Operators_Dependencies: theory Deriving.Derive_Manager
21:05:25 Complex_Bounded_Operators_Dependencies: theory Deriving.Generator_Aux
21:05:25 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Fun_More
21:05:25 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Relation_More
21:05:25 Complex_Bounded_Operators_Dependencies: theory Containers.Closure_Set
21:05:25 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Union
21:05:25 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fraction_Field
21:05:25 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Adhoc_Overloading
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Char_ord
21:05:26 Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Generator
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Monad_Syntax
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Extension
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellfounded_More
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Abstract_Nat
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Relation
21:05:26 Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Auxiliary
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Int
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Nat
21:05:26 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Embedding
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Complemented_Lattices
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Numeral
21:05:27 Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Instances
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Constructions
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Congruence
21:05:27 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Misc
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Function_Algebras
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Library.IArray
21:05:27 Complex_Bounded_Operators_Dependencies: theory HOL-Library.More_List
21:05:28 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare
21:05:28 Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator_Generator
21:05:28 Complex_Bounded_Operators_Dependencies: theory Containers.Lexicographic_Order
21:05:28 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Normalized_Fraction
21:05:28 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Order_Relation
21:05:29 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Ordinal_Arithmetic
21:05:29 Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Generator
21:05:29 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Order
21:05:29 Complex_Bounded_Operators_Dependencies: theory Containers.Set_Linorder
21:05:29 Complex_Bounded_Operators_Dependencies: theory HOL-Library.RBT_Impl
21:05:30 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Generator
21:05:30 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Enum
21:05:30 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Arithmetic
21:05:30 Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Instances
21:05:30 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Eq
21:05:31 Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinals
21:05:31 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Lattice
21:05:31 Complex_Bounded_Operators_Dependencies: theory HOL-Library.Rewrite
21:05:31 Complex_Bounded_Operators_Dependencies: theory HOL-Types_To_Sets.Types_To_Sets
21:05:31 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Unsorted
21:05:31 Complex_Bounded_Operators_Dependencies: theory Containers.DList_Set
21:05:32 Complex_Bounded_Operators_Dependencies: theory Cauchy.CauchysMeanTheorem
21:05:32 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial
21:05:33 Complex_Bounded_Operators_Dependencies: theory HOL-Examples.Sqrt
21:05:33 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Complete_Lattice
21:05:33 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Conjugate
21:05:33 Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus_Missing
21:05:34 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Group
21:05:34 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
21:05:34 Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus
21:05:34 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom
21:05:34 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Log_Impl
21:05:34 Complex_Bounded_Operators_Dependencies: theory Show.Show
21:05:34 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.NthRoot_Impl
21:05:36 Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian
21:05:36 Complex_Bounded_Operators_Dependencies: theory Show.Show_Instances
21:05:37 Complex_Bounded_Operators_Dependencies: theory Real_Impl.Real_Impl
21:05:37 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Coset
21:05:37 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.FiniteProduct
21:05:38 Complex_Bounded_Operators_Dependencies: theory Show.Shows_Literal
21:05:38 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Ring
21:05:38 Complex_Bounded_Operators_Dependencies: theory VectorSpace.FunctionLemmas
21:05:41 Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Module
21:05:41 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Ring
21:05:41 Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Order
21:05:42 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:05:42 Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial_Factorial
21:05:43 Complex_Bounded_Operators_Dependencies: theory VectorSpace.RingModuleFacts
21:05:44 Complex_Bounded_Operators_Dependencies: theory VectorSpace.MonoidSums
21:05:44 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Polynomial
21:05:44 Complex_Bounded_Operators_Dependencies: theory VectorSpace.LinearCombinations
21:05:45 Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Order_Polynomial
21:05:45 Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom_Poly
21:05:46 Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
21:05:47 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix
21:05:51 Complex_Bounded_Operators_Dependencies: theory VectorSpace.SumSpaces
21:05:51 Complex_Bounded_Operators_Dependencies: theory VectorSpace.VectorSpace
21:05:52 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
21:05:52 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Show_Matrix
21:05:52 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Shows_Literal_Matrix
21:05:54 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Column_Operations
21:05:55 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant
21:05:58 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant_Impl
21:05:58 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Char_Poly
21:05:58 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_VectorSpace
21:05:59 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form
21:06:02 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.VS_Connect
21:06:16 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gram_Schmidt
21:06:16 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Kernel
21:06:18 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Schur_Decomposition
21:06:23 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
21:06:36 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_ext
21:06:36 Complex_Bounded_Operators_Dependencies: theory Deriving.RBT_Comparator_Impl
21:06:47 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Mapping2
21:06:49 Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Set2
21:06:51 Complex_Bounded_Operators_Dependencies: theory Containers.Set_Impl
21:07:15 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_IArray_Impl
21:07:18 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
21:07:20 Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Impl
21:10:56 Timing Complex_Bounded_Operators_Dependencies (8 threads, 279.902s elapsed time, 1768.538s cpu time, 112.523s GC time, factor 6.32)
21:10:56 Finished Complex_Bounded_Operators_Dependencies (0:05:29 elapsed time, 0:31:20 cpu time, factor 5.71)
21:10:56 Building Jinja (on lxcisa1/0) ...
21:10:58 Jinja: theory Jinja.Auxiliary
21:10:58 Jinja: theory Jinja.Semilat
21:10:58 Jinja: theory List-Index.List_Index
21:10:59 Jinja: theory Jinja.Type
21:10:59 Jinja: theory Jinja.Err
21:10:59 Jinja: theory Jinja.Hidden
21:10:59 Jinja: theory Jinja.Decl
21:10:59 Jinja: theory Jinja.TypeRel
21:11:00 Jinja: theory Jinja.Listn
21:11:00 Jinja: theory Jinja.Opt
21:11:00 Jinja: theory Jinja.Product
21:11:01 Jinja: theory Jinja.Semilattices
21:11:01 Jinja: theory Jinja.Typing_Framework_1
21:11:01 Jinja: theory Jinja.Value
21:11:01 Jinja: theory Jinja.SemilatAlg
21:11:01 Jinja: theory Jinja.Typing_Framework_2
21:11:02 Jinja: theory Jinja.Kildall_1
21:11:02 Jinja: theory Jinja.Kildall_2
21:11:02 Jinja: theory Jinja.LBVSpec
21:11:02 Jinja: theory Jinja.Objects
21:11:02 Jinja: theory Jinja.Typing_Framework_err
21:11:02 Jinja: theory Jinja.Exceptions
21:11:02 Jinja: theory Jinja.JVMState
21:11:02 Jinja: theory Jinja.JVMInstructions
21:11:03 Jinja: theory Jinja.Conform
21:11:03 Jinja: theory Jinja.Expr
21:11:03 Jinja: theory Jinja.State
21:11:03 Jinja: theory Jinja.SystemClasses
21:11:03 Jinja: theory Jinja.LBVComplete
21:11:03 Jinja: theory Jinja.WellForm
21:11:03 Jinja: theory Jinja.LBVCorrect
21:11:03 Jinja: theory Jinja.Abstract_BV
21:11:03 Jinja: theory Jinja.PCompiler
21:11:03 Jinja: theory Jinja.SemiType
21:11:04 Jinja: theory Jinja.JVM_SemiType
21:11:05 Jinja: theory Jinja.JVMExceptions
21:11:05 Jinja: theory Jinja.JVMExecInstr
21:11:05 Jinja: theory Jinja.Effect
21:11:05 Jinja: theory Jinja.JVMExec
21:11:06 Jinja: theory Jinja.JVMDefensive
21:11:06 Jinja: theory Jinja.JVMListExample
21:11:10 Jinja: theory Jinja.Examples
21:11:10 Jinja: theory Jinja.BigStep
21:11:10 Jinja: theory Jinja.SmallStep
21:11:10 Jinja: theory Jinja.WellType
21:11:11 Jinja: theory Jinja.WWellForm
21:11:12 Jinja: theory Jinja.Annotate
21:11:12 Jinja: theory Jinja.WellTypeRT
21:11:12 Jinja: theory Jinja.execute_WellType
21:11:15 Jinja: theory Jinja.DefAss
21:11:15 Jinja: theory Jinja.J1
21:11:15 Jinja: theory Jinja.execute_Bigstep
21:11:15 Jinja: theory Jinja.JWellForm
21:11:17 Jinja: theory Jinja.Equivalence
21:11:17 Jinja: theory Jinja.BVSpec
21:11:17 Jinja: theory Jinja.EffectMono
21:11:17 Jinja: theory Jinja.Compiler2
21:11:17 Jinja: theory Jinja.J1WellForm
21:11:17 Jinja: theory Jinja.Compiler1
21:11:17 Jinja: theory Jinja.BVConform
21:11:18 Jinja: theory Jinja.TF_JVM
21:11:18 Jinja: theory Jinja.Correctness2
21:11:18 Jinja: theory Jinja.BVSpecTypeSafe
21:11:19 Jinja: theory Jinja.Progress
21:11:19 Jinja: theory Jinja.LBVJVM
21:11:19 Jinja: theory Jinja.BVExec
21:11:19 Jinja: theory Jinja.Correctness1
21:11:21 Jinja: theory Jinja.BVNoTypeError
21:11:21 Jinja: theory Jinja.BVExample
21:11:21 Jinja: theory Jinja.TypeSafe
21:11:22 Jinja: theory Jinja.Compiler
21:11:22 Jinja: theory Jinja.TypeComp
21:11:47 Jinja: theory Jinja.Jinja
21:13:34 Preparing Jinja/document ...
21:13:43 Finished Jinja/document (0:00:09 elapsed time)
21:13:43 Preparing Jinja/outline ...
21:13:52 Finished Jinja/outline (0:00:08 elapsed time)
21:13:52 Timing Jinja (8 threads, 137.903s elapsed time, 991.112s cpu time, 16.648s GC time, factor 7.19)
21:13:52 Finished Jinja (0:02:35 elapsed time, 0:17:09 cpu time, factor 6.62)
21:13:52 Building IP_Addresses (on lxcisa1/1) ...
21:13:54 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
21:13:54 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
21:13:54 IP_Addresses: theory HOL-Library.Cancellation
21:13:54 IP_Addresses: theory HOL-Library.Option_ord
21:13:54 IP_Addresses: theory HOL-Library.Infinite_Set
21:13:55 IP_Addresses: theory HOL-Library.Multiset
21:14:01 IP_Addresses: theory HOL-ex.Quicksort
21:14:02 IP_Addresses: theory Automatic_Refinement.Misc
21:14:09 IP_Addresses: theory IP_Addresses.Hs_Compat
21:14:09 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
21:14:09 IP_Addresses: theory HOL-Library.Product_Lexorder
21:14:09 IP_Addresses: theory IP_Addresses.WordInterval
21:14:09 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
21:14:09 IP_Addresses: theory HOL-Library.Code_Target_Nat
21:14:09 IP_Addresses: theory IP_Addresses.Lib_List_toString
21:14:09 IP_Addresses: theory IP_Addresses.Lib_Word_toString
21:14:13 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
21:14:13 IP_Addresses: theory IP_Addresses.IP_Address
21:14:19 IP_Addresses: theory IP_Addresses.IPv4
21:14:20 IP_Addresses: theory IP_Addresses.Prefix_Match
21:14:20 IP_Addresses: theory IP_Addresses.IPv6
21:14:20 IP_Addresses: theory IP_Addresses.CIDR_Split
21:15:11 IP_Addresses: theory IP_Addresses.IP_Address_Parser
21:15:11 IP_Addresses: theory IP_Addresses.IP_Address_toString
21:15:12 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
21:17:51 Preparing IP_Addresses/document ...
21:17:54 Finished IP_Addresses/document (0:00:03 elapsed time)
21:17:54 Preparing IP_Addresses/outline ...
21:17:57 Finished IP_Addresses/outline (0:00:02 elapsed time)
21:17:57 Timing IP_Addresses (8 threads, 224.378s elapsed time, 802.416s cpu time, 30.878s GC time, factor 3.58)
21:17:57 Finished IP_Addresses (0:03:57 elapsed time, 0:13:51 cpu time, factor 3.50)
21:17:57 Running HOL-Codegenerator_Test (on lxcisa1/0) ...
21:18:00 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False
21:18:00 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Group_Closure
21:18:00 HOL-Codegenerator_Test: theory HOL-Examples.Records
21:18:00 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp
21:18:00 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fraction_Field
21:18:00 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Factorial_Ring
21:18:00 HOL-Codegenerator_Test: theory HOL-Examples.Gauss_Numbers
21:18:00 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Lazy_Test
21:18:00 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less
21:18:00 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del
21:18:00 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del
21:18:01 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_Specs
21:18:01 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_Specs
21:18:01 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set
21:18:03 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map
21:18:12 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML
21:18:12 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala
21:18:12 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm
21:18:27 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Normalized_Fraction
21:18:27 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Primes
21:18:36 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Nth_Powers
21:18:36 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Squarefree
21:18:36 HOL-Codegenerator_Test: theory HOL-Number_Theory.Eratosthenes
21:18:36 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Power_Series
21:18:36 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial
21:18:48 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:18:48 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_FPS
21:18:48 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Polynomial_Factorial
21:18:48 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Formal_Laurent_Series
21:18:52 HOL-Codegenerator_Test: theory HOL-Computational_Algebra.Computational_Algebra
21:18:54 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates
21:18:58 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate
21:18:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Abstract_Char
21:18:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat
21:18:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures
21:18:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat
21:24:38 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC
21:24:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton
21:24:44 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml
21:24:45 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ
21:24:49 Timing HOL-Codegenerator_Test (8 threads, 406.748s elapsed time, 1136.018s cpu time, 57.625s GC time, factor 2.79)
21:24:49 Finished HOL-Codegenerator_Test (0:06:50 elapsed time, 0:19:04 cpu time, factor 2.79)
21:24:49 Building Padic_Ints (on lxcisa1/1) ...
21:24:52 Padic_Ints: theory Padic_Ints.Function_Ring
21:24:52 Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
21:24:52 Padic_Ints: theory Padic_Ints.Extended_Int
21:24:52 Padic_Ints: theory HOL-Number_Theory.Cong
21:24:54 Padic_Ints: theory HOL-Number_Theory.Totient
21:24:55 Padic_Ints: theory HOL-Number_Theory.Residues
21:24:58 Padic_Ints: theory Padic_Ints.Padic_Construction
21:24:59 Padic_Ints: theory Padic_Ints.Padic_Integers
21:25:01 Padic_Ints: theory Padic_Ints.Cring_Poly
21:25:56 Padic_Ints: theory Padic_Ints.Padic_Int_Topology
21:25:59 Padic_Ints: theory Padic_Ints.Zp_Compact
21:26:32 Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
21:26:36 Padic_Ints: theory Padic_Ints.Hensels_Lemma
21:27:10 Preparing Padic_Ints/document ...
21:27:41 Finished Padic_Ints/document (0:00:30 elapsed time)
21:27:41 Preparing Padic_Ints/outline ...
21:27:52 Finished Padic_Ints/outline (0:00:11 elapsed time)
21:27:52 Timing Padic_Ints (8 threads, 119.354s elapsed time, 500.210s cpu time, 47.196s GC time, factor 4.19)
21:27:52 Finished Padic_Ints (0:02:19 elapsed time, 0:09:04 cpu time, factor 3.89)
21:27:52 Building Projective_Measurements (on lxcisa1/0) ...
21:27:58 Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
21:27:58 Projective_Measurements: theory HOL-Computational_Algebra.Fraction_Field
21:27:58 Projective_Measurements: theory HOL-Algebra.Congruence
21:27:58 Projective_Measurements: theory Abstract-Rewriting.Seq
21:27:58 Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
21:27:58 Projective_Measurements: theory HOL-Library.More_List
21:27:58 Projective_Measurements: theory HOL-Library.While_Combinator
21:27:58 Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
21:27:58 Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
21:27:58 Projective_Measurements: theory Jordan_Normal_Form.Conjugate
21:27:59 Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
21:27:59 Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
21:27:59 Projective_Measurements: theory Matrix.Utility
21:27:59 Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
21:27:59 Projective_Measurements: theory Regular-Sets.Regular_Set
21:27:59 Projective_Measurements: theory HOL-Algebra.Order
21:27:59 Projective_Measurements: theory HOL-Computational_Algebra.Normalized_Fraction
21:28:00 Projective_Measurements: theory VectorSpace.FunctionLemmas
21:28:00 Projective_Measurements: theory HOL-Algebra.Lattice
21:28:02 Projective_Measurements: theory HOL-Algebra.Complete_Lattice
21:28:03 Projective_Measurements: theory HOL-Algebra.Group
21:28:04 Projective_Measurements: theory Regular-Sets.Regular_Exp
21:28:06 Projective_Measurements: theory HOL-Algebra.Coset
21:28:06 Projective_Measurements: theory HOL-Algebra.FiniteProduct
21:28:06 Projective_Measurements: theory HOL-Algebra.Ring
21:28:08 Projective_Measurements: theory Regular-Sets.NDerivative
21:28:08 Projective_Measurements: theory Regular-Sets.Relation_Interpretation
21:28:10 Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
21:28:10 Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
21:28:11 Projective_Measurements: theory HOL-Algebra.Module
21:28:11 Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
21:28:12 Projective_Measurements: theory Regular-Sets.Equivalence_Checking
21:28:12 Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
21:28:12 Projective_Measurements: theory Regular-Sets.Regexp_Method
21:28:13 Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
21:28:13 Projective_Measurements: theory VectorSpace.RingModuleFacts
21:28:14 Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
21:28:14 Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
21:28:14 Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
21:28:15 Projective_Measurements: theory VectorSpace.MonoidSums
21:28:15 Projective_Measurements: theory VectorSpace.LinearCombinations
21:28:16 Projective_Measurements: theory Abstract-Rewriting.SN_Orders
21:28:17 Projective_Measurements: theory Jordan_Normal_Form.Matrix
21:28:19 Projective_Measurements: theory Matrix.Ordered_Semiring
21:28:20 Projective_Measurements: theory Matrix.Matrix_Legacy
21:28:21 Projective_Measurements: theory VectorSpace.SumSpaces
21:28:22 Projective_Measurements: theory VectorSpace.VectorSpace
21:28:22 Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
21:28:23 Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
21:28:25 Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
21:28:26 Projective_Measurements: theory Jordan_Normal_Form.Determinant
21:28:28 Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
21:28:29 Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
21:28:29 Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
21:28:30 Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
21:28:30 Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
21:28:30 Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
21:28:33 Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
21:28:33 Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
21:28:34 Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
21:28:34 Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
21:28:46 Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
21:28:48 Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
21:28:53 Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
21:28:58 Projective_Measurements: theory QHLProver.Complex_Matrix
21:29:07 Projective_Measurements: theory QHLProver.Gates
21:29:07 Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
21:29:13 Projective_Measurements: theory Projective_Measurements.Projective_Measurements
21:29:15 Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
21:37:27 Preparing Projective_Measurements/document ...
21:37:32 Finished Projective_Measurements/document (0:00:04 elapsed time)
21:37:32 Preparing Projective_Measurements/outline ...
21:37:34 Finished Projective_Measurements/outline (0:00:02 elapsed time)
21:37:34 Timing Projective_Measurements (8 threads, 532.616s elapsed time, 1330.921s cpu time, 51.809s GC time, factor 2.50)
21:37:34 Finished Projective_Measurements (0:09:29 elapsed time, 0:23:32 cpu time, factor 2.48)
21:37:35 Building Algebraic_Numbers (on lxcisa1/1) ...
21:37:43 Algebraic_Numbers: theory Pure-ex.Guess
21:37:43 Algebraic_Numbers: theory Deriving.Compare_Rat
21:37:43 Algebraic_Numbers: theory Deriving.Compare_Real
21:37:43 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Roots_Real_Poly
21:37:43 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
21:37:43 Algebraic_Numbers: theory Algebraic_Numbers.Bivariate_Polynomials
21:37:43 Algebraic_Numbers: theory Show.Show_Real
21:37:43 Algebraic_Numbers: theory Sturm_Sequences.Misc_Polynomial
21:37:43 Algebraic_Numbers: theory Show.Show_Complex
21:37:43 Algebraic_Numbers: theory Algebraic_Numbers.Compare_Complex
21:37:44 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Library
21:37:44 Algebraic_Numbers: theory Sturm_Sequences.Sturm_Theorem
21:37:46 Algebraic_Numbers: theory Algebraic_Numbers.Resultant
21:37:46 Algebraic_Numbers: theory Algebraic_Numbers.Interval_Arithmetic
21:37:46 Algebraic_Numbers: theory Algebraic_Numbers.Min_Int_Poly
21:37:46 Algebraic_Numbers: theory Algebraic_Numbers.Sturm_Rat
21:37:46 Algebraic_Numbers: theory Algebraic_Numbers.Factors_of_Int_Poly
21:37:48 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers
21:37:51 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
21:37:57 Algebraic_Numbers: theory Algebraic_Numbers.Cauchy_Root_Bound
21:37:57 Algebraic_Numbers: theory Algebraic_Numbers.Real_Algebraic_Numbers
21:38:09 Algebraic_Numbers: theory Algebraic_Numbers.Real_Roots
21:38:09 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Alg
21:38:09 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Approx
21:38:09 Algebraic_Numbers: theory Algebraic_Numbers.Show_Real_Precise
21:38:10 Algebraic_Numbers: theory Algebraic_Numbers.Complex_Algebraic_Numbers
21:38:14 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Number_Tests
21:38:19 Algebraic_Numbers: theory Algebraic_Numbers.Algebraic_Numbers_External_Code
21:40:05 Preparing Algebraic_Numbers/document ...
21:40:15 Build timed out (after 400 minutes). Marking the build as aborted.
21:40:15 Build was aborted
21:40:15 Started calculate disk usage of build
21:40:15 Finished Calculation of disk usage of build in 0 seconds
21:40:15 Started calculate disk usage of workspace
21:40:17 Finished Calculation of disk usage of workspace in  1 second
21:40:17 Finished: ABORTED