Console Output

14:59:05 Started by an SCM change
14:59:05 [EnvInject] - Loading node environment variables.
14:59:05 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all
14:59:05 [isabelle-all] $ hg showconfig paths.default
14:59:05 [isabelle-all] $ hg pull --rev default
14:59:05 pulling from http://isabelle.in.tum.de/repos/isabelle/
14:59:05 searching for changes
14:59:05 no changes found
14:59:05 [isabelle-all] $ hg update --clean --rev default
14:59:05 3 files updated, 0 files merged, 0 files removed, 0 files unresolved
14:59:05 [isabelle-all] $ hg log --rev . --template {node}
14:59:05 [isabelle-all] $ hg log --rev . --template {rev}
14:59:06 [isabelle-all] $ hg log --rev 4343c1bfa52d63a9a9a2d50361005e27bc129893 --template exists\n
14:59:06 exists
14:59:06 [isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(4343c1bfa52d63a9a9a2d50361005e27bc129893)" --encoding UTF-8 --encodingmode replace
14:59:06 [afp] $ hg showconfig paths.default
14:59:06 [afp] $ hg pull --rev default
14:59:07 pulling from https://bitbucket.org/isa-afp/afp-devel/
14:59:07 no changes found
14:59:07 [afp] $ hg update --clean --rev default
14:59:07 470 files updated, 0 files merged, 0 files removed, 0 files unresolved
14:59:07 [afp] $ hg --config extensions.purge= clean --all
14:59:08 [afp] $ hg log --rev . --template {node}
14:59:08 [afp] $ hg log --rev . --template {rev}
14:59:08 [afp] $ hg log --rev c4aeccf9476e45692f55bdd0f6c480ec3414b2a0 --template exists\n
14:59:08 exists
14:59:08 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(c4aeccf9476e45692f55bdd0f6c480ec3414b2a0)" --encoding UTF-8 --encodingmode replace
14:59:08 No emails were triggered.
14:59:08 [isabelle-all] $ /bin/sh -xe /tmp/jenkins1079242947500548391.sh
14:59:08 + Admin/jenkins/run_build all
14:59:08 + set -e
14:59:08 + PROFILE=all
14:59:08 + shift
14:59:08 + bin/isabelle components -a
14:59:08 + bin/isabelle jedit -bf
14:59:08 ### Building Isabelle/Scala ...
14:59:36 ### Building Isabelle/jEdit ...
14:59:54 + bin/isabelle ocaml_setup
14:59:54 # To setup the new switch in the current shell, you need to run:
14:59:54 eval `opam config env`
14:59:54 + bin/isabelle ghc_setup
14:59:55 stack will use a sandboxed GHC it installed
14:59:55 For more information on paths, see 'stack path' and 'stack exec env'
14:59:55 To use this GHC and packages outside of a project, consider using:
14:59:55 stack ghc, stack ghci, stack runghc, or stack exec
14:59:55 The Glorious Glasgow Haskell Compilation System, version 8.4.4
14:59:56 + bin/isabelle ci_build_all
15:00:02 
15:00:02 === CONFIGURATION ===
15:00:02 
15:00:02 ISABELLE_BUILD_OPTIONS=""
15:00:02 
15:00:02 ML_PLATFORM="x86_64-linux"
15:00:02 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"
15:00:02 ML_SYSTEM="polyml-5.8"
15:00:02 ML_OPTIONS="-H 4000 --maxheap 8G"
15:00:02 jobs = 10, threads = 4, numa = false
15:00:02 
15:00:02 === BUILD ===
15:00:02 
15:00:02 Build started at Thu, 14 Mar 2019 14:00:01 GMT
15:00:02 Isabelle id 5382f5691a11
15:00:02 AFP id 0af9f364ab60
15:00:02 
15:00:02 === LOG ===
15:00:02 
15:00:03 Session Pure/Pure
15:00:03 Session CTT/CTT
15:00:04 Session Cube/Cube
15:00:04 Session FOL/FOL
15:00:04 Session CCL/CCL
15:00:04 Session FOL/FOL-ex
15:00:04 Session FOLP/FOLP
15:00:04 Session FOLP/FOLP-ex
15:00:04 Session HOL/HOL (main)
15:00:05 Session AFP/AVL-Trees (AFP)
15:00:05 Session AFP/AWN (AFP)
15:00:05 Session AFP/Abortable_Linearizable_Modules (AFP)
15:00:05 Session AFP/Abstract-Hoare-Logics (AFP)
15:00:05 Session AFP/AnselmGod (AFP)
15:00:05 Session AFP/AxiomaticCategoryTheory (AFP)
15:00:05 Session AFP/BinarySearchTree (AFP)
15:00:05 Session AFP/Binomial-Queues (AFP)
15:00:05 Session AFP/Bondy (AFP)
15:00:05 Session AFP/Bounded_Deducibility_Security (AFP)
15:00:05 Session AFP/BytecodeLogicJmlTypes (AFP)
15:00:05 Session AFP/CISC-Kernel (AFP)
15:00:05 Session AFP/CYK (AFP)
15:00:05 Session AFP/Cauchy (AFP)
15:00:05 Session AFP/Sqrt_Babylonian (AFP)
15:00:05 Session Doc/Classes (doc)
15:00:05 Session AFP/ClockSynchInst (AFP)
15:00:05 Session AFP/Compiling-Exceptions-Correctly (AFP)
15:00:05 Session AFP/ComponentDependencies (AFP)
15:00:05 Session AFP/Concurrent_Revisions (AFP)
15:00:05 Session AFP/Constructor_Funs (AFP)
15:00:05 Session AFP/CryptoBasedCompositionalProperties (AFP)
15:00:05 Session AFP/DPT-SAT-Solver (AFP)
15:00:06 Session AFP/Depth-First-Search (AFP)
15:00:06 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
15:00:06 Session AFP/DiskPaxos (AFP)
15:00:06 Session AFP/Example-Submission (AFP)
15:00:06 Session AFP/FFT (AFP)
15:00:06 Session AFP/FLP (AFP)
15:00:06 Session AFP/FeatherweightJava (AFP)
15:00:06 Session AFP/Featherweight_OCL (AFP)
15:00:06 Session AFP/FileRefinement (AFP)
15:00:06 Session AFP/FocusStreamsCaseStudies (AFP)
15:00:06 Session AFP/Free-Boolean-Algebra (AFP)
15:00:06 Session AFP/FunWithFunctions (AFP)
15:00:06 Session AFP/FunWithTilings (AFP)
15:00:06 Session Doc/Functions (doc)
15:00:06 Session AFP/GPU_Kernel_PL (AFP)
15:00:06 Session AFP/Gauss-Jordan-Elim-Fun (AFP)
15:00:06 Session AFP/GenClock (AFP)
15:00:06 Session AFP/General-Triangle (AFP)
15:00:06 Session AFP/Generic_Deriving (AFP)
15:00:06 Session AFP/GewirthPGCProof (AFP)
15:00:06 Session AFP/GoedelGod (AFP)
15:00:06 Session HOL/HOL-Eisbach
15:00:06 Session AFP/Allen_Calculus (AFP)
15:00:06 Session AFP/Dependent_SIFUM_Type_Systems (AFP)
15:00:06 Session AFP/Dependent_SIFUM_Refinement (AFP)
15:00:07 Session Doc/Eisbach (doc)
15:00:07 Session HOL/HOL-Hoare
15:00:07 Session AFP/Case_Labeling (AFP)
15:00:07 Session HOL/HOL-Hoare_Parallel (timing)
15:00:07 Session HOL/HOL-IMPP
15:00:07 Session HOL/HOL-IOA
15:00:07 Session HOL/HOL-Import
15:00:07 Session HOL/HOL-Lattice
15:00:07 Session HOL/HOL-Library (main timing)
15:00:07 Session AFP/ArrowImpossibilityGS (AFP)
15:00:07 Session AFP/Auto2_HOL (AFP)
15:00:08 Session AFP/BNF_CC (AFP)
15:00:08 Session AFP/BNF_Operations (AFP)
15:00:08 Session AFP/Binomial-Heaps (AFP)
15:00:08 Session AFP/Boolean_Expression_Checkers (AFP)
15:00:08 Session AFP/Buildings (AFP)
15:00:08 Session AFP/CRDT (AFP)
15:00:08 Session AFP/IMAP-CRDT (AFP)
15:00:08 Session AFP/Card_Multisets (AFP)
15:00:08 Session AFP/Card_Number_Partitions (AFP)
15:00:09 Session AFP/Category (AFP)
15:00:09 Session AFP/Category3 (AFP)
15:00:09 Session AFP/MonoidalCategory (AFP)
15:00:09 Session Doc/Codegen (doc)
15:00:09 Session AFP/CofGroups (AFP)
15:00:09 Session AFP/Completeness (AFP)
15:00:09 Session AFP/ConcurrentIMP (AFP)
15:00:09 Session AFP/Concurrent_Ref_Alg (AFP)
15:00:09 Session AFP/CoreC++ (AFP)
15:00:09 Session AFP/Core_DOM (AFP)
15:00:10 Session Doc/Datatypes (doc)
15:00:10 Session Doc/Corec (doc)
15:00:10 Session AFP/Decl_Sem_Fun_PL (AFP)
15:00:10 Session AFP/Derangements (AFP)
15:00:10 Session AFP/Discrete_Summation (AFP)
15:00:10 Session AFP/Card_Partitions (AFP)
15:00:10 Session AFP/Bell_Numbers_Spivey (AFP)
15:00:10 Session AFP/Card_Equiv_Relations (AFP)
15:00:10 Session AFP/Efficient-Mergesort (AFP)
15:00:11 Session AFP/Encodability_Process_Calculi (AFP)
15:00:11 Session AFP/Epistemic_Logic (AFP)
15:00:11 Session AFP/Euler_Partition (AFP)
15:00:11 Session AFP/FOL-Fitting (AFP)
15:00:11 Session AFP/FOL_Harrison (AFP)
15:00:11 Session AFP/Factored_Transition_System_Bounding (AFP)
15:00:11 Session AFP/Falling_Factorial_Sum (AFP)
15:00:11 Session AFP/FinFun (AFP)
15:00:11 Session AFP/Finger-Trees (AFP)
15:00:11 Session AFP/Graph_Saturation (AFP)
15:00:11 Session AFP/Graph_Theory (AFP)
15:00:11 Session AFP/ShortestPath (AFP)
15:00:12 Session AFP/Group-Ring-Module (AFP)
15:00:12 Session AFP/Valuation (AFP)
15:00:12 Session HOL/HOL-Auth (timing)
15:00:12 Session HOL/HOL-UNITY (timing)
15:00:12 Session HOL/HOL-Bali (timing)
15:00:12 Session HOL/HOL-Cardinals (timing)
15:00:12 Session AFP/Ordinals_and_Cardinals (AFP)
15:00:12 Session AFP/Sort_Encodings (AFP)
15:00:12 Session HOL/HOL-Computational_Algebra (main timing)
15:00:12 Session AFP/Descartes_Sign_Rule (AFP)
15:00:12 Session HOL/HOL-Algebra (main timing)
15:00:13 Session HOL/HOL-Decision_Procs (timing)
15:00:13 Session HOL/HOL-Quotient_Examples (timing)
15:00:13 Session AFP/JNF-HOL-Lib (AFP)
15:00:13 Session AFP/Localization_Ring (AFP)
15:00:13 Session AFP/Orbit_Stabiliser (AFP)
15:00:13 Session AFP/Perfect-Number-Thm (AFP)
15:00:14 Session AFP/Secondary_Sylow (AFP)
15:00:14 Session AFP/Jordan_Hoelder (AFP)
15:00:14 Session AFP/VectorSpace (AFP)
15:00:14 Session HOL/HOL-Analysis (main timing)
15:00:14 Session AFP/Bernoulli (AFP)
15:00:14 Session AFP/Cartan_FP (AFP)
15:00:14 Session AFP/Cayley_Hamilton (AFP)
15:00:15 Session AFP/Coinductive (AFP)
15:00:15 Session AFP/DynamicArchitectures (AFP)
15:00:15 Session AFP/Architectural_Design_Patterns (AFP)
15:00:15 Session AFP/Lazy-Lists-II (AFP)
15:00:15 Session AFP/Stream_Fusion_Code (AFP)
15:00:15 Session AFP/Topology (AFP)
15:00:15 Session AFP/First_Welfare_Theorem (AFP)
15:00:15 Session AFP/Green (AFP)
15:00:15 Session HOL/HOL-Analysis-ex
15:00:15 Session HOL/HOL-Probability (main timing)
15:00:16 Session AFP/Buffons_Needle (AFP)
15:00:16 Session AFP/Density_Compiler (AFP)
15:00:16 Session AFP/DiscretePricing (AFP)
15:00:16 Session AFP/Ergodic_Theory (AFP)
15:00:16 Session AFP/Gromov_Hyperbolicity (AFP)
15:00:16 Session AFP/Fisher_Yates (AFP)
15:00:16 Session AFP/Girth_Chromatic (AFP)
15:00:17 Session AFP/Random_Graph_Subgraph_Threshold (AFP)
15:00:17 Session HOL/HOL-Probability-ex (timing)
15:00:17 Session AFP/Lp (AFP)
15:00:17 Session AFP/Markov_Models (AFP)
15:00:17 Session AFP/Monad_Normalisation (AFP)
15:00:17 Session AFP/Monomorphic_Monad (AFP)
15:00:17 Session AFP/Neumann_Morgenstern_Utility (AFP)
15:00:17 Session AFP/Probabilistic_Noninterference (AFP)
15:00:18 Session AFP/Probabilistic_System_Zoo (AFP)
15:00:18 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
15:00:18 Session AFP/Source_Coding_Theorem (AFP)
15:00:18 Session AFP/Irrationality_J_Hancl (AFP)
15:00:18 Session AFP/Kuratowski_Closure_Complement (AFP)
15:00:18 Session AFP/Lower_Semicontinuous (AFP)
15:00:18 Session AFP/Minkowskis_Theorem (AFP)
15:00:18 Session AFP/Octonions (AFP)
15:00:18 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
15:00:18 Session AFP/Ptolemys_Theorem (AFP)
15:00:19 Session AFP/Quaternions (AFP)
15:00:19 Session AFP/Rank_Nullity_Theorem (AFP)
15:00:19 Session AFP/Gauss_Jordan (AFP)
15:00:19 Session AFP/Echelon_Form (AFP)
15:00:19 Session AFP/Hermite (AFP)
15:00:19 Session AFP/Tarskis_Geometry (AFP)
15:00:19 Session AFP/Triangle (AFP)
15:00:19 Session AFP/Chord_Segments (AFP)
15:00:19 Session AFP/Stewart_Apollonius (AFP)
15:00:19 Session AFP/pGCL (AFP)
15:00:20 Session HOL/HOL-Isar_Examples
15:00:20 Session HOL/HOL-Nonstandard_Analysis (timing)
15:00:20 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
15:00:20 Session HOL/HOL-Number_Theory (main timing)
15:00:20 Session AFP/E_Transcendental (AFP)
15:00:20 Session AFP/Elliptic_Curves_Group_Law (AFP)
15:00:20 Session AFP/Fermat3_4 (AFP)
15:00:20 Session HOL/HOL-Data_Structures (timing)
15:00:21 Session HOL/HOL-ex (timing)
15:00:21 Session AFP/Automatic_Refinement (AFP)
15:00:21 Session HOL/HOL-Codegenerator_Test
15:00:22 Session AFP/Lehmer (AFP)
15:00:22 Session AFP/Pratt_Certificate (AFP)
15:00:22 Session AFP/Bertrands_Postulate (AFP)
15:00:22 Session AFP/Prime_Harmonic_Series (AFP)
15:00:22 Session AFP/RSAPSS (AFP)
15:00:22 Session AFP/SumSquares (AFP)
15:00:22 Session AFP/Liouville_Numbers (AFP)
15:00:22 Session AFP/Mason_Stothers (AFP)
15:00:22 Session AFP/Polynomial_Interpolation (AFP)
15:00:23 Session AFP/Probabilistic_Prime_Tests (AFP)
15:00:23 Session AFP/Rep_Fin_Groups (AFP)
15:00:23 Session AFP/Sturm_Sequences (AFP)
15:00:23 Session AFP/Special_Function_Bounds (AFP)
15:00:23 Session AFP/Sturm_Tarski (AFP)
15:00:23 Session AFP/Budan_Fourier (AFP)
15:00:23 Session AFP/Winding_Number_Eval (AFP)
15:00:23 Session AFP/Count_Complex_Roots (AFP)
15:00:24 Session HOL/HOL-Corec_Examples (timing)
15:00:24 Session HOL/HOL-Datatype_Examples (timing)
15:00:24 Session HOL/HOL-Hahn_Banach
15:00:24 Session HOL/HOL-IMP (timing)
15:00:24 Session AFP/Abs_Int_ITP2012 (AFP)
15:00:24 Session HOL/HOL-Imperative_HOL (timing)
15:00:24 Session AFP/Auto2_Imperative_HOL (AFP)
15:00:24 Session AFP/Imperative_Insertion_Sort (AFP)
15:00:24 Session HOL/HOL-Induct
15:00:24 Session HOL/HOL-Matrix_LP
15:00:24 Session HOL/HOL-Metis_Examples (timing)
15:00:24 Session HOL/HOL-MicroJava (timing)
15:00:25 Session HOL/HOL-Mutabelle
15:00:25 Session HOL/HOL-Nitpick_Examples
15:00:25 Session HOL/HOL-Nominal
15:00:25 Session AFP/CCS (AFP)
15:00:25 Session HOL/HOL-Nominal-Examples (timing)
15:00:25 Session AFP/Lam-ml-Normalization (AFP)
15:00:25 Session AFP/Pi_Calculus (AFP)
15:00:25 Session AFP/Psi_Calculi (AFP)
15:00:26 Session AFP/SequentInvertibility (AFP)
15:00:26 Session HOL/HOL-Predicate_Compile_Examples (timing)
15:00:26 Session HOL/HOL-Quickcheck_Examples (timing)
15:00:26 Session HOL/HOL-SET_Protocol (timing)
15:00:26 Session HOL/HOL-TPTP
15:00:26 Session HOL/HOL-Unix
15:00:26 Session HOL/HOL-ZF
15:00:26 Session AFP/Category2 (AFP)
15:00:26 Session AFP/HereditarilyFinite (AFP)
15:00:26 Session AFP/HyperCTL (AFP)
15:00:26 Session AFP/Integration (AFP)
15:00:26 Session AFP/Isabelle_Meta_Model (AFP)
15:00:27 Session AFP/LTL (AFP)
15:00:27 Session AFP/Stuttering_Equivalence (AFP)
15:00:27 Session AFP/Lambda_Free_RPOs (AFP)
15:00:27 Session AFP/Lambda_Free_EPO (AFP)
15:00:27 Session AFP/Landau_Symbols (AFP)
15:00:27 Session AFP/Akra_Bazzi (AFP)
15:00:27 Session AFP/Catalan_Numbers (AFP)
15:00:27 Session AFP/Error_Function (AFP)
15:00:27 Session AFP/Euler_MacLaurin (AFP)
15:00:27 Session AFP/Stirling_Formula (AFP)
15:00:28 Session AFP/LightweightJava (AFP)
15:00:28 Session AFP/LinearQuantifierElim (AFP)
15:00:28 Session AFP/List-Infinite (AFP)
15:00:28 Session AFP/Nat-Interval-Logic (AFP)
15:00:28 Session AFP/AutoFocus-Stream (AFP)
15:00:28 Session AFP/MuchAdoAboutTwo (AFP)
15:00:28 Session AFP/Optics (AFP)
15:00:28 Session AFP/UTP-Toolkit (AFP)
15:00:28 Session AFP/UTP (AFP)
15:00:28 Session AFP/Order_Lattice_Props (AFP)
15:00:28 Session AFP/POPLmark-deBruijn (AFP)
15:00:28 Session AFP/Pairing_Heap (AFP)
15:00:28 Session AFP/Password_Authentication_Protocol (AFP)
15:00:29 Session AFP/Pell (AFP)
15:00:29 Session AFP/Presburger-Automata (AFP)
15:00:29 Session AFP/Priority_Queue_Braun (AFP)
15:00:29 Session AFP/Program-Conflict-Analysis (AFP)
15:00:29 Session AFP/Regular-Sets (AFP)
15:00:29 Session AFP/Abstract-Rewriting (AFP)
15:00:29 Session AFP/Decreasing-Diagrams (AFP)
15:00:29 Session AFP/First_Order_Terms (AFP)
15:00:29 Session AFP/Matrix (AFP)
15:00:29 Session AFP/Matrix_Tensor (AFP)
15:00:29 Session AFP/Knot_Theory (AFP)
15:00:29 Session AFP/Coinductive_Languages (AFP)
15:00:30 Session AFP/Finite_Automata_HF (AFP)
15:00:30 Session AFP/Functional-Automata (AFP)
15:00:30 Session AFP/Posix-Lexing (AFP)
15:00:30 Session AFP/Ribbon_Proofs (AFP)
15:00:30 Session AFP/SATSolverVerification (AFP)
15:00:30 Session AFP/Selection_Heap_Sort (AFP)
15:00:30 Session AFP/Simplex (AFP)
15:00:30 Session AFP/Farkas (AFP)
15:00:30 Session AFP/Skew_Heap (AFP)
15:00:30 Session AFP/Splay_Tree (AFP)
15:00:30 Session AFP/Amortized_Complexity (AFP)
15:00:31 Session AFP/Dynamic_Tables (AFP)
15:00:31 Session AFP/Root_Balanced_Tree (AFP)
15:00:31 Session AFP/Stable_Matching (AFP)
15:00:31 Session AFP/SuperCalc (AFP)
15:00:31 Session AFP/Tail_Recursive_Functions (AFP)
15:00:31 Session AFP/TortoiseHare (AFP)
15:00:31 Session AFP/Trie (AFP)
15:00:31 Session AFP/Flyspeck-Tame (AFP)
15:00:31 Session AFP/Twelvefold_Way (AFP)
15:00:32 Session AFP/Vickrey_Clarke_Groves (AFP)
15:00:32 Session HOL/HOL-Mirabelle
15:00:32 Session HOL/HOL-Mirabelle-ex
15:00:32 Session HOL/HOL-NanoJava
15:00:32 Session HOL/HOL-Prolog
15:00:32 Session HOL/HOL-Real_Asymp
15:00:32 Session HOL/HOL-Real_Asymp-Manual
15:00:32 Session HOL/HOL-Statespace
15:00:32 Session HOL/HOL-TLA
15:00:32 Session HOL/HOL-TLA-Buffer
15:00:32 Session HOL/HOL-TLA-Inc
15:00:32 Session HOL/HOL-TLA-Memory
15:00:32 Session HOL/HOL-Types_To_Sets
15:00:32 Session AFP/Smooth_Manifolds (AFP)
15:00:32 Session HOL/HOL-Word (main timing)
15:00:33 Session HOL/HOL-SPARK
15:00:33 Session HOL/HOL-SPARK-Examples
15:00:33 Session AFP/RIPEMD-160-SPARK (AFP)
15:00:33 Session HOL/HOL-SPARK-Manual
15:00:33 Session HOL/HOL-Word-SMT_Examples (timing)
15:00:33 Session AFP/Kleene_Algebra (AFP)
15:00:33 Session AFP/KAT_and_DRA (AFP)
15:00:33 Session AFP/Multirelations (AFP)
15:00:33 Session AFP/Quantales (AFP)
15:00:33 Session AFP/Transformer_Semantics (AFP)
15:00:34 Session AFP/Regular_Algebras (AFP)
15:00:34 Session AFP/Relation_Algebra (AFP)
15:00:34 Session AFP/Residuated_Lattices (AFP)
15:00:34 Session AFP/LEM (AFP)
15:00:34 Session AFP/Native_Word (AFP)
15:00:34 Session AFP/WebAssembly (AFP)
15:00:35 Session AFP/Refine_Monadic (AFP)
15:00:35 Session AFP/Collections (AFP)
15:00:35 Session AFP/Abstract_Completeness (AFP)
15:00:35 Session AFP/Abstract_Soundness (AFP)
15:00:35 Session AFP/Incredible_Proof_Machine (AFP)
15:00:36 Session AFP/Deriving (AFP)
15:00:36 Session AFP/CAVA_Base (AFP)
15:00:36 Session AFP/CAVA_Automata (AFP)
15:00:36 Session AFP/DFS_Framework (AFP)
15:00:36 Session AFP/Gabow_SCC (AFP)
15:00:37 Session AFP/LTL_to_GBA (AFP)
15:00:37 Session AFP/Promela (AFP)
15:00:37 Session AFP/Containers (AFP)
15:00:37 Session AFP/Collections_Examples (AFP)
15:00:38 Session AFP/Containers-Benchmarks (AFP)
15:00:38 Session AFP/Datatype_Order_Generator (AFP)
15:00:39 Session AFP/Old_Datatype_Show (AFP)
15:00:39 Session AFP/Show (AFP)
15:00:39 Session AFP/JNF-AFP-Lib (AFP)
15:00:39 Session AFP/Real_Impl (AFP)
15:00:40 Session AFP/QR_Decomposition (AFP)
15:00:40 Session AFP/Dijkstra_Shortest_Path (AFP)
15:00:40 Session AFP/Koenigsberg_Friendship (AFP)
15:00:40 Session AFP/Transition_Systems_and_Automata (AFP)
15:00:40 Session AFP/Buchi_Complementation (AFP)
15:00:41 Session AFP/Partial_Order_Reduction (AFP)
15:00:41 Session AFP/SM_Base (AFP)
15:00:41 Session AFP/SM (AFP)
15:00:42 Session AFP/CAVA_Setup (AFP)
15:00:42 Session AFP/CAVA_LTL_Modelchecker (AFP)
15:00:42 Session AFP/Transitive-Closure (AFP)
15:00:42 Session AFP/KBPs (AFP)
15:00:42 Session AFP/Tree-Automata (AFP)
15:00:42 Session AFP/SPARCv8 (AFP)
15:00:43 Session AFP/Separation_Algebra (AFP)
15:00:43 Session AFP/Separata (AFP)
15:00:43 Session AFP/Separation_Logic_Imperative_HOL (AFP)
15:00:43 Session AFP/Sepref_Prereq (AFP)
15:00:44 Session AFP/ROBDD (AFP)
15:00:44 Session AFP/UpDown_Scheme (AFP)
15:00:44 Session AFP/Word_Lib (AFP)
15:00:44 Session AFP/Complx (AFP)
15:00:44 Session AFP/IEEE_Floating_Point (AFP)
15:00:44 Session AFP/CakeML (AFP)
15:00:45 Session AFP/IP_Addresses (AFP)
15:00:45 Session AFP/Simple_Firewall (AFP)
15:00:45 Session AFP/Routing (AFP)
15:00:45 Session AFP/Iptables_Semantics (AFP)
15:00:45 Session AFP/Iptables_Semantics_Examples (AFP)
15:00:45 Session AFP/LOFT (AFP)
15:00:46 Session HOL/HOLCF (main timing)
15:00:46 Session AFP/Circus (AFP)
15:00:46 Session HOL/HOLCF-IMP
15:00:46 Session HOL/HOLCF-Library
15:00:46 Session HOL/HOLCF-FOCUS
15:00:46 Session HOL/HOLCF-ex
15:00:46 Session AFP/PCF (AFP)
15:00:46 Session AFP/HOLCF-Prelude (AFP)
15:00:46 Session HOL/HOLCF-Tutorial
15:00:46 Session HOL/IOA (timing)
15:00:46 Session HOL/IOA-ABP
15:00:47 Session HOL/IOA-NTP
15:00:47 Session HOL/IOA-Storage
15:00:47 Session HOL/IOA-ex
15:00:47 Session AFP/Shivers-CFA (AFP)
15:00:47 Session AFP/Stream-Fusion (AFP)
15:00:47 Session AFP/Tycon (AFP)
15:00:47 Session AFP/WorkerWrapper (AFP)
15:00:47 Session AFP/Heard_Of (AFP)
15:00:47 Session AFP/Consensus_Refined (AFP)
15:00:47 Session AFP/Hoare_Time (AFP)
15:00:47 Session AFP/HotelKeyCards (AFP)
15:00:47 Session Doc/How_to_Prove_it (no_doc)
15:00:47 Session AFP/Huffman (AFP)
15:00:47 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
15:00:48 Session AFP/IMP2 (AFP)
15:00:48 Session Doc/Implementation (doc)
15:00:48 Session AFP/Impossible_Geometry (AFP)
15:00:48 Session AFP/Inductive_Confidentiality (AFP)
15:00:48 Session AFP/InfPathElimination (AFP)
15:00:48 Session Doc/Isar_Ref (doc)
15:00:48 Session Doc/JEdit (doc)
15:00:48 Session AFP/JiveDataStoreModel (AFP)
15:00:48 Session AFP/KAD (AFP)
15:00:48 Session AFP/Algebraic_VCs (AFP)
15:00:49 Session AFP/Key_Agreement_Strong_Adversaries (AFP)
15:00:49 Session AFP/LambdaMu (AFP)
15:00:49 Session AFP/LatticeProperties (AFP)
15:00:49 Session AFP/DataRefinementIBP (AFP)
15:00:49 Session AFP/GraphMarkingIBP (AFP)
15:00:49 Session AFP/Lazy_Case (AFP)
15:00:49 Session AFP/Dict_Construction (AFP)
15:00:49 Session AFP/Lifting_Definition_Option (AFP)
15:00:49 Session AFP/List-Index (AFP)
15:00:49 Session AFP/Affine_Arithmetic (AFP)
15:00:50 Session AFP/Taylor_Models (AFP)
15:00:50 Session AFP/Comparison_Sort_Lower_Bound (AFP)
15:00:50 Session AFP/Formula_Derivatives (AFP)
15:00:50 Session AFP/Formula_Derivatives-Examples (AFP)
15:00:50 Session AFP/Higher_Order_Terms (AFP)
15:00:51 Session AFP/Jinja (AFP)
15:00:51 Session AFP/HRB-Slicing (AFP)
15:00:51 Session AFP/InformationFlowSlicing_Inter (AFP)
15:00:51 Session AFP/Slicing (AFP)
15:00:51 Session AFP/Formal_SSA (AFP)
15:00:52 Session AFP/Minimal_SSA (AFP)
15:00:52 Session AFP/InformationFlowSlicing (AFP)
15:00:52 Session AFP/LTL_to_DRA (AFP)
15:00:52 Session AFP/List_Update (AFP)
15:00:52 Session AFP/Ordinary_Differential_Equations (AFP)
15:00:53 Session AFP/Differential_Dynamic_Logic (AFP)
15:00:53 Session AFP/HOL-ODE-Numerics (AFP)
15:00:54 Session AFP/HOL-ODE-ARCH-COMP (AFP)
15:00:54 Session AFP/HOL-ODE-Examples (AFP large)
15:00:54 Session AFP/Lorenz_Approximation (AFP)
15:00:54 Session AFP/Lorenz_C0 (AFP large)
15:00:54 Session AFP/Lorenz_C1 (AFP large)
15:00:54 Session AFP/Quick_Sort_Cost (AFP)
15:00:54 Session AFP/Random_BSTs (AFP)
15:00:55 Session AFP/Randomised_BSTs (AFP)
15:00:55 Session AFP/Treaps (AFP)
15:00:55 Session AFP/Randomised_Social_Choice (AFP)
15:00:55 Session AFP/Fishburn_Impossibility (AFP)
15:00:55 Session AFP/SDS_Impossibility (AFP)
15:00:56 Session AFP/Refine_Imperative_HOL (AFP)
15:00:56 Session AFP/Floyd_Warshall (AFP)
15:00:56 Session AFP/Sepref_Basic (AFP)
15:00:56 Session AFP/Sepref_IICF (AFP)
15:00:57 Session AFP/Flow_Networks (AFP)
15:00:57 Session AFP/EdmondsKarp_Maxflow (AFP)
15:00:57 Session AFP/MFMC_Countable (AFP)
15:00:57 Session AFP/Prpu_Maxflow (AFP)
15:00:58 Session AFP/Knuth_Morris_Pratt (AFP)
15:00:58 Session AFP/VerifyThis2018 (AFP)
15:00:58 Session AFP/List_Interleaving (AFP)
15:00:58 Session AFP/List_Inversions (AFP)
15:00:58 Session AFP/LocalLexing (AFP)
15:00:58 Session Doc/Locales (doc)
15:00:58 Session AFP/Lowe_Ontological_Argument (AFP)
15:00:58 Session AFP/MSO_Regex_Equivalence (AFP)
15:00:59 Session Doc/Main (doc)
15:00:59 Session AFP/Marriage (AFP)
15:00:59 Session AFP/Latin_Square (AFP)
15:00:59 Session AFP/Matroids (AFP)
15:00:59 Session AFP/Kruskal (AFP)
15:00:59 Session AFP/Max-Card-Matching (AFP)
15:00:59 Session AFP/Median_Of_Medians_Selection (AFP)
15:00:59 Session AFP/Menger (AFP)
15:01:00 Session AFP/MiniML (AFP)
15:01:00 Session AFP/Modular_Assembly_Kit_Security (AFP)
15:01:00 Session AFP/Monad_Memo_DP (AFP)
15:01:00 Session AFP/Hidden_Markov_Models (AFP)
15:01:00 Session AFP/Optimal_BST (AFP)
15:01:00 Session AFP/MonoBoolTranAlgebra (AFP)
15:01:00 Session AFP/Name_Carrying_Type_Inference (AFP)
15:01:00 Session AFP/Network_Security_Policy_Verification (AFP)
15:01:01 Session AFP/No_FTL_observers (AFP)
15:01:01 Session AFP/Nominal2 (AFP)
15:01:01 Session AFP/Incompleteness (AFP)
15:01:02 Session AFP/Surprise_Paradox (AFP)
15:01:02 Session AFP/Launchbury (AFP)
15:01:02 Session AFP/Call_Arity (AFP)
15:01:02 Session AFP/Modal_Logics_for_NTS (AFP)
15:01:02 Session AFP/Rewriting_Z (AFP)
15:01:02 Session AFP/Noninterference_CSP (AFP)
15:01:02 Session AFP/Noninterference_Ipurge_Unwinding (AFP)
15:01:02 Session AFP/Noninterference_Generic_Unwinding (AFP)
15:01:03 Session AFP/Noninterference_Inductive_Unwinding (AFP)
15:01:03 Session AFP/Noninterference_Sequential_Composition (AFP)
15:01:03 Session AFP/Noninterference_Concurrent_Composition (AFP)
15:01:03 Session AFP/NormByEval (AFP)
15:01:03 Session AFP/OpSets (AFP)
15:01:03 Session AFP/Open_Induction (AFP)
15:01:03 Session AFP/Well_Quasi_Orders (AFP)
15:01:03 Session AFP/Decreasing-Diagrams-II (AFP)
15:01:03 Session AFP/Myhill-Nerode (AFP)
15:01:03 Session AFP/Polynomials (AFP)
15:01:03 Session AFP/Symmetric_Polynomials (AFP)
15:01:04 Session AFP/Pi_Transcendental (AFP)
15:01:04 Session AFP/Ordinal (AFP)
15:01:04 Session AFP/Nested_Multisets_Ordinals (AFP)
15:01:05 Session AFP/Lambda_Free_KBOs (AFP)
15:01:05 Session AFP/Ordered_Resolution_Prover (AFP)
15:01:05 Session AFP/PLM (AFP)
15:01:05 Session AFP/PSemigroupsConvolution (AFP)
15:01:05 Session AFP/Paraconsistency (AFP)
15:01:05 Session AFP/Parity_Game (AFP)
15:01:06 Session AFP/Partial_Function_MR (AFP)
15:01:06 Session AFP/Certification_Monads (AFP)
15:01:06 Session AFP/XML (AFP)
15:01:06 Session AFP/Pre_Polynomial_Factorization (AFP)
15:01:06 Session AFP/Polynomial_Factorization (AFP)
15:01:07 Session AFP/Dirichlet_Series (AFP)
15:01:08 Session AFP/Zeta_Function (AFP)
15:01:08 Session AFP/Dirichlet_L (AFP)
15:01:08 Session AFP/Prime_Number_Theorem (AFP)
15:01:09 Session AFP/Prime_Distribution_Elementary (AFP)
15:01:09 Session AFP/Functional_Ordered_Resolution_Prover (AFP)
15:01:10 Session AFP/Jordan_Normal_Form (AFP)
15:01:10 Session AFP/Deep_Learning (AFP)
15:01:10 Session AFP/Groebner_Bases (AFP)
15:01:11 Session AFP/Signature_Groebner (AFP)
15:01:11 Session AFP/Linear_Recurrences (AFP)
15:01:12 Session AFP/Perron_Frobenius (AFP)
15:01:12 Session AFP/Stochastic_Matrices (AFP)
15:01:13 Session AFP/Subresultants (AFP)
15:01:13 Session AFP/Pre_BZ (AFP)
15:01:14 Session AFP/Berlekamp_Zassenhaus (AFP)
15:01:14 Session AFP/Algebraic_Numbers (AFP)
15:01:14 Session AFP/LLL_Basis_Reduction (AFP)
15:01:15 Session AFP/LLL_Factorization (AFP)
15:01:15 Session AFP/Linear_Recurrences_Solver (AFP)
15:01:15 Session AFP/Probabilistic_While (AFP)
15:01:15 Session AFP/Pop_Refinement (AFP)
15:01:15 Session AFP/Possibilistic_Noninterference (AFP)
15:01:16 Session Doc/Prog_Prove (doc)
15:01:16 Session AFP/Projective_Geometry (AFP)
15:01:16 Session AFP/Proof_Strategy_Language (AFP)
15:01:16 Session AFP/PropResPI (AFP)
15:01:16 Session AFP/Propositional_Proof_Systems (AFP)
15:01:16 Session AFP/PseudoHoops (AFP)
15:01:16 Session AFP/Ramsey-Infinite (AFP)
15:01:16 Session AFP/Recursion-Theory-I (AFP)
15:01:16 Session AFP/Minsky_Machines (AFP)
15:01:17 Session AFP/RefinementReactive (AFP)
15:01:17 Session AFP/Resolution_FOL (AFP)
15:01:17 Session AFP/Robbins-Conjecture (AFP)
15:01:17 Session AFP/Roy_Floyd_Warshall (AFP)
15:01:17 Session AFP/SIFPL (AFP)
15:01:17 Session AFP/SIFUM_Type_Systems (AFP)
15:01:17 Session AFP/Security_Protocol_Refinement (AFP)
15:01:17 Session AFP/SenSocialChoice (AFP)
15:01:17 Session AFP/Simpl (AFP)
15:01:18 Session AFP/BDD (AFP)
15:01:18 Session AFP/Planarity_Certificates (AFP)
15:01:18 Session AFP/Statecharts (AFP)
15:01:18 Session AFP/Stone_Algebras (AFP)
15:01:18 Session AFP/Stone_Relation_Algebras (AFP)
15:01:18 Session AFP/Stone_Kleene_Relation_Algebras (AFP)
15:01:18 Session AFP/Aggregation_Algebras (AFP)
15:01:18 Session AFP/Store_Buffer_Reduction (AFP)
15:01:19 Session AFP/Strong_Security (AFP)
15:01:19 Session Doc/Sugar (doc)
15:01:19 Session AFP/TLA (AFP)
15:01:19 Session AFP/Timed_Automata (AFP)
15:01:19 Session AFP/Probabilistic_Timed_Automata (AFP)
15:01:19 Session AFP/Transitive-Closure-II (AFP)
15:01:19 Session AFP/Tree_Decomposition (AFP)
15:01:19 Session Doc/Tutorial (doc)
15:01:19 Session Doc/Typeclass_Hierarchy (doc)
15:01:20 Session AFP/Types_Tableaus_and_Goedels_God (AFP)
15:01:20 Session AFP/UPF (AFP)
15:01:20 Session AFP/UPF_Firewall (AFP)
15:01:20 Session AFP/Universal_Turing_Machine (AFP)
15:01:20 Session AFP/Verified-Prover (AFP)
15:01:20 Session AFP/VolpanoSmith (AFP)
15:01:20 Session AFP/WHATandWHERE_Security (AFP)
15:01:20 Session AFP/Weight_Balanced_Trees (AFP)
15:01:20 Session HOL/HOL-Proofs (timing)
15:01:21 Session HOL/HOL-Proofs-Extraction (timing)
15:01:21 Session HOL/HOL-Proofs-Lambda (timing)
15:01:21 Session AFP/Applicative_Lifting (AFP)
15:01:22 Session AFP/CryptHOL (AFP)
15:01:22 Session AFP/Constructive_Cryptography (AFP)
15:01:22 Session AFP/Game_Based_Crypto (AFP)
15:01:23 Session AFP/Free-Groups (AFP)
15:01:23 Session AFP/Locally-Nameless-Sigma (AFP)
15:01:23 Session AFP/Stern_Brocot (AFP)
15:01:23 Session HOL/HOL-Proofs-ex
15:01:23 Session Tools/Haskell
15:01:23 Session Doc/Intro (doc)
15:01:23 Session LCF/LCF
15:01:23 Session Doc/Logics (doc)
15:01:23 Session Doc/Nitpick (doc)
15:01:23 Session Tools/SML
15:01:23 Session Sequents/Sequents
15:01:23 Session Doc/Sledgehammer (doc)
15:01:23 Session Tools/Spec_Check
15:01:23 Session AFP/Regex_Equivalence (AFP)
15:01:24 Session Doc/System (doc)
15:01:24 Session ZF/ZF (main timing)
15:01:24 Session Doc/Logics_ZF (doc)
15:01:24 Session ZF/ZF-AC
15:01:24 Session ZF/ZF-Coind
15:01:24 Session ZF/ZF-Constructible
15:01:24 Session ZF/ZF-IMP
15:01:24 Session ZF/ZF-Induct
15:01:24 Session ZF/ZF-UNITY (timing)
15:01:24 Session ZF/ZF-Resid
15:01:24 Session ZF/ZF-ex
15:01:38 Building HOL-Library ...
15:01:40 Building HOL-ODE-Numerics ...
15:01:40 Building Collections ...
15:01:40 Building Iptables_Semantics ...
15:01:40 Building HOL-Probability ...
15:01:40 Running Native_Word ...
15:01:40 Building Affine_Arithmetic ...
15:01:41 HOL-Library: theory HOL-Library.AList
15:01:41 HOL-Library: theory HOL-Library.Adhoc_Overloading
15:01:41 HOL-Library: theory HOL-Library.BNF_Axiomatization
15:01:41 HOL-Library: theory HOL-Library.BNF_Corec
15:01:41 Running CakeML ...
15:01:41 HOL-Library: theory HOL-Library.Bit
15:01:41 HOL-Library: theory HOL-Library.Monad_Syntax
15:01:41 HOL-Library: theory HOL-Library.State_Monad
15:01:41 Running Higher_Order_Terms ...
15:01:41 Running Factored_Transition_System_Bounding ...
15:01:41 HOL-Library: theory HOL-Library.Boolean_Algebra
15:01:41 Collections: theory Collections.ICF_Tools
15:01:41 Collections: theory Collections.Partial_Equivalence_Relation
15:01:41 Collections: theory Finger-Trees.FingerTree
15:01:41 Collections: theory HOL-Library.AList
15:01:41 Native_Word: theory HOL-Library.Adhoc_Overloading
15:01:41 Native_Word: theory HOL-Library.Code_Target_Int
15:01:41 Native_Word: theory HOL-Library.Code_Test
15:01:41 Native_Word: theory HOL-Library.Nat_Bijection
15:01:41 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
15:01:41 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
15:01:41 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
15:01:41 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
15:01:41 HOL-ODE-Numerics: theory Collections.ICF_Tools
15:01:41 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
15:01:41 Iptables_Semantics: theory Iptables_Semantics.List_Misc
15:01:41 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
15:01:41 Native_Word: theory HOL-Library.Monad_Syntax
15:01:41 Collections: theory Binomial-Heaps.BinomialHeap
15:01:41 Native_Word: theory HOL-Library.Old_Datatype
15:01:41 Collections: theory Collections.Ord_Code_Preproc
15:01:42 HOL-Library: theory HOL-Library.Cancellation
15:01:42 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
15:01:42 Native_Word: theory Native_Word.More_Bits_Int
15:01:42 HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc
15:01:42 Collections: theory Collections.Locale_Code
15:01:42 HOL-Probability: theory HOL-Library.AList
15:01:42 HOL-Probability: theory HOL-Library.Adhoc_Overloading
15:01:42 HOL-Probability: theory HOL-Library.Conditional_Parametricity
15:01:42 HOL-Probability: theory HOL-Library.Lattice_Syntax
15:01:42 HOL-ODE-Numerics: theory Deriving.Comparator
15:01:42 Higher_Order_Terms: theory HOL-Library.AList
15:01:42 Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading
15:01:42 Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity
15:01:42 Higher_Order_Terms: theory HOL-Library.Nat_Bijection
15:01:42 CakeML: theory CakeML.Doc_Generated
15:01:42 CakeML: theory CakeML.Doc_Ported
15:01:42 CakeML: theory Deriving.Derive_Manager
15:01:42 CakeML: theory CakeML.Doc_Proofs
15:01:42 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
15:01:42 CakeML: theory Deriving.Generator_Aux
15:01:42 CakeML: theory HOL-Library.AList
15:01:42 CakeML: theory HOL-Library.Case_Converter
15:01:42 HOL-ODE-Numerics: theory Collections.Locale_Code
15:01:42 CakeML: theory HOL-Library.Conditional_Parametricity
15:01:42 Affine_Arithmetic: theory Deriving.Comparator
15:01:42 Affine_Arithmetic: theory Deriving.Derive_Manager
15:01:42 Affine_Arithmetic: theory Deriving.Generator_Aux
15:01:42 Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order
15:01:42 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.Acyclicity
15:01:42 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.HoArithUtils
15:01:42 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.RelUtils
15:01:42 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.SetUtils
15:01:42 HOL-Probability: theory HOL-Library.Monad_Syntax
15:01:42 Factored_Transition_System_Bounding: theory HOL-Library.AList
15:01:42 Higher_Order_Terms: theory HOL-Library.Monad_Syntax
15:01:42 Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
15:01:42 HOL-Probability: theory HOL-Library.Mapping
15:01:42 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
15:01:42 HOL-Library: theory HOL-Library.Cardinal_Notations
15:01:42 Collections: theory Collections.Record_Intf
15:01:42 HOL-Library: theory HOL-Library.Case_Converter
15:01:42 Higher_Order_Terms: theory HOL-Library.State_Monad
15:01:42 Factored_Transition_System_Bounding: theory HOL-Library.Conditional_Parametricity
15:01:42 Factored_Transition_System_Bounding: theory HOL-Library.Nat_Bijection
15:01:42 HOL-ODE-Numerics: theory Deriving.Derive_Manager
15:01:42 CakeML: theory HOL-Library.Datatype_Records
15:01:42 Affine_Arithmetic: theory HOL-Library.Monad_Syntax
15:01:42 Collections: theory Binomial-Heaps.SkewBinomialHeap
15:01:42 Affine_Arithmetic: theory Deriving.Equality_Generator
15:01:42 HOL-ODE-Numerics: theory Deriving.Generator_Aux
15:01:42 Affine_Arithmetic: theory HOL-Library.Bit
15:01:42 CakeML: theory HOL-Library.Simps_Case_Conv
15:01:42 HOL-Library: theory HOL-Library.DAList
15:01:42 HOL-Library: theory HOL-Library.Code_Lazy
15:01:42 CakeML: theory HOL-Library.Infinite_Set
15:01:42 HOL-Probability: theory HOL-Library.Stream
15:01:42 HOL-Library: theory HOL-Library.Multiset
15:01:42 Higher_Order_Terms: theory HOL-Library.Old_Datatype
15:01:42 Higher_Order_Terms: theory List-Index.List_Index
15:01:43 HOL-ODE-Numerics: theory Deriving.Equality_Generator
15:01:43 Native_Word: theory HOL-Library.Countable
15:01:43 CakeML: theory HOL-Library.Lattice_Syntax
15:01:43 HOL-ODE-Numerics: theory HOL-Library.AList
15:01:43 CakeML: theory HOL-Library.Complete_Partial_Order2
15:01:43 CakeML: theory HOL-Library.Nat_Bijection
15:01:43 Factored_Transition_System_Bounding: theory HOL-Library.Old_Datatype
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
15:01:43 Factored_Transition_System_Bounding: theory HOL-Library.Sublist
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
15:01:43 CakeML: theory HOL-Library.Old_Datatype
15:01:43 Affine_Arithmetic: theory Deriving.Equality_Instances
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
15:01:43 Affine_Arithmetic: theory HOL-Library.Boolean_Algebra
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
15:01:43 Affine_Arithmetic: theory HOL-Library.Permutation
15:01:43 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
15:01:43 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
15:01:43 Affine_Arithmetic: theory Deriving.Compare
15:01:43 HOL-ODE-Numerics: theory Deriving.Compare
15:01:43 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
15:01:43 Affine_Arithmetic: theory Deriving.Comparator_Generator
15:01:43 HOL-ODE-Numerics: theory Deriving.Equality_Instances
15:01:43 Affine_Arithmetic: theory HOL-Library.Char_ord
15:01:44 Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
15:01:44 CakeML: theory HOL-Library.Sublist
15:01:44 Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
15:01:44 HOL-Probability: theory HOL-Library.Rewrite
15:01:44 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
15:01:44 Higher_Order_Terms: theory HOL-Library.Countable
15:01:44 HOL-Library: theory HOL-Library.Simps_Case_Conv
15:01:44 Affine_Arithmetic: theory HOL-Library.Code_Target_Int
15:01:44 HOL-Library: theory HOL-Library.Extended
15:01:44 Collections: theory HOL-Library.Code_Abstract_Nat
15:01:44 Affine_Arithmetic: theory HOL-Library.Mapping
15:01:44 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
15:01:44 CakeML: theory Word_Lib.Hex_Words
15:01:44 Factored_Transition_System_Bounding: theory HOL-Library.Countable
15:01:44 HOL-Probability: theory HOL-Library.AList_Mapping
15:01:44 Collections: theory HOL-Library.Code_Target_Nat
15:01:44 Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
15:01:44 HOL-ODE-Numerics: theory HOL-Library.Bit
15:01:44 CakeML: theory Word_Lib.Signed_Words
15:01:44 CakeML: theory Word_Lib.Word_Type_Syntax
15:01:44 CakeML: theory Word_Lib.Norm_Words
15:01:44 HOL-Probability: theory HOL-Library.Sublist
15:01:44 Affine_Arithmetic: theory HOL-Library.Type_Length
15:01:44 CakeML: theory Word_Lib.WordBitwise_Signed
15:01:44 HOL-Probability: theory HOL-Library.Tree
15:01:44 HOL-ODE-Numerics: theory HOL-Library.Boolean_Algebra
15:01:44 CakeML: theory HOL-Library.Countable
15:01:44 Collections: theory HOL-Library.Code_Target_Int
15:01:45 HOL-Probability: theory HOL-Library.FSet
15:01:45 Affine_Arithmetic: theory HOL-Library.RBT_Impl
15:01:45 Iptables_Semantics: theory HOL-Library.Code_Target_Int
15:01:45 Iptables_Semantics: theory HOL-Library.LaTeXsugar
15:01:45 Iptables_Semantics: theory Native_Word.More_Bits_Int
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
15:01:45 Native_Word: theory Native_Word.Bits_Integer
15:01:45 Native_Word: theory Native_Word.Word_Misc
15:01:45 HOL-Library: theory HOL-Library.Char_ord
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
15:01:45 CakeML: theory Word_Lib.Word_Syntax
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
15:01:45 Affine_Arithmetic: theory Deriving.Compare_Generator
15:01:45 HOL-Library: theory HOL-Library.Code_Abstract_Nat
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
15:01:45 HOL-Library: theory HOL-Library.Code_Binary_Nat
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Ternary
15:01:45 HOL-Library: theory HOL-Library.Code_Target_Nat
15:01:45 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
15:01:45 HOL-ODE-Numerics: theory HOL-Library.Permutation
15:01:45 Native_Word: theory HOL-Imperative_HOL.Heap
15:01:45 HOL-ODE-Numerics: theory HOL-ex.Quicksort
15:01:45 HOL-Library: theory HOL-Library.Code_Prolog
15:01:45 Collections: theory HOL-Library.Code_Target_Numeral
15:01:45 HOL-ODE-Numerics: theory Deriving.Compare_Generator
15:01:45 HOL-ODE-Numerics: theory HOL-Library.Char_ord
15:01:45 HOL-ODE-Numerics: theory HOL-Library.Mapping
15:01:45 Collections: theory HOL-Library.Dlist
15:01:45 HOL-ODE-Numerics: theory HOL-Library.Option_ord
15:01:46 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
15:01:46 Affine_Arithmetic: theory Deriving.Compare_Instances
15:01:46 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.ListUtils
15:01:46 Factored_Transition_System_Bounding: theory Factored_Transition_System_Bounding.FSSublist
15:01:46 HOL-ODE-Numerics: theory Deriving.Compare_Instances
15:01:46 CakeML: theory Word_Lib.Word_Lib
15:01:46 HOL-ODE-Numerics: theory HOL-Library.Parallel
15:01:46 Affine_Arithmetic: theory HOL-Word.Bits
15:01:46 Higher_Order_Terms: theory HOL-Library.FSet
15:01:46 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
15:01:46 Affine_Arithmetic: theory HOL-Word.Bits_Bit
15:01:46 Affine_Arithmetic: theory HOL-Word.Misc_Numeric
15:01:46 Affine_Arithmetic: theory HOL-Word.Bit_Representation
15:01:47 HOL-Library: theory HOL-Library.Code_Target_Int
15:01:47 HOL-Library: theory HOL-Library.Code_Test
15:01:47 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
15:01:47 Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous
15:01:47 Factored_Transition_System_Bounding: theory HOL-Library.FSet
15:01:47 CakeML: theory HOL-Library.Lattice_Algebras
15:01:47 Affine_Arithmetic: theory HOL-Word.Misc_Typedef
15:01:47 HOL-Probability: theory HOL-Library.Multiset_Permutations
15:01:47 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
15:01:47 HOL-Library: theory HOL-Library.Code_Target_Numeral
15:01:47 HOL-ODE-Numerics: theory HOL-Library.Type_Length
15:01:47 Affine_Arithmetic: theory Deriving.Countable_Generator
15:01:47 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
15:01:47 CakeML: theory HOL-Library.Log_Nat
15:01:47 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
15:01:47 HOL-Library: theory HOL-Library.Comparator
15:01:47 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
15:01:47 Affine_Arithmetic: theory HOL-Word.Bits_Int
15:01:47 CakeML: theory HOL-Library.Countable_Set
15:01:47 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
15:01:47 Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
15:01:47 CakeML: theory HOL-Library.FSet
15:01:48 Collections: theory Collections.SetIterator
15:01:48 Native_Word: theory HOL-Imperative_HOL.Heap_Monad
15:01:48 HOL-ODE-Numerics: theory HOL-Word.Bits_Bit
15:01:48 Collections: theory Collections.Sorted_List_Operations
15:01:48 Affine_Arithmetic: theory HOL-Library.Log_Nat
15:01:48 Iptables_Semantics: theory Native_Word.Bits_Integer
15:01:48 HOL-ODE-Numerics: theory HOL-Word.Word_Miscellaneous
15:01:49 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
15:01:49 CakeML: theory HOL-Library.Countable_Complete_Lattices
15:01:49 HOL-ODE-Numerics: theory Native_Word.More_Bits_Int
15:01:49 CakeML: theory CakeML.Namespace
15:01:49 HOL-Library: theory HOL-Library.Conditional_Parametricity
15:01:49 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
15:01:49 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
15:01:49 HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef
15:01:49 HOL-Library: theory HOL-Library.Datatype_Records
15:01:49 HOL-Probability: theory HOL-Probability.Discrete_Topology
15:01:49 HOL-ODE-Numerics: theory HOL-Word.Word
15:01:50 HOL-Probability: theory HOL-Probability.Essential_Supremum
15:01:50 HOL-Library: theory HOL-Library.Debug
15:01:50 HOL-Library: theory HOL-Library.Disjoint_Sets
15:01:50 HOL-Probability: theory HOL-Probability.Probability_Measure
15:01:50 Collections: theory HOL-Library.RBT_Impl
15:01:50 HOL-Library: theory HOL-Library.Dlist
15:01:50 Affine_Arithmetic: theory HOL-Word.Bool_List_Representation
15:01:50 HOL-Probability: theory HOL-Probability.Stopping_Time
15:01:50 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
15:01:51 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
15:01:51 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
15:01:51 HOL-Probability: theory HOL-Probability.Tree_Space
15:01:51 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
15:01:51 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
15:01:51 Collections: theory Collections.Idx_Iterator
15:01:51 HOL-Library: theory HOL-Library.Fun_Lexorder
15:01:52 HOL-Library: theory HOL-Library.FuncSet
15:01:52 Affine_Arithmetic: theory Native_Word.More_Bits_Int
15:01:52 Native_Word: theory Native_Word.Native_Word_Imperative_HOL
15:01:52 Iptables_Semantics: theory Iptables_Semantics.Ports
15:01:52 Collections: theory Collections.SetAbstractionIterator
15:01:52 HOL-Library: theory HOL-Library.Function_Algebras
15:01:52 CakeML: theory HOL-Library.Order_Continuity
15:01:53 Affine_Arithmetic: theory HOL-Word.Word
15:01:53 HOL-Library: theory HOL-Library.DAList_Multiset
15:01:53 HOL-Library: theory HOL-Library.Multiset_Order
15:01:53 HOL-ODE-Numerics: theory Native_Word.Bits_Integer
15:01:53 HOL-Library: theory HOL-Library.Permutation
15:01:53 HOL-Probability: theory HOL-Library.Finite_Map
15:01:53 HOL-Probability: theory HOL-Probability.Conditional_Expectation
15:01:54 Collections: theory Collections.SetIteratorOperations
15:01:54 CakeML: theory HOL-Library.Extended_Nat
15:01:54 HOL-Probability: theory HOL-Probability.Distribution_Functions
15:01:54 Higher_Order_Terms: theory HOL-Library.Finite_Map
15:01:54 HOL-Probability: theory HOL-Probability.Weak_Convergence
15:01:54 Factored_Transition_System_Bounding: theory HOL-Library.Finite_Map
15:01:55 HOL-Library: theory HOL-Library.Permutations
15:01:55 HOL-Probability: theory HOL-Probability.Giry_Monad
15:01:55 HOL-Library: theory HOL-Library.Equipollence
15:01:55 HOL-Probability: theory HOL-Probability.Helly_Selection
15:01:55 HOL-Library: theory HOL-Library.Function_Division
15:01:55 CakeML: theory HOL-Library.Float
15:01:55 HOL-Library: theory HOL-Library.Groups_Big_Fun
15:01:55 CakeML: theory HOL-Library.Finite_Map
15:01:55 HOL-Library: theory HOL-Library.IArray
15:01:55 Affine_Arithmetic: theory Native_Word.Bits_Integer
15:01:56 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
15:01:56 HOL-Library: theory HOL-Library.Infinite_Set
15:01:56 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
15:01:56 CakeML: theory Coinductive.Coinductive_Nat
15:01:56 Affine_Arithmetic: theory HOL-Library.Float
15:01:56 HOL-Library: theory HOL-Library.LaTeXsugar
15:01:56 HOL-Library: theory HOL-Library.Lattice_Constructions
15:01:56 HOL-Library: theory HOL-Library.Omega_Words_Fun
15:01:57 HOL-Library: theory HOL-Library.Ramsey
15:01:57 HOL-Library: theory HOL-Library.Lattice_Syntax
15:01:57 HOL-Library: theory HOL-Library.Combine_PER
15:01:57 HOL-Library: theory HOL-Library.Complete_Partial_Order2
15:01:57 HOL-Library: theory HOL-Library.ListVector
15:01:57 HOL-Library: theory HOL-Library.List_Lexorder
15:01:57 HOL-Library: theory HOL-Library.Mapping
15:01:57 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
15:01:58 CakeML: theory Coinductive.Coinductive_List
15:01:58 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Native_Word
15:01:58 Native_Word FAILED
15:01:58 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Native_Word)
15:01:58 ROOT.ML:277: warning: Value identifier (x22) has not been referenced.
15:01:58 ROOT.ML:277: warning: Value identifier (x21) has not been referenced.
15:01:58 ROOT.ML:277: warning: Value identifier (A_) has not been referenced.
15:01:58 ROOT.ML:276: warning: Value identifier (x22) has not been referenced.
15:01:58 ROOT.ML:276: warning: Value identifier (x21) has not been referenced.
15:01:58 ROOT.ML:276: warning: Value identifier (A_) has not been referenced.
15:01:58 structure Generated_Code:
15:01:58   sig val bit_integer_test: bool type nat type num end
15:01:58 consts
15:01:58   fold_map ::
15:01:58     "('a \<Rightarrow> 'b Heap)
15:01:58      \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"
15:01:58 ### theory "HOL-Imperative_HOL.Heap_Monad"
15:01:58 ### 4.141s elapsed time, 12.232s cpu time, 0.340s GC time
15:01:58 Loading theory "Native_Word.Native_Word_Imperative_HOL"
15:01:58 ### Metis: Unused theorems: "Nat.semiring_1_class.of_nat_mult"
15:01:58 ocamlfind: Package `zarith' not found
15:01:58 ### theory "Native_Word.Bits_Integer"
15:01:58 ### 8.364s elapsed time, 26.388s cpu time, 1.356s GC time
15:01:58 ### theory "Native_Word.Native_Word_Imperative_HOL"
15:01:58 ### 0.985s elapsed time, 2.592s cpu time, 0.000s GC time
15:01:58 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Native_Word/document -o pdf -n document
15:01:58 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Native_Word/outline -o pdf -n outline -t /proof,/ML
15:01:58 *** Failed to load theory "Native_Word.Code_Target_Bits_Int" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Uint" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Uint16" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Uint32" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Uint64" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Uint8" (unresolved "Native_Word.Bits_Integer")
15:01:58 *** Failed to load theory "Native_Word.Native_Cast" (unresolved "Native_Word.Uint16", "Native_Word.Uint32", "Native_Word.Uint64", "Native_Word.Uint8")
15:01:58 *** Failed to load theory "Native_Word.Native_Cast_Uint" (unresolved "Native_Word.Native_Cast", "Native_Word.Uint")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test" (unresolved "Native_Word.Native_Cast_Uint", "Native_Word.Uint", "Native_Word.Uint16", "Native_Word.Uint32", "Native_Word.Uint64", "Native_Word.Uint8")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test_Emu" (unresolved "Native_Word.Code_Target_Bits_Int", "Native_Word.Native_Word_Test")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test_PolyML2" (unresolved "Native_Word.Native_Word_Test_Emu")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test_PolyML" (unresolved "Native_Word.Native_Word_Test")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test_PolyML64" (unresolved "Native_Word.Native_Word_Test")
15:01:58 *** Failed to load theory "Native_Word.Native_Word_Test_Scala" (unresolved "Native_Word.Native_Word_Test")
15:01:58 *** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Native_Word/outline"
15:01:58 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:01:58 *** At command "export_code" (line 630 of "$AFP/Native_Word/Bits_Integer.thy")
15:01:58 HOL-Library: theory HOL-Library.More_List
15:01:59 HOL-Library: theory HOL-Library.Nat_Bijection
15:01:59 Collections: theory Collections.Assoc_List
15:01:59 HOL-ODE-Numerics: theory Collections.SetIterator
15:01:59 HOL-Library: theory HOL-Library.Stream
15:01:59 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
15:02:00 HOL-Library: theory HOL-Library.AList_Mapping
15:02:00 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
15:02:00 CakeML: theory CakeML.Tokens
15:02:00 CakeML: theory CakeML.NamespaceAuxiliary
15:02:00 CakeML: theory Show.Show
15:02:00 HOL-Library: theory HOL-Library.Old_Datatype
15:02:00 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
15:02:00 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
15:02:00 Collections: theory Collections.Diff_Array
15:02:01 HOL-ODE-Numerics: theory Native_Word.Word_Misc
15:02:01 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
15:02:01 HOL-Probability: theory HOL-Probability.Projective_Family
15:02:01 Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
15:02:01 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
15:02:01 HOL-Library: theory HOL-Library.Old_Recdef
15:02:01 HOL-Library: theory HOL-Library.Open_State_Syntax
15:02:01 HOL-Library: theory HOL-Library.Option_ord
15:02:02 HOL-Library: theory HOL-Library.Parallel
15:02:02 Affine_Arithmetic: theory Native_Word.Word_Misc
15:02:02 HOL-ODE-Numerics: theory Deriving.Countable_Generator
15:02:02 CakeML: theory Show.Show_Instances
15:02:02 HOL-Library: theory HOL-Library.Pattern_Aliases
15:02:02 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
15:02:02 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
15:02:02 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
15:02:02 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
15:02:02 HOL-Library: theory HOL-Library.Perm
15:02:02 HOL-Library: theory HOL-Library.Phantom_Type
15:02:02 HOL-Library: theory HOL-Library.Power_By_Squaring
15:02:03 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
15:02:03 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
15:02:03 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
15:02:03 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
15:02:03 HOL-Library: theory HOL-Library.Preorder
15:02:03 Affine_Arithmetic: theory Affine_Arithmetic.Polygon
15:02:03 HOL-Probability: theory HOL-Probability.Independent_Family
15:02:04 HOL-Probability: theory HOL-Probability.Stream_Space
15:02:04 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
15:02:04 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
15:02:04 HOL-Library: theory HOL-Library.Product_Lexorder
15:02:04 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
15:02:04 HOL-Library: theory HOL-Library.Cardinality
15:02:04 HOL-Library: theory HOL-Library.Product_Plus
15:02:04 HOL-Library: theory HOL-Library.Product_Order
15:02:04 Affine_Arithmetic: theory List-Index.List_Index
15:02:04 HOL-Library: theory HOL-Library.Quotient_Syntax
15:02:04 HOL-Library: theory HOL-Library.Quotient_Option
15:02:04 HOL-Library: theory HOL-Library.Quotient_Product
15:02:04 Affine_Arithmetic: theory Show.Show
15:02:04 HOL-Library: theory HOL-Library.Quotient_Set
15:02:04 Collections: theory Collections.Dlist_add
15:02:05 HOL-Library: theory HOL-Library.Finite_Lattice
15:02:05 HOL-Library: theory HOL-Library.Quotient_List
15:02:05 Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
15:02:05 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
15:02:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
15:02:05 HOL-Probability: theory HOL-Probability.PMF_Impl
15:02:05 CakeML: theory Word_Lib.Enumeration
15:02:05 HOL-Library: theory HOL-Library.Quotient_Sum
15:02:05 HOL-Library: theory HOL-Library.Quotient_Type
15:02:05 Collections: theory Collections.Proper_Iterator
15:02:05 Collections: theory Collections.SetIteratorGA
15:02:05 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
15:02:05 HOL-Library: theory HOL-Library.RBT_Impl
15:02:05 HOL-Library: theory HOL-Library.Realizers
15:02:06 HOL-Probability: theory HOL-Probability.Random_Permutations
15:02:06 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
15:02:06 HOL-Probability: theory HOL-Probability.SPMF
15:02:06 CakeML: theory Word_Lib.Word_Enum
15:02:06 HOL-ODE-Numerics: theory Collections.Assoc_List
15:02:06 Collections: theory Collections.It_to_It
15:02:06 HOL-Library: theory HOL-Library.Numeral_Type
15:02:06 Affine_Arithmetic: theory Show.Show_Instances
15:02:06 Collections: theory Collections.DatRef
15:02:06 HOL-Library: theory HOL-Library.Reflection
15:02:06 Collections: theory Native_Word.More_Bits_Int
15:02:07 HOL-Library: theory HOL-Library.Refute
15:02:07 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
15:02:07 HOL-ODE-Numerics: theory Collections.Diff_Array
15:02:07 CakeML: theory Word_Lib.Word_Setup_64
15:02:07 CakeML: theory Word_Lib.HOL_Lemmas
15:02:07 HOL-ODE-Numerics: theory Collections.Proper_Iterator
15:02:07 CakeML: theory Word_Lib.More_Divides
15:02:07 HOL-Probability: theory HOL-Probability.Convolution
15:02:07 CakeML: theory Word_Lib.Aligned
15:02:08 Collections: theory Collections.Gen_Iterator
15:02:08 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
15:02:08 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
15:02:08 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
15:02:08 HOL-Probability: theory HOL-Probability.Information
15:02:08 HOL-ODE-Numerics: theory Collections.It_to_It
15:02:08 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
15:02:09 HOL-ODE-Numerics: theory Collections.SetIteratorGA
15:02:09 CakeML: theory Word_Lib.Word_Next
15:02:09 CakeML: theory Word_Lib.Word_Lemmas
15:02:09 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
15:02:09 Collections: theory Collections.Iterator
15:02:10 Collections: theory Native_Word.Bits_Integer
15:02:10 CakeML: theory CakeML.Lib
15:02:10 Collections: theory Native_Word.Word_Misc
15:02:10 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
15:02:11 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
15:02:12 HOL-Library: theory HOL-Library.Type_Length
15:02:12 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
15:02:12 Collections: theory Collections.ICF_Spec_Base
15:02:12 HOL-Library: theory HOL-Library.Saturated
15:02:13 Collections: theory Collections.MapSpec
15:02:13 HOL-Library: theory HOL-Library.Rewrite
15:02:13 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
15:02:14 HOL-Probability: theory HOL-Probability.Distributions
15:02:14 HOL-Library: theory HOL-Library.Set_Algebras
15:02:14 HOL-Library: theory HOL-Library.Sorting_Algorithms
15:02:14 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
15:02:14 HOL-Library: theory HOL-Library.Stirling
15:02:15 HOL-Library: theory HOL-Library.Sublist
15:02:15 HOL-Library: theory HOL-Library.Transitive_Closure_Table
15:02:15 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
15:02:15 Iptables_Semantics: theory Iptables_Semantics.Semantics
15:02:15 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
15:02:17 HOL-Library: theory HOL-Library.Tree
15:02:17 HOL-Library: theory HOL-Library.Uprod
15:02:17 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
15:02:17 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
15:02:17 HOL-ODE-Numerics: theory Collections.Intf_Comp
15:02:17 HOL-Probability: theory HOL-Probability.Characteristic_Functions
15:02:17 HOL-Probability: theory HOL-Probability.Sinc_Integral
15:02:18 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
15:02:18 CakeML: theory CakeML.LibAuxiliary
15:02:18 CakeML: theory CakeML.Ffi
15:02:19 HOL-Library: theory HOL-Library.While_Combinator
15:02:19 HOL-Library: theory HOL-Library.Prefix_Order
15:02:19 HOL-Library: theory HOL-Library.Subseq_Order
15:02:19 HOL-Library: theory HOL-Library.Countable
15:02:19 HOL-Probability: theory HOL-Probability.Levy
15:02:19 Iptables_Semantics: theory Iptables_Semantics.Matching
15:02:19 CakeML: theory IEEE_Floating_Point.IEEE
15:02:20 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
15:02:20 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
15:02:20 CakeML: theory Word_Lib.Word_Lemmas_64
15:02:20 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
15:02:20 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
15:02:20 HOL-ODE-Numerics: theory Collections.Idx_Iterator
15:02:20 HOL-Library: theory HOL-Library.BigO
15:02:21 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
15:02:21 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
15:02:21 Collections: theory Collections.Robdd
15:02:21 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
15:02:21 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
15:02:21 HOL-Library: theory HOL-Library.Countable_Set
15:02:22 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
15:02:22 HOL-Library: theory HOL-Library.Tree_Multiset
15:02:22 HOL-Library: theory HOL-Library.FSet
15:02:22 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
15:02:22 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
15:02:22 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
15:02:23 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms
15:02:23 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document.pdf
15:02:23 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline.pdf
15:02:23 Higher_Order_Terms FAILED
15:02:23 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Higher_Order_Terms)
15:02:23     val fmdoma: ('a, 'b) fmap -> 'a set
15:02:23     val fmdrop: 'a equal -> 'a -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmdrop_fset: 'a equal -> 'a fset -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmdrop_set: 'a equal -> 'a set -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmempty: ('a, 'b) fmap
15:02:23     val fmfilter: ('a -> bool) -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmimage: 'a equal -> ('a, 'b) fmap -> 'a fset -> 'b fset
15:02:23     val fmlookup: 'a equal -> ('a, 'b) fmap -> 'a -> 'b option
15:02:23     val fmmap: ('a -> 'b) -> ('c, 'a) fmap -> ('c, 'b) fmap
15:02:23     val fmmap_keys: ('a -> 'b -> 'c) -> ('a, 'b) fmap -> ('a, 'c) fmap
15:02:23     val fmpred: 'a equal -> ('a -> 'b -> bool) -> ('a, 'b) fmap -> bool
15:02:23     val fmran: 'a equal -> ('a, 'b) fmap -> 'b fset
15:02:23     val fmrana: 'a equal -> ('a, 'b) fmap -> 'b set
15:02:23     val fmrel:
15:02:23        'a equal ->
15:02:23          ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool
15:02:23     val fmrel_on_fset:
15:02:23        'a equal ->
15:02:23          'a fset ->
15:02:23            ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool
15:02:23     val fmrestrict_fset:
15:02:23        'a equal -> 'a fset -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmrestrict_set: 'a equal -> 'a set -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     val fmsubset:
15:02:23        'a equal -> 'b equal -> ('a, 'b) fmap -> ('a, 'b) fmap -> bool
15:02:23     val fmupd: 'a equal -> 'a -> 'b -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:23     type 'a fset
15:02:23     val pred_fmap: 'a equal -> ('b -> bool) -> ('a, 'b) fmap -> bool
15:02:23     type 'a set
15:02:23   end
15:02:23 ocamlfind: Package `zarith' not found
15:02:23 ### theory "HOL-Library.Finite_Map"
15:02:23 ### 23.382s elapsed time, 15.576s cpu time, 0.208s GC time
15:02:23 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document -o pdf -n document
15:02:23 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline -o pdf -n outline -t /proof,/ML
15:02:23 *** Failed to load theory "Higher_Order_Terms.Disjoint_Sets" (unresolved "HOL-Library.Finite_Map")
15:02:23 *** Failed to load theory "Higher_Order_Terms.Term_Utils" (unresolved "HOL-Library.Finite_Map")
15:02:23 *** Failed to load theory "Higher_Order_Terms.Find_First" (unresolved "HOL-Library.Finite_Map")
15:02:23 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:02:23 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")
15:02:23 HOL-Library: theory HOL-Library.Countable_Set_Type
15:02:23 Iptables_Semantics: theory Iptables_Semantics.Optimizing
15:02:24 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factored_Transition_System_Bounding
15:02:24 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factored_Transition_System_Bounding/document.pdf
15:02:24 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factored_Transition_System_Bounding/outline.pdf
15:02:24 Factored_Transition_System_Bounding FAILED
15:02:24 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Factored_Transition_System_Bounding)
15:02:24     val fmimage: 'a equal -> ('a, 'b) fmap -> 'a fset -> 'b fset
15:02:24     val fmlookup: 'a equal -> ('a, 'b) fmap -> 'a -> 'b option
15:02:24     val fmmap: ('a -> 'b) -> ('c, 'a) fmap -> ('c, 'b) fmap
15:02:24     val fmmap_keys: ('a -> 'b -> 'c) -> ('a, 'b) fmap -> ('a, 'c) fmap
15:02:24     val fmpred: 'a equal -> ('a -> 'b -> bool) -> ('a, 'b) fmap -> bool
15:02:24     val fmran: 'a equal -> ('a, 'b) fmap -> 'b fset
15:02:24     val fmrana: 'a equal -> ('a, 'b) fmap -> 'b set
15:02:24     val fmrel:
15:02:24        'a equal ->
15:02:24          ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool
15:02:24     val fmrel_on_fset:
15:02:24        'a equal ->
15:02:24          'a fset ->
15:02:24            ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool
15:02:24     val fmrestrict_fset:
15:02:24        'a equal -> 'a fset -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:24     val fmrestrict_set: 'a equal -> 'a set -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:24     val fmsubset:
15:02:24        'a equal -> 'b equal -> ('a, 'b) fmap -> ('a, 'b) fmap -> bool
15:02:24     val fmupd: 'a equal -> 'a -> 'b -> ('a, 'b) fmap -> ('a, 'b) fmap
15:02:24     type 'a fset
15:02:24     val pred_fmap: 'a equal -> ('b -> bool) -> ('a, 'b) fmap -> bool
15:02:24     type 'a set
15:02:24   end
15:02:24 ocamlfind: Package `zarith' not found
15:02:24 ### theory "HOL-Library.Finite_Map"
15:02:24 ### 23.492s elapsed time, 35.028s cpu time, 0.848s GC time
15:02:24 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factored_Transition_System_Bounding/document -o pdf -n document
15:02:24 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factored_Transition_System_Bounding/outline -o pdf -n outline -t /proof,/ML
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.FactoredSystemLib" (unresolved "HOL-Library.Finite_Map")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.FmapUtils" (unresolved "Factored_Transition_System_Bounding.FactoredSystemLib", "HOL-Library.Finite_Map")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.FactoredSystem" (unresolved "Factored_Transition_System_Bounding.FactoredSystemLib", "Factored_Transition_System_Bounding.FmapUtils", "HOL-Library.Finite_Map")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.ActionSeqProcess" (unresolved "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FactoredSystemLib")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.Invariants" (unresolved "Factored_Transition_System_Bounding.FactoredSystem")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.Dependency" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem", "HOL-Library.Finite_Map")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.TopologicalProps" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.SystemAbstraction" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.Dependency", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FactoredSystemLib", "Factored_Transition_System_Bounding.FmapUtils", "Factored_Transition_System_Bounding.TopologicalProps", "HOL-Library.Finite_Map")
15:02:24 *** Failed to load theory "Factored_Transition_System_Bounding.AcycSspace" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FmapUtils", "Factored_Transition_System_Bounding.SystemAbstraction")
15:02:24 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:02:24 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")
15:02:24 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
15:02:24 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
15:02:25 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
15:02:25 Affine_Arithmetic: theory Affine_Arithmetic.Intersection
15:02:25 CakeML: theory IEEE_Floating_Point.FP64
15:02:25 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
15:02:25 HOL-Library: theory HOL-Library.Set_Idioms
15:02:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
15:02:26 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
15:02:26 HOL-Library: theory HOL-Library.Diagonal_Subsequence
15:02:26 CakeML: theory CakeML.FpSem
15:02:26 HOL-Library: theory HOL-Library.Discrete
15:02:26 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
15:02:26 HOL-Library: theory HOL-Library.Going_To_Filter
15:02:26 HOL-Library: theory HOL-Library.Indicator_Function
15:02:26 HOL-Library: theory HOL-Library.Landau_Symbols
15:02:27 HOL-Library: theory HOL-Library.Lattice_Algebras
15:02:28 HOL-Library: theory HOL-Library.Finite_Map
15:02:30 HOL-Library: theory HOL-Library.Liminf_Limsup
15:02:30 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
15:02:31 CakeML: theory CakeML.SimpleIO
15:02:31 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
15:02:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
15:02:31 HOL-Library: theory HOL-Library.Log_Nat
15:02:31 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
15:02:32 HOL-Library: theory HOL-Library.Lub_Glb
15:02:32 CakeML: theory CakeML.Ast
15:02:32 HOL-Library: theory HOL-Library.Multiset_Permutations
15:02:32 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
15:02:32 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
15:02:33 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
15:02:33 HOL-ODE-Numerics: theory Show.Show
15:02:33 HOL-Library: theory HOL-Library.Float
15:02:33 HOL-Library: theory HOL-Library.Nonpos_Ints
15:02:34 HOL-Library: theory HOL-Library.OptionalSugar
15:02:34 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
15:02:34 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
15:02:34 HOL-Library: theory HOL-Library.Order_Continuity
15:02:35 HOL-ODE-Numerics: theory Show.Show_Instances
15:02:35 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
15:02:35 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
15:02:35 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
15:02:35 HOL-Library: theory HOL-Library.Extended_Nat
15:02:36 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
15:02:36 HOL-Library: theory HOL-Library.Periodic_Fun
15:02:36 HOL-Library: theory HOL-Library.Extended_Real
15:02:37 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
15:02:37 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
15:02:37 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
15:02:39 HOL-Library: theory HOL-Library.Quadratic_Discriminant
15:02:39 HOL-Library: theory HOL-Library.Sum_of_Squares
15:02:42 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
15:02:42 Affine_Arithmetic: theory HOL-Library.RBT
15:02:42 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
15:02:42 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
15:02:42 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
15:02:43 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
15:02:43 Affine_Arithmetic: theory HOL-Library.RBT_Mapping
15:02:43 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
15:02:45 HOL-Library: theory HOL-Library.Tree_Real
15:02:45 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
15:02:46 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
15:02:46 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
15:02:46 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
15:02:48 HOL-ODE-Numerics: theory HOL-Library.RBT
15:02:49 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
15:02:50 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
15:02:51 Collections: theory Collections.RBT_add
15:02:51 HOL-ODE-Numerics: theory Collections.Gen_Iterator
15:02:51 HOL-ODE-Numerics: theory Collections.Intf_Map
15:02:51 HOL-ODE-Numerics: theory Collections.Intf_Set
15:02:52 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
15:02:52 HOL-ODE-Numerics: theory Collections.Iterator
15:02:54 HOL-ODE-Numerics: theory Collections.RBT_add
15:02:54 HOL-ODE-Numerics: theory Collections.Gen_Map
15:02:55 HOL-ODE-Numerics: theory Collections.Impl_List_Map
15:02:55 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
15:02:56 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
15:02:56 HOL-ODE-Numerics: theory Collections.Gen_Set
15:02:56 HOL-ODE-Numerics: theory Collections.Impl_List_Set
15:03:03 HOL-Library: theory HOL-Library.RBT
15:03:04 HOL-Library: theory HOL-Library.RBT_Mapping
15:03:05 HOL-Library: theory HOL-Library.RBT_Set
15:03:12 CakeML: theory CakeML.CakeML_Compiler
15:03:12 CakeML: theory CakeML.AstAuxiliary
15:03:12 CakeML: theory CakeML.SemanticPrimitives
15:03:15 Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
15:03:27 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
15:03:27 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
15:03:27 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
15:03:28 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
15:03:28 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
15:03:28 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
15:03:30 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
15:03:31 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
15:03:31 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections
15:03:31 Collections FAILED
15:03:31 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Collections)
15:03:31 \<lbrakk>\<And>e a r ts.
15:03:31             ?Q ts \<Longrightarrow>
15:03:31             ?P (SkewBinomialHeapStruc.Node e a r ts);
15:03:31  ?Q [];
15:03:31  \<And>t q.
15:03:31     \<lbrakk>?P t; ?Q q\<rbrakk> \<Longrightarrow> ?Q (t # q)\<rbrakk>
15:03:31 \<Longrightarrow> ?Q ?a1.0
15:03:31 ### Ignoring duplicate rewrite rule:
15:03:31 ### ?n1 \<le> Suc (length ?kvs1) \<Longrightarrow>
15:03:31 ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \<equiv> take (?n1 - 1) ?kvs1
15:03:31 Found termination order:
15:03:31   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>
15:03:31    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"
15:03:31 Found termination order:
15:03:31   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>
15:03:31    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"
15:03:31 ### Rule already declared as introduction (intro)
15:03:31 ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
15:03:31 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/document -o pdf -n document
15:03:31 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/userguide -o pdf -n userguide
15:03:31 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/outline -o pdf -n outline -t /proof,/ML
15:03:31 *** Failed to load theory "Native_Word.Code_Target_Bits_Int" (unresolved "Native_Word.Bits_Integer")
15:03:31 *** Failed to load theory "Collections.Code_Target_ICF" (unresolved "Native_Word.Code_Target_Bits_Int")
15:03:31 *** Failed to load theory "Collections.Locale_Code_Ex" (unresolved "Collections.Code_Target_ICF")
15:03:31 *** Failed to load theory "Native_Word.Uint32" (unresolved "Native_Word.Bits_Integer")
15:03:31 *** Failed to load theory "Collections.HashCode" (unresolved "Native_Word.Uint32")
15:03:31 *** Latex error:
15:03:31 ***   File `ICF_Userguide.tex' not found.
15:03:31 *** Latex error (line 55 of "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/userguide/root_userguide.tex"):
15:03:31 ***   Emergency stop.
15:03:31 ***   <read *> 
15:03:31 ***            
15:03:31 ***   \input{ICF_Userguide}
15:03:31 *** Latex error (line 55 of "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/userguide/root_userguide.tex"):
15:03:31 ***    ==> Fatal error occurred, no output PDF file produced
15:03:31 *** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Collections/userguide"
15:03:31 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:03:31 *** At command "export_code" (line 630 of "$AFP/Native_Word/Bits_Integer.thy")
15:03:31 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:03:31 *** At command "export_code" (line 1067 of "$AFP/Collections/Lib/Diff_Array.thy")
15:03:31 CAVA_Base CANCELLED
15:03:31 CAVA_Automata CANCELLED
15:03:31 CAVA_Setup CANCELLED
15:03:31 Sepref_Prereq CANCELLED
15:03:31 Formal_SSA CANCELLED
15:03:31 Sepref_Basic CANCELLED
15:03:31 Sepref_IICF CANCELLED
15:03:31 CAVA_LTL_Modelchecker CANCELLED
15:03:31 Flow_Networks CANCELLED
15:03:31 Refine_Imperative_HOL CANCELLED
15:03:31 SM_Base CANCELLED
15:03:31 Transition_Systems_and_Automata CANCELLED
15:03:31 DFS_Framework CANCELLED
15:03:31 Prpu_Maxflow CANCELLED
15:03:31 Promela CANCELLED
15:03:31 Collections_Examples CANCELLED
15:03:31 LTL_to_GBA CANCELLED
15:03:31 Gabow_SCC CANCELLED
15:03:31 SM CANCELLED
15:03:31 EdmondsKarp_Maxflow CANCELLED
15:03:31 Dijkstra_Shortest_Path CANCELLED
15:03:31 VerifyThis2018 CANCELLED
15:03:31 Partial_Order_Reduction CANCELLED
15:03:31 Tree-Automata CANCELLED
15:03:31 Buchi_Complementation CANCELLED
15:03:31 Kruskal CANCELLED
15:03:31 ROBDD CANCELLED
15:03:31 Knuth_Morris_Pratt CANCELLED
15:03:31 Floyd_Warshall CANCELLED
15:03:31 Minimal_SSA CANCELLED
15:03:31 Transitive-Closure CANCELLED
15:03:33 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
15:03:33 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
15:03:36 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
15:03:39 Iptables_Semantics: theory Iptables_Semantics.Transform
15:03:44 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
15:03:45 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
15:03:54 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
15:03:54 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
15:03:55 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
15:03:55 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
15:03:56 CakeML: theory CakeML.CakeML_Quickcheck
15:03:56 CakeML: theory CakeML.Evaluate
15:03:56 CakeML: theory CakeML.SmallStep
15:03:59 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability
15:03:59 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/document.pdf
15:03:59 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/outline.pdf
15:03:59 HOL-Probability FAILED
15:03:59 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/HOL-Probability)
15:03:59 ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True
15:03:59 ### Ignoring duplicate rewrite rule:
15:03:59 ### of_real (?x1 * ?y1) \<equiv> of_real ?x1 * of_real ?y1
15:03:59 ### Ignoring duplicate rewrite rule:
15:03:59 ### \<Prod>x\<in>?A1. ?y1 \<equiv> ?y1 ^ card ?A1
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s)
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
15:03:59 ### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
15:03:59 ### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>;
15:03:59 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
15:03:59 ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
15:03:59 ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>;
15:03:59 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
15:03:59 ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>;
15:03:59 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>
15:03:59 ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F
15:03:59 ### Rule already declared as introduction (intro)
15:03:59 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>
15:03:59 ### ((\<lambda>x. ennreal (?f x)) \<longlongrightarrow> ennreal ?x) ?F
15:03:59 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/outline -o pdf -n outline -t /proof,/ML
15:03:59 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/document -o pdf -n document
15:03:59 *** Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
15:03:59 *** Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
15:03:59 *** Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
15:03:59 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:03:59 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")
15:03:59 Probabilistic_While CANCELLED
15:03:59 CryptHOL CANCELLED
15:03:59 Markov_Models CANCELLED
15:03:59 Constructive_Cryptography CANCELLED
15:03:59 Stochastic_Matrices CANCELLED
15:03:59 Probabilistic_Timed_Automata CANCELLED
15:03:59 Deep_Learning CANCELLED
15:03:59 Probabilistic_Prime_Tests CANCELLED
15:03:59 List_Update CANCELLED
15:03:59 Hidden_Markov_Models CANCELLED
15:03:59 Density_Compiler CANCELLED
15:03:59 Girth_Chromatic CANCELLED
15:03:59 Probabilistic_Noninterference CANCELLED
15:03:59 Applicative_Lifting CANCELLED
15:03:59 MFMC_Countable CANCELLED
15:03:59 DiscretePricing CANCELLED
15:03:59 Ergodic_Theory CANCELLED
15:03:59 Randomised_Social_Choice CANCELLED
15:03:59 Stern_Brocot CANCELLED
15:03:59 Probabilistic_System_Zoo CANCELLED
15:03:59 Treaps CANCELLED
15:03:59 Probabilistic_System_Zoo-Non_BNFs CANCELLED
15:03:59 SDS_Impossibility CANCELLED
15:03:59 Monomorphic_Monad CANCELLED
15:03:59 Game_Based_Crypto CANCELLED
15:03:59 Quick_Sort_Cost CANCELLED
15:03:59 Lp CANCELLED
15:03:59 Random_BSTs CANCELLED
15:03:59 Neumann_Morgenstern_Utility CANCELLED
15:03:59 Randomised_BSTs CANCELLED
15:03:59 HOL-Probability-ex CANCELLED
15:03:59 Random_Graph_Subgraph_Threshold CANCELLED
15:03:59 Buffons_Needle CANCELLED
15:03:59 Source_Coding_Theorem CANCELLED
15:03:59 Fisher_Yates CANCELLED
15:03:59 Monad_Normalisation CANCELLED
15:04:02 CakeML: theory CakeML.BigStep
15:04:02 CakeML: theory CakeML.PrimTypes
15:04:26 CakeML: theory CakeML.BigSmallInvariants
15:04:27 CakeML: theory CakeML.TypeSystem
15:04:31 CakeML: theory CakeML.SemanticPrimitivesAuxiliary
15:04:32 CakeML: theory CakeML.Semantic_Extras
15:04:35 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics
15:04:35 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics/document.pdf
15:04:35 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics/outline.pdf
15:04:35 Iptables_Semantics FAILED
15:04:35 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Iptables_Semantics)
15:04:35  \<forall>a. \<not> ?disc2.0 (Prot a);
15:04:35  \<forall>r\<in>set ?rs.
15:04:35     normalized_n_primitive (?disc2.0, ?sel2.0) ?f (get_match r)\<rbrakk>
15:04:35 \<Longrightarrow> \<forall>r\<in>set (transform_normalize_primitives ?rs).
15:04:35                      normalized_n_primitive (?disc2.0, ?sel2.0) ?f
15:04:35                       (get_match r)
15:04:35 \<lbrakk>simple_ruleset ?rs;
15:04:35  \<forall>r\<in>set ?rs. normalized_nnf_match (get_match r);
15:04:35  (\<forall>a. \<not> ?disc3.0 (Src_Ports a)) \<and>
15:04:35  (\<forall>a. \<not> ?disc3.0 (Dst_Ports a)) \<and>
15:04:35  (\<forall>a. \<not> ?disc3.0 (Src a)) \<and>
15:04:35  (\<forall>a. \<not> ?disc3.0 (Dst a));
15:04:35  ((\<forall>a. \<not> ?disc3.0 (IIface a)) \<or>
15:04:35   ?disc3.0 = is_Iiface) \<and>
15:04:35  ((\<forall>a. \<not> ?disc3.0 (OIface a)) \<or> ?disc3.0 = is_Oiface);
15:04:35  (\<forall>a. \<not> ?disc3.0 (Prot a)) \<or>
15:04:35  ?disc3.0 = is_Prot \<and>
15:04:35  (\<forall>r\<in>set ?rs.
15:04:35      \<not> has_disc_negated is_Src_Ports False (get_match r) \<and>
15:04:35      \<not> has_disc_negated is_Dst_Ports False (get_match r) \<and>
15:04:35      \<not> has_disc is_MultiportPorts (get_match r));
15:04:35  \<forall>r\<in>set ?rs.
15:04:35     \<not> has_disc_negated ?disc3.0 False (get_match r)\<rbrakk>
15:04:35 \<Longrightarrow> \<forall>r\<in>set (transform_normalize_primitives ?rs).
15:04:35                      \<not> has_disc_negated ?disc3.0 False (get_match r)
15:04:35 simple_ruleset ?rs \<Longrightarrow>
15:04:35 (common_matcher,
15:04:35  in_doubt_allow),?p\<turnstile> \<langle>transform_optimize_dnf_strict
15:04:35     ?rs, ?s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?t =
15:04:35 (common_matcher,
15:04:35  in_doubt_allow),?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?t
15:04:35 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics/document -o pdf -n document
15:04:35 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics/outline -o pdf -n outline -t /proof,/ML
15:04:35 *** Failed to load theory "Native_Word.Code_Target_Bits_Int" (unresolved "Native_Word.Bits_Integer")
15:04:35 *** Failed to load theory "Iptables_Semantics.Code_Interface" (unresolved "Native_Word.Code_Target_Bits_Int")
15:04:35 *** Failed to load theory "Iptables_Semantics.Parser" (unresolved "Iptables_Semantics.Code_Interface")
15:04:35 *** Failed to load theory "Iptables_Semantics.Code_haskell" (unresolved "Iptables_Semantics.Parser")
15:04:35 *** Failed to load theory "Iptables_Semantics.Documentation" (unresolved "Iptables_Semantics.Code_Interface")
15:04:35 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:04:35 *** At command "export_code" (line 630 of "$AFP/Native_Word/Bits_Integer.thy")
15:04:35 Iptables_Semantics_Examples CANCELLED
15:04:35 LOFT CANCELLED
15:04:39 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Library
15:04:39 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Library/document.pdf
15:04:39 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Library/outline.pdf
15:04:39 HOL-Library FAILED
15:04:39 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/HOL-Library)
15:04:39   :: "ereal"
15:04:39 "True"
15:04:39   :: "bool"
15:04:39 "True"
15:04:39   :: "bool"
15:04:39 "\<infinity>"
15:04:39   :: "ereal"
15:04:39 ### Rule already declared as introduction (intro)
15:04:39 ### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
15:04:39 ### rel_fun ?A ?B ?f ?g
15:04:39 "ereal (13 / 4)"
15:04:39   :: "ereal"
15:04:39 ### Ignoring duplicate rewrite rule:
15:04:39 ### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
15:04:39 ### Rule already declared as introduction (intro)
15:04:39 ### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
15:04:39 ### rel_fun ?A ?B ?f ?g
15:04:39 ### Ignoring duplicate rewrite rule:
15:04:39 ### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
15:04:39 ### Ignoring duplicate rewrite rule:
15:04:39 ### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
15:04:39 ### Ignoring duplicate rewrite rule:
15:04:39 ### ?n1 \<le> Suc (length ?kvs1) \<Longrightarrow>
15:04:39 ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \<equiv> take (?n1 - 1) ?kvs1
15:04:39 Found termination order:
15:04:39   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>
15:04:39    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"
15:04:39 Found termination order:
15:04:39   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>
15:04:39    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"
15:04:39 ### Rule already declared as introduction (intro)
15:04:39 ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
15:04:39 ### Introduced fixed type variable(s): 'd in "x__"
15:04:39 \<Sqinter> (Sup ` ?A) =
15:04:39 \<Squnion> (Inf ` {f ` ?A |f. \<forall>Y\<in>?A. f Y \<in> Y})
15:04:39 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Library/document -o pdf -n document
15:04:39 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Library/outline -o pdf -n outline -t /proof,/ML
15:04:39 *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Finite_Map")
15:04:39 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:04:39 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")
15:04:39 HOL-Computational_Algebra CANCELLED
15:04:39 HOL-Algebra CANCELLED
15:04:39 JNF-HOL-Lib CANCELLED
15:04:39 JNF-AFP-Lib CANCELLED
15:04:39 Jordan_Normal_Form CANCELLED
15:04:39 Category3 CANCELLED
15:04:39 Subresultants CANCELLED
15:04:39 Pre_BZ CANCELLED
15:04:39 Berlekamp_Zassenhaus CANCELLED
15:04:39 Jinja CANCELLED
15:04:39 HereditarilyFinite CANCELLED
15:04:39 Formula_Derivatives CANCELLED
15:04:39 Incompleteness CANCELLED
15:04:39 HOL-Decision_Procs CANCELLED
15:04:39 HOL-Nominal CANCELLED
15:04:39 HOL-Nominal-Examples CANCELLED
15:04:39 Groebner_Bases CANCELLED
15:04:39 Psi_Calculi CANCELLED
15:04:39 Algebraic_Numbers CANCELLED
15:04:39 MonoidalCategory CANCELLED
15:04:39 HOL-Number_Theory CANCELLED
15:04:39 HRB-Slicing CANCELLED
15:04:39 LLL_Basis_Reduction CANCELLED
15:04:39 HOL-ex CANCELLED
15:04:39 Deriving CANCELLED
15:04:39 Slicing CANCELLED
15:04:39 Linear_Recurrences_Solver CANCELLED
15:04:39 Group-Ring-Module CANCELLED
15:04:39 Containers CANCELLED
15:04:39 HOL-Codegenerator_Test CANCELLED
15:04:39 Core_DOM CANCELLED
15:04:39 HOL-Corec_Examples CANCELLED
15:04:39 Perron_Frobenius CANCELLED
15:04:39 CoreC++ CANCELLED
15:04:39 HOL-Nitpick_Examples CANCELLED
15:04:39 Datatype_Order_Generator CANCELLED
15:04:39 HOL-Auth CANCELLED
15:04:39 Isabelle_Meta_Model CANCELLED
15:04:39 Abstract-Rewriting CANCELLED
15:04:39 Containers-Benchmarks CANCELLED
15:04:39 Order_Lattice_Props CANCELLED
15:04:39 Polynomials CANCELLED
15:04:39 Coinductive CANCELLED
15:04:39 KBPs CANCELLED
15:04:39 HOL-Datatype_Examples CANCELLED
15:04:40 WebAssembly CANCELLED
15:04:40 Functional_Ordered_Resolution_Prover CANCELLED
15:04:40 HOL-Quickcheck_Examples CANCELLED
15:04:40 Stable_Matching CANCELLED
15:04:40 Rep_Fin_Groups CANCELLED
15:04:40 HOL-IMP CANCELLED
15:04:40 Simplex CANCELLED
15:04:40 Vickrey_Clarke_Groves CANCELLED
15:04:40 HOL-MicroJava CANCELLED
15:04:40 Matrix CANCELLED
15:04:40 LTL CANCELLED
15:04:40 Quantales CANCELLED
15:04:40 Separation_Logic_Imperative_HOL CANCELLED
15:04:40 Password_Authentication_Protocol CANCELLED
15:04:40 Buildings CANCELLED
15:04:40 List-Infinite CANCELLED
15:04:40 Signature_Groebner CANCELLED
15:04:40 Matrix_Tensor CANCELLED
15:04:40 Nat-Interval-Logic CANCELLED
15:04:40 HOL-Predicate_Compile_Examples CANCELLED
15:04:40 HOL-Bali CANCELLED
15:04:40 HOL-Cardinals CANCELLED
15:04:40 Symmetric_Polynomials CANCELLED
15:04:40 Splay_Tree CANCELLED
15:04:40 Root_Balanced_Tree CANCELLED
15:04:40 Abs_Int_ITP2012 CANCELLED
15:04:40 LTL_to_DRA CANCELLED
15:04:40 UTP-Toolkit CANCELLED
15:04:40 Twelvefold_Way CANCELLED
15:04:40 Amortized_Complexity CANCELLED
15:04:40 Regular-Sets CANCELLED
15:04:40 Sturm_Sequences CANCELLED
15:04:40 Elliptic_Curves_Group_Law CANCELLED
15:04:40 Sort_Encodings CANCELLED
15:04:40 Pre_Polynomial_Factorization CANCELLED
15:04:40 HOL-Imperative_HOL CANCELLED
15:04:40 Pi_Calculus CANCELLED
15:04:40 SATSolverVerification CANCELLED
15:04:40 Bertrands_Postulate CANCELLED
15:04:40 LightweightJava CANCELLED
15:04:40 LinearQuantifierElim CANCELLED
15:04:40 Knot_Theory CANCELLED
15:04:40 AutoFocus-Stream CANCELLED
15:04:40 HOL-SET_Protocol CANCELLED
15:04:40 Ordered_Resolution_Prover CANCELLED
15:04:40 HOL-Quotient_Examples CANCELLED
15:04:40 Polynomial_Factorization CANCELLED
15:04:40 Koenigsberg_Friendship CANCELLED
15:04:40 LLL_Factorization CANCELLED
15:04:40 UTP CANCELLED
15:04:40 HOL-UNITY CANCELLED
15:04:40 SequentInvertibility CANCELLED
15:04:40 Valuation CANCELLED
15:04:40 Graph_Theory CANCELLED
15:04:40 DynamicArchitectures CANCELLED
15:04:40 Formula_Derivatives-Examples CANCELLED
15:04:40 SuperCalc CANCELLED
15:04:40 Incredible_Proof_Machine CANCELLED
15:04:40 Localization_Ring CANCELLED
15:04:40 VectorSpace CANCELLED
15:04:40 Graph_Saturation CANCELLED
15:04:40 Special_Function_Bounds CANCELLED
15:04:40 Myhill-Nerode CANCELLED
15:04:40 Farkas CANCELLED
15:04:40 HOL-Metis_Examples CANCELLED
15:04:40 Trie CANCELLED
15:04:40 Architectural_Design_Patterns CANCELLED
15:04:40 Well_Quasi_Orders CANCELLED
15:04:40 Presburger-Automata CANCELLED
15:04:40 Lambda_Free_EPO CANCELLED
15:04:40 Abstract_Completeness CANCELLED
15:04:40 ConcurrentIMP CANCELLED
15:04:40 Budan_Fourier CANCELLED
15:04:40 Priority_Queue_Braun CANCELLED
15:04:40 XML CANCELLED
15:04:40 Show CANCELLED
15:04:40 FOL-Fitting CANCELLED
15:04:40 Program-Conflict-Analysis CANCELLED
15:04:40 POPLmark-deBruijn CANCELLED
15:04:40 Sturm_Tarski CANCELLED
15:04:40 Boolean_Expression_Checkers CANCELLED
15:04:40 Posix-Lexing CANCELLED
15:04:40 Finger-Trees CANCELLED
15:04:40 Ribbon_Proofs CANCELLED
15:04:40 Binomial-Heaps CANCELLED
15:04:40 Decreasing-Diagrams CANCELLED
15:04:40 Minsky_Machines CANCELLED
15:04:40 InformationFlowSlicing_Inter CANCELLED
15:04:40 Polynomial_Interpolation CANCELLED
15:04:40 Stream_Fusion_Code CANCELLED
15:04:40 Functional-Automata CANCELLED
15:04:40 RSAPSS CANCELLED
15:04:40 Abstract_Soundness CANCELLED
15:04:40 CCS CANCELLED
15:04:40 HOL-Induct CANCELLED
15:04:40 Decreasing-Diagrams-II CANCELLED
15:04:40 Pell CANCELLED
15:04:40 Old_Datatype_Show CANCELLED
15:04:40 Category2 CANCELLED
15:04:40 HOL-Nonstandard_Analysis CANCELLED
15:04:40 Pratt_Certificate CANCELLED
15:04:40 Jordan_Hoelder CANCELLED
15:04:40 Orbit_Stabiliser CANCELLED
15:04:40 Fermat3_4 CANCELLED
15:04:40 Lambda_Free_RPOs CANCELLED
15:04:40 Separata CANCELLED
15:04:40 HyperCTL CANCELLED
15:04:40 Bell_Numbers_Spivey CANCELLED
15:04:40 Lam-ml-Normalization CANCELLED
15:04:40 Transformer_Semantics CANCELLED
15:04:40 Efficient-Mergesort CANCELLED
15:04:40 Landau_Symbols CANCELLED
15:04:40 Integration CANCELLED
15:04:40 HOL-Matrix_LP CANCELLED
15:04:40 Selection_Heap_Sort CANCELLED
15:04:40 HOL-TPTP CANCELLED
15:04:40 First_Order_Terms CANCELLED
15:04:40 InformationFlowSlicing CANCELLED
15:04:40 HOL-Unix CANCELLED
15:04:40 Epistemic_Logic CANCELLED
15:04:40 SumSquares CANCELLED
15:04:40 Dynamic_Tables CANCELLED
15:04:40 Topology CANCELLED
15:04:40 Tail_Recursive_Functions CANCELLED
15:04:40 ShortestPath CANCELLED
15:04:40 Stuttering_Equivalence CANCELLED
15:04:40 MuchAdoAboutTwo CANCELLED
15:04:40 Imperative_Insertion_Sort CANCELLED
15:04:40 TortoiseHare CANCELLED
15:04:40 HOL-Isar_Examples CANCELLED
15:04:40 Secondary_Sylow CANCELLED
15:04:40 HOL-Hahn_Banach CANCELLED
15:04:40 Falling_Factorial_Sum CANCELLED
15:04:40 Pairing_Heap CANCELLED
15:04:40 HOL-ZF CANCELLED
15:04:40 Card_Number_Partitions CANCELLED
15:04:40 Mason_Stothers CANCELLED
15:04:40 Surprise_Paradox CANCELLED
15:04:40 HOL-Nonstandard_Analysis-Examples CANCELLED
15:04:40 Lazy-Lists-II CANCELLED
15:04:40 Descartes_Sign_Rule CANCELLED
15:04:40 Skew_Heap CANCELLED
15:04:40 Perfect-Number-Thm CANCELLED
15:04:40 Liouville_Numbers CANCELLED
15:04:40 Lehmer CANCELLED
15:04:40 HOL-Mutabelle CANCELLED
15:04:40 Card_Equiv_Relations CANCELLED
15:04:40 Ordinals_and_Cardinals CANCELLED
15:04:42 CakeML: theory CakeML.Big_Step_Determ
15:04:42 CakeML: theory CakeML.Big_Step_Total
15:04:42 CakeML: theory CakeML.Big_Step_Clocked
15:04:43 CakeML: theory CakeML.Big_Step_Unclocked
15:04:44 CakeML: theory CakeML.Evaluate_Termination
15:04:45 CakeML: theory CakeML.Evaluate_Clock
15:04:45 CakeML: theory CakeML.Big_Step_Fun_Equiv
15:04:45 CakeML: theory CakeML.TypeSystemAuxiliary
15:04:45 CakeML: theory CakeML.Evaluate_Single
15:04:46 CakeML: theory CakeML.Matching
15:04:47 CakeML: theory CakeML.Big_Step_Unclocked_Single
15:04:54 CakeML: theory CakeML.CakeML_Code
15:05:06 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic
15:05:06 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/document.pdf
15:05:06 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/outline.pdf
15:05:06 Affine_Arithmetic FAILED
15:05:06 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Affine_Arithmetic)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
15:05:06 ### \<Longrightarrow> closed (\<Union> (?B ` ?A))
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### closed ?S \<Longrightarrow> open (- ?S)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### open ?S \<Longrightarrow> closed (- ?S)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### continuous_on ?s (linepath ?a ?b)
15:05:06 ### Rule already declared as introduction (intro)
15:05:06 ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
15:05:06 ### continuous_on UNIV ?f
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3"
15:05:06 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/outline -o pdf -n outline -t /proof,/ML
15:05:06 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/document -o pdf -n document
15:05:06 *** Failed to load theory "Native_Word.Uint32" (unresolved "Native_Word.Bits_Integer")
15:05:06 *** Failed to load theory "Collections.HashCode" (unresolved "Native_Word.Uint32")
15:05:06 *** Failed to load theory "Deriving.Hash_Generator" (unresolved "Collections.HashCode")
15:05:06 *** Failed to load theory "Deriving.Hash_Instances" (unresolved "Deriving.Hash_Generator")
15:05:06 *** Failed to load theory "Deriving.Derive" (unresolved "Deriving.Hash_Instances")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Straight_Line_Program" (unresolved "Deriving.Derive")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Affine_Approximation" (unresolved "Affine_Arithmetic.Straight_Line_Program")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Affine_Code" (unresolved "Affine_Arithmetic.Affine_Approximation")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Print" (unresolved "Affine_Arithmetic.Affine_Code")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Ex_Affine_Approximation" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Ex_Ineqs" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Ex_Inter" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:06 *** Failed to load theory "Affine_Arithmetic.Affine_Arithmetic" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Ex_Affine_Approximation", "Affine_Arithmetic.Ex_Ineqs", "Affine_Arithmetic.Ex_Inter", "Affine_Arithmetic.Straight_Line_Program")
15:05:06 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:05:06 *** At command "export_code" (line 630 of "$AFP/Native_Word/Bits_Integer.thy")
15:05:06 Taylor_Models CANCELLED
15:05:37 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics
15:05:37 HOL-ODE-Numerics FAILED
15:05:37 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/HOL-ODE-Numerics)
15:05:37 *** Failed to load theory "Affine_Arithmetic.Print" (unresolved "Affine_Arithmetic.Affine_Code")
15:05:37 *** Failed to load theory "Affine_Arithmetic.Ex_Affine_Approximation" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:37 *** Failed to load theory "Affine_Arithmetic.Ex_Ineqs" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:37 *** Failed to load theory "Affine_Arithmetic.Ex_Inter" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Print")
15:05:37 *** Failed to load theory "Affine_Arithmetic.Affine_Arithmetic" (unresolved "Affine_Arithmetic.Affine_Code", "Affine_Arithmetic.Ex_Affine_Approximation", "Affine_Arithmetic.Ex_Ineqs", "Affine_Arithmetic.Ex_Inter", "Affine_Arithmetic.Straight_Line_Program")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.GenCF_No_Comp" (unresolved "Collections.Code_Target_ICF", "Collections.Gen_Hash", "Collections.Impl_Array_Hash_Map", "Collections.Impl_Array_Map", "Collections.Impl_Array_Stack", "Collections.Impl_Bit_Set", "Collections.Impl_Uv_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Dflt_No_Comp" (unresolved "Collections.Code_Target_ICF", "HOL-ODE-Numerics.GenCF_No_Comp")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Autoref_Misc" (unresolved "HOL-ODE-Numerics.Refine_Dflt_No_Comp")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Folds" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_String" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Weak_Set" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Parallel" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Weak_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Enclosure_Operations" (unresolved "Affine_Arithmetic.Print", "HOL-ODE-Numerics.Autoref_Misc")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Default" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Unions" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Intersection" (unresolved "HOL-ODE-Numerics.Refine_Unions")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Invar" (unresolved "HOL-ODE-Numerics.Refine_Intersection", "HOL-ODE-Numerics.Refine_Unions")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Phantom" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Refine_Unions")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Vector_List" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Info" (unresolved "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" (unresolved "HOL-ODE-Numerics.Refine_Vector_List")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Hyperplane" (unresolved "Affine_Arithmetic.Print", "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Refine_Vector_List")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Interval" (unresolved "HOL-ODE-Numerics.Refine_Hyperplane", "HOL-ODE-Numerics.Refine_Invar", "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Abstract_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Refine_Hyperplane", "HOL-ODE-Numerics.Refine_Info", "HOL-ODE-Numerics.Refine_Interval", "HOL-ODE-Numerics.Refine_Invar", "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis" (unresolved "Affine_Arithmetic.Affine_Arithmetic", "HOL-ODE-Numerics.Abstract_Rigorous_Numerics", "HOL-ODE-Numerics.Refine_Folds", "HOL-ODE-Numerics.Refine_String")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Refine_Default", "HOL-ODE-Numerics.Refine_Parallel", "HOL-ODE-Numerics.Refine_Phantom", "HOL-ODE-Numerics.Weak_Set")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Concrete_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Abstract_Rigorous_Numerics")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Concrete_Rigorous_Numerics")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1", "HOL-ODE-Numerics.Concrete_Reachability_Analysis")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Abstract_Rigorous_Numerics")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Refine_Rigorous_Numerics")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Reachability_Analysis")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Rigorous_Numerics")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Init_ODE_Solver" (unresolved "HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.Example_Utilities" (unresolved "HOL-ODE-Numerics.Init_ODE_Solver")
15:05:37 *** Failed to load theory "HOL-ODE-Numerics.ODE_Numerics" (unresolved "Affine_Arithmetic.Print", "HOL-ODE-Numerics.Example_Utilities", "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector")
15:05:37 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:05:37 *** At command "export_code" (line 1067 of "$AFP/Collections/Lib/Diff_Array.thy")
15:05:37 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:05:37 *** At command "export_code" (line 630 of "$AFP/Native_Word/Bits_Integer.thy")
15:05:37 Lorenz_Approximation CANCELLED
15:05:37 Lorenz_C0 CANCELLED
15:05:37 HOL-ODE-ARCH-COMP CANCELLED
15:05:37 HOL-ODE-Examples CANCELLED
15:05:37 Lorenz_C1 CANCELLED
15:08:27 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML
15:08:27 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML/document.pdf
15:08:27 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML/outline.pdf
15:08:27 CakeML FAILED
15:08:27 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/CakeML)
15:08:27 ### Metis: Unused theorems: "local.evaluate_iff_1", "local.evaluate_iff_3"
15:08:27 ### Metis: Unused theorems: "local.evaluate_iff_sym_2", "local.evaluate_iff_sym_3"
15:08:27 ### Metis: Unused theorems: "local.evaluate_iff_sym_2", "local.evaluate_iff_sym_3"
15:08:27 ### Metis: Unused theorems: "local.evaluate_iff_2", "local.evaluate_iff_3"
15:08:27 ### Metis: Unused theorems: "local.evaluate_iff_1", "local.evaluate_iff_2"
15:08:27 ### Metis: Unused theorems: "Big_Step_Fun_Equiv.fun_evaluate_1"
15:08:27 ### Metis: Unused theorems: "Big_Step_Unclocked_Single.unclocked_single_complete_1"
15:08:27 ### Metis: Unused theorems: "Big_Step_Unclocked.unclocked_determ_1"
15:08:27 \<lbrakk>evaluate ?ck ?env ?s ?e ?r3.0;
15:08:27  clock ?s = ?count + ?extra3.0 \<and>
15:08:27  ?r3.0 = (?s', ?r') \<and>
15:08:27  clock ?s' = ?count' + ?extra3.0 \<and> ?ck = True\<rbrakk>
15:08:27 \<Longrightarrow> evaluate True ?env (update_clock (\<lambda>_. ?count) ?s)
15:08:27                    ?e (update_clock (\<lambda>_. ?count') ?s', ?r')
15:08:27 "(make_state 0 []
15:08:27    (make_ffi_state (\<lambda>_ _ _ _. Oracle_fail) () None [])
15:08:27    {TypeId (Short ''option''), TypeId (Short ''list''),
15:08:27     TypeId (Short ''bool''), TypeExn (Short ''Subscript''),
15:08:27     TypeExn (Short ''Div''), TypeExn (Short ''Chr''),
15:08:27     TypeExn (Short ''Bind'')}
15:08:27    {},
15:08:27   make_sem_env (Bind [] [])
15:08:27    (Bind
15:08:27      [(''SOME'', 1, TypeId (Short ''option'')),
15:08:27       (''NONE'', 0, TypeId (Short ''option'')),
15:08:27       (''::'', 2, TypeId (Short ''list'')),
15:08:27       (''nil'', 0, TypeId (Short ''list'')),
15:08:27       (''true'', 0, TypeId (Short ''bool'')),
15:08:27       (''false'', 0, TypeId (Short ''bool'')),
15:08:27       (''Subscript'', 0, TypeExn (Short ''Subscript'')),
15:08:27       (''Div'', 0, TypeExn (Short ''Div'')),
15:08:27       (''Chr'', 0, TypeExn (Short ''Chr'')),
15:08:27       (''Bind'', 0, TypeExn (Short ''Bind''))]
15:08:27      []))"
15:08:27   :: "unit state \<times> v sem_env"
15:08:27 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML/document -o pdf -n document
15:08:27 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML/outline -o pdf -n outline -t /proof,/ML
15:08:27 *** Failed to load theory "CakeML.Semantics" (unresolved "HOL-Library.Finite_Map")
15:08:27 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
15:08:27 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")
15:08:27 Unfinished session(s): Abs_Int_ITP2012, Abstract-Rewriting, Abstract_Completeness, Abstract_Soundness, Affine_Arithmetic, Algebraic_Numbers, Amortized_Complexity, Applicative_Lifting, Architectural_Design_Patterns, AutoFocus-Stream, Bell_Numbers_Spivey, Berlekamp_Zassenhaus, Bertrands_Postulate, Binomial-Heaps, Boolean_Expression_Checkers, Buchi_Complementation, Budan_Fourier, Buffons_Needle, Buildings, CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker, CAVA_Setup, CCS, CakeML, Card_Equiv_Relations, Card_Number_Partitions, Category2, Category3, Coinductive, Collections, Collections_Examples, ConcurrentIMP, Constructive_Cryptography, Containers, Containers-Benchmarks, CoreC++, Core_DOM, CryptHOL, DFS_Framework, Datatype_Order_Generator, Decreasing-Diagrams, Decreasing-Diagrams-II, Deep_Learning, Density_Compiler, Deriving, Descartes_Sign_Rule, Dijkstra_Shortest_Path, DiscretePricing, DynamicArchitectures, Dynamic_Tables, EdmondsKarp_Maxflow, Efficient-Mergesort, Elliptic_Curves_Group_Law, Epistemic_Logic, Ergodic_Theory, FOL-Fitting, Factored_Transition_System_Bounding, Falling_Factorial_Sum, Farkas, Fermat3_4, Finger-Trees, First_Order_Terms, Fisher_Yates, Flow_Networks, Floyd_Warshall, Formal_SSA, Formula_Derivatives, Formula_Derivatives-Examples, Functional-Automata, Functional_Ordered_Resolution_Prover, Gabow_SCC, Game_Based_Crypto, Girth_Chromatic, Graph_Saturation, Graph_Theory, Groebner_Bases, Group-Ring-Module, HOL-Algebra, HOL-Auth, HOL-Bali, HOL-Cardinals, HOL-Codegenerator_Test, HOL-Computational_Algebra, HOL-Corec_Examples, HOL-Datatype_Examples, HOL-Decision_Procs, HOL-Hahn_Banach, HOL-IMP, HOL-Imperative_HOL, HOL-Induct, HOL-Isar_Examples, HOL-Library, HOL-Matrix_LP, HOL-Metis_Examples, HOL-MicroJava, HOL-Mutabelle, HOL-Nitpick_Examples, HOL-Nominal, HOL-Nominal-Examples, HOL-Nonstandard_Analysis, HOL-Nonstandard_Analysis-Examples, HOL-Number_Theory, HOL-ODE-ARCH-COMP, HOL-ODE-Examples, HOL-ODE-Numerics, HOL-Predicate_Compile_Examples, HOL-Probability, HOL-Probability-ex, HOL-Quickcheck_Examples, HOL-Quotient_Examples, HOL-SET_Protocol, HOL-TPTP, HOL-UNITY, HOL-Unix, HOL-ZF, HOL-ex, HRB-Slicing, HereditarilyFinite, Hidden_Markov_Models, Higher_Order_Terms, HyperCTL, Imperative_Insertion_Sort, Incompleteness, Incredible_Proof_Machine, InformationFlowSlicing, InformationFlowSlicing_Inter, Integration, Iptables_Semantics, Iptables_Semantics_Examples, Isabelle_Meta_Model, JNF-AFP-Lib, JNF-HOL-Lib, Jinja, Jordan_Hoelder, Jordan_Normal_Form, KBPs, Knot_Theory, Knuth_Morris_Pratt, Koenigsberg_Friendship, Kruskal, LLL_Basis_Reduction, LLL_Factorization, LOFT, LTL, LTL_to_DRA, LTL_to_GBA, Lam-ml-Normalization, Lambda_Free_EPO, Lambda_Free_RPOs, Landau_Symbols, Lazy-Lists-II, Lehmer, LightweightJava, LinearQuantifierElim, Linear_Recurrences_Solver, Liouville_Numbers, List-Infinite, List_Update, Localization_Ring, Lorenz_Approximation, Lorenz_C0, Lorenz_C1, Lp, MFMC_Countable, Markov_Models, Mason_Stothers, Matrix, Matrix_Tensor, Minimal_SSA, Minsky_Machines, Monad_Normalisation, MonoidalCategory, Monomorphic_Monad, MuchAdoAboutTwo, Myhill-Nerode, Nat-Interval-Logic, Native_Word, Neumann_Morgenstern_Utility, Old_Datatype_Show, Orbit_Stabiliser, Order_Lattice_Props, Ordered_Resolution_Prover, Ordinals_and_Cardinals, POPLmark-deBruijn, Pairing_Heap, Partial_Order_Reduction, Password_Authentication_Protocol, Pell, Perfect-Number-Thm, Perron_Frobenius, Pi_Calculus, Polynomial_Factorization, Polynomial_Interpolation, Polynomials, Posix-Lexing, Pratt_Certificate, Pre_BZ, Pre_Polynomial_Factorization, Presburger-Automata, Priority_Queue_Braun, Probabilistic_Noninterference, Probabilistic_Prime_Tests, Probabilistic_System_Zoo, Probabilistic_System_Zoo-Non_BNFs, Probabilistic_Timed_Automata, Probabilistic_While, Program-Conflict-Analysis, Promela, Prpu_Maxflow, Psi_Calculi, Quantales, Quick_Sort_Cost, ROBDD, RSAPSS, Random_BSTs, Random_Graph_Subgraph_Threshold, Randomised_BSTs, Randomised_Social_Choice, Refine_Imperative_HOL, Regular-Sets, Rep_Fin_Groups, Ribbon_Proofs, Root_Balanced_Tree, SATSolverVerification, SDS_Impossibility, SM, SM_Base, Secondary_Sylow, Selection_Heap_Sort, Separata, Separation_Logic_Imperative_HOL, Sepref_Basic, Sepref_IICF, Sepref_Prereq, SequentInvertibility, ShortestPath, Show, Signature_Groebner, Simplex, Skew_Heap, Slicing, Sort_Encodings, Source_Coding_Theorem, Special_Function_Bounds, Splay_Tree, Stable_Matching, Stern_Brocot, Stochastic_Matrices, Stream_Fusion_Code, Sturm_Sequences, Sturm_Tarski, Stuttering_Equivalence, Subresultants, SumSquares, SuperCalc, Surprise_Paradox, Symmetric_Polynomials, Tail_Recursive_Functions, Taylor_Models, Topology, TortoiseHare, Transformer_Semantics, Transition_Systems_and_Automata, Transitive-Closure, Treaps, Tree-Automata, Trie, Twelvefold_Way, UTP, UTP-Toolkit, Valuation, VectorSpace, VerifyThis2018, Vickrey_Clarke_Groves, WebAssembly, Well_Quasi_Orders, XML
15:08:27 
15:08:27 === TIMING ===
15:08:27 
15:08:27 Group AFP: 0:20:33 elapsed time, 1:12:12 cpu time, factor 3.51
15:08:27 Group main: 0:05:17 elapsed time, 0:18:58 cpu time, factor 3.59
15:08:27 Group doc: 0:00:00 elapsed time
15:08:27 Group timing: 0:05:17 elapsed time, 0:18:58 cpu time, factor 3.59
15:08:27 Group large: 0:00:00 elapsed time
15:08:27 Group no_doc: 0:00:00 elapsed time
15:08:27 Overall: 0:08:25 elapsed time, 1:31:11 cpu time, factor 10.83
15:08:27 
15:08:27 === FAILED SESSIONS ===
15:08:27 
15:08:27 Session HOL-Matrix_LP: CANCELLED
15:08:27 Session Liouville_Numbers: CANCELLED
15:08:27 Session SM_Base: CANCELLED
15:08:27 Session Fermat3_4: CANCELLED
15:08:27 Session Random_BSTs: CANCELLED
15:08:27 Session Pell: CANCELLED
15:08:27 Session Markov_Models: CANCELLED
15:08:27 Session Stern_Brocot: CANCELLED
15:08:27 Session Taylor_Models: CANCELLED
15:08:27 Session Pi_Calculus: CANCELLED
15:08:27 Session Containers: CANCELLED
15:08:27 Session Simplex: CANCELLED
15:08:27 Session Probabilistic_Prime_Tests: CANCELLED
15:08:27 Session Integration: CANCELLED
15:08:27 Session Efficient-Mergesort: CANCELLED
15:08:27 Session Core_DOM: CANCELLED
15:08:27 Session Category3: CANCELLED
15:08:27 Session Datatype_Order_Generator: CANCELLED
15:08:27 Session Category2: CANCELLED
15:08:27 Session Regular-Sets: CANCELLED
15:08:27 Session Separation_Logic_Imperative_HOL: CANCELLED
15:08:27 Session Probabilistic_While: CANCELLED
15:08:27 Session Posix-Lexing: CANCELLED
15:08:27 Session Lazy-Lists-II: CANCELLED
15:08:27 Session Topology: CANCELLED
15:08:27 Session Subresultants: CANCELLED
15:08:27 Session Probabilistic_System_Zoo: CANCELLED
15:08:27 Session Lam-ml-Normalization: CANCELLED
15:08:27 Session HOL-Probability: FAILED 2
15:08:27 Session Abs_Int_ITP2012: CANCELLED
15:08:27 Session Factored_Transition_System_Bounding: FAILED 2
15:08:27 Session HOL-Predicate_Compile_Examples: CANCELLED
15:08:27 Session Slicing: CANCELLED
15:08:27 Session Perfect-Number-Thm: CANCELLED
15:08:27 Session CAVA_Setup: CANCELLED
15:08:27 Session Iptables_Semantics_Examples: CANCELLED
15:08:27 Session Perron_Frobenius: CANCELLED
15:08:27 Session HOL-Nitpick_Examples: CANCELLED
15:08:27 Session Buildings: CANCELLED
15:08:27 Session Randomised_Social_Choice: CANCELLED
15:08:27 Session Containers-Benchmarks: CANCELLED
15:08:27 Session Valuation: CANCELLED
15:08:27 Session XML: CANCELLED
15:08:27 Session EdmondsKarp_Maxflow: CANCELLED
15:08:27 Session Treaps: CANCELLED
15:08:27 Session Formula_Derivatives: CANCELLED
15:08:27 Session Nat-Interval-Logic: CANCELLED
15:08:27 Session Secondary_Sylow: CANCELLED
15:08:27 Session Quick_Sort_Cost: CANCELLED
15:08:27 Session Source_Coding_Theorem: CANCELLED
15:08:27 Session Promela: CANCELLED
15:08:27 Session Formal_SSA: CANCELLED
15:08:27 Session SM: CANCELLED
15:08:27 Session Vickrey_Clarke_Groves: CANCELLED
15:08:27 Session SequentInvertibility: CANCELLED
15:08:27 Session Trie: CANCELLED
15:08:27 Session Program-Conflict-Analysis: CANCELLED
15:08:27 Session HOL-Hahn_Banach: CANCELLED
15:08:27 Session Bell_Numbers_Spivey: CANCELLED
15:08:27 Session Decreasing-Diagrams: CANCELLED
15:08:27 Session Selection_Heap_Sort: CANCELLED
15:08:27 Session Pratt_Certificate: CANCELLED
15:08:27 Session Old_Datatype_Show: CANCELLED
15:08:27 Session Architectural_Design_Patterns: CANCELLED
15:08:27 Session Graph_Theory: CANCELLED
15:08:27 Session Abstract_Soundness: CANCELLED
15:08:27 Session Deriving: CANCELLED
15:08:27 Session Minsky_Machines: CANCELLED
15:08:27 Session Iptables_Semantics: FAILED 2
15:08:27 Session HOL-ODE-Examples: CANCELLED
15:08:27 Session Farkas: CANCELLED
15:08:27 Session Imperative_Insertion_Sort: CANCELLED
15:08:27 Session Functional_Ordered_Resolution_Prover: CANCELLED
15:08:27 Session Randomised_BSTs: CANCELLED
15:08:27 Session HOL-Induct: CANCELLED
15:08:27 Session Localization_Ring: CANCELLED
15:08:27 Session HOL-ZF: CANCELLED
15:08:27 Session Sepref_IICF: CANCELLED
15:08:27 Session HOL-Nonstandard_Analysis-Examples: CANCELLED
15:08:27 Session DFS_Framework: CANCELLED
15:08:27 Session Higher_Order_Terms: FAILED 2
15:08:27 Session List-Infinite: CANCELLED
15:08:27 Session HOL-Mutabelle: CANCELLED
15:08:27 Session Transformer_Semantics: CANCELLED
15:08:27 Session LTL_to_DRA: CANCELLED
15:08:27 Session CryptHOL: CANCELLED
15:08:27 Session Lehmer: CANCELLED
15:08:27 Session Stream_Fusion_Code: CANCELLED
15:08:27 Session Pre_BZ: CANCELLED
15:08:27 Session WebAssembly: CANCELLED
15:08:27 Session SumSquares: CANCELLED
15:08:27 Session HOL-Nominal: CANCELLED
15:08:27 Session Priority_Queue_Braun: CANCELLED
15:08:27 Session Constructive_Cryptography: CANCELLED
15:08:27 Session Sturm_Sequences: CANCELLED
15:08:27 Session LTL: CANCELLED
15:08:27 Session Coinductive: CANCELLED
15:08:27 Session Mason_Stothers: CANCELLED
15:08:27 Session HOL-Datatype_Examples: CANCELLED
15:08:27 Session Incompleteness: CANCELLED
15:08:27 Session HOL-Isar_Examples: CANCELLED
15:08:27 Session LLL_Factorization: CANCELLED
15:08:27 Session HOL-Cardinals: CANCELLED
15:08:27 Session Dijkstra_Shortest_Path: CANCELLED
15:08:27 Session Bertrands_Postulate: CANCELLED
15:08:27 Session Landau_Symbols: CANCELLED
15:08:27 Session Card_Equiv_Relations: CANCELLED
15:08:27 Session Lorenz_C0: CANCELLED
15:08:27 Session Signature_Groebner: CANCELLED
15:08:27 Session HereditarilyFinite: CANCELLED
15:08:27 Session Psi_Calculi: CANCELLED
15:08:27 Session Monomorphic_Monad: CANCELLED
15:08:27 Session Card_Number_Partitions: CANCELLED
15:08:27 Session AutoFocus-Stream: CANCELLED
15:08:27 Session Partial_Order_Reduction: CANCELLED
15:08:27 Session LightweightJava: CANCELLED
15:08:27 Session Floyd_Warshall: CANCELLED
15:08:27 Session HOL-Nominal-Examples: CANCELLED
15:08:27 Session Sort_Encodings: CANCELLED
15:08:27 Session Matrix_Tensor: CANCELLED
15:08:27 Session JNF-HOL-Lib: CANCELLED
15:08:27 Session DiscretePricing: CANCELLED
15:08:27 Session Amortized_Complexity: CANCELLED
15:08:27 Session KBPs: CANCELLED
15:08:27 Session Algebraic_Numbers: CANCELLED
15:08:27 Session Dynamic_Tables: CANCELLED
15:08:27 Session HOL-Auth: CANCELLED
15:08:27 Session Abstract-Rewriting: CANCELLED
15:08:27 Session HOL-MicroJava: CANCELLED
15:08:27 Session Collections: FAILED 2
15:08:27 Session HOL-Corec_Examples: CANCELLED
15:08:27 Session Native_Word: FAILED 2
15:08:27 Session Neumann_Morgenstern_Utility: CANCELLED
15:08:27 Session UTP-Toolkit: CANCELLED
15:08:27 Session InformationFlowSlicing_Inter: CANCELLED
15:08:27 Session Buffons_Needle: CANCELLED
15:08:27 Session HOL-Bali: CANCELLED
15:08:27 Session Sturm_Tarski: CANCELLED
15:08:27 Session LOFT: CANCELLED
15:08:27 Session Functional-Automata: CANCELLED
15:08:27 Session VectorSpace: CANCELLED
15:08:27 Session Prpu_Maxflow: CANCELLED
15:08:27 Session LinearQuantifierElim: CANCELLED
15:08:27 Session Graph_Saturation: CANCELLED
15:08:27 Session InformationFlowSlicing: CANCELLED
15:08:27 Session JNF-AFP-Lib: CANCELLED
15:08:27 Session Abstract_Completeness: CANCELLED
15:08:27 Session Password_Authentication_Protocol: CANCELLED
15:08:27 Session ShortestPath: CANCELLED
15:08:27 Session Sepref_Basic: CANCELLED
15:08:27 Session Minimal_SSA: CANCELLED
15:08:27 Session Kruskal: CANCELLED
15:08:27 Session MonoidalCategory: CANCELLED
15:08:27 Session RSAPSS: CANCELLED
15:08:27 Session HOL-UNITY: CANCELLED
15:08:27 Session Special_Function_Bounds: CANCELLED
15:08:27 Session CakeML: FAILED 2
15:08:27 Session CoreC++: CANCELLED
15:08:27 Session Gabow_SCC: CANCELLED
15:08:27 Session Hidden_Markov_Models: CANCELLED
15:08:27 Session Skew_Heap: CANCELLED
15:08:27 Session Applicative_Lifting: CANCELLED
15:08:27 Session Elliptic_Curves_Group_Law: CANCELLED
15:08:27 Session SDS_Impossibility: CANCELLED
15:08:27 Session Group-Ring-Module: CANCELLED
15:08:27 Session CCS: CANCELLED
15:08:27 Session Separata: CANCELLED
15:08:27 Session Boolean_Expression_Checkers: CANCELLED
15:08:27 Session Lambda_Free_EPO: CANCELLED
15:08:27 Session HOL-ex: CANCELLED
15:08:27 Session Pairing_Heap: CANCELLED
15:08:27 Session HOL-Quickcheck_Examples: CANCELLED
15:08:27 Session HOL-ODE-Numerics: FAILED 2
15:08:27 Session Ordered_Resolution_Prover: CANCELLED
15:08:27 Session Symmetric_Polynomials: CANCELLED
15:08:27 Session FOL-Fitting: CANCELLED
15:08:27 Session Root_Balanced_Tree: CANCELLED
15:08:27 Session UTP: CANCELLED
15:08:27 Session Density_Compiler: CANCELLED
15:08:27 Session Incredible_Proof_Machine: CANCELLED
15:08:27 Session HOL-Unix: CANCELLED
15:08:27 Session VerifyThis2018: CANCELLED
15:08:27 Session HOL-TPTP: CANCELLED
15:08:27 Session HOL-Imperative_HOL: CANCELLED
15:08:27 Session Deep_Learning: CANCELLED
15:08:27 Session Girth_Chromatic: CANCELLED
15:08:27 Session Formula_Derivatives-Examples: CANCELLED
15:08:27 Session HRB-Slicing: CANCELLED
15:08:27 Session LTL_to_GBA: CANCELLED
15:08:27 Session Jordan_Normal_Form: CANCELLED
15:08:27 Session HOL-Probability-ex: CANCELLED
15:08:27 Session HOL-Metis_Examples: CANCELLED
15:08:27 Session SATSolverVerification: CANCELLED
15:08:27 Session HOL-IMP: CANCELLED
15:08:27 Session HyperCTL: CANCELLED
15:08:27 Session DynamicArchitectures: CANCELLED
15:08:27 Session Polynomial_Interpolation: CANCELLED
15:08:27 Session Lorenz_C1: CANCELLED
15:08:27 Session Buchi_Complementation: CANCELLED
15:08:27 Session Finger-Trees: CANCELLED
15:08:27 Session Matrix: CANCELLED
15:08:27 Session ConcurrentIMP: CANCELLED
15:08:27 Session Ergodic_Theory: CANCELLED
15:08:27 Session Stochastic_Matrices: CANCELLED
15:08:27 Session Lp: CANCELLED
15:08:27 Session Orbit_Stabiliser: CANCELLED
15:08:27 Session First_Order_Terms: CANCELLED
15:08:27 Session Random_Graph_Subgraph_Threshold: CANCELLED
15:08:27 Session POPLmark-deBruijn: CANCELLED
15:08:27 Session CAVA_Base: CANCELLED
15:08:27 Session HOL-ODE-ARCH-COMP: CANCELLED
15:08:27 Session Tree-Automata: CANCELLED
15:08:27 Session Collections_Examples: CANCELLED
15:08:27 Session Order_Lattice_Props: CANCELLED
15:08:27 Session Show: CANCELLED
15:08:27 Session HOL-SET_Protocol: CANCELLED
15:08:27 Session Koenigsberg_Friendship: CANCELLED
15:08:27 Session Stable_Matching: CANCELLED
15:08:27 Session Well_Quasi_Orders: CANCELLED
15:08:27 Session Game_Based_Crypto: CANCELLED
15:08:27 Session Linear_Recurrences_Solver: CANCELLED
15:08:27 Session Ordinals_and_Cardinals: CANCELLED
15:08:27 Session HOL-Number_Theory: CANCELLED
15:08:27 Session Transition_Systems_and_Automata: CANCELLED
15:08:27 Session Knuth_Morris_Pratt: CANCELLED
15:08:27 Session Jinja: CANCELLED
15:08:27 Session Probabilistic_Noninterference: CANCELLED
15:08:27 Session Fisher_Yates: CANCELLED
15:08:27 Session HOL-Decision_Procs: CANCELLED
15:08:27 Session Rep_Fin_Groups: CANCELLED
15:08:27 Session Transitive-Closure: CANCELLED
15:08:27 Session Surprise_Paradox: CANCELLED
15:08:27 Session CAVA_LTL_Modelchecker: CANCELLED
15:08:27 Session HOL-Library: FAILED 2
15:08:27 Session Polynomial_Factorization: CANCELLED
15:08:27 Session List_Update: CANCELLED
15:08:27 Session Sepref_Prereq: CANCELLED
15:08:27 Session HOL-Codegenerator_Test: CANCELLED
15:08:27 Session MuchAdoAboutTwo: CANCELLED
15:08:27 Session Binomial-Heaps: CANCELLED
15:08:27 Session Refine_Imperative_HOL: CANCELLED
15:08:27 Session HOL-Quotient_Examples: CANCELLED
15:08:27 Session Myhill-Nerode: CANCELLED
15:08:27 Session Presburger-Automata: CANCELLED
15:08:27 Session Flow_Networks: CANCELLED
15:08:27 Session HOL-Nonstandard_Analysis: CANCELLED
15:08:27 Session Affine_Arithmetic: FAILED 2
15:08:27 Session Knot_Theory: CANCELLED
15:08:27 Session HOL-Computational_Algebra: CANCELLED
15:08:27 Session Epistemic_Logic: CANCELLED
15:08:27 Session CAVA_Automata: CANCELLED
15:08:27 Session ROBDD: CANCELLED
15:08:27 Session Berlekamp_Zassenhaus: CANCELLED
15:08:27 Session Splay_Tree: CANCELLED
15:08:27 Session Polynomials: CANCELLED
15:08:27 Session Monad_Normalisation: CANCELLED
15:08:27 Session Probabilistic_Timed_Automata: CANCELLED
15:08:27 Session HOL-Algebra: CANCELLED
15:08:27 Session Pre_Polynomial_Factorization: CANCELLED
15:08:27 Session SuperCalc: CANCELLED
15:08:27 Session Probabilistic_System_Zoo-Non_BNFs: CANCELLED
15:08:27 Session Falling_Factorial_Sum: CANCELLED
15:08:27 Session Decreasing-Diagrams-II: CANCELLED
15:08:27 Session Jordan_Hoelder: CANCELLED
15:08:27 Session LLL_Basis_Reduction: CANCELLED
15:08:27 Session MFMC_Countable: CANCELLED
15:08:27 Session Lambda_Free_RPOs: CANCELLED
15:08:27 Session Twelvefold_Way: CANCELLED
15:08:27 Session Ribbon_Proofs: CANCELLED
15:08:27 Session Lorenz_Approximation: CANCELLED
15:08:27 Session Groebner_Bases: CANCELLED
15:08:27 Session Tail_Recursive_Functions: CANCELLED
15:08:27 Session Isabelle_Meta_Model: CANCELLED
15:08:27 Session Descartes_Sign_Rule: CANCELLED
15:08:27 Session Budan_Fourier: CANCELLED
15:08:27 Session Quantales: CANCELLED
15:08:27 Session TortoiseHare: CANCELLED
15:08:27 Session Stuttering_Equivalence: CANCELLED
15:08:27 
15:08:27 === DEPENDENCIES ===
15:08:27 
15:08:27 Generating dependencies file ...
15:08:33 Writing dependencies file ...
15:08:33 
15:08:33 === REPORT ===
15:08:33 
15:08:33 Writing report file ...
15:08:33 
15:08:33 === SITEGEN ===
15:08:33 
15:08:33 Writing status file ...
15:08:33 Running sitegen ...
15:08:35 Success: Generated topics.html
15:08:35 Success: Generated index.html
15:08:35 Success: Generated html files for 466 entries
15:08:36 Success: Generated statistics.html
15:08:36 Success: Generated download.html
15:08:36 Success: Generated about.html
15:08:36 Success: Generated citing.html
15:08:36 Success: Generated updating.html
15:08:36 Success: Generated search.html
15:08:36 Success: Generated submitting.html
15:08:36 Success: Generated using.html
15:08:36 Success: Generated rss.xml
15:08:36 Success: Generated status.html
15:08:36 Checked directory thys. Found 0 warnings.
15:08:36 Packing tars ...
15:08:42 
15:08:42 === NOTIFICATIONS ===
15:08:42 
15:08:51 
15:08:51 === COMPLETED ===
15:08:51 
15:08:52 Build step 'Execute shell' marked build as failure
15:08:52 Archiving artifacts
15:12:19 Started calculate disk usage of build
15:12:20 Finished Calculation of disk usage of build in 0 seconds
15:12:29 Started calculate disk usage of workspace
15:12:30 Finished Calculation of disk usage of workspace in 0 seconds
15:12:30 No emails were triggered.
15:12:30 Finished: FAILURE