Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all [isabelle-all] $ hg showconfig paths.default [isabelle-all] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes no changes found [isabelle-all] $ hg update --clean --rev default 1 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-all] $ hg log --rev . --template {node} [isabelle-all] $ hg log --rev . --template {rev} [isabelle-all] $ hg log --rev 2c48be88f84718fa75d0e09779dba679fcb7a26d --template exists\n exists [isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(2c48be88f84718fa75d0e09779dba679fcb7a26d)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://bitbucket.org/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 469 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev 51034f90c51c656ab647f5f8bc53dfcaefab41e3 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(51034f90c51c656ab647f5f8bc53dfcaefab41e3)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-all] $ /bin/sh -xe /tmp/jenkins595160143016447298.sh + Admin/jenkins/run_build all + set -e + PROFILE=all + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup The following actions will be performed: ∗ install base-bigarray base ∗ install ocaml-base-compiler 4.05.0 [required by ocaml] ∗ install base-threads base ∗ install conf-gmp 1 ∗ install conf-perl 1 ∗ install base-unix base ∗ install conf-m4 1 ∗ install ocaml-config 1 [required by ocaml] ∗ install ocaml 4.05.0 [required by ocamlfind, zarith] ∗ install ocamlfind 1.8.0 ∗ install zarith 1.7 ===== ∗ 11 ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ocaml-base-compiler.4.05.0] found in cache [ocamlfind.1.8.0] found in cache [zarith.1.7] found in cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> ∗ installed base-bigarray.base ∗ installed base-threads.base ∗ installed base-unix.base ∗ installed conf-gmp.1 ∗ installed conf-m4.1 ∗ installed conf-perl.1 ∗ installed ocaml-base-compiler.4.05.0 ∗ installed ocaml-config.1 ∗ installed ocaml.4.05.0 ∗ installed ocamlfind.1.8.0 ∗ installed zarith.1.7 Done. # Run eval $(opam env) to update the current shell environment [NOTE] Package zarith is already installed (current version is 1.7). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.4.4 + bin/isabelle ci_build_all === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 10, threads = 4, numa = false === BUILD === Build started at Thu, 21 Mar 2019 18:54:18 GMT Isabelle id ab8aad4aa76e AFP id 51034f90c51c === LOG === Session Pure/Pure Session CTT/CTT Session Cube/Cube Session FOL/FOL Session CCL/CCL Session FOL/FOL-ex Session FOLP/FOLP Session FOLP/FOLP-ex Session HOL/HOL (main) Session AFP/AVL-Trees (AFP) Session AFP/AWN (AFP) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/AnselmGod (AFP) Session AFP/AxiomaticCategoryTheory (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/CISC-Kernel (AFP) Session AFP/CYK (AFP) Session AFP/Cauchy (AFP) Session AFP/Sqrt_Babylonian (AFP) Session Doc/Classes (doc) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Depth-First-Search (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/DiskPaxos (AFP) Session AFP/Example-Submission (AFP) Session AFP/FFT (AFP) Session AFP/FLP (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session Doc/Functions (doc) Session AFP/GPU_Kernel_PL (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (AFP) Session AFP/GoedelGod (AFP) Session HOL/HOL-Eisbach Session AFP/Allen_Calculus (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session Doc/Eisbach (doc) Session HOL/HOL-Hoare Session AFP/Case_Labeling (AFP) Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-IMPP Session HOL/HOL-IOA Session HOL/HOL-Import Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session AFP/ArrowImpossibilityGS (AFP) Session AFP/Auto2_HOL (AFP) Session AFP/BNF_CC (AFP) Session AFP/BNF_Operations (AFP) Session AFP/Binomial-Heaps (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Buildings (AFP) Session AFP/CRDT (AFP) Session AFP/IMAP-CRDT (AFP) Session AFP/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Category (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session Doc/Codegen (doc) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/CoreC++ (AFP) Session AFP/Core_DOM (AFP) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Efficient-Mergesort (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Epistemic_Logic (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/FinFun (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Graph_Saturation (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session AFP/Group-Ring-Module (AFP) Session AFP/Valuation (AFP) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Cardinals (timing) Session AFP/Ordinals_and_Cardinals (AFP) Session AFP/Sort_Encodings (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session AFP/JNF-HOL-Lib (AFP) Session AFP/Localization_Ring (AFP) Session AFP/Orbit_Stabiliser (AFP) Session AFP/Perfect-Number-Thm (AFP) Session AFP/Secondary_Sylow (AFP) Session AFP/Jordan_Hoelder (AFP) Session AFP/VectorSpace (AFP) Session HOL/HOL-Analysis (main timing) Session AFP/Bernoulli (AFP) Session AFP/Cartan_FP (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/Coinductive (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Architectural_Design_Patterns (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Topology (AFP) Session AFP/First_Welfare_Theorem (AFP) Session AFP/Green (AFP) Session HOL/HOL-Analysis-ex Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/DiscretePricing (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Gromov_Hyperbolicity (AFP) Session AFP/Fisher_Yates (AFP) Session AFP/Girth_Chromatic (AFP) Session AFP/Random_Graph_Subgraph_Threshold (AFP) Session HOL/HOL-Probability-ex (timing) Session AFP/Lp (AFP) Session AFP/Markov_Models (AFP) Session AFP/Monad_Normalisation (AFP) Session AFP/Monomorphic_Monad (AFP) Session AFP/Neumann_Morgenstern_Utility (AFP) Session AFP/Probabilistic_Noninterference (AFP) Session AFP/Probabilistic_System_Zoo (AFP) Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Octonions (AFP) Session AFP/Probabilistic_System_Zoo-BNFs (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Quaternions (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Hermite (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Isar_Examples Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Lehmer (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (AFP) Session AFP/RSAPSS (AFP) Session AFP/SumSquares (AFP) Session AFP/Liouville_Numbers (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Probabilistic_Prime_Tests (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Budan_Fourier (AFP) Session AFP/Winding_Number_Eval (AFP) Session AFP/Count_Complex_Roots (AFP) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-Hahn_Banach Session HOL/HOL-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Auto2_Imperative_HOL (AFP) Session AFP/Imperative_Insertion_Sort (AFP) Session HOL/HOL-Induct Session HOL/HOL-Matrix_LP Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mutabelle Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal Session AFP/CCS (AFP) Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/Pi_Calculus (AFP) Session AFP/Psi_Calculi (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-TPTP Session HOL/HOL-Unix Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/HyperCTL (AFP) Session AFP/Integration (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/LTL (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Lambda_Free_EPO (AFP) Session AFP/Landau_Symbols (AFP) Session AFP/Akra_Bazzi (AFP) Session AFP/Catalan_Numbers (AFP) Session AFP/Error_Function (AFP) Session AFP/Euler_MacLaurin (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/MuchAdoAboutTwo (AFP) Session AFP/Optics (AFP) Session AFP/UTP-Toolkit (AFP) Session AFP/UTP (AFP) Session AFP/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (AFP) Session AFP/Pell (AFP) Session AFP/Presburger-Automata (AFP) Session AFP/Priority_Queue_Braun (AFP) Session AFP/Program-Conflict-Analysis (AFP) Session AFP/Regular-Sets (AFP) Session AFP/Abstract-Rewriting (AFP) Session AFP/Decreasing-Diagrams (AFP) Session AFP/First_Order_Terms (AFP) Session AFP/Matrix (AFP) Session AFP/Matrix_Tensor (AFP) Session AFP/Knot_Theory (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Simplex (AFP) Session AFP/Farkas (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-Mirabelle Session HOL/HOL-Mirabelle-ex Session HOL/HOL-NanoJava Session HOL/HOL-Prolog Session HOL/HOL-Real_Asymp Session HOL/HOL-Real_Asymp-Manual Session HOL/HOL-Statespace Session HOL/HOL-TLA Session HOL/HOL-TLA-Buffer Session HOL/HOL-TLA-Inc Session HOL/HOL-TLA-Memory Session HOL/HOL-Types_To_Sets Session AFP/Smooth_Manifolds (AFP) Session HOL/HOL-Word (main timing) Session HOL/HOL-SPARK Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session HOL/HOL-SPARK-Manual Session HOL/HOL-Word-SMT_Examples (timing) Session AFP/Kleene_Algebra (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Multirelations (AFP) Session AFP/Quantales (AFP) Session AFP/Transformer_Semantics (AFP) Session AFP/Regular_Algebras (AFP) Session AFP/Relation_Algebra (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/LEM (AFP) Session AFP/Native_Word (AFP) Session AFP/WebAssembly (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/Incredible_Proof_Machine (AFP) Session AFP/Deriving (AFP) Session AFP/CAVA_Base (AFP) Session AFP/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Gabow_SCC (AFP) Session AFP/LTL_to_GBA (AFP) Session AFP/Promela (AFP) Session AFP/Containers (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/Show (AFP) Session AFP/JNF-AFP-Lib (AFP) Session AFP/Real_Impl (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/Partial_Order_Reduction (AFP) Session AFP/SM_Base (AFP) Session AFP/SM (AFP) Session AFP/CAVA_Setup (AFP) Session AFP/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (AFP) Session AFP/KBPs (AFP) Session AFP/Tree-Automata (AFP) Session AFP/SPARCv8 (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Separata (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/CakeML (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session HOL/HOLCF-Tutorial Session HOL/IOA (timing) Session HOL/IOA-ABP Session HOL/IOA-NTP Session HOL/IOA-Storage Session HOL/IOA-ex Session AFP/Shivers-CFA (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/Tycon (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hoare_Time (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Huffman (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IMP2 (AFP) Session Doc/Implementation (doc) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/InfPathElimination (AFP) Session Doc/Isar_Ref (doc) Session Doc/JEdit (doc) Session AFP/JiveDataStoreModel (AFP) Session AFP/KAD (AFP) Session AFP/Algebraic_VCs (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Taylor_Models (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Higher_Order_Terms (AFP) Session AFP/Jinja (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/LTL_to_DRA (AFP) Session AFP/List_Update (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-ARCH-COMP (AFP) Session AFP/HOL-ODE-Examples (AFP large) Session AFP/Lorenz_Approximation (AFP) Session AFP/Lorenz_C0 (AFP large) Session AFP/Lorenz_C1 (AFP large) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Random_BSTs (AFP) Session AFP/Randomised_BSTs (AFP) Session AFP/Treaps (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/Fishburn_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Sepref_IICF (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/LocalLexing (AFP) Session Doc/Locales (doc) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session Doc/Main (doc) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Matroids (AFP) Session AFP/Kruskal (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/Menger (AFP) Session AFP/MiniML (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/Monad_Memo_DP (AFP) Session AFP/Hidden_Markov_Models (AFP) Session AFP/Optimal_BST (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/Launchbury (AFP) Session AFP/Call_Arity (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Rewriting_Z (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/NormByEval (AFP) Session AFP/OpSets (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/Polynomials (AFP) Session AFP/Symmetric_Polynomials (AFP) Session AFP/Pi_Transcendental (AFP) Session AFP/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Ordered_Resolution_Prover (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Certification_Monads (AFP) Session AFP/XML (AFP) Session AFP/Pre_Polynomial_Factorization (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Deep_Learning (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Signature_Groebner (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Subresultants (AFP) Session AFP/Pre_BZ (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/LLL_Basis_Reduction (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Recurrences_Solver (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session Doc/Prog_Prove (doc) Session AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/Minsky_Machines (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Statecharts (AFP) Session AFP/Stone_Algebras (AFP) Session AFP/Stone_Relation_Algebras (AFP) Session AFP/Stone_Kleene_Relation_Algebras (AFP) Session AFP/Aggregation_Algebras (AFP) Session AFP/Store_Buffer_Reduction (AFP) Session AFP/Strong_Security (AFP) Session Doc/Sugar (doc) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Probabilistic_Timed_Automata (AFP) Session AFP/Transitive-Closure-II (AFP) Session AFP/Tree_Decomposition (AFP) Session Doc/Tutorial (doc) Session Doc/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session AFP/Weight_Balanced_Trees (AFP) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/CryptHOL (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Free-Groups (AFP) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Stern_Brocot (AFP) Session HOL/HOL-Proofs-ex Session Tools/Haskell Session Doc/Intro (doc) Session LCF/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Tools/SML Session Sequents/Sequents Session Doc/Sledgehammer (doc) Session Tools/Spec_Check Session AFP/Regex_Equivalence (AFP) Session Doc/System (doc) Session ZF/ZF (main timing) Session Doc/Logics_ZF (doc) Session ZF/ZF-AC Session ZF/ZF-Coind Session ZF/ZF-Constructible Session ZF/ZF-IMP Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Session ZF/ZF-Resid Session ZF/ZF-ex Running Smooth_Manifolds ... Running HOL-Data_Structures ... Running Valuation ... Running Verified-Prover ... Running Higher_Order_Terms ... Running Lambda_Free_EPO ... Running Lambda_Free_KBOs ... Running Lambda_Free_RPOs ... HOL-Data_Structures: theory HOL-Data_Structures.Less_False Running Functional_Ordered_Resolution_Prover ... HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs HOL-Data_Structures: theory HOL-Data_Structures.Cmp HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less HOL-Data_Structures: theory HOL-Data_Structures.Tree2 Running Noninterference_Generic_Unwinding ... HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del Smooth_Manifolds: theory HOL-Library.Function_Algebras Smooth_Manifolds: theory HOL-Library.Quotient_Syntax Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets Verified-Prover: theory Verified-Prover.Prover Smooth_Manifolds: theory HOL-Library.Quotient_Set Higher_Order_Terms: theory HOL-Library.AList Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading Higher_Order_Terms: theory HOL-Library.Nat_Bijection Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity HOL-Data_Structures: theory HOL-Data_Structures.Tree23 HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs Higher_Order_Terms: theory HOL-Library.Monad_Syntax HOL-Data_Structures: theory HOL-Data_Structures.Trie Higher_Order_Terms: theory HOL-Library.State_Monad Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs Valuation: theory Valuation.Valuation1 Lambda_Free_EPO: theory HOL-Cardinals.Order_Union Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util HOL-Data_Structures: theory HOL-Data_Structures.Tree234 Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension Higher_Order_Terms: theory HOL-Library.Old_Datatype Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension Higher_Order_Terms: theory List-Index.List_Index HOL-Data_Structures: theory HOL-Data_Structures.Isin2 Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With Higher_Order_Terms: theory HOL-Library.Countable Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders HOL-Data_Structures: theory HOL-Data_Structures.AA_Set Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On Higher_Order_Terms: theory HOL-Library.FSet Functional_Ordered_Resolution_Prover: theory Deriving.Comparator Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux HOL-Data_Structures: theory HOL-Data_Structures.Lookup2 HOL-Data_Structures: theory HOL-Data_Structures.RBT Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set HOL-Data_Structures: theory HOL-Data_Structures.AA_Map Valuation: theory Valuation.Valuation2 Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances Functional_Ordered_Resolution_Prover: theory Nested_Multisets_Ordinals.Multiset_More Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq HOL-Data_Structures: theory HOL-Library.Cancellation Functional_Ordered_Resolution_Prover: theory Deriving.Compare Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Clausal_Logic Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std HOL-Data_Structures: theory HOL-Library.Multiset Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits Lambda_Free_KBOs: theory HOL-Cardinals.Order_Union Lambda_Free_KBOs: theory Abstract-Rewriting.Seq Lambda_Free_KBOs: theory HOL-Library.While_Combinator Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Util Lambda_Free_KBOs: theory HOL-Cardinals.Wellorder_Extension Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Bit Lambda_Free_KBOs: theory Matrix.Utility Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Numeric Lambda_Free_KBOs: theory Regular-Sets.Regular_Set Functional_Ordered_Resolution_Prover: theory HOL-Word.Bit_Representation Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Herbrand_Interpretation Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ground_Resolution_Model Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim Lambda_Free_KBOs: theory Lambda_Free_RPOs.Infinite_Chain Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_KBOs: theory Lambda_Free_RPOs.Extension_Orders Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Inference_System Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Int Functional_Ordered_Resolution_Prover: theory HOL-Word.Word_Miscellaneous Valuation: theory Valuation.Valuation3 Lambda_Free_EPO: theory Lambda_Free_EPO.Chop Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Typedef Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_Nat Higher_Order_Terms: theory HOL-Library.Finite_Map Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO HOL-Data_Structures: theory HOL-Library.Pattern_Aliases Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/outline.pdf Verified-Prover FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Verified-Prover) *** FEval (gs, g) e (NAtom p vs)\ *** \ FEval (gs, g) e (snd a) \ *** (\f\set list. FEval (gs, g) e (snd f)) *** 2. \n t gs g e a list p vs. *** \init s; finite (deriv s); m \ fst ` deriv s; *** \y. *** (\u. (y, u) \ deriv s) \ y \ m; *** (m, a # list) \ deriv s; n = m; is_env (gs, g) e; t = a # list; *** snd a = PAtom p vs; NAtom p vs \ snd ` set list\ *** \ FEval (gs, g) e (PAtom p vs) \ *** FEval (gs, g) e (NAtom p vs) *** 3. \n t gs g e a list. *** \init s; finite (deriv s); m \ fst ` deriv s; *** \y. *** (\u. (y, u) \ deriv s) \ y \ m; *** (m, a # list) \ deriv s; n = m; is_env (gs, g) e; t = a # list; *** \p vs. *** snd a = NAtom p vs \ *** PAtom p vs \ snd ` set list\ *** \ FEval (gs, g) e (snd a) \ *** (\f\set list. FEval (gs, g) e (snd f)) *** 4. \n t gs g e. *** \init s; finite (deriv s); m \ fst ` deriv s; *** \y. *** (\u. (y, u) \ deriv s) \ y \ m; *** (m, t) \ deriv s; n = m; is_env (gs, g) e; *** \ is_axiom (s_of_ns t)\ *** \ \f. *** f \ set (s_of_ns t) \ FEval (gs, g) e f *** 5. \n. *** \init s; finite (deriv s); m \ fst ` deriv s; *** \y u. (y, u) \ deriv s \ y \ m; *** \na t. *** n = m - na \ (na, t) \ deriv s \ *** Svalid (s_of_ns t)\ *** \ \na t. *** Suc n = m - na \ *** (na, t) \ deriv s \ *** Svalid (s_of_ns t) *** At command "apply" (line 609 of "$AFP/Verified-Prover/Prover.thy") Functional_Ordered_Resolution_Prover: theory Matrix.Utility HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS HOL-Data_Structures: theory HOL-Library.Tree Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ordered_Ground_Resolution Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_List Functional_Ordered_Resolution_Prover: theory HOL-Word.Bool_List_Representation Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates Lambda_Free_KBOs: theory Regular-Sets.Regular_Exp Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Map2 Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Abstract_Substitution Functional_Ordered_Resolution_Prover: theory Native_Word.More_Bits_Int Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Encoding HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set Functional_Ordered_Resolution_Prover: theory HOL-Word.Word HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap Lambda_Free_KBOs: theory Regular-Sets.NDerivative Lambda_Free_KBOs: theory Regular-Sets.Relation_Interpretation Functional_Ordered_Resolution_Prover: theory Native_Word.Bits_Integer HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline.pdf Lambda_Free_RPOs FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_RPOs) assumes "rpo_optim ground_heads_var (>\<^sub>s) extf arity_sym arity_var" Proofs for inductive predicate(s) "gt" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale rpo fixes ground_heads_var :: "'v \ 's set" and gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var" ### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim" ### 0.466s elapsed time, 1.864s cpu time, 0.000s GC time Loading theory "Lambda_Free_RPOs.Lambda_Free_RPOs" locale simple_rpo_instances ### theory "Lambda_Free_RPOs.Lambda_Free_RPOs" ### 0.864s elapsed time, 3.432s cpu time, 0.204s GC time isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set Lambda_Free_KBOs: theory Regular-Sets.Equivalence_Checking Smooth_Manifolds: theory Smooth_Manifolds.Smooth Smooth_Manifolds: theory Smooth_Manifolds.Chart Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp Lambda_Free_KBOs: theory Regular-Sets.Regexp_Method Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold Lambda_Free_KBOs: theory Abstract-Rewriting.Abstract_Rewriting Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Liminf Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Chain Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Misc HOL-Data_Structures: theory HOL-Data_Structures.Sorting HOL-Data_Structures: theory HOL-Library.Tree_Real Lambda_Free_KBOs: theory Abstract-Rewriting.SN_Orders HOL-Data_Structures: theory HOL-Data_Structures.Balance Higher_Order_Terms: theory Higher_Order_Terms.Term_Utils Higher_Order_Terms: theory Higher_Order_Terms.Disjoint_Sets Higher_Order_Terms: theory Higher_Order_Terms.Find_First Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space Smooth_Manifolds: theory Smooth_Manifolds.Sphere HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map Higher_Order_Terms: theory Deriving.Derive_Manager Higher_Order_Terms: theory HOL-Library.Cancellation Higher_Order_Terms: theory HOL-Library.Infinite_Set Higher_Order_Terms: theory HOL-ex.Unification Higher_Order_Terms: theory Datatype_Order_Generator.Derive_Aux Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space Higher_Order_Terms: theory Datatype_Order_Generator.Order_Generator HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT Higher_Order_Terms: theory HOL-Library.Countable_Set Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Monad Higher_Order_Terms: theory HOL-Library.Multiset Higher_Order_Terms: theory Higher_Order_Terms.Name Higher_Order_Terms: theory HOL-Library.Countable_Complete_Lattices Lambda_Free_KBOs: theory Polynomials.Polynomials HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding Noninterference_Generic_Unwinding FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Noninterference_Generic_Unwinding) Loading theory "Noninterference_Generic_Unwinding.GenericUnwinding" Proofs for inductive predicate(s) "rel_induct_auxp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... *** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (ys @ [y']) \ {} *** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") *** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (zs @ [z]) \ {} *** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") ### theory "Noninterference_Generic_Unwinding.GenericUnwinding" ### 1.837s elapsed time, 4.632s cpu time, 0.132s GC time isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/document -o pdf -n document *** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline" *** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (zs @ [z]) \ {} *** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") *** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (ys @ [y']) \ {} *** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Class HOL-Data_Structures: theory HOL-Number_Theory.Fib HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set Higher_Order_Terms: theory Higher_Order_Terms.Term_Class Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline.pdf Lambda_Free_EPO FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_EPO) Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_chop" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_diff" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_same" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Lambda_Free_EPO.Lambda_Free_EPO" ### 1.040s elapsed time, 3.800s cpu time, 0.160s GC time \?X \ ?C; ?A \ ?X\ \ ?A \ \ ?C ?P ?a \ ?a \ {x. ?P x} isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking Higher_Order_Terms: theory HOL-Library.Order_Continuity HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method Higher_Order_Terms: theory HOL-Library.Extended_Nat Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32 Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Proving_Process Higher_Order_Terms: theory HOL-Library.Multiset_Order Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Util Functional_Ordered_Resolution_Prover: theory Collections.HashCode Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Standard_Redundancy Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching Functional_Ordered_Resolution_Prover: theory Deriving.Derive Higher_Order_Terms: theory Higher_Order_Terms.Nterm Higher_Order_Terms: theory Higher_Order_Terms.Term Higher_Order_Terms: theory Higher_Order_Terms.Unification_Compat Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Encoding_KBO Higher_Order_Terms: theory Higher_Order_Terms.Pats Higher_Order_Terms: theory Higher_Order_Terms.Lambda_Free_Compat Higher_Order_Terms: theory Higher_Order_Terms.Term_to_Nterm Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/outline.pdf Valuation FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Valuation) ### ("_applC" ("_position" K) ("_position" P)) ("_position" j)) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### an 0 \ 0 \Ring K; b\<^bsup>\ K\<^esup> \ carrier K; ?y \ carrier K; ?z \ carrier K\ \ (?y \ ?z) \\<^sub>r b\<^bsup>\ K\<^esup> = ?y \\<^sub>r b\<^bsup>\ K\<^esup> \ ?z \\<^sub>r b\<^bsup>\ K\<^esup> isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Valuation/document -o pdf -n document *** Failed to apply proof method (line 899 of "$AFP/Valuation/Valuation1.thy"): *** goal (1 subgoal): *** 1. \x. *** \valuation K v; \x\carrier K. 0 < v x; *** {x \ v ` carrier K. 0 < x} \ LBset 1; *** AMin {x \ v ` carrier K. 0 < x} \ v ` carrier K \ *** 0 < AMin {x \ v ` carrier K. 0 < x}; *** \x. *** x \ v ` carrier K \ 0 < x \ *** AMin {x \ v ` carrier K. 0 < x} \ x; *** x \ carrier K; v x \ \; v x \ 0; *** 0 < v x\ *** \ \a. *** AMin {x \ v ` carrier K. 0 < x} = ant a *** At command "apply" (line 899 of "$AFP/Valuation/Valuation1.thy") *** Failed to apply proof method (line 947 of "$AFP/Valuation/Valuation1.thy"): *** goal (1 subgoal): *** 1. valuation K v \ *** \w\carrier K - {\}. *** \z. v w = z *\<^sub>a AMin {x \ v ` carrier K. 0 < x} *** At command "apply" (line 947 of "$AFP/Valuation/Valuation1.thy") *** Failed to apply proof method (line 837 of "$AFP/Valuation/Valuation1.thy"): *** goal (1 subgoal): *** 1. valuation K v \ *** {x \ v ` carrier K. 0 < x} \ {} *** At command "apply" (line 837 of "$AFP/Valuation/Valuation1.thy") Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline.pdf Higher_Order_Terms FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Higher_Order_Terms) ### Introduced fixed type variable(s): 'd, 'e in "f__" ### Introduced fixed type variable(s): 'd in "X__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__" ### Introduced fixed type variable(s): 'd, 'e in "R__" ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Introduced fixed type variable(s): 'd in "z__" ### Introduced fixed type variable(s): 'd in "P__" *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") ### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_2" ### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_1" ### Rule already declared as introduction (intro) ### \rel_option ?R ?x ?y; ### \a b. ?R a b \ rel_option ?R (?f a) (?g b)\ ### \ rel_option ?R (?x \ ?f) (?y \ ?g) isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline.pdf Lambda_Free_KBOs FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_KBOs) Proving the simplification rules ... Proofs for inductive predicate(s) "gt_diff" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_same" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... consts subst_zpassign :: "('v \ ('s, 'v) tm) \ ('v pvar \ zhmultiset) \ 'v pvar \ zhmultiset" ### theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs" ### 3.647s elapsed time, 7.600s cpu time, 0.560s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBOs" locale simple_kbo_instances ### theory "Lambda_Free_KBOs.Lambda_Free_KBOs" ### 1.358s elapsed time, 2.720s cpu time, 0.000s GC time Found termination order: "size <*mlex*> {}" "(>\<^sub>h\<^sub>d)" :: "('s, 'v) hd \ ('s, 'v) hd \ bool" isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline.pdf Functional_Ordered_Resolution_Prover FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Functional_Ordered_Resolution_Prover) compare_order: register types in class compare_order, options: (linorder) or () countable: register datatypes is class countable equality: generate an equality function, options are () and (eq) hash_code: generate a hash function, options are () and (hashcode) hashable: register types in class hashable linorder: register types in class linorder, options: (linorder) or () *** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy") ### Ignoring duplicate rewrite rule: ### mset (filter ?P1 ?xs1) \ filter_mset ?P1 (mset ?xs1) Testing conjecture with Quickcheck-narrowing... [1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Data_Bits.hs.o ) [2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Typerep.hs.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Typerep.hs.o ) [3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Generated_Code.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Generated_Code.o ) [4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Narrowing_Engine.o ) [5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Main.hs, /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/Main.o ) Linking /tmp/isabelle-jenkins/process2927976256498384663/Quickcheck_Narrowing4614918/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document -o pdf -n document *** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy") HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map Timing HOL-Data_Structures (4 threads, 273.732s elapsed time, 971.180s cpu time, 38.072s GC time, factor 3.55) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Data_Structures Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Data_Structures/document.pdf Finished HOL-Data_Structures (0:04:39 elapsed time, 0:16:18 cpu time, factor 3.50) *** Timeout Smooth_Manifolds FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Smooth_Manifolds) *** Failed to finish proof (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \U. *** \U \ f ` topspace T; *** openin T (f -` U \ topspace T)\ *** \ openin T {x \ topspace T. f x \ U} *** At command "by" (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \openin Z V; *** \x\topspace (Y i). g (f i x) \ topspace Z; *** openin (Y i) {x \ topspace (Y i). g (f i x) \ V}\ *** \ openin (Y i) *** ((g \ f i) -` V \ topspace (Y i)) *** At command "by" (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \U. *** \\i. f i \ topspace (Y i) \ X; *** U \ X; *** \i. openin (Y i) (f i -` U \ topspace (Y i))\ *** \ openin (Y i) *** {x \ topspace (Y i). f i x \ U} *** At command "by" (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (2 subgoals): *** 1. \X. *** \\x\topspace T1. x \ topspace T2; *** \U. *** openin T2 U \ *** openin T1 {x \ topspace T1. x \ U}; *** openin T2 X\ *** \ openin T1 (X \ topspace T1) *** 2. \U. *** \\X. *** openin T2 X \ *** openin T1 (X \ topspace T1); *** topspace T1 \ topspace T2; openin T2 U\ *** \ openin T1 {x \ topspace T1. x \ U} *** At command "by" (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy") Unfinished session(s): Functional_Ordered_Resolution_Prover, Higher_Order_Terms, Lambda_Free_EPO, Lambda_Free_KBOs, Lambda_Free_RPOs, Noninterference_Generic_Unwinding, Smooth_Manifolds, Valuation, Verified-Prover === TIMING === Group AFP: 0:26:26 elapsed time, 0:43:00 cpu time, factor 1.63 Group main: 0:00:00 elapsed time Group doc: 0:00:00 elapsed time Group timing: 0:04:39 elapsed time, 0:16:18 cpu time, factor 3.50 Group large: 0:00:00 elapsed time Group no_doc: 0:00:00 elapsed time Overall: 0:21:35 elapsed time, 0:59:19 cpu time, factor 2.75 === FAILED SESSIONS === Session Lambda_Free_KBOs: FAILED 2 Session Valuation: FAILED 2 Session Smooth_Manifolds: FAILED 1 Session Functional_Ordered_Resolution_Prover: FAILED 2 Session Higher_Order_Terms: FAILED 2 Session Noninterference_Generic_Unwinding: FAILED 2 Session Lambda_Free_EPO: FAILED 2 Session Lambda_Free_RPOs: FAILED 2 Session Verified-Prover: FAILED 2 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === REPORT === Writing report file ... === SITEGEN === Writing status file ... Running sitegen ... Success: Generated topics.html Success: Generated index.html Success: Generated html files for 466 entries Success: Generated statistics.html Success: Generated download.html Success: Generated about.html Success: Generated citing.html Success: Generated updating.html Success: Generated search.html Success: Generated submitting.html Success: Generated using.html Success: Generated rss.xml Success: Generated status.html Checked directory thys. Found 0 warnings. Packing tars ... === NOTIFICATIONS === Entry Noninterference_Generic_Unwinding: WARNING no maintainers specified === COMPLETED === Build step 'Execute shell' marked build as failure Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: FAILURE