Console Output

+ 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:28 elapsed time, 0:00:27 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.Option ...
Processing theory HOL.Extraction ...
Processing theory HOL.Lattices_Big ...
Processing theory HOL.Partial_Function ...
Processing theory HOL.Fun_Def ...
Processing theory HOL.Quotient ...
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.Semiring_Normalization ...
Processing theory HOL.SMT ...
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.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.Random ...
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_Exhaustive ...
Processing theory HOL.Record ...
Processing theory HOL.Predicate_Compile ...
Processing theory HOL.Mirabelle ...
Processing theory HOL.Quickcheck_Narrowing ...
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.Higman ...
Processing theory HOL-Proofs-Extraction.Util ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Extraction.Warshall ...
Removing 3 theories ...
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 ...
Processing theory HOL-Proofs-Lambda.ListBeta ...
Processing theory HOL-Proofs-Lambda.InductTermi ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-Lambda.ParRed ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Processing theory HOL-Proofs-Lambda.LambdaType ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Lambda.StrongNorm ...
Processing theory HOL-Library.Multiset ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Removing 14 theories ...
Processing theory HOL-Computational_Algebra.Factorial_Ring ...
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 ...
wrapper script does not seem to be touching the log file in /media/data/jenkins/workspace/isabelle-dump@tmp/durable-f04ac989
(JENKINS-48300: if on an extremely laggy filesystem, consider -Dorg.jenkinsci.plugins.durabletask.BourneShellScript.HEARTBEAT_CHECK_INTERVAL=86400)