Console Output

Started by timer
Running in Durability level: MAX_SURVIVABILITY
[Pipeline] Start of Pipeline
[Pipeline] node
Running on workerlrz6 in /media/data/jenkins/workspace/isabelle-dump
[Pipeline] {
[Pipeline] timeout
Timeout set to expire in 1 day 6 hr
[Pipeline] {
[Pipeline] stage
[Pipeline] { (Prepare)
[Pipeline] cleanWs
[WS-CLEANUP] Deleting project workspace...
[WS-CLEANUP] Deferred wipeout is used...
[WS-CLEANUP] done
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Checkout)
[Pipeline] script
[Pipeline] {
[Pipeline] httpRequest
HttpMethod: GET
URL: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Sending request to url: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Response Code: HTTP/1.1 200 OK
Success code from java.util.stream.IntPipeline$Head@6952adc5
[Pipeline] }
[Pipeline] // script
[Pipeline] checkout
$ hg clone --rev 304f22435bc7e7f710dcbfb36243a87ea57a04f5 --noupdate https://isabelle.in.tum.de/repos/isabelle /media/data/jenkins/workspace/isabelle-dump
adding changesets
adding manifests
adding file changes
added 74163 changesets with 202901 changes to 11442 files
new changesets a5a9c433f639:304f22435bc7
[isabelle-dump] $ hg update --rev 304f22435bc7e7f710dcbfb36243a87ea57a04f5
3457 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-dump] $ hg log --rev . --template {node}
[isabelle-dump] $ hg log --rev . --template {rev}
[isabelle-dump] $ hg id --branch
[isabelle-dump] $ hg log --rev d030b988d470061e400b8e4ed78ea337281e7001 --template exists\n
exists
[isabelle-dump] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('304f22435bc7e7f710dcbfb36243a87ea57a04f5') and not ancestors(d030b988d470061e400b8e4ed78ea337281e7001)" --encoding UTF-8 --encodingmode replace
[isabelle-dump] $ hg log --rev . --template {node}
[isabelle-dump] $ hg log --rev . --template {rev}
[isabelle-dump] $ hg id --branch
[Pipeline] checkout
$ hg clone --rev dd34e0937e25100492e64393993bc4fcc72667fc --noupdate https://foss.heptapod.net/isa-afp/afp-devel /media/data/jenkins/workspace/isabelle-dump/afp
adding changesets
adding manifests
adding file changes
added 11982 changesets with 80916 changes to 12500 files
new changesets 86acbdb19eec:dd34e0937e25
[afp] $ hg update --rev dd34e0937e25100492e64393993bc4fcc72667fc
10047 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[afp] $ hg log --rev 34754976c5bf15e62139cb21ec528a78a0ca0119 --template exists\n
exists
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('dd34e0937e25100492e64393993bc4fcc72667fc') and not ancestors(34754976c5bf15e62139cb21ec528a78a0ca0119)" --encoding UTF-8 --encodingmode replace
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Install)
[Pipeline] sh
+ bin/isabelle components -a
[Pipeline] sh
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle_admin.jar) ...
[Pipeline] sh
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
[Pipeline] sh
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.4
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Dump)
[Pipeline] sh
+ bin/isabelle dump -o threads=4 -D afp/thys -b Pure -X slow -X large -X very_slow -O dump -a
Loading 757 sessions ...
Build started for Isabelle/Pure ...
Building Pure ...
Finished Pure (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.97)
### Skipping theory HOL-Import.HOL_Light_Import  (undefined HOL_LIGHT_BUNDLE)
### Skipping theory HOL-Codegenerator_Test.Code_Test_MLton  (undefined ISABELLE_MLTON)
### Skipping theory HOL-Codegenerator_Test.Code_Test_SMLNJ  (undefined ISABELLE_SMLNJ)
### Skipping theory HOL-Library.Code_Prolog  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Hotel_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Lambda_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.List_Examples  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Reg_Exp_Example  (undefined ISABELLE_SWIPL)
### Skipping theory PAC_Checker.PAC_Checker_MLton  (undefined ISABELLE_MLTON)
### Skipping theory Buchi_Complementation.Complementation_Build  (undefined ISABELLE_MLTON)
### Skipping theory CakeML.Compiler_Test  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
### Skipping theory CakeML_Codegen.Test_Datatypes  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
### Skipping theory Native_Word.Native_Word_Test_MLton  (undefined ISABELLE_MLTON)
### Skipping theory Native_Word.Native_Word_Test_MLton2  (undefined ISABELLE_MLTON)
### Skipping theory Native_Word.Native_Word_Test_SMLNJ  (undefined ISABELLE_SMLNJ)
### Skipping theory Native_Word.Native_Word_Test_SMLNJ2  (undefined ISABELLE_SMLNJ)
Starting session Pure ...
Loading 133 theories ...
Processing theory Tools.Code_Generator ...
Processing theory HOL.HOL ...
Processing theory HOL.Argo ...
Processing theory HOL.SAT ...
Processing theory HOL.Ctr_Sugar ...
Processing theory HOL.Orderings ...
Processing theory HOL.Groups ...
Processing theory HOL.Lattices ...
Processing theory HOL.Boolean_Algebras ...
Processing theory HOL.Set ...
Processing theory HOL.Fun ...
Processing theory HOL.Typedef ...
Processing theory HOL.Complete_Lattices ...
Processing theory HOL.Inductive ...
Processing theory HOL.Product_Type ...
Processing theory HOL.Complete_Partial_Order ...
Processing theory HOL.Sum_Type ...
Processing theory HOL.Rings ...
Processing theory HOL.Nat ...
Processing theory HOL.Meson ...
Processing theory HOL.ATP ...
Processing theory HOL.Metis ...
Processing theory HOL.Fields ...
Processing theory HOL.Finite_Set ...
Processing theory HOL.Relation ...
Processing theory HOL.Transitive_Closure ...
Processing theory HOL.Wellfounded ...
Processing theory HOL.Fun_Def_Base ...
Processing theory HOL.Hilbert_Choice ...
Processing theory HOL.Wfrec ...
Processing theory HOL.Order_Relation ...
Processing theory HOL.BNF_Wellorder_Relation ...
Processing theory HOL.BNF_Wellorder_Embedding ...
Processing theory HOL.BNF_Wellorder_Constructions ...
Processing theory HOL.Zorn ...
Processing theory HOL.BNF_Cardinal_Order_Relation ...
Processing theory HOL.BNF_Cardinal_Arithmetic ...
Processing theory HOL.BNF_Def ...
Processing theory HOL.BNF_Composition ...
Processing theory HOL.Basic_BNFs ...
Processing theory HOL.BNF_Fixpoint_Base ...
Processing theory HOL.BNF_Least_Fixpoint ...
Processing theory HOL.Basic_BNF_LFPs ...
Processing theory HOL.Transfer ...
Processing theory HOL.Num ...
Processing theory HOL.Power ...
Processing theory HOL.Groups_Big ...
Processing theory HOL.Equiv_Relations ...
Processing theory HOL.Lifting ...
Processing theory HOL.Lifting_Set ...
Processing theory HOL.Quotient ...
Processing theory HOL.Option ...
Processing theory HOL.Extraction ...
Processing theory HOL.Lattices_Big ...
Processing theory HOL.Partial_Function ...
Processing theory HOL.Fun_Def ...
Processing theory HOL.Int ...
Processing theory HOL.Euclidean_Division ...
Processing theory HOL.Parity ...
Processing theory HOL.Divides ...
Processing theory HOL.Numeral_Simprocs ...
Processing theory HOL.SMT ...
Processing theory HOL.Semiring_Normalization ...
Processing theory HOL.Groebner_Basis ...
Processing theory HOL.Set_Interval ...
Processing theory HOL.Presburger ...
Processing theory HOL.Conditionally_Complete_Lattices ...
Processing theory HOL.Sledgehammer ...
Processing theory HOL.Filter ...
Processing theory HOL.List ...
Processing theory HOL.Groups_List ...
Processing theory HOL.Factorial ...
Processing theory HOL.Map ...
Processing theory HOL.Binomial ...
Processing theory HOL.Enum ...
Processing theory HOL.Bit_Operations ...
Processing theory HOL.Code_Numeral ...
Processing theory HOL.Random ...
Processing theory HOL.String ...
Processing theory HOL.Predicate ...
Processing theory HOL.Lazy_Sequence ...
Processing theory HOL.Limited_Sequence ...
Processing theory HOL.Typerep ...
Processing theory HOL.Code_Evaluation ...
Processing theory HOL.BNF_Greatest_Fixpoint ...
Processing theory HOL.Quickcheck_Random ...
Processing theory HOL.Random_Pred ...
Processing theory HOL.Random_Sequence ...
Processing theory HOL.Quickcheck_Narrowing ...
Processing theory HOL.Quickcheck_Exhaustive ...
Processing theory HOL.Record ...
Processing theory HOL.Predicate_Compile ...
Processing theory HOL.Mirabelle ...
Processing theory HOL.GCD ...
Processing theory HOL.Nitpick ...
Processing theory HOL.Nunchaku ...
Processing theory Main ...
Processing theory HOL-Examples.Drinker ...
Processing theory HOL-Proofs-ex.XML_Data ...
Processing theory HOL-Library.Cancellation ...
Processing theory HOL-Library.Code_Abstract_Nat ...
Processing theory HOL-Library.Code_Target_Nat ...
Processing theory HOL-Library.Code_Target_Int ...
Processing theory HOL-Library.Code_Target_Numeral ...
Processing theory HOL-Library.Open_State_Syntax ...
Processing theory HOL-Library.Realizers ...
Processing theory HOL-Proofs-Extraction.Warshall ...
Processing theory HOL-Proofs-Extraction.Higman ...
Processing theory HOL-Proofs-Extraction.Util ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Extraction.Greatest_Common_Divisor ...
Processing theory HOL-Proofs-Lambda.ListOrder ...
Processing theory HOL-Proofs-ex.Hilbert_Classical ...
Processing theory HOL-Proofs-ex.Proof_Terms ...
Processing theory HOL-Proofs-Lambda.Lambda ...
Processing theory HOL-Proofs-Lambda.ListApplication ...
Processing theory HOL-Proofs-Extraction.Higman_Extraction ...
Removing 10 theories ...
Processing theory HOL-Proofs-Lambda.ListBeta ...
Processing theory HOL-Proofs-Lambda.ParRed ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Lambda.InductTermi ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Processing theory HOL-Proofs-Lambda.LambdaType ...
Processing theory HOL-Proofs-Lambda.StrongNorm ...
Processing theory HOL-Library.Multiset ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Processing theory HOL-Computational_Algebra.Factorial_Ring ...
Removing 7 theories ...
Processing theory HOL-Computational_Algebra.Euclidean_Algorithm ...
Processing theory HOL-Computational_Algebra.Primes ...
Processing theory HOL-Proofs-Extraction.Euclid ...
Removing 10 theories ...
Processing theory HOL-Proofs-Lambda.WeakNorm ...
Starting session Pure ...
Loading 252 theories ...
Processing theory HOL-Combinatorics.Transposition ...
Processing theory HOL.Hull ...
Processing theory HOL-Library.Disjoint_Sets ...
Processing theory HOL-Library.FuncSet ...
Processing theory HOL.Archimedean_Field ...
Processing theory HOL-Library.Nat_Bijection ...
Processing theory HOL-Library.Infinite_Set ...
Processing theory HOL.Rat ...
Processing theory HOL.Modules ...
Processing theory HOL-Library.Old_Datatype ...
Processing theory HOL-Library.Countable ...
Processing theory HOL.Real ...
Processing theory HOL-Library.Countable_Set ...
Processing theory HOL-Library.Phantom_Type ...
Processing theory HOL-Library.Cardinality ...
Processing theory HOL.Vector_Spaces ...
Processing theory HOL-Library.Product_Plus ...
Processing theory HOL-Library.Set_Idioms ...
Processing theory HOL-Library.Product_Order ...
Processing theory HOL-Library.Set_Algebras ...
Processing theory HOL-Combinatorics.Permutations ...
Processing theory HOL-Library.Countable_Complete_Lattices ...
Processing theory HOL-Library.Numeral_Type ...
Processing theory HOL.Topological_Spaces ...
Processing theory HOL.Real_Vector_Spaces ...
Processing theory HOL-Analysis.Metric_Arith ...
Processing theory HOL.Inequalities ...
Processing theory HOL.Limits ...
Processing theory HOL.Series ...
Processing theory HOL.Deriv ...
Processing theory HOL.NthRoot ...
Processing theory HOL.Transcendental ...
Processing theory HOL.Complex ...
Processing theory HOL.MacLaurin ...
Processing theory Complex_Main ...
Processing theory HOL-Analysis.Continuum_Not_Denumerable ...
Processing theory HOL-Analysis.L2_Norm ...
Processing theory HOL-Analysis.Operator_Norm ...
Processing theory HOL-Analysis.Poly_Roots ...
Processing theory HOL-Analysis.Inner_Product ...
Processing theory HOL-Analysis.Product_Vector ...
Processing theory HOL-Analysis.Euclidean_Space ...
Processing theory HOL-Analysis.Finite_Cartesian_Product ...
Processing theory HOL-Analysis.Linear_Algebra ...
Processing theory HOL-Analysis.Affine ...
Processing theory HOL-Analysis.Elementary_Topology ...
Processing theory HOL-Analysis.Cartesian_Space ...
Processing theory HOL-Library.Discrete ...
Processing theory HOL-Library.Liminf_Limsup ...
Processing theory HOL-Analysis.Determinants ...
Processing theory HOL-Library.Indicator_Function ...
Processing theory HOL-Library.Nonpos_Ints ...
Processing theory HOL-Library.Order_Continuity ...
Processing theory HOL-Library.Periodic_Fun ...
Processing theory HOL-Analysis.Convex ...
Processing theory HOL-Analysis.Abstract_Topology ...
Processing theory HOL-Library.Landau_Symbols ...
Processing theory HOL-Computational_Algebra.Formal_Power_Series ...
Processing theory HOL-Analysis.Abstract_Limits ...
Processing theory HOL-Library.Sum_of_Squares ...
Processing theory HOL-Analysis.Norm_Arith ...
Processing theory HOL-Library.Extended_Nat ...
Processing theory HOL-Analysis.Abstract_Topology_2 ...
Processing theory HOL-Analysis.Connected ...
Processing theory HOL-Library.Extended_Real ...
Processing theory HOL-Analysis.Function_Topology ...
Processing theory HOL-Library.Extended_Nonnegative_Real ...
Processing theory HOL-Analysis.Elementary_Metric_Spaces ...
Processing theory HOL-Analysis.Product_Topology ...
Processing theory HOL-Analysis.Function_Metric ...
Processing theory HOL-Analysis.Elementary_Normed_Spaces ...
Processing theory HOL-Analysis.Sigma_Algebra ...
Processing theory HOL-Analysis.Measurable ...
Processing theory HOL-Analysis.T1_Spaces ...
Processing theory HOL-Analysis.Topology_Euclidean_Space ...
Processing theory HOL-Analysis.Lindelof_Spaces ...
Processing theory HOL-Analysis.Extended_Real_Limits ...
Processing theory HOL-Analysis.Measure_Space ...
Processing theory HOL-Analysis.Convex_Euclidean_Space ...
Processing theory HOL-Analysis.Caratheodory ...
Processing theory HOL-Analysis.Ordered_Euclidean_Space ...
Processing theory HOL-Analysis.Summation_Tests ...
Processing theory HOL-Analysis.Uniform_Limit ...
Processing theory HOL-Analysis.Bounded_Continuous_Function ...
Processing theory HOL-Analysis.Bounded_Linear_Function ...
Processing theory HOL-Analysis.Line_Segment ...
Processing theory HOL-Analysis.Tagged_Division ...
Processing theory HOL-Analysis.Derivative ...
Processing theory HOL-Analysis.Cartesian_Euclidean_Space ...
Processing theory HOL-Analysis.Complex_Analysis_Basics ...
Processing theory HOL-Analysis.Cross3 ...
Processing theory HOL-Analysis.Lipschitz ...
Processing theory HOL-Analysis.Borel_Space ...
Processing theory HOL-Analysis.Regularity ...
Processing theory HOL-Analysis.Starlike ...
Processing theory HOL-Analysis.Continuous_Extension ...
Processing theory HOL-Analysis.Multivariate_Analysis ...
Processing theory HOL-Analysis.Nonnegative_Lebesgue_Integration ...
Processing theory HOL-Analysis.Complex_Transcendental ...
Processing theory HOL-Analysis.Generalised_Binomial_Theorem ...
Processing theory HOL-Analysis.Harmonic_Numbers ...
Processing theory HOL-Analysis.Binary_Product_Measure ...
Processing theory HOL-Analysis.Embed_Measure ...
Processing theory HOL-Analysis.FPS_Convergence ...
Processing theory HOL-Analysis.Finite_Product_Measure ...
Processing theory HOL-Analysis.Infinite_Products ...
Processing theory HOL-Analysis.Path_Connected ...
Processing theory HOL-Analysis.Locally ...
Processing theory HOL-Analysis.Bochner_Integration ...
Processing theory HOL-Analysis.Radon_Nikodym ...
Processing theory HOL-Analysis.Complete_Measure ...
Processing theory HOL-Analysis.Arcwise_Connected ...
Processing theory HOL-Analysis.Set_Integral ...
Processing theory HOL-Analysis.Infinite_Set_Sum ...
Processing theory HOL-Analysis.Lebesgue_Measure ...
Processing theory HOL-Analysis.Polytope ...
Processing theory HOL-Analysis.Weierstrass_Theorems ...
Processing theory HOL-Analysis.Homotopy ...
Processing theory HOL-Analysis.Abstract_Euclidean_Space ...
Processing theory HOL-Analysis.Homeomorphism ...
Processing theory HOL-Analysis.Brouwer_Fixpoint ...
Processing theory HOL-Analysis.Fashoda_Theorem ...
Processing theory HOL-Analysis.Henstock_Kurzweil_Integration ...
Processing theory HOL-Analysis.Integral_Test ...
Processing theory HOL-Analysis.Retracts ...
Processing theory HOL-Analysis.Smooth_Paths ...
Processing theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration ...
Processing theory HOL-Analysis.Interval_Integral ...
Processing theory HOL-Analysis.Lebesgue_Integral_Substitution ...
Processing theory HOL-Analysis.Gamma_Function ...
Processing theory HOL-Analysis.Ball_Volume ...
Processing theory HOL-Analysis.Vitali_Covering_Theorem ...
Processing theory HOL-Analysis.Improper_Integral ...
Processing theory HOL-Analysis.Equivalence_Measurable_On_Borel ...
Processing theory HOL-Analysis.Further_Topology ...
Processing theory HOL-Analysis.Jordan_Curve ...
Processing theory HOL-Analysis.Change_Of_Vars ...
Processing theory HOL-Analysis.Simplex_Content ...
Processing theory HOL-Analysis.Analysis ...
Processing theory HOL-Complex_Analysis.Contour_Integration ...
Processing theory HOL-Complex_Analysis.Cauchy_Integral_Theorem ...
Processing theory HOL-Complex_Analysis.Winding_Numbers ...
Processing theory HOL-Complex_Analysis.Cauchy_Integral_Formula ...
Processing theory HOL-Complex_Analysis.Conformal_Mappings ...
Processing theory HOL-Complex_Analysis.Complex_Singularities ...
Processing theory HOL-Complex_Analysis.Complex_Residues ...
Processing theory HOL-Complex_Analysis.Residue_Theorem ...
Processing theory HOL-Complex_Analysis.Great_Picard ...
Processing theory HOL-Complex_Analysis.Riemann_Mapping ...
Loading 48 theories ...
Processing theory HOL-Complex_Analysis.Complex_Analysis ...
Processing theory HOL-Library.Adhoc_Overloading ...
Processing theory HOL-Library.Monad_Syntax ...
Processing theory HOL-Library.Conditional_Parametricity ...
Processing theory HOL-Library.Lattice_Syntax ...
Processing theory HOL-Library.Rewrite ...
Processing theory HOL-Library.AList ...
Processing theory HOL-Library.Complete_Partial_Order2 ...
Processing theory HOL-Library.Stream ...
Processing theory HOL-Library.Diagonal_Subsequence ...
Processing theory HOL-Probability.Discrete_Topology ...
Processing theory HOL-Combinatorics.Multiset_Permutations ...
Processing theory HOL-Probability.Essential_Supremum ...
Processing theory HOL-Library.Mapping ...
Processing theory HOL-Library.AList_Mapping ...
Processing theory HOL-Probability.Stopping_Time ...
Processing theory HOL-Library.FSet ...
Processing theory HOL-Library.Sublist ...
Processing theory HOL-Library.Tree ...
Processing theory HOL-Library.Linear_Temporal_Logic_on_Streams ...
Removing 11 theories ...
Processing theory HOL-Probability.Probability_Measure ...
Processing theory HOL-Probability.Distribution_Functions ...
Processing theory HOL-Probability.Tree_Space ...
Processing theory HOL-Library.Finite_Map ...
Processing theory HOL-Probability.Weak_Convergence ...
Processing theory HOL-Probability.Helly_Selection ...
Processing theory HOL-Probability.Fin_Map ...
Processing theory HOL-Probability.Conditional_Expectation ...
Processing theory HOL-Probability.Giry_Monad ...
Processing theory HOL-Probability.Projective_Family ...
Processing theory HOL-Probability.Infinite_Product_Measure ...
Processing theory HOL-Probability.Probability_Mass_Function ...
Processing theory HOL-Probability.PMF_Impl ...
Processing theory HOL-Probability.Random_Permutations ...
Processing theory HOL-Probability.Projective_Limit ...
Processing theory HOL-Probability.Stream_Space ...
Processing theory HOL-Probability.Independent_Family ...
Processing theory HOL-Probability.Convolution ...
Processing theory HOL-Probability.Product_PMF ...
Processing theory HOL-Probability.Hoeffding ...
Processing theory HOL-Probability.SPMF ...
Processing theory HOL-Probability.Information ...
Processing theory HOL-Probability.Distributions ...
Processing theory HOL-Probability.Characteristic_Functions ...
Processing theory HOL-Probability.Sinc_Integral ...
Processing theory HOL-Probability.Levy ...
Processing theory HOL-Probability.Central_Limit_Theorem ...
Processing theory HOL-Probability.Probability ...
Processing theory HOL-Probability-ex.Measure_Not_CCC ...
Removing 25 theories ...
Processing theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure ...
Processing theory HOL-Probability-ex.Dining_Cryptographers ...
Loading 39 theories ...
Processing theory HOL-Cardinals.Fun_More ...
Processing theory HOL-Library.Fun_Lexorder ...
Processing theory HOL-Cardinals.Order_Union ...
Processing theory HOL-Cardinals.Order_Relation_More ...
Processing theory HOL-Cardinals.Wellfounded_More ...
Processing theory HOL-Cardinals.Wellorder_Relation ...
Processing theory HOL-Cardinals.Wellorder_Embedding ...
Processing theory HOL-Library.Equipollence ...
Processing theory HOL-Library.More_List ...
Processing theory HOL-Cardinals.Wellorder_Constructions ...
Processing theory HOL-Library.Groups_Big_Fun ...
Processing theory HOL-Algebra.Congruence ...
Processing theory HOL-Algebra.Order ...
Removing 59 theories ...
Processing theory HOL-Cardinals.Cardinal_Order_Relation ...
Processing theory HOL-Cardinals.Cardinal_Arithmetic ...
Processing theory HOL-Algebra.Lattice ...
Processing theory HOL-Library.Poly_Mapping ...
Processing theory HOL-Algebra.Complete_Lattice ...
Processing theory HOL-Algebra.Group ...
Processing theory HOL-Algebra.FiniteProduct ...
Processing theory HOL-Algebra.Coset ...
Processing theory HOL-Algebra.Generated_Groups ...
Processing theory HOL-Algebra.Solvable_Groups ...
Processing theory HOL-Algebra.Ring ...
Processing theory HOL-Algebra.AbelCoset ...
Processing theory HOL-Algebra.Module ...
Processing theory HOL-Algebra.Ideal ...
Processing theory HOL-Algebra.RingHom ...
Processing theory HOL-Algebra.Elementary_Groups ...
Processing theory HOL-Algebra.Exact_Sequence ...
Processing theory HOL-Algebra.Product_Groups ...
Processing theory HOL-Algebra.Free_Abelian_Groups ...
Processing theory HOL-Algebra.UnivPoly ...
Processing theory HOL-Algebra.Multiplicative_Group ...
Processing theory HOL-Homology.Simplices ...
Processing theory HOL-Homology.Homology_Groups ...
Processing theory HOL-Homology.Brouwer_Degree ...
Processing theory HOL-Homology.Invariance_of_Domain ...
Processing theory HOL-Homology.Homology ...
Processing theory HOL-Analysis-ex.Approximations ...
Removing 41 theories ...
Processing theory HOL-Analysis-ex.Metric_Arith_Examples ...
Loading 95 theories ...
Processing theory HOL-Data_Structures.Less_False ...
Processing theory HOL-Data_Structures.Sorted_Less ...
Processing theory HOL-Computational_Algebra.Group_Closure ...
Processing theory HOL-Computational_Algebra.Fraction_Field ...
Processing theory HOL-Data_Structures.Cmp ...
Processing theory HOL-Data_Structures.AList_Upd_Del ...
Processing theory HOL-Data_Structures.Map_Specs ...
Processing theory HOL-Data_Structures.List_Ins_Del ...
Processing theory HOL-Data_Structures.Set_Specs ...
Processing theory HOL-Library.State_Monad ...
Processing theory HOL-Library.BNF_Axiomatization ...
Processing theory HOL-Computational_Algebra.Normalized_Fraction ...
Processing theory HOL-Computational_Algebra.Nth_Powers ...
Processing theory HOL-Computational_Algebra.Squarefree ...
Processing theory HOL-Library.Case_Converter ...
Processing theory HOL-Library.Code_Lazy ...
Processing theory HOL-Library.Simps_Case_Conv ...
Processing theory HOL-Library.BNF_Corec ...
Processing theory HOL-Library.Multiset_Order ...
Processing theory HOL-Library.Confluence ...
Processing theory HOL-Library.Code_Test ...
Processing theory HOL-Library.Confluent_Quotient ...
Processing theory HOL-Library.Comparator ...
Processing theory HOL-Library.Debug ...
Processing theory HOL-Library.Dual_Ordered_Lattice ...
Processing theory HOL-Library.Function_Algebras ...
Processing theory HOL-Library.Function_Division ...
Processing theory HOL-Library.Dlist ...
Processing theory HOL-Library.Omega_Words_Fun ...
Processing theory HOL-Library.Combine_PER ...
Processing theory HOL-Library.ListVector ...
Processing theory HOL-Library.Extended ...
Processing theory HOL-Examples.Records ...
Processing theory HOL-Library.IArray ...
Processing theory HOL-Library.Char_ord ...
Processing theory HOL-Library.Disjoint_FSets ...
Processing theory HOL-Library.Option_ord ...
Processing theory HOL-Library.Pattern_Aliases ...
Processing theory HOL-Library.Code_Cardinality ...
Processing theory HOL-Library.Type_Length ...
Processing theory HOL-Library.Saturated ...
Processing theory HOL-Library.Power_By_Squaring ...
Processing theory HOL-Library.Quotient_Syntax ...
Processing theory HOL-Library.Quotient_Product ...
Processing theory HOL-Library.Countable_Set_Type ...
Processing theory HOL-Library.Parallel ...
Processing theory HOL-Library.Preorder ...
Processing theory HOL-Library.Quotient_Option ...
Processing theory HOL-Library.Quotient_Set ...
Processing theory HOL-Library.Quotient_List ...
Processing theory HOL-Library.Quotient_Sum ...
Processing theory HOL-Library.Quotient_Type ...
Processing theory HOL-Library.Reflection ...
Processing theory HOL-Library.Finite_Lattice ...
Processing theory HOL-Library.Lattice_Constructions ...
Removing 6 theories ...
Processing theory HOL-Library.Subseq_Order ...
Processing theory HOL-Library.Transitive_Closure_Table ...
Processing theory HOL-Library.Ramsey ...
Processing theory HOL-Library.Signed_Division ...
Processing theory HOL-Library.Tree_Multiset ...
Processing theory HOL-Data_Structures.Tree_Set ...
Processing theory HOL-Data_Structures.Tree_Map ...
Processing theory HOL-Library.While_Combinator ...
Processing theory HOL-Library.Bourbaki_Witt_Fixpoint ...
Processing theory HOL-Library.Z2 ...
Processing theory HOL-Library.Sorting_Algorithms ...
Processing theory HOL-Library.Uprod ...
Processing theory HOL-Number_Theory.Eratosthenes ...
Processing theory HOL-Library.Going_To_Filter ...
Processing theory HOL-Library.Log_Nat ...
Processing theory HOL-Library.BigO ...
Processing theory HOL-Library.Word ...
Processing theory HOL-Library.Quadratic_Discriminant ...
Processing theory HOL-Library.Tree_Real ...
Processing theory HOL-Library.Lub_Glb ...
Processing theory HOL-Library.Lattice_Algebras ...
Processing theory HOL-Computational_Algebra.Polynomial ...
Processing theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra ...
Processing theory HOL-Computational_Algebra.Polynomial_FPS ...
Processing theory HOL-Computational_Algebra.Formal_Laurent_Series ...
Processing theory HOL-Library.Float ...
Processing theory HOL-Computational_Algebra.Polynomial_Factorial ...
Processing theory HOL-Computational_Algebra.Computational_Algebra ...
Processing theory HOL-Library.Interval ...
Processing theory HOL-Library.Interval_Float ...
Processing theory HOL-Library.Library ...
Processing theory HOL-Library.RBT_Impl ...
Processing theory HOL-Library.RBT ...
Processing theory HOL-Codegenerator_Test.Candidates ...
Processing theory HOL-Codegenerator_Test.Generate_Target_Nat ...
Loading 6 theories ...
Processing theory HOL-Library.Product_Lexorder ...
Processing theory HOL-Library.RBT_Mapping ...
Processing theory HOL-Library.RBT_Set ...
Processing theory HOL-Library.DAList ...
Processing theory HOL-Library.DAList_Multiset ...
Removing 1 theories ...
Processing theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures ...
Loading 2 theories ...
Processing theory HOL-Library.Code_Binary_Nat ...
Removing 4 theories ...
Processing theory HOL-Codegenerator_Test.Generate_Binary_Nat ...
Removing 1 theories ...
wrapper script does not seem to be touching the log file in /media/data/jenkins/workspace/isabelle-dump@tmp/durable-3b89ea74
(JENKINS-48300: if on an extremely laggy filesystem, consider -Dorg.jenkinsci.plugins.durabletask.BourneShellScript.HEARTBEAT_CHECK_INTERVAL=86400)
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Store)
Stage "Store" skipped due to earlier failure(s)
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // timeout
[Pipeline] }
[Pipeline] // node
[Pipeline] End of Pipeline
ERROR: script returned exit code -1
Finished: FAILURE