17:24:32QR_Decomposition: theory HOL-Library.Function_Algebras
17:24:32QR_Decomposition: theory HOL-Library.Code_Target_Numeral
17:24:32QR_Decomposition: theory HOL-Library.IArray
17:24:33QR_Decomposition: theory Gauss_Jordan.Code_Set
17:24:33QR_Decomposition: theory Cauchy.CauchysMeanTheorem
17:24:33QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float
17:24:34QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
17:24:34QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
17:24:34QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR
17:24:34QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order
17:24:34QR_Decomposition: theory Sqrt_Babylonian.Log_Impl
17:24:34QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type
17:24:34QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl
17:24:35QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian
17:24:36QR_Decomposition: theory Real_Impl.Prime_Product
17:24:37QR_Decomposition: theory Real_Impl.Real_Impl
17:24:37QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous
17:24:37QR_Decomposition: theory Show.Show
17:24:38QR_Decomposition: theory Show.Show_Instances
17:24:38QR_Decomposition: theory Gauss_Jordan.Code_Matrix
17:24:39QR_Decomposition: theory Gauss_Jordan.Rref
17:24:39QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces
17:24:40QR_Decomposition: theory Gauss_Jordan.Elementary_Operations
17:24:40QR_Decomposition: theory QR_Decomposition.Generalizations2
17:24:41QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR
17:24:42QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula
17:24:42QR_Decomposition: theory Gauss_Jordan.Rank
17:24:42QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan
17:24:44QR_Decomposition: theory Show.Show_Real
17:24:44QR_Decomposition: theory Real_Impl.Real_Unique_Impl
17:24:44QR_Decomposition: theory Gauss_Jordan.Linear_Maps
17:24:45QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA
17:24:46QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
17:24:46QR_Decomposition: theory Gauss_Jordan.Determinants2
17:24:46Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
17:24:46QR_Decomposition: theory Gauss_Jordan.Inverse
17:24:47QR_Decomposition: theory Gauss_Jordan.System_Of_Equations
17:24:47QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
17:24:48QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR
17:24:49HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
17:24:49QR_Decomposition: theory QR_Decomposition.Projections
17:24:49QR_Decomposition: theory QR_Decomposition.Gram_Schmidt
17:24:50QR_Decomposition: theory QR_Decomposition.QR_Decomposition
17:24:50Timing Linear_Recurrences (2 threads, 15.556s elapsed time, 30.464s cpu time, 1.808s GC time, factor 1.96)
17:24:50Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences
17:24:50Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences/document.pdf
17:24:50Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences/outline.pdf
17:24:50Finished Linear_Recurrences (0:01:04 elapsed time, 0:01:34 cpu time, factor 1.48)
17:24:50Running Linear_Recurrences_Test ...
17:24:50QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float
17:24:50QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays
17:24:51QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays
17:24:51QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float
17:24:52QR_Decomposition: theory QR_Decomposition.QR_Efficient
17:24:53QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation
17:24:53QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic
17:24:59Linear_Recurrences_Test: theory Linear_Recurrences_Test.Eulerian_Polynomials
17:24:59Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Common
17:24:59Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Misc
17:25:00Linear_Recurrences_Test: theory Linear_Recurrences_Test.Pochhammer_Polynomials
17:25:00Linear_Recurrences_Test: theory Linear_Recurrences_Test.Factorizations
17:25:00QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic
17:25:00Linear_Recurrences_Test: theory Linear_Recurrences_Test.RatFPS
17:25:01Linear_Recurrences_Test: theory Linear_Recurrences_Test.Partial_Fraction_Decomposition
17:25:03Linear_Recurrences_Test: theory Linear_Recurrences_Test.Rational_FPS_Solver
17:25:03Linear_Recurrences_Test: theory Linear_Recurrences_Test.Show_RatFPS
17:25:03Linear_Recurrences_Test: theory Show.Show_Complex
17:25:04Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Homogenous_Recurrences
17:25:04Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Pretty
17:25:06Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Inhomogenous_Recurrences
17:25:06Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Solver
17:25:12Linear_Recurrences_Test: theory Linear_Recurrences_Test.Linear_Recurrences_Test
17:27:48Timing Differential_Dynamic_Logic (2 threads, 245.306s elapsed time, 411.132s cpu time, 24.036s GC time, factor 1.68)
17:27:48Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Differential_Dynamic_Logic
17:27:48Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Differential_Dynamic_Logic/document.pdf
17:27:48Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Differential_Dynamic_Logic/outline.pdf
17:27:48Finished Differential_Dynamic_Logic (0:04:16 elapsed time, 0:07:08 cpu time, factor 1.67)
17:27:48Collections_Examples CANCELLED
17:27:48Running Containers-Benchmarks ...
17:27:50Containers-Benchmarks: theory HOL-Eisbach.Eisbach
17:27:50Containers-Benchmarks: theory Automatic_Refinement.Foldi
17:27:50Containers-Benchmarks: theory Automatic_Refinement.Prio_List
17:27:50Containers-Benchmarks: theory Automatic_Refinement.Refine_Util_Bootstrap1
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Mk_Term_Antiquot
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Mpat_Antiquot
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Refine_Util
17:27:51Containers-Benchmarks: theory Collections.ICF_Tools
17:27:51Containers-Benchmarks: theory Collections.Ord_Code_Preproc
17:27:51Containers-Benchmarks: theory Collections.Locale_Code
17:27:51Containers-Benchmarks: theory Collections.Record_Intf
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Anti_Unification
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Attr_Comb
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Autoref_Data
17:27:51Containers-Benchmarks: theory Automatic_Refinement.Indep_Vars
17:27:52Containers-Benchmarks: theory Automatic_Refinement.Named_Sorted_Thms
17:27:52Containers-Benchmarks: theory Automatic_Refinement.Mk_Record_Simp
17:27:52Containers-Benchmarks: theory Automatic_Refinement.Tagged_Solver
17:27:52Containers-Benchmarks: theory Automatic_Refinement.Select_Solve
17:27:52Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Comparison
17:27:52Containers-Benchmarks: theory Finger-Trees.FingerTree
17:27:53Containers-Benchmarks: theory Trie.Trie
17:27:55Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
17:27:55Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
17:27:55Perron_Frobenius: theory Perron_Frobenius.Roots_Unity
17:27:55Containers-Benchmarks: theory Binomial-Heaps.BinomialHeap
17:27:55Perron_Frobenius: theory Perron_Frobenius.HMA_Connect
17:27:56Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan
17:27:59Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux
17:27:59Containers-Benchmarks: theory Binomial-Heaps.SkewBinomialHeap
17:28:00Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius
17:28:01Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible
17:28:02Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory
17:28:03Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General
17:28:04Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block
17:28:05Containers-Benchmarks: theory HOL-ex.Quicksort
17:28:05Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Default
17:28:06Containers-Benchmarks: theory Automatic_Refinement.Misc
17:28:07Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2
17:28:08Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth
17:28:13Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_RBT
17:28:15Containers-Benchmarks: theory Automatic_Refinement.Refine_Lib
17:28:16Containers-Benchmarks: theory Collections.SetIterator
17:28:16Containers-Benchmarks: theory Automatic_Refinement.Autoref_Phases
17:28:16Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tagging
17:28:16Containers-Benchmarks: theory Automatic_Refinement.Relators
17:28:17Containers-Benchmarks: theory Collections.SetIteratorOperations
17:28:18Containers-Benchmarks: theory Automatic_Refinement.Param_Tool
17:28:18Containers-Benchmarks: theory Automatic_Refinement.Param_HOL
17:28:19Containers-Benchmarks: theory Automatic_Refinement.Parametricity
17:28:19Containers-Benchmarks: theory Automatic_Refinement.Autoref_Id_Ops
17:28:19Containers-Benchmarks: theory Collections.Assoc_List
17:28:20Containers-Benchmarks: theory Collections.Diff_Array
17:28:21Containers-Benchmarks: theory Automatic_Refinement.Autoref_Fix_Rel
17:28:21Containers-Benchmarks: theory Automatic_Refinement.Autoref_Translate
17:28:21Containers-Benchmarks: theory Automatic_Refinement.Autoref_Gen_Algo
17:28:21Containers-Benchmarks: theory Automatic_Refinement.Autoref_Relator_Interface
17:28:21Containers-Benchmarks: theory Automatic_Refinement.Autoref_Tool
17:28:22Containers-Benchmarks: theory Automatic_Refinement.Autoref_Bindings_HOL
17:28:25Timing QR_Decomposition (2 threads, 227.316s elapsed time, 410.312s cpu time, 18.336s GC time, factor 1.81)
17:28:25Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/QR_Decomposition
17:28:25Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/QR_Decomposition/document.pdf
17:28:25Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/QR_Decomposition/outline.pdf
17:28:25Finished QR_Decomposition (0:03:54 elapsed time, 0:07:01 cpu time, factor 1.80)
17:28:25Running CoreC++ ...
17:28:25Timing Linear_Recurrences_Test (2 threads, 204.550s elapsed time, 378.648s cpu time, 44.396s GC time, factor 1.85)
17:28:25Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Linear_Recurrences_Test
17:28:25Finished Linear_Recurrences_Test (0:03:34 elapsed time, 0:06:28 cpu time, factor 1.81)
17:28:25Running LOFT ...
17:28:25Containers-Benchmarks: theory Automatic_Refinement.Automatic_Refinement
17:28:25Containers-Benchmarks: theory Collections.Idx_Iterator
17:28:26Containers-Benchmarks: theory Collections.Trie_Impl
17:28:26CoreC++: theory CoreC++.Auxiliary
17:28:27Containers-Benchmarks: theory Collections.Trie2
17:28:27CoreC++: theory CoreC++.Type
17:28:27Containers-Benchmarks: theory Collections.Dlist_add
17:28:27Containers-Benchmarks: theory Collections.Proper_Iterator
17:28:27LOFT: theory LOFT.OpenFlow_Helpers
17:28:27LOFT: theory LOFT.Sort_Descending
17:28:28Containers-Benchmarks: theory Collections.It_to_It
17:28:28Containers-Benchmarks: theory Collections.SetIteratorGA
17:28:28LOFT: theory LOFT.List_Group
17:28:28CoreC++: theory CoreC++.Value
17:28:29Containers-Benchmarks: theory Collections.Sorted_List_Operations
17:28:29LOFT: theory HOL-Library.List_Lexorder
17:28:29LOFT: theory LOFT.Semantics_OpenFlow
17:28:29LOFT: theory LOFT.OpenFlow_Matches
17:28:29CoreC++: theory CoreC++.Expr
17:28:30Containers-Benchmarks: theory Collections.DatRef
17:28:30Containers-Benchmarks: theory Native_Word.Code_Target_Bits_Int
17:28:31Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set
17:28:31Containers-Benchmarks: theory Collections.Code_Target_ICF
17:28:31Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Bool
17:28:31Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_LC
17:28:32Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_Default
17:28:33Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_Set_LC
17:28:33Timing Perron_Frobenius (2 threads, 298.037s elapsed time, 518.040s cpu time, 25.636s GC time, factor 1.74)
17:28:33Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius
17:28:33Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/document.pdf
17:28:33Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perron_Frobenius/outline.pdf
17:28:33Finished Perron_Frobenius (0:05:07 elapsed time, 0:08:51 cpu time, factor 1.73)
17:28:33Promela CANCELLED
17:28:33Running Dependent_SIFUM_Refinement ...
17:28:34LOFT: theory LOFT.Featherweight_OpenFlow_Comparison
17:28:34CoreC++: theory CoreC++.Decl
17:28:34CoreC++: theory CoreC++.ClassRel
17:28:34Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.CompositionalRefinement
17:28:35Containers-Benchmarks: theory Containers-Benchmarks.Clauses
17:28:35CoreC++: theory CoreC++.SubObj
17:28:35Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
17:28:35Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
17:28:36Containers-Benchmarks: theory Refine_Monadic.Refine_Chapter
17:28:36Containers-Benchmarks: theory Refine_Monadic.Refine_Mono_Prover
17:28:36Containers-Benchmarks: theory Refine_Monadic.Refine_Misc
17:28:36Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
17:28:37Containers-Benchmarks: theory Refine_Monadic.RefineG_Domain
17:28:37CoreC++: theory CoreC++.Objects
17:28:37CoreC++: theory CoreC++.TypeRel
17:28:37CoreC++: theory CoreC++.Exceptions
17:28:37LOFT: theory LOFT.OpenFlow_Action
17:28:37CoreC++: theory CoreC++.State
17:28:37Containers-Benchmarks: theory Refine_Monadic.RefineG_Transfer
17:28:37CoreC++: theory CoreC++.Syntax
17:28:37CoreC++: theory CoreC++.SystemClasses
17:28:37CoreC++: theory CoreC++.BigStep
17:28:37CoreC++: theory CoreC++.SmallStep
17:28:37Containers-Benchmarks: theory Refine_Monadic.RefineG_Assert
17:28:38Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
17:28:38Containers-Benchmarks: theory Refine_Monadic.RefineG_Recursion
17:28:38Containers-Benchmarks: theory Refine_Monadic.RefineG_While
17:28:39LOFT: theory LOFT.OpenFlow_Serialize
17:28:39Containers-Benchmarks: theory Refine_Monadic.Refine_Det
17:28:40Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
17:28:40Containers-Benchmarks: theory Refine_Monadic.Refine_Basic
17:28:43CoreC++: theory CoreC++.DefAss
17:28:43Containers-Benchmarks: theory Refine_Monadic.Refine_Heuristics
17:28:43Containers-Benchmarks: theory Refine_Monadic.Refine_Leof
17:28:43CoreC++: theory CoreC++.WellType
17:28:43Containers-Benchmarks: theory Refine_Monadic.Refine_Pfun
17:28:44Containers-Benchmarks: theory Refine_Monadic.Refine_More_Comb
17:28:44Containers-Benchmarks: theory Refine_Monadic.Refine_While
17:28:44CoreC++: theory CoreC++.Annotate
17:28:45CoreC++: theory CoreC++.Execute
17:28:45CoreC++: theory CoreC++.WellForm
17:28:45LOFT: theory LOFT.LinuxRouter_OpenFlow_Translation
17:28:45Containers-Benchmarks: theory Refine_Monadic.Refine_Transfer
17:28:46Containers-Benchmarks: theory Refine_Monadic.Autoref_Monadic
17:28:46Containers-Benchmarks: theory Refine_Monadic.Refine_Automation
17:28:46Containers-Benchmarks: theory Refine_Monadic.Refine_Foreach
17:28:46CoreC++: theory CoreC++.WellTypeRT
17:28:48Timing Stochastic_Matrices (2 threads, 343.650s elapsed time, 553.896s cpu time, 27.648s GC time, factor 1.61)
17:28:48Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stochastic_Matrices
17:28:48Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stochastic_Matrices/document.pdf
17:28:48Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stochastic_Matrices/outline.pdf
17:28:48Finished Stochastic_Matrices (0:05:49 elapsed time, 0:09:22 cpu time, factor 1.61)
17:28:48Running Gromov_Hyperbolicity ...
17:28:48CoreC++: theory CoreC++.Conform
17:28:49CoreC++: theory CoreC++.WWellForm
17:28:49LOFT: theory LOFT.OpenFlow_Documentation
17:28:49Containers-Benchmarks: theory Refine_Monadic.Refine_Monadic
17:28:49CoreC++: theory CoreC++.CWellForm
17:28:49Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Relation_More
17:28:49Gromov_Hyperbolicity: theory HOL-Cardinals.Fun_More
17:28:49LOFT: theory LOFT.OF_conv_test
17:28:49Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Union
17:28:49Gromov_Hyperbolicity: theory HOL-Decision_Procs.Dense_Linear_Order
17:28:49Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More
17:28:49Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation
17:28:49CoreC++: theory CoreC++.Equivalence
17:28:50Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding
17:28:50Containers-Benchmarks: theory Collections.Gen_Iterator
17:28:50Containers-Benchmarks: theory Collections.Intf_Map
17:28:50Gromov_Hyperbolicity: theory HOL-Library.Cardinal_Notations
17:28:50Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions
17:28:50LOFT: theory LOFT.RFC2544
17:28:51Containers-Benchmarks: theory Collections.Intf_Set
17:28:51Containers-Benchmarks: theory Collections.Iterator
17:28:51Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation
17:28:51Containers-Benchmarks: theory Collections.Array_Iterator
17:28:52Containers-Benchmarks: theory Collections.ICF_Spec_Base
17:28:52Containers-Benchmarks: theory Collections.RBT_add
17:28:52Containers-Benchmarks: theory Collections.AnnotatedListSpec
17:28:52CoreC++: theory CoreC++.Progress
17:28:52Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat
17:28:52Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat
17:28:52Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int
17:28:52Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral
17:28:53Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras
17:28:53Gromov_Hyperbolicity: theory HOL-Library.Log_Nat
17:28:53Gromov_Hyperbolicity: theory Ergodic_Theory.Fekete
17:28:53Containers-Benchmarks: theory Collections.ListSpec
17:28:53Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements
17:28:54CoreC++: theory CoreC++.HeapExtension
17:28:54CoreC++: theory CoreC++.TypeSafe
17:28:54Containers-Benchmarks: theory Collections.FTAnnotatedListImpl
17:28:55Containers-Benchmarks: theory Collections.ListGA
17:28:55CoreC++: theory CoreC++.Determinism
17:28:55Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg2
17:28:55Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.EgHighBranchRevC
17:28:56Containers-Benchmarks: theory Collections.Fifo
17:28:56Containers-Benchmarks: theory Collections.MapSpec
17:28:56Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln
17:28:56Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance
17:28:56Containers-Benchmarks: theory Collections.PrioSpec
17:28:57Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries
17:28:58Containers-Benchmarks: theory Collections.BinoPrioImpl
17:28:58Gromov_Hyperbolicity: theory HOL-Library.Float
17:28:58Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1
17:28:58Containers-Benchmarks: theory Collections.PrioByAnnotatedList
17:28:59Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion
17:29:00Containers-Benchmarks: theory Collections.SkewPrioImpl
17:29:01Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds
17:29:01Containers-Benchmarks: theory Collections.FTPrioImpl
17:29:01Containers-Benchmarks: theory Collections.PrioUniqueSpec
17:29:02Containers-Benchmarks: theory Collections.SetSpec
17:29:02Containers-Benchmarks: theory Collections.PrioUniqueByAnnotatedList
17:29:03Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2
17:29:05Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation
17:29:05Containers-Benchmarks: theory Collections.FTPrioUniqueImpl
17:29:06Containers-Benchmarks: theory Collections.Algos
17:29:07Containers-Benchmarks: theory Collections.SetIndex
17:29:07Containers-Benchmarks: theory Collections.SetIteratorCollectionsGA
17:29:08Containers-Benchmarks: theory Collections.MapGA
17:29:08Containers-Benchmarks: theory Collections.SetGA
17:29:10Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple
17:29:10Containers-Benchmarks: theory Collections.ArrayMapImpl
17:29:12Containers-Benchmarks: theory Collections.ListMapImpl
17:29:13Containers-Benchmarks: theory Collections.ListMapImpl_Invar
17:29:14Containers-Benchmarks: theory Collections.ArrayHashMap_Impl
17:29:15Containers-Benchmarks: theory Collections.TrieMapImpl
17:29:15Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial
17:29:16Containers-Benchmarks: theory Collections.ListSetImpl
17:29:17Containers-Benchmarks: theory Collections.ArrayHashMap
17:29:18Containers-Benchmarks: theory Collections.ListSetImpl_Invar
17:29:19Containers-Benchmarks: theory Collections.ListSetImpl_NotDist
17:29:19Containers-Benchmarks: theory Collections.ListSetImpl_Sorted
17:29:21Containers-Benchmarks: theory Collections.SetByMap
17:29:22Containers-Benchmarks: theory Collections.RBTMapImpl
17:29:23Containers-Benchmarks: theory Collections.ArrayHashSet
17:29:25Containers-Benchmarks: theory Collections.ArraySetImpl
17:29:25Containers-Benchmarks: theory Collections.TrieSetImpl
17:29:27Containers-Benchmarks: theory Collections.HashMap_Impl
17:29:27Containers-Benchmarks: theory Collections.RBTSetImpl
17:29:29Containers-Benchmarks: theory Collections.HashMap
17:29:31Containers-Benchmarks: theory Collections.HashSet
17:29:31Containers-Benchmarks: theory Collections.MapStdImpl
17:29:33Containers-Benchmarks: theory Collections.SetStdImpl
17:29:36Containers-Benchmarks: theory Collections.ICF_Impl
17:29:38CoreC++: theory CoreC++.CoreC++
17:29:41Containers-Benchmarks: theory Collections.ICF_Refine_Monadic
17:29:41Containers-Benchmarks: theory Collections.ICF_Autoref
17:29:44Timing Algebraic_Numbers (2 threads, 409.230s elapsed time, 736.936s cpu time, 58.884s GC time, factor 1.80)
17:29:44Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers
17:29:44Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/document.pdf
17:29:44Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Algebraic_Numbers/outline.pdf
17:29:44Finished Algebraic_Numbers (0:07:03 elapsed time, 0:12:35 cpu time, factor 1.79)
17:29:44Prpu_Maxflow CANCELLED
17:29:44Running Taylor_Models ...
17:29:45Containers-Benchmarks: theory Collections.Collections
17:29:45Containers-Benchmarks: theory Collections.CollectionsV1
17:29:46Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
17:29:46Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
17:29:47Timing LLL_Basis_Reduction (2 threads, 440.615s elapsed time, 799.568s cpu time, 43.024s GC time, factor 1.81)
17:29:47Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction
17:29:47Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/document.pdf
17:29:47Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/outline.pdf
17:29:47Finished LLL_Basis_Reduction (0:08:40 elapsed time, 0:15:10 cpu time, factor 1.75)
17:29:47Running E_Transcendental ...
17:29:49E_Transcendental: theory HOL-Algebra.Congruence
17:29:49E_Transcendental: theory HOL-Number_Theory.Cong
17:29:49Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity
17:29:50E_Transcendental: theory HOL-Algebra.Order
17:29:50E_Transcendental: theory HOL-Library.More_List
17:29:51E_Transcendental: theory HOL-Number_Theory.Eratosthenes
17:29:51E_Transcendental: theory HOL-Computational_Algebra.Polynomial
17:29:51E_Transcendental: theory HOL-Algebra.Lattice
17:29:53E_Transcendental: theory HOL-Algebra.Complete_Lattice
17:29:53Containers-Benchmarks: theory Containers-Benchmarks.Benchmark_ICF
17:29:54E_Transcendental: theory HOL-Algebra.Group
17:29:54Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension
17:29:55Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary
17:29:56Taylor_Models: theory Taylor_Models.Polynomial_Expression
17:29:57E_Transcendental: theory HOL-Algebra.Coset
17:29:57Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Boundary_Extension
17:29:57Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Busemann_Function
17:29:58E_Transcendental: theory HOL-Algebra.FiniteProduct
17:29:58Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries_Classification
17:29:58E_Transcendental: theory HOL-Algebra.Ring
17:30:00E_Transcendental: theory HOL-Number_Theory.Fib
17:30:00E_Transcendental: theory HOL-Number_Theory.Prime_Powers
17:30:01E_Transcendental: theory HOL-Number_Theory.Totient
17:30:03E_Transcendental: theory HOL-Algebra.AbelCoset
17:30:07E_Transcendental: theory HOL-Algebra.Module
17:30:10E_Transcendental: theory HOL-Algebra.Ideal
17:30:13E_Transcendental: theory HOL-Algebra.RingHom
17:30:14E_Transcendental: theory HOL-Algebra.UnivPoly
17:30:26Taylor_Models: theory HOL-Library.Function_Algebras
17:30:26Taylor_Models: theory Taylor_Models.Float_Topology
17:30:26Taylor_Models: theory Taylor_Models.Interval
17:30:26Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
17:30:28E_Transcendental: theory HOL-Algebra.Multiplicative_Group
17:30:29Taylor_Models: theory Taylor_Models.Horner_Eval
17:30:30Taylor_Models: theory Taylor_Models.Interval_Approximation
17:30:31E_Transcendental: theory HOL-Number_Theory.Residues
17:30:33E_Transcendental: theory HOL-Number_Theory.Euler_Criterion
17:30:33E_Transcendental: theory HOL-Number_Theory.Gauss
17:30:33E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity
17:30:33Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
17:30:34E_Transcendental: theory HOL-Number_Theory.Pocklington
17:30:34E_Transcendental: theory HOL-Number_Theory.Number_Theory
17:30:36E_Transcendental: theory E_Transcendental.E_Transcendental
17:30:38Taylor_Models: theory Taylor_Models.Taylor_Models
17:31:05Taylor_Models: theory Taylor_Models.Experiments
17:31:20Timing Dependent_SIFUM_Refinement (2 threads, 159.913s elapsed time, 287.368s cpu time, 11.860s GC time, factor 1.80)
17:31:20Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement
17:31:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement/document.pdf
17:31:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Refinement/outline.pdf
17:31:20Finished Dependent_SIFUM_Refinement (0:02:45 elapsed time, 0:04:56 cpu time, factor 1.79)
17:31:20Running Probabilistic_Noninterference ...
17:31:21Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv
17:31:21Probabilistic_Noninterference: theory HOL-Library.Prefix_Order
17:31:21Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat
17:31:22Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers-Benchmarks
17:31:22Containers-Benchmarks FAILED
17:31:22(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Containers-Benchmarks)
17:31:22 ?Q [];
17:31:22 \<And>t q.
17:31:22 \<lbrakk>?P t; ?Q q\<rbrakk> \<Longrightarrow> ?Q (t # q)\<rbrakk>
17:31:22\<Longrightarrow> ?Q ?a1.0
17:31:22(\<And>i len a c f \<sigma>.
17:31:22 (\<And>x.
17:31:22 \<lbrakk>\<not> (len \<le> i \<or> \<not> c \<sigma>);
17:31:22 x =
17:31:22 (case array_get a i of None \<Rightarrow> \<sigma>
17:31:22 | Some x \<Rightarrow> f (i, x) \<sigma>)\<rbrakk>
17:31:22 \<Longrightarrow> ?P (i + 1) len a c f x) \<Longrightarrow>
17:31:22 ?P i len a c f \<sigma>) \<Longrightarrow>
17:31:22?P ?a0.0 ?a1.0 ?a2.0 ?a3.0 ?a4.0 ?a5.0
17:31:22a_idx_it.idx_iteratei ?s = foldli (list_of_array ?s)
17:31:22*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:31:22***
17:31:22*** Type error in application: incompatible operand type
17:31:22***
17:31:22*** Operator: (\<noteq>) (aluprio_\<alpha> \<alpha> s) ::
17:31:22*** ('b \<Rightarrow> 'c option) \<Rightarrow> bool
17:31:22*** Operand: {} :: ??'a set
17:31:22***
17:31:22*** Coercion Inference:
17:31:22***
17:31:22*** Local coercion insertion on the operand failed:
17:31:22*** No coercion known for type constructors: "set" and "fun"
17:31:22*** At command "assume" (line 966 of "~~/afp/thys/Collections/ICF/gen_algo/PrioUniqueByAnnotatedList.thy")
17:31:22*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:31:22***
17:31:22*** Type error in application: incompatible operand type
17:31:22***
17:31:22*** Operator: (=) (aluprio_\<alpha> \<alpha> s) ::
17:31:22*** ('b \<Rightarrow> 'c option) \<Rightarrow> bool
17:31:22*** Operand: {} :: ??'a set
17:31:22***
17:31:22*** Coercion Inference:
17:31:22***
17:31:22*** Local coercion insertion on the operand failed:
17:31:22*** No coercion known for type constructors: "set" and "fun"
17:31:22*** At command "hence" (line 851 of "~~/afp/thys/Collections/ICF/gen_algo/PrioUniqueByAnnotatedList.thy")
17:31:22Gabow_SCC CANCELLED
17:31:22Running List_Update ...
17:31:23Probabilistic_Noninterference: theory Coinductive.Coinductive_List
17:31:24List_Update: theory HOL-Library.While_Combinator
17:31:24List_Update: theory List_Update.Prob_Theory
17:31:25List_Update: theory List_Update.Bit_Strings
17:31:25List_Update: theory List_Update.On_Off
17:31:25List_Update: theory List-Index.List_Index
17:31:25Timing Gromov_Hyperbolicity (2 threads, 146.983s elapsed time, 270.708s cpu time, 12.376s GC time, factor 1.84)
17:31:25Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gromov_Hyperbolicity
17:31:25Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gromov_Hyperbolicity/document.pdf
17:31:25Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gromov_Hyperbolicity/outline.pdf
17:31:25Finished Gromov_Hyperbolicity (0:02:37 elapsed time, 0:04:45 cpu time, factor 1.82)
17:31:25Running Prime_Harmonic_Series ...
17:31:26List_Update: theory List_Update.Inversion
17:31:26List_Update: theory List_Update.Swaps
17:31:26List_Update: theory Regular-Sets.Regular_Set
17:31:26List_Update: theory List_Update.Competitive_Analysis
17:31:27Prime_Harmonic_Series: theory HOL-Number_Theory.Cong
17:31:27Prime_Harmonic_Series: theory HOL-Algebra.Congruence
17:31:28List_Update: theory List_Update.Move_to_Front
17:31:29Prime_Harmonic_Series: theory HOL-Algebra.Order
17:31:29Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes
17:31:29Prime_Harmonic_Series: theory HOL-Number_Theory.Fib
17:31:29List_Update: theory Regular-Sets.Regular_Exp
17:31:29Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers
17:31:30Prime_Harmonic_Series: theory HOL-Algebra.Lattice
17:31:30Prime_Harmonic_Series: theory HOL-Number_Theory.Totient
17:31:31Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
17:31:31Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice
17:31:32Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
17:31:33Prime_Harmonic_Series: theory HOL-Algebra.Group
17:31:33List_Update: theory List_Update.MTF2_Effects
17:31:33List_Update: theory List_Update.Partial_Cost_Model
17:31:34List_Update: theory List_Update.BIT
17:31:34List_Update: theory List_Update.List_Factoring
17:31:34Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
17:31:35Prime_Harmonic_Series: theory HOL-Algebra.Coset
17:31:35Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct
17:31:35Prime_Harmonic_Series: theory HOL-Algebra.Ring
17:31:36Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
17:31:36List_Update: theory Regular-Sets.NDerivative
17:31:38List_Update: theory List_Update.BIT_pairwise
17:31:40Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset
17:31:40Prime_Harmonic_Series: theory HOL-Algebra.Module
17:31:41List_Update: theory Regular-Sets.Equivalence_Checking
17:31:41List_Update: theory List_Update.RExp_Var
17:31:44Timing LOFT (2 threads, 188.892s elapsed time, 340.500s cpu time, 14.520s GC time, factor 1.80)
17:31:44Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT
17:31:44Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT/document.pdf
17:31:44Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LOFT/outline.pdf
17:31:44Finished LOFT (0:03:18 elapsed time, 0:06:00 cpu time, factor 1.82)
17:31:44Running Dirichlet_L ...
17:31:44List_Update: theory List_Update.OPT2
17:31:45Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order
17:31:45Dirichlet_L: theory HOL-Library.Lattice_Algebras
17:31:46Prime_Harmonic_Series: theory HOL-Algebra.Ideal
17:31:46List_Update: theory List_Update.Phase_Partitioning
17:31:46List_Update: theory List_Update.BIT_2comp_on2
17:31:48Dirichlet_L: theory HOL-Library.Log_Nat
17:31:48Dirichlet_L: theory Bernoulli.Bernoulli_Zeta
17:31:49Dirichlet_L: theory Zeta_Function.Zeta_Function
17:31:49Prime_Harmonic_Series: theory HOL-Algebra.RingHom
17:31:49List_Update: theory List_Update.TS
17:31:50Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly
17:31:50Dirichlet_L: theory HOL-Library.Float
17:31:51List_Update: theory List_Update.Comb
17:31:52Dirichlet_L: theory Lehmer.Lehmer
17:31:52Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate
17:31:53Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
17:31:55Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
17:31:58Dirichlet_L: theory Bertrands_Postulate.Bertrand
17:32:01Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group
17:32:02Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
17:32:04Prime_Harmonic_Series: theory HOL-Number_Theory.Residues
17:32:04Timing CoreC++ (2 threads, 207.458s elapsed time, 368.988s cpu time, 34.052s GC time, factor 1.78)
17:32:04Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++
17:32:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/document.pdf
17:32:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/outline.pdf
17:32:04Finished CoreC++ (0:03:38 elapsed time, 0:06:25 cpu time, factor 1.77)
17:32:04Running Free-Groups ...
17:32:05Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
17:32:05Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
17:32:05Free-Groups: theory HOL-Cardinals.Order_Relation_More
17:32:05Free-Groups: theory HOL-Cardinals.Fun_More
17:32:05Free-Groups: theory HOL-Cardinals.Order_Union
17:32:05Free-Groups: theory HOL-Library.Cancellation
17:32:05Free-Groups: theory HOL-Cardinals.Wellfounded_More
17:32:05Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion
17:32:05Free-Groups: theory HOL-Cardinals.Wellorder_Relation
17:32:06Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss
17:32:06Free-Groups: theory HOL-Cardinals.Wellorder_Embedding
17:32:06Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
17:32:06Free-Groups: theory HOL-Library.Cardinal_Notations
17:32:06Free-Groups: theory HOL-Library.Multiset
17:32:06Free-Groups: theory HOL-Cardinals.Wellorder_Constructions
17:32:06Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington
17:32:07Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory
17:32:07Free-Groups: theory HOL-Cardinals.Cardinal_Order_Relation
17:32:08Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
17:32:08Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc
17:32:08Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat
17:32:08Timing E_Transcendental (2 threads, 135.540s elapsed time, 234.860s cpu time, 20.660s GC time, factor 1.73)
17:32:08Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/E_Transcendental
17:32:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/E_Transcendental/document.pdf
17:32:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/E_Transcendental/outline.pdf
17:32:08Finished E_Transcendental (0:02:20 elapsed time, 0:04:02 cpu time, factor 1.73)
17:32:08Running Count_Complex_Roots ...
17:32:08Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic
17:32:09Free-Groups: theory HOL-Library.FuncSet
17:32:09Free-Groups: theory HOL-Algebra.Congruence
17:32:10Count_Complex_Roots: theory HOL-Eisbach.Eisbach
17:32:10Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field
17:32:10Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
17:32:10Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools
17:32:10Count_Complex_Roots: theory HOL-Library.More_List
17:32:11Free-Groups: theory HOL-Algebra.Order
17:32:11Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial
17:32:11Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction
17:32:11Timing Taylor_Models (2 threads, 140.612s elapsed time, 244.248s cpu time, 11.636s GC time, factor 1.74)
17:32:11Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Taylor_Models
17:32:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Taylor_Models/document.pdf
17:32:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Taylor_Models/outline.pdf
17:32:11Finished Taylor_Models (0:02:27 elapsed time, 0:04:14 cpu time, factor 1.73)
17:32:11Running Ergodic_Theory ...
17:32:12Free-Groups: theory HOL-Computational_Algebra.Factorial_Ring
17:32:12Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring
17:32:12Free-Groups: theory HOL-Algebra.Lattice
17:32:13Ergodic_Theory: theory Ergodic_Theory.Fekete
17:32:13Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement
17:32:13Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis
17:32:13Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
17:32:13Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology
17:32:13Free-Groups: theory HOL-Algebra.Complete_Lattice
17:32:14Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density
17:32:14Free-Groups: theory HOL-Algebra.Group
17:32:14Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
17:32:16Ergodic_Theory: theory Ergodic_Theory.Recurrence
17:32:16Free-Groups: theory Free-Groups.C2
17:32:16Free-Groups: theory Free-Groups.Generators
17:32:17Free-Groups: theory Free-Groups.UnitGroup
17:32:17Free-Groups: theory HOL-Algebra.Bij
17:32:17Free-Groups: theory HOL-Algebra.Coset
17:32:18Ergodic_Theory: theory Ergodic_Theory.Invariants
17:32:18Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
17:32:18Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
17:32:19Ergodic_Theory: theory Ergodic_Theory.Ergodicity
17:32:19Free-Groups: theory HOL-Computational_Algebra.Euclidean_Algorithm
17:32:19Free-Groups: theory HOL-Algebra.FiniteProduct
17:32:19Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
17:32:19Free-Groups: theory HOL-Algebra.Ring
17:32:20Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial
17:32:20Ergodic_Theory: theory Ergodic_Theory.Kingman
17:32:22Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
17:32:26Free-Groups: theory HOL-Algebra.AbelCoset
17:32:28Free-Groups: theory HOL-Computational_Algebra.Primes
17:32:28Free-Groups: theory HOL-Proofs-Lambda.Commutation
17:32:28Free-Groups: theory Free-Groups.Cancelation
17:32:29Free-Groups: theory Free-Groups.FreeGroups
17:32:29Free-Groups: theory Free-Groups.PingPongLemma
17:32:30Free-Groups: theory HOL-Algebra.Ideal
17:32:32Free-Groups: theory HOL-Algebra.RingHom
17:32:34Count_Complex_Roots: theory Sturm_Tarski.PolyMisc
17:32:34Free-Groups: theory HOL-Algebra.QuotRing
17:32:34Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic
17:32:34Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski
17:32:34Free-Groups: theory HOL-Algebra.IntRing
17:32:35Free-Groups: theory Free-Groups.Isomorphisms
17:32:36Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental
17:32:36Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem
17:32:40Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm
17:32:40Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval
17:32:42Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots
17:32:43Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples
17:33:26Dirichlet_L: theory Dirichlet_L.Group_Adjoin
17:33:26Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
17:33:27Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
17:33:27Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
17:33:30Timing Probabilistic_Noninterference (2 threads, 122.265s elapsed time, 207.568s cpu time, 8.388s GC time, factor 1.70)
17:33:30Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference
17:33:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference/document.pdf
17:33:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Noninterference/outline.pdf
17:33:30Finished Probabilistic_Noninterference (0:02:09 elapsed time, 0:03:41 cpu time, factor 1.72)
17:33:30Running Gauss_Jordan ...
17:33:30Timing Prime_Harmonic_Series (2 threads, 118.888s elapsed time, 204.428s cpu time, 13.068s GC time, factor 1.72)
17:33:30Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Prime_Harmonic_Series
17:33:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Prime_Harmonic_Series/document.pdf
17:33:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Prime_Harmonic_Series/outline.pdf
17:33:30Finished Prime_Harmonic_Series (0:02:04 elapsed time, 0:03:32 cpu time, factor 1.71)
17:33:30Running UPF_Firewall ...
17:33:31Gauss_Jordan: theory HOL-Library.Bit
17:33:31Gauss_Jordan: theory HOL-Library.Code_Abstract_Nat
17:33:31Gauss_Jordan: theory HOL-Library.Code_Target_Nat
17:33:31Gauss_Jordan: theory HOL-Library.Code_Target_Int
17:33:31Gauss_Jordan: theory HOL-Library.Code_Target_Numeral
17:33:31Gauss_Jordan: theory Gauss_Jordan.Code_Bit
17:33:32Gauss_Jordan: theory HOL-Library.Function_Algebras
17:33:32Gauss_Jordan: theory HOL-Library.IArray
17:33:32Gauss_Jordan: theory Gauss_Jordan.Code_Set
17:33:32Gauss_Jordan: theory HOL-Library.Code_Real_Approx_By_Float
17:33:32Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
17:33:32Gauss_Jordan: theory Rank_Nullity_Theorem.Dual_Order
17:33:32Gauss_Jordan: theory Rank_Nullity_Theorem.Mod_Type
17:33:33Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda
17:33:33Gauss_Jordan: theory Gauss_Jordan.IArray_Haskell
17:33:34Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
17:33:35Gauss_Jordan: theory Rank_Nullity_Theorem.Miscellaneous
17:33:36UPF_Firewall: theory UPF_Firewall.NetworkCore
17:33:36UPF_Firewall: theory UPF_Firewall.LTL_alike
17:33:36Gauss_Jordan: theory Gauss_Jordan.Code_Matrix
17:33:37UPF_Firewall: theory UPF_Firewall.Ports
17:33:37Gauss_Jordan: theory Gauss_Jordan.Rref
17:33:37UPF_Firewall: theory UPF_Firewall.DatatypeAddress
17:33:37UPF_Firewall: theory UPF_Firewall.DatatypePort
17:33:37Gauss_Jordan: theory Rank_Nullity_Theorem.Fundamental_Subspaces
17:33:37Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations
17:33:37Gauss_Jordan: theory Rank_Nullity_Theorem.Dim_Formula
17:33:37UPF_Firewall: theory UPF_Firewall.IPv4
17:33:37UPF_Firewall: theory UPF_Firewall.IntegerAddress
17:33:37UPF_Firewall: theory UPF_Firewall.IntegerPort
17:33:37Gauss_Jordan: theory Gauss_Jordan.Rank
17:33:37UPF_Firewall: theory UPF_Firewall.IPv4_TCPUDP
17:33:37UPF_Firewall: theory UPF_Firewall.IntegerPort_TCPUDP
17:33:37UPF_Firewall: theory UPF_Firewall.PolicyCore
17:33:38UPF_Firewall: theory UPF_Firewall.NetworkModels
17:33:38UPF_Firewall: theory UPF_Firewall.PolicyCombinators
17:33:38Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray
17:33:38Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan
17:33:38UPF_Firewall: theory UPF_Firewall.PortCombinators
17:33:39UPF_Firewall: theory UPF_Firewall.ProtocolPortCombinators
17:33:39Timing List_Update (2 threads, 124.594s elapsed time, 217.044s cpu time, 10.812s GC time, factor 1.74)
17:33:39Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update
17:33:39Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update/document.pdf
17:33:39Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/List_Update/outline.pdf
17:33:39Finished List_Update (0:02:15 elapsed time, 0:03:58 cpu time, factor 1.75)
17:33:39Running Density_Compiler ...
17:33:39UPF_Firewall: theory UPF_Firewall.PacketFilter
17:33:39UPF_Firewall: theory UPF_Firewall.FWNormalisationCore
17:33:39UPF_Firewall: theory UPF_Firewall.NAT
17:33:40UPF_Firewall: theory UPF_Firewall.StatefulCore
17:33:40Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays
17:33:40Gauss_Jordan: theory Gauss_Jordan.Linear_Maps
17:33:40Density_Compiler: theory Density_Compiler.Density_Predicates
17:33:40UPF_Firewall: theory UPF_Firewall.FTP
17:33:41Density_Compiler: theory Density_Compiler.PDF_Transformations
17:33:41Density_Compiler: theory Density_Compiler.PDF_Values
17:33:41Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA
17:33:42Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
17:33:43Gauss_Jordan: theory Gauss_Jordan.Determinants2
17:33:43Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays
17:33:44Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
17:33:44Gauss_Jordan: theory Gauss_Jordan.Inverse
17:33:44Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations
17:33:44UPF_Firewall: theory UPF_Firewall.FTP_WithPolicy
17:33:44Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays
17:33:45Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays
17:33:45Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
17:33:45Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays
17:33:45UPF_Firewall: theory UPF_Firewall.VOIP
17:33:45Density_Compiler: theory Density_Compiler.PDF_Semantics
17:33:46Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays
17:33:46Timing Dirichlet_L (2 threads, 115.556s elapsed time, 223.056s cpu time, 8.128s GC time, factor 1.93)
17:33:46Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dirichlet_L
17:33:46Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dirichlet_L/document.pdf
17:33:46Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dirichlet_L/outline.pdf
17:33:46Finished Dirichlet_L (0:02:01 elapsed time, 0:03:52 cpu time, factor 1.91)
17:33:46Running Green ...
17:33:47Green: theory Green.General_Utils
17:33:47Green: theory Green.Derivs
17:33:47Green: theory Green.Integrals
17:33:48Green: theory Green.Paths
17:33:48Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays
17:33:49Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML
17:33:49Gauss_Jordan: theory Gauss_Jordan.Code_Rational
17:33:51Green: theory Green.Green
17:33:51Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell
17:33:52UPF_Firewall: theory UPF_Firewall.FTPVOIP
17:33:53Green: theory Green.SymmetricR2Shapes
17:33:53Green: theory Green.CircExample
17:33:53Green: theory Green.DiamExample
17:33:55UPF_Firewall: theory UPF_Firewall.ElementaryRules
17:33:55UPF_Firewall: theory UPF_Firewall.NormalisationGenericProofs
17:33:55Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
17:33:55Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
17:33:56Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
17:33:57UPF_Firewall: theory UPF_Firewall.NormalisationIntegerPortProof
17:33:59Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
17:34:00Density_Compiler: theory Density_Compiler.PDF_Compiler
17:34:02UPF_Firewall: theory UPF_Firewall.StatefulFW
17:34:04Timing Count_Complex_Roots (2 threads, 109.421s elapsed time, 202.220s cpu time, 7.864s GC time, factor 1.85)
17:34:04Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Count_Complex_Roots
17:34:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Count_Complex_Roots/document.pdf
17:34:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Count_Complex_Roots/outline.pdf
17:34:04Finished Count_Complex_Roots (0:01:55 elapsed time, 0:03:31 cpu time, factor 1.83)
17:34:04Running Deep_Learning ...
17:34:07Deep_Learning: theory Deep_Learning.Tensor
17:34:07Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
17:34:07Deep_Learning: theory Deep_Learning.Lebesgue_Functional
17:34:07Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
17:34:07Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
17:34:07Deep_Learning: theory Polynomials.More_List2
17:34:07Deep_Learning: theory Deep_Learning.Tensor_Subtensor
17:34:07Deep_Learning: theory Polynomials.Poly_Mapping
17:34:07Deep_Learning: theory Deep_Learning.Tensor_Plus
17:34:08Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
17:34:08Deep_Learning: theory Deep_Learning.Tensor_Product
17:34:08Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
17:34:08Deep_Learning: theory Deep_Learning.Tensor_Rank
17:34:08Deep_Learning: theory Deep_Learning.DL_Network
17:34:09Deep_Learning: theory Deep_Learning.Tensor_Matricization
17:34:10Timing Free-Groups (2 threads, 120.589s elapsed time, 195.128s cpu time, 13.260s GC time, factor 1.62)
17:34:10Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Free-Groups
17:34:10Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Free-Groups/document.pdf
17:34:10Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Free-Groups/outline.pdf
17:34:10Finished Free-Groups (0:02:05 elapsed time, 0:03:23 cpu time, factor 1.62)
17:34:10Running Akra_Bazzi ...
17:34:11Deep_Learning: theory Polynomials.MPoly_Type
17:34:11Timing Ergodic_Theory (2 threads, 107.526s elapsed time, 196.812s cpu time, 6.260s GC time, factor 1.83)
17:34:11Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory
17:34:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory/document.pdf
17:34:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ergodic_Theory/outline.pdf
17:34:11Finished Ergodic_Theory (0:01:59 elapsed time, 0:03:34 cpu time, factor 1.79)
17:34:11Running MFMC_Countable ...
17:34:11Akra_Bazzi: theory HOL-Library.Code_Abstract_Nat
17:34:11Akra_Bazzi: theory HOL-Decision_Procs.Dense_Linear_Order
17:34:11Akra_Bazzi: theory HOL-Library.Code_Target_Nat
17:34:12Deep_Learning: theory Polynomials.More_MPoly_Type
17:34:12Akra_Bazzi: theory HOL-Library.Code_Target_Int
17:34:12Akra_Bazzi: theory HOL-Library.Code_Target_Numeral
17:34:12Akra_Bazzi: theory HOL-Library.Function_Algebras
17:34:12Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral
17:34:12Akra_Bazzi: theory HOL-Library.Landau_Symbols
17:34:13Deep_Learning: theory Polynomials.MPoly_Type_Univariate
17:34:13MFMC_Countable: theory Flow_Networks.Graph
17:34:13MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
17:34:13Deep_Learning: theory Deep_Learning.DL_Shallow_Model
17:34:13Deep_Learning: theory Deep_Learning.DL_Deep_Model
17:34:13MFMC_Countable: theory HOL-Library.While_Combinator
17:34:13Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
17:34:14MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
17:34:14Akra_Bazzi: theory HOL-Library.Lattice_Algebras
17:34:14Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
17:34:15MFMC_Countable: theory MFMC_Countable.MFMC_Misc
17:34:15MFMC_Countable: theory Flow_Networks.Network
17:34:15Akra_Bazzi: theory HOL-Library.Log_Nat
17:34:15MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
17:34:16Akra_Bazzi: theory Landau_Symbols.Group_Sort
17:34:16MFMC_Countable: theory Flow_Networks.Residual_Graph
17:34:17Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
17:34:17Akra_Bazzi: theory Landau_Symbols.Landau_Real_Products
17:34:18MFMC_Countable: theory Flow_Networks.Augmenting_Flow
17:34:18Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
17:34:18MFMC_Countable: theory Flow_Networks.Augmenting_Path
17:34:18MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
17:34:19Akra_Bazzi: theory HOL-Library.Float
17:34:19MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
17:34:20MFMC_Countable: theory MFMC_Countable.MFMC_Finite
17:34:20MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
17:34:21Akra_Bazzi: theory HOL-Decision_Procs.Approximation_Bounds
17:34:21Akra_Bazzi: theory Landau_Symbols.Landau_Simprocs
17:34:21MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
17:34:22Akra_Bazzi: theory Landau_Symbols.Landau_More
17:34:22Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library
17:34:23Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics
17:34:23Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real
17:34:24Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi
17:34:26Akra_Bazzi: theory Akra_Bazzi.Master_Theorem
17:34:26Akra_Bazzi: theory HOL-Decision_Procs.Approximation
17:34:27Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method
17:34:34Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall
17:34:34UPF_Firewall FAILED
17:34:34(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/UPF_Firewall)
17:34:34isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall/document -o pdf -n document
17:34:34isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall/outline -o pdf -n outline -t /proof,/ML
17:34:34*** Failed to load theory "UPF_Firewall.NormalisationIPPProofs" (unresolved "UPF_Firewall.NormalisationIntegerPortProof")
17:34:34*** Failed to load theory "UPF_Firewall.FWNormalisation" (unresolved "UPF_Firewall.NormalisationIPPProofs")
17:34:34*** Failed to load theory "UPF_Firewall.UPF-Firewall" (unresolved "UPF_Firewall.FWNormalisation")
17:34:34*** Failed to load theory "UPF_Firewall.DMZDatatype" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.DMZInteger" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.DMZ" (unresolved "UPF_Firewall.DMZDatatype", "UPF_Firewall.DMZInteger")
17:34:34*** Failed to load theory "UPF_Firewall.NAT-FW" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.PersonalFirewallDatatype" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.PersonalFirewallInt" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.PersonalFirewallIpv4" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.PersonalFirewall" (unresolved "UPF_Firewall.PersonalFirewallDatatype", "UPF_Firewall.PersonalFirewallInt", "UPF_Firewall.PersonalFirewallIpv4")
17:34:34*** Failed to load theory "UPF_Firewall.Transformation01" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.Transformation02" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.Transformation" (unresolved "UPF_Firewall.Transformation01", "UPF_Firewall.Transformation02")
17:34:34*** Failed to load theory "UPF_Firewall.VoIP" (unresolved "UPF_Firewall.UPF-Firewall")
17:34:34*** Failed to load theory "UPF_Firewall.Examples" (unresolved "UPF_Firewall.DMZ", "UPF_Firewall.NAT-FW", "UPF_Firewall.PersonalFirewall", "UPF_Firewall.Transformation", "UPF_Firewall.VoIP")
17:34:34*** Latex error:
17:34:34*** File `UPF-Firewall.tex' not found.
17:34:34*** Latex error (line 134 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall/outline/root.tex"):
17:34:34*** Emergency stop.
17:34:34*** <read *>
17:34:34***
17:34:34*** \input{UPF-Firewall}
17:34:34*** Latex error (line 134 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall/outline/root.tex"):
17:34:34*** ==> Fatal error occurred, no output PDF file produced!
17:34:34*** Failed to build document in "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UPF_Firewall/outline"
17:34:34*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:34:34***
17:34:34*** Type error in application: incompatible operand type
17:34:34***
17:34:34*** Operator: (\<noteq>) (C DenyAll) ::
17:34:34*** (int \<times>
17:34:34*** (int \<times> int) \<times> (int \<times> int) \<times> DummyContent
17:34:34*** \<Rightarrow> unit decision option)
17:34:34*** \<Rightarrow> bool
17:34:34*** Operand: {} :: ??'a set
17:34:34***
17:34:34*** At command "lemma" (line 873 of "~~/afp/thys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy")
17:34:34Running Knot_Theory ...
17:34:35Knot_Theory: theory HOL-Computational_Algebra.Fraction_Field
17:34:35Knot_Theory: theory HOL-Computational_Algebra.Factorial_Ring
17:34:37Knot_Theory: theory Knot_Theory.Preliminaries
17:34:38Knot_Theory: theory Knot_Theory.Tangles
17:34:38Knot_Theory: theory Knot_Theory.Tangle_Algebra
17:34:40Knot_Theory: theory Knot_Theory.Tangle_Relation
17:34:40Knot_Theory: theory Knot_Theory.Tangle_Moves
17:34:40Knot_Theory: theory Knot_Theory.Link_Algebra
17:34:41Knot_Theory: theory Knot_Theory.Example
17:34:42Knot_Theory: theory HOL-Computational_Algebra.Polynomial
17:34:50Knot_Theory: theory Knot_Theory.Kauffman_Matrix
17:34:53Knot_Theory: theory Knot_Theory.Computations
17:34:53Knot_Theory: theory Knot_Theory.Linkrel_Kauffman
17:34:54Knot_Theory: theory Knot_Theory.Kauffman_Invariance
17:34:54Knot_Theory: theory Knot_Theory.Knot_Theory
17:35:13Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation
17:35:13Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples
17:35:27Timing Gauss_Jordan (2 threads, 107.089s elapsed time, 198.228s cpu time, 6.812s GC time, factor 1.85)
17:35:27Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gauss_Jordan
17:35:27Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gauss_Jordan/document.pdf
17:35:27Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Gauss_Jordan/outline.pdf
17:35:27Finished Gauss_Jordan (0:01:56 elapsed time, 0:03:33 cpu time, factor 1.83)
17:35:27Running Hermite ...
17:35:28Hermite: theory Hermite.Hermite
17:35:29Timing Density_Compiler (2 threads, 101.514s elapsed time, 197.148s cpu time, 5.368s GC time, factor 1.94)
17:35:29Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler
17:35:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler/document.pdf
17:35:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Density_Compiler/outline.pdf
17:35:29Finished Density_Compiler (0:01:49 elapsed time, 0:03:29 cpu time, factor 1.91)
17:35:29Running Winding_Number_Eval ...
17:35:30Winding_Number_Eval: theory HOL-Eisbach.Eisbach
17:35:30Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field
17:35:31Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
17:35:31Winding_Number_Eval: theory HOL-Library.More_List
17:35:31Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial
17:35:31Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
17:35:32Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring
17:35:33Hermite: theory Hermite.Hermite_IArrays
17:35:33Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
17:35:34Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
17:35:36Timing Green (2 threads, 101.001s elapsed time, 181.380s cpu time, 3.540s GC time, factor 1.80)
17:35:36Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Green
17:35:36Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Green/document.pdf
17:35:36Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Green/outline.pdf
17:35:36Finished Green (0:01:49 elapsed time, 0:03:18 cpu time, factor 1.81)
17:35:36Running Probabilistic_Timed_Automata ...
17:35:38Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic
17:35:38Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux
17:35:38Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
17:35:38Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
17:35:39Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
17:35:39Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
17:35:39Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
17:35:40Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
17:35:40Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
17:35:40Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
17:35:41Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
17:35:50Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
17:35:51Timing Akra_Bazzi (2 threads, 93.967s elapsed time, 185.132s cpu time, 11.140s GC time, factor 1.97)
17:35:51Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Akra_Bazzi
17:35:51Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Akra_Bazzi/document.pdf
17:35:51Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Akra_Bazzi/outline.pdf
17:35:51Finished Akra_Bazzi (0:01:40 elapsed time, 0:03:15 cpu time, factor 1.94)
17:35:51Running Bertrands_Postulate ...
17:35:53Timing MFMC_Countable (2 threads, 91.549s elapsed time, 165.812s cpu time, 6.892s GC time, factor 1.81)
17:35:53Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable
17:35:53Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable/document.pdf
17:35:53Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/MFMC_Countable/outline.pdf
17:35:53Finished MFMC_Countable (0:01:41 elapsed time, 0:02:59 cpu time, factor 1.77)
17:35:53Running Call_Arity ...
17:35:53Bertrands_Postulate: theory HOL-Decision_Procs.Dense_Linear_Order
17:35:53Bertrands_Postulate: theory Lehmer.Lehmer
17:35:54Bertrands_Postulate: theory Pratt_Certificate.Pratt_Certificate
17:35:54Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
17:35:54Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
17:35:54Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
17:35:54Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
17:35:54Call_Arity: theory Call_Arity.ConstOn
17:35:54Call_Arity: theory Call_Arity.BalancedTraces
17:35:54Call_Arity: theory Call_Arity.List-Interleavings
17:35:54Call_Arity: theory Call_Arity.Set-Cpo
17:35:55Call_Arity: theory Call_Arity.Arity
17:35:55Call_Arity: theory Call_Arity.TTree
17:35:55Call_Arity: theory Call_Arity.EtaExpansion
17:35:55Call_Arity: theory Call_Arity.SestoftConf
17:35:56Timing Deep_Learning (2 threads, 103.382s elapsed time, 180.952s cpu time, 5.716s GC time, factor 1.75)
17:35:56Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning
17:35:56Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/document.pdf
17:35:56Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/outline.pdf
17:35:56Finished Deep_Learning (0:01:50 elapsed time, 0:03:12 cpu time, factor 1.74)
17:35:56Running Hidden_Markov_Models ...
17:35:56Bertrands_Postulate: theory HOL-Decision_Procs.Approximation_Bounds
17:35:56Call_Arity: theory Call_Arity.AEnv
17:35:56Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
17:35:57Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
17:35:57Call_Arity: theory Call_Arity.ArityStack
17:35:57Call_Arity: theory Call_Arity.Sestoft
17:35:57Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary
17:35:58Call_Arity: theory Call_Arity.EtaExpansionSafe
17:35:58Call_Arity: theory Call_Arity.SestoftGC
17:35:58Call_Arity: theory Call_Arity.SestoftCorrect
17:35:58Hidden_Markov_Models: theory HOL-Library.State_Monad
17:35:58Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap
17:35:58Call_Arity: theory Call_Arity.Env-Set-Cpo
17:35:59Call_Arity: theory Call_Arity.AList-Utils-HOLCF
17:35:59Call_Arity: theory Call_Arity.AnalBinds
17:35:59Call_Arity: theory Call_Arity.Cardinality-Domain
17:35:59Call_Arity: theory Call_Arity.CardinalityAnalysisSig
17:36:00Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext
17:36:00Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model
17:36:00Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad
17:36:01Call_Arity: theory Call_Arity.CoCallGraph
17:36:01Call_Arity: theory Call_Arity.TTree-HOLCF
17:36:01Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
17:36:01Bertrands_Postulate: theory Bertrands_Postulate.Bertrand
17:36:02Call_Arity: theory Call_Arity.TTreeAnalysisSig
17:36:02Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
17:36:02Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
17:36:02Call_Arity: theory Call_Arity.CoCallAnalysisSig
17:36:03Call_Arity: theory Call_Arity.CoCallGraph-TTree
17:36:03Call_Arity: theory Call_Arity.Arity-Nominal
17:36:03Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref
17:36:03Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL
17:36:04Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext
17:36:04Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad
17:36:04Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS
17:36:04Call_Arity: theory Call_Arity.ArityAnalysisSig
17:36:04Hidden_Markov_Models: theory Monad_Memo_DP.Memory
17:36:04Call_Arity: theory Call_Arity.Cardinality-Domain-Lists
17:36:05Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
17:36:05Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap
17:36:05Call_Arity: theory Call_Arity.ArityAnalysisAbinds
17:36:05Call_Arity: theory Call_Arity.ArityAnalysisSpec
17:36:06Call_Arity: theory Call_Arity.ArityAnalysisFix
17:36:06Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
17:36:06Call_Arity: theory Call_Arity.ArityAnalysisStack
17:36:06Call_Arity: theory Call_Arity.CardinalityAnalysisSpec
17:36:06Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
17:36:07Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
17:36:07Call_Arity: theory Call_Arity.ArityAnalysisFixProps
17:36:07Call_Arity: theory Call_Arity.ArityConsistent
17:36:07Call_Arity: theory Call_Arity.NoCardinalityAnalysis
17:36:08Call_Arity: theory Call_Arity.CoCallAritySig
17:36:08Call_Arity: theory Call_Arity.TTreeAnalysisSpec
17:36:09Call_Arity: theory Call_Arity.CoCallAnalysisSpec
17:36:09Call_Arity: theory Call_Arity.CoCallImplTTree
17:36:09Call_Arity: theory Call_Arity.TTreeImplCardinality
17:36:10Call_Arity: theory Call_Arity.CoCallImplTTreeSafe
17:36:11Call_Arity: theory Call_Arity.TTreeImplCardinalitySafe
17:36:11Call_Arity: theory Call_Arity.CoCallGraph-Nominal
17:36:12Call_Arity: theory Call_Arity.CoCallAnalysisBinds
17:36:12Call_Arity: theory Call_Arity.TransformTools
17:36:12Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
17:36:13Call_Arity: theory Call_Arity.CoCallFix
17:36:13Call_Arity: theory Call_Arity.AbstractTransform
17:36:14Call_Arity: theory Call_Arity.ArityEtaExpansion
17:36:15Call_Arity: theory Call_Arity.CoCallAnalysisImpl
17:36:15Call_Arity: theory Call_Arity.ArityEtaExpansionSafe
17:36:16Timing Knot_Theory (2 threads, 95.130s elapsed time, 163.144s cpu time, 6.244s GC time, factor 1.71)
17:36:16Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory
17:36:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory/document.pdf
17:36:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Knot_Theory/outline.pdf
17:36:16Finished Knot_Theory (0:01:41 elapsed time, 0:02:53 cpu time, factor 1.70)
17:36:16VerifyThis2018 CANCELLED
17:36:16EdmondsKarp_Maxflow CANCELLED
17:36:16Partial_Order_Reduction CANCELLED
17:36:16Running Elliptic_Curves_Group_Law ...
17:36:16Call_Arity: theory Call_Arity.ArityTransform
17:36:17Call_Arity: theory Call_Arity.CoCallImplSafe
17:36:17Call_Arity: theory Call_Arity.ArityTransformSafe
17:36:18Call_Arity: theory Call_Arity.CardArityTransformSafe
17:36:18Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Algebra_Aux
17:36:18Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Conversions
17:36:19Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Commutative_Ring
17:36:19Call_Arity: theory Call_Arity.CallArityEnd2End
17:36:20Call_Arity: theory Call_Arity.TrivialArityAnal
17:36:20Call_Arity: theory Call_Arity.ArityAnalysisCorrDenotational
17:36:20Call_Arity: theory Call_Arity.CallArityEnd2EndSafe
17:36:29Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
17:36:30Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Reflective_Field
17:36:41Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Axclass
17:36:42Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Locale
17:36:46Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Test
17:36:58Timing Hermite (2 threads, 84.854s elapsed time, 133.716s cpu time, 11.556s GC time, factor 1.58)
17:36:58Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hermite
17:36:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hermite/document.pdf
17:36:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hermite/outline.pdf
17:36:58Finished Hermite (0:01:30 elapsed time, 0:02:23 cpu time, factor 1.58)
17:36:58Running LLL_Factorization ...
17:37:00Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
17:37:04Timing Winding_Number_Eval (2 threads, 86.853s elapsed time, 157.332s cpu time, 6.000s GC time, factor 1.81)
17:37:04Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Winding_Number_Eval
17:37:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Winding_Number_Eval/document.pdf
17:37:04Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Winding_Number_Eval/outline.pdf
17:37:04Finished Winding_Number_Eval (0:01:34 elapsed time, 0:02:49 cpu time, factor 1.79)
17:37:04Dijkstra_Shortest_Path CANCELLED
17:37:04Running Irrationality_J_Hancl ...
17:37:05Irrationality_J_Hancl: theory HOL-Library.Code_Abstract_Nat
17:37:05Irrationality_J_Hancl: theory HOL-Decision_Procs.Dense_Linear_Order
17:37:05Irrationality_J_Hancl: theory HOL-Library.Code_Target_Nat
17:37:06Irrationality_J_Hancl: theory HOL-Library.Code_Target_Int
17:37:06Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral
17:37:06Irrationality_J_Hancl: theory HOL-Library.Lattice_Algebras
17:37:08LLL_Factorization: theory LLL_Factorization.Sub_Sums
17:37:08LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
17:37:08LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
17:37:08Irrationality_J_Hancl: theory HOL-Library.Log_Nat
17:37:09Timing Probabilistic_Timed_Automata (2 threads, 83.794s elapsed time, 156.896s cpu time, 7.968s GC time, factor 1.87)
17:37:09Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Timed_Automata
17:37:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Timed_Automata/document.pdf
17:37:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_Timed_Automata/outline.pdf
17:37:09Finished Probabilistic_Timed_Automata (0:01:32 elapsed time, 0:02:50 cpu time, factor 1.85)
17:37:09Running Koenigsberg_Friendship ...
17:37:09LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
17:37:11Irrationality_J_Hancl: theory HOL-Library.Float
17:37:11Koenigsberg_Friendship: theory Dijkstra_Shortest_Path.Graph
17:37:12Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph
17:37:13Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds
17:37:14Timing Hidden_Markov_Models (2 threads, 72.718s elapsed time, 109.068s cpu time, 14.876s GC time, factor 1.50)
17:37:14Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hidden_Markov_Models
17:37:14Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hidden_Markov_Models/document.pdf
17:37:14Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Hidden_Markov_Models/outline.pdf
17:37:14Finished Hidden_Markov_Models (0:01:18 elapsed time, 0:01:58 cpu time, factor 1.50)
17:37:14Running SDS_Impossibility ...
17:37:16Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory
17:37:16SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
17:37:17Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge
17:37:17Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation
17:37:17Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization
17:37:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/document.pdf
17:37:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/outline.pdf
17:37:17LLL_Factorization FAILED
17:37:17(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/LLL_Factorization)
17:37:17Found termination order: "length <*mlex*> {}"
17:37:17### theory "LLL_Factorization.Sub_Sums"
17:37:17### 0.152s elapsed time, 0.440s cpu time, 0.000s GC time
17:37:17Loading theory "LLL_Factorization.Factor_Bound_2" (required by "LLL_Factorization.LLL_Factorization_Impl")
17:37:17locale poly_mod
17:37:17 fixes m :: "int"
17:37:17locale poly_mod_prime_type
17:37:17 fixes m :: "int"
17:37:17 and ty :: "'a itself"
17:37:17 assumes "poly_mod_prime_type TYPE('a) m"
17:37:17### theory "LLL_Factorization.Missing_Dvd_Int_Poly"
17:37:17### 1.091s elapsed time, 2.312s cpu time, 0.000s GC time
17:37:17### theory "LLL_Factorization.Factor_Bound_2"
17:37:17### 1.483s elapsed time, 2.972s cpu time, 0.000s GC time
17:37:17Loading theory "LLL_Factorization.LLL_Factorization_Impl"
17:37:17Found termination order: "{}"
17:37:17Found termination order: "length <*mlex*> {}"
17:37:17locale LLL_implementation
17:37:17 fixes p :: "int"
17:37:17 and pl :: "int"
17:37:17### theory "LLL_Factorization.LLL_Factorization_Impl"
17:37:17### 3.663s elapsed time, 7.152s cpu time, 0.312s GC time
17:37:17isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/outline -o pdf -n outline -t /proof,/ML
17:37:17isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Factorization/document -o pdf -n document
17:37:17*** Failed to load theory "LLL_Factorization.LLL_Factorization" (unresolved "LLL_Factorization.LLL_Factorization_Impl")
17:37:17*** Failed to load theory "LLL_Factorization.Factorization_Algorithm_16_22" (unresolved "LLL_Factorization.LLL_Factorization")
17:37:17*** Failed to load theory "LLL_Factorization.Modern_Computer_Algebra_Problem" (unresolved "LLL_Factorization.Factorization_Algorithm_16_22")
17:37:17*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ set"
17:37:17***
17:37:17*** Type error in application: incompatible operand type
17:37:17***
17:37:17*** Operator: Congruence.partition ::
17:37:17*** ??'a set \<Rightarrow> ??'a set set \<Rightarrow> bool
17:37:17*** Operand: \<lambda>gi. poly_mod.dvdm p gi f1 :: int poly \<Rightarrow> bool
17:37:17***
17:37:17*** Coercion Inference:
17:37:17***
17:37:17*** Local coercion insertion on the operand failed:
17:37:17*** No coercion known for type constructors: "fun" and "set"
17:37:17*** At command "function" (line 72 of "~~/afp/thys/LLL_Factorization/LLL_Factorization_Impl.thy")
17:37:17Running Treaps ...
17:37:19Treaps: theory HOL-Data_Structures.Cmp
17:37:19Treaps: theory HOL-Data_Structures.Less_False
17:37:19Treaps: theory HOL-Data_Structures.Sorted_Less
17:37:19Treaps: theory HOL-Data_Structures.List_Ins_Del
17:37:20Treaps: theory HOL-Data_Structures.Set_Specs
17:37:20Treaps: theory HOL-Library.Function_Algebras
17:37:20Treaps: theory HOL-Data_Structures.Tree_Set
17:37:20Treaps: theory HOL-Library.Landau_Symbols
17:37:21Treaps: theory Landau_Symbols.Group_Sort
17:37:22Timing Bertrands_Postulate (2 threads, 83.495s elapsed time, 161.536s cpu time, 3.860s GC time, factor 1.93)
17:37:22Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate
17:37:22Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate/document.pdf
17:37:22Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bertrands_Postulate/outline.pdf
17:37:22Finished Bertrands_Postulate (0:01:29 elapsed time, 0:02:50 cpu time, factor 1.91)
17:37:22Running Probabilistic_System_Zoo-BNFs ...
17:37:22Treaps: theory List-Index.List_Index
17:37:23Treaps: theory Landau_Symbols.Landau_Real_Products
17:37:23Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
17:37:23Probabilistic_System_Zoo-BNFs: theory HOL-Library.Adhoc_Overloading
17:37:23Probabilistic_System_Zoo-BNFs: theory HOL-Library.Cardinal_Notations
17:37:23Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Probability_Measure
17:37:23Probabilistic_System_Zoo-BNFs: theory HOL-Library.Monad_Syntax
17:37:23Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Fun_More
17:37:23Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Order_Relation_More
17:37:24Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity
17:37:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/document.pdf
17:37:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/outline.pdf
17:37:24Call_Arity FAILED
17:37:24(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Call_Arity)
17:37:24(PROP ?P \<Longrightarrow> True) \<equiv> True
17:37:24[1]Rewriting:
17:37:24(x' = y \<Longrightarrow> True) \<equiv> True
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Ignoring duplicate rewrite rule:
17:37:24### map_transform ?t1 ?ae1 [] \<equiv> []
17:37:24### Ignoring duplicate rewrite rule:
17:37:24### map_transform ?t1 ?ae1 [] \<equiv> []
17:37:24### Ignoring duplicate rewrite rule:
17:37:24### map_transform ?t1 ?ae1 [] \<equiv> []
17:37:24Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24Found termination order: "size <*mlex*> {}"
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Ignoring duplicate rewrite rule:
17:37:24### map_transform ?t1 ?ae1 [] \<equiv> []
17:37:24### Cannot solve equivariance for Abs_cfun
17:37:24### Ignoring duplicate introduction (intro)
17:37:24### (?\<Gamma>, ?e, Upd ?x # ?S) \<Rightarrow>\<^sub>G
17:37:24### (?\<Gamma>, ?e, ?S @ [Dummy ?x])
17:37:24### Ignoring duplicate introduction (intro)
17:37:24### (?\<Gamma>, ?e, Upd ?x # ?S) \<Rightarrow>\<^sub>G
17:37:24### (?\<Gamma>, ?e, ?S @ [Dummy ?x])
17:37:24isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/document -o pdf -n document
17:37:24isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Call_Arity/outline -o pdf -n outline -t /proof,/ML
17:37:24*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:37:24***
17:37:24*** Type error in application: incompatible operand type
17:37:24***
17:37:24*** Operator: (=) m :: ('b \<Rightarrow> 'c option) \<Rightarrow> bool
17:37:24*** Operand: {} :: ??'a set
17:37:24***
17:37:24*** At command "by" (line 21 of "~~/afp/thys/Call_Arity/AList-Utils-HOLCF.thy")
17:37:24Running Polynomial_Factorization ...
17:37:24Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Order_Union
17:37:24Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellfounded_More
17:37:24Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Relation
17:37:24Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Embedding
17:37:24Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Constructions
17:37:25Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Giry_Monad
17:37:26Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinal_Order_Relation
17:37:27Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinal_Arithmetic
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Precomputation
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial
17:37:27Treaps: theory Landau_Symbols.Landau_Simprocs
17:37:27Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Ordinal_Arithmetic
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility
17:37:27Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Wellorder_Extension
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
17:37:27Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots
17:37:28Polynomial_Factorization: theory Polynomial_Factorization.Missing_List
17:37:28Treaps: theory Landau_Symbols.Landau_More
17:37:28Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
17:37:28Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly
17:37:29Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Cardinals
17:37:29Timing Elliptic_Curves_Group_Law (2 threads, 66.035s elapsed time, 124.804s cpu time, 7.140s GC time, factor 1.89)
17:37:29Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law
17:37:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/document.pdf
17:37:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/outline.pdf
17:37:29Finished Elliptic_Curves_Group_Law (0:01:13 elapsed time, 0:02:15 cpu time, factor 1.85)
17:37:29Running Tarskis_Geometry ...
17:37:29Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma
17:37:30Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly
17:37:31Tarskis_Geometry: theory HOL-Algebra.Congruence
17:37:31Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant
17:37:31Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset
17:37:31Tarskis_Geometry: theory Tarskis_Geometry.Metric
17:37:31Tarskis_Geometry: theory Tarskis_Geometry.Miscellany
17:37:31Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization
17:37:31Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization
17:37:31Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
17:37:31Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2
17:37:32Tarskis_Geometry: theory Tarskis_Geometry.Tarski
17:37:32Tarskis_Geometry: theory HOL-Algebra.Order
17:37:32Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test
17:37:32Treaps: theory Random_BSTs.Random_BSTs
17:37:33Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski
17:37:33Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization
17:37:33Tarskis_Geometry: theory HOL-Algebra.Lattice
17:37:35Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice
17:37:35Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization
17:37:36Tarskis_Geometry: theory HOL-Algebra.Group
17:37:38Tarskis_Geometry: theory Tarskis_Geometry.Action
17:37:38Tarskis_Geometry: theory Tarskis_Geometry.Projective
17:37:41Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski
17:37:48Treaps: theory Treaps.Treap
17:37:48Treaps: theory Treaps.Probability_Misc
17:37:49Treaps: theory Treaps.Random_List_Permutation
17:37:50Treaps: theory Treaps.Treap_Sort_and_BSTs
17:37:53Treaps: theory Treaps.Random_Treap
17:38:02Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl
17:38:05Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Probability_Mass_Function
17:38:05Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bool_Bounded_Set
17:38:05Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bounded_Set
17:38:06Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Nonempty_Bounded_Set
17:38:11Timing Irrationality_J_Hancl (2 threads, 61.975s elapsed time, 113.564s cpu time, 5.836s GC time, factor 1.83)
17:38:11Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Irrationality_J_Hancl
17:38:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Irrationality_J_Hancl/document.pdf
17:38:11Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Irrationality_J_Hancl/outline.pdf
17:38:11Finished Irrationality_J_Hancl (0:01:07 elapsed time, 0:02:02 cpu time, factor 1.82)
17:38:11Running Probabilistic_System_Zoo ...
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Fun_More
17:38:13Probabilistic_System_Zoo: theory HOL-Library.Cardinal_Notations
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Relation_More
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Order_Union
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Extension
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellfounded_More
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Relation
17:38:13Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Embedding
17:38:14Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Wellorder_Constructions
17:38:15Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Order_Relation
17:38:15Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Ordinal_Arithmetic
17:38:16Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinal_Arithmetic
17:38:16Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Cardinals
17:38:16Timing Koenigsberg_Friendship (2 threads, 60.070s elapsed time, 110.076s cpu time, 5.224s GC time, factor 1.83)
17:38:16Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship
17:38:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship/document.pdf
17:38:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship/outline.pdf
17:38:16Finished Koenigsberg_Friendship (0:01:07 elapsed time, 0:02:01 cpu time, factor 1.80)
17:38:16Running Probabilistic_System_Zoo-Non_BNFs ...
17:38:17Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bounded_Set
17:38:17Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
17:38:18Probabilistic_System_Zoo-Non_BNFs: theory HOL-Eisbach.Eisbach
17:38:18Probabilistic_System_Zoo-Non_BNFs: theory HOL-Library.Cardinal_Notations
17:38:18Timing SDS_Impossibility (2 threads, 57.586s elapsed time, 80.900s cpu time, 2.320s GC time, factor 1.40)
17:38:18Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility
17:38:18Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility/document.pdf
17:38:18Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SDS_Impossibility/outline.pdf
17:38:18Finished SDS_Impossibility (0:01:02 elapsed time, 0:01:29 cpu time, factor 1.42)
17:38:18Running VectorSpace ...
17:38:18Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Fun_More
17:38:18Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Relation_More
17:38:18Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Order_Union
17:38:19Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellfounded_More
17:38:19Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Relation
17:38:19Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Extension
17:38:19Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Embedding
17:38:19Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Wellorder_Constructions
17:38:19Timing Treaps (2 threads, 56.197s elapsed time, 104.972s cpu time, 4.748s GC time, factor 1.87)
17:38:19Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Treaps
17:38:19Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Treaps/document.pdf
17:38:19Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Treaps/outline.pdf
17:38:19Finished Treaps (0:01:01 elapsed time, 0:01:53 cpu time, factor 1.84)
17:38:19Running Stern_Brocot ...
17:38:20Timing Probabilistic_System_Zoo-BNFs (2 threads, 52.808s elapsed time, 92.480s cpu time, 3.632s GC time, factor 1.75)
17:38:20Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs
17:38:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs/document.pdf
17:38:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-BNFs/outline.pdf
17:38:20Finished Probabilistic_System_Zoo-BNFs (0:00:58 elapsed time, 0:01:41 cpu time, factor 1.74)
17:38:20Running Lp ...
17:38:20VectorSpace: theory VectorSpace.FunctionLemmas
17:38:20VectorSpace: theory VectorSpace.RingModuleFacts
17:38:20Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Order_Relation
17:38:20Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Ordinal_Arithmetic
17:38:21Stern_Brocot: theory HOL-Library.BNF_Corec
17:38:21VectorSpace: theory VectorSpace.MonoidSums
17:38:21Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinal_Arithmetic
17:38:22VectorSpace: theory VectorSpace.LinearCombinations
17:38:22Lp: theory Ergodic_Theory.SG_Library_Complement
17:38:22Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Cardinals
17:38:22Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Bounded_Set
17:38:23Lp: theory Lp.Functional_Spaces
17:38:23Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Nonempty_Bounded_Set
17:38:23Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy
17:38:24Lp: theory Lp.Lp
17:38:24Timing Polynomial_Factorization (2 threads, 51.812s elapsed time, 89.264s cpu time, 3.644s GC time, factor 1.72)
17:38:24Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization
17:38:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf
17:38:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf
17:38:24Finished Polynomial_Factorization (0:01:00 elapsed time, 0:01:42 cpu time, factor 1.69)
17:38:25Running pGCL ...
17:38:26pGCL: theory pGCL.Misc
17:38:26pGCL: theory pGCL.Expectations
17:38:27pGCL: theory pGCL.Transformers
17:38:28VectorSpace: theory VectorSpace.SumSpaces
17:38:28VectorSpace: theory VectorSpace.VectorSpace
17:38:28pGCL: theory pGCL.Induction
17:38:29Stern_Brocot: theory Stern_Brocot.Cotree
17:38:29pGCL: theory pGCL.Embedding
17:38:29Timing Tarskis_Geometry (2 threads, 51.079s elapsed time, 90.280s cpu time, 3.900s GC time, factor 1.77)
17:38:29Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tarskis_Geometry
17:38:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tarskis_Geometry/document.pdf
17:38:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Tarskis_Geometry/outline.pdf
17:38:29Finished Tarskis_Geometry (0:00:59 elapsed time, 0:01:42 cpu time, factor 1.73)
17:38:29Tree-Automata CANCELLED
17:38:29ROBDD CANCELLED
17:38:29Running Monomorphic_Monad ...
17:38:29pGCL: theory pGCL.Healthiness
17:38:30pGCL: theory pGCL.Continuity
17:38:31Monomorphic_Monad: theory HOL-Library.Cardinal_Notations
17:38:31Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
17:38:31pGCL: theory pGCL.LoopInduction
17:38:31pGCL: theory pGCL.Sublinearity
17:38:31pGCL: theory pGCL.WellDefined
17:38:32pGCL: theory pGCL.Algebra
17:38:33pGCL: theory pGCL.StructuredReasoning
17:38:33Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
17:38:33pGCL: theory pGCL.Automation
17:38:35pGCL: theory pGCL.Determinism
17:38:35pGCL: theory pGCL.Loops
17:38:35pGCL: theory pGCL.Termination
17:38:35Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
17:38:35pGCL: theory pGCL.pGCL
17:38:36Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
17:38:36Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
17:38:36pGCL: theory pGCL.LoopExamples
17:38:36pGCL: theory pGCL.Monty
17:38:36pGCL: theory pGCL.Primitives
17:38:38Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
17:38:41Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi
17:38:53Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
17:38:55Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
17:38:55Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
17:38:55Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
17:39:00Stern_Brocot: theory Stern_Brocot.Bird_Tree
17:39:01Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi_Counterexample
17:39:01Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Finitely_Bounded_Set_Counterexample
17:39:05Timing Lp (2 threads, 38.146s elapsed time, 67.040s cpu time, 1.716s GC time, factor 1.76)
17:39:05Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp
17:39:05Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp/document.pdf
17:39:05Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lp/outline.pdf
17:39:05Finished Lp (0:00:44 elapsed time, 0:01:16 cpu time, factor 1.72)
17:39:05Running Rewriting_Z ...
17:39:06Timing Stern_Brocot (2 threads, 39.598s elapsed time, 61.272s cpu time, 4.288s GC time, factor 1.55)
17:39:06Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot
17:39:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot/document.pdf
17:39:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stern_Brocot/outline.pdf
17:39:06Finished Stern_Brocot (0:00:45 elapsed time, 0:01:10 cpu time, factor 1.54)
17:39:06Buchi_Complementation CANCELLED
17:39:06Running Kuratowski_Closure_Complement ...
17:39:06Timing Probabilistic_System_Zoo (2 threads, 49.481s elapsed time, 81.392s cpu time, 3.932s GC time, factor 1.64)
17:39:06Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo
17:39:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/document.pdf
17:39:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf
17:39:06Finished Probabilistic_System_Zoo (0:00:54 elapsed time, 0:01:29 cpu time, factor 1.63)
17:39:06Running Euler_MacLaurin ...
17:39:07Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem
17:39:07Timing Probabilistic_System_Zoo-Non_BNFs (2 threads, 45.517s elapsed time, 85.296s cpu time, 5.032s GC time, factor 1.87)
17:39:07Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs
17:39:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/document.pdf
17:39:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/outline.pdf
17:39:07Finished Probabilistic_System_Zoo-Non_BNFs (0:00:50 elapsed time, 0:01:32 cpu time, factor 1.83)
17:39:07Knuth_Morris_Pratt CANCELLED
17:39:07Running InformationFlowSlicing_Inter ...
17:39:08Euler_MacLaurin: theory HOL-Library.Function_Algebras
17:39:08Euler_MacLaurin: theory HOL-Library.Stirling
17:39:08Euler_MacLaurin: theory Bernoulli.Bernoulli
17:39:08Timing Monomorphic_Monad (2 threads, 31.160s elapsed time, 50.800s cpu time, 3.080s GC time, factor 1.63)
17:39:08Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monomorphic_Monad
17:39:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monomorphic_Monad/document.pdf
17:39:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monomorphic_Monad/outline.pdf
17:39:08Finished Monomorphic_Monad (0:00:38 elapsed time, 0:01:02 cpu time, factor 1.60)
17:39:08Floyd_Warshall CANCELLED
17:39:08Running RSAPSS ...
17:39:08Euler_MacLaurin: theory HOL-Library.Landau_Symbols
17:39:08Euler_MacLaurin: theory Bernoulli.Bernoulli_FPS
17:39:08Timing VectorSpace (2 threads, 43.947s elapsed time, 75.244s cpu time, 6.880s GC time, factor 1.71)
17:39:08Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace
17:39:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/document.pdf
17:39:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/VectorSpace/outline.pdf
17:39:08Finished VectorSpace (0:00:50 elapsed time, 0:01:24 cpu time, factor 1.68)
17:39:08Running Pratt_Certificate ...
17:39:09Timing pGCL (2 threads, 34.930s elapsed time, 67.456s cpu time, 2.240s GC time, factor 1.93)
17:39:09Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/pGCL
17:39:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/pGCL/document.pdf
17:39:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/pGCL/outline.pdf
17:39:09Finished pGCL (0:00:43 elapsed time, 0:01:20 cpu time, factor 1.84)
17:39:09Running Jordan_Hoelder ...
17:39:09Rewriting_Z: theory HOL-Eisbach.Eisbach
17:39:09Rewriting_Z: theory Abstract-Rewriting.Seq
17:39:10Rewriting_Z: theory HOL-Library.While_Combinator
17:39:10InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.NonInterferenceInter
17:39:10Rewriting_Z: theory Regular-Sets.Regular_Set
17:39:10Euler_MacLaurin: theory Bernoulli.Periodic_Bernpoly
17:39:10RSAPSS: theory RSAPSS.Word
17:39:10Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
17:39:11Pratt_Certificate: theory Lehmer.Lehmer
17:39:11Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate
17:39:11Euler_MacLaurin: theory Landau_Symbols.Group_Sort
17:39:11Jordan_Hoelder: theory Secondary_Sylow.GroupAction
17:39:11Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses
17:39:12Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation
17:39:12Jordan_Hoelder: theory Secondary_Sylow.SndSylow
17:39:12Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp
17:39:12Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
17:39:13Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups
17:39:13Rewriting_Z: theory Regular-Sets.Regular_Exp
17:39:13Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups
17:39:14Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups
17:39:14Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries
17:39:14InformationFlowSlicing_Inter: theory InformationFlowSlicing_Inter.LiftingInter
17:39:14Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder
17:39:15RSAPSS: theory RSAPSS.Mod
17:39:15RSAPSS: theory RSAPSS.WordOperations
17:39:15RSAPSS: theory RSAPSS.Crypt
17:39:15RSAPSS: theory RSAPSS.Pdifference
17:39:15RSAPSS: theory RSAPSS.Productdivides
17:39:15RSAPSS: theory RSAPSS.Cryptinverts
17:39:16Rewriting_Z: theory Regular-Sets.NDerivative
17:39:16Rewriting_Z: theory Regular-Sets.Relation_Interpretation
17:39:17Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
17:39:17RSAPSS: theory RSAPSS.SHA1Padding
17:39:17RSAPSS: theory RSAPSS.SHA1
17:39:17RSAPSS: theory RSAPSS.Wordarith
17:39:18Euler_MacLaurin: theory Landau_Symbols.Landau_More
17:39:18Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
17:39:18RSAPSS: theory RSAPSS.EMSAPSS
17:39:19RSAPSS: theory RSAPSS.RSAPSS
17:39:21Rewriting_Z: theory Regular-Sets.Equivalence_Checking
17:39:21Rewriting_Z: theory Regular-Sets.Regexp_Method
17:39:22Rewriting_Z: theory Abstract-Rewriting.Abstract_Rewriting
17:39:24Rewriting_Z: theory Rewriting_Z.Z
17:39:24Rewriting_Z: theory Rewriting_Z.CL_Z
17:39:24Rewriting_Z: theory Rewriting_Z.Lambda_Z
17:39:34Timing Jordan_Hoelder (2 threads, 18.069s elapsed time, 33.420s cpu time, 1.664s GC time, factor 1.85)
17:39:34Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder
17:39:34Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/document.pdf
17:39:34Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/outline.pdf
17:39:34Finished Jordan_Hoelder (0:00:24 elapsed time, 0:00:43 cpu time, factor 1.74)
17:39:34Running Error_Function ...
17:39:35Timing Pratt_Certificate (2 threads, 20.711s elapsed time, 40.516s cpu time, 0.840s GC time, factor 1.96)
17:39:35Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate
17:39:35Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate/document.pdf
17:39:35Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Pratt_Certificate/outline.pdf
17:39:35Finished Pratt_Certificate (0:00:26 elapsed time, 0:00:49 cpu time, factor 1.86)
17:39:35Running Fermat3_4 ...
17:39:35Error_Function: theory HOL-Library.Function_Algebras
17:39:35Error_Function: theory HOL-Library.Landau_Symbols
17:39:35Error_Function: theory Landau_Symbols.Group_Sort
17:39:36Timing RSAPSS (2 threads, 21.881s elapsed time, 40.944s cpu time, 1.528s GC time, factor 1.87)
17:39:36Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RSAPSS
17:39:36Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RSAPSS/document.pdf
17:39:36Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/RSAPSS/outline.pdf
17:39:36Finished RSAPSS (0:00:28 elapsed time, 0:00:50 cpu time, factor 1.79)
17:39:36Running Catalan_Numbers ...
17:39:37Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing_Inter
17:39:37Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing_Inter/document.pdf
17:39:37Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing_Inter/outline.pdf
17:39:37InformationFlowSlicing_Inter FAILED
17:39:37(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/InformationFlowSlicing_Inter)
17:39:37### ("\<^const>BasicDefs.edge_kind.ReturnEdge" ("_position" Q)
17:39:37### ("_position" Main) ("_position" f))))
17:39:37### Fortunately, only one parse tree is well-formed and type-correct,
17:39:37### but you may still want to disambiguate your grammar or your input.
17:39:37### Ambiguous input (line 1878 of "~~/afp/thys/InformationFlowSlicing_Inter/LiftingInter.thy") produces 2 parse trees:
17:39:37### ("\<^const>HOL.Trueprop"
17:39:37### ("\<^const>BasicDefs.edge_kind.ReturnEdge"
17:39:37### ("\<^const>HOL.eq" ("_applC" ("_position" knd) ("_position" a'))
17:39:37### ("_position" Q'))
17:39:37### ("_position" p') ("_position" f')))
17:39:37### ("\<^const>HOL.Trueprop"
17:39:37### ("\<^const>HOL.eq" ("_applC" ("_position" knd) ("_position" a'))
17:39:37### ("\<^const>BasicDefs.edge_kind.ReturnEdge" ("_position" Q')
17:39:37### ("_position" p') ("_position" f'))))
17:39:37### Fortunately, only one parse tree is well-formed and type-correct,
17:39:37### but you may still want to disambiguate your grammar or your input.
17:39:37### Ambiguous input (line 1880 of "~~/afp/thys/InformationFlowSlicing_Inter/LiftingInter.thy") produces 2 parse trees:
17:39:37### ("\<^const>HOL.Trueprop"
17:39:37### ("\<^const>BasicDefs.edge_kind.ReturnEdge"
17:39:37### ("\<^const>HOL.eq" ("_applC" ("_position" kind) ("_position" x'))
17:39:37### ("_position" Q'))
17:39:37### ("_position" p') ("_position" f')))
17:39:37### ("\<^const>HOL.Trueprop"
17:39:37### ("\<^const>HOL.eq" ("_applC" ("_position" kind) ("_position" x'))
17:39:37### ("\<^const>BasicDefs.edge_kind.ReturnEdge" ("_position" Q')
17:39:37### ("_position" p') ("_position" f'))))
17:39:37### Fortunately, only one parse tree is well-formed and type-correct,
17:39:37### but you may still want to disambiguate your grammar or your input.
17:39:37isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing_Inter/document -o pdf -n document
17:39:37isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing_Inter/outline -o pdf -n outline -t /proof,/ML
17:39:37*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:39:37***
17:39:37*** Type error in application: incompatible operand type
17:39:37***
17:39:37*** Operator: (=) (csppa (targetnode a) (HRB_slice S) 0 fs ! i) ::
17:39:37*** (('var \<Rightarrow> 'val option) \<Rightarrow> 'val option)
17:39:37*** \<Rightarrow> bool
17:39:37*** Operand: {} :: ??'a set
17:39:37***
17:39:37*** At command "have" (line 702 of "~~/afp/thys/InformationFlowSlicing_Inter/NonInterferenceInter.thy")
17:39:37Running Cayley_Hamilton ...
17:39:37Fermat3_4: theory Fermat3_4.Fermat4
17:39:37Fermat3_4: theory Fermat3_4.Quad_Form
17:39:37Catalan_Numbers: theory HOL-Library.Function_Algebras
17:39:37Catalan_Numbers: theory HOL-Library.Landau_Symbols
17:39:38Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral
17:39:38Fermat3_4: theory Fermat3_4.Fermat3
17:39:38Catalan_Numbers: theory Landau_Symbols.Group_Sort
17:39:38Cayley_Hamilton: theory HOL-Library.More_List
17:39:38Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
17:39:38Error_Function: theory Error_Function.Error_Function
17:39:38Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
17:39:39Error_Function: theory Landau_Symbols.Landau_Real_Products
17:39:40Timing Kuratowski_Closure_Complement (2 threads, 28.035s elapsed time, 48.268s cpu time, 1.548s GC time, factor 1.72)
17:39:40Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kuratowski_Closure_Complement
17:39:40Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kuratowski_Closure_Complement/document.pdf
17:39:40Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf
17:39:40Finished Kuratowski_Closure_Complement (0:00:33 elapsed time, 0:00:57 cpu time, factor 1.72)
17:39:40Running Bernoulli ...
17:39:40Timing Rewriting_Z (2 threads, 30.446s elapsed time, 51.948s cpu time, 2.440s GC time, factor 1.71)
17:39:40Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rewriting_Z
17:39:40Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rewriting_Z/document.pdf
17:39:40Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rewriting_Z/outline.pdf
17:39:40Finished Rewriting_Z (0:00:34 elapsed time, 0:01:03 cpu time, factor 1.83)
17:39:40Running Consensus_Refined ...
17:39:40Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
17:39:41Bernoulli: theory HOL-Library.Stirling
17:39:41Bernoulli: theory Bernoulli.Bernoulli
17:39:41Consensus_Refined: theory Consensus_Refined.Consensus_Misc
17:39:41Consensus_Refined: theory Consensus_Refined.Consensus_Types
17:39:41Consensus_Refined: theory Consensus_Refined.Quorums
17:39:41Consensus_Refined: theory Consensus_Refined.Infra
17:39:41Consensus_Refined: theory Consensus_Refined.Refinement
17:39:41Bernoulli: theory Bernoulli.Periodic_Bernpoly
17:39:41Consensus_Refined: theory Consensus_Refined.Three_Steps
17:39:41Bernoulli: theory Bernoulli.Bernoulli_FPS
17:39:41Consensus_Refined: theory Consensus_Refined.Two_Steps
17:39:42Consensus_Refined: theory HOL-Library.Infinite_Set
17:39:42Consensus_Refined: theory HOL-Library.Omega_Words_Fun
17:39:42Timing Euler_MacLaurin (2 threads, 30.386s elapsed time, 52.728s cpu time, 2.344s GC time, factor 1.74)
17:39:42Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Euler_MacLaurin
17:39:42Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Euler_MacLaurin/document.pdf
17:39:42Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Euler_MacLaurin/outline.pdf
17:39:42Finished Euler_MacLaurin (0:00:35 elapsed time, 0:01:01 cpu time, factor 1.72)
17:39:42Running FeatherweightJava ...
17:39:42Consensus_Refined: theory Heard_Of.HOModel
17:39:43Bernoulli: theory Bernoulli.Bernoulli_Zeta
17:39:43FeatherweightJava: theory FeatherweightJava.FJDefs
17:39:43Consensus_Refined: theory Consensus_Refined.Voting
17:39:44Error_Function: theory Landau_Symbols.Landau_Simprocs
17:39:44Consensus_Refined: theory Consensus_Refined.Same_Vote
17:39:44Consensus_Refined: theory Consensus_Refined.MRU_Vote
17:39:44Consensus_Refined: theory Consensus_Refined.MRU_Vote_Opt
17:39:44Error_Function: theory Landau_Symbols.Landau_More
17:39:44Consensus_Refined: theory Consensus_Refined.Observing_Quorums
17:39:44Error_Function: theory Error_Function.Error_Function_Asymptotics
17:39:45Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
17:39:45Consensus_Refined: theory Consensus_Refined.Three_Step_MRU
17:39:45Consensus_Refined: theory Consensus_Refined.Observing_Quorums_Opt
17:39:45Consensus_Refined: theory Consensus_Refined.Two_Step_Observing
17:39:45Consensus_Refined: theory Consensus_Refined.Voting_Opt
17:39:45Catalan_Numbers: theory Landau_Symbols.Landau_More
17:39:46Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
17:39:46Consensus_Refined: theory Consensus_Refined.Ate_Defs
17:39:46Consensus_Refined: theory Consensus_Refined.BenOr_Defs
17:39:47Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
17:39:47Consensus_Refined: theory Consensus_Refined.CT_Defs
17:39:48Consensus_Refined: theory Consensus_Refined.HO_Transition_System
17:39:48Consensus_Refined: theory Consensus_Refined.New_Algorithm_Defs
17:39:49Consensus_Refined: theory Consensus_Refined.OneThirdRule_Defs
17:39:49Consensus_Refined: theory Consensus_Refined.Paxos_Defs
17:39:50Consensus_Refined: theory Consensus_Refined.Uv_Defs
17:39:50Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FeatherweightJava
17:39:50Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FeatherweightJava/document.pdf
17:39:50Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FeatherweightJava/outline.pdf
17:39:50FeatherweightJava FAILED
17:39:50(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/FeatherweightJava)
17:39:50*** ("\<^const>Pure.eq"
17:39:50*** ("\<^fixed>substs_syn" ("_position" ds) ("_position" xs) ("_position" e))
17:39:50*** ("_applC" ("_position" substs)
17:39:50*** ("_cargs"
17:39:50*** ("_applC" ("_position" map_upds)
17:39:50*** ("_cargs" ("_position" empty)
17:39:50*** ("_cargs" ("_position" xs) ("_position" ds))))
17:39:50*** ("_position" e))))
17:39:50*** ("\<^const>Pure.eq"
17:39:50*** ("_applC"
17:39:50*** ("\<^const>Fields.inverse_class.inverse_divide" ("_position" ds)
17:39:50*** ("_position" xs))
17:39:50*** ("_position" e))
17:39:50*** ("_applC" ("_position" substs)
17:39:50*** ("_cargs"
17:39:50*** ("_applC" ("_position" map_upds)
17:39:50*** ("_cargs" ("_position" empty)
17:39:50*** ("_cargs" ("_position" xs) ("_position" ds))))
17:39:50*** ("_position" e))))
17:39:50*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")
17:39:50*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:39:50***
17:39:50*** Type error in application: incompatible operand type
17:39:50***
17:39:50*** Operator: map_upds ::
17:39:50*** (??'a \<Rightarrow> ??'b option)
17:39:50*** \<Rightarrow> ??'a list
17:39:50*** \<Rightarrow> ??'b list
17:39:50*** \<Rightarrow> ??'a \<Rightarrow> ??'b option
17:39:50*** Operand: {} :: ??'c set
17:39:50***
17:39:50*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")
17:39:50*** Type unification failed: No type arity fun :: inverse
17:39:50***
17:39:50*** Type error in application: operator not of function type
17:39:50***
17:39:50*** Operator: ds / xs :: ??'a
17:39:50*** Operand: e :: ??'b
17:39:50***
17:39:50*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")
17:39:50Running Featherweight_OCL ...
17:39:52Consensus_Refined: theory Heard_Of.Majorities
17:39:52Consensus_Refined: theory Stuttering_Equivalence.Samplers
17:39:52Consensus_Refined: theory Consensus_Refined.Ate_Proofs
17:39:52Consensus_Refined: theory Consensus_Refined.CT_Proofs
17:39:52Consensus_Refined: theory Consensus_Refined.New_Algorithm_Proofs
17:39:53Consensus_Refined: theory Consensus_Refined.OneThirdRule_Proofs
17:39:53Consensus_Refined: theory Consensus_Refined.Paxos_Proofs
17:39:53Consensus_Refined: theory Stuttering_Equivalence.StutterEquivalence
17:39:54Consensus_Refined: theory Heard_Of.Reduction
17:39:55Consensus_Refined: theory Consensus_Refined.BenOr_Proofs
17:39:55Consensus_Refined: theory Consensus_Refined.Uv_Proofs
17:39:57Timing Error_Function (2 threads, 18.182s elapsed time, 34.392s cpu time, 1.756s GC time, factor 1.89)
17:39:57Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Error_Function
17:39:57Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Error_Function/document.pdf
17:39:57Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Error_Function/outline.pdf
17:39:57Finished Error_Function (0:00:23 elapsed time, 0:00:42 cpu time, factor 1.83)
17:39:57Running Game_Based_Crypto ...
17:39:58Timing Catalan_Numbers (2 threads, 16.970s elapsed time, 32.040s cpu time, 1.748s GC time, factor 1.89)
17:39:58Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Catalan_Numbers
17:39:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Catalan_Numbers/document.pdf
17:39:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Catalan_Numbers/outline.pdf
17:39:58Finished Catalan_Numbers (0:00:21 elapsed time, 0:00:39 cpu time, factor 1.82)
17:39:58Running Zeta_Function ...
17:39:59Timing Cayley_Hamilton (2 threads, 16.934s elapsed time, 30.432s cpu time, 1.400s GC time, factor 1.80)
17:39:59Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cayley_Hamilton
17:39:59Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cayley_Hamilton/document.pdf
17:39:59Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cayley_Hamilton/outline.pdf
17:39:59Finished Cayley_Hamilton (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.74)
17:39:59Running Orbit_Stabiliser ...
17:39:59Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym
17:39:59Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman
17:40:00Timing Fermat3_4 (2 threads, 17.733s elapsed time, 32.192s cpu time, 0.892s GC time, factor 1.82)
17:40:00Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4
17:40:00Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4/document.pdf
17:40:00Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fermat3_4/outline.pdf
17:40:00Finished Fermat3_4 (0:00:24 elapsed time, 0:00:41 cpu time, factor 1.71)
17:40:00Running Random_Graph_Subgraph_Threshold ...
17:40:00Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single
17:40:00Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function
17:40:00Timing Bernoulli (2 threads, 14.324s elapsed time, 20.068s cpu time, 0.572s GC time, factor 1.40)
17:40:00Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli
17:40:00Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli/document.pdf
17:40:00Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Bernoulli/outline.pdf
17:40:00Finished Bernoulli (0:00:20 elapsed time, 0:00:28 cpu time, factor 1.42)
17:40:00Running InformationFlowSlicing ...
17:40:00Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation
17:40:00Zeta_Function: theory Bernoulli.Bernoulli_Zeta
17:40:00Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One
17:40:01Featherweight_OCL: theory Featherweight_OCL.UML_Types
17:40:01Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset
17:40:01Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
17:40:01Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
17:40:01Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser
17:40:01Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
17:40:02Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron
17:40:02Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
17:40:02Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
17:40:02Featherweight_OCL: theory Featherweight_OCL.UML_Logic
17:40:02InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceIntra
17:40:03Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
17:40:03Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
17:40:03InformationFlowSlicing: theory InformationFlowSlicing.LiftingIntra
17:40:03Featherweight_OCL: theory Featherweight_OCL.UML_PropertyProfiles
17:40:04Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
17:40:04Featherweight_OCL: theory Featherweight_OCL.UML_Boolean
17:40:04Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
17:40:05Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
17:40:05Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
17:40:05InformationFlowSlicing: theory InformationFlowSlicing.NonInterferenceWhile
17:40:05Zeta_Function: theory Zeta_Function.Zeta_Function
17:40:06Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
17:40:06Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
17:40:06Featherweight_OCL: theory Featherweight_OCL.UML_Integer
17:40:07Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
17:40:09Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
17:40:11Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
17:40:13Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
17:40:13Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
17:40:14Featherweight_OCL: theory Featherweight_OCL.UML_Sequence
17:40:16Featherweight_OCL: theory Featherweight_OCL.UML_Pair
17:40:17Timing Random_Graph_Subgraph_Threshold (2 threads, 10.699s elapsed time, 20.040s cpu time, 0.692s GC time, factor 1.87)
17:40:17Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf
17:40:17Finished Random_Graph_Subgraph_Threshold (0:00:16 elapsed time, 0:00:28 cpu time, factor 1.73)
17:40:17Timing InformationFlowSlicing (2 threads, 9.526s elapsed time, 17.268s cpu time, 0.920s GC time, factor 1.81)
17:40:17Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing/document.pdf
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/InformationFlowSlicing/outline.pdf
17:40:17Finished InformationFlowSlicing (0:00:16 elapsed time, 0:00:26 cpu time, factor 1.62)
17:40:17Timing Orbit_Stabiliser (2 threads, 11.268s elapsed time, 15.356s cpu time, 0.688s GC time, factor 1.36)
17:40:17Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser/document.pdf
17:40:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Orbit_Stabiliser/outline.pdf
17:40:17Finished Orbit_Stabiliser (0:00:17 elapsed time, 0:00:24 cpu time, factor 1.37)
17:40:17Running LightweightJava ...
17:40:17Running Locally-Nameless-Sigma ...
17:40:17Running SIFUM_Type_Systems ...
17:40:17Featherweight_OCL: theory Featherweight_OCL.UML_Real
17:40:18Locally-Nameless-Sigma: theory HOL-Proofs-Lambda.Commutation
17:40:18Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.Environments
17:40:18SIFUM_Type_Systems: theory HOL-Library.Lattice_Syntax
17:40:18SIFUM_Type_Systems: theory SIFUM_Type_Systems.Preliminaries
17:40:18Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.ListPre
17:40:18Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.FMap
17:40:18LightweightJava: theory LightweightJava.Lightweight_Java_Definition
17:40:18Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.Sigma
17:40:19Timing Zeta_Function (2 threads, 13.650s elapsed time, 19.824s cpu time, 0.560s GC time, factor 1.45)
17:40:19Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Zeta_Function
17:40:19Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Zeta_Function/document.pdf
17:40:19Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Zeta_Function/outline.pdf
17:40:19Finished Zeta_Function (0:00:19 elapsed time, 0:00:28 cpu time, factor 1.47)
17:40:19Running Separation_Algebra ...
17:40:19Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
17:40:19SIFUM_Type_Systems: theory SIFUM_Type_Systems.Language
17:40:19SIFUM_Type_Systems: theory SIFUM_Type_Systems.Security
17:40:20Separation_Algebra: theory HOL-Hoare.Hoare_Logic_Abort
17:40:20Separation_Algebra: theory Separation_Algebra.Types_D
17:40:21SIFUM_Type_Systems: theory SIFUM_Type_Systems.Compositionality
17:40:22Separation_Algebra: theory Separation_Algebra.Map_Extra
17:40:22Separation_Algebra: theory Separation_Algebra.Separation_Algebra
17:40:23Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.ParRed
17:40:23Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.TypedSigma
17:40:23Separation_Algebra: theory Separation_Algebra.Sep_Heap_Instance
17:40:23Separation_Algebra: theory Separation_Algebra.Sep_Tactics
17:40:24Separation_Algebra: theory Separation_Algebra.Sep_Tactics_Test
17:40:24Separation_Algebra: theory Separation_Algebra.Simple_Separation_Example
17:40:24SIFUM_Type_Systems: theory SIFUM_Type_Systems.LocallySoundModeUse
17:40:24SIFUM_Type_Systems: theory SIFUM_Type_Systems.TypeSystem
17:40:25Separation_Algebra: theory Separation_Algebra.VM_Example
17:40:25Separation_Algebra: theory Separation_Algebra.Abstract_Separation_D
17:40:25Featherweight_OCL: theory Featherweight_OCL.UML_String
17:40:26Separation_Algebra: theory Separation_Algebra.Separation_Algebra_Alt
17:40:27Locally-Nameless-Sigma: theory Locally-Nameless-Sigma.Locally_Nameless_Sigma
17:40:27Separation_Algebra: theory Separation_Algebra.Sep_Eq
17:40:27Separation_Algebra: theory Separation_Algebra.Separation_D
17:40:28Featherweight_OCL: theory Featherweight_OCL.UML_Void
17:40:29Featherweight_OCL: theory Featherweight_OCL.UML_Bag
17:40:30LightweightJava: theory LightweightJava.Lightweight_Java_Equivalence
17:40:31Featherweight_OCL: theory Featherweight_OCL.UML_Set
17:40:32Timing Consensus_Refined (2 threads, 44.969s elapsed time, 81.664s cpu time, 6.416s GC time, factor 1.82)
17:40:32Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Consensus_Refined
17:40:32Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Consensus_Refined/document.pdf
17:40:32Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Consensus_Refined/outline.pdf
17:40:32Finished Consensus_Refined (0:00:51 elapsed time, 0:01:32 cpu time, factor 1.79)
17:40:32Running Separation_Logic_Imperative_HOL ...
17:40:32LightweightJava: theory LightweightJava.Lightweight_Java_Proof
17:40:33Separation_Logic_Imperative_HOL: theory HOL-Eisbach.Eisbach
17:40:33Separation_Logic_Imperative_HOL: theory HOL-ex.Quicksort
17:40:34Separation_Logic_Imperative_HOL: theory HOL-Word.Bits
17:40:34Separation_Logic_Imperative_HOL: theory Automatic_Refinement.Misc
17:40:34Separation_Logic_Imperative_HOL: theory HOL-Word.Bits_Bit
17:40:34Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_Numeric
17:40:35Separation_Logic_Imperative_HOL: theory HOL-Word.Bit_Representation
17:40:35Separation_Logic_Imperative_HOL: theory HOL-Word.Bits_Int
17:40:36Featherweight_OCL: theory Featherweight_OCL.UML_Library
17:40:37Separation_Logic_Imperative_HOL: theory HOL-Word.Bool_List_Representation
17:40:38Separation_Logic_Imperative_HOL: theory Native_Word.More_Bits_Int
17:40:40Separation_Logic_Imperative_HOL: theory Native_Word.Bits_Integer
17:40:41Separation_Logic_Imperative_HOL: theory HOL-Word.Word_Miscellaneous
17:40:41Separation_Logic_Imperative_HOL: theory HOL-Word.Misc_Typedef
17:40:41Separation_Logic_Imperative_HOL: theory HOL-Word.Word
17:40:41Timing Separation_Algebra (2 threads, 16.866s elapsed time, 32.124s cpu time, 1.856s GC time, factor 1.90)
17:40:41Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra
17:40:41Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra/document.pdf
17:40:41Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Algebra/outline.pdf
17:40:41Finished Separation_Algebra (0:00:22 elapsed time, 0:00:40 cpu time, factor 1.85)
17:40:41Running Shivers-CFA ...
17:40:42Shivers-CFA: theory HOL-Library.Adhoc_Overloading
17:40:42Shivers-CFA: theory Shivers-CFA.FixTransform
17:40:42Shivers-CFA: theory Shivers-CFA.HOLCFUtils
17:40:43Shivers-CFA: theory Shivers-CFA.CPSScheme
17:40:43Shivers-CFA: theory Shivers-CFA.Computability
17:40:43Shivers-CFA: theory Shivers-CFA.SetMap
17:40:43Shivers-CFA: theory Shivers-CFA.Utils
17:40:43Shivers-CFA: theory Shivers-CFA.MapSets
17:40:45Timing Game_Based_Crypto (2 threads, 40.566s elapsed time, 78.496s cpu time, 2.480s GC time, factor 1.94)
17:40:45Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Game_Based_Crypto
17:40:45Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Game_Based_Crypto/document.pdf
17:40:45Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Game_Based_Crypto/outline.pdf
17:40:45Finished Game_Based_Crypto (0:00:47 elapsed time, 0:01:29 cpu time, factor 1.88)
17:40:45Running Statecharts ...
17:40:46Statecharts: theory Statecharts.Contrib
17:40:46Statecharts: theory Statecharts.Kripke
17:40:46Statecharts: theory Statecharts.DataSpace
17:40:46Statecharts: theory Statecharts.Data
17:40:47Statecharts: theory Statecharts.Update
17:40:47Separation_Logic_Imperative_HOL: theory Native_Word.Word_Misc
17:40:47Statecharts: theory Statecharts.Expr
17:40:48Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap
17:40:49Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
17:40:51Statecharts: theory Statecharts.SA
17:40:52Statecharts: theory Statecharts.HA
17:40:52Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Array
17:40:52Shivers-CFA: theory Shivers-CFA.CPSUtils
17:40:53Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Ref
17:40:53Separation_Logic_Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
17:40:53Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
17:40:53Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Syntax_Match
17:40:53Statecharts: theory Statecharts.HAOps
17:40:53Statecharts: theory Statecharts.HASem
17:40:54Separation_Logic_Imperative_HOL: theory Native_Word.Code_Target_Bits_Int
17:40:54Separation_Logic_Imperative_HOL: theory Native_Word.Uint32
17:40:55Separation_Logic_Imperative_HOL: theory Collections.Code_Target_ICF
17:40:55Shivers-CFA: theory Shivers-CFA.Eval
17:40:55Statecharts: theory Statecharts.HAKripke
17:40:55Statecharts: theory Statecharts.CarAudioSystem
17:40:56Shivers-CFA: theory Shivers-CFA.AbsCF
17:40:57Shivers-CFA: theory Shivers-CFA.ExCF
17:40:58Separation_Logic_Imperative_HOL: theory Collections.HashCode
17:40:59Shivers-CFA: theory Shivers-CFA.ExCFSV
17:41:00Shivers-CFA: theory Shivers-CFA.AbsCFCorrect
17:41:00Shivers-CFA: theory Shivers-CFA.AbsCFComp
17:41:06Timing Locally-Nameless-Sigma (2 threads, 41.795s elapsed time, 69.512s cpu time, 2.444s GC time, factor 1.66)
17:41:06Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Locally-Nameless-Sigma
17:41:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Locally-Nameless-Sigma/document.pdf
17:41:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Locally-Nameless-Sigma/outline.pdf
17:41:06Finished Locally-Nameless-Sigma (0:00:48 elapsed time, 0:01:19 cpu time, factor 1.65)
17:41:06Running SumSquares ...
17:41:07Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SIFUM_Type_Systems
17:41:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SIFUM_Type_Systems/document.pdf
17:41:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SIFUM_Type_Systems/outline.pdf
17:41:07SIFUM_Type_Systems FAILED
17:41:07(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/SIFUM_Type_Systems)
17:41:07### ("\<^const>HOL.Trueprop"
17:41:07### ("\<^const>HOL.conj"
17:41:07### ("\<^const>local.eval_abv2"
17:41:07### ("\<^const>local.conf_abv" ("_position" c\<^sub>1) ("_position" mds)
17:41:07### ("_position" mem\<^sub>1))
17:41:07### ("\<^const>local.conf_abv" ("_position" c\<^sub>1'')
17:41:07### ("_position" mds') ("_position" mem\<^sub>1')))
17:41:07### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1')
17:41:07### ("_indexdefault")
17:41:07### ("\<^const>Language.Stmt.Seq" ("_position" c\<^sub>1'')
17:41:07### ("_position" c\<^sub>2)))))
17:41:07### Fortunately, only one parse tree is well-formed and type-correct,
17:41:07### but you may still want to disambiguate your grammar or your input.
17:41:07### Ambiguous input (line 1072 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
17:41:07### ("\<^const>HOL.Trueprop"
17:41:07### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
17:41:07### ("\<^const>HOL.Trueprop"
17:41:07### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
17:41:07### ("_indexdefault") ("_position" Stop)))
17:41:07### Fortunately, only one parse tree is well-formed and type-correct,
17:41:07### but you may still want to disambiguate your grammar or your input.
17:41:07### Ambiguous input (line 1074 of "~~/afp/thys/SIFUM_Type_Systems/TypeSystem.thy") produces 2 parse trees:
17:41:07### ("\<^const>HOL.Trueprop"
17:41:07### ("\<^const>HOL.eq" ("_position" c\<^sub>1) ("_position" Stop)))
17:41:07### ("\<^const>HOL.Trueprop"
17:41:07### ("\<^const>local.tyenv_eq_indexed" ("_position" c\<^sub>1)
17:41:07### ("_indexdefault") ("_position" Stop)))
17:41:07### Fortunately, only one parse tree is well-formed and type-correct,
17:41:07### but you may still want to disambiguate your grammar or your input.
17:41:07isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SIFUM_Type_Systems/outline -o pdf -n outline -t /proof,/ML
17:41:07isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SIFUM_Type_Systems/document -o pdf -n document
17:41:07*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
17:41:07***
17:41:07*** Type error in application: incompatible operand type
17:41:07***
17:41:07*** Operator: subst_abv mem ::
17:41:07*** ('Var \<Rightarrow> 'Val option) \<Rightarrow> 'Var \<Rightarrow> 'Val
17:41:07*** Operand: {} :: ??'a set
17:41:07***
17:41:07*** At command "have" (line 288 of "~~/afp/thys/SIFUM_Type_Systems/Compositionality.thy")
17:41:07Running UpDown_Scheme ...
17:41:08SumSquares: theory SumSquares.TwoSquares
17:41:08SumSquares: theory SumSquares.FourSquares
17:41:08UpDown_Scheme: theory HOL-Eisbach.Eisbach
17:41:08UpDown_Scheme: theory HOL-ex.Quicksort
17:41:09UpDown_Scheme: theory HOL-Library.Option_ord
17:41:09UpDown_Scheme: theory HOL-Imperative_HOL.Heap
17:41:09UpDown_Scheme: theory Automatic_Refinement.Misc
17:41:11UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad
17:41:13Timing LightweightJava (2 threads, 51.365s elapsed time, 77.136s cpu time, 2.840s GC time, factor 1.50)
17:41:13Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava
17:41:13Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava/document.pdf
17:41:13Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LightweightJava/outline.pdf
17:41:13Finished LightweightJava (0:00:56 elapsed time, 0:01:24 cpu time, factor 1.50)
17:41:13Running FinFun ...
17:41:13UpDown_Scheme: theory HOL-Imperative_HOL.Array
17:41:14UpDown_Scheme: theory HOL-Imperative_HOL.Ref
17:41:14FinFun: theory HOL-Library.Phantom_Type
17:41:14UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL
17:41:14UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
17:41:14UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run
17:41:15UpDown_Scheme: theory UpDown_Scheme.Grid_Point
17:41:15FinFun: theory HOL-Library.Cardinality
17:41:16UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match
17:41:16FinFun: theory FinFun.FinFun
17:41:16UpDown_Scheme: theory UpDown_Scheme.Grid
17:41:16UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions
17:41:17Timing Shivers-CFA (2 threads, 29.153s elapsed time, 56.156s cpu time, 2.768s GC time, factor 1.93)
17:41:17Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA
17:41:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document.pdf
17:41:17Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/outline.pdf
17:41:17Finished Shivers-CFA (0:00:34 elapsed time, 0:01:05 cpu time, factor 1.89)
17:41:17Minimal_SSA CANCELLED
17:41:17Running First_Welfare_Theorem ...
17:41:17UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
17:41:18First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
17:41:18First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
17:41:18First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
17:41:18First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
17:41:18UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
17:41:19UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple
17:41:19Featherweight_OCL: theory Featherweight_OCL.UML_State
17:41:19UpDown_Scheme: theory UpDown_Scheme.Down
17:41:19UpDown_Scheme: theory UpDown_Scheme.Up
17:41:19FinFun: theory FinFun.FinFunPred
17:41:19First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
17:41:20UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation
17:41:20First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
17:41:20UpDown_Scheme: theory UpDown_Scheme.Up_Down
17:41:20Timing SumSquares (2 threads, 8.172s elapsed time, 14.488s cpu time, 0.316s GC time, factor 1.77)
17:41:20Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares
17:41:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares/document.pdf
17:41:20Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/SumSquares/outline.pdf
17:41:20Finished SumSquares (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.66)
17:41:20Running Rank_Nullity_Theorem ...
17:41:21First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
17:41:21UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main
17:41:21UpDown_Scheme: theory UpDown_Scheme.Imperative
17:41:21Featherweight_OCL: theory Featherweight_OCL.UML_Contracts
17:41:22Rank_Nullity_Theorem: theory HOL-Library.Bit
17:41:22Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
17:41:22Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
17:41:22Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
17:41:22Featherweight_OCL: theory Featherweight_OCL.UML_Tools
17:41:23Featherweight_OCL: theory Featherweight_OCL.UML_Main
17:41:23Featherweight_OCL: theory Featherweight_OCL.Analysis_UML
17:41:24Timing FinFun (2 threads, 6.368s elapsed time, 11.472s cpu time, 0.540s GC time, factor 1.80)
17:41:24Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FinFun
17:41:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FinFun/document.pdf
17:41:24Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/FinFun/outline.pdf
17:41:24Finished FinFun (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.75)
17:41:24Running Comparison_Sort_Lower_Bound ...
17:41:25Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
17:41:26Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations
17:41:26Comparison_Sort_Lower_Bound: theory List-Index.List_Index
17:41:26Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
17:41:27Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
17:41:27Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
17:41:28Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
17:41:30Timing First_Welfare_Theorem (2 threads, 7.941s elapsed time, 14.992s cpu time, 0.392s GC time, factor 1.89)
17:41:30Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/First_Welfare_Theorem
17:41:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/First_Welfare_Theorem/document.pdf
17:41:30Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/First_Welfare_Theorem/outline.pdf
17:41:30Finished First_Welfare_Theorem (0:00:13 elapsed time, 0:00:23 cpu time, factor 1.79)
17:41:30Running Lower_Semicontinuous ...
17:41:32Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
17:41:32Separation_Logic_Imperative_HOL: theory Collections.Partial_Equivalence_Relation
17:41:32Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Run
17:41:32Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Assertions
17:41:33Featherweight_OCL: theory Featherweight_OCL.Design_UML
17:41:34Timing Rank_Nullity_Theorem (2 threads, 8.015s elapsed time, 13.136s cpu time, 0.508s GC time, factor 1.64)
17:41:34Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rank_Nullity_Theorem
17:41:34Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rank_Nullity_Theorem/document.pdf
17:41:34Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf
17:41:34Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.64)
17:41:34Running Random_BSTs ...
17:41:34Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hoare_Triple
17:41:35Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Automation
17:41:35Featherweight_OCL: theory Featherweight_OCL.Analysis_OCL
17:41:35Random_BSTs: theory HOL-Data_Structures.Less_False
17:41:35Random_BSTs: theory HOL-Data_Structures.Cmp
17:41:36Random_BSTs: theory HOL-Data_Structures.Sorted_Less
17:41:36Random_BSTs: theory HOL-Data_Structures.List_Ins_Del
17:41:36Random_BSTs: theory HOL-Data_Structures.Set_Specs
17:41:36Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Main
17:41:36Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Table
17:41:36Random_BSTs: theory HOL-Data_Structures.Tree_Set
17:41:37Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
17:41:37Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
17:41:37Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
17:41:37Random_BSTs: theory Random_BSTs.Random_BSTs
17:41:37Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.List_Seg
17:41:38Timing Comparison_Sort_Lower_Bound (2 threads, 8.200s elapsed time, 15.444s cpu time, 0.624s GC time, factor 1.88)
17:41:38Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound
17:41:38Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf
17:41:38Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf
17:41:38Finished Comparison_Sort_Lower_Bound (0:00:13 elapsed time, 0:00:23 cpu time, factor 1.76)
17:41:38Running Buffons_Needle ...
17:41:39Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Circ_List
17:41:39Buffons_Needle: theory Buffons_Needle.Buffons_Needle
17:41:40Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map
17:41:41Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
17:41:43Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Open_List
17:41:43Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Union_Find
17:41:43Timing Lower_Semicontinuous (2 threads, 7.401s elapsed time, 12.252s cpu time, 0.272s GC time, factor 1.66)
17:41:43Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lower_Semicontinuous
17:41:43Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lower_Semicontinuous/document.pdf
17:41:43Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lower_Semicontinuous/outline.pdf
17:41:43Finished Lower_Semicontinuous (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.60)
17:41:43Running Secondary_Sylow ...
17:41:45Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
17:41:46Secondary_Sylow: theory Secondary_Sylow.GroupAction
17:41:46Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation
17:41:46Timing Random_BSTs (2 threads, 7.229s elapsed time, 11.284s cpu time, 0.652s GC time, factor 1.56)
17:41:46Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs
17:41:46Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/document.pdf
17:41:46Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/outline.pdf
17:41:46Finished Random_BSTs (0:00:12 elapsed time, 0:00:19 cpu time, factor 1.55)
17:41:46Running Chord_Segments ...
17:41:47Secondary_Sylow: theory Secondary_Sylow.SndSylow
17:41:48Chord_Segments: theory Triangle.Angles
17:41:48Chord_Segments: theory Triangle.Triangle
17:41:49Chord_Segments: theory Chord_Segments.Chord_Segments
17:41:50Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Idioms
17:41:51Timing Buffons_Needle (2 threads, 7.387s elapsed time, 10.552s cpu time, 0.108s GC time, factor 1.43)
17:41:51Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buffons_Needle
17:41:51Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buffons_Needle/document.pdf
17:41:51Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Buffons_Needle/outline.pdf
17:41:51Finished Buffons_Needle (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.45)
17:41:51Running Source_Coding_Theorem ...
17:41:51Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.To_List_GA
17:41:53Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
17:41:56Timing Secondary_Sylow (2 threads, 5.996s elapsed time, 9.236s cpu time, 0.360s GC time, factor 1.54)
17:41:56Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow
17:41:56Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/document.pdf
17:41:56Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Secondary_Sylow/outline.pdf
17:41:56Finished Secondary_Sylow (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.44)
17:41:56Running Stewart_Apollonius ...
17:41:57Stewart_Apollonius: theory Triangle.Angles
17:41:58Stewart_Apollonius: theory Triangle.Triangle
17:41:58Timing Chord_Segments (2 threads, 6.343s elapsed time, 7.760s cpu time, 0.156s GC time, factor 1.22)
17:41:58Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Chord_Segments
17:41:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Chord_Segments/document.pdf
17:41:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Chord_Segments/outline.pdf
17:41:58Finished Chord_Segments (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.40)
17:41:58Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
17:41:58Timing Statecharts (2 threads, 66.390s elapsed time, 115.952s cpu time, 2.904s GC time, factor 1.75)
17:41:58Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Statecharts
17:41:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Statecharts/document.pdf
17:41:58Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Statecharts/outline.pdf
17:41:58Finished Statecharts (0:01:12 elapsed time, 0:02:05 cpu time, factor 1.73)
17:41:58Running Triangle ...
17:41:58Transitive-Closure CANCELLED
17:41:58Running Fisher_Yates ...
17:41:59Triangle: theory Triangle.Angles
17:42:00Fisher_Yates: theory Fisher_Yates.Fisher_Yates
17:42:00Triangle: theory Triangle.Triangle
17:42:01Featherweight_OCL: theory Featherweight_OCL.Design_OCL
17:42:02Timing Source_Coding_Theorem (2 threads, 5.627s elapsed time, 8.816s cpu time, 0.180s GC time, factor 1.57)
17:42:02Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem
17:42:02Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem/document.pdf
17:42:02Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Source_Coding_Theorem/outline.pdf
17:42:02Finished Source_Coding_Theorem (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.55)
17:42:02Running Ptolemys_Theorem ...
17:42:03Timing UpDown_Scheme (2 threads, 50.346s elapsed time, 95.336s cpu time, 3.488s GC time, factor 1.89)
17:42:03Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme
17:42:03Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme/document.pdf
17:42:03Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/UpDown_Scheme/outline.pdf
17:42:03Finished UpDown_Scheme (0:00:56 elapsed time, 0:01:44 cpu time, factor 1.85)
17:42:03Running Surprise_Paradox ...
17:42:03Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
17:42:05Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
17:42:05Timing Stewart_Apollonius (2 threads, 4.431s elapsed time, 6.084s cpu time, 0.092s GC time, factor 1.37)
17:42:05Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stewart_Apollonius
17:42:05Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stewart_Apollonius/document.pdf
17:42:05Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Stewart_Apollonius/outline.pdf
17:42:05Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.54)
17:42:05Running Minkowskis_Theorem ...
17:42:06Timing Fisher_Yates (2 threads, 2.829s elapsed time, 5.360s cpu time, 0.144s GC time, factor 1.89)
17:42:06Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates
17:42:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates/document.pdf
17:42:06Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Fisher_Yates/outline.pdf
17:42:06Finished Fisher_Yates (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.65)
17:42:06Running Cartan_FP ...
17:42:06Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
17:42:07Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Blit
17:42:07Timing Triangle (2 threads, 4.247s elapsed time, 5.664s cpu time, 0.120s GC time, factor 1.33)
17:42:07Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Triangle
17:42:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Triangle/document.pdf
17:42:07Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Triangle/outline.pdf
17:42:07Finished Triangle (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.50)
17:42:07Running Perfect-Number-Thm ...
17:42:08Cartan_FP: theory Cartan_FP.Cartan
17:42:09Timing Ptolemys_Theorem (2 threads, 2.577s elapsed time, 4.096s cpu time, 0.104s GC time, factor 1.59)
17:42:09Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ptolemys_Theorem
17:42:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ptolemys_Theorem/document.pdf
17:42:09Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Ptolemys_Theorem/outline.pdf
17:42:09Finished Ptolemys_Theorem (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.65)
17:42:09Running Lehmer ...
17:42:09Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics
17:42:09Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma
17:42:10Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect
17:42:10Timing Surprise_Paradox (2 threads, 2.252s elapsed time, 3.164s cpu time, 0.000s GC time, factor 1.41)
17:42:10Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Surprise_Paradox
17:42:10Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Surprise_Paradox/document.pdf
17:42:10Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Surprise_Paradox/outline.pdf
17:42:10Finished Surprise_Paradox (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.48)
17:42:10Running Monad_Normalisation ...
17:42:11Lehmer: theory Lehmer.Lehmer
17:42:12Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
17:42:12Timing Minkowskis_Theorem (2 threads, 1.915s elapsed time, 3.420s cpu time, 0.072s GC time, factor 1.79)
17:42:12Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Minkowskis_Theorem
17:42:12Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Minkowskis_Theorem/document.pdf
17:42:12Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Minkowskis_Theorem/outline.pdf
17:42:12Finished Minkowskis_Theorem (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.67)
17:42:12Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
17:42:13Timing Cartan_FP (2 threads, 2.016s elapsed time, 3.640s cpu time, 0.084s GC time, factor 1.81)
17:42:13Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cartan_FP
17:42:13Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cartan_FP/document.pdf
17:42:13Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cartan_FP/outline.pdf
17:42:13Finished Cartan_FP (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.68)
17:42:14Timing Perfect-Number-Thm (2 threads, 1.728s elapsed time, 3.240s cpu time, 0.000s GC time, factor 1.88)
17:42:14Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm
17:42:14Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/document.pdf
17:42:14Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Perfect-Number-Thm/outline.pdf
17:42:14Finished Perfect-Number-Thm (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.60)
17:42:16Timing Lehmer (2 threads, 1.280s elapsed time, 2.276s cpu time, 0.000s GC time, factor 1.78)
17:42:16Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer
17:42:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer/document.pdf
17:42:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lehmer/outline.pdf
17:42:16Finished Lehmer (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.55)
17:42:16Timing Monad_Normalisation (2 threads, 0.851s elapsed time, 1.220s cpu time, 0.000s GC time, factor 1.43)
17:42:16Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monad_Normalisation
17:42:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monad_Normalisation/document.pdf
17:42:16Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Monad_Normalisation/outline.pdf
17:42:16Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.57)
17:42:21Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
17:42:21Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
17:42:21Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.From_List_GA
17:42:22Separation_Logic_Imperative_HOL: theory Separation_Logic_Imperative_HOL.Sep_Examples
17:42:29Timing Separation_Logic_Imperative_HOL (2 threads, 110.206s elapsed time, 149.996s cpu time, 10.368s GC time, factor 1.36)
17:42:29Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL
17:42:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL/document.pdf
17:42:29Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Separation_Logic_Imperative_HOL/outline.pdf
17:42:29Finished Separation_Logic_Imperative_HOL (0:01:56 elapsed time, 0:04:42 cpu time, factor 2.43)
17:43:08Timing Featherweight_OCL (2 threads, 152.108s elapsed time, 284.072s cpu time, 15.396s GC time, factor 1.87)
17:43:08Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL
17:43:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/annex-a.pdf
17:43:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/document.pdf
17:43:08Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/outline.pdf
17:43:08Finished Featherweight_OCL (0:03:17 elapsed time, 0:06:11 cpu time, factor 1.88)
17:43:44HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
17:45:06HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
17:45:58HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
17:52:38Timing HOL-ODE-Numerics (2 threads, 1937.513s elapsed time, 3659.244s cpu time, 638.028s GC time, factor 1.89)
17:52:38Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOL-ODE-Numerics
17:52:38Finished HOL-ODE-Numerics (0:33:53 elapsed time, 1:04:42 cpu time, factor 1.91)
17:52:38Building Lorenz_Approximation ...
17:52:38Running HOL-ODE-Examples ...
17:52:40Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
17:52:40HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
17:52:40HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
17:52:41HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
17:52:44Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
17:53:00Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
17:54:01HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
17:57:33Timing Lorenz_Approximation (2 threads, 254.354s elapsed time, 453.984s cpu time, 41.980s GC time, factor 1.78)
17:57:33Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lorenz_Approximation
17:57:33Finished Lorenz_Approximation (0:04:54 elapsed time, 0:08:29 cpu time, factor 1.73)
17:57:33Running Lorenz_C1 ...
17:57:36Lorenz_C1: theory Lorenz_C1.Lorenz_C1
17:57:38Timing Lorenz_C1 (2 threads, 0.760s elapsed time, 1.344s cpu time, 0.000s GC time, factor 1.77)
17:57:38Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Lorenz_C1
17:57:38Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.02)
18:01:57Timing HOL-ODE-Examples (2 threads, 555.991s elapsed time, 1066.792s cpu time, 29.244s GC time, factor 1.92)
18:01:57Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOL-ODE-Examples
18:01:57Finished HOL-ODE-Examples (0:09:19 elapsed time, 0:17:49 cpu time, factor 1.91)
18:01:57Unfinished session(s): Buchi_Complementation, CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker, CAVA_buildchain1, CAVA_buildchain3, Call_Arity, Collections, Collections_Examples, Containers-Benchmarks, DFS_Framework, Dijkstra_Shortest_Path, EdmondsKarp_Maxflow, FeatherweightJava, Flow_Networks, Floyd_Warshall, Formal_SSA, Gabow_SCC, InformationFlowSlicing_Inter, Knuth_Morris_Pratt, LLL_Factorization, LTL_to_GBA, Maxflow_Lib, Minimal_SSA, Partial_Order_Reduction, Promela, Prpu_Maxflow, ROBDD, Refine_Imperative_HOL, SIFUM_Type_Systems, Sepref_Basic, Sepref_IICF, Sepref_Prereq, Transition_Systems_and_Automata, Transitive-Closure, Tree-Automata, UPF_Firewall, VerifyThis2018
18:01:5818:01:58=== TIMING ===
18:01:5818:01:58Group AFP: 5:56:32 elapsed time, 10:28:33 cpu time, factor 1.76
18:01:58Group main: 0:24:39 elapsed time, 0:41:25 cpu time, factor 1.68
18:01:58Group timing: 0:24:39 elapsed time, 0:41:25 cpu time, factor 1.68
18:01:58Overall: 1:05:31 elapsed time, 11:09:58 cpu time, factor 10.22
18:01:5818:01:58=== FAILED SESSIONS ===
18:01:5818:01:58Session CAVA_buildchain3: CANCELLED
18:01:58Session Containers-Benchmarks: FAILED 2
18:01:58Session EdmondsKarp_Maxflow: CANCELLED
18:01:58Session Maxflow_Lib: CANCELLED
18:01:58Session Promela: CANCELLED
18:01:58Session Formal_SSA: CANCELLED
18:01:58Session Sepref_IICF: CANCELLED
18:01:58Session DFS_Framework: CANCELLED
18:01:58Session FeatherweightJava: FAILED 2
18:01:58Session LLL_Factorization: FAILED 2
18:01:58Session Dijkstra_Shortest_Path: CANCELLED
18:01:58Session Partial_Order_Reduction: CANCELLED
18:01:58Session Floyd_Warshall: CANCELLED
18:01:58Session Collections: FAILED 2
18:01:58Session InformationFlowSlicing_Inter: FAILED 2
18:01:58Session Call_Arity: FAILED 2
18:01:58Session Prpu_Maxflow: CANCELLED
18:01:58Session Sepref_Basic: CANCELLED
18:01:58Session Minimal_SSA: CANCELLED
18:01:58Session Gabow_SCC: CANCELLED
18:01:58Session SIFUM_Type_Systems: FAILED 2
18:01:58Session VerifyThis2018: CANCELLED
18:01:58Session LTL_to_GBA: CANCELLED
18:01:58Session Buchi_Complementation: CANCELLED
18:01:58Session CAVA_Base: CANCELLED
18:01:58Session Tree-Automata: CANCELLED
18:01:58Session Collections_Examples: CANCELLED
18:01:58Session Transition_Systems_and_Automata: CANCELLED
18:01:58Session Knuth_Morris_Pratt: CANCELLED
18:01:58Session Transitive-Closure: CANCELLED
18:01:58Session CAVA_LTL_Modelchecker: CANCELLED
18:01:58Session Sepref_Prereq: CANCELLED
18:01:58Session Refine_Imperative_HOL: CANCELLED
18:01:58Session Flow_Networks: CANCELLED
18:01:58Session UPF_Firewall: FAILED 2
18:01:58Session CAVA_Automata: CANCELLED
18:01:58Session ROBDD: CANCELLED
18:01:58Session CAVA_buildchain1: CANCELLED
18:01:5818:01:58=== DEPENDENCIES ===
18:01:5818:01:58Generating dependencies file ...
18:02:04Writing dependencies file ...
18:02:0418:02:04=== SITEGEN ===
18:02:0418:02:04Writing status file ...
18:02:04Running sitegen ...
18:02:05Success: Generated topics.html
18:02:05Success: Generated index.html
18:02:06Success: Generated html files for 423 entries
18:02:06Success: Generated statistics.html
18:02:06Success: Generated download.html
18:02:06Success: Generated about.html
18:02:06Success: Generated citing.html
18:02:06Success: Generated updating.html
18:02:06Success: Generated search.html
18:02:06Success: Generated submitting.html
18:02:06Success: Generated using.html
18:02:06Success: Generated rss.xml
18:02:06Success: Generated status.html
18:02:06Packing tars ...
18:02:1318:02:13=== NOTIFICATIONS ===
18:02:1318:02:14Entry InformationFlowSlicing_Inter: WARNING no maintainers specified
18:02:14Entry Call_Arity: WARNING no maintainers specified
18:02:1418:02:14=== COMPLETED ===
18:02:1418:02:14Build step 'Execute shell' marked build as failure
18:02:14Archiving artifacts
18:03:22Started calculate disk usage of build
18:03:22Finished Calculation of disk usage of build in 0 seconds
18:03:53Started calculate disk usage of workspace
18:03:54Finished Calculation of disk usage of workspace in 0 seconds
18:03:54No emails were triggered.
18:03:54Finished: FAILURE
![[Jenkins]](/jenkins/static/0ab21b84/images/svgs/logo.svg){kind=logo}
