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@75f763dc [Pipeline] } [Pipeline] // script [Pipeline] checkout $ hg clone --rev 24a2a6ced0abb13c6af9966f6281d0af3804240b --noupdate https://isabelle.in.tum.de/repos/isabelle /media/data/jenkins/workspace/isabelle-dump adding changesets adding manifests adding file changes added 74210 changesets with 203002 changes to 11443 files new changesets a5a9c433f639:24a2a6ced0ab [isabelle-dump] $ hg update --rev 24a2a6ced0abb13c6af9966f6281d0af3804240b 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 304f22435bc7e7f710dcbfb36243a87ea57a04f5 --template exists\n exists [isabelle-dump] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('24a2a6ced0abb13c6af9966f6281d0af3804240b') and not ancestors(304f22435bc7e7f710dcbfb36243a87ea57a04f5)" --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 80d141ead0ab579853892b330ffab29b269c5d22 --noupdate https://foss.heptapod.net/isa-afp/afp-devel /media/data/jenkins/workspace/isabelle-dump/afp adding changesets adding manifests adding file changes added 11991 changesets with 80935 changes to 12500 files new changesets 86acbdb19eec:80d141ead0ab [afp] $ hg update --rev 80d141ead0ab579853892b330ffab29b269c5d22 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 dd34e0937e25100492e64393993bc4fcc72667fc --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('80d141ead0ab579853892b330ffab29b269c5d22') and not ancestors(dd34e0937e25100492e64393993bc4fcc72667fc)" --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: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) [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