Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) 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/
real URL is https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-all] $ hg update --clean --rev default
0 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 2c1b0156316380307b467e44783426064ac2923c --template exists\n
exists
[isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(2c1b0156316380307b467e44783426064ac2923c)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
1495 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 8c220a4fb5ab9297c611cde7194f03c3516708ff --template exists\n
exists
[afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(8c220a4fb5ab9297c611cde7194f03c3516708ff)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins10431350949507752774.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
opam update
[NOTE] Package zarith is already installed (current version is 1.12).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.7
+ bin/isabelle ci_build all
=== CONFIGURATION ===
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5e9c8155ea96/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 8, threads = 8, numa = true
=== BUILD ===
Build started at Mon, 22 May 2023 13:27:29 +0200
Isabelle id 2c1b01563163
AFP id 1a1e92696b0d
=== LOG ===
Session Pure/Pure
Session Misc/CTT
Session Misc/Cube
Session FOL/FOL
Session FOL/CCL
Session FOL/FOL-ex
Session FOL/FOLP
Session FOL/FOLP-ex
Session Doc/Intro (doc)
Session FOL/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/SML
Session Misc/Sequents
Session Doc/Sledgehammer (doc)
Session AFP/SpecCheck (AFP)
Session Misc/Tools
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/Ackermanns_not_PR (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/Boolos_Curious_Inference_Automated (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (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/Dedekind_Real (AFP)
Session Doc/Demo_EPTCS (doc)
Session Doc/Demo_Easychair (doc)
Session Doc/Demo_FoilTeX (doc)
Session Doc/Demo_LIPIcs (doc)
Session Doc/Demo_LLNCS (doc)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (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/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Risk_Free_Lending (AFP)
Session HOL/HOL-Hoare
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/ADS_Functor (AFP)
Session AFP/Approximation_Algorithms (AFP)
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/Birkhoff_Finite_Distributive_Lattices (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/CoSMeDis (AFP)
Session AFP/CoCon (AFP)
Session AFP/CoSMed (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 Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Complete_Non_Orders (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Conditional_Simplification (AFP)
Session AFP/Conditional_Transfer_Rule (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session AFP/Shadow_DOM (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Core_SC_DOM (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/FinFun (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (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-Combinatorics (main timing)
Session AFP/Blue_Eyes (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/Finitely_Generated_Abelian_Groups (AFP)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Interpolation_Polynomials_HOL_Algebra (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/Actuarial_Mathematics (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/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Cartan_FP (AFP)
Session HOL/HOL-Eisbach
Session AFP/AOT (AFP)
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Cook_Levin (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-Homology (timing)
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/Laws_of_Large_Numbers (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/Hahn_Jordan_Decomposition (AFP)
Session AFP/Lp (AFP)
Session AFP/MDP-Rewards (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/Quasi_Borel_Spaces (AFP)
Session AFP/Skip_Lists (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Turans_Graph_Theorem (AFP)
Session AFP/Hyperdual (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (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/Youngs_Inequality (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Examples
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/Arith_Prog_Rel_Primes (AFP)
Session AFP/Bernoulli (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Query_Optimization (AFP)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lehmer (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Padic_Ints (AFP)
Session AFP/Padic_Field (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/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (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-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (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-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-ex
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Stern_Brocot (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/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/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (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/Prefix_Free_Code_Combinators (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/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (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/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Safe_OCL (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Solidity (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session Doc/System (doc)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (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-Matrix_LP
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-Mutabelle
Session HOL/HOL-NanoJava
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-Prolog
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-Real_Asymp
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Fourier (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session AFP/Lambert_W (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-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-TPTP
Session HOL/HOL-Types_To_Sets
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session AFP/CSP_RefTK (AFP)
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/BirdKMP (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/Hales_Jewett (AFP)
Session Misc/Haskell
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hello_World (AFP)
Session AFP/HoareForDivergence (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2 (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Involutions2Squares (AFP)
Session AFP/IsaGeoCoq (AFP)
Session AFP/IsaNet (AFP)
Session Doc/Isar_Ref (doc)
Session AFP/Isabelle_C (AFP)
Session Doc/JEdit (doc)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/Kneser_Cauchy_Davenport (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAD (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Algebraic_VCs (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/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Jinja (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/JinjaDCI (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/List_Update (AFP)
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/PAPP_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Maximum_Segment_Sum (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/Mereology (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Multitape_To_Singletape_TM (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nano_JSON (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (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/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Undirected_Graph_Theory (AFP)
Session AFP/Balog_Szemeredi_Gowers (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/Chandy_Lamport (AFP)
Session AFP/Saturation_Framework (AFP)
Session AFP/Saturation_Framework_Extensions (AFP)
Session AFP/Progress_Tracking (AFP)
Session AFP/PAL (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Logic_Class (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Power (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Sauer_Shelah_Lemma (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stellar_Quorums (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/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/StrictOmegaCategories (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Suppes_Theorem (AFP)
Session AFP/Syntax_Independent_Logic (AFP)
Session AFP/Goedel_Incompleteness (AFP)
Session AFP/Goedel_HFSet_Semantic (AFP)
Session AFP/Goedel_HFSet_Semanticless (AFP)
Session AFP/Robinson_Arithmetic (AFP)
Session AFP/Synthetic_Completeness (AFP)
Session AFP/Szpilrajn (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (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/Van_der_Waerden (AFP)
Session AFP/VeriComp (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (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/CHERI-C_Memory_Model (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Eval_FO (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/VYDRA_MDL (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Show (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/CakeML (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Gauss_Sums (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/IMO2019 (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Farkas (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Regular_Tree_Relations (AFP)
Session AFP/FO_Theory_Rewriting (AFP)
Session AFP/Rewrite_Properties_Reduction (AFP)
Session AFP/Weighted_Path_Order (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/MDP-Algorithms (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/BenOr_Kozen_Reif (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/LP_Duality (AFP)
Session AFP/Linear_Programming (AFP)
Session AFP/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Fishers_Inequality (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Power_Sum_Polynomials (AFP)
Session AFP/Hermite_Lindemann (AFP)
Session AFP/Factor_Algebraic_Polynomial (AFP)
Session AFP/Cubic_Quartic_Equations (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/Registers (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/XML (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/Gale_Shapley (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/Poincare_Bendixson (AFP)
Session AFP/Safe_Range_RC (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (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/LTL_to_DRA (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Quantifier_Elimination_Hybrid (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/FSM_Tests (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/MiniSail (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/BTree (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/Probabilistic_While (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Constructive_Cryptography_CM (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/Kruskal (AFP)
Session AFP/PAC_Checker (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session FOL/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session AFP/Recursion-Addition (AFP)
Session FOL/ZF-AC
Session FOL/ZF-Coind
Session FOL/ZF-Constructible
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Session AFP/Forcing (AFP)
Session FOL/ZF-IMP
Session FOL/ZF-Induct
Session FOL/ZF-UNITY (timing)
Session FOL/ZF-Resid
Session FOL/ZF-ex
Building CakeML on hpcisabelle/0 ...
Running MFODL_Monitor_Optimized on hpcisabelle/1 ...
Running IEEE_Floating_Point on hpcisabelle/2 ...
CakeML: theory HOL-Eisbach.Eisbach
CakeML: theory CakeML.Doc_Generated
CakeML: theory CakeML.Doc_Proofs
CakeML: theory Deriving.Derive_Manager
CakeML: theory Deriving.Generator_Aux
CakeML: theory HOL-Library.Case_Converter
CakeML: theory HOL-Library.Datatype_Records
CakeML: theory HOL-Library.Complete_Partial_Order2
CakeML: theory HOL-Library.Infinite_Set
CakeML: theory HOL-Library.Nat_Bijection
CakeML: theory HOL-Library.Old_Datatype
IEEE_Floating_Point: theory HOL-Library.Adhoc_Overloading
IEEE_Floating_Point: theory HOL-Library.Code_Abstract_Nat
IEEE_Floating_Point: theory HOL-Library.Code_Target_Int
IEEE_Floating_Point: theory HOL-Library.Log_Nat
IEEE_Floating_Point: theory HOL-Library.Lattice_Algebras
IEEE_Floating_Point: theory HOL-Library.Monad_Syntax
IEEE_Floating_Point: theory HOL-Library.Code_Target_Nat
CakeML: theory Word_Lib.Signed_Words
MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach
MFODL_Monitor_Optimized: theory Word_Lib.Signed_Words
MFODL_Monitor_Optimized: theory Word_Lib.Type_Syntax
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Regex
MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join
MFODL_Monitor_Optimized: theory Word_Lib.Enumeration
MFODL_Monitor_Optimized: theory Word_Lib.Aligned
MFODL_Monitor_Optimized: theory Word_Lib.Even_More_List
IEEE_Floating_Point: theory HOL-Library.Code_Target_Numeral
CakeML: theory HOL-Library.Simps_Case_Conv
CakeML: theory Word_Lib.Word_Names
CakeML: theory Word_Lib.Type_Syntax
CakeML: theory Word_Lib.Word_Syntax
CakeML: theory HOL-Library.Signed_Division
CakeML: theory HOL-Library.Lattice_Algebras
CakeML: theory HOL-Library.Log_Nat
CakeML: theory Show.Show
MFODL_Monitor_Optimized: theory Word_Lib.Enumeration_Word
MFODL_Monitor_Optimized: theory HOL-Eisbach.Eisbach_Tools
MFODL_Monitor_Optimized: theory Word_Lib.Word_EqI
CakeML: theory HOL-Library.Countable
CakeML: theory Word_Lib.Enumeration
CakeML: theory HOL-Eisbach.Eisbach_Tools
CakeML: theory Word_Lib.Word_EqI
CakeML: theory Word_Lib.Rsplit
CakeML: theory Word_Lib.More_Misc
CakeML: theory CakeML.Namespace
CakeML: theory Word_Lib.Enumeration_Word
CakeML: theory Word_Lib.Signed_Division_Word
MFODL_Monitor_Optimized: theory Generic_Join.Generic_Join_Correctness
CakeML: theory Show.Show_Instances
IEEE_Floating_Point: theory HOL-Library.Float
CakeML: theory CakeML.Tokens
CakeML: theory HOL-Library.Countable_Set
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_Join
CakeML: theory HOL-Library.Countable_Complete_Lattices
MFODL_Monitor_Optimized: theory Word_Lib.Word_Lemmas
CakeML: theory Word_Lib.Word_Lemmas
IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE
CakeML: theory HOL-Library.Order_Continuity
CakeML: theory Word_Lib.More_Word_Operations
IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Properties
IEEE_Floating_Point: theory IEEE_Floating_Point.FP64
CakeML: theory CakeML.NamespaceAuxiliary
CakeML: theory HOL-Library.Float
CakeML: theory HOL-Library.Extended_Nat
IEEE_Floating_Point: theory IEEE_Floating_Point.Conversion_IEEE_Float
IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN
MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE
IEEE_Floating_Point: theory IEEE_Floating_Point.Double
IEEE_Floating_Point: theory IEEE_Floating_Point.IEEE_Single_NaN_SMTLIB
CakeML: theory Coinductive.Coinductive_Nat
CakeML: theory Word_Lib.Word_64
MFODL_Monitor_Optimized: theory IEEE_Floating_Point.IEEE_Properties
CakeML: theory Coinductive.Coinductive_List
CakeML: theory IEEE_Floating_Point.IEEE
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Code_Double
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Event_Data
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Formula
CakeML: theory IEEE_Floating_Point.FP64
CakeML: theory CakeML.Lib
Preparing IEEE_Floating_Point/document ...
CakeML: theory CakeML.LibAuxiliary
CakeML: theory CakeML.Ffi
CakeML: theory CakeML.FpSem
CakeML: theory CakeML.Ast
Finished IEEE_Floating_Point/document (0:00:05 elapsed time)
Preparing IEEE_Floating_Point/outline ...
CakeML: theory CakeML.SimpleIO
Finished IEEE_Floating_Point/outline (0:00:03 elapsed time)
Timing IEEE_Floating_Point (8 threads, 24.015s elapsed time, 89.803s cpu time, 2.127s GC time, factor 3.74)
Finished IEEE_Floating_Point (0:00:26 elapsed time, 0:01:33 cpu time, factor 3.53)
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor
CakeML: theory CakeML.CakeML_Compiler
CakeML: theory CakeML.AstAuxiliary
CakeML: theory CakeML.SemanticPrimitives
CakeML: theory CakeML.CakeML_Quickcheck
CakeML: theory CakeML.Evaluate
CakeML: theory CakeML.SmallStep
CakeML: theory CakeML.TypeSystem
CakeML: theory CakeML.SemanticPrimitivesAuxiliary
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Optimized_MTL
CakeML: theory CakeML.BigStep
CakeML: theory CakeML.PrimTypes
CakeML: theory CakeML.BigSmallInvariants
CakeML: theory CakeML.Semantic_Extras
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Impl
CakeML: theory CakeML.TypeSystemAuxiliary
CakeML: theory CakeML.Big_Step_Determ
CakeML: theory CakeML.Big_Step_Total
CakeML: theory CakeML.Big_Step_Clocked
CakeML: theory CakeML.Big_Step_Unclocked
CakeML: theory CakeML.Evaluate_Termination
CakeML: theory CakeML.Matching
CakeML: theory CakeML.Evaluate_Clock
CakeML: theory CakeML.Big_Step_Fun_Equiv
CakeML: theory CakeML.Evaluate_Single
CakeML: theory CakeML.Big_Step_Unclocked_Single
CakeML: theory CakeML.CakeML_Code
CakeML: theory CakeML.Compiler_Test
CakeML: theory CakeML.Code_Test_Haskell
MFODL_Monitor_Optimized: theory MFODL_Monitor_Optimized.Monitor_Code
Preparing MFODL_Monitor_Optimized/document ...
Finished MFODL_Monitor_Optimized/document (0:00:14 elapsed time)
Preparing MFODL_Monitor_Optimized/outline ...
Finished MFODL_Monitor_Optimized/outline (0:00:07 elapsed time)
Timing MFODL_Monitor_Optimized (8 threads, 257.248s elapsed time, 1299.056s cpu time, 66.479s GC time, factor 5.05)
Finished MFODL_Monitor_Optimized (0:04:22 elapsed time, 0:21:53 cpu time, factor 5.00)
Preparing CakeML/document ...
Finished CakeML/document (0:00:06 elapsed time)
Preparing CakeML/outline ...
Finished CakeML/outline (0:00:04 elapsed time)
Timing CakeML (8 threads, 232.272s elapsed time, 1206.576s cpu time, 125.537s GC time, factor 5.19)
Finished CakeML (0:04:57 elapsed time, 0:22:51 cpu time, factor 4.61)
Running CakeML_Codegen on hpcisabelle/3 ...
CakeML_Codegen: theory Automatic_Refinement.Refine_Util_Bootstrap1
CakeML_Codegen: theory HOL-Data_Structures.Cmp
CakeML_Codegen: theory HOL-Data_Structures.Less_False
CakeML_Codegen: theory HOL-Library.Adhoc_Overloading
CakeML_Codegen: theory HOL-Library.AList
CakeML_Codegen: theory HOL-Data_Structures.Priority_Queue_Specs
CakeML_Codegen: theory HOL-Library.Conditional_Parametricity
CakeML_Codegen: theory HOL-Library.Pattern_Aliases
CakeML_Codegen: theory Automatic_Refinement.Mk_Term_Antiquot
CakeML_Codegen: theory Automatic_Refinement.Mpat_Antiquot
CakeML_Codegen: theory HOL-Data_Structures.Sorted_Less
CakeML_Codegen: theory HOL-Library.Monad_Syntax
CakeML_Codegen: theory HOL-Library.Tree
CakeML_Codegen: theory HOL-Data_Structures.List_Ins_Del
CakeML_Codegen: theory HOL-Library.FSet
CakeML_Codegen: theory Amortized_Complexity.Amortized_Framework0
CakeML_Codegen: theory Automatic_Refinement.Refine_Util
CakeML_Codegen: theory Huffman.Huffman
CakeML_Codegen: theory HOL-Data_Structures.Set_Specs
CakeML_Codegen: theory Root_Balanced_Tree.Time_Monad
CakeML_Codegen: theory Dict_Construction.Dict_Construction
CakeML_Codegen: theory HOL-Data_Structures.Tree2
CakeML_Codegen: theory HOL-Data_Structures.Tree_Set
CakeML_Codegen: theory HOL-Library.Tree_Multiset
CakeML_Codegen: theory HOL-Library.Tree_Real
CakeML_Codegen: theory HOL-Data_Structures.Leftist_Heap
CakeML_Codegen: theory HOL-Data_Structures.Balance
CakeML_Codegen: theory Pairing_Heap.Pairing_Heap_Tree
CakeML_Codegen: theory Root_Balanced_Tree.Root_Balanced_Tree
CakeML_Codegen: theory CakeML_Codegen.ML_Utils
CakeML_Codegen: theory HOL-Library.Finite_Map
CakeML_Codegen: theory CakeML_Codegen.Code_Utils
CakeML_Codegen: theory CakeML_Codegen.Test_Utils
CakeML_Codegen: theory CakeML_Codegen.Compiler_Utils
CakeML_Codegen: theory CakeML_Codegen.CakeML_Utils
CakeML_Codegen: theory CakeML_Codegen.Doc_Backend
CakeML_Codegen: theory CakeML_Codegen.Doc_Compiler
CakeML_Codegen: theory CakeML_Codegen.Doc_Rewriting
CakeML_Codegen: theory CakeML_Codegen.Doc_CupCake
CakeML_Codegen: theory CakeML_Codegen.Doc_Preproc
CakeML_Codegen: theory Constructor_Funs.Constructor_Funs
CakeML_Codegen: theory CakeML_Codegen.Doc_Terms
CakeML_Codegen: theory Datatype_Order_Generator.Derive_Aux
CakeML_Codegen: theory HOL-Library.State_Monad
CakeML_Codegen: theory HOL-Library.Disjoint_FSets
CakeML_Codegen: theory Higher_Order_Terms.Name
CakeML_Codegen: theory List-Index.List_Index
CakeML_Codegen: theory CakeML_Codegen.CakeML_Byte
CakeML_Codegen: theory CakeML_Codegen.CupCake_Env
CakeML_Codegen: theory Datatype_Order_Generator.Order_Generator
CakeML_Codegen: theory Higher_Order_Terms.Find_First
CakeML_Codegen: theory Higher_Order_Terms.Term_Utils
CakeML_Codegen: theory Higher_Order_Terms.Fresh_Monad
CakeML_Codegen: theory Higher_Order_Terms.Term_Class
CakeML_Codegen: theory Higher_Order_Terms.Fresh_Class
CakeML_Codegen: theory CakeML_Codegen.CupCake_Semantics
CakeML_Codegen: theory Higher_Order_Terms.Nterm
CakeML_Codegen: theory Higher_Order_Terms.Term
CakeML_Codegen: theory Higher_Order_Terms.Pats
CakeML_Codegen: theory CakeML_Codegen.Terms_Extras
CakeML_Codegen: theory Higher_Order_Terms.Term_to_Nterm
CakeML_Codegen: theory CakeML_Codegen.General_Rewriting
CakeML_Codegen: theory CakeML_Codegen.HOL_Datatype
CakeML_Codegen: theory CakeML_Codegen.Constructors
CakeML_Codegen: theory CakeML_Codegen.Consts
CakeML_Codegen: theory CakeML_Codegen.Strong_Term
CakeML_Codegen: theory CakeML_Codegen.CakeML_Setup
CakeML_Codegen: theory CakeML_Codegen.Rewriting_Term
CakeML_Codegen: theory CakeML_Codegen.Sterm
CakeML_Codegen: theory CakeML_Codegen.Rewriting_Nterm
CakeML_Codegen: theory CakeML_Codegen.Eval_Class
CakeML_Codegen: theory CakeML_Codegen.Embed
CakeML_Codegen: theory CakeML_Codegen.Pterm
CakeML_Codegen: theory CakeML_Codegen.Term_as_Value
CakeML_Codegen: theory CakeML_Codegen.Value
CakeML_Codegen: theory CakeML_Codegen.Eval_Instances
CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm_Elim
CakeML_Codegen: theory CakeML_Codegen.Rewriting_Pterm
CakeML_Codegen: theory CakeML_Codegen.Rewriting_Sterm
CakeML_Codegen: theory CakeML_Codegen.Big_Step_Sterm
CakeML_Codegen: theory CakeML_Codegen.CakeML_Backend
CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value
CakeML_Codegen: theory CakeML_Codegen.Big_Step_Value_ML
CakeML_Codegen: theory CakeML_Codegen.CakeML_Correctness
CakeML_Codegen: theory CakeML_Codegen.Composition
CakeML_Codegen: theory CakeML_Codegen.Compiler
CakeML_Codegen: theory Lazy_Case.Lazy_Case
CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data
CakeML_Codegen: theory CakeML_Codegen.Test_Composition
CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Data2
CakeML_Codegen: theory CakeML_Codegen.Test_Embed_Tree
CakeML_Codegen: theory CakeML_Codegen.Test_Print
CakeML_Codegen: theory CakeML_Codegen.Test_Datatypes
Preparing CakeML_Codegen/document ...
Finished CakeML_Codegen/document (0:00:09 elapsed time)
Preparing CakeML_Codegen/outline ...
Finished CakeML_Codegen/outline (0:00:04 elapsed time)
Timing CakeML_Codegen (8 threads, 326.096s elapsed time, 1282.420s cpu time, 58.980s GC time, factor 3.93)
Finished CakeML_Codegen (0:05:31 elapsed time, 0:21:37 cpu time, factor 3.92)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting CakeML in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML" ...
Presenting IEEE_Floating_Point in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IEEE_Floating_Point" ...
Presenting MFODL_Monitor_Optimized in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFODL_Monitor_Optimized" ...
Presenting CakeML_Codegen in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CakeML_Codegen" ...
Presenting document IEEE_Floating_Point/document
Presenting document IEEE_Floating_Point/outline
Presenting document MFODL_Monitor_Optimized/document
Presenting document MFODL_Monitor_Optimized/outline
Presenting document CakeML/document
Presenting document CakeML/outline
Presenting theory "Word_Lib.Type_Syntax"
Presenting theory "CakeML.Doc_Generated"
Presenting theory "HOL-Library.Log_Nat"
Presenting document CakeML_Codegen/document
Presenting document CakeML_Codegen/outline
Presenting theory "Word_Lib.Signed_Words"
Presenting theory "HOL-Library.Datatype_Records"
Presenting file "~~/src/HOL/Library/datatype_records.ML"
Presenting theory "Word_Lib.Enumeration"
Presenting theory "HOL-Library.FSet"
Presenting theory "Word_Lib.Even_More_List"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Word_Lib.Enumeration_Word"
Presenting theory "Automatic_Refinement.Refine_Util_Bootstrap1"
Presenting theory "Automatic_Refinement.Mpat_Antiquot"
Presenting theory "Automatic_Refinement.Mk_Term_Antiquot"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Automatic_Refinement.Refine_Util"
Presenting theory "Word_Lib.Aligned"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.Float"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "IEEE_Floating_Point.IEEE"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Dict_Construction.Dict_Construction"
Presenting file "$AFP/Dict_Construction/dict_construction_util.ML"
Presenting file "$AFP/Dict_Construction/transfer_termination.ML"
Presenting file "$AFP/Dict_Construction/congruences.ML"
Presenting file "$AFP/Dict_Construction/side_conditions.ML"
Presenting file "$AFP/Dict_Construction/class_graph.ML"
Presenting file "$AFP/Dict_Construction/dict_construction.ML"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "CakeML_Codegen.ML_Utils"
Presenting file "$AFP/CakeML_Codegen/Utils/utils.ML"
Presenting theory "IEEE_Floating_Point.IEEE_Properties"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Word_Lib.Word_EqI"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "IEEE_Floating_Point.FP64"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "HOL-Library.Complete_Partial_Order2"
Presenting theory "IEEE_Floating_Point.Conversion_IEEE_Float"
Presenting theory "HOL-Library.AList"
Presenting theory "Word_Lib.Word_Lemmas"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "IEEE_Floating_Point.Double"
Presenting theory "IEEE_Floating_Point.IEEE_Single_NaN"
Presenting theory "Coinductive.Coinductive_Nat"
Presenting theory "IEEE_Floating_Point.IEEE_Single_NaN_SMTLIB"
Presenting file "$AFP/IEEE_Floating_Point/smt_float.ML"
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting theory "IEEE_Floating_Point.IEEE"
Presenting theory "IEEE_Floating_Point.IEEE_Properties"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "MFODL_Monitor_Optimized.Code_Double"
Presenting theory "MFODL_Monitor_Optimized.Event_Data"
Presenting theory "MFODL_Monitor_Optimized.Regex"
Presenting theory "CakeML_Codegen.Compiler_Utils"
Presenting theory "CakeML_Codegen.Code_Utils"
Presenting file "$AFP/CakeML_Codegen/Utils/pattern_compatibility.ML"
Presenting file "$AFP/CakeML_Codegen/Utils/dynamic_unfold.ML"
Presenting theory "CakeML_Codegen.CakeML_Utils"
Presenting theory "Coinductive.Coinductive_List"
Presenting theory "Huffman.Huffman"
Presenting theory "MFODL_Monitor_Optimized.Formula"
Presenting theory "HOL-Library.Pattern_Aliases"
Presenting theory "HOL-Library.Tree"
Presenting theory "Generic_Join.Generic_Join"
Presenting theory "HOL-Data_Structures.Tree2"
Presenting theory "HOL-Data_Structures.Priority_Queue_Specs"
Presenting theory "CakeML.Lib"
Presenting theory "HOL-Data_Structures.Leftist_Heap"
Presenting theory "CakeML.Namespace"
Presenting theory "HOL-Library.Tree_Multiset"
Presenting theory "HOL-Library.Log_Nat"
Presenting theory "Pairing_Heap.Pairing_Heap_Tree"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "Amortized_Complexity.Amortized_Framework0"
Presenting theory "HOL-Data_Structures.Cmp"
Presenting theory "HOL-Data_Structures.Less_False"
Presenting theory "HOL-Data_Structures.Sorted_Less"
Presenting theory "HOL-Data_Structures.List_Ins_Del"
Presenting theory "HOL-Data_Structures.Set_Specs"
Presenting theory "HOL-Data_Structures.Tree_Set"
Presenting theory "HOL-Library.Tree_Real"
Presenting theory "HOL-Data_Structures.Balance"
Presenting theory "Root_Balanced_Tree.Time_Monad"
Presenting theory "HOL-Library.Float"
Presenting theory "Word_Lib.Type_Syntax"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "Word_Lib.Signed_Words"
Presenting theory "Generic_Join.Generic_Join_Correctness"
Presenting theory "Root_Balanced_Tree.Root_Balanced_Tree"
Presenting theory "Word_Lib.Enumeration"
Presenting theory "Word_Lib.Enumeration_Word"
Presenting theory "CakeML_Codegen.Test_Utils"
Presenting theory "CakeML_Codegen.Doc_Terms"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting theory "Datatype_Order_Generator.Derive_Aux"
Presenting file "$AFP/Datatype_Order_Generator/derive_aux.ML"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Word_Lib.Word_EqI"
Presenting theory "MFODL_Monitor_Optimized.Optimized_Join"
Presenting theory "Datatype_Order_Generator.Order_Generator"
Presenting file "$AFP/Datatype_Order_Generator/order_generator.ML"
Presenting theory "Higher_Order_Terms.Name"
Presenting theory "HOL-Library.State_Monad"
Presenting theory "Word_Lib.Word_Lemmas"
Presenting theory "Higher_Order_Terms.Term_Utils"
Presenting theory "HOL-Library.Disjoint_FSets"
Presenting theory "Higher_Order_Terms.Term_Class"
Presenting theory "IEEE_Floating_Point.IEEE"
Presenting theory "Word_Lib.Word_Names"
Presenting theory "Word_Lib.Word_Syntax"
Presenting theory "Word_Lib.Rsplit"
Presenting theory "Word_Lib.More_Misc"
Presenting theory "Higher_Order_Terms.Term"
Presenting theory "Word_Lib.More_Word_Operations"
Presenting theory "Higher_Order_Terms.Pats"
Presenting theory "Word_Lib.Word_64"
Presenting theory "IEEE_Floating_Point.FP64"
Presenting theory "CakeML.FpSem"
Presenting theory "CakeML.Ast"
Presenting theory "CakeML.AstAuxiliary"
Presenting theory "CakeML_Codegen.Terms_Extras"
Presenting file "$AFP/CakeML_Codegen/Terms/hol_term.ML"
Presenting theory "CakeML.Ffi"
Presenting theory "CakeML_Codegen.HOL_Datatype"
Presenting file "$AFP/CakeML_Codegen/Terms/hol_datatype.ML"
Presenting theory "CakeML_Codegen.Constructors"
Presenting theory "Higher_Order_Terms.Nterm"
Presenting theory "CakeML_Codegen.Consts"
Presenting theory "CakeML_Codegen.Strong_Term"
Presenting theory "CakeML_Codegen.Sterm"
Presenting theory "CakeML.SemanticPrimitives"
Presenting theory "CakeML_Codegen.Pterm"
Presenting theory "CakeML.SmallStep"
Presenting theory "CakeML_Codegen.Term_as_Value"
Presenting theory "CakeML.BigStep"
Presenting theory "CakeML_Codegen.Value"
Presenting theory "CakeML_Codegen.Doc_CupCake"
Presenting theory "CakeML.BigSmallInvariants"
Presenting theory "CakeML_Codegen.CupCake_Env"
Presenting theory "CakeML.Evaluate"
Presenting theory "CakeML.LibAuxiliary"
Presenting theory "CakeML.NamespaceAuxiliary"
Presenting theory "CakeML.PrimTypes"
Presenting theory "CakeML.SemanticPrimitivesAuxiliary"
Presenting theory "CakeML.SimpleIO"
Presenting theory "CakeML.Tokens"
Presenting theory "CakeML_Codegen.CupCake_Semantics"
Presenting theory "CakeML_Codegen.Doc_Rewriting"
Presenting theory "CakeML_Codegen.General_Rewriting"
Presenting theory "CakeML_Codegen.Rewriting_Term"
Presenting theory "Higher_Order_Terms.Fresh_Monad"
Presenting theory "Higher_Order_Terms.Fresh_Class"
Presenting theory "CakeML.TypeSystem"
Presenting theory "List-Index.List_Index"
Presenting theory "CakeML.TypeSystemAuxiliary"
Presenting theory "CakeML.Doc_Proofs"
Presenting theory "Higher_Order_Terms.Find_First"
Presenting theory "CakeML.Semantic_Extras"
Presenting theory "CakeML.Evaluate_Termination"
Presenting theory "CakeML.Evaluate_Clock"
Presenting theory "Higher_Order_Terms.Term_to_Nterm"
Presenting theory "CakeML.Evaluate_Single"
Presenting theory "MFODL_Monitor_Optimized.Monitor"
Presenting theory "CakeML.Big_Step_Determ"
Presenting theory "CakeML_Codegen.Rewriting_Nterm"
Presenting theory "CakeML.Big_Step_Total"
Presenting theory "CakeML.Big_Step_Fun_Equiv"
Presenting theory "CakeML.Big_Step_Unclocked"
Presenting theory "CakeML_Codegen.Rewriting_Pterm_Elim"
Presenting theory "CakeML_Codegen.Rewriting_Pterm"
Presenting theory "CakeML_Codegen.Rewriting_Sterm"
Presenting theory "CakeML.Big_Step_Clocked"
Presenting theory "CakeML_Codegen.Big_Step_Sterm"
Presenting theory "CakeML.Big_Step_Unclocked_Single"
Presenting theory "CakeML.Matching"
Presenting theory "CakeML.CakeML_Code"
Presenting theory "CakeML.CakeML_Quickcheck"
Presenting theory "CakeML_Codegen.Big_Step_Value"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Show.Show_Instances"
Presenting theory "CakeML.CakeML_Compiler"
Presenting file "$AFP/CakeML/Tools/cakeml_sexp.ML"
Presenting file "$AFP/CakeML/Tools/cakeml_compiler.ML"
Presenting theory "CakeML.Compiler_Test"
Presenting theory "CakeML.Code_Test_Haskell"
Presenting theory "CakeML_Codegen.Big_Step_Value_ML"
Presenting theory "CakeML_Codegen.Doc_Preproc"
Presenting theory "MFODL_Monitor_Optimized.Optimized_MTL"
Presenting theory "CakeML_Codegen.Eval_Class"
Presenting file "$AFP/CakeML_Codegen/Preproc/tactics.ML"
Presenting theory "Constructor_Funs.Constructor_Funs"
Presenting file "$AFP/Constructor_Funs/constructor_funs.ML"
Presenting theory "CakeML_Codegen.Embed"
Presenting file "$AFP/CakeML_Codegen/Preproc/embed.ML"
Presenting theory "CakeML_Codegen.Eval_Instances"
Presenting file "$AFP/CakeML_Codegen/Preproc/eval_instances.ML"
Presenting theory "CakeML_Codegen.Doc_Backend"
Presenting theory "CakeML_Codegen.CakeML_Setup"
Presenting theory "CakeML_Codegen.CakeML_Backend"
Presenting theory "MFODL_Monitor_Optimized.Monitor_Impl"
Presenting theory "CakeML_Codegen.CakeML_Correctness"
Presenting theory "MFODL_Monitor_Optimized.Monitor_Code"
Presenting theory "CakeML_Codegen.CakeML_Byte"
Presenting theory "CakeML_Codegen.Doc_Compiler"
Presenting theory "CakeML_Codegen.Composition"
Presenting theory "CakeML_Codegen.Compiler"
Presenting theory "Lazy_Case.Lazy_Case"
Presenting file "$AFP/Lazy_Case/lazy_case.ML"
Presenting theory "CakeML_Codegen.Test_Composition"
Presenting theory "CakeML_Codegen.Test_Print"
Presenting theory "CakeML_Codegen.Test_Embed_Data"
Presenting theory "CakeML_Codegen.Test_Embed_Data2"
Presenting theory "CakeML_Codegen.Test_Embed_Tree"
Presenting theory "CakeML_Codegen.Test_Datatypes"
=== TIMING ===
Group AFP: 0:15:17 elapsed time, 1:07:55 cpu time, factor 4.44
Group main: 0:00:00 elapsed time
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Group doc: 0:00:00 elapsed time
Group timing: 0:00:00 elapsed time
Overall: 0:13:09 elapsed time, 1:07:55 cpu time, factor 5.16
=== DEPENDENCIES ===
Generating dependencies file ...
Writing dependencies file ...
=== REPORT ===
Writing report file ...
=== SITEGEN ===
Writing status file ...
Running sitegen ...
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Preparing topics...
Preparing licenses...
Preparing releases...
Preparing authors...
Extracting keywords...
Preparing entries...
Preparing statistics...
Preparing project files
Preparing devel version...
Finished sitegen preparation.
Cleaning output dir...
Building site...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Packing tars ...
=== COMPLETED ===
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: SUCCESS