HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
13:35:07HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
13:35:08HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
13:35:08HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
13:35:08HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
13:35:09HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
13:35:09HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
13:35:09HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
13:35:09HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
13:35:10HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
13:35:11HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
13:35:11HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
13:35:11HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
13:35:11HOL-ODE-Numerics: theory Collections.Intf_Comp
13:35:11HOL-ODE-Numerics: theory Collections.Idx_Iterator
13:35:12HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
13:35:13HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
13:35:13HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
13:35:13HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
13:35:14HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
13:35:15HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
13:35:15HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
13:35:15HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
13:35:19HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
13:35:19HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
13:35:19HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
13:35:19HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
13:35:20HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
13:35:20HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
13:35:22HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
13:35:23HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
13:35:23HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
13:35:23HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
13:35:27HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
13:35:27HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
13:35:27HOL-ODE-Numerics: theory Native_Word.Uint
13:35:27HOL-ODE-Numerics: theory Native_Word.Uint32
13:35:27HOL-ODE-Numerics: theory Collections.Code_Target_ICF
13:35:28HOL-ODE-Numerics: theory Collections.Gen_Iterator
13:35:28HOL-ODE-Numerics: theory Collections.Intf_Map
13:35:28HOL-ODE-Numerics: theory Collections.Intf_Set
13:35:29HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
13:35:29HOL-ODE-Numerics: theory Collections.Iterator
13:35:29HOL-ODE-Numerics: theory Collections.HashCode
13:35:30HOL-ODE-Numerics: theory Collections.Intf_Hash
13:35:30HOL-ODE-Numerics: theory Deriving.Hash_Generator
13:35:30HOL-ODE-Numerics: theory Collections.Array_Iterator
13:35:30HOL-ODE-Numerics: theory Collections.Gen_Map
13:35:30HOL-ODE-Numerics: theory Collections.Gen_Map2Set
13:35:30HOL-ODE-Numerics: theory Collections.Gen_Set
13:35:31HOL-ODE-Numerics: theory Collections.Impl_List_Set
13:35:31HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
13:35:31HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
13:35:31HOL-ODE-Numerics: theory Collections.Impl_Array_Map
13:35:31HOL-ODE-Numerics: theory Collections.Impl_List_Map
13:35:32HOL-ODE-Numerics: theory Collections.Gen_Hash
13:35:32HOL-ODE-Numerics: theory Deriving.Hash_Instances
13:35:32HOL-ODE-Numerics: theory Deriving.Derive
13:35:33HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
13:36:05HOL-ODE-Numerics: theory HOL-Library.RBT
13:36:05HOL-ODE-Numerics: theory Collections.RBT_add
13:36:06HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
13:36:06HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
13:36:07HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
13:36:15HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
13:36:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
13:36:22HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
13:36:23HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
13:36:24HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
13:36:27HOL-ODE-Numerics: theory Affine_Arithmetic.Print
13:36:29HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
13:36:30HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
13:36:30HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
13:36:30HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
13:36:30HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
13:36:31HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
13:36:31HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
13:36:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
13:36:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
13:36:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
13:36:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
13:36:50HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
13:36:50HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
13:36:54HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
13:36:57HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
13:36:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
13:36:59HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
13:37:01HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
13:37:17HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
13:37:42HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
13:37:42HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
13:37:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
13:38:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
13:38:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
13:38:00HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
13:38:14HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
13:38:16HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
13:38:26HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
13:38:51HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
13:39:41HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
13:47:48HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
13:48:22HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
13:49:43HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
13:51:23Timing HOL-ODE-Numerics (8 threads, 911.302s elapsed time, 5035.373s cpu time, 299.781s GC time, factor 5.53)
13:51:23Finished HOL-ODE-Numerics (0:16:26 elapsed time, 1:26:58 cpu time, factor 5.29)
13:51:24Building Lorenz_Approximation (on hpcisabelle/1) ...
13:51:28Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
13:51:33Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
13:51:53Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
13:56:00Timing Lorenz_Approximation (8 threads, 249.666s elapsed time, 623.783s cpu time, 34.616s GC time, factor 2.50)
13:56:00Finished Lorenz_Approximation (0:04:35 elapsed time, 0:11:11 cpu time, factor 2.44)
13:56:01Running Lorenz_C0 (on hpcisabelle/2) ...
13:56:04Lorenz_C0: theory Lorenz_C0.Lorenz_C0
14:20:53Timing Lorenz_C0 (8 threads, 1488.107s elapsed time, 11733.540s cpu time, 23.860s GC time, factor 7.88)
14:20:53Finished Lorenz_C0 (0:24:52 elapsed time, 3:15:39 cpu time, factor 7.87)
14:20:54Building HOL-Library (on hpcisabelle/3) ...
14:20:55HOL-Library: theory HOL-Library.README
14:20:55HOL-Library: theory HOL-Library.Adhoc_Overloading
14:20:55HOL-Library: theory HOL-Library.AList
14:20:55HOL-Library: theory HOL-Library.BNF_Corec
14:20:55HOL-Library: theory HOL-Library.BNF_Axiomatization
14:20:55HOL-Library: theory HOL-Library.Case_Converter
14:20:55HOL-Library: theory HOL-Library.Cancellation
14:20:55HOL-Library: theory HOL-Library.Centered_Division
14:20:55HOL-Library: theory HOL-Library.Char_ord
14:20:55HOL-Library: theory HOL-Library.Code_Abstract_Char
14:20:55HOL-Library: theory HOL-Library.Code_Abstract_Nat
14:20:56HOL-Library: theory HOL-Library.Code_Prolog
14:20:56HOL-Library: theory HOL-Library.Monad_Syntax
14:20:56HOL-Library: theory HOL-Library.Code_Binary_Nat
14:20:56HOL-Library: theory HOL-Library.State_Monad
14:20:56HOL-Library: theory HOL-Library.Code_Lazy
14:20:56HOL-Library: theory HOL-Library.Simps_Case_Conv
14:20:57HOL-Library: theory HOL-Library.Extended
14:20:57HOL-Library: theory HOL-Library.Multiset
14:20:57HOL-Library: theory HOL-Library.Code_Target_Nat
14:20:58HOL-Library: theory HOL-Library.Code_Target_Int
14:20:58HOL-Library: theory HOL-Library.Code_Test
14:20:58HOL-Library: theory HOL-Library.Code_Target_Numeral
14:20:58HOL-Library: theory HOL-Library.Combine_PER
14:20:58HOL-Library: theory HOL-Library.DAList
14:20:58HOL-Library: theory HOL-Library.Comparator
14:20:58HOL-Library: theory HOL-Library.Complete_Partial_Order2
14:20:59HOL-Library: theory HOL-Library.Conditional_Parametricity
14:20:59HOL-Library: theory HOL-Library.Confluence
14:21:00HOL-Library: theory HOL-Library.Datatype_Records
14:21:00HOL-Library: theory HOL-Library.Confluent_Quotient
14:21:00HOL-Library: theory HOL-Library.Debug
14:21:00HOL-Library: theory HOL-Library.Dlist
14:21:00HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
14:21:00HOL-Library: theory HOL-Library.Fun_Lexorder
14:21:00HOL-Library: theory HOL-Library.FuncSet
14:21:01HOL-Library: theory HOL-Library.Function_Algebras
14:21:01HOL-Library: theory HOL-Library.Groups_Big_Fun
14:21:01HOL-Library: theory HOL-Library.Function_Division
14:21:02HOL-Library: theory HOL-Library.IArray
14:21:02HOL-Library: theory HOL-Library.Infinite_Set
14:21:02HOL-Library: theory HOL-Library.Disjoint_Sets
14:21:02HOL-Library: theory HOL-Library.LaTeXsugar
14:21:03HOL-Library: theory HOL-Library.Lattice_Constructions
14:21:03HOL-Library: theory HOL-Library.Omega_Words_Fun
14:21:03HOL-Library: theory HOL-Library.ListVector
14:21:03HOL-Library: theory HOL-Library.List_Lenlexorder
14:21:04HOL-Library: theory HOL-Library.List_Lexorder
14:21:04HOL-Library: theory HOL-Library.Mapping
14:21:04HOL-Library: theory HOL-Library.More_List
14:21:04HOL-Library: theory HOL-Library.NList
14:21:04HOL-Library: theory HOL-Library.Nat_Bijection
14:21:04HOL-Library: theory HOL-Library.Poly_Mapping
14:21:04HOL-Library: theory HOL-Library.Stream
14:21:06HOL-Library: theory HOL-Library.Old_Datatype
14:21:07HOL-Library: theory HOL-Library.AList_Mapping
14:21:08HOL-Library: theory HOL-Library.Old_Recdef
14:21:08HOL-Library: theory HOL-Library.Open_State_Syntax
14:21:08HOL-Library: theory HOL-Library.Option_ord
14:21:08HOL-Library: theory HOL-Library.Parallel
14:21:09HOL-Library: theory HOL-Library.Pattern_Aliases
14:21:09HOL-Library: theory HOL-Library.Phantom_Type
14:21:09HOL-Library: theory HOL-Library.Power_By_Squaring
14:21:09HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
14:21:09HOL-Library: theory HOL-Library.DAList_Multiset
14:21:09HOL-Library: theory HOL-Library.Multiset_Order
14:21:09HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
14:21:09HOL-Library: theory HOL-Library.Preorder
14:21:09HOL-Library: theory HOL-Library.Cardinality
14:21:11HOL-Library: theory HOL-Library.Product_Lexorder
14:21:11HOL-Library: theory HOL-Library.Product_Plus
14:21:11HOL-Library: theory HOL-Library.Quotient_Syntax
14:21:11HOL-Library: theory HOL-Library.Quotient_Option
14:21:11HOL-Library: theory HOL-Library.Quotient_Product
14:21:11HOL-Library: theory HOL-Library.Quotient_Set
14:21:11HOL-Library: theory HOL-Library.Quotient_Sum
14:21:11HOL-Library: theory HOL-Library.Product_Order
14:21:11HOL-Library: theory HOL-Library.Quotient_Type
14:21:11HOL-Library: theory HOL-Library.RBT_Impl
14:21:11HOL-Library: theory HOL-Library.Realizers
14:21:11HOL-Library: theory HOL-Library.Quotient_List
14:21:13HOL-Library: theory HOL-Library.Finite_Lattice
14:21:13HOL-Library: theory HOL-Library.Reflection
14:21:13HOL-Library: theory HOL-Library.Refute
14:21:13HOL-Library: theory HOL-Library.Rewrite
14:21:13HOL-Library: theory HOL-Library.Set_Algebras
14:21:13HOL-Library: theory HOL-Library.Code_Cardinality
14:21:13HOL-Library: theory HOL-Library.Numeral_Type
14:21:14HOL-Library: theory HOL-Library.Signed_Division
14:21:14HOL-Library: theory HOL-Library.Sorting_Algorithms
14:21:14HOL-Library: theory HOL-Library.Sublist
14:21:15HOL-Library: theory HOL-Library.Transitive_Closure_Table
14:21:15HOL-Library: theory HOL-Library.Tree
14:21:15HOL-Library: theory HOL-Library.Type_Length
14:21:15HOL-Library: theory HOL-Library.Uprod
14:21:15HOL-Library: theory HOL-Library.While_Combinator
14:21:16HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
14:21:16HOL-Library: theory HOL-Library.Saturated
14:21:16HOL-Library: theory HOL-Library.Word
14:21:16HOL-Library: theory HOL-Library.Z2
14:21:16HOL-Library: theory HOL-Library.Countable
14:21:16HOL-Library: theory HOL-Library.Prefix_Order
14:21:16HOL-Library: theory HOL-Library.Subseq_Order
14:21:17HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
14:21:17HOL-Library: theory HOL-Library.Complex_Order
14:21:17HOL-Library: theory HOL-Library.Diagonal_Subsequence
14:21:17HOL-Library: theory HOL-Library.Discrete
14:21:17HOL-Library: theory HOL-Library.Going_To_Filter
14:21:17HOL-Library: theory HOL-Library.Indicator_Function
14:21:17HOL-Library: theory HOL-Library.Infinite_Typeclass
14:21:17HOL-Library: theory HOL-Library.Landau_Symbols
14:21:17HOL-Library: theory HOL-Library.Lattice_Algebras
14:21:18HOL-Library: theory HOL-Library.Liminf_Limsup
14:21:18HOL-Library: theory HOL-Library.Tree_Multiset
14:21:18HOL-Library: theory HOL-Library.Countable_Set
14:21:18HOL-Library: theory HOL-Library.FSet
14:21:18HOL-Library: theory HOL-Library.Log_Nat
14:21:18HOL-Library: theory HOL-Library.Countable_Complete_Lattices
14:21:18HOL-Library: theory HOL-Library.Countable_Set_Type
14:21:20HOL-Library: theory HOL-Library.Equipollence
14:21:20HOL-Library: theory HOL-Library.Set_Idioms
14:21:20HOL-Library: theory HOL-Library.Lub_Glb
14:21:20HOL-Library: theory HOL-Library.Ramsey
14:21:21HOL-Library: theory HOL-Library.Nonpos_Ints
14:21:21HOL-Library: theory HOL-Library.OptionalSugar
14:21:21HOL-Library: theory HOL-Library.Order_Continuity
14:21:21HOL-Library: theory HOL-Library.Periodic_Fun
14:21:21HOL-Library: theory HOL-Library.Quadratic_Discriminant
14:21:21HOL-Library: theory HOL-Library.Finite_Map
14:21:21HOL-Library: theory HOL-Library.Real_Mod
14:21:21HOL-Library: theory HOL-Library.Sum_of_Squares
14:21:22HOL-Library: theory HOL-Library.Extended_Nat
14:21:22HOL-Library: theory HOL-Library.Tree_Real
14:21:22HOL-Library: theory HOL-Library.Extended_Real
14:21:22HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
14:21:22HOL-Library: theory HOL-Library.Interval
14:21:25HOL-Library: theory HOL-Library.Float
14:21:28HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
14:21:28HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
14:21:28HOL-Library: theory HOL-Library.Interval_Float
14:21:37HOL-Library: theory HOL-Library.Disjoint_FSets
14:21:38HOL-Library: theory HOL-Library.Library
14:22:18HOL-Library: theory HOL-Library.RBT
14:22:19HOL-Library: theory HOL-Library.RBT_Mapping
14:22:19HOL-Library: theory HOL-Library.RBT_Set
14:24:34Preparing HOL-Library/document ...
14:25:39Finished HOL-Library/document (0:01:04 elapsed time)
14:25:39Preparing HOL-Library/outline ...
14:26:16Finished HOL-Library/outline (0:00:37 elapsed time)
14:26:17Timing HOL-Library (8 threads, 179.460s elapsed time, 1203.175s cpu time, 56.232s GC time, factor 6.70)
14:26:17Finished HOL-Library (0:03:34 elapsed time, 0:21:29 cpu time, factor 6.00)
14:26:17Building HOL-Computational_Algebra (on hpcisabelle/4) ...
14:26:19HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
14:26:19HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
14:26:19HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
14:26:30HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
14:26:44HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
14:26:44HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
14:26:44HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
14:26:53HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
14:26:53HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
14:26:53HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
14:26:54HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
14:27:07HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
14:27:07HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
14:27:07HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
14:27:08HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
14:27:12HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
14:27:42Preparing HOL-Computational_Algebra/document ...
14:28:08Finished HOL-Computational_Algebra/document (0:00:25 elapsed time)
14:28:08Preparing HOL-Computational_Algebra/outline ...
14:28:20Finished HOL-Computational_Algebra/outline (0:00:12 elapsed time)
14:28:20Timing HOL-Computational_Algebra (8 threads, 67.236s elapsed time, 274.206s cpu time, 6.105s GC time, factor 4.08)
14:28:20Finished HOL-Computational_Algebra (0:01:23 elapsed time, 0:05:06 cpu time, factor 3.67)
14:28:20Building HOL-Algebra (on hpcisabelle/5) ...
14:28:23HOL-Algebra: theory HOL-Algebra.README
14:28:23HOL-Algebra: theory HOL-Cardinals.Fun_More
14:28:23HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
14:28:23HOL-Algebra: theory HOL-Combinatorics.Transposition
14:28:23HOL-Algebra: theory HOL-Algebra.Congruence
14:28:23HOL-Algebra: theory HOL-Algebra.Exponent
14:28:23HOL-Algebra: theory HOL-Cardinals.Order_Union
14:28:23HOL-Algebra: theory HOL-Combinatorics.Permutations
14:28:23HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
14:28:23HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
14:28:24HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
14:28:24HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
14:28:25HOL-Algebra: theory HOL-Algebra.Order
14:28:25HOL-Algebra: theory HOL-Combinatorics.Cycles
14:28:25HOL-Algebra: theory HOL-Combinatorics.List_Permutation
14:28:25HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
14:28:26HOL-Algebra: theory HOL-Algebra.Lattice
14:28:26HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
14:28:27HOL-Algebra: theory HOL-Algebra.Complete_Lattice
14:28:29HOL-Algebra: theory HOL-Algebra.Galois_Connection
14:28:29HOL-Algebra: theory HOL-Algebra.Group
14:28:31HOL-Algebra: theory HOL-Algebra.Bij
14:28:31HOL-Algebra: theory HOL-Algebra.Coset
14:28:32HOL-Algebra: theory HOL-Algebra.FiniteProduct
14:28:32HOL-Algebra: theory HOL-Algebra.Ring
14:28:34HOL-Algebra: theory HOL-Algebra.Group_Action
14:28:34HOL-Algebra: theory HOL-Algebra.Left_Coset
14:28:34HOL-Algebra: theory HOL-Algebra.SimpleGroups
14:28:34HOL-Algebra: theory HOL-Algebra.SndIsomorphismGrp
14:28:35HOL-Algebra: theory HOL-Algebra.Sylow
14:28:35HOL-Algebra: theory HOL-Algebra.Generated_Groups
14:28:35HOL-Algebra: theory HOL-Algebra.Divisibility
14:28:35HOL-Algebra: theory HOL-Algebra.Zassenhaus
14:28:36HOL-Algebra: theory HOL-Algebra.Solvable_Groups
14:28:36HOL-Algebra: theory HOL-Algebra.Elementary_Groups
14:28:36HOL-Algebra: theory HOL-Algebra.Sym_Groups
14:28:38HOL-Algebra: theory HOL-Algebra.Exact_Sequence
14:28:38HOL-Algebra: theory HOL-Algebra.Product_Groups
14:28:39HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
14:28:39HOL-Algebra: theory HOL-Algebra.AbelCoset
14:28:39HOL-Algebra: theory HOL-Algebra.Module
14:28:44HOL-Algebra: theory HOL-Algebra.Ideal
14:28:47HOL-Algebra: theory HOL-Algebra.Ideal_Product
14:28:47HOL-Algebra: theory HOL-Algebra.RingHom
14:28:49HOL-Algebra: theory HOL-Algebra.QuotRing
14:28:49HOL-Algebra: theory HOL-Algebra.UnivPoly
14:28:53HOL-Algebra: theory HOL-Algebra.IntRing
14:28:53HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
14:28:54HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
14:29:05HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
14:29:10HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
14:29:10HOL-Algebra: theory HOL-Algebra.Subrings
14:29:13HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
14:29:15HOL-Algebra: theory HOL-Algebra.Generated_Rings
14:29:16HOL-Algebra: theory HOL-Algebra.Generated_Fields
14:29:20HOL-Algebra: theory HOL-Algebra.Polynomials
14:29:40HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
14:30:21HOL-Algebra: theory HOL-Algebra.Finite_Extensions
14:30:21HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
14:30:35HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
14:30:45HOL-Algebra: theory HOL-Algebra.Algebra
14:30:45HOL-Algebra: theory HOL-Algebra.Algebraic_Closure_Type
14:31:28Preparing HOL-Algebra/document ...
14:31:57Finished HOL-Algebra/document (0:00:28 elapsed time)
14:31:57Preparing HOL-Algebra/outline ...
14:32:11Finished HOL-Algebra/outline (0:00:13 elapsed time)
14:32:11Timing HOL-Algebra (8 threads, 157.008s elapsed time, 787.585s cpu time, 79.329s GC time, factor 5.02)
14:32:11Finished HOL-Algebra (0:03:05 elapsed time, 0:14:11 cpu time, factor 4.60)
14:32:11Building Automatic_Refinement (on hpcisabelle/6) ...
14:32:13Automatic_Refinement: theory HOL-Eisbach.Eisbach
14:32:13Automatic_Refinement: theory Automatic_Refinement.Foldi
14:32:13Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
14:32:13Automatic_Refinement: theory Automatic_Refinement.Prio_List
14:32:13Automatic_Refinement: theory HOL-Library.Option_ord
14:32:13Automatic_Refinement: theory HOL-Library.Infinite_Set
14:32:13Automatic_Refinement: theory HOL-Library.Cancellation
14:32:13Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
14:32:13Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
14:32:13Automatic_Refinement: theory Automatic_Refinement.Refine_Util
14:32:14Automatic_Refinement: theory HOL-Library.Multiset
14:32:14Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
14:32:15Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
14:32:15Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
14:32:15Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
14:32:15Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
14:32:15Automatic_Refinement: theory Automatic_Refinement.Select_Solve
14:32:15Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
14:32:21Automatic_Refinement: theory HOL-ex.Quicksort
14:32:21Automatic_Refinement: theory Automatic_Refinement.Misc
14:32:28Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
14:32:30Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
14:32:30Automatic_Refinement: theory Automatic_Refinement.Relators
14:32:32Automatic_Refinement: theory Automatic_Refinement.Param_Tool
14:32:32Automatic_Refinement: theory Automatic_Refinement.Param_HOL
14:32:33Automatic_Refinement: theory Automatic_Refinement.Parametricity
14:32:34Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
14:32:34Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
14:32:34Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
14:32:34Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
14:32:35Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
14:32:36Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
14:32:41Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
14:32:51Preparing Automatic_Refinement/document ...
14:32:54Finished Automatic_Refinement/document (0:00:03 elapsed time)
14:32:54Preparing Automatic_Refinement/outline ...
14:32:57Finished Automatic_Refinement/outline (0:00:02 elapsed time)
14:32:57Timing Automatic_Refinement (8 threads, 28.281s elapsed time, 120.079s cpu time, 3.656s GC time, factor 4.25)
14:32:57Finished Automatic_Refinement (0:00:38 elapsed time, 0:02:19 cpu time, factor 3.64)
14:32:57Building Refine_Monadic (on hpcisabelle/7) ...
14:32:58Refine_Monadic: theory HOL-Library.Phantom_Type
14:32:58Refine_Monadic: theory HOL-Library.Adhoc_Overloading
14:32:58Refine_Monadic: theory Refine_Monadic.Refine_Chapter
14:32:58Refine_Monadic: theory Refine_Monadic.Example_Chapter
14:32:58Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
14:32:58Refine_Monadic: theory HOL-Library.While_Combinator
14:32:59Refine_Monadic: theory HOL-Library.Monad_Syntax
14:32:59Refine_Monadic: theory Refine_Monadic.Refine_Misc
14:33:00Refine_Monadic: theory HOL-Library.Cardinality
14:33:00Refine_Monadic: theory Refine_Monadic.RefineG_Domain
14:33:00Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
14:33:00Refine_Monadic: theory Refine_Monadic.RefineG_Assert
14:33:01Refine_Monadic: theory HOL-Library.Numeral_Type
14:33:01Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
14:33:02Refine_Monadic: theory Refine_Monadic.RefineG_While
14:33:02Refine_Monadic: theory Refine_Monadic.Refine_Basic
14:33:02Refine_Monadic: theory HOL-Library.Type_Length
14:33:03Refine_Monadic: theory Refine_Monadic.Refine_Det
14:33:03Refine_Monadic: theory HOL-Library.Word
14:33:06Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
14:33:06Refine_Monadic: theory Refine_Monadic.Refine_Leof
14:33:07Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
14:33:07Refine_Monadic: theory Refine_Monadic.Refine_Pfun
14:33:07Refine_Monadic: theory Refine_Monadic.Refine_While
14:33:09Refine_Monadic: theory Refine_Monadic.Refine_Transfer
14:33:10Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
14:33:10Refine_Monadic: theory Refine_Monadic.Refine_Automation
14:33:10Refine_Monadic: theory Refine_Monadic.Refine_Foreach
14:33:13Refine_Monadic: theory Refine_Monadic.Refine_Monadic
14:33:14Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
14:33:15Refine_Monadic: theory Refine_Monadic.WordRefine
14:33:15Refine_Monadic: theory Refine_Monadic.Examples
14:33:51Preparing Refine_Monadic/document ...
14:34:02Finished Refine_Monadic/document (0:00:10 elapsed time)
14:34:02Preparing Refine_Monadic/outline ...
14:34:09Finished Refine_Monadic/outline (0:00:07 elapsed time)
14:34:10Timing Refine_Monadic (8 threads, 40.912s elapsed time, 184.968s cpu time, 10.587s GC time, factor 4.52)
14:34:10Finished Refine_Monadic (0:00:52 elapsed time, 0:03:29 cpu time, factor 3.96)
14:34:10Building Collections (on hpcisabelle/0) ...
14:34:11Collections: theory Collections.ICF_Tools
14:34:11Collections: theory Collections.Partial_Equivalence_Relation
14:34:11Collections: theory Finger-Trees.FingerTree
14:34:11Collections: theory HOL-Library.AList
14:34:11Collections: theory Binomial-Heaps.BinomialHeap
14:34:11Collections: theory Binomial-Heaps.SkewBinomialHeap
14:34:11Collections: theory HOL-Library.Code_Target_Int
14:34:11Collections: theory HOL-Library.Code_Abstract_Nat
14:34:12Collections: theory HOL-Library.Confluence
14:34:12Collections: theory HOL-Library.Code_Target_Nat
14:34:12Collections: theory Collections.Ord_Code_Preproc
14:34:12Collections: theory HOL-Library.Confluent_Quotient
14:34:12Collections: theory Collections.Locale_Code
14:34:12Collections: theory Collections.Record_Intf
14:34:12Collections: theory HOL-Library.Code_Target_Numeral
14:34:12Collections: theory Collections.SetIterator
14:34:12Collections: theory HOL-Library.Dlist
14:34:12Collections: theory Collections.Sorted_List_Operations
14:34:12Collections: theory Word_Lib.Bit_Comprehension
14:34:13Collections: theory Word_Lib.More_Divides
14:34:14Collections: theory HOL-Library.RBT_Impl
14:34:14Collections: theory HOL-Library.Signed_Division
14:34:14Collections: theory Collections.DatRef
14:34:14Collections: theory Collections.Idx_Iterator
14:34:15Collections: theory Collections.SetAbstractionIterator
14:34:15Collections: theory Collections.SetIteratorOperations
14:34:15Collections: theory Word_Lib.Signed_Division_Word
14:34:15Collections: theory Native_Word.Code_Int_Integer_Conversion
14:34:15Collections: theory Word_Lib.More_Arithmetic
14:34:15Collections: theory Word_Lib.More_Bit_Ring
14:34:17Collections: theory Word_Lib.More_Word
14:34:19Collections: theory Collections.Assoc_List
14:34:19Collections: theory Collections.Dlist_add
14:34:19Collections: theory Collections.Proper_Iterator
14:34:19Collections: theory Collections.SetIteratorGA
14:34:19Collections: theory Native_Word.Code_Target_Word_Base
14:34:19Collections: theory Collections.Diff_Array
14:34:19Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
14:34:19Collections: theory Collections.It_to_It
14:34:20Collections: theory Collections.Gen_Iterator
14:34:20Collections: theory Word_Lib.Least_significant_bit
14:34:20Collections: theory Collections.Iterator
14:34:21Collections: theory Word_Lib.Most_significant_bit
14:34:21Collections: theory Collections.ICF_Spec_Base
14:34:21Collections: theory Word_Lib.Generic_set_bit
14:34:21Collections: theory Collections.MapSpec
14:34:22Collections: theory Native_Word.Code_Target_Integer_Bit
14:34:22Collections: theory Native_Word.Word_Type_Copies
14:34:27Collections: theory Collections.Robdd
14:34:38Collections: theory Native_Word.Code_Target_Int_Bit
14:34:38Collections: theory Native_Word.Uint32
14:34:38Collections: theory Collections.Code_Target_ICF
14:34:38Collections: theory Collections.Locale_Code_Ex
14:34:40Collections: theory Collections.HashCode
14:35:27Collections: theory Collections.RBT_add
14:36:04Collections: theory Collections.GenCF_Gen_Chapter
14:36:04Collections: theory Collections.GenCF_Impl_Chapter
14:36:04Collections: theory Collections.GenCF_Chapter
14:36:04Collections: theory Collections.GenCF_Intf_Chapter
14:36:04Collections: theory Collections.Intf_Comp
14:36:04Collections: theory Collections.Impl_Array_Stack
14:36:04Collections: theory HOL-Library.Product_Lexorder
14:36:04Collections: theory Collections.Array_Iterator
14:36:04Collections: theory Collections.Intf_Set
14:36:04Collections: theory Collections.Intf_Map
14:36:04Collections: theory Collections.Intf_Hash
14:36:05Collections: theory Collections.Gen_Set
14:36:05Collections: theory Collections.Impl_Cfun_Set
14:36:05Collections: theory Collections.Gen_Map
14:36:05Collections: theory Collections.Impl_List_Set
14:36:07Collections: theory Collections.Gen_Comp
14:36:07Collections: theory Collections.Impl_Array_Map
14:36:07Collections: theory Collections.Impl_List_Map
14:36:07Collections: theory Collections.Impl_RBT_Map
14:36:07Collections: theory Collections.Gen_Map2Set
14:36:08Collections: theory Collections.Impl_Array_Hash_Map
14:36:22Collections: theory Collections.Impl_Bit_Set
14:36:22Collections: theory Collections.Gen_Hash
14:36:22Collections: theory Native_Word.Uint
14:36:23Collections: theory Collections.Impl_Uv_Set
14:36:39Collections: theory Collections.GenCF
14:36:43Collections: theory Collections.ICF_Chapter
14:36:43Collections: theory Collections.ICF_Gen_Algo_Chapter
14:36:43Collections: theory Collections.ICF_Impl_Chapter
14:36:43Collections: theory Collections.ICF_Spec_Chapter
14:36:43Collections: theory Trie.Trie
14:36:43Collections: theory Collections.AnnotatedListSpec
14:36:43Collections: theory Collections.ListSpec
14:36:43Collections: theory HOL-Library.RBT
14:36:43Collections: theory Collections.PrioSpec
14:36:43Collections: theory Collections.PrioUniqueSpec
14:36:43Collections: theory Collections.SetSpec
14:36:46Collections: theory Collections.BinoPrioImpl
14:36:46Collections: theory Collections.SkewPrioImpl
14:36:47Collections: theory Collections.ListGA
14:36:48Collections: theory Collections.Trie_Impl
14:36:48Collections: theory Collections.FTAnnotatedListImpl
14:36:48Collections: theory Collections.PrioByAnnotatedList
14:36:48Collections: theory Collections.Fifo
14:36:48Collections: theory Collections.PrioUniqueByAnnotatedList
14:36:48Collections: theory Collections.Trie2
14:36:50Collections: theory Collections.Algos
14:36:50Collections: theory Collections.SetIndex
14:36:50Collections: theory Collections.SetIteratorCollectionsGA
14:36:51Collections: theory Collections.MapGA
14:36:51Collections: theory Collections.SetGA
14:36:54Collections: theory Collections.FTPrioImpl
14:36:54Collections: theory Collections.FTPrioUniqueImpl
14:36:57Collections: theory Collections.ArrayMapImpl
14:36:57Collections: theory Collections.ListMapImpl
14:36:57Collections: theory Collections.ListMapImpl_Invar
14:36:57Collections: theory Collections.TrieMapImpl
14:36:59Collections: theory Collections.RBTMapImpl
14:37:00Collections: theory Collections.ListSetImpl
14:37:00Collections: theory Collections.ListSetImpl_Invar
14:37:00Collections: theory Collections.ListSetImpl_NotDist
14:37:02Collections: theory Collections.ListSetImpl_Sorted
14:37:02Collections: theory Collections.SetByMap
14:37:03Collections: theory Collections.ArrayHashMap_Impl
14:37:05Collections: theory Collections.ArraySetImpl
14:37:05Collections: theory Collections.TrieSetImpl
14:37:06Collections: theory Collections.RBTSetImpl
14:37:06Collections: theory Collections.HashMap_Impl
14:37:07Collections: theory Collections.ArrayHashMap
14:37:08Collections: theory Collections.HashMap
14:37:13Collections: theory Collections.ArrayHashSet
14:37:14Collections: theory Collections.HashSet
14:37:14Collections: theory Collections.MapStdImpl
14:37:20Collections: theory Collections.SetStdImpl
14:37:25Collections: theory Collections.ICF_Impl
14:37:29Collections: theory Collections.ICF_Refine_Monadic
14:37:30Collections: theory Collections.ICF_Autoref
14:37:34Collections: theory Collections.Collections_Entrypoints_Chapter
14:37:34Collections: theory Collections.ICF_Entrypoints_Chapter
14:37:34Collections: theory Collections.Userguides_Chapter
14:37:34Collections: theory Collections.Collections
14:37:34Collections: theory Collections.Refine_Dflt
14:37:34Collections: theory Collections.CollectionsV1
14:37:34Collections: theory Collections.ICF_Userguide
14:37:34Collections: theory Collections.Refine_Dflt_Only_ICF
14:37:34Collections: theory Collections.Refine_Dflt_ICF
14:37:35Collections: theory Collections.Refine_Monadic_Userguide
14:39:02Preparing Collections/document ...
14:39:21Finished Collections/document (0:00:19 elapsed time)
14:39:21Preparing Collections/outline ...
14:39:34Finished Collections/outline (0:00:12 elapsed time)
14:39:34Preparing Collections/userguide ...
14:39:37Finished Collections/userguide (0:00:03 elapsed time)
14:39:37Timing Collections (8 threads, 229.325s elapsed time, 1050.953s cpu time, 96.378s GC time, factor 4.58)
14:39:37Finished Collections (0:04:48 elapsed time, 0:20:01 cpu time, factor 4.17)
14:39:38Building Core_SC_DOM (on hpcisabelle/1) ...
14:39:53Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
14:39:53Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
14:39:53Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
14:39:54Core_SC_DOM: theory Core_SC_DOM.Ref
14:39:54Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
14:39:54Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
14:39:54Core_SC_DOM: theory Core_SC_DOM.BaseClass
14:39:55Core_SC_DOM: theory Core_SC_DOM.NodePointer
14:39:55Core_SC_DOM: theory Core_SC_DOM.ObjectClass
14:39:56Core_SC_DOM: theory Core_SC_DOM.ElementPointer
14:39:56Core_SC_DOM: theory Core_SC_DOM.NodeClass
14:39:57Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
14:39:57Core_SC_DOM: theory Core_SC_DOM.BaseMonad
14:39:58Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
14:39:59Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
14:39:59Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
14:40:00Core_SC_DOM: theory Core_SC_DOM.ElementClass
14:40:00Core_SC_DOM: theory Core_SC_DOM.NodeMonad
14:40:02Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
14:40:02Core_SC_DOM: theory Core_SC_DOM.ElementMonad
14:40:03Core_SC_DOM: theory Core_SC_DOM.DocumentClass
14:40:03Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
14:40:05Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
14:40:07Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
14:40:28Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
14:40:48Core_SC_DOM: theory Core_SC_DOM.Core_DOM
14:40:48Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
14:40:56Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
14:40:56Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
14:40:56Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
14:40:56Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
14:40:59Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
14:43:16Preparing Core_SC_DOM/document ...
14:43:32Finished Core_SC_DOM/document (0:00:16 elapsed time)
14:43:32Preparing Core_SC_DOM/outline ...
14:43:44Finished Core_SC_DOM/outline (0:00:11 elapsed time)
14:43:44Timing Core_SC_DOM (8 threads, 160.013s elapsed time, 868.027s cpu time, 55.945s GC time, factor 5.42)
14:43:44Finished Core_SC_DOM (0:03:37 elapsed time, 0:16:55 cpu time, factor 4.67)
14:43:44Building Jordan_Normal_Form (on hpcisabelle/2) ...
14:43:46Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
14:43:46Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
14:43:54Jordan_Normal_Form: theory Deriving.Derive_Manager
14:43:54Jordan_Normal_Form: theory Deriving.Comparator
14:43:54Jordan_Normal_Form: theory Containers.List_Fusion
14:43:54Jordan_Normal_Form: theory Containers.Extend_Partial_Order
14:43:54Jordan_Normal_Form: theory Containers.Equal
14:43:54Jordan_Normal_Form: theory Deriving.Generator_Aux
14:43:54Jordan_Normal_Form: theory Containers.Containers_Auxiliary
14:43:54Jordan_Normal_Form: theory Abstract-Rewriting.Seq
14:43:54Jordan_Normal_Form: theory Containers.Closure_Set
14:43:54Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
14:43:54Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
14:43:54Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
14:43:55Jordan_Normal_Form: theory Deriving.Equality_Generator
14:43:55Jordan_Normal_Form: theory Containers.Containers_Generator
14:43:55Jordan_Normal_Form: theory Regular-Sets.Regular_Set
14:43:55Jordan_Normal_Form: theory Deriving.Equality_Instances
14:43:55Jordan_Normal_Form: theory Show.Show
14:43:55Jordan_Normal_Form: theory Containers.Collection_Enum
14:43:55Jordan_Normal_Form: theory Deriving.Compare
14:43:56Jordan_Normal_Form: theory Deriving.Comparator_Generator
14:43:56Jordan_Normal_Form: theory Containers.Lexicographic_Order
14:43:56Jordan_Normal_Form: theory Containers.Collection_Eq
14:43:57Jordan_Normal_Form: theory Containers.RBT_ext
14:43:57Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl
14:43:57Jordan_Normal_Form: theory Containers.Set_Linorder
14:43:57Jordan_Normal_Form: theory Deriving.Compare_Generator
14:43:57Jordan_Normal_Form: theory Containers.DList_Set
14:43:57Jordan_Normal_Form: theory Deriving.Compare_Instances
14:43:58Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
14:43:58Jordan_Normal_Form: theory Show.Show_Instances
14:43:59Jordan_Normal_Form: theory Regular-Sets.Regular_Exp
14:43:59Jordan_Normal_Form: theory Show.Shows_Literal
14:43:59Jordan_Normal_Form: theory VectorSpace.FunctionLemmas
14:44:00Jordan_Normal_Form: theory VectorSpace.RingModuleFacts
14:44:00Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
14:44:00Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
14:44:00Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
14:44:00Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
14:44:01Jordan_Normal_Form: theory VectorSpace.MonoidSums
14:44:01Jordan_Normal_Form: theory VectorSpace.LinearCombinations
14:44:03Jordan_Normal_Form: theory Regular-Sets.NDerivative
14:44:03Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation
14:44:08Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
14:44:08Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
14:44:08Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
14:44:08Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
14:44:09Jordan_Normal_Form: theory Jordan_Normal_Form.Shows_Literal_Matrix
14:44:09Jordan_Normal_Form: theory VectorSpace.SumSpaces
14:44:10Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking
14:44:10Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
14:44:10Jordan_Normal_Form: theory Regular-Sets.Regexp_Method
14:44:10Jordan_Normal_Form: theory VectorSpace.VectorSpace
14:44:11Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
14:44:11Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
14:44:11Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting
14:44:11Jordan_Normal_Form: theory Containers.Collection_Order
14:44:14Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders
14:44:14Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
14:44:14Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
14:44:14Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
14:44:14Jordan_Normal_Form: theory Containers.RBT_Mapping2
14:44:15Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
14:44:16Jordan_Normal_Form: theory Containers.RBT_Set2
14:44:17Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier
14:44:17Jordan_Normal_Form: theory Matrix.Ordered_Semiring
14:44:17Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
14:44:18Jordan_Normal_Form: theory Containers.Set_Impl
14:44:18Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
14:44:21Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
14:44:21Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
14:44:21Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
14:44:26Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
14:44:34Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
14:44:34Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
14:44:36Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
14:44:38Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
14:44:40Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
14:44:41Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
14:44:44Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
14:44:46Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
14:44:46Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
14:48:17Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
14:48:17Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
14:48:17Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
14:48:20Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
14:48:28Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
14:49:13Preparing Jordan_Normal_Form/document ...
14:49:39Finished Jordan_Normal_Form/document (0:00:26 elapsed time)
14:49:39Preparing Jordan_Normal_Form/outline ...
14:49:50Finished Jordan_Normal_Form/outline (0:00:10 elapsed time)
14:49:51Timing Jordan_Normal_Form (8 threads, 283.106s elapsed time, 1738.963s cpu time, 68.529s GC time, factor 6.14)
14:49:51Finished Jordan_Normal_Form (0:05:25 elapsed time, 0:30:35 cpu time, factor 5.65)
14:49:51Building HOL-Number_Theory (on hpcisabelle/3) ...
14:49:53HOL-Number_Theory: theory HOL-Number_Theory.Cong
14:49:53HOL-Number_Theory: theory HOL-Algebra.Congruence
14:49:53HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
14:49:53HOL-Number_Theory: theory HOL-Number_Theory.Fib
14:49:53HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
14:49:54HOL-Number_Theory: theory HOL-Algebra.Order
14:49:55HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
14:49:55HOL-Number_Theory: theory HOL-Number_Theory.Totient
14:49:56HOL-Number_Theory: theory HOL-Algebra.Lattice
14:49:57HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
14:49:58HOL-Number_Theory: theory HOL-Algebra.Group
14:50:01HOL-Number_Theory: theory HOL-Algebra.Coset
14:50:02HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
14:50:02HOL-Number_Theory: theory HOL-Algebra.Ring
14:50:04HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
14:50:05HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
14:50:07HOL-Number_Theory: theory HOL-Algebra.AbelCoset
14:50:07HOL-Number_Theory: theory HOL-Algebra.Module
14:50:12HOL-Number_Theory: theory HOL-Algebra.Ideal
14:50:15HOL-Number_Theory: theory HOL-Algebra.RingHom
14:50:16HOL-Number_Theory: theory HOL-Algebra.UnivPoly
14:50:30HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
14:50:35HOL-Number_Theory: theory HOL-Number_Theory.Residues
14:50:38HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
14:50:38HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
14:50:38HOL-Number_Theory: theory HOL-Number_Theory.Gauss
14:50:39HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
14:50:39HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
14:50:39HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
14:51:09Preparing HOL-Number_Theory/document ...
14:51:15Finished HOL-Number_Theory/document (0:00:05 elapsed time)
14:51:15Preparing HOL-Number_Theory/outline ...
14:51:18Finished HOL-Number_Theory/outline (0:00:02 elapsed time)
14:51:18Timing HOL-Number_Theory (8 threads, 59.103s elapsed time, 336.150s cpu time, 10.212s GC time, factor 5.69)
14:51:18Finished HOL-Number_Theory (0:01:16 elapsed time, 0:06:11 cpu time, factor 4.83)
14:51:18Building HOL-Probability (on hpcisabelle/4) ...
14:51:21HOL-Probability: theory HOL-Library.AList
14:51:21HOL-Probability: theory HOL-Library.Adhoc_Overloading
14:51:21HOL-Probability: theory HOL-Library.Conditional_Parametricity
14:51:21HOL-Probability: theory HOL-Library.Complete_Partial_Order2
14:51:21HOL-Probability: theory HOL-Library.Stream
14:51:21HOL-Probability: theory HOL-Library.Sublist
14:51:21HOL-Probability: theory HOL-Library.Tree
14:51:21HOL-Probability: theory HOL-Library.Rewrite
14:51:21HOL-Probability: theory HOL-Library.Monad_Syntax
14:51:21HOL-Probability: theory HOL-Library.FSet
14:51:22HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
14:51:22HOL-Probability: theory HOL-Library.Diagonal_Subsequence
14:51:22HOL-Probability: theory HOL-Probability.Discrete_Topology
14:51:23HOL-Probability: theory HOL-Probability.Essential_Supremum
14:51:23HOL-Probability: theory HOL-Probability.Probability_Measure
14:51:24HOL-Probability: theory HOL-Probability.Stopping_Time
14:51:24HOL-Probability: theory HOL-Library.Mapping
14:51:25HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
14:51:26HOL-Probability: theory HOL-Probability.Tree_Space
14:51:26HOL-Probability: theory HOL-Library.AList_Mapping
14:51:26HOL-Probability: theory HOL-Probability.Conditional_Expectation
14:51:26HOL-Probability: theory HOL-Probability.Distribution_Functions
14:51:26HOL-Probability: theory HOL-Probability.Giry_Monad
14:51:27HOL-Probability: theory HOL-Probability.Weak_Convergence
14:51:28HOL-Probability: theory HOL-Probability.Helly_Selection
14:51:28HOL-Probability: theory HOL-Library.Finite_Map
14:51:29HOL-Probability: theory HOL-Probability.Probability_Mass_Function
14:51:29HOL-Probability: theory HOL-Probability.Projective_Family
14:51:30HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
14:51:31HOL-Probability: theory HOL-Probability.Independent_Family
14:51:31HOL-Probability: theory HOL-Probability.Stream_Space
14:51:32HOL-Probability: theory HOL-Probability.PMF_Impl
14:51:32HOL-Probability: theory HOL-Probability.Random_Permutations
14:51:32HOL-Probability: theory HOL-Probability.SPMF
14:51:32HOL-Probability: theory HOL-Probability.Convolution
14:51:32HOL-Probability: theory HOL-Probability.Information
14:51:32HOL-Probability: theory HOL-Probability.Product_PMF
14:51:33HOL-Probability: theory HOL-Probability.Hoeffding
14:51:35HOL-Probability: theory HOL-Probability.Distributions
14:51:37HOL-Probability: theory HOL-Probability.Characteristic_Functions
14:51:37HOL-Probability: theory HOL-Probability.Sinc_Integral
14:51:38HOL-Probability: theory HOL-Probability.Levy
14:51:39HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
14:51:42HOL-Probability: theory HOL-Probability.Fin_Map
14:51:44HOL-Probability: theory HOL-Probability.Projective_Limit
14:51:47HOL-Probability: theory HOL-Probability.Probability
14:53:01Preparing HOL-Probability/document ...
14:53:22Finished HOL-Probability/document (0:00:21 elapsed time)
14:53:22Preparing HOL-Probability/outline ...
14:53:30Finished HOL-Probability/outline (0:00:08 elapsed time)
14:53:30Timing HOL-Probability (8 threads, 74.727s elapsed time, 503.813s cpu time, 13.047s GC time, factor 6.74)
14:53:30Finished HOL-Probability (0:01:39 elapsed time, 0:09:16 cpu time, factor 5.60)
14:53:30Building Abstract-Rewriting (on hpcisabelle/5) ...
14:53:35Abstract-Rewriting: theory Abstract-Rewriting.Seq
14:53:35Abstract-Rewriting: theory Regular-Sets.Regular_Set
14:53:39Abstract-Rewriting: theory Regular-Sets.Regular_Exp
14:53:42Abstract-Rewriting: theory Regular-Sets.NDerivative
14:53:42Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
14:53:46Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
14:53:46Abstract-Rewriting: theory Regular-Sets.Regexp_Method
14:53:47Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
14:53:49Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
14:53:49Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
14:53:53Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
14:54:11Preparing Abstract-Rewriting/document ...
14:54:19Finished Abstract-Rewriting/document (0:00:08 elapsed time)
14:54:19Preparing Abstract-Rewriting/outline ...
14:54:23Finished Abstract-Rewriting/outline (0:00:04 elapsed time)
14:54:23Timing Abstract-Rewriting (8 threads, 25.164s elapsed time, 86.849s cpu time, 2.506s GC time, factor 3.45)
14:54:23Finished Abstract-Rewriting (0:00:39 elapsed time, 0:01:53 cpu time, factor 2.88)
14:54:24Running Crypto_Standards (on hpcisabelle/6) ...
14:54:26Crypto_Standards: theory Crypto_Standards.More_Bit_Operations_Nat
14:54:26Crypto_Standards: theory HOL-Decision_Procs.Conversions
14:54:26Crypto_Standards: theory HOL-Decision_Procs.Algebra_Aux
14:54:26Crypto_Standards: theory Crypto_Standards.Words
14:54:28Crypto_Standards: theory Crypto_Standards.More_Residues
14:54:28Crypto_Standards: theory HOL-Decision_Procs.Commutative_Ring
14:54:30Crypto_Standards: theory Crypto_Standards.FIPS180_4
14:54:30Crypto_Standards: theory Crypto_Standards.PKCS1v2_2
14:54:36Crypto_Standards: theory Crypto_Standards.FIPS180_4_Test_Vectors
14:54:39Crypto_Standards: theory Crypto_Standards.Efficient_Mod_Exp
14:54:39Crypto_Standards: theory HOL-Decision_Procs.Reflective_Field
14:54:40Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Interpretations
14:54:43Crypto_Standards: theory Crypto_Standards.FIPS198_1
14:54:43Crypto_Standards: theory Crypto_Standards.FIPS198_1_Test_Vectors
14:54:45Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Test_Vectors
14:54:52Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Locale
14:54:56Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Test
14:55:02Crypto_Standards: theory Crypto_Standards.EC_Common
14:55:13Crypto_Standards: theory Crypto_Standards.SEC1v2_0
14:55:30Crypto_Standards: theory Crypto_Standards.Crypto_Standards
14:55:30Crypto_Standards: theory Crypto_Standards.Efficient_SEC1
14:55:38Crypto_Standards: theory Crypto_Standards.FIPS186_4_Curves
14:56:11Crypto_Standards: theory Crypto_Standards.SEC1v2_0_Test_Vectors
15:01:49Crypto_Standards: theory Crypto_Standards.Test_Vectors
15:08:53Preparing Crypto_Standards/document ...
15:08:57Finished Crypto_Standards/document (0:00:04 elapsed time)
15:08:57Preparing Crypto_Standards/outline ...
15:08:59Finished Crypto_Standards/outline (0:00:02 elapsed time)
15:08:59Timing Crypto_Standards (8 threads, 862.299s elapsed time, 6445.010s cpu time, 587.288s GC time, factor 7.47)
15:08:59Finished Crypto_Standards (0:14:26 elapsed time, 1:47:35 cpu time, factor 7.45)
15:09:00Building First_Order_Terms (on hpcisabelle/7) ...
15:09:02First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
15:09:02First_Order_Terms: theory Fresh_Identifiers.Fresh
15:09:02First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
15:09:02First_Order_Terms: theory First_Order_Terms.Renaming2
15:09:03First_Order_Terms: theory First_Order_Terms.Renaming2_String
15:09:03First_Order_Terms: theory First_Order_Terms.Fun_More
15:09:03First_Order_Terms: theory First_Order_Terms.Option_Monad
15:09:03First_Order_Terms: theory First_Order_Terms.Seq_More
15:09:04First_Order_Terms: theory First_Order_Terms.Term
15:09:06First_Order_Terms: theory First_Order_Terms.Unifiers
15:09:06First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
15:09:06First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
15:09:06First_Order_Terms: theory First_Order_Terms.Subsumption
15:09:07First_Order_Terms: theory First_Order_Terms.Abstract_Matching
15:09:07First_Order_Terms: theory First_Order_Terms.Abstract_Unification
15:09:08First_Order_Terms: theory First_Order_Terms.Unification
15:09:09First_Order_Terms: theory First_Order_Terms.Matching
15:09:09First_Order_Terms: theory First_Order_Terms.Unification_String
15:09:12First_Order_Terms: theory Deriving.Derive_Manager
15:09:12First_Order_Terms: theory Matrix.Utility
15:09:12First_Order_Terms: theory Deriving.Generator_Aux
15:09:12First_Order_Terms: theory Show.Show
15:09:12First_Order_Terms: theory Polynomial_Factorization.Missing_List
15:09:14First_Order_Terms: theory Show.Show_Instances
15:09:15First_Order_Terms: theory Show.Shows_Literal
15:09:16First_Order_Terms: theory First_Order_Terms.Position
15:09:18First_Order_Terms: theory First_Order_Terms.Term_More
15:09:45Preparing First_Order_Terms/document ...
15:09:55Finished First_Order_Terms/document (0:00:10 elapsed time)
15:09:55Preparing First_Order_Terms/outline ...
15:10:01Finished First_Order_Terms/outline (0:00:05 elapsed time)
15:10:01Timing First_Order_Terms (8 threads, 26.450s elapsed time, 116.909s cpu time, 3.947s GC time, factor 4.42)
15:10:01Finished First_Order_Terms (0:00:43 elapsed time, 0:02:31 cpu time, factor 3.44)
15:10:01Building Expander_Graphs (on hpcisabelle/0) ...
15:10:06Expander_Graphs: theory HOL-Eisbach.Eisbach
15:10:06Expander_Graphs: theory Digit_Expansions.Bits_Digits
15:10:06Expander_Graphs: theory Graph_Theory.Rtrancl_On
15:10:06Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
15:10:06Expander_Graphs: theory HOL-Decision_Procs.Dense_Linear_Order
15:10:06Expander_Graphs: theory HOL-Library.Code_Abstract_Nat
15:10:06Expander_Graphs: theory HOL-Library.Code_Target_Int
15:10:06Expander_Graphs: theory HOL-Algebra.Congruence
15:10:06Expander_Graphs: theory HOL-Library.Code_Target_Nat
15:10:07Expander_Graphs: theory Finite_Fields.Finite_Fields_More_Bijections
15:10:07Expander_Graphs: theory HOL-Combinatorics.List_Permutation
15:10:07Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
15:10:07Expander_Graphs: theory HOL-Library.Code_Target_Numeral
15:10:07Expander_Graphs: theory HOL-Library.Function_Algebras
15:10:07Expander_Graphs: theory Abstract-Rewriting.Seq
15:10:07Expander_Graphs: theory HOL-Library.More_List
15:10:07Expander_Graphs: theory Perron_Frobenius.Bij_Nat
15:10:07Expander_Graphs: theory HOL-Library.While_Combinator
15:10:08Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
15:10:08Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
15:10:08Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
15:10:08Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
15:10:08Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
15:10:08Expander_Graphs: theory HOL-Algebra.Order
15:10:08Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
15:10:08Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
15:10:09Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
15:10:09Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
15:10:09Expander_Graphs: theory Jordan_Normal_Form.Conjugate
15:10:09Expander_Graphs: theory HOL-Library.Lattice_Algebras
15:10:09Expander_Graphs: theory HOL-Library.Log_Nat
15:10:09Expander_Graphs: theory Graph_Theory.Stuff
15:10:09Expander_Graphs: theory HOL-Algebra.Lattice
15:10:10Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families
15:10:10Expander_Graphs: theory Graph_Theory.Digraph
15:10:10Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
15:10:10Expander_Graphs: theory Ergodic_Theory.SG_Library_Complement
15:10:11Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
15:10:11Expander_Graphs: theory HOL-Algebra.Complete_Lattice
15:10:11Expander_Graphs: theory Matrix.Utility
15:10:12Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
15:10:12Expander_Graphs: theory Lp.Functional_Spaces
15:10:12Expander_Graphs: theory Graph_Theory.Arc_Walk
15:10:12Expander_Graphs: theory HOL-Algebra.Group
15:10:13Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
15:10:13Expander_Graphs: theory Regular-Sets.Regular_Set
15:10:14Expander_Graphs: theory Graph_Theory.Pair_Digraph
15:10:14Expander_Graphs: theory VectorSpace.FunctionLemmas
15:10:14Expander_Graphs: theory HOL-Algebra.Coset
15:10:15Expander_Graphs: theory HOL-Algebra.FiniteProduct
15:10:15Expander_Graphs: theory Lp.Lp
15:10:15Expander_Graphs: theory HOL-Algebra.Ring
15:10:16Expander_Graphs: theory HOL-Library.Interval
15:10:17Expander_Graphs: theory HOL-Library.Float
15:10:17Expander_Graphs: theory HOL-Algebra.Generated_Groups
15:10:17Expander_Graphs: theory HOL-Algebra.Divisibility
15:10:19Expander_Graphs: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
15:10:20Expander_Graphs: theory HOL-Algebra.Elementary_Groups
15:10:21Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
15:10:21Expander_Graphs: theory Regular-Sets.Regular_Exp
15:10:21Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
15:10:21Expander_Graphs: theory HOL-Library.Interval_Float
15:10:22Expander_Graphs: theory HOL-Algebra.AbelCoset
15:10:22Expander_Graphs: theory HOL-Algebra.Module
15:10:22Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
15:10:22Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
15:10:22Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
15:10:22Expander_Graphs: theory Graph_Theory.Digraph_Component
15:10:23Expander_Graphs: theory Universal_Hash_Families.Pseudorandom_Objects
15:10:23Expander_Graphs: theory HOL-Decision_Procs.Approximation_Bounds
15:10:24Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
15:10:24Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
15:10:24Expander_Graphs: theory VectorSpace.RingModuleFacts
15:10:25Expander_Graphs: theory Regular-Sets.NDerivative
15:10:25Expander_Graphs: theory Regular-Sets.Relation_Interpretation
15:10:25Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
15:10:26Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
15:10:26Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
15:10:26Expander_Graphs: theory VectorSpace.MonoidSums
15:10:26Expander_Graphs: theory HOL-Algebra.Ideal
15:10:26Expander_Graphs: theory VectorSpace.LinearCombinations
15:10:27Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
15:10:28Expander_Graphs: theory Jordan_Normal_Form.Matrix
15:10:29Expander_Graphs: theory HOL-Decision_Procs.Approximation
15:10:30Expander_Graphs: theory HOL-Algebra.RingHom
15:10:30Expander_Graphs: theory Regular-Sets.Equivalence_Checking
15:10:30Expander_Graphs: theory Regular-Sets.Regexp_Method
15:10:31Expander_Graphs: theory HOL-Algebra.QuotRing
15:10:31Expander_Graphs: theory HOL-Algebra.UnivPoly
15:10:31Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
15:10:34Expander_Graphs: theory VectorSpace.SumSpaces
15:10:34Expander_Graphs: theory Abstract-Rewriting.SN_Orders
15:10:34Expander_Graphs: theory VectorSpace.VectorSpace
15:10:35Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
15:10:35Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
15:10:37Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
15:10:37Expander_Graphs: theory Matrix.Ordered_Semiring
15:10:37Expander_Graphs: theory Jordan_Normal_Form.Determinant
15:10:39Expander_Graphs: theory Matrix.Matrix_Legacy
15:10:40Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
15:10:41Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
15:10:41Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
15:10:42Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
15:10:43Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
15:10:43Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
15:10:43Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
15:10:45Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
15:10:45Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
15:10:46Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
15:10:47Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
15:10:48Expander_Graphs: theory HOL-Algebra.Multiplicative_Group
15:10:52Expander_Graphs: theory HOL-Algebra.Ring_Divisibility
15:10:52Expander_Graphs: theory HOL-Algebra.Subrings
15:10:56Expander_Graphs: theory HOL-Algebra.Embedded_Algebras
15:10:59Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
15:11:01Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
15:11:02Expander_Graphs: theory HOL-Algebra.Polynomials
15:11:06Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
15:11:12Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
15:11:12Expander_Graphs: theory QHLProver.Complex_Matrix
15:11:12Expander_Graphs: theory Perron_Frobenius.HMA_Connect
15:11:22Expander_Graphs: theory QHLProver.Gates
15:11:22Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
15:11:26Expander_Graphs: theory HOL-Algebra.Polynomial_Divisibility
15:11:29Expander_Graphs: theory Projective_Measurements.Projective_Measurements
15:11:30Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
15:11:32Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
15:12:08Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
15:12:08Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
15:12:13Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
15:12:16Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
15:12:20Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
15:12:20Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
15:12:21Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
15:12:24Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
15:12:30Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
15:12:30Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
15:12:34Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
15:12:37Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
15:12:44Expander_Graphs: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
15:20:57Preparing Expander_Graphs/document ...
15:21:09Finished Expander_Graphs/document (0:00:12 elapsed time)
15:21:09Preparing Expander_Graphs/outline ...
15:21:14Finished Expander_Graphs/outline (0:00:04 elapsed time)
15:21:14Timing Expander_Graphs (8 threads, 584.083s elapsed time, 2703.982s cpu time, 202.441s GC time, factor 4.63)
15:21:14Finished Expander_Graphs (0:10:46 elapsed time, 0:47:30 cpu time, factor 4.41)
15:21:15Building Stateful_Protocol_Composition_and_Typing (on hpcisabelle/1) ...
15:21:19Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
15:21:21Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
15:21:23Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
15:21:26Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
15:21:28Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
15:21:38Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
15:21:38Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
15:21:39Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
15:21:40Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
15:21:48Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
15:21:48Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
15:21:53Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
15:21:57Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
15:21:58Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
15:22:17Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
15:22:44Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
15:23:00Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
15:26:01Preparing Stateful_Protocol_Composition_and_Typing/document ...
15:26:39Finished Stateful_Protocol_Composition_and_Typing/document (0:00:38 elapsed time)
15:26:39Preparing Stateful_Protocol_Composition_and_Typing/outline ...
15:26:55Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:16 elapsed time)
15:26:55Timing Stateful_Protocol_Composition_and_Typing (8 threads, 236.464s elapsed time, 1391.623s cpu time, 50.399s GC time, factor 5.89)
15:26:55Finished Stateful_Protocol_Composition_and_Typing (0:04:42 elapsed time, 0:25:04 cpu time, factor 5.32)
15:26:55Building Shadow_SC_DOM (on hpcisabelle/2) ...
15:27:35Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
15:27:37Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
15:27:40Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
15:29:00Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
15:29:12Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
15:29:12Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
15:29:13Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
15:29:13Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
15:29:14Shadow_SC_DOM: theory Shadow_SC_DOM.slots
15:29:14Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
15:29:22Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
15:35:34Preparing Shadow_SC_DOM/document ...
15:35:50Finished Shadow_SC_DOM/document (0:00:16 elapsed time)
15:35:50Preparing Shadow_SC_DOM/outline ...
15:36:00Finished Shadow_SC_DOM/outline (0:00:10 elapsed time)
15:36:01Timing Shadow_SC_DOM (8 threads, 427.342s elapsed time, 2610.229s cpu time, 174.638s GC time, factor 6.11)
15:36:01Finished Shadow_SC_DOM (0:08:37 elapsed time, 0:47:23 cpu time, factor 5.49)
15:36:01Building CAVA_Base (on hpcisabelle/3) ...
15:36:03CAVA_Base: theory Deriving.Comparator
15:36:03CAVA_Base: theory CAVA_Base.Statistics
15:36:03CAVA_Base: theory CAVA_Base.Lexord_List
15:36:03CAVA_Base: theory Deriving.Generator_Aux
15:36:03CAVA_Base: theory Deriving.Derive_Manager
15:36:03CAVA_Base: theory HOL-Library.Char_ord
15:36:03CAVA_Base: theory HOL-Library.Old_Datatype
15:36:03CAVA_Base: theory HOL-Library.Nat_Bijection
15:36:03CAVA_Base: theory CAVA_Base.Code_String
15:36:04CAVA_Base: theory CAVA_Base.CAVA_Code_Target
15:36:04CAVA_Base: theory CAVA_Base.CAVA_Base
15:36:04CAVA_Base: theory Deriving.Equality_Generator
15:36:04CAVA_Base: theory Deriving.Hash_Generator
15:36:04CAVA_Base: theory HOL-Library.Countable
15:36:05CAVA_Base: theory Deriving.Equality_Instances
15:36:05CAVA_Base: theory Deriving.Hash_Instances
15:36:05CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base
15:36:05CAVA_Base: theory Deriving.Compare
15:36:05CAVA_Base: theory Deriving.Comparator_Generator
15:36:06CAVA_Base: theory Deriving.Compare_Generator
15:36:06CAVA_Base: theory Deriving.Countable_Generator
15:36:07CAVA_Base: theory Deriving.Compare_Instances
15:36:07CAVA_Base: theory Deriving.Derive
15:36:22Timing CAVA_Base (8 threads, 6.034s elapsed time, 24.919s cpu time, 0.566s GC time, factor 4.13)
15:36:22Finished CAVA_Base (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.50)
15:36:22Building CAVA_Automata (on hpcisabelle/4) ...
15:36:25CAVA_Automata: theory CAVA_Automata.Step_Conv
15:36:25CAVA_Automata: theory HOL-Library.Omega_Words_Fun
15:36:26CAVA_Automata: theory CAVA_Automata.Digraph_Basic
15:36:26CAVA_Automata: theory CAVA_Automata.Digraph
15:36:28CAVA_Automata: theory CAVA_Automata.Digraph_Impl
15:36:28CAVA_Automata: theory CAVA_Automata.Automata
15:36:35CAVA_Automata: theory CAVA_Automata.Lasso
15:36:35CAVA_Automata: theory CAVA_Automata.Simulation
15:36:36CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
15:36:50CAVA_Automata: theory CAVA_Automata.Automata_Impl
15:37:32CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
15:37:48Preparing CAVA_Automata/document ...
15:37:52Finished CAVA_Automata/document (0:00:04 elapsed time)
15:37:52Preparing CAVA_Automata/outline ...
15:37:55Finished CAVA_Automata/outline (0:00:03 elapsed time)
15:37:55Timing CAVA_Automata (8 threads, 68.275s elapsed time, 122.945s cpu time, 4.488s GC time, factor 1.80)
15:37:55Finished CAVA_Automata (0:01:24 elapsed time, 0:02:35 cpu time, factor 1.83)
15:37:56Running Cook_Levin (on hpcisabelle/5) ...
15:37:59Cook_Levin: theory HOL-Eisbach.Eisbach
15:37:59Cook_Levin: theory Cook_Levin.Basics
15:38:01Cook_Levin: theory Cook_Levin.Combinations
15:38:03Cook_Levin: theory Cook_Levin.Elementary
15:38:05Cook_Levin: theory Cook_Levin.Composing
15:38:05Cook_Levin: theory Cook_Levin.Memorizing
15:38:06Cook_Levin: theory Cook_Levin.Arithmetic
15:38:06Cook_Levin: theory Cook_Levin.Oblivious
15:38:07Cook_Levin: theory Cook_Levin.Oblivious_Polynomial
15:38:10Cook_Levin: theory Cook_Levin.Lists_Lists
15:38:13Cook_Levin: theory Cook_Levin.Two_Four_Symbols
15:38:14Cook_Levin: theory Cook_Levin.Symbol_Ops
15:38:16Cook_Levin: theory Cook_Levin.Wellformed
15:38:16Cook_Levin: theory Cook_Levin.NP
15:38:16Cook_Levin: theory Cook_Levin.Oblivious_2_Tape
15:38:18Cook_Levin: theory Cook_Levin.Satisfiability
15:38:22Cook_Levin: theory Cook_Levin.Reducing
15:38:24Cook_Levin: theory Cook_Levin.Aux_TM_Reducing
15:38:28Cook_Levin: theory Cook_Levin.Sat_TM_CNF
15:38:34Cook_Levin: theory Cook_Levin.Reduction_TM
15:50:53Preparing Cook_Levin/document ...
15:52:15Finished Cook_Levin/document (0:01:21 elapsed time)
15:52:15Preparing Cook_Levin/outline ...
15:52:49Finished Cook_Levin/outline (0:00:33 elapsed time)
15:52:49Timing Cook_Levin (8 threads, 768.950s elapsed time, 3941.976s cpu time, 30.687s GC time, factor 5.13)
15:52:49Finished Cook_Levin (0:12:52 elapsed time, 1:05:50 cpu time, factor 5.11)
15:52:49Building Padic_Ints (on hpcisabelle/6) ...
15:52:52Padic_Ints: theory Padic_Ints.Function_Ring
15:52:52Padic_Ints: theory HOL-Number_Theory.Cong
15:52:52Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
15:52:52Padic_Ints: theory Padic_Ints.Extended_Int
15:52:54Padic_Ints: theory HOL-Number_Theory.Totient
15:52:55Padic_Ints: theory HOL-Number_Theory.Residues
15:52:58Padic_Ints: theory Padic_Ints.Padic_Construction
15:52:59Padic_Ints: theory Padic_Ints.Padic_Integers
15:53:02Padic_Ints: theory Padic_Ints.Cring_Poly
15:54:03Padic_Ints: theory Padic_Ints.Padic_Int_Topology
15:54:06Padic_Ints: theory Padic_Ints.Zp_Compact
15:54:44Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
15:54:48Padic_Ints: theory Padic_Ints.Hensels_Lemma
15:55:26Preparing Padic_Ints/document ...
15:55:56Finished Padic_Ints/document (0:00:29 elapsed time)
15:55:56Preparing Padic_Ints/outline ...
15:56:07Finished Padic_Ints/outline (0:00:11 elapsed time)
15:56:08Timing Padic_Ints (8 threads, 132.227s elapsed time, 554.009s cpu time, 63.810s GC time, factor 4.19)
15:56:08Finished Padic_Ints (0:02:35 elapsed time, 0:10:03 cpu time, factor 3.88)
15:56:08Building Frequency_Moments (on hpcisabelle/7) ...
15:56:13Frequency_Moments: theory HOL-Eisbach.Eisbach
15:56:13Frequency_Moments: theory Digit_Expansions.Bits_Digits
15:56:13Frequency_Moments: theory Flow_Networks.Graph
15:56:13Frequency_Moments: theory Graph_Theory.Rtrancl_On
15:56:13Frequency_Moments: theory HOL-Combinatorics.Stirling
15:56:13Frequency_Moments: theory HOL-Computational_Algebra.Fraction_Field
15:56:13Frequency_Moments: theory HOL-Computational_Algebra.Group_Closure
15:56:13Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order
15:56:14Frequency_Moments: theory HOL-Computational_Algebra.Nth_Powers
15:56:14Frequency_Moments: theory HOL-Computational_Algebra.Squarefree
15:56:14Frequency_Moments: theory HOL-Number_Theory.Cong
15:56:14Frequency_Moments: theory HOL-Library.Case_Converter
15:56:14Frequency_Moments: theory HOL-Library.Code_Abstract_Nat
15:56:15Frequency_Moments: theory HOL-Library.Code_Target_Nat
15:56:15Frequency_Moments: theory Expander_Graphs.Extra_Congruence_Method
15:56:15Frequency_Moments: theory HOL-Library.Code_Target_Int
15:56:15Frequency_Moments: theory HOL-Library.Code_Lazy
15:56:15Frequency_Moments: theory Finite_Fields.Finite_Fields_More_Bijections
15:56:16Frequency_Moments: theory HOL-Library.Code_Target_Numeral
15:56:16Frequency_Moments: theory HOL-Algebra.Congruence
15:56:16Frequency_Moments: theory Card_Partitions.Injectivity_Solver
15:56:16Frequency_Moments: theory HOL-Computational_Algebra.Normalized_Fraction
15:56:16Frequency_Moments: theory Card_Partitions.Set_Partition
15:56:16Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
15:56:17Frequency_Moments: theory HOL-Combinatorics.List_Permutation
15:56:17Frequency_Moments: theory Card_Partitions.Card_Partitions
15:56:17Frequency_Moments: theory Jordan_Normal_Form.Missing_Misc
15:56:17Frequency_Moments: theory HOL-Library.Function_Algebras
15:56:17Frequency_Moments: theory Abstract-Rewriting.Seq
15:56:17Frequency_Moments: theory HOL-Library.List_Lexorder
15:56:18Frequency_Moments: theory HOL-Library.More_List
15:56:18Frequency_Moments: theory Flow_Networks.Network
15:56:18Frequency_Moments: theory Perron_Frobenius.Bij_Nat
15:56:18Frequency_Moments: theory HOL-Library.Power_By_Squaring
15:56:18Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers
15:56:18Frequency_Moments: theory HOL-Algebra.Order
15:56:18Frequency_Moments: theory HOL-Library.Transitive_Closure_Table
15:56:18Frequency_Moments: theory HOL-Library.While_Combinator
15:56:19Frequency_Moments: theory HOL-Number_Theory.Mod_Exp
15:56:19Frequency_Moments: theory HOL-Number_Theory.Eratosthenes
15:56:20Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations
15:56:20Frequency_Moments: theory HOL-Types_To_Sets.Prerequisites
15:56:20Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
15:56:20Frequency_Moments: theory HOL-Types_To_Sets.Types_To_Sets
15:56:20Frequency_Moments: theory Polynomial_Interpolation.Missing_Unsorted
15:56:20Frequency_Moments: theory HOL-Library.Bourbaki_Witt_Fixpoint
15:56:20Frequency_Moments: theory HOL-Computational_Algebra.Polynomial
15:56:20Frequency_Moments: theory Jordan_Normal_Form.Conjugate
15:56:20Frequency_Moments: theory HOL-Types_To_Sets.Group_On_With
15:56:21Frequency_Moments: theory Perron_Frobenius.Cancel_Card_Constraint
15:56:21Frequency_Moments: theory HOL-Algebra.Lattice
15:56:21Frequency_Moments: theory HOL-Library.Going_To_Filter
15:56:21Frequency_Moments: theory Frequency_Moments.Landau_Ext
15:56:21Frequency_Moments: theory Flow_Networks.Residual_Graph
15:56:21Frequency_Moments: theory HOL-Library.Lattice_Algebras
15:56:21Frequency_Moments: theory HOL-Library.Log_Nat
15:56:21Frequency_Moments: theory Graph_Theory.Stuff
15:56:22Frequency_Moments: theory Graph_Theory.Digraph
15:56:22Frequency_Moments: theory Executable_Randomized_Algorithms.Tau_Additivity
15:56:22Frequency_Moments: theory HOL-Algebra.Complete_Lattice
15:56:22Frequency_Moments: theory HOL-Number_Theory.Fib
15:56:22Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
15:56:22Frequency_Moments: theory HOL-Number_Theory.Totient
15:56:22Frequency_Moments: theory HOL-Algebra.Group
15:56:23Frequency_Moments: theory Finite_Fields.Finite_Fields_More_PMF
15:56:23Frequency_Moments: theory HOL-Complex_Analysis.Contour_Integration
15:56:23Frequency_Moments: theory Flow_Networks.Augmenting_Flow
15:56:23Frequency_Moments: theory Flow_Networks.Augmenting_Path
15:56:23Frequency_Moments: theory Graph_Theory.Arc_Walk
15:56:24Frequency_Moments: theory Graph_Theory.Bidirected_Digraph
15:56:24Frequency_Moments: theory Flow_Networks.Ford_Fulkerson
15:56:25Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
15:56:25Frequency_Moments: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
15:56:25Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
15:56:26Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
15:56:26Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
15:56:26Frequency_Moments: theory HOL-Algebra.Coset
15:56:26Frequency_Moments: theory HOL-Algebra.FiniteProduct
15:56:26Frequency_Moments: theory MFMC_Countable.MFMC_Finite
15:56:27Frequency_Moments: theory Graph_Theory.Pair_Digraph
15:56:28Frequency_Moments: theory HOL-Complex_Analysis.Winding_Numbers
15:56:28Frequency_Moments: theory Executable_Randomized_Algorithms.Coin_Space
15:56:28Frequency_Moments: theory HOL-Algebra.Ring
15:56:28Frequency_Moments: theory MFMC_Countable.MFMC_Misc
15:56:29Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
15:56:29Frequency_Moments: theory MFMC_Countable.Matrix_For_Marginals
15:56:29Frequency_Moments: theory HOL-Algebra.Generated_Groups
15:56:30Frequency_Moments: theory HOL-Algebra.Divisibility
15:56:30Frequency_Moments: theory HOL-Library.Interval
15:56:31Frequency_Moments: theory HOL-Algebra.Elementary_Groups
15:56:31Frequency_Moments: theory HOL-Library.Float
15:56:31Frequency_Moments: theory HOL-Complex_Analysis.Conformal_Mappings
15:56:33Frequency_Moments: theory HOL-Complex_Analysis.Complex_Singularities
15:56:33Frequency_Moments: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
15:56:33Frequency_Moments: theory HOL-Algebra.AbelCoset
15:56:34Frequency_Moments: theory HOL-Algebra.Module
15:56:34Frequency_Moments: theory Jordan_Normal_Form.Missing_Ring
15:56:34Frequency_Moments: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
15:56:34Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_FPS
15:56:35Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_Factorial
15:56:35Frequency_Moments: theory HOL-Library.Code_Target_Numeral_Float
15:56:35Frequency_Moments: theory HOL-Library.Interval_Float
15:56:35Frequency_Moments: theory Graph_Theory.Digraph_Component
15:56:35Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
15:56:35Frequency_Moments: theory HOL-Computational_Algebra.Formal_Laurent_Series
15:56:36Frequency_Moments: theory HOL-Complex_Analysis.Complex_Residues
15:56:36Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
15:56:36Frequency_Moments: theory Polynomial_Interpolation.Missing_Polynomial
15:56:36Frequency_Moments: theory HOL-Complex_Analysis.Residue_Theorem
15:56:37Frequency_Moments: theory HOL-Complex_Analysis.Great_Picard
15:56:38Frequency_Moments: theory MFMC_Countable.Rel_PMF_Characterisation
15:56:38Frequency_Moments: theory Polynomial_Factorization.Order_Polynomial
15:56:38Frequency_Moments: theory Probabilistic_While.While_SPMF
15:56:39Frequency_Moments: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
15:56:39Frequency_Moments: theory HOL-Complex_Analysis.Riemann_Mapping
15:56:39Frequency_Moments: theory Median_Method.Median
15:56:39Frequency_Moments: theory HOL-Algebra.Ideal
15:56:40Frequency_Moments: theory Lp.Functional_Spaces
15:56:40Frequency_Moments: theory HOL-Computational_Algebra.Computational_Algebra
15:56:40Frequency_Moments: theory HOL-Complex_Analysis.Laurent_Convergence
15:56:40Frequency_Moments: theory Graph_Theory.Digraph_Isomorphism
15:56:40Frequency_Moments: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
15:56:40Frequency_Moments: theory Matrix.Utility
15:56:41Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom
15:56:41Frequency_Moments: theory Regular-Sets.Regular_Set
15:56:41Frequency_Moments: theory VectorSpace.FunctionLemmas
15:56:41Frequency_Moments: theory VectorSpace.RingModuleFacts
15:56:42Frequency_Moments: theory VectorSpace.MonoidSums
15:56:42Frequency_Moments: theory HOL-Algebra.RingHom
15:56:42Frequency_Moments: theory VectorSpace.LinearCombinations
15:56:42Frequency_Moments: theory HOL-Decision_Procs.Approximation
15:56:43Frequency_Moments: theory Lp.Lp
15:56:43Frequency_Moments: theory HOL-Complex_Analysis.Meromorphic
15:56:43Frequency_Moments: theory HOL-Algebra.QuotRing
15:56:44Frequency_Moments: theory HOL-Algebra.UnivPoly
15:56:44Frequency_Moments: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
15:56:44Frequency_Moments: theory Concentration_Inequalities.Bienaymes_Identity
15:56:44Frequency_Moments: theory HOL-Complex_Analysis.Weierstrass_Factorization
15:56:44Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
15:56:45Frequency_Moments: theory HOL-Complex_Analysis.Complex_Analysis
15:56:45Frequency_Moments: theory Jordan_Normal_Form.Matrix
15:56:45Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects
15:56:45Frequency_Moments: theory Expander_Graphs.Constructive_Chernoff_Bound
15:56:45Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom_Poly
15:56:45Frequency_Moments: theory HOL-Algebra.IntRing
15:56:45Frequency_Moments: theory Regular-Sets.Regular_Exp
15:56:47Frequency_Moments: theory VectorSpace.SumSpaces
15:56:47Frequency_Moments: theory VectorSpace.VectorSpace
15:56:50Frequency_Moments: theory Regular-Sets.NDerivative
15:56:50Frequency_Moments: theory Regular-Sets.Relation_Interpretation
15:56:50Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian_Misc
15:56:50Frequency_Moments: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
15:56:52Frequency_Moments: theory Jordan_Normal_Form.Column_Operations
15:56:53Frequency_Moments: theory Jordan_Normal_Form.Determinant
15:56:54Frequency_Moments: theory Regular-Sets.Equivalence_Checking
15:56:55Frequency_Moments: theory Regular-Sets.Regexp_Method
15:56:56Frequency_Moments: theory Jordan_Normal_Form.Missing_VectorSpace
15:56:56Frequency_Moments: theory Jordan_Normal_Form.Char_Poly
15:56:56Frequency_Moments: theory Abstract-Rewriting.Abstract_Rewriting
15:56:57Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form
15:56:58Frequency_Moments: theory Isabelle_Marries_Dirac.Basics
15:56:58Frequency_Moments: theory Isabelle_Marries_Dirac.Binary_Nat
15:56:58Frequency_Moments: theory Isabelle_Marries_Dirac.Quantum
15:56:58Frequency_Moments: theory Abstract-Rewriting.SN_Orders
15:56:58Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
15:56:59Frequency_Moments: theory Jordan_Normal_Form.VS_Connect
15:57:00Frequency_Moments: theory Isabelle_Marries_Dirac.Complex_Vectors
15:57:02Frequency_Moments: theory Matrix.Ordered_Semiring
15:57:03Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
15:57:03Frequency_Moments: theory HOL-Algebra.Subrings
15:57:03Frequency_Moments: theory HOL-Number_Theory.Residues
15:57:03Frequency_Moments: theory Matrix.Matrix_Legacy
15:57:05Frequency_Moments: theory Matrix_Tensor.Matrix_Tensor
15:57:07Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
15:57:07Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
15:57:07Frequency_Moments: theory HOL-Number_Theory.Pocklington
15:57:07Frequency_Moments: theory HOL-Number_Theory.Gauss
15:57:08Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
15:57:08Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
15:57:08Frequency_Moments: theory Lehmer.Lehmer
15:57:08Frequency_Moments: theory Isabelle_Marries_Dirac.Tensor
15:57:08Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
15:57:08Frequency_Moments: theory HOL-Number_Theory.Number_Theory
15:57:09Frequency_Moments: theory Isabelle_Marries_Dirac.More_Tensor
15:57:10Frequency_Moments: theory Dirichlet_Series.Dirichlet_Misc
15:57:11Frequency_Moments: theory Dirichlet_Series.Multiplicative_Function
15:57:11Frequency_Moments: theory Dirichlet_Series.Dirichlet_Product
15:57:11Frequency_Moments: theory Dirichlet_Series.Euler_Products
15:57:12Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series
15:57:16Frequency_Moments: theory Bertrands_Postulate.Bertrand
15:57:17Frequency_Moments: theory HOL-Algebra.Polynomials
15:57:18Frequency_Moments: theory Jordan_Normal_Form.Gram_Schmidt
15:57:20Frequency_Moments: theory Jordan_Normal_Form.Schur_Decomposition
15:57:21Frequency_Moments: theory Dirichlet_Series.Moebius_Mu
15:57:21Frequency_Moments: theory Dirichlet_Series.More_Totient
15:57:21Frequency_Moments: theory Dirichlet_Series.Divisor_Count
15:57:22Frequency_Moments: theory Dirichlet_Series.Liouville_Lambda
15:57:22Frequency_Moments: theory Dirichlet_Series.Arithmetic_Summatory
15:57:22Frequency_Moments: theory Dirichlet_Series.Partial_Summation
15:57:24Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series_Analysis
15:57:26Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
15:57:31Frequency_Moments: theory Jordan_Normal_Form.Spectral_Radius
15:57:31Frequency_Moments: theory QHLProver.Complex_Matrix
15:57:31Frequency_Moments: theory Perron_Frobenius.HMA_Connect
15:57:34Frequency_Moments: theory Zeta_Function.Zeta_Library
15:57:35Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
15:57:41Frequency_Moments: theory QHLProver.Gates
15:57:41Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
15:57:41Frequency_Moments: theory Projective_Measurements.Linear_Algebra_Complements
15:57:42Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm
15:57:45Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
15:57:48Frequency_Moments: theory Projective_Measurements.Projective_Measurements
15:57:51Frequency_Moments: theory Commuting_Hermitian.Spectral_Theory_Complements
15:57:52Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian
15:58:14Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
15:58:14Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
15:58:14Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
15:58:19Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
15:58:21Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
15:58:21Frequency_Moments: theory Finite_Fields.Ring_Characteristic
15:58:22Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Definition
15:58:22Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
15:58:22Frequency_Moments: theory Frequency_Moments.K_Smallest
15:58:25Frequency_Moments: theory Expander_Graphs.Expander_Graphs_TTS
15:58:26Frequency_Moments: theory Expander_Graphs.Expander_Graphs_MGG
15:58:27Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Algebra
15:58:28Frequency_Moments: theory Frequency_Moments.Probability_Ext
15:58:29Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Eigenvalues
15:58:32Frequency_Moments: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
15:58:32Frequency_Moments: theory Finite_Fields.Formal_Polynomial_Derivatives
15:58:33Frequency_Moments: theory Finite_Fields.Monic_Polynomial_Factorization
15:58:33Frequency_Moments: theory Frequency_Moments.Frequency_Moments
15:58:34Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
15:58:34Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
15:58:35Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
15:58:36Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Walks
15:58:40Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Power_Construction
15:58:40Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
15:58:43Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
15:58:47Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
15:58:47Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test
15:58:47Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials
15:58:50Frequency_Moments: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
15:58:54Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test_Code
15:58:58Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
15:59:06Frequency_Moments: theory Finite_Fields.Find_Irreducible_Poly
15:59:14Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
15:59:18Frequency_Moments: theory Frequency_Moments.Tutorial_Pseudorandom_Objects
16:09:44Preparing Frequency_Moments/document ...
16:09:53Finished Frequency_Moments/document (0:00:08 elapsed time)
16:09:53Preparing Frequency_Moments/outline ...
16:09:57Finished Frequency_Moments/outline (0:00:03 elapsed time)
16:09:57Timing Frequency_Moments (8 threads, 720.116s elapsed time, 4229.164s cpu time, 344.975s GC time, factor 5.87)
16:09:57Finished Frequency_Moments (0:13:21 elapsed time, 1:13:52 cpu time, factor 5.53)
16:09:57Running HOL-ODE-ARCH-COMP (on hpcisabelle/0) ...
16:10:01HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
16:22:30Timing HOL-ODE-ARCH-COMP (8 threads, 748.055s elapsed time, 1694.060s cpu time, 17.476s GC time, factor 2.26)
16:22:30Finished HOL-ODE-ARCH-COMP (0:12:32 elapsed time, 0:28:20 cpu time, factor 2.26)
16:22:30Building Sepref_Prereq (on hpcisabelle/1) ...
16:22:33Sepref_Prereq: theory HOL-Library.Nat_Bijection
16:22:33Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
16:22:33Sepref_Prereq: theory HOL-Library.Old_Datatype
16:22:34Sepref_Prereq: theory HOL-Library.Countable
16:22:36Sepref_Prereq: theory HOL-Imperative_HOL.Heap
16:22:37Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
16:22:40Sepref_Prereq: theory HOL-Imperative_HOL.Array
16:22:41Sepref_Prereq: theory HOL-Imperative_HOL.Ref
16:22:41Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
16:22:41Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
16:22:41Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
16:22:41Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
16:22:44Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
16:22:44Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
16:22:46Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
16:22:47Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
16:22:48Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
16:22:50Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
16:22:51Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
16:22:56Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
16:23:02Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
16:23:02Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
16:23:04Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
16:23:04Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
16:23:04Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
16:23:06Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
16:23:24Timing Sepref_Prereq (8 threads, 35.454s elapsed time, 103.384s cpu time, 3.331s GC time, factor 2.92)
16:23:24Finished Sepref_Prereq (0:00:53 elapsed time, 0:02:16 cpu time, factor 2.56)
16:23:24Running Finite_Fields (on hpcisabelle/2) ...
16:23:30Finite_Fields: theory Flow_Networks.Graph
16:23:30Finite_Fields: theory Digit_Expansions.Bits_Digits
16:23:30Finite_Fields: theory HOL-Number_Theory.Cong
16:23:30Finite_Fields: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
16:23:30Finite_Fields: theory HOL-Number_Theory.Eratosthenes
16:23:30Finite_Fields: theory HOL-Types_To_Sets.Types_To_Sets
16:23:30Finite_Fields: theory HOL-Real_Asymp.Inst_Existentials
16:23:30Finite_Fields: theory HOL-Analysis.Metric_Arith
16:23:30Finite_Fields: theory Finite_Fields.Finite_Fields_Preliminary_Results
16:23:30Finite_Fields: theory Finite_Fields.Finite_Fields_More_Bijections
16:23:30Finite_Fields: theory HOL-Analysis.Abstract_Topology
16:23:30Finite_Fields: theory HOL-Analysis.Continuum_Not_Denumerable
16:23:30Finite_Fields: theory HOL-Analysis.Inner_Product
16:23:31Finite_Fields: theory HOL-Analysis.L2_Norm
16:23:31Finite_Fields: theory HOL-Analysis.Operator_Norm
16:23:31Finite_Fields: theory HOL-Analysis.Poly_Roots
16:23:31Finite_Fields: theory HOL-Analysis.Product_Vector
16:23:31Finite_Fields: theory HOL-Combinatorics.Multiset_Permutations
16:23:32Finite_Fields: theory HOL-Number_Theory.Mod_Exp
16:23:32Finite_Fields: theory HOL-Analysis.Sigma_Algebra
16:23:32Finite_Fields: theory Flow_Networks.Network
16:23:32Finite_Fields: theory HOL-Analysis.Norm_Arith
16:23:33Finite_Fields: theory HOL-Number_Theory.Fib
16:23:33Finite_Fields: theory HOL-Number_Theory.Prime_Powers
16:23:33Finite_Fields: theory HOL-Number_Theory.Totient
16:23:34Finite_Fields: theory HOL-Real_Asymp.Eventuallize
16:23:34Finite_Fields: theory HOL-Real_Asymp.Lazy_Eval
16:23:34Finite_Fields: theory HOL-Analysis.Elementary_Topology
16:23:35Finite_Fields: theory HOL-Analysis.Euclidean_Space
16:23:35Finite_Fields: theory Flow_Networks.Residual_Graph
16:23:35Finite_Fields: theory HOL-Number_Theory.Residues
16:23:35Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion
16:23:37Finite_Fields: theory HOL-Analysis.Measurable
16:23:37Finite_Fields: theory HOL-Analysis.Abstract_Limits
16:23:38Finite_Fields: theory HOL-Analysis.FSigma
16:23:38Finite_Fields: theory HOL-Analysis.Sum_Topology
16:23:38Finite_Fields: theory HOL-Analysis.Measure_Space
16:23:39Finite_Fields: theory Flow_Networks.Augmenting_Flow
16:23:40Finite_Fields: theory Flow_Networks.Augmenting_Path
16:23:40Finite_Fields: theory HOL-Analysis.Finite_Cartesian_Product
16:23:40Finite_Fields: theory HOL-Analysis.Linear_Algebra
16:23:40Finite_Fields: theory Flow_Networks.Ford_Fulkerson
16:23:40Finite_Fields: theory HOL-Analysis.Abstract_Topology_2
16:23:41Finite_Fields: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
16:23:41Finite_Fields: theory Finite_Fields.Finite_Fields_Factorization_Ext
16:23:41Finite_Fields: theory HOL-Analysis.Affine
16:23:42Finite_Fields: theory Finite_Fields.Ring_Characteristic
16:23:43Finite_Fields: theory HOL-Analysis.Convex
16:23:43Finite_Fields: theory HOL-Analysis.Infinite_Sum
16:23:43Finite_Fields: theory HOL-Analysis.Cartesian_Space
16:23:43Finite_Fields: theory MFMC_Countable.MFMC_Finite
16:23:43Finite_Fields: theory HOL-Analysis.Caratheodory
16:23:43Finite_Fields: theory HOL-Number_Theory.Euler_Criterion
16:23:43Finite_Fields: theory HOL-Number_Theory.Pocklington
16:23:44Finite_Fields: theory HOL-Number_Theory.Gauss
16:23:44Finite_Fields: theory HOL-Analysis.Connected
16:23:44Finite_Fields: theory HOL-Analysis.Elementary_Metric_Spaces
16:23:44Finite_Fields: theory HOL-Number_Theory.Quadratic_Reciprocity
16:23:45Finite_Fields: theory HOL-Analysis.Function_Topology
16:23:45Finite_Fields: theory HOL-Number_Theory.Residue_Primitive_Roots
16:23:46Finite_Fields: theory HOL-Number_Theory.Number_Theory
16:23:47Finite_Fields: theory HOL-Analysis.Determinants
16:23:47Finite_Fields: theory HOL-Analysis.Product_Topology
16:23:47Finite_Fields: theory HOL-Analysis.T1_Spaces
16:23:47Finite_Fields: theory HOL-Analysis.Lindelof_Spaces
16:23:48Finite_Fields: theory HOL-Analysis.Elementary_Normed_Spaces
16:23:48Finite_Fields: theory HOL-Analysis.Function_Metric
16:23:48Finite_Fields: theory HOL-Analysis.Isolated
16:23:48Finite_Fields: theory Dirichlet_Series.Dirichlet_Misc
16:23:48Finite_Fields: theory Dirichlet_Series.Multiplicative_Function
16:23:49Finite_Fields: theory Dirichlet_Series.Dirichlet_Product
16:23:49Finite_Fields: theory Dirichlet_Series.Dirichlet_Series
16:23:49Finite_Fields: theory HOL-Analysis.Topology_Euclidean_Space
16:23:51Finite_Fields: theory HOL-Analysis.Extended_Real_Limits
16:23:51Finite_Fields: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
16:23:52Finite_Fields: theory Finite_Fields.Formal_Polynomial_Derivatives
16:23:52Finite_Fields: theory HOL-Analysis.Line_Segment
16:23:52Finite_Fields: theory HOL-Analysis.Tagged_Division
16:23:52Finite_Fields: theory HOL-Analysis.Summation_Tests
16:23:53Finite_Fields: theory Dirichlet_Series.Moebius_Mu
16:23:53Finite_Fields: theory Finite_Fields.Monic_Polynomial_Factorization
16:23:53Finite_Fields: theory Dirichlet_Series.More_Totient
16:23:53Finite_Fields: theory Dirichlet_Series.Divisor_Count
16:23:54Finite_Fields: theory HOL-Analysis.Uniform_Limit
16:23:54Finite_Fields: theory Dirichlet_Series.Liouville_Lambda
16:23:54Finite_Fields: theory HOL-Analysis.Convex_Euclidean_Space
16:23:54Finite_Fields: theory Dirichlet_Series.Arithmetic_Summatory
16:23:55Finite_Fields: theory HOL-Analysis.Ordered_Euclidean_Space
16:23:55Finite_Fields: theory HOL-Analysis.Starlike
16:23:55Finite_Fields: theory HOL-Analysis.Bounded_Continuous_Function
16:23:55Finite_Fields: theory HOL-Analysis.Bounded_Linear_Function
16:23:57Finite_Fields: theory HOL-Analysis.Continuous_Extension
16:23:57Finite_Fields: theory HOL-Analysis.Path_Connected
16:23:58Finite_Fields: theory HOL-Analysis.Derivative
16:23:59Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
16:24:00Finite_Fields: theory HOL-Analysis.Locally
16:24:00Finite_Fields: theory HOL-Analysis.Uncountable_Sets
16:24:00Finite_Fields: theory HOL-Analysis.Arcwise_Connected
16:24:00Finite_Fields: theory HOL-Analysis.Homotopy
16:24:01Finite_Fields: theory HOL-Analysis.Borel_Space
16:24:01Finite_Fields: theory HOL-Analysis.Cartesian_Euclidean_Space
16:24:01Finite_Fields: theory HOL-Analysis.Complex_Analysis_Basics
16:24:01Finite_Fields: theory HOL-Analysis.Weierstrass_Theorems
16:24:01Finite_Fields: theory HOL-Analysis.Cross3
16:24:03Finite_Fields: theory HOL-Analysis.Polytope
16:24:04Finite_Fields: theory HOL-Analysis.Complex_Transcendental
16:24:05Finite_Fields: theory HOL-Analysis.Abstract_Euclidean_Space
16:24:05Finite_Fields: theory HOL-Analysis.Homeomorphism
16:24:05Finite_Fields: theory HOL-Analysis.Sparse_In
16:24:06Finite_Fields: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
16:24:06Finite_Fields: theory HOL-Analysis.Regularity
16:24:07Finite_Fields: theory HOL-Analysis.Abstract_Topological_Spaces
16:24:07Finite_Fields: theory HOL-Analysis.Brouwer_Fixpoint
16:24:08Finite_Fields: theory Executable_Randomized_Algorithms.Tau_Additivity
16:24:10Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
16:24:10Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test
16:24:12Finite_Fields: theory Finite_Fields.Card_Irreducible_Polynomials
16:24:14Finite_Fields: theory HOL-Analysis.Generalised_Binomial_Theorem
16:24:14Finite_Fields: theory HOL-Analysis.Harmonic_Numbers
16:24:14Finite_Fields: theory HOL-Analysis.FPS_Convergence
16:24:15Finite_Fields: theory HOL-Analysis.Infinite_Products
16:24:15Finite_Fields: theory HOL-Analysis.Binary_Product_Measure
16:24:16Finite_Fields: theory HOL-Analysis.Fashoda_Theorem
16:24:17Finite_Fields: theory HOL-Analysis.Embed_Measure
16:24:17Finite_Fields: theory HOL-Analysis.Finite_Product_Measure
16:24:17Finite_Fields: theory HOL-Analysis.Abstract_Metric_Spaces
16:24:17Finite_Fields: theory HOL-Analysis.Retracts
16:24:17Finite_Fields: theory Finite_Fields.Finite_Fields_Isomorphic
16:24:22Finite_Fields: theory HOL-Analysis.Bochner_Integration
16:24:22Finite_Fields: theory HOL-Probability.Fin_Map
16:24:22Finite_Fields: theory HOL-Analysis.Smooth_Paths
16:24:26Finite_Fields: theory Finite_Fields.Rabin_Irreducibility_Test_Code
16:24:26Finite_Fields: theory HOL-Analysis.Complete_Measure
16:24:26Finite_Fields: theory HOL-Analysis.Radon_Nikodym
16:24:27Finite_Fields: theory HOL-Analysis.Set_Integral
16:24:27Finite_Fields: theory HOL-Analysis.Lebesgue_Measure
16:24:27Finite_Fields: theory HOL-Analysis.Lipschitz
16:24:27Finite_Fields: theory HOL-Analysis.Urysohn
16:24:29Finite_Fields: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
16:24:29Finite_Fields: theory HOL-Analysis.Infinite_Set_Sum
16:24:29Finite_Fields: theory HOL-Analysis.Multivariate_Analysis
16:24:31Finite_Fields: theory HOL-Analysis.Henstock_Kurzweil_Integration
16:24:31Finite_Fields: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
16:24:33Finite_Fields: theory HOL-Real_Asymp.Real_Asymp
16:24:36Finite_Fields: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
16:24:36Finite_Fields: theory HOL-Analysis.Integral_Test
16:24:36Finite_Fields: theory HOL-Analysis.Kronecker_Approximation_Theorem
16:24:38Finite_Fields: theory HOL-Analysis.Further_Topology
16:24:38Finite_Fields: theory HOL-Analysis.Gamma_Function
16:24:38Finite_Fields: theory HOL-Analysis.Improper_Integral
16:24:38Finite_Fields: theory HOL-Analysis.Interval_Integral
16:24:38Finite_Fields: theory HOL-Analysis.Vitali_Covering_Theorem
16:24:39Finite_Fields: theory HOL-Analysis.Equivalence_Measurable_On_Borel
16:24:39Finite_Fields: theory HOL-Analysis.Lebesgue_Integral_Substitution
16:24:40Finite_Fields: theory HOL-Analysis.Change_Of_Vars
16:24:42Finite_Fields: theory HOL-Analysis.Simplex_Content
16:24:43Finite_Fields: theory HOL-Analysis.Jordan_Curve
16:24:44Finite_Fields: theory HOL-Analysis.Ball_Volume
16:24:44Finite_Fields: theory HOL-Analysis.Analysis
16:24:46Finite_Fields: theory Dirichlet_Series.Euler_Products
16:24:46Finite_Fields: theory Dirichlet_Series.Partial_Summation
16:24:46Finite_Fields: theory HOL-Complex_Analysis.Contour_Integration
16:24:46Finite_Fields: theory HOL-Probability.Discrete_Topology
16:24:46Finite_Fields: theory HOL-Probability.Essential_Supremum
16:24:46Finite_Fields: theory HOL-Probability.Probability_Measure
16:24:46Finite_Fields: theory HOL-Probability.Stopping_Time
16:24:46Finite_Fields: theory HOL-Probability.Tree_Space
16:24:47Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
16:24:48Finite_Fields: theory HOL-Complex_Analysis.Winding_Numbers
16:24:48Finite_Fields: theory HOL-Probability.Conditional_Expectation
16:24:48Finite_Fields: theory HOL-Probability.Distribution_Functions
16:24:48Finite_Fields: theory HOL-Probability.Giry_Monad
16:24:48Finite_Fields: theory HOL-Probability.Weak_Convergence
16:24:49Finite_Fields: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
16:24:49Finite_Fields: theory HOL-Probability.Helly_Selection
16:24:50Finite_Fields: theory HOL-Complex_Analysis.Conformal_Mappings
16:24:51Finite_Fields: theory HOL-Probability.Probability_Mass_Function
16:24:51Finite_Fields: theory HOL-Probability.Projective_Family
16:24:51Finite_Fields: theory HOL-Complex_Analysis.Complex_Singularities
16:24:51Finite_Fields: theory HOL-Complex_Analysis.Great_Picard
16:24:52Finite_Fields: theory HOL-Probability.Infinite_Product_Measure
16:24:52Finite_Fields: theory HOL-Complex_Analysis.Riemann_Mapping
16:24:54Finite_Fields: theory HOL-Probability.Independent_Family
16:24:54Finite_Fields: theory HOL-Probability.Projective_Limit
16:24:54Finite_Fields: theory HOL-Complex_Analysis.Complex_Residues
16:24:54Finite_Fields: theory HOL-Probability.Stream_Space
16:24:54Finite_Fields: theory HOL-Complex_Analysis.Residue_Theorem
16:24:55Finite_Fields: theory Finite_Fields.Finite_Fields_More_PMF
16:24:55Finite_Fields: theory HOL-Probability.PMF_Impl
16:24:55Finite_Fields: theory HOL-Probability.Random_Permutations
16:24:55Finite_Fields: theory HOL-Complex_Analysis.Laurent_Convergence
16:24:55Finite_Fields: theory HOL-Probability.SPMF
16:24:56Finite_Fields: theory HOL-Probability.Convolution
16:24:56Finite_Fields: theory HOL-Probability.Information
16:24:56Finite_Fields: theory HOL-Probability.Product_PMF
16:24:57Finite_Fields: theory HOL-Probability.Hoeffding
16:24:59Finite_Fields: theory HOL-Probability.Distributions
16:24:59Finite_Fields: theory HOL-Complex_Analysis.Meromorphic
16:25:00Finite_Fields: theory HOL-Complex_Analysis.Weierstrass_Factorization
16:25:00Finite_Fields: theory HOL-Probability.Characteristic_Functions
16:25:01Finite_Fields: theory HOL-Complex_Analysis.Complex_Analysis
16:25:01Finite_Fields: theory HOL-Probability.Sinc_Integral
16:25:01Finite_Fields: theory HOL-Probability.Levy
16:25:01Finite_Fields: theory Dirichlet_Series.Dirichlet_Series_Analysis
16:25:01Finite_Fields: theory HOL-Probability.Central_Limit_Theorem
16:25:01Finite_Fields: theory HOL-Probability.Probability
16:25:07Finite_Fields: theory Executable_Randomized_Algorithms.Coin_Space
16:25:07Finite_Fields: theory MFMC_Countable.MFMC_Misc
16:25:08Finite_Fields: theory MFMC_Countable.Matrix_For_Marginals
16:25:10Finite_Fields: theory MFMC_Countable.Rel_PMF_Characterisation
16:25:10Finite_Fields: theory Zeta_Function.Zeta_Library
16:25:10Finite_Fields: theory Probabilistic_While.While_SPMF
16:25:10Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
16:25:14Finite_Fields: theory Executable_Randomized_Algorithms.Randomized_Algorithm
16:25:15Finite_Fields: theory Finite_Fields.Find_Irreducible_Poly
16:35:10Preparing Finite_Fields/document ...
16:35:21Finished Finite_Fields/document (0:00:11 elapsed time)
16:35:21Preparing Finite_Fields/outline ...
16:35:26Finished Finite_Fields/outline (0:00:04 elapsed time)
16:35:27Timing Finite_Fields (8 threads, 677.446s elapsed time, 4709.555s cpu time, 225.821s GC time, factor 6.95)
16:35:27Finished Finite_Fields (0:11:24 elapsed time, 1:18:58 cpu time, factor 6.92)
16:35:27Building CAVA_Setup (on hpcisabelle/3) ...
16:35:29CAVA_Setup: theory Partial_Order_Reduction.Basic_Extensions
16:35:29CAVA_Setup: theory HOL-Library.Case_Converter
16:35:29CAVA_Setup: theory Partial_Order_Reduction.Set_Extensions
16:35:29CAVA_Setup: theory HOL-Library.Complete_Partial_Order2
16:35:29CAVA_Setup: theory HOL-Library.IArray
16:35:29CAVA_Setup: theory HOL-Library.Mapping
16:35:29CAVA_Setup: theory HOL-Library.Stream
16:35:29CAVA_Setup: theory DFS_Framework.DFS_Framework_Misc
16:35:30CAVA_Setup: theory HOL-Library.Sublist
16:35:30CAVA_Setup: theory Partial_Order_Reduction.Functions
16:35:30CAVA_Setup: theory HOL-Library.Countable_Set
16:35:31CAVA_Setup: theory HOL-Library.Simps_Case_Conv
16:35:31CAVA_Setup: theory Partial_Order_Reduction.Relation_Extensions
16:35:31CAVA_Setup: theory LTL.LTL
16:35:31CAVA_Setup: theory Promela.PromelaAST
16:35:32CAVA_Setup: theory DFS_Framework.DFS_Framework_Refine_Aux
16:35:32CAVA_Setup: theory HOL-Library.Countable_Complete_Lattices
16:35:32CAVA_Setup: theory SM.SM_Syntax
16:35:32CAVA_Setup: theory SM.SOS_Misc_Add
16:35:32CAVA_Setup: theory Stuttering_Equivalence.Samplers
16:35:32CAVA_Setup: theory HOL-Library.RBT_Mapping
16:35:33CAVA_Setup: theory Stuttering_Equivalence.StutterEquivalence
16:35:33CAVA_Setup: theory Transition_Systems_and_Automata.Basic
16:35:33CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton
16:35:33CAVA_Setup: theory Transition_Systems_and_Automata.Sequence
16:35:33CAVA_Setup: theory HOL-Library.Prefix_Order
16:35:33CAVA_Setup: theory Partial_Order_Reduction.List_Prefixes
16:35:34CAVA_Setup: theory Partial_Order_Reduction.List_Extensions
16:35:34CAVA_Setup: theory SM.LTS
16:35:34CAVA_Setup: theory SM.Gen_Scheduler
16:35:34CAVA_Setup: theory Partial_Order_Reduction.Word_Prefixes
16:35:35CAVA_Setup: theory Partial_Order_Reduction.Traces
16:35:35CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System
16:35:36CAVA_Setup: theory HOL-Library.Order_Continuity
16:35:36CAVA_Setup: theory DFS_Framework.Impl_Rev_Array_Stack
16:35:36CAVA_Setup: theory DFS_Framework.Param_DFS
16:35:36CAVA_Setup: theory HOL-Library.Extended_Nat
16:35:38CAVA_Setup: theory SM.Gen_Scheduler_Refine
16:35:38CAVA_Setup: theory Promela.PromelaStatistics
16:35:38CAVA_Setup: theory Coinductive.Coinductive_Nat
16:35:39CAVA_Setup: theory HOL-Library.Linear_Temporal_Logic_on_Streams
16:35:39CAVA_Setup: theory SM.SM_Cfg
16:35:39CAVA_Setup: theory Gabow_SCC.Gabow_SCC
16:35:39CAVA_Setup: theory SM.Gen_Cfg_Bisim
16:35:40CAVA_Setup: theory Coinductive.Coinductive_List
16:35:40CAVA_Setup: theory Partial_Order_Reduction.ENat_Extensions
16:35:40CAVA_Setup: theory Gabow_SCC.Find_Path
16:35:40CAVA_Setup: theory Partial_Order_Reduction.CCPO_Extensions
16:35:41CAVA_Setup: theory Gabow_SCC.Find_Path_Impl
16:35:41CAVA_Setup: theory Transition_Systems_and_Automata.Sequence_LTL
16:35:42CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Construction
16:35:42CAVA_Setup: theory Partial_Order_Reduction.ESet_Extensions
16:35:42CAVA_Setup: theory Transition_Systems_and_Automata.Transition_System_Extra
16:35:43CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Extensions
16:35:43CAVA_Setup: theory DFS_Framework.DFS_Invars_Basic
16:35:44CAVA_Setup: theory DFS_Framework.General_DFS_Structure
16:35:45CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Traces
16:35:46CAVA_Setup: theory SM.Pid_Scheduler
16:35:46CAVA_Setup: theory Gabow_SCC.Gabow_GBG
16:35:46CAVA_Setup: theory Gabow_SCC.Gabow_Skeleton_Code
16:35:49CAVA_Setup: theory Coinductive.Coinductive_List_Prefix
16:35:49CAVA_Setup: theory Coinductive.Coinductive_Stream
16:35:49CAVA_Setup: theory Word_Lib.Bits_Int
16:35:50CAVA_Setup: theory Partial_Order_Reduction.Coinductive_List_Extensions
16:35:51CAVA_Setup: theory Stuttering_Equivalence.PLTL
16:35:52CAVA_Setup: theory DFS_Framework.Rec_Impl
16:35:52CAVA_Setup: theory Partial_Order_Reduction.LList_Prefixes
16:35:52CAVA_Setup: theory DFS_Framework.Tailrec_Impl
16:35:53CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA
16:35:53CAVA_Setup: theory Partial_Order_Reduction.Stuttering
16:35:54CAVA_Setup: theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
16:35:54CAVA_Setup: theory Word_Lib.Typedef_Morphisms
16:35:55CAVA_Setup: theory Partial_Order_Reduction.Ample_Abstract
16:35:55CAVA_Setup: theory SM.SM_State
16:35:56CAVA_Setup: theory Partial_Order_Reduction.Ample_Analysis
16:35:57CAVA_Setup: theory SM.SM_Semantics
16:35:59CAVA_Setup: theory Promela.PromelaDatastructures
16:36:01CAVA_Setup: theory DFS_Framework.Simple_Impl
16:36:01CAVA_Setup: theory LTL_to_GBA.LTL_to_GBA_impl
16:36:02CAVA_Setup: theory SM.Decide_Locality
16:36:02CAVA_Setup: theory SM.SM_LTL
16:36:04CAVA_Setup: theory SM.Type_System
16:36:08CAVA_Setup: theory DFS_Framework.Restr_Impl
16:36:08CAVA_Setup: theory SM.SM_Finite_Reachable
16:36:09CAVA_Setup: theory SM.Rename_Cfg
16:36:10CAVA_Setup: theory DFS_Framework.DFS_Framework
16:36:11CAVA_Setup: theory DFS_Framework.Reachable_Nodes
16:36:16CAVA_Setup: theory Gabow_SCC.Gabow_GBG_Code
16:36:16CAVA_Setup: theory Gabow_SCC.Gabow_SCC_Code
16:36:18CAVA_Setup: theory SM.SM_Visible
16:36:20CAVA_Setup: theory SM.SM_Pid
16:36:24CAVA_Setup: theory SM.SM_Variables
16:36:26CAVA_Setup: theory SM.SM_Indep
16:36:55CAVA_Setup: theory LTL_to_GBA.All_Of_LTL_to_GBA
16:37:04CAVA_Setup: theory DFS_Framework.Feedback_Arcs
16:37:29CAVA_Setup: theory Promela.PromelaInvariants
16:37:31CAVA_Setup: theory Promela.Promela
16:37:38CAVA_Setup: theory Gabow_SCC.All_Of_Gabow_SCC
16:37:47CAVA_Setup: theory SM.SM_Datastructures
16:37:48CAVA_Setup: theory SM.SM_Sticky
16:37:59CAVA_Setup: theory SM.SM_POR
16:38:11CAVA_Setup: theory SM.SM_Ample_Impl
16:38:42CAVA_Setup: theory Promela.PromelaLTL
16:38:46CAVA_Setup: theory Promela.PromelaLTLConv
16:38:54CAVA_Setup: theory Promela.All_Of_Promela
16:39:57CAVA_Setup: theory SM.SM_Wrapup
16:42:16Timing CAVA_Setup (8 threads, 341.036s elapsed time, 2284.015s cpu time, 163.953s GC time, factor 6.70)
16:42:16Finished CAVA_Setup (0:06:44 elapsed time, 0:40:42 cpu time, factor 6.04)
16:42:16Building Refine_Imperative_HOL (on hpcisabelle/4) ...
16:42:18Refine_Imperative_HOL: theory Refine_Imperative_HOL.User_Smashing
16:42:18Refine_Imperative_HOL: theory Isar_Ref.Base
16:42:18Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Misc
16:42:18Refine_Imperative_HOL: theory Refine_Imperative_HOL.PO_Normalizer
16:42:18Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Add
16:42:18Refine_Imperative_HOL: theory List-Index.List_Index
16:42:18Refine_Imperative_HOL: theory Refine_Imperative_HOL.Concl_Pres_Clarification
16:42:18Refine_Imperative_HOL: theory Refine_Imperative_HOL.Named_Theorems_Rev
16:42:19Refine_Imperative_HOL: theory Refine_Imperative_HOL.Structured_Apply
16:42:19Refine_Imperative_HOL: theory Refine_Imperative_HOL.Pf_Mono_Prover
16:42:19Refine_Imperative_HOL: theory DFS_Framework.DFS_Framework_Refine_Aux
16:42:19Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Misc
16:42:21Refine_Imperative_HOL: theory Refine_Imperative_HOL.Term_Synth
16:42:22Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Tool
16:42:22Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Setup
16:42:22Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_IICF
16:42:22Refine_Imperative_HOL: theory HOL-Library.Rewrite
16:42:22Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Userguides
16:42:22Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Id_Op
16:42:22Refine_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Default_Insts
16:42:23Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Basic
16:42:24Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Constraints
16:42:24Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Monadify
16:42:25Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Frame
16:42:25Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Rules
16:42:30Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Combinator_Setup
16:42:30Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Definition
16:42:31Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Translate
16:42:32Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Intf_Util
16:42:35Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Tool
16:42:36Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_HOL_Bindings
16:42:39Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Foreach
16:42:41Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Improper
16:42:41Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref
16:42:42Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List
16:42:42Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Map
16:42:42Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Multiset
16:42:42Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Matrix
16:42:42Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Set
16:42:43Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Map
16:42:43Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_Mset
16:42:43Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_MsetO
16:42:43Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Prio_Bag
16:42:43Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_List_SetO
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_List
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_HOL_List
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_MS_Array_List
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heap
16:42:44Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Sepl_Binding
16:42:45Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Abs_Heapmap
16:42:45Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Indexed_Array_List
16:42:46Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heap
16:42:46Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Array_Matrix
16:42:48Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF_Impl_Heapmap
16:43:05Refine_Imperative_HOL: theory Refine_Imperative_HOL.IICF
16:43:06Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_General_Util
16:43:07Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
16:43:07Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Guide_Reference
16:43:54Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Graph
16:43:54Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Misc
16:43:54Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Weight
16:43:54Refine_Imperative_HOL: theory HOL-Library.Omega_Words_Fun
16:43:54Refine_Imperative_HOL: theory Collections_Examples.Succ_Graph
16:43:54Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_ICF_Bindings
16:43:54Refine_Imperative_HOL: theory CAVA_Automata.Digraph_Basic
16:43:55Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphSpec
16:43:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_WGraph
16:43:58Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra
16:44:00Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphGA
16:44:00Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.GraphByMap
16:44:03Refine_Imperative_HOL: theory Collections_Examples.Nested_DFS
16:44:03Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.HashGraphImpl
16:44:06Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
16:44:51Refine_Imperative_HOL: theory Dijkstra_Shortest_Path.Test
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Examples
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Heapmap_Bench
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Graph
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Dijkstra
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Combinator
16:44:57Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Snip_Datatype
16:45:00Refine_Imperative_HOL: theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
16:45:03Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_DFS
16:45:03Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_NDFS
16:45:03Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_Minitests
16:45:19Refine_Imperative_HOL: theory Refine_Imperative_HOL.Dijkstra_Benchmark
16:45:33Refine_Imperative_HOL: theory Refine_Imperative_HOL.NDFS_Benchmark
16:45:33Refine_Imperative_HOL: theory Refine_Imperative_HOL.Sepref_All_Examples
16:46:32Preparing Refine_Imperative_HOL/document ...
16:46:46Finished Refine_Imperative_HOL/document (0:00:13 elapsed time)
16:46:46Preparing Refine_Imperative_HOL/outline ...
16:46:55Finished Refine_Imperative_HOL/outline (0:00:08 elapsed time)
16:46:55Timing Refine_Imperative_HOL (8 threads, 225.690s elapsed time, 594.621s cpu time, 24.915s GC time, factor 2.63)
16:46:55Finished Refine_Imperative_HOL (0:04:14 elapsed time, 0:10:57 cpu time, factor 2.58)
16:46:56Building Subresultants (on hpcisabelle/5) ...
16:46:59Subresultants: theory Subresultants.Coeff_Int
16:46:59Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial
16:46:59Subresultants: theory Subresultants.Dichotomous_Lazard
16:46:59Subresultants: theory Subresultants.More_Homomorphisms
16:46:59Subresultants: theory Subresultants.Resultant_Prelim
16:46:59Subresultants: theory Subresultants.Binary_Exponentiation
16:47:00Subresultants: theory Subresultants.Subresultant
16:47:06Subresultants: theory Subresultants.Subresultant_Gcd
16:48:13Preparing Subresultants/document ...
16:48:19Finished Subresultants/document (0:00:06 elapsed time)
16:48:19Preparing Subresultants/outline ...
16:48:23Finished Subresultants/outline (0:00:03 elapsed time)
16:48:23Timing Subresultants (8 threads, 55.664s elapsed time, 274.315s cpu time, 2.671s GC time, factor 4.93)
16:48:23Finished Subresultants (0:01:16 elapsed time, 0:05:13 cpu time, factor 4.11)
16:48:23Building Core_DOM (on hpcisabelle/6) ...
16:48:41Core_DOM: theory Core_DOM.Hiding_Type_Variables
16:48:41Core_DOM: theory Core_DOM.Core_DOM_Basic_Datatypes
16:48:41Core_DOM: theory Core_DOM.Testing_Utils
16:48:42Core_DOM: theory Core_DOM.Ref
16:48:42Core_DOM: theory Core_DOM.Heap_Error_Monad
16:48:43Core_DOM: theory Core_DOM.ObjectPointer
16:48:43Core_DOM: theory Core_DOM.BaseClass
16:48:43Core_DOM: theory Core_DOM.NodePointer
16:48:43Core_DOM: theory Core_DOM.ObjectClass
16:48:44Core_DOM: theory Core_DOM.ElementPointer
16:48:45Core_DOM: theory Core_DOM.NodeClass
16:48:45Core_DOM: theory Core_DOM.CharacterDataPointer
16:48:46Core_DOM: theory Core_DOM.BaseMonad
16:48:46Core_DOM: theory Core_DOM.DocumentPointer
16:48:47Core_DOM: theory Core_DOM.ShadowRootPointer
16:48:48Core_DOM: theory Core_DOM.ObjectMonad
16:48:49Core_DOM: theory Core_DOM.NodeMonad
16:48:49Core_DOM: theory Core_DOM.ElementClass
16:48:51Core_DOM: theory Core_DOM.CharacterDataClass
16:48:51Core_DOM: theory Core_DOM.ElementMonad
16:48:52Core_DOM: theory Core_DOM.DocumentClass
16:48:52Core_DOM: theory Core_DOM.CharacterDataMonad
16:48:53Core_DOM: theory Core_DOM.DocumentMonad
16:48:55Core_DOM: theory Core_DOM.Core_DOM_Functions
16:49:15Core_DOM: theory Core_DOM.Core_DOM_Heap_WF
16:49:37Core_DOM: theory Core_DOM.Core_DOM
16:49:37Core_DOM: theory Core_DOM.Core_DOM_BaseTest
16:49:47Core_DOM: theory Core_DOM.Document_adoptNode
16:49:47Core_DOM: theory Core_DOM.Document_getElementById
16:49:47Core_DOM: theory Core_DOM.Node_insertBefore
16:49:48Core_DOM: theory Core_DOM.Node_removeChild
16:49:50Core_DOM: theory Core_DOM.Core_DOM_Tests
16:52:28Preparing Core_DOM/document ...
16:52:45Finished Core_DOM/document (0:00:16 elapsed time)
16:52:45Preparing Core_DOM/outline ...
16:52:56Finished Core_DOM/outline (0:00:11 elapsed time)
16:52:56Timing Core_DOM (8 threads, 183.621s elapsed time, 1014.340s cpu time, 56.463s GC time, factor 5.52)
16:52:56Finished Core_DOM (0:04:03 elapsed time, 0:19:29 cpu time, factor 4.80)
16:52:56Building IP_Addresses (on hpcisabelle/7) ...
16:52:58IP_Addresses: theory IP_Addresses.NumberWang_IPv4
16:52:58IP_Addresses: theory HOL-Library.Option_ord
16:52:58IP_Addresses: theory IP_Addresses.NumberWang_IPv6
16:52:58IP_Addresses: theory HOL-Library.Cancellation
16:52:58IP_Addresses: theory HOL-Library.Infinite_Set
16:52:59IP_Addresses: theory HOL-Library.Multiset
16:53:05IP_Addresses: theory HOL-ex.Quicksort
16:53:06IP_Addresses: theory Automatic_Refinement.Misc
16:53:15IP_Addresses: theory IP_Addresses.Hs_Compat
16:53:15IP_Addresses: theory HOL-Library.Product_Lexorder
16:53:15IP_Addresses: theory HOL-Library.Code_Abstract_Nat
16:53:15IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
16:53:15IP_Addresses: theory IP_Addresses.WordInterval
16:53:15IP_Addresses: theory HOL-Library.Code_Target_Nat
16:53:15IP_Addresses: theory IP_Addresses.Lib_List_toString
16:53:15IP_Addresses: theory IP_Addresses.Lib_Word_toString
16:53:19IP_Addresses: theory IP_Addresses.WordInterval_Sorted
16:53:19IP_Addresses: theory IP_Addresses.IP_Address
16:53:25IP_Addresses: theory IP_Addresses.IPv4
16:53:26IP_Addresses: theory IP_Addresses.Prefix_Match
16:53:26IP_Addresses: theory IP_Addresses.IPv6
16:53:26IP_Addresses: theory IP_Addresses.CIDR_Split
16:54:23IP_Addresses: theory IP_Addresses.IP_Address_Parser
16:54:23IP_Addresses: theory IP_Addresses.IP_Address_toString
16:54:24IP_Addresses: theory IP_Addresses.Prefix_Match_toString
16:57:38Preparing IP_Addresses/document ...
16:57:42Finished IP_Addresses/document (0:00:03 elapsed time)
16:57:42Preparing IP_Addresses/outline ...
16:57:44Finished IP_Addresses/outline (0:00:02 elapsed time)
16:57:44Timing IP_Addresses (8 threads, 265.185s elapsed time, 878.984s cpu time, 32.035s GC time, factor 3.31)
16:57:44Finished IP_Addresses (0:04:40 elapsed time, 0:15:10 cpu time, factor 3.25)
16:57:45Running Padic_Field (on hpcisabelle/0) ...
16:57:47Padic_Field: theory Padic_Field.Cring_Multivariable_Poly
16:57:47Padic_Field: theory Localization_Ring.Localization
16:57:47Padic_Field: theory Padic_Field.Indices
16:57:47Padic_Field: theory Padic_Field.Generated_Boolean_Algebra
16:57:49Padic_Field: theory Padic_Field.Fraction_Field
16:57:59Padic_Field: theory Padic_Field.Padic_Fields
16:58:24Padic_Field: theory Padic_Field.Ring_Powers
16:58:48Padic_Field: theory Padic_Field.Padic_Field_Polynomials
16:58:48Padic_Field: theory Padic_Field.Padic_Field_Topology
17:01:12Padic_Field: theory Padic_Field.Padic_Field_Powers
17:03:25Padic_Field: theory Padic_Field.Padic_Semialgebraic_Function_Ring
17:08:09Preparing Padic_Field/document ...
17:09:22Finished Padic_Field/document (0:01:13 elapsed time)
17:09:22Preparing Padic_Field/outline ...
17:09:45Finished Padic_Field/outline (0:00:22 elapsed time)
17:09:45Timing Padic_Field (8 threads, 614.487s elapsed time, 1502.666s cpu time, 135.652s GC time, factor 2.45)
17:09:45Finished Padic_Field (0:10:19 elapsed time, 0:25:15 cpu time, factor 2.45)
17:09:45Building Berlekamp_Zassenhaus (on hpcisabelle/1) ...
17:09:49Berlekamp_Zassenhaus: theory Efficient-Mergesort.Efficient_Sort
17:09:49Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
17:09:49Berlekamp_Zassenhaus: theory Word_Lib.More_Divides
17:09:49Berlekamp_Zassenhaus: theory Word_Lib.Bit_Comprehension
17:09:49Berlekamp_Zassenhaus: theory HOL-Number_Theory.Cong
17:09:49Berlekamp_Zassenhaus: theory Polynomial_Factorization.Precomputation
17:09:49Berlekamp_Zassenhaus: theory Word_Lib.Signed_Division_Word
17:09:49Berlekamp_Zassenhaus: theory HOL-Types_To_Sets.Types_To_Sets
17:09:49Berlekamp_Zassenhaus: theory Cauchy.CauchysMeanTheorem
17:09:49Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Improved_Code_Equations
17:09:49Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
17:09:49Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd
17:09:50Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
17:09:50Berlekamp_Zassenhaus: theory Polynomial_Factorization.Polynomial_Irreducibility
17:09:50Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Lagrange_Interpolation
17:09:50Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
17:09:50Berlekamp_Zassenhaus: theory Matrix.Utility
17:09:50Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_List
17:09:51Berlekamp_Zassenhaus: theory Native_Word.Code_Int_Integer_Conversion
17:09:51Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Divmod_Int
17:09:51Berlekamp_Zassenhaus: theory HOL-Number_Theory.Totient
17:09:51Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gauss_Lemma
17:09:51Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Is_Rat_To_Rat
17:09:51Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Log_Impl
17:09:51Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound
17:09:51Berlekamp_Zassenhaus: theory Sqrt_Babylonian.NthRoot_Impl
17:09:52Berlekamp_Zassenhaus: theory HOL-Number_Theory.Residues
17:09:52Berlekamp_Zassenhaus: theory Polynomial_Factorization.Gcd_Rat_Poly
17:09:52Berlekamp_Zassenhaus: theory Polynomial_Factorization.Square_Free_Factorization
17:09:52Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based
17:09:52Berlekamp_Zassenhaus: theory Sqrt_Babylonian.Sqrt_Babylonian
17:09:53Berlekamp_Zassenhaus: theory Show.Show_Poly
17:09:53Berlekamp_Zassenhaus: theory Polynomial_Factorization.Explicit_Roots
17:09:53Berlekamp_Zassenhaus: theory Polynomial_Factorization.Dvd_Int_Poly
17:09:53Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Newton_Interpolation
17:09:53Berlekamp_Zassenhaus: theory Word_Lib.More_Arithmetic
17:09:53Berlekamp_Zassenhaus: theory Polynomial_Factorization.Missing_Multiset
17:09:54Berlekamp_Zassenhaus: theory Word_Lib.More_Bit_Ring
17:09:54Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.More_Missing_Multiset
17:09:54Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration
17:09:54Berlekamp_Zassenhaus: theory Polynomial_Factorization.Prime_Factorization
17:09:54Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization
17:09:54Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
17:09:55Berlekamp_Zassenhaus: theory Word_Lib.More_Word
17:09:55Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
17:09:55Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Root_Test
17:09:55Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field
17:09:57Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Word_Base
17:09:57Berlekamp_Zassenhaus: theory Polynomial_Interpolation.Polynomial_Interpolation
17:09:57Berlekamp_Zassenhaus: theory Word_Lib.Bit_Shifts_Infix_Syntax
17:09:57Berlekamp_Zassenhaus: theory Word_Lib.Least_significant_bit
17:09:59Berlekamp_Zassenhaus: theory Word_Lib.Most_significant_bit
17:10:00Berlekamp_Zassenhaus: theory Word_Lib.Generic_set_bit
17:10:00Berlekamp_Zassenhaus: theory Polynomial_Factorization.Kronecker_Factorization
17:10:01Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Integer_Bit
17:10:01Berlekamp_Zassenhaus: theory Native_Word.Word_Type_Copies
17:10:02Berlekamp_Zassenhaus: theory Polynomial_Factorization.Rational_Factorization
17:10:05Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
17:10:08Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
17:10:10Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod
17:10:12Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
17:10:15Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
17:10:16Berlekamp_Zassenhaus: theory Native_Word.Code_Target_Int_Bit
17:10:16Berlekamp_Zassenhaus: theory Native_Word.Uint32
17:10:16Berlekamp_Zassenhaus: theory Native_Word.Uint64
17:10:18Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
17:10:23Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
17:10:24Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
17:10:25Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
17:10:27Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
17:10:27Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting
17:10:27Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure
17:10:27Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime
17:10:29Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl
17:10:29Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int
17:10:31Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound
17:10:33Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
17:10:34Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based
17:10:34Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction
17:10:39Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
17:10:40Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly
17:10:42Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly
17:10:42Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorization_External_Interface
17:12:39Preparing Berlekamp_Zassenhaus/document ...
17:13:05Finished Berlekamp_Zassenhaus/document (0:00:25 elapsed time)
17:13:05Preparing Berlekamp_Zassenhaus/outline ...
17:13:16Finished Berlekamp_Zassenhaus/outline (0:00:10 elapsed time)
17:13:16Timing Berlekamp_Zassenhaus (8 threads, 136.539s elapsed time, 812.743s cpu time, 20.438s GC time, factor 5.95)
17:13:16Finished Berlekamp_Zassenhaus (0:02:50 elapsed time, 0:14:48 cpu time, factor 5.20)
17:13:16Building Category3 (on hpcisabelle/2) ...
17:13:18Category3: theory Category3.Category
17:13:18Category3: theory HOL-Cardinals.Fun_More
17:13:18Category3: theory HOL-Cardinals.Order_Relation_More
17:13:18Category3: theory HOL-Cardinals.Order_Union
17:13:18Category3: theory HereditarilyFinite.HF
17:13:18Category3: theory HOL-Cardinals.Wellorder_Extension
17:13:19Category3: theory HOL-Cardinals.Wellfounded_More
17:13:19Category3: theory HOL-Cardinals.Wellorder_Relation
17:13:19Category3: theory Category3.ConcreteCategory
17:13:19Category3: theory Category3.DiscreteCategory
17:13:19Category3: theory Category3.EpiMonoIso
17:13:19Category3: theory HOL-Cardinals.Wellorder_Embedding
17:13:19Category3: theory HOL-Cardinals.Wellorder_Constructions
17:13:20Category3: theory Category3.DualCategory
17:13:20Category3: theory Category3.InitialTerminal
17:13:20Category3: theory Category3.ProductCategory
17:13:20Category3: theory HOL-Cardinals.Cardinal_Order_Relation
17:13:20Category3: theory HOL-Cardinals.Ordinal_Arithmetic
17:13:21Category3: theory Category3.FreeCategory
17:13:21Category3: theory Category3.Functor
17:13:21Category3: theory HOL-Cardinals.Cardinal_Arithmetic
17:13:22Category3: theory HOL-Cardinals.Cardinals
17:13:22Category3: theory ZFC_in_HOL.ZFC_Library
17:13:23Category3: theory ZFC_in_HOL.ZFC_in_HOL
17:13:24Category3: theory ZFC_in_HOL.ZFC_Cardinals
17:13:28Category3: theory Category3.NaturalTransformation
17:13:28Category3: theory Category3.Subcategory
17:13:30Category3: theory Category3.SetCategory
17:13:31Category3: theory Category3.BinaryFunctor
17:13:34Category3: theory Category3.SetCat
17:13:38Category3: theory Category3.FunctorCategory
17:13:52Category3: theory Category3.Yoneda
17:14:19Category3: theory Category3.Adjunction
17:15:13Category3: theory Category3.EquivalenceOfCategories
17:15:13Category3: theory Category3.Limit
17:16:57Category3: theory Category3.CategoryWithPullbacks
17:16:58Category3: theory Category3.ZFC_SetCat
17:17:12Category3: theory Category3.ZFC_SetCat_Interp
17:17:12Category3: theory Category3.CartesianCategory
17:17:33Category3: theory Category3.CartesianClosedCategory
17:17:34Category3: theory Category3.CategoryWithFiniteLimits
17:17:35Category3: theory Category3.HF_SetCat
17:17:38Category3: theory Category3.HF_SetCat_Interp
17:19:25Preparing Category3/document ...
17:19:55Finished Category3/document (0:00:30 elapsed time)
17:19:55Preparing Category3/outline ...
17:20:07Finished Category3/outline (0:00:11 elapsed time)
17:20:07Timing Category3 (8 threads, 330.975s elapsed time, 1882.200s cpu time, 102.576s GC time, factor 5.69)
17:20:07Finished Category3 (0:06:05 elapsed time, 0:32:44 cpu time, factor 5.37)
17:20:07Running Automated_Stateful_Protocol_Verification (on hpcisabelle/3) ...
17:20:10Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
17:20:10Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
17:20:10Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
17:20:10Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
17:20:10Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
17:20:11Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
17:20:11Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
17:20:13Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
17:20:13Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
17:20:14Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
17:20:23Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
17:20:28Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
17:20:58Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
17:21:41Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
17:25:35Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
17:27:57Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
17:28:58Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
17:29:21Preparing Automated_Stateful_Protocol_Verification/document ...
17:29:59Finished Automated_Stateful_Protocol_Verification/document (0:00:38 elapsed time)
17:29:59Preparing Automated_Stateful_Protocol_Verification/outline ...
17:30:17Finished Automated_Stateful_Protocol_Verification/outline (0:00:17 elapsed time)
17:30:17Timing Automated_Stateful_Protocol_Verification (8 threads, 537.807s elapsed time, 2099.542s cpu time, 249.203s GC time, factor 3.90)
17:30:17Finished Automated_Stateful_Protocol_Verification (0:09:06 elapsed time, 0:35:41 cpu time, factor 3.92)
17:30:17Building Simpl (on hpcisabelle/4) ...
17:30:19Simpl: theory HOL-Library.LaTeXsugar
17:30:19Simpl: theory HOL-Library.Cancellation
17:30:19Simpl: theory HOL-Library.Old_Recdef
17:30:19Simpl: theory Simpl.Simpl_Heap
17:30:19Simpl: theory HOL-Statespace.DistinctTreeProver
17:30:19Simpl: theory Simpl.HeapList
17:30:20Simpl: theory HOL-Library.Multiset
17:30:21Simpl: theory Simpl.Generalise
17:30:21Simpl: theory HOL-Statespace.StateFun
17:30:22Simpl: theory HOL-Statespace.StateSpaceLocale
17:30:22Simpl: theory Simpl.Language
17:30:22Simpl: theory HOL-Statespace.StateSpaceSyntax
17:30:29Simpl: theory Simpl.Semantic
17:30:35Simpl: theory Simpl.HoarePartialDef
17:30:35Simpl: theory Simpl.Termination
17:30:36Simpl: theory Simpl.HoarePartialProps
17:30:37Simpl: theory Simpl.HoareTotalDef
17:30:37Simpl: theory Simpl.SmallStep
17:30:38Simpl: theory Simpl.AlternativeSmallStep
17:30:38Simpl: theory Simpl.HoarePartial
17:30:40Simpl: theory Simpl.HoareTotalProps
17:30:42Simpl: theory Simpl.Compose
17:30:42Simpl: theory Simpl.HoareTotal
17:30:45Simpl: theory Simpl.Hoare
17:30:45Simpl: theory Simpl.Closure
17:30:45Simpl: theory Simpl.StateSpace
17:30:45Simpl: theory Simpl.Vcg
17:30:55Simpl: theory Simpl.ProcParEx
17:30:55Simpl: theory Simpl.ProcParExSP
17:30:55Simpl: theory Simpl.XVcg
17:30:55Simpl: theory Simpl.ClosureEx
17:30:55Simpl: theory Simpl.ComposeEx
17:30:55Simpl: theory Simpl.Quicksort
17:30:55Simpl: theory Simpl.XVcgEx
17:30:55Simpl: theory Simpl.SyntaxTest
17:30:55Simpl: theory Simpl.UserGuide
17:30:55Simpl: theory Simpl.VcgEx
17:30:55Simpl: theory Simpl.VcgExSP
17:30:56Simpl: theory Simpl.VcgExTotal
17:31:02Simpl: theory Simpl.Simpl
17:31:38Preparing Simpl/document ...
17:32:14Finished Simpl/document (0:00:35 elapsed time)
17:32:14Preparing Simpl/outline ...
17:32:31Finished Simpl/outline (0:00:17 elapsed time)
17:32:31Timing Simpl (8 threads, 57.346s elapsed time, 369.553s cpu time, 25.820s GC time, factor 6.44)
17:32:31Finished Simpl (0:01:17 elapsed time, 0:06:55 cpu time, factor 5.37)
17:32:31Building Complex_Bounded_Operators_Dependencies (on hpcisabelle/5) ...
17:32:34Complex_Bounded_Operators_Dependencies: theory Containers.List_Fusion
17:32:34Complex_Bounded_Operators_Dependencies: theory Containers.Extend_Partial_Order
17:32:34Complex_Bounded_Operators_Dependencies: theory Containers.Equal
17:32:34Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator
17:32:34Complex_Bounded_Operators_Dependencies: theory Deriving.Derive_Manager
17:32:34Complex_Bounded_Operators_Dependencies: theory Deriving.Generator_Aux
17:32:34Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Fun_More
17:32:34Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Relation_More
17:32:34Complex_Bounded_Operators_Dependencies: theory Containers.Closure_Set
17:32:34Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Order_Union
17:32:34Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fraction_Field
17:32:34Complex_Bounded_Operators_Dependencies: theory HOL-Library.Adhoc_Overloading
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Library.Char_ord
17:32:35Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Generator
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Extension
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Library.Monad_Syntax
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Abstract_Nat
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellfounded_More
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Int
17:32:35Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Auxiliary
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Relation
17:32:35Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Nat
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Library.Complemented_Lattices
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Embedding
17:32:36Complex_Bounded_Operators_Dependencies: theory Deriving.Equality_Instances
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Library.Code_Target_Numeral
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Congruence
17:32:36Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Misc
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Library.Function_Algebras
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Wellorder_Constructions
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Library.IArray
17:32:36Complex_Bounded_Operators_Dependencies: theory HOL-Library.More_List
17:32:36Complex_Bounded_Operators_Dependencies: theory Deriving.Compare
17:32:37Complex_Bounded_Operators_Dependencies: theory Deriving.Comparator_Generator
17:32:37Complex_Bounded_Operators_Dependencies: theory Containers.Lexicographic_Order
17:32:37Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Normalized_Fraction
17:32:37Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Order_Relation
17:32:37Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Ordinal_Arithmetic
17:32:37Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Order
17:32:37Complex_Bounded_Operators_Dependencies: theory Containers.Containers_Generator
17:32:38Complex_Bounded_Operators_Dependencies: theory Containers.Set_Linorder
17:32:38Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Generator
17:32:38Complex_Bounded_Operators_Dependencies: theory HOL-Library.RBT_Impl
17:32:38Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Enum
17:32:39Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinal_Arithmetic
17:32:39Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Eq
17:32:39Complex_Bounded_Operators_Dependencies: theory Deriving.Compare_Instances
17:32:39Complex_Bounded_Operators_Dependencies: theory HOL-Cardinals.Cardinals
17:32:39Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Lattice
17:32:40Complex_Bounded_Operators_Dependencies: theory HOL-Library.Rewrite
17:32:40Complex_Bounded_Operators_Dependencies: theory HOL-Types_To_Sets.Types_To_Sets
17:32:40Complex_Bounded_Operators_Dependencies: theory Containers.DList_Set
17:32:41Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Unsorted
17:32:41Complex_Bounded_Operators_Dependencies: theory Cauchy.CauchysMeanTheorem
17:32:41Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial
17:32:41Complex_Bounded_Operators_Dependencies: theory HOL-Examples.Sqrt
17:32:41Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Complete_Lattice
17:32:41Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Conjugate
17:32:42Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus_Missing
17:32:42Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Group
17:32:42Complex_Bounded_Operators_Dependencies: theory Banach_Steinhaus.Banach_Steinhaus
17:32:42Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
17:32:42Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom
17:32:42Complex_Bounded_Operators_Dependencies: theory Show.Show
17:32:43Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Log_Impl
17:32:43Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.NthRoot_Impl
17:32:44Complex_Bounded_Operators_Dependencies: theory Show.Show_Instances
17:32:45Complex_Bounded_Operators_Dependencies: theory Sqrt_Babylonian.Sqrt_Babylonian
17:32:45Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Coset
17:32:45Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.FiniteProduct
17:32:45Complex_Bounded_Operators_Dependencies: theory Real_Impl.Real_Impl
17:32:46Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Ring
17:32:46Complex_Bounded_Operators_Dependencies: theory Show.Shows_Literal
17:32:46Complex_Bounded_Operators_Dependencies: theory VectorSpace.FunctionLemmas
17:32:50Complex_Bounded_Operators_Dependencies: theory HOL-Algebra.Module
17:32:50Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_Ring
17:32:51Complex_Bounded_Operators_Dependencies: theory Containers.Collection_Order
17:32:52Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
17:32:52Complex_Bounded_Operators_Dependencies: theory HOL-Computational_Algebra.Polynomial_Factorial
17:32:53Complex_Bounded_Operators_Dependencies: theory VectorSpace.RingModuleFacts
17:32:54Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Missing_Polynomial
17:32:54Complex_Bounded_Operators_Dependencies: theory VectorSpace.MonoidSums
17:32:55Complex_Bounded_Operators_Dependencies: theory VectorSpace.LinearCombinations
17:32:56Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Order_Polynomial
17:32:56Complex_Bounded_Operators_Dependencies: theory Polynomial_Interpolation.Ring_Hom_Poly
17:32:56Complex_Bounded_Operators_Dependencies: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
17:32:56Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix
17:33:02Complex_Bounded_Operators_Dependencies: theory VectorSpace.SumSpaces
17:33:03Complex_Bounded_Operators_Dependencies: theory VectorSpace.VectorSpace
17:33:03Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
17:33:03Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Show_Matrix
17:33:03Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Shows_Literal_Matrix
17:33:05Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Column_Operations
17:33:05Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant
17:33:09Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Determinant_Impl
17:33:09Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Char_Poly
17:33:10Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form
17:33:10Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Missing_VectorSpace
17:33:14Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.VS_Connect
17:33:29Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gram_Schmidt
17:33:29Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Kernel
17:33:31Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Schur_Decomposition
17:33:36Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
17:33:50Complex_Bounded_Operators_Dependencies: theory Containers.RBT_ext
17:33:50Complex_Bounded_Operators_Dependencies: theory Deriving.RBT_Comparator_Impl
17:34:03Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Mapping2
17:34:05Complex_Bounded_Operators_Dependencies: theory Containers.RBT_Set2
17:34:08Complex_Bounded_Operators_Dependencies: theory Containers.Set_Impl
17:34:32Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_IArray_Impl
17:34:35Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
17:34:37Complex_Bounded_Operators_Dependencies: theory Jordan_Normal_Form.Matrix_Impl
17:38:42Timing Complex_Bounded_Operators_Dependencies (8 threads, 309.317s elapsed time, 2015.189s cpu time, 149.325s GC time, factor 6.51)
17:38:42Finished Complex_Bounded_Operators_Dependencies (0:06:04 elapsed time, 0:35:47 cpu time, factor 5.89)
17:38:42Building Echelon_Form (on hpcisabelle/6) ...
17:38:44Echelon_Form: theory HOL-Library.Code_Abstract_Nat
17:38:44Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field
17:38:44Echelon_Form: theory HOL-Library.Code_Target_Int
17:38:44Echelon_Form: theory HOL-Library.Code_Cardinality
17:38:44Echelon_Form: theory HOL-Library.IArray
17:38:44Echelon_Form: theory HOL-Library.Function_Algebras
17:38:44Echelon_Form: theory HOL-Library.More_List
17:38:44Echelon_Form: theory HOL-Library.Z2
17:38:45Echelon_Form: theory HOL-Library.Code_Target_Nat
17:38:45Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
17:38:45Echelon_Form: theory Cayley_Hamilton.Square_Matrix
17:38:45Echelon_Form: theory HOL-Computational_Algebra.Polynomial
17:38:45Echelon_Form: theory HOL-Library.Code_Target_Numeral
17:38:45Echelon_Form: theory Gauss_Jordan.Code_Set
17:38:45Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
17:38:45Echelon_Form: theory Gauss_Jordan.Code_Z2
17:38:45Echelon_Form: theory Gauss_Jordan.IArray_Addenda
17:38:46Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
17:38:46Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
17:38:50Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
17:38:51Echelon_Form: theory Gauss_Jordan.Code_Matrix
17:38:51Echelon_Form: theory Gauss_Jordan.Rref
17:38:51Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
17:38:52Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
17:38:52Echelon_Form: theory Gauss_Jordan.Rank
17:38:52Echelon_Form: theory Gauss_Jordan.Elementary_Operations
17:38:53Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
17:38:53Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
17:38:55Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
17:38:55Echelon_Form: theory Gauss_Jordan.Linear_Maps
17:38:56Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
17:38:57Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
17:38:57Echelon_Form: theory Gauss_Jordan.Determinants2
17:38:57Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
17:38:57Echelon_Form: theory Gauss_Jordan.Inverse
17:38:58Echelon_Form: theory Gauss_Jordan.System_Of_Equations
17:38:58Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
17:38:58Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
17:38:58Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
17:38:59Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
17:39:00Echelon_Form: theory Echelon_Form.Rings2
17:39:36Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
17:39:37Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
17:39:37Echelon_Form: theory Echelon_Form.Echelon_Form
17:39:40Echelon_Form: theory Echelon_Form.Echelon_Form_Det
17:39:40Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
17:39:40Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
17:39:41Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
17:39:41Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
17:39:42Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
17:39:43Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
17:39:44Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
17:41:32Preparing Echelon_Form/document ...
17:41:37Finished Echelon_Form/document (0:00:05 elapsed time)
17:41:37Preparing Echelon_Form/outline ...
17:41:40Finished Echelon_Form/outline (0:00:03 elapsed time)
17:41:40Timing Echelon_Form (8 threads, 144.675s elapsed time, 888.742s cpu time, 45.234s GC time, factor 6.14)
17:41:40Finished Echelon_Form (0:02:47 elapsed time, 0:15:35 cpu time, factor 5.58)
17:41:41Building Projective_Measurements (on hpcisabelle/7) ...
17:41:45Projective_Measurements: theory HOL-Computational_Algebra.Fraction_Field
17:41:45Projective_Measurements: theory Abstract-Rewriting.Seq
17:41:45Projective_Measurements: theory Jordan_Normal_Form.Missing_Misc
17:41:45Projective_Measurements: theory HOL-Algebra.Congruence
17:41:45Projective_Measurements: theory HOL-Library.More_List
17:41:45Projective_Measurements: theory HOL-Types_To_Sets.Prerequisites
17:41:45Projective_Measurements: theory HOL-Library.While_Combinator
17:41:45Projective_Measurements: theory HOL-Types_To_Sets.Types_To_Sets
17:41:46Projective_Measurements: theory Polynomial_Interpolation.Missing_Unsorted
17:41:46Projective_Measurements: theory Jordan_Normal_Form.Conjugate
17:41:46Projective_Measurements: theory HOL-Computational_Algebra.Polynomial
17:41:46Projective_Measurements: theory HOL-Types_To_Sets.Group_On_With
17:41:46Projective_Measurements: theory Matrix.Utility
17:41:47Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom
17:41:47Projective_Measurements: theory Regular-Sets.Regular_Set
17:41:47Projective_Measurements: theory HOL-Algebra.Order
17:41:47Projective_Measurements: theory HOL-Computational_Algebra.Normalized_Fraction
17:41:47Projective_Measurements: theory VectorSpace.FunctionLemmas
17:41:48Projective_Measurements: theory HOL-Algebra.Lattice
17:41:49Projective_Measurements: theory HOL-Algebra.Complete_Lattice
17:41:51Projective_Measurements: theory HOL-Algebra.Group
17:41:51Projective_Measurements: theory Regular-Sets.Regular_Exp
17:41:53Projective_Measurements: theory HOL-Algebra.Coset
17:41:53Projective_Measurements: theory HOL-Algebra.FiniteProduct
17:41:54Projective_Measurements: theory HOL-Algebra.Ring
17:41:55Projective_Measurements: theory Regular-Sets.NDerivative
17:41:55Projective_Measurements: theory Regular-Sets.Relation_Interpretation
17:41:59Projective_Measurements: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
17:41:59Projective_Measurements: theory HOL-Computational_Algebra.Polynomial_Factorial
17:41:59Projective_Measurements: theory HOL-Algebra.Module
17:41:59Projective_Measurements: theory Jordan_Normal_Form.Missing_Ring
17:41:59Projective_Measurements: theory Regular-Sets.Equivalence_Checking
17:42:00Projective_Measurements: theory Regular-Sets.Regexp_Method
17:42:01Projective_Measurements: theory Polynomial_Interpolation.Missing_Polynomial
17:42:01Projective_Measurements: theory Abstract-Rewriting.Abstract_Rewriting
17:42:02Projective_Measurements: theory VectorSpace.RingModuleFacts
17:42:03Projective_Measurements: theory Polynomial_Factorization.Order_Polynomial
17:42:03Projective_Measurements: theory Polynomial_Interpolation.Ring_Hom_Poly
17:42:03Projective_Measurements: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
17:42:03Projective_Measurements: theory VectorSpace.MonoidSums
17:42:04Projective_Measurements: theory Abstract-Rewriting.SN_Orders
17:42:04Projective_Measurements: theory VectorSpace.LinearCombinations
17:42:06Projective_Measurements: theory Jordan_Normal_Form.Matrix
17:42:07Projective_Measurements: theory Matrix.Ordered_Semiring
17:42:08Projective_Measurements: theory Matrix.Matrix_Legacy
17:42:10Projective_Measurements: theory Matrix_Tensor.Matrix_Tensor
17:42:11Projective_Measurements: theory VectorSpace.SumSpaces
17:42:12Projective_Measurements: theory VectorSpace.VectorSpace
17:42:12Projective_Measurements: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
17:42:14Projective_Measurements: theory Jordan_Normal_Form.Column_Operations
17:42:15Projective_Measurements: theory Jordan_Normal_Form.Determinant
17:42:17Projective_Measurements: theory Jordan_Normal_Form.Char_Poly
17:42:19Projective_Measurements: theory Jordan_Normal_Form.Missing_VectorSpace
17:42:19Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form
17:42:20Projective_Measurements: theory Isabelle_Marries_Dirac.Basics
17:42:20Projective_Measurements: theory Isabelle_Marries_Dirac.Binary_Nat
17:42:20Projective_Measurements: theory Isabelle_Marries_Dirac.Quantum
17:42:22Projective_Measurements: theory Isabelle_Marries_Dirac.Complex_Vectors
17:42:23Projective_Measurements: theory Jordan_Normal_Form.VS_Connect
17:42:23Projective_Measurements: theory Isabelle_Marries_Dirac.Tensor
17:42:25Projective_Measurements: theory Isabelle_Marries_Dirac.More_Tensor
17:42:37Projective_Measurements: theory Jordan_Normal_Form.Gram_Schmidt
17:42:39Projective_Measurements: theory Jordan_Normal_Form.Schur_Decomposition
17:42:44Projective_Measurements: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
17:42:49Projective_Measurements: theory QHLProver.Complex_Matrix
17:43:00Projective_Measurements: theory QHLProver.Gates
17:43:00Projective_Measurements: theory Projective_Measurements.Linear_Algebra_Complements
17:43:07Projective_Measurements: theory Projective_Measurements.Projective_Measurements
17:43:09Projective_Measurements: theory Projective_Measurements.CHSH_Inequality
17:50:44Preparing Projective_Measurements/document ...
17:50:50Finished Projective_Measurements/document (0:00:05 elapsed time)
17:50:50Preparing Projective_Measurements/outline ...
17:50:52Finished Projective_Measurements/outline (0:00:02 elapsed time)
17:50:52Timing Projective_Measurements (8 threads, 498.008s elapsed time, 1495.913s cpu time, 56.942s GC time, factor 3.00)
17:50:52Finished Projective_Measurements (0:08:58 elapsed time, 0:26:28 cpu time, factor 2.95)
17:50:53Running AutoCorres2 (on hpcisabelle/0) ...
17:50:55AutoCorres2: theory AutoCorres2.MkTermAntiquote
17:50:55AutoCorres2: theory AutoCorres2.ML_Fun_Cache
17:50:55AutoCorres2: theory AutoCorres2.TermPatternAntiquote
17:50:55AutoCorres2: theory HOL-Eisbach.Eisbach
17:50:55AutoCorres2: theory AutoCorres2.Apply_Trace
17:50:55AutoCorres2: theory AutoCorres2.ML_Infer_Instantiate
17:50:55AutoCorres2: theory AutoCorres2.Introduction_AutoCorres2
17:50:55AutoCorres2: theory AutoCorres2.ML_Record_Antiquotation
17:50:55AutoCorres2: theory AutoCorres2.MapExtra
17:50:55AutoCorres2: theory AutoCorres2.Misc_Antiquotation
17:50:55AutoCorres2: theory AutoCorres2.MkTermAntiquote_Tests
17:50:55AutoCorres2: theory AutoCorres2.Named_Rules
17:50:55AutoCorres2: theory AutoCorres2.Padding
17:50:55AutoCorres2: theory AutoCorres2.Print_Annotated
17:50:55AutoCorres2: theory AutoCorres2.Option_Scanner
17:50:55AutoCorres2: theory AutoCorres2.AutoCorres_Utils
17:50:55AutoCorres2: theory AutoCorres2.Apply_Trace_Cmd
17:50:55AutoCorres2: theory AutoCorres2.StaticFun
17:50:55AutoCorres2: theory AutoCorres2.Subgoal_Methods
17:50:56AutoCorres2: theory AutoCorres2.Subgoals
17:50:56AutoCorres2: theory AutoCorres2.Target_Architecture
17:50:56AutoCorres2: theory AutoCorres2.TermPatternAntiquote_Tests
17:50:56AutoCorres2: theory AutoCorres2.Tuple_Tools
17:50:56AutoCorres2: theory AutoCorres2.MapExtraTrans
17:50:56AutoCorres2: theory HOL-Library.Adhoc_Overloading
17:50:56AutoCorres2: theory HOL-Library.Code_Abstract_Nat
17:50:56AutoCorres2: theory HOL-Library.Complete_Partial_Order2
17:50:56AutoCorres2: theory HOL-Library.Code_Binary_Nat
17:50:56AutoCorres2: theory HOL-Library.Monad_Syntax
17:50:57AutoCorres2: theory AutoCorres2.Less_Monad_Syntax
17:50:57AutoCorres2: theory HOL-Library.Phantom_Type
17:50:57AutoCorres2: theory HOL-Library.Signed_Division
17:50:57AutoCorres2: theory HOL-Eisbach.Eisbach_Tools
17:50:57AutoCorres2: theory AutoCorres2.Tagging
17:50:57AutoCorres2: theory AutoCorres2.Cong_Tactic
17:50:57AutoCorres2: theory AutoCorres2.Match_Cterm
17:50:57AutoCorres2: theory AutoCorres2.Simp_Trace
17:50:58AutoCorres2: theory AutoCorres2.Rule_By_Method
17:50:58AutoCorres2: theory HOL-Library.Sublist
17:50:58AutoCorres2: theory AutoCorres2.PrettyProgs
17:50:58AutoCorres2: theory AutoCorres2.Basic_Runs_To_VCG
17:50:58AutoCorres2: theory AutoCorres2.IndirectCalls
17:50:58AutoCorres2: theory HOL-Library.Cardinality
17:50:59AutoCorres2: theory Word_Lib.Enumeration
17:50:59AutoCorres2: theory Word_Lib.Even_More_List
17:51:00AutoCorres2: theory Word_Lib.More_Bit_Ring
17:51:00AutoCorres2: theory AutoCorres2.Eisbach_Methods
17:51:00AutoCorres2: theory Word_Lib.More_Misc
17:51:00AutoCorres2: theory HOL-Library.Numeral_Type
17:51:01AutoCorres2: theory AutoCorres2.Runs_To_VCG
17:51:01AutoCorres2: theory AutoCorres2.Arrays
17:51:01AutoCorres2: theory HOL-Library.Type_Length
17:51:01AutoCorres2: theory HOL-Library.Prefix_Order
17:51:01AutoCorres2: theory Word_Lib.More_Sublist
17:51:02AutoCorres2: theory HOL-Library.Word
17:51:02AutoCorres2: theory Word_Lib.More_Arithmetic
17:51:02AutoCorres2: theory AutoCorres2.Mutual_CCPO_Recursion
17:51:02AutoCorres2: theory AutoCorres2.Spec_Monad
17:51:09AutoCorres2: theory AutoCorres2.Synthesize
17:51:13AutoCorres2: theory Word_Lib.Bit_Comprehension
17:51:13AutoCorres2: theory Word_Lib.Hex_Words
17:51:13AutoCorres2: theory Word_Lib.Legacy_Aliases
17:51:13AutoCorres2: theory Word_Lib.More_Divides
17:51:13AutoCorres2: theory Word_Lib.Signed_Words
17:51:13AutoCorres2: theory Word_Lib.Syntax_Bundles
17:51:13AutoCorres2: theory Word_Lib.Type_Syntax
17:51:13AutoCorres2: theory Word_Lib.Word_Syntax
17:51:13AutoCorres2: theory Word_Lib.Norm_Words
17:51:13AutoCorres2: theory Word_Lib.Word_Names
17:51:14AutoCorres2: theory Word_Lib.Signed_Division_Word
17:51:14AutoCorres2: theory Word_Lib.More_Word
17:51:14AutoCorres2: theory AutoCorres2.Reaches
17:51:15AutoCorres2: theory Word_Lib.Bit_Comprehension_Int
17:51:15AutoCorres2: theory Word_Lib.Bit_Shifts_Infix_Syntax
17:51:15AutoCorres2: theory Word_Lib.Enumeration_Word
17:51:15AutoCorres2: theory Word_Lib.Least_significant_bit
17:51:15AutoCorres2: theory Word_Lib.Many_More
17:51:15AutoCorres2: theory Word_Lib.Strict_part_mono
17:51:15AutoCorres2: theory Word_Lib.Word_16
17:51:16AutoCorres2: theory AutoCorres2.Distinct_Prop
17:51:16AutoCorres2: theory AutoCorres2.Lens
17:51:17AutoCorres2: theory Word_Lib.Aligned
17:51:17AutoCorres2: theory Word_Lib.Singleton_Bit_Shifts
17:51:17AutoCorres2: theory Word_Lib.Most_significant_bit
17:51:17AutoCorres2: theory Word_Lib.Generic_set_bit
17:51:17AutoCorres2: theory Word_Lib.Sgn_Abs
17:51:18AutoCorres2: theory Word_Lib.Next_and_Prev
17:51:18AutoCorres2: theory Word_Lib.Word_EqI
17:51:18AutoCorres2: theory Word_Lib.Bits_Int
17:51:21AutoCorres2: theory Word_Lib.Boolean_Inequalities
17:51:23AutoCorres2: theory Word_Lib.Rsplit
17:51:23AutoCorres2: theory Word_Lib.Typedef_Morphisms
17:51:23AutoCorres2: theory Word_Lib.Reversed_Bit_Lists
17:51:24AutoCorres2: theory Word_Lib.Word_Lemmas
17:51:27AutoCorres2: theory Word_Lib.Bitwise
17:51:27AutoCorres2: theory Word_Lib.Word_8
17:51:27AutoCorres2: theory Word_Lib.More_Word_Operations
17:51:27AutoCorres2: theory Word_Lib.Bitwise_Signed
17:51:29AutoCorres2: theory AutoCorres2.Word_Lemmas_Internal
17:51:29AutoCorres2: theory Word_Lib.Word_32
17:51:29AutoCorres2: theory Word_Lib.Word_64
17:51:30AutoCorres2: theory Word_Lib.Machine_Word_64_Basics
17:51:30AutoCorres2: theory Word_Lib.Machine_Word_64
17:51:30AutoCorres2: theory Word_Lib.Machine_Word_32_Basics
17:51:30AutoCorres2: theory Word_Lib.Word_Lib_Sumo
17:51:30AutoCorres2: theory Word_Lib.Machine_Word_32
17:51:33AutoCorres2: theory AutoCorres2.More_Lib
17:51:33AutoCorres2: theory AutoCorres2.Word_Lemmas_32_Internal
17:51:33AutoCorres2: theory AutoCorres2.Word_Lemmas_64_Internal
17:51:34AutoCorres2: theory AutoCorres2.WordSetup
17:51:34AutoCorres2: theory AutoCorres2.Addr_Type_ARM
17:51:34AutoCorres2: theory AutoCorres2.Addr_Type_ARM64
17:51:34AutoCorres2: theory AutoCorres2.Addr_Type_ARM_HYP
17:51:34AutoCorres2: theory AutoCorres2.Addr_Type_RISCV64
17:51:34AutoCorres2: theory AutoCorres2.Addr_Type_X64
17:51:35AutoCorres2: theory AutoCorres2.Addr_Type
17:51:36AutoCorres2: theory AutoCorres2.NatBitwise
17:51:36AutoCorres2: theory AutoCorres2.Reader_Monad
17:51:36AutoCorres2: theory AutoCorres2.CTypesBase
17:51:37AutoCorres2: theory AutoCorres2.Option_MonadND
17:51:39AutoCorres2: theory AutoCorres2.CTypesDefs
17:51:53AutoCorres2: theory AutoCorres2.CTypes
17:51:57AutoCorres2: theory AutoCorres2.HeapRawState
17:51:57AutoCorres2: theory AutoCorres2.Vanilla32_Preliminaries
17:51:57AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM
17:51:58AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM64
17:51:58AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
17:51:58AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_RISCV64
17:51:58AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_X64
17:51:58AutoCorres2: theory AutoCorres2.Word_Mem_Encoding
17:51:58AutoCorres2: theory AutoCorres2.Vanilla32
17:51:59AutoCorres2: theory AutoCorres2.CompoundCTypes
17:52:05AutoCorres2: theory AutoCorres2.ArraysMemInstance
17:52:06AutoCorres2: theory AutoCorres2.ArchArraysMemInstance
17:52:09AutoCorres2: theory AutoCorres2.TypHeap
17:52:17AutoCorres2: theory AutoCorres2.Separation_UMM
17:52:18AutoCorres2: theory AutoCorres2.SepCode
17:52:20AutoCorres2: theory AutoCorres2.SepInv
17:52:21AutoCorres2: theory AutoCorres2.SepTactic
17:52:22AutoCorres2: theory AutoCorres2.SepFrame
17:52:24AutoCorres2: theory AutoCorres2.StructSupport
17:52:25AutoCorres2: theory AutoCorres2.ArrayAssertion
17:52:25AutoCorres2: theory AutoCorres2.CProof
17:52:35AutoCorres2: theory AutoCorres2.CLanguage
17:52:35AutoCorres2: theory AutoCorres2.Padding_Equivalence
17:52:35AutoCorres2: theory AutoCorres2.PackedTypes
17:52:42AutoCorres2: theory AutoCorres2.ModifiesProofs
17:52:45AutoCorres2: theory AutoCorres2.UMM
17:52:53AutoCorres2: theory AutoCorres2.CLocals
17:52:56AutoCorres2: theory AutoCorres2.CTranslationSetup
17:53:25AutoCorres2: theory AutoCorres2.Array_Selectors
17:53:25AutoCorres2: theory AutoCorres2.CTranslation
17:53:26AutoCorres2: theory AutoCorres2.CTranslationInfrastructure
17:53:26AutoCorres2: theory AutoCorres2.TypHeapLib
17:53:26AutoCorres2: theory AutoCorres2.AbstractArrays
17:53:26AutoCorres2: theory AutoCorres2.LemmaBucket_C
17:53:27AutoCorres2: theory AutoCorres2.AutoCorres_Base
17:53:31AutoCorres2: theory AutoCorres2.SimplBucket
17:53:31AutoCorres2: theory AutoCorres2.TypHeapSimple
17:53:32AutoCorres2: theory AutoCorres2.AutoCorresSimpset
17:53:32AutoCorres2: theory AutoCorres2.CCorresE
17:53:33AutoCorres2: theory AutoCorres2.CorresXF
17:53:33AutoCorres2: theory AutoCorres2.L1Defs
17:53:36AutoCorres2: theory AutoCorres2.L1Peephole
17:53:36AutoCorres2: theory AutoCorres2.L1Valid
17:53:36AutoCorres2: theory AutoCorres2.ExceptionRewrite
17:53:36AutoCorres2: theory AutoCorres2.SimplConv
17:53:36AutoCorres2: theory AutoCorres2.L2Defs
17:53:41AutoCorres2: theory AutoCorres2.Split_Heap
17:53:44AutoCorres2: theory AutoCorres2.L2ExceptionRewrite
17:53:45AutoCorres2: theory AutoCorres2.L2Peephole
17:53:45AutoCorres2: theory AutoCorres2.LocalVarExtract
17:53:46AutoCorres2: theory AutoCorres2.Stack_Typing
17:53:46AutoCorres2: theory AutoCorres2.WordAbstract
17:53:47AutoCorres2: theory AutoCorres2.Refines_Spec
17:53:48AutoCorres2: theory AutoCorres2.In_Out_Parameters
17:53:49AutoCorres2: theory AutoCorres2.WordPolish
17:54:05AutoCorres2: theory AutoCorres2.HeapLift
17:54:07AutoCorres2: theory AutoCorres2.TypeStrengthen
17:54:29AutoCorres2: theory AutoCorres2.Polish
17:54:29AutoCorres2: theory AutoCorres2.Runs_To_VCG_StackPointer
17:54:38AutoCorres2: theory AutoCorres2.AutoCorres
17:55:05AutoCorres2: theory AutoCorres2.AutoCorresInfrastructure
17:55:05AutoCorres2: theory AutoCorres2.Chapter1_MinMax
17:55:05AutoCorres2: theory AutoCorres2.In_Out_Parameters_Ex
17:55:05AutoCorres2: theory AutoCorres2.Chapter2_HoareHeap
17:55:05AutoCorres2: theory AutoCorres2.Chapter3_HoareHeap
17:55:05AutoCorres2: theory AutoCorres2.fnptr
17:55:05AutoCorres2: theory AutoCorres2.open_struct
17:55:05AutoCorres2: theory AutoCorres2.pointers_to_locals
17:55:14AutoCorres2: theory AutoCorres2.union_ac
17:58:55AutoCorres2: theory AutoCorres2.AutoCorres_Documentation
17:59:40Preparing AutoCorres2/document ...
18:01:17Finished AutoCorres2/document (0:01:37 elapsed time)
18:01:17Preparing AutoCorres2/outline ...
18:02:13Finished AutoCorres2/outline (0:00:56 elapsed time)
18:02:14Timing AutoCorres2 (8 threads, 507.062s elapsed time, 3378.150s cpu time, 103.635s GC time, factor 6.66)
18:02:14Finished AutoCorres2 (0:08:33 elapsed time, 0:56:47 cpu time, factor 6.64)
18:02:14Running HOL-ODE-Examples (on hpcisabelle/1) ...
18:02:18HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
18:02:18HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
18:02:18HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
18:04:20HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
18:10:29Timing HOL-ODE-Examples (8 threads, 490.079s elapsed time, 1755.693s cpu time, 9.136s GC time, factor 3.58)
18:10:29Finished HOL-ODE-Examples (0:08:14 elapsed time, 0:29:21 cpu time, factor 3.56)
18:10:30Building Deriving (on hpcisabelle/2) ...
18:10:31Deriving: theory Deriving.Comparator
18:10:31Deriving: theory Deriving.Derive_Manager
18:10:31Deriving: theory Deriving.Generator_Aux
18:10:31Deriving: theory Word_Lib.More_Divides
18:10:31Deriving: theory Word_Lib.Bit_Comprehension
18:10:31Deriving: theory Word_Lib.Signed_Division_Word
18:10:31Deriving: theory Native_Word.Code_Int_Integer_Conversion
18:10:31Deriving: theory Word_Lib.More_Arithmetic
18:10:32Deriving: theory Word_Lib.More_Bit_Ring
18:10:32Deriving: theory Deriving.Countable_Generator
18:10:32Deriving: theory Deriving.Equality_Generator
18:10:33Deriving: theory Deriving.Equality_Instances
18:10:33Deriving: theory Deriving.Compare
18:10:33Deriving: theory Deriving.Comparator_Generator
18:10:33Deriving: theory Deriving.RBT_Comparator_Impl
18:10:34Deriving: theory Word_Lib.More_Word
18:10:34Deriving: theory Deriving.Compare_Generator
18:10:35Deriving: theory Deriving.RBT_Compare_Order_Impl
18:10:35Deriving: theory Deriving.Compare_Instances
18:10:35Deriving: theory Deriving.Compare_Rat
18:10:35Deriving: theory Deriving.Compare_Real
18:10:36Deriving: theory Deriving.Compare_Order_Instances
18:10:36Deriving: theory Native_Word.Code_Target_Word_Base
18:10:36Deriving: theory Word_Lib.Bit_Shifts_Infix_Syntax
18:10:36Deriving: theory Word_Lib.Least_significant_bit
18:10:38Deriving: theory Word_Lib.Most_significant_bit
18:10:38Deriving: theory Word_Lib.Generic_set_bit
18:10:39Deriving: theory Native_Word.Code_Target_Integer_Bit
18:10:39Deriving: theory Native_Word.Word_Type_Copies
18:10:53Deriving: theory Native_Word.Uint32
18:10:55Deriving: theory Collections.HashCode
18:10:55Deriving: theory Deriving.Hash_Generator
18:10:56Deriving: theory Deriving.Hash_Instances
18:10:56Deriving: theory Deriving.Derive
18:10:57Deriving: theory Deriving.Derive_Examples
18:11:29Preparing Deriving/document ...
18:11:33Finished Deriving/document (0:00:03 elapsed time)
18:11:33Preparing Deriving/outline ...
18:11:36Finished Deriving/outline (0:00:03 elapsed time)
18:11:36Timing Deriving (8 threads, 40.348s elapsed time, 150.993s cpu time, 4.308s GC time, factor 3.74)
18:11:36Finished Deriving (0:00:59 elapsed time, 0:03:10 cpu time, factor 3.21)
18:11:36Running BTree (on hpcisabelle/3) ...
18:11:39BTree: theory HOL-Data_Structures.Cmp
18:11:39BTree: theory HOL-Data_Structures.Less_False
18:11:39BTree: theory HOL-Library.Sublist
18:11:39BTree: theory HOL-Data_Structures.Sorted_Less
18:11:40BTree: theory HOL-Data_Structures.List_Ins_Del
18:11:40BTree: theory BTree.BTree
18:11:40BTree: theory BTree.BPlusTree
18:11:40BTree: theory HOL-Data_Structures.Set_Specs
18:11:43BTree: theory BTree.BTree_Height
18:11:43BTree: theory BTree.BTree_Set
18:11:45BTree: theory BTree.BPlusTree_Split
18:11:45BTree: theory BTree.BPlusTree_Set
18:11:45BTree: theory BTree.BPlusTree_Range
18:11:49BTree: theory BTree.BTree_Split
18:11:53BTree: theory BTree.BPlusTree_SplitCE
18:13:15Build timed out (after 300 minutes). Marking the build as failed.
18:13:15Build was aborted
18:17:36Started calculate disk usage of build
18:17:37Finished Calculation of disk usage of build in 0 seconds
18:17:37Started calculate disk usage of workspace
18:17:38Finished Calculation of disk usage of workspace in 1 second
18:17:40No emails were triggered.
18:17:40Finished: FAILURE
![[Jenkins]](/jenkins/static/858a1f95/images/svgs/logo.svg){kind=logo}
