diff --git a/thys/AODV/ROOT b/thys/AODV/ROOT --- a/thys/AODV/ROOT +++ b/thys/AODV/ROOT @@ -1,14 +1,20 @@ chapter AFP session AODV (AFP slow) = AWN + description "Mechanized invariant proof of AODV (RFC3561) loop freedom: all variants" options [timeout = 45000] + directories + "variants/a_norreqid" + "variants/b_fwdrreps" + "variants/c_gtobcast" + "variants/d_fwdrreqs" + "variants/e_all_abcd" theories All document_files "root.bib" "root.tex" "mathpartir.sty" (* Separate single-variant sesssions removed for build performance. See rev 4fd7ada36eb9 to recover if necessary. *) diff --git a/thys/Abstract-Hoare-Logics/ROOT b/thys/Abstract-Hoare-Logics/ROOT --- a/thys/Abstract-Hoare-Logics/ROOT +++ b/thys/Abstract-Hoare-Logics/ROOT @@ -1,11 +1,15 @@ chapter AFP session "Abstract-Hoare-Logics" (AFP) = HOL + options [timeout = 600] + directories + "While" + "Proc" + "Procs" theories "While/HoareTotal" "Proc/PHoareTotal" "Procs/PsHoareTotal" document_files "root.bib" "root.tex" diff --git a/thys/Algebraic_VCs/ROOT b/thys/Algebraic_VCs/ROOT --- a/thys/Algebraic_VCs/ROOT +++ b/thys/Algebraic_VCs/ROOT @@ -1,33 +1,36 @@ chapter AFP session Algebraic_VCs (AFP) = KAT_and_DRA + options [timeout = 1200] sessions "HOL-Eisbach" "HOL-Hoare" KAD + directories + "AVC_KAD" + "AVC_KAT" theories "AVC_KAT/VC_KAT_scratch" "AVC_KAD/VC_KAD_scratch" P2S2R "AVC_KAT/VC_KAT" "AVC_KAT/VC_KAT_Examples" "AVC_KAT/VC_KAT_Examples2" RKAT RKAT_Models "AVC_KAT/VC_RKAT" "AVC_KAT/VC_RKAT_Examples" "AVC_KAD/VC_KAD" "AVC_KAD/VC_KAD_Examples" "AVC_KAD/VC_KAD_Examples2" "AVC_KAD/VC_KAD_dual" "AVC_KAD/VC_KAD_dual_Examples" "AVC_KAD/VC_KAD_wf" "AVC_KAD/VC_KAD_wf_Examples" "AVC_KAD/Path_Model_Example" "AVC_KAD/Pointer_Examples" KAD_is_KAT Domain_Quantale document_files "root.tex" "root.bib" diff --git a/thys/ArrowImpossibilityGS/ROOT b/thys/ArrowImpossibilityGS/ROOT --- a/thys/ArrowImpossibilityGS/ROOT +++ b/thys/ArrowImpossibilityGS/ROOT @@ -1,12 +1,14 @@ chapter AFP session ArrowImpossibilityGS (AFP) = HOL + options [timeout = 600] sessions "HOL-Library" + directories + "Thys" theories "Thys/Arrow_Utility" "Thys/GS" document_files "root.bib" "root.tex" diff --git a/thys/Auto2_HOL/ROOT b/thys/Auto2_HOL/ROOT --- a/thys/Auto2_HOL/ROOT +++ b/thys/Auto2_HOL/ROOT @@ -1,21 +1,21 @@ chapter AFP session Auto2_HOL (AFP) = HOL + description \ Instantiation of Auto2 for Isabelle/HOL. \ options [timeout = 600] sessions "HOL-Library" + directories + "HOL" theories [document = false] (* Core setup *) "HOL/Auto2_Test" - theories (* Simple examples *) "HOL/Pelletier" "HOL/Primes_Ex" - document_files "root.tex" "root.bib" diff --git a/thys/Auto2_Imperative_HOL/ROOT b/thys/Auto2_Imperative_HOL/ROOT --- a/thys/Auto2_Imperative_HOL/ROOT +++ b/thys/Auto2_Imperative_HOL/ROOT @@ -1,38 +1,41 @@ chapter AFP session Auto2_Imperative_HOL (AFP) = Auto2_HOL + description \ Application of auto2 to verify functional and imperative programs. \ options [timeout = 2100] sessions "HOL-Library" "HOL-Imperative_HOL" + directories + "Functional" + "Imperative" theories (* Functional programs *) "Functional/BST" "Functional/Lists_Ex" "Functional/Connectivity" "Functional/Dijkstra" "Functional/Interval_Tree" "Functional/Quicksort" "Functional/Indexed_PQueue" "Functional/RBTree" "Functional/Rect_Intersect" (* Imperative programs *) "Imperative/GCD_Impl" "Imperative/LinkedList" "Imperative/BST_Impl" "Imperative/RBTree_Impl" "Imperative/Quicksort_Impl" "Imperative/Connectivity_Impl" "Imperative/Dijkstra_Impl" "Imperative/Rect_Intersect_Impl" theories [document = false] "Imperative/Sep_Examples" document_files "root.tex" "root.bib" diff --git a/thys/Automatic_Refinement/ROOT b/thys/Automatic_Refinement/ROOT --- a/thys/Automatic_Refinement/ROOT +++ b/thys/Automatic_Refinement/ROOT @@ -1,29 +1,33 @@ chapter AFP session Automatic_Refinement (AFP) = HOL + options [timeout = 300] sessions "HOL-Library" "HOL-Eisbach" "HOL-ex" + directories + "Lib" + "Parametricity" + "Tool" theories [document = false] "Lib/Refine_Lib" theories "Parametricity/Param_Chapter" "Parametricity/Relators" "Parametricity/Parametricity" theories [document = false] "Tool/Autoref_Phases" "Tool/Autoref_Data" "Tool/Autoref_Id_Ops" "Tool/Autoref_Relator_Interface" "Tool/Autoref_Fix_Rel" "Tool/Autoref_Gen_Algo" "Tool/Autoref_Translate" theories "Tool/Autoref_Chapter" "Tool/Autoref_Tool" Autoref_Bindings_HOL Automatic_Refinement document_files "root.tex" diff --git a/thys/CAVA_LTL_Modelchecker/ROOT b/thys/CAVA_LTL_Modelchecker/ROOT --- a/thys/CAVA_LTL_Modelchecker/ROOT +++ b/thys/CAVA_LTL_Modelchecker/ROOT @@ -1,55 +1,66 @@ chapter AFP session SM_Base (AFP) in "SM_Base" = CAVA_Automata + options [timeout = 1200] sessions Partial_Order_Reduction DFS_Framework theories Partial_Order_Reduction.Ample_Correctness Partial_Order_Reduction.Ample_Analysis DFS_Framework.Feedback_Arcs session SM (AFP) in "SM" = SM_Base + options [timeout = 1200] sessions Stuttering_Equivalence + directories + "Analysis" + "Impl" + "Lib" + "Refine" + "RefPoint" theories [document = false] "Lib/LTS" "Lib/SOS_Misc_Add" theories "Impl/SM_Wrapup" session CAVA_Setup (AFP) in "CAVA_Setup" = CAVA_Automata + options [timeout = 3600] sessions LTL_to_GBA Gabow_SCC Promela SM theories LTL_to_GBA.All_Of_LTL_to_GBA Gabow_SCC.All_Of_Gabow_SCC Promela.All_Of_Promela SM.SM_Wrapup session CAVA_LTL_Modelchecker (AFP) = CAVA_Setup + options [timeout = 1200] + directories + "Nested_DFS" + "BoolProgs" + "BoolProgs/Programs" + "Examples" theories [document = false] "Nested_DFS/NDFS_SI_Statistics" theories "Nested_DFS/NDFS_SI" CAVA_Abstract "BoolProgs/BoolProgs" theories [document = false] "BoolProgs/BoolProgs_Extras" "BoolProgs/BoolProgs_LTL_Conv" "BoolProgs/Programs/BoolProgs_Programs" "Examples/Mulog" theories CAVA_Impl theories [document = false] All_Of_CAVA_LTL_Modelchecker document_files "root.tex" "root.bib" diff --git a/thys/CISC-Kernel/ROOT b/thys/CISC-Kernel/ROOT --- a/thys/CISC-Kernel/ROOT +++ b/thys/CISC-Kernel/ROOT @@ -1,28 +1,32 @@ chapter AFP session "CISC-Kernel" (AFP) = HOL + options [timeout=600] + directories + "step" + "trace" + "trace/Rushby-with-Control" theories "trace/Rushby-with-Control/Option_Binders" "trace/Rushby-with-Control/List_Theorems" "trace/Rushby-with-Control/K" "trace/Rushby-with-Control/SK" "trace/Rushby-with-Control/ISK" "trace/Rushby-with-Control/CISK" "step/Step_configuration" "step/Step_policies" "step/Step" "step/Step_invariants" "step/Step_vpeq" "step/Step_vpeq_locally_respects" "step/Step_vpeq_weakly_step_consistent" "trace/Rushby-with-Control/Separation_kernel_model" "trace/Rushby-with-Control/Link_separation_kernel_model_to_CISK" document_files "euromils.sty" "locales.png" "logo/EU-flag.jpg" "logo/EURO-MILS_4C.jpg" "logo/fp7-logo.pdf" "root.bib" "root.tex" diff --git a/thys/CakeML/ROOT b/thys/CakeML/ROOT --- a/thys/CakeML/ROOT +++ b/thys/CakeML/ROOT @@ -1,62 +1,66 @@ chapter AFP session LEM (AFP) in "generated" = "HOL-Word" + options [timeout = 300] theories Lem_pervasives Lem_pervasives_extra Lem_list_extra Lem_set_extra Lem_string Lem_string_extra session CakeML (AFP) = LEM + options [timeout = 2400] sessions Coinductive IEEE_Floating_Point Show + directories + "doc" + "generated/CakeML" + "Tests" theories "doc/Doc_Generated" "generated/CakeML/Ast" "generated/CakeML/AstAuxiliary" "generated/CakeML/BigSmallInvariants" "generated/CakeML/BigStep" "generated/CakeML/Evaluate" "generated/CakeML/Lib" "generated/CakeML/LibAuxiliary" "generated/CakeML/Namespace" "generated/CakeML/NamespaceAuxiliary" "generated/CakeML/PrimTypes" "generated/CakeML/SemanticPrimitives" "generated/CakeML/SemanticPrimitivesAuxiliary" "generated/CakeML/SimpleIO" "generated/CakeML/Tokens" "generated/CakeML/TypeSystem" "generated/CakeML/TypeSystemAuxiliary" "doc/Doc_Proofs" Semantic_Extras Evaluate_Termination Evaluate_Clock Evaluate_Single Big_Step_Determ Big_Step_Fun_Equiv Big_Step_Total Big_Step_Unclocked Big_Step_Unclocked_Single Big_Step_Clocked Matching CakeML_Code CakeML_Quickcheck CakeML_Compiler theories [condition = "ISABELLE_CAKEML_HOME,ISABELLE_CC", document = false] "Tests/Compiler_Test" theories [condition = "ISABELLE_GHC", document = false] "Tests/Code_Test_Haskell" document_files "root.tex" \ No newline at end of file diff --git a/thys/CakeML_Codegen/ROOT b/thys/CakeML_Codegen/ROOT --- a/thys/CakeML_Codegen/ROOT +++ b/thys/CakeML_Codegen/ROOT @@ -1,74 +1,85 @@ chapter AFP session CakeML_Codegen (AFP) = CakeML + options [timeout = 3600] sessions Constructor_Funs Dict_Construction Higher_Order_Terms "HOL-Data_Structures" Huffman Pairing_Heap Root_Balanced_Tree Show + directories + "Utils" + "Doc" + "Terms" + "CupCakeML" + "Rewriting" + "Preproc" + "Backend" + "Compiler" + "Test" + theories [document = false] "Utils/ML_Utils" "Utils/Compiler_Utils" "Utils/Code_Utils" "Utils/CakeML_Utils" "Utils/Test_Utils" theories "Doc/Doc_Terms" "Terms/Terms_Extras" "Terms/HOL_Datatype" "Terms/Constructors" "Terms/Consts" "Terms/Strong_Term" "Terms/Sterm" "Terms/Pterm" "Terms/Term_as_Value" "Terms/Value" "Doc/Doc_CupCake" "CupCakeML/CupCake_Env" "CupCakeML/CupCake_Semantics" "Doc/Doc_Rewriting" "Rewriting/Rewriting_Term" "Rewriting/Rewriting_Nterm" "Rewriting/Rewriting_Pterm_Elim" "Rewriting/Rewriting_Pterm" "Rewriting/Rewriting_Sterm" "Rewriting/Big_Step_Sterm" "Rewriting/Big_Step_Value" "Rewriting/Big_Step_Value_ML" "Doc/Doc_Preproc" "Preproc/Eval_Class" "Preproc/Embed" "Preproc/Eval_Instances" "Doc/Doc_Backend" "Backend/CakeML_Setup" "Backend/CakeML_Backend" "Backend/CakeML_Correctness" "Backend/CakeML_Byte" "Doc/Doc_Compiler" "Compiler/Composition" "Compiler/Compiler" theories [document = false] "Test/Test_Composition" "Test/Test_Print" "Test/Test_Embed_Data" "Test/Test_Embed_Data2" "Test/Test_Embed_Tree" theories [condition = "ISABELLE_CAKEML_HOME,ISABELLE_CC", document = false] "Test/Test_Datatypes" document_files "root.tex" diff --git a/thys/Case_Labeling/ROOT b/thys/Case_Labeling/ROOT --- a/thys/Case_Labeling/ROOT +++ b/thys/Case_Labeling/ROOT @@ -1,13 +1,16 @@ chapter AFP session Case_Labeling (AFP) = HOL + options [timeout = 300] sessions "HOL-Eisbach" "HOL-Hoare" + directories + "Examples" + "Examples/Hoare" theories Case_Labeling Case_Labeling_Examples document_files "root.tex" "root.bib" diff --git a/thys/Coinductive/ROOT b/thys/Coinductive/ROOT --- a/thys/Coinductive/ROOT +++ b/thys/Coinductive/ROOT @@ -1,12 +1,14 @@ chapter AFP session Coinductive (AFP) = "HOL-Computational_Algebra" + options [timeout = 600] sessions "HOL-Analysis" + directories + "Examples" theories Coinductive Lazy_TLList "Examples/Coinductive_Examples" document_files "root.tex" diff --git a/thys/Complx/ROOT b/thys/Complx/ROOT --- a/thys/Complx/ROOT +++ b/thys/Complx/ROOT @@ -1,19 +1,22 @@ (* * Copyright 2016, Data61, CSIRO * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(DATA61_BSD) *) chapter AFP session Complx (AFP) = Word_Lib + options [timeout = 2400] + directories + "ex" + "lib" theories OG_Syntax "ex/Examples" "ex/SumArr" document_files "root.tex" diff --git a/thys/ConcurrentGC/ROOT b/thys/ConcurrentGC/ROOT --- a/thys/ConcurrentGC/ROOT +++ b/thys/ConcurrentGC/ROOT @@ -1,18 +1,20 @@ chapter AFP session ConcurrentGC (AFP slow) = ConcurrentIMP + options [timeout = 36000] + directories + "concrete" theories [show_question_marks = false, names_short] Model Tactics Proofs_basis TSO Handshakes MarkObject StrongTricolour Proofs "concrete/Concrete_heap" "concrete/Concrete" document_files "root.bib" "root.tex" diff --git a/thys/Consensus_Refined/ROOT b/thys/Consensus_Refined/ROOT --- a/thys/Consensus_Refined/ROOT +++ b/thys/Consensus_Refined/ROOT @@ -1,35 +1,39 @@ chapter AFP session Consensus_Refined (AFP) = HOL + options [show_question_marks = false, timeout = 600] sessions "HOL-Library" Heard_Of Stuttering_Equivalence + directories + "MRU" + "Observing" + "Voting" theories Infra Consensus_Types Quorums Consensus_Misc Two_Steps "MRU/Three_Steps" Refinement HO_Transition_System Voting Voting_Opt "Voting/OneThirdRule_Proofs" "Voting/Ate_Proofs" Same_Vote Observing_Quorums Observing_Quorums_Opt "Observing/Uv_Proofs" "Observing/BenOr_Proofs" MRU_Vote MRU_Vote_Opt "MRU/New_Algorithm_Proofs" "MRU/Paxos_Proofs" "MRU/CT_Proofs" document_files "root.tex" "root.bib" "ref-tree.pdf" diff --git a/thys/Constructive_Cryptography/ROOT b/thys/Constructive_Cryptography/ROOT --- a/thys/Constructive_Cryptography/ROOT +++ b/thys/Constructive_Cryptography/ROOT @@ -1,10 +1,13 @@ chapter AFP session Constructive_Cryptography (AFP) = CryptHOL + options [timeout = 1500] + directories + "Examples" + "Examples/Secure_Channel" theories Constructive_Cryptography "Examples/Examples" document_files "root.tex" "root.bib" diff --git a/thys/Containers/ROOT b/thys/Containers/ROOT --- a/thys/Containers/ROOT +++ b/thys/Containers/ROOT @@ -1,41 +1,43 @@ chapter AFP session Containers (AFP) = "Deriving" + options [timeout = 600] sessions "Finger-Trees" "Regular-Sets" Automatic_Refinement Collections + directories + "Examples" theories Containers_Auxiliary Card_Datatype Set_Linorder Collection_Order List_Proper_Interval Containers Compatibility_Containers_Regular_Sets Containers_Userguide theories [document = false] "Examples/Card_Datatype_Ex" "Examples/Map_To_Mapping_Ex" "Examples/TwoSat_Ex" "Examples/Containers_DFS_Ex" "Examples/Containers_TwoSat_Ex" document_files "root.tex" "root.bib" session "Containers-Benchmarks" (AFP) in "ITP-2013" = Containers + options [timeout = 1200] sessions Trie theories Benchmark_Bool Benchmark_LC Benchmark_Default Benchmark_ICF Benchmark_RBT Benchmark_Set_Default Benchmark_Set_LC Clauses diff --git a/thys/Core_DOM/ROOT b/thys/Core_DOM/ROOT --- a/thys/Core_DOM/ROOT +++ b/thys/Core_DOM/ROOT @@ -1,10 +1,16 @@ chapter AFP session "Core_DOM" (AFP) = "HOL-Library" + options [timeout = 1200] + directories + "classes" + "monads" + "pointers" + "preliminaries" + "tests" theories Core_DOM Core_DOM_Tests document_files "root.tex" "root.bib" diff --git a/thys/DFS_Framework/ROOT b/thys/DFS_Framework/ROOT --- a/thys/DFS_Framework/ROOT +++ b/thys/DFS_Framework/ROOT @@ -1,27 +1,33 @@ chapter AFP session "DFS_Framework" (AFP) = "CAVA_Automata" + options [timeout = 1200] + directories + "Examples" + "Impl/Data" + "Impl/Structural" + "Invars" + "Misc" theories [document = false] "Misc/DFS_Framework_Refine_Aux" "Misc/Impl_Rev_Array_Stack" "Misc/On_Stack" theories DFS_Chapter_Framework Param_DFS "Invars/DFS_Invars_Basic" "Invars/DFS_Invars_SCC" "Impl/Structural/General_DFS_Structure" "Impl/Structural/Tailrec_Impl" "Impl/Structural/Rec_Impl" "Impl/Data/Simple_Impl" "Impl/Data/Restr_Impl" DFS_Framework "Examples/DFS_Chapter_Examples" "Examples/DFS_All_Examples" document_files "root.tex" diff --git a/thys/Dependent_SIFUM_Refinement/ROOT b/thys/Dependent_SIFUM_Refinement/ROOT --- a/thys/Dependent_SIFUM_Refinement/ROOT +++ b/thys/Dependent_SIFUM_Refinement/ROOT @@ -1,21 +1,23 @@ chapter AFP session Dependent_SIFUM_Refinement (AFP) = Dependent_SIFUM_Type_Systems + description " An Isabelle/HOL formalization of a Compositional Refinement theory for Value-Dependent SIFUM Security Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah " options [timeout = 600] sessions "HOL-Eisbach" + directories + "Examples" theories CompositionalRefinement theories [document = false] "Examples/Eg1RefinementTrivial" "Examples/Eg1Eg2RefinementSimple" "Examples/EgHighBranchRevC" document_files "root.bib" "root.tex" diff --git a/thys/Dependent_SIFUM_Type_Systems/ROOT b/thys/Dependent_SIFUM_Type_Systems/ROOT --- a/thys/Dependent_SIFUM_Type_Systems/ROOT +++ b/thys/Dependent_SIFUM_Type_Systems/ROOT @@ -1,27 +1,29 @@ chapter AFP session Dependent_SIFUM_Type_Systems (AFP) = HOL + description " An Isabelle/HOL formalization of a Value-Dependent extension to Assumptions and Guarantees for Compositional Noninterference Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah The original SIFUM_Type_Systems entry was authored by: Sylvia Grewe, TU Darmstadt Heiko Mantel, TU Darmstadt Daniel Schoepe " options [timeout = 600] sessions "HOL-Eisbach" + directories + "Examples" theories TypeSystem LocallySoundModeUse theories [document = false] "Examples/Example" "Examples/Example_TypeSystem" "Examples/Example_Swap_Add" document_files "root.bib" "root.tex" diff --git a/thys/Deriving/ROOT b/thys/Deriving/ROOT --- a/thys/Deriving/ROOT +++ b/thys/Deriving/ROOT @@ -1,22 +1,27 @@ chapter AFP session Deriving (AFP) = "HOL-Library" + options [timeout = 600] sessions Collections + directories + "Comparator_Generator" + "Countable_Generator" + "Equality_Generator" + "Hash_Generator" theories Derive_Manager Generator_Aux "Comparator_Generator/Compare" "Comparator_Generator/RBT_Compare_Order_Impl" "Comparator_Generator/RBT_Comparator_Impl" "Comparator_Generator/Compare_Order_Instances" "Comparator_Generator/Compare_Rat" "Comparator_Generator/Compare_Real" "Equality_Generator/Equality_Instances" "Hash_Generator/Hash_Instances" "Countable_Generator/Countable_Generator" Derive_Examples document_files "root.bib" "root.tex" diff --git a/thys/Dict_Construction/ROOT b/thys/Dict_Construction/ROOT --- a/thys/Dict_Construction/ROOT +++ b/thys/Dict_Construction/ROOT @@ -1,20 +1,22 @@ chapter AFP session Dict_Construction (AFP) = HOL + options [timeout = 300] sessions "HOL-Library" Automatic_Refinement Lazy_Case Show + directories + "Documentation" theories "Documentation/Introduction" "Documentation/Impossibility" Dict_Construction "Documentation/Termination" Test_Dict_Construction Test_Side_Conditions Test_Lazy_Case document_files "root.bib" "root.tex" \ No newline at end of file diff --git a/thys/Featherweight_OCL/ROOT b/thys/Featherweight_OCL/ROOT --- a/thys/Featherweight_OCL/ROOT +++ b/thys/Featherweight_OCL/ROOT @@ -1,25 +1,30 @@ chapter AFP session Featherweight_OCL (AFP) = HOL + description "Featherweight-OCL" options [document_variants = "annex-a=annexa,-theory,-afp,-proof,-ML:document=afp,-annexa:outline=-annexa,afp,/proof,/ML", show_question_marks = false, timeout = 600] + directories + "basic_types" + "collection_types" + "examples/Employee_Model/Analysis" + "examples/Employee_Model/Design" theories UML_Main "examples/Employee_Model/Analysis/Analysis_OCL" "examples/Employee_Model/Design/Design_OCL" document_files "conclusion.tex" "figures/AbstractSimpleChair.pdf" "figures/jedit.png" "figures/pdf.png" "figures/person.png" "figures/pre-post.pdf" "hol-ocl-isar.sty" "introduction.tex" "lstisar.sty" "omg.sty" "prooftree.sty" "root.bib" "root.tex" "FOCL_Syntax.tex" diff --git a/thys/First_Welfare_Theorem/ROOT b/thys/First_Welfare_Theorem/ROOT --- a/thys/First_Welfare_Theorem/ROOT +++ b/thys/First_Welfare_Theorem/ROOT @@ -1,18 +1,20 @@ (* License: LGPL *) chapter AFP session First_Welfare_Theorem (AFP) = "HOL-Analysis" + options [timeout = 600] + directories + "Microeconomics" theories Syntax Argmax Preferences Utility_Functions "Microeconomics/Consumers" "Microeconomics/Common" "Microeconomics/Exchange_Economy" "Microeconomics/Private_Ownership_Economy" "Microeconomics/Arrow_Debreu_Model" document_files "root.bib" "root.tex" diff --git a/thys/Flow_Networks/ROOT b/thys/Flow_Networks/ROOT --- a/thys/Flow_Networks/ROOT +++ b/thys/Flow_Networks/ROOT @@ -1,29 +1,31 @@ chapter AFP session Flow_Networks (AFP) = Sepref_IICF + options [timeout = 1200] sessions "Program-Conflict-Analysis" CAVA_Automata DFS_Framework Refine_Imperative_HOL + directories + "Lib" theories [document = false] DFS_Framework.DFS_Framework DFS_Framework.Reachable_Nodes "Lib/Fofu_Abs_Base" "Lib/Fofu_Impl_Base" "Lib/Refine_Add_Fofu" Graph theories Network Residual_Graph Augmenting_Flow Augmenting_Path Ford_Fulkerson theories [document = false] Graph_Impl Network_Impl NetCheck document_files "root.tex" "root.bib" diff --git a/thys/Generic_Deriving/ROOT b/thys/Generic_Deriving/ROOT --- a/thys/Generic_Deriving/ROOT +++ b/thys/Generic_Deriving/ROOT @@ -1,17 +1,19 @@ chapter AFP session "Generic_Deriving" (AFP) = HOL + options [timeout = 600] + directories + "tests" theories Derive Tagged_Prod_Sum "tests/Derive_Datatypes" "tests/Derive_Eq" "tests/Derive_Encode" "tests/Derive_Algebra" "tests/Derive_Show" "tests/Derive_Eq_Laws" "tests/Derive_Algebra_Laws" document_files "root.bib" "root.tex" diff --git a/thys/HOLCF-Prelude/ROOT b/thys/HOLCF-Prelude/ROOT --- a/thys/HOLCF-Prelude/ROOT +++ b/thys/HOLCF-Prelude/ROOT @@ -1,29 +1,31 @@ chapter AFP session "HOLCF-Prelude" (AFP) = HOLCF + options [show_question_marks = false, timeout = 3600] sessions "HOL-Computational_Algebra" "HOLCF-Library" + directories + "examples" theories HOLCF_Main Type_Classes Numeral_Cpo Data_Function Data_Bool Data_Tuple Data_Integer Data_List Data_Maybe Definedness List_Comprehension Num_Class "examples/Fibs" "examples/Sieve_Primes" "examples/GHC_Rewrite_Rules" "examples/HLint" theories [document = false] HOLCF_Prelude document_files "root.bib" "root.tex" diff --git a/thys/HRB-Slicing/ROOT b/thys/HRB-Slicing/ROOT --- a/thys/HRB-Slicing/ROOT +++ b/thys/HRB-Slicing/ROOT @@ -1,8 +1,12 @@ chapter AFP session "HRB-Slicing" (AFP) = Jinja + options [timeout = 2400] + directories + "JinjaVM_Inter" + "Proc" + "StaticInter" theories HRBSlicing document_files "root.tex" diff --git a/thys/Heard_Of/ROOT b/thys/Heard_Of/ROOT --- a/thys/Heard_Of/ROOT +++ b/thys/Heard_Of/ROOT @@ -1,24 +1,31 @@ chapter AFP session Heard_Of (AFP) = HOL + options [timeout = 600] sessions "HOL-Library" Stuttering_Equivalence + directories + "ate" + "eigbyz" + "lastvoting" + "otr" + "ute" + "uv" theories (* generic model and reduction theorem *) HOModel Reduction (* utility lemmas about majorities *) Majorities (* algorithms for benign faults *) "otr/OneThirdRuleProof" "uv/UvProof" "lastvoting/LastVotingProof" (* algorithms for Byzantine faults *) "ute/UteProof" "ate/AteProof" "eigbyz/EigbyzProof" document_files "root.bib" "root.tex" diff --git a/thys/Hoare_Time/ROOT b/thys/Hoare_Time/ROOT --- a/thys/Hoare_Time/ROOT +++ b/thys/Hoare_Time/ROOT @@ -1,13 +1,15 @@ chapter AFP session Hoare_Time (AFP) = "HOL" + options [timeout = 600] sessions "Separation_Algebra" "HOL-Library" "HOL-Eisbach" + directories + "SepLogAdd" theories Hoare_Time document_files "root.bib" "root.tex" diff --git a/thys/Hybrid_Multi_Lane_Spatial_Logic/ROOT b/thys/Hybrid_Multi_Lane_Spatial_Logic/ROOT --- a/thys/Hybrid_Multi_Lane_Spatial_Logic/ROOT +++ b/thys/Hybrid_Multi_Lane_Spatial_Logic/ROOT @@ -1,11 +1,14 @@ chapter AFP session Hybrid_Multi_Lane_Spatial_Logic (AFP) = HOL + options [timeout = 600] + directories + "perfect" + "regular" theories HMLSL "perfect/Safety_Perfect" "regular/Safety_Regular" document_files "root.tex" "root.bib" diff --git a/thys/IMP2/ROOT b/thys/IMP2/ROOT --- a/thys/IMP2/ROOT +++ b/thys/IMP2/ROOT @@ -1,23 +1,29 @@ chapter AFP session IMP2 (AFP) = HOL + options [timeout = 600] sessions "HOL-Library" "HOL-Eisbach" + directories + "automation" + "basic" + "doc" + "lib" + "parser" theories [document = false] "lib/IMP2_Aux_Lemmas" "lib/IMP2_Utils" "lib/Named_Simpsets" "lib/Subgoal_Focus_Some" theories "basic/Syntax" "basic/Semantics" "basic/Annotated_Syntax" theories [document = false] "IMP2" theories "doc/Quickstart_Guide" "doc/IMP2_from_IMP" "doc/Examples" document_files "root.tex" diff --git a/thys/Inductive_Confidentiality/ROOT b/thys/Inductive_Confidentiality/ROOT --- a/thys/Inductive_Confidentiality/ROOT +++ b/thys/Inductive_Confidentiality/ROOT @@ -1,19 +1,22 @@ chapter AFP session Inductive_Confidentiality (AFP) = HOL + options [timeout = 600] + directories + "DolevYao" + "GeneralAttacker" theories "DolevYao/Message" "DolevYao/Event" "DolevYao/Public" "DolevYao/NS_Public_Bad" "DolevYao/ConfidentialityDY" "GeneralAttacker/MessageGA" "GeneralAttacker/EventGA" "GeneralAttacker/PublicGA" "GeneralAttacker/NS_Public_Bad_GA" "GeneralAttacker/ConfidentialityGA" "GeneralAttacker/Knowledge" document_files "root.bib" "root.tex" diff --git a/thys/Isabelle_Meta_Model/ROOT b/thys/Isabelle_Meta_Model/ROOT --- a/thys/Isabelle_Meta_Model/ROOT +++ b/thys/Isabelle_Meta_Model/ROOT @@ -1,30 +1,43 @@ chapter AFP session Isabelle_Meta_Model (AFP) = "HOL-Library" + description "Isabelle_Meta_Model containing a Toy Example" options [timeout = 600] + directories + "document" + "isabelle_home/src/HOL" + "isabelle_home/src/HOL/ex" + "isabelle_home/src/Pure/Isar" + "isabelle_home/src/Tools/Code" + "meta_isabelle" + "toy_example" + "toy_example/document_generated" + "toy_example/embedding" + "toy_example/embedding/core" + "toy_example/embedding/meta_toy" + "toy_example/generator" theories [document = false] "isabelle_home/src/HOL/Isabelle_Main0" "isabelle_home/src/HOL/Isabelle_Main1" "isabelle_home/src/HOL/Isabelle_Main2" theories "meta_isabelle/Parser_Pure" "meta_isabelle/Meta_Isabelle" "meta_isabelle/Printer_Isabelle" theories [document = false] "toy_example/embedding/Printer" theories "toy_example/embedding/Generator_static" "toy_example/embedding/Generator_dynamic_sequential" "toy_example/generator/Design_deep" "toy_example/generator/Design_shallow" "document/Rail" theories (* This part ensures that generated theories are accepted: in general, if X..._generated_generated.thy is wellformed then we also have X..._generated.thy wellformed *) "toy_example/document_generated/Design_generated" "toy_example/document_generated/Design_generated_generated" document_files "root.bib" "root.tex" diff --git a/thys/Jinja/ROOT b/thys/Jinja/ROOT --- a/thys/Jinja/ROOT +++ b/thys/Jinja/ROOT @@ -1,12 +1,19 @@ chapter AFP session Jinja (AFP) = "HOL-Library" + options [timeout = 1200] sessions "List-Index" + directories + "BV" + "Common" + "Compiler" + "DFA" + "J" + "JVM" theories Jinja document_files "introduction.tex" "root.bib" "root.tex" diff --git a/thys/JinjaThreads/ROOT b/thys/JinjaThreads/ROOT --- a/thys/JinjaThreads/ROOT +++ b/thys/JinjaThreads/ROOT @@ -1,22 +1,34 @@ chapter AFP session JinjaThreads (AFP slow) = HOL + options [timeout = 28800] sessions "HOL-Word" "Binomial-Heaps" "Finger-Trees" Automatic_Refinement Coinductive Collections FinFun Native_Word Refine_Monadic Trie + directories + "BV" + "Basic" + "Common" + "Compiler" + "DFA" + "Examples" + "Execute" + "Framework" + "J" + "JVM" + "MM" theories [document = false] "Basic/Basic_Main" theories JinjaThreads document_files "root.bib" "root.tex" diff --git a/thys/JiveDataStoreModel/ROOT b/thys/JiveDataStoreModel/ROOT --- a/thys/JiveDataStoreModel/ROOT +++ b/thys/JiveDataStoreModel/ROOT @@ -1,25 +1,30 @@ chapter AFP session JiveDataStoreModel (AFP) = HOL + options [timeout = 600] + directories + "Isa_Counter" + "Isa_Counter_Store" + "Isabelle" + "Isabelle_Store" theories "Isa_Counter/TypeIds" "Isabelle/JavaType" "Isa_Counter/DirectSubtypes" "Isabelle/Subtype" "Isa_Counter_Store/Attributes" "Isabelle_Store/AttributesIndep" "Isabelle/Value" "Isabelle_Store/Location" "Isabelle_Store/Store" "Isabelle_Store/StoreProperties" "Isabelle/JML" "Isa_Counter/UnivSpec" document_files "Counter.java" "TypeHierarchy.eps" "TypeHierarchy.pdf" "my_logic.sty" "prooftree.sty" "root.bib" "root.tex" diff --git a/thys/KAT_and_DRA/ROOT b/thys/KAT_and_DRA/ROOT --- a/thys/KAT_and_DRA/ROOT +++ b/thys/KAT_and_DRA/ROOT @@ -1,18 +1,21 @@ chapter AFP session KAT_and_DRA (AFP) = Kleene_Algebra + options [timeout = 600] + directories + "SingleSorted" + "TwoSorted" theories "SingleSorted/Test_Dioid" "SingleSorted/Conway_Tests" "SingleSorted/KAT" "SingleSorted/DRAT" "SingleSorted/DRA_Models" "SingleSorted/KAT_Models" "SingleSorted/FolkTheorem" "SingleSorted/PHL_KAT" "SingleSorted/PHL_DRAT" "TwoSorted/KAT2" "TwoSorted/DRAT2" document_files "root.tex" "root.bib" diff --git a/thys/LOFT/ROOT b/thys/LOFT/ROOT --- a/thys/LOFT/ROOT +++ b/thys/LOFT/ROOT @@ -1,24 +1,27 @@ chapter AFP session LOFT (AFP) = Iptables_Semantics + options [timeout = 1200] + directories + "Examples/OF_conv_test" + "Examples/RFC2544" theories [document = false] OpenFlow_Helpers (* just some helper lemmas *) List_Group Sort_Descending theories OpenFlow_Action OpenFlow_Matches OpenFlow_Serialize Semantics_OpenFlow Featherweight_OpenFlow_Comparison LinuxRouter_OpenFlow_Translation "Examples/OF_conv_test/OF_conv_test" "Examples/RFC2544/RFC2544" OpenFlow_Documentation document_files "root.tex" "chap3.tex" "root.bib" "moeptikz.sty" "bench.csv" diff --git a/thys/LTL/ROOT b/thys/LTL/ROOT --- a/thys/LTL/ROOT +++ b/thys/LTL/ROOT @@ -1,19 +1,20 @@ chapter AFP session LTL (AFP) = "HOL-Library" + options [timeout = 600] sessions Boolean_Expression_Checkers + directories + "example" theories LTL Rewriting Equivalence_Relations Disjunctive_Normal_Form Code_Equations - "example/Example" document_files "root.tex" "root.bib" export_files (in "example") [2] "LTL.Example:**" diff --git a/thys/LTL_Master_Theorem/ROOT b/thys/LTL_Master_Theorem/ROOT --- a/thys/LTL_Master_Theorem/ROOT +++ b/thys/LTL_Master_Theorem/ROOT @@ -1,21 +1,24 @@ chapter AFP session LTL_Master_Theorem (AFP) = "Transition_Systems_and_Automata" + options [timeout = 600] sessions LTL Deriving + directories + "Logical_Characterization" + "LTL_to_DRA" theories "Logical_Characterization/Master_Theorem" "Logical_Characterization/Asymmetric_Master_Theorem" "LTL_to_DRA/DRA_Construction" "LTL_to_DRA/DRA_Instantiation" "LTL_to_DRA/DRA_Implementation" Code_Export document_files "root.tex" "root.bib" export_files (in ".") [1] "LTL_Master_Theorem.Code_Export:**" diff --git a/thys/LTL_to_DRA/ROOT b/thys/LTL_to_DRA/ROOT --- a/thys/LTL_to_DRA/ROOT +++ b/thys/LTL_to_DRA/ROOT @@ -1,15 +1,18 @@ chapter AFP session LTL_to_DRA (AFP) = LTL + options [timeout = 600] sessions "List-Index" Boolean_Expression_Checkers KBPs + directories + "Auxiliary" + "Impl" theories LTL_Rabin LTL_Rabin_Unfold_Opt "Impl/Export_Code" document_files "root.tex" "root.bib" diff --git a/thys/LinearQuantifierElim/ROOT b/thys/LinearQuantifierElim/ROOT --- a/thys/LinearQuantifierElim/ROOT +++ b/thys/LinearQuantifierElim/ROOT @@ -1,20 +1,22 @@ chapter AFP session LinearQuantifierElim (AFP) = "HOL-Library" + options [timeout = 600] + directories + "Thys" theories "Thys/QEdlo" "Thys/QEdlo_ex" "Thys/QEdlo_fr" "Thys/QEdlo_inf" "Thys/QElin_opt" "Thys/FRE" "Thys/QElin_inf" "Thys/QEpres" "Thys/Cooper" theories [document = false] "Thys/CertDlo" "Thys/CertLin" document_files "root.bib" "root.tex" diff --git a/thys/List-Infinite/ROOT b/thys/List-Infinite/ROOT --- a/thys/List-Infinite/ROOT +++ b/thys/List-Infinite/ROOT @@ -1,8 +1,12 @@ chapter AFP session "List-Infinite" (AFP) = "HOL-Library" + options [timeout = 600] + directories + "CommonArith" + "CommonSet" + "ListInf" theories ListInfinite document_files "root.tex" diff --git a/thys/Locally-Nameless-Sigma/ROOT b/thys/Locally-Nameless-Sigma/ROOT --- a/thys/Locally-Nameless-Sigma/ROOT +++ b/thys/Locally-Nameless-Sigma/ROOT @@ -1,10 +1,13 @@ chapter AFP session "Locally-Nameless-Sigma" (AFP) = HOL + options [timeout = 600] sessions Applicative_Lifting + directories + "preliminary" + "Sigma" theories Locally_Nameless_Sigma document_files "root.tex" diff --git a/thys/Markov_Models/ROOT b/thys/Markov_Models/ROOT --- a/thys/Markov_Models/ROOT +++ b/thys/Markov_Models/ROOT @@ -1,22 +1,24 @@ chapter AFP session Markov_Models (AFP) = "HOL-Probability" + options [timeout = 600] sessions Coinductive "Gauss-Jordan-Elim-Fun" + directories + "ex" theories Markov_Models "ex/Example_A" "ex/Example_B" "ex/PCTL" "ex/PGCL" "ex/Crowds_Protocol" "ex/Zeroconf_Analysis" "ex/Gossip_Broadcast" "ex/MDP_RP_Certification" theories [document = false] "ex/MDP_RP" document_files "root.bib" "root.tex" diff --git a/thys/Modular_Assembly_Kit_Security/ROOT b/thys/Modular_Assembly_Kit_Security/ROOT --- a/thys/Modular_Assembly_Kit_Security/ROOT +++ b/thys/Modular_Assembly_Kit_Security/ROOT @@ -1,36 +1,43 @@ chapter AFP session Modular_Assembly_Kit_Security (AFP) = HOL + description " An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties Author: Oliver Bracevac, TU Darmstadt Author: Richard Gay, TU Darmstadt Author: Sylvia Grewe, TU Darmstadt Author: Heiko Mantel, TU Darmstadt Author: Henning Sudbrock, TU Darmstadt Author: Markus Tasch, TU Darmstadt " options [timeout = 600] + directories + "Basics" + "SystemSpecification" + "SecuritySpecification" + "Verification/Basics" + "Verification/Unwinding" + "Verification/Compositionality" theories "Basics/Projection" "Basics/Prefix" "SystemSpecification/EventSystems" "SystemSpecification/StateEventSystems" "SecuritySpecification/Views" "SecuritySpecification/FlowPolicies" "SecuritySpecification/InformationFlowProperties" "SecuritySpecification/BasicSecurityPredicates" "SecuritySpecification/PropertyLibrary" "Verification/Basics/BSPTaxonomy" "Verification/Basics/SecureSystems" "Verification/Unwinding/UnwindingConditions" "Verification/Unwinding/AuxiliaryLemmas" "Verification/Unwinding/UnwindingResults" "Verification/Compositionality/CompositionBase" "Verification/Compositionality/CompositionSupport" "Verification/Compositionality/GeneralizedZippingLemma" "Verification/Compositionality/CompositionalityResults" document_files "root.bib" "root.tex" diff --git a/thys/Monad_Memo_DP/ROOT b/thys/Monad_Memo_DP/ROOT --- a/thys/Monad_Memo_DP/ROOT +++ b/thys/Monad_Memo_DP/ROOT @@ -1,14 +1,20 @@ chapter AFP session Monad_Memo_DP (AFP) = HOL + options [timeout = 1200] sessions "HOL-Library" "HOL-Eisbach" "HOL-Imperative_HOL" "Show" + directories + "example" + "heap_monad" + "state_monad" + "transform" + "util" theories "example/All_Examples" document_files "root.tex" "root.bib" diff --git a/thys/Network_Security_Policy_Verification/ROOT b/thys/Network_Security_Policy_Verification/ROOT --- a/thys/Network_Security_Policy_Verification/ROOT +++ b/thys/Network_Security_Policy_Verification/ROOT @@ -1,39 +1,44 @@ chapter AFP session "Network_Security_Policy_Verification" (AFP) = HOL + options [timeout = 3600] sessions "HOL-Library" "HOL-Lattice" "Transitive-Closure" Automatic_Refinement + directories + "Lib" + "Security_Invariants" + "Examples" + "Examples/Tainting" theories [document = false] "Lib/ML_GraphViz_Disable" "Lib/FiniteListGraph_Impl" "Lib/FiniteListGraph" "Lib/Efficient_Distinct" theories "Security_Invariants/SINVAR_Subnets2" "Security_Invariants/SINVAR_BLPstrict" "Security_Invariants/Analysis_Tainting" Network_Security_Policy_Verification TopoS_generateCode theories [document = false] attic "Examples/Impl_List_Playground_statefulpolicycompliance" "Examples/Example" "Examples/Example_NetModel" "Examples/Example_Forte14" "Examples/Distributed_WebApp" "Examples/I8_SSH_Landscape" "Examples/Impl_List_Playground" "Examples/Impl_List_Playground_ChairNetwork_statefulpolicy_example" "Examples/Tainting/CryptoDB" "Examples/Tainting/IDEM" "Examples/Tainting/MeasrDroid" theories SINVAR_Examples "Examples/Imaginary_Factory_Network" document_files "root.bib" "root.tex" diff --git a/thys/Partial_Order_Reduction/ROOT b/thys/Partial_Order_Reduction/ROOT --- a/thys/Partial_Order_Reduction/ROOT +++ b/thys/Partial_Order_Reduction/ROOT @@ -1,13 +1,16 @@ chapter AFP session Partial_Order_Reduction (AFP) = Transition_Systems_and_Automata + options [timeout = 600] sessions Coinductive Stuttering_Equivalence + directories + "Basics" + "Extensions" theories Ample_Correctness Ample_Analysis document_files "root.tex" "root.bib" diff --git a/thys/Planarity_Certificates/ROOT b/thys/Planarity_Certificates/ROOT --- a/thys/Planarity_Certificates/ROOT +++ b/thys/Planarity_Certificates/ROOT @@ -1,17 +1,22 @@ chapter AFP session Planarity_Certificates (AFP) = Simpl + options [timeout = 600] sessions "HOL-Eisbach" "List-Index" "Transitive-Closure" Case_Labeling Graph_Theory + directories + "l4v/lib" + "l4v/lib/wp" + "Planarity" + "Verification" theories [document = false] "l4v/lib/OptionMonadWP" theories Planarity_Certificates document_files "root.tex" "root.bib" diff --git a/thys/Probabilistic_Timed_Automata/ROOT b/thys/Probabilistic_Timed_Automata/ROOT --- a/thys/Probabilistic_Timed_Automata/ROOT +++ b/thys/Probabilistic_Timed_Automata/ROOT @@ -1,15 +1,17 @@ chapter AFP session Probabilistic_Timed_Automata (AFP) = "Markov_Models" + options [timeout = 1200] sessions "Timed_Automata" "HOL-Eisbach" + directories + "library" theories [document = false] "library/Lib" theories "PTA" "PTA_Reachability" document_files "root.tex" "root.bib" diff --git a/thys/Randomised_Social_Choice/ROOT b/thys/Randomised_Social_Choice/ROOT --- a/thys/Randomised_Social_Choice/ROOT +++ b/thys/Randomised_Social_Choice/ROOT @@ -1,12 +1,14 @@ chapter AFP session Randomised_Social_Choice (AFP) = "HOL-Probability" + options [timeout = 300] sessions "List-Index" + directories + "Automation" theories Randomised_Social_Choice "Automation/SDS_Automation" document_files "root.tex" "root.bib" diff --git a/thys/Refine_Imperative_HOL/ROOT b/thys/Refine_Imperative_HOL/ROOT --- a/thys/Refine_Imperative_HOL/ROOT +++ b/thys/Refine_Imperative_HOL/ROOT @@ -1,86 +1,100 @@ chapter AFP session Sepref_Prereq (AFP) in "Sepref_Prereq" = Collections + options [timeout = 300] sessions "HOL-Library" "HOL-Imperative_HOL" Separation_Logic_Imperative_HOL theories Separation_Logic_Imperative_HOL.Sep_Examples session Refine_Imperative_HOL (AFP) = Sepref_Prereq + options [timeout = 1200] sessions Isar_Ref "HOL-Eisbach" "List-Index" Collections_Examples DFS_Framework Dijkstra_Shortest_Path + directories + "Examples" + "Examples/Snippets" + "IICF" + "IICF/Impl" + "IICF/Impl/Heaps" + "IICF/Intf" + "Lib" + "Userguides" + "benchmarks" + "benchmarks/Dijkstra/isabelle" + "benchmarks/Heapmap/isabelle" + "benchmarks/NestedDFS/isabelle" + theories [document = false] "Lib/Concl_Pres_Clarification" "Lib/Named_Theorems_Rev" "Lib/Pf_Add" "Lib/Pf_Mono_Prover" "Lib/PO_Normalizer" "Lib/Sepref_Misc" "Lib/Structured_Apply" "Lib/Term_Synth" "Lib/User_Smashing" "HOL-Library.Code_Target_Numeral" DFS_Framework.DFS_Framework_Refine_Aux Isar_Ref.Base theories Sepref_Chapter_Tool Sepref_Tool Sepref_Chapter_Setup Sepref "IICF/Sepref_Chapter_IICF" "IICF/IICF" "Userguides/Sepref_Chapter_Userguides" "Userguides/Sepref_Guide_Quickstart" "Userguides/Sepref_Guide_Reference" "Userguides/Sepref_Guide_General_Util" theories [document = false] Dijkstra_Shortest_Path.Dijkstra Dijkstra_Shortest_Path.Test Collections_Examples.Nested_DFS "Examples/Sepref_WGraph" theories "Examples/Sepref_Chapter_Examples" "Examples/Sepref_All_Examples" "benchmarks/Sepref_Chapter_Benchmarks" "benchmarks/Heapmap/isabelle/Heapmap_Bench" "benchmarks/Dijkstra/isabelle/Dijkstra_Benchmark" "benchmarks/NestedDFS/isabelle/NDFS_Benchmark" document_files "root.tex" (* Smaller Sessions: *) session Sepref_Basic (AFP) in "Sepref_Basic" = Sepref_Prereq + options [timeout = 300] sessions "HOL-Eisbach" "List-Index" Refine_Imperative_HOL theories Refine_Imperative_HOL.Sepref session Sepref_IICF (AFP) in "Sepref_IICF" = Sepref_Basic + options [timeout = 600] sessions Refine_Imperative_HOL theories Refine_Imperative_HOL.IICF diff --git a/thys/Refine_Monadic/ROOT b/thys/Refine_Monadic/ROOT --- a/thys/Refine_Monadic/ROOT +++ b/thys/Refine_Monadic/ROOT @@ -1,12 +1,15 @@ chapter AFP session Refine_Monadic (AFP) = Automatic_Refinement + options [timeout = 1200] sessions "HOL-Word" + directories + "Generic" + "examples" theories Refine_Monadic "examples/Examples" document_files "root.bib" "root.tex" diff --git a/thys/SPARCv8/ROOT b/thys/SPARCv8/ROOT --- a/thys/SPARCv8/ROOT +++ b/thys/SPARCv8/ROOT @@ -1,14 +1,18 @@ chapter AFP session SPARCv8 (AFP) = "HOL-Word" + options [timeout = 1200] sessions "HOL-Eisbach" + directories + "lib" + "lib/wp" + "SparcModel_MMU" theories [document = false] "lib/WordDecl" theories "SparcModel_MMU/Sparc_Properties" theories [document = false] "SparcModel_MMU/Sparc_Code_Gen" document_files "root.tex" diff --git a/thys/Security_Protocol_Refinement/ROOT b/thys/Security_Protocol_Refinement/ROOT --- a/thys/Security_Protocol_Refinement/ROOT +++ b/thys/Security_Protocol_Refinement/ROOT @@ -1,101 +1,105 @@ (******************************************************************************* Project: Development of Security Protocols by Refinement Module: ROOT file for session building (Isabelle/HOL 2016-1) ID: $Id: ROOT 134926 2017-05-24 17:53:45Z csprenge $ Author: Christoph Sprenger, ETH Zurich build command example: isabelle build -v -b -d . Copyright (c) 2013-2017 Christoph Sprenger Licence: LGPL *******************************************************************************) chapter AFP session Security_Protocol_Refinement (AFP) = HOL + description "Developing Security Protocols by Stepwise Refinement" options [timeout = 2400] + directories + "Refinement" + "Auth_simple" + "Key_establish" theories (* Infrastructure *) "Refinement/Infra" "Refinement/Refinement" "Refinement/Agents" "Refinement/Keys" "Refinement/Atoms" "Refinement/Runs" "Refinement/Channels" "Refinement/Message" "Refinement/s0g_secrecy" "Refinement/a0n_agree" "Refinement/a0i_agree" (* Authentication protocols *) "Auth_simple/m1_auth" "Auth_simple/m2_auth_chan" "Auth_simple/m2_confid_chan" "Auth_simple/m3_sig" "Auth_simple/m3_enc" (* Key establishment protocols *) "Key_establish/m1_keydist" "Key_establish/m1_keydist_iirn" "Key_establish/m1_keydist_inrn" "Key_establish/m1_kerberos" "Key_establish/m2_kerberos" "Key_establish/m3_kerberos_par" "Key_establish/m3_kerberos5" "Key_establish/m3_kerberos4" "Key_establish/m1_nssk" "Key_establish/m2_nssk" "Key_establish/m3_nssk_par" "Key_establish/m3_nssk" "Key_establish/m1_ds" "Key_establish/m2_ds" "Key_establish/m3_ds_par" "Key_establish/m3_ds" document_files "root.tex" "isapreamble.tex" "session_graph.tex" (* The following sessions were used for producing the statistics for the JCS journal paper "Refining Security Protocols". used command: isabelle build -c -d . (without -b) *) (* session Refinement_timing in Refinement = HOL + description {* Security protocol refinement infrastructure *} options [threads=4] theories Infra Refinement Agents Keys Atoms Runs Channels Message s0g_secrecy a0n_agree a0i_agree session KE_Level1 in Key_establish = Refinement + description {* general Level 1 models *} options [threads=4] theories m1_keydist m1_keydist_iirn m1_keydist_inrn session KE_Kerberos5 in Key_establish = KE_Level1 + description {* Kerberos 5 models *} options [threads=4] theories m1_kerberos m2_kerberos m3_kerberos5 session KE_NSSK in Key_establish = KE_Level1 + description {* NSSK models *} options [threads=4] theories m1_nssk m2_nssk m3_nssk session KE_DS in Key_establish = KE_Level1 + description {* Denning-Sacco models *} options [threads=4] theories m1_ds m2_ds m3_ds *) diff --git a/thys/Separation_Algebra/ROOT b/thys/Separation_Algebra/ROOT --- a/thys/Separation_Algebra/ROOT +++ b/thys/Separation_Algebra/ROOT @@ -1,15 +1,18 @@ chapter AFP session Separation_Algebra (AFP) = "HOL-Word" + options [timeout = 600] sessions "HOL-Hoare" + directories + "ex" + "ex/capDL" theories "ex/Simple_Separation_Example" "ex/Sep_Tactics_Test" "ex/VM_Example" Sep_Eq "ex/capDL/Separation_D" document_files "root.bib" "root.tex" diff --git a/thys/Simpl/ROOT b/thys/Simpl/ROOT --- a/thys/Simpl/ROOT +++ b/thys/Simpl/ROOT @@ -1,13 +1,15 @@ chapter AFP session Simpl (AFP) = HOL + options [timeout = 600] sessions "HOL-Library" "HOL-Statespace" + directories + "ex" theories Simpl document_files "mathpartir.sty" "root.bib" "root.tex" diff --git a/thys/Simple_Firewall/ROOT b/thys/Simple_Firewall/ROOT --- a/thys/Simple_Firewall/ROOT +++ b/thys/Simple_Firewall/ROOT @@ -1,15 +1,18 @@ chapter AFP session Simple_Firewall (AFP) = IP_Addresses + options [timeout = 600] + directories + "Common" + "Primitives" theories Simple_Packet SimpleFw_Syntax SimpleFw_Semantics Generic_SimpleFw Shadowed Service_Matrix SimpleFw_toString document_files "root.tex" "root.bib" diff --git a/thys/Slicing/ROOT b/thys/Slicing/ROOT --- a/thys/Slicing/ROOT +++ b/thys/Slicing/ROOT @@ -1,8 +1,14 @@ chapter AFP session Slicing (AFP) = Jinja + options [timeout = 3600] + directories + "Basic" + "Dynamic" + "JinjaVM" + "StaticIntra" + "While" theories Slicing document_files "root.tex" diff --git a/thys/Sturm_Sequences/ROOT b/thys/Sturm_Sequences/ROOT --- a/thys/Sturm_Sequences/ROOT +++ b/thys/Sturm_Sequences/ROOT @@ -1,17 +1,20 @@ chapter AFP session Sturm_Sequences (AFP) = "HOL-Computational_Algebra" + options [timeout = 600, document_variants = "document:outline=/proof,/ML:userguide"] + directories + "Lib" + "Examples" theories "Lib/Sturm_Library_Document" "Lib/Misc_Polynomial" theories [document = false] "Lib/Sturm_Library" theories Sturm_Theorem Sturm_Method "Examples/Sturm_Ex" document_files "build" "root.tex" "root_userguide.tex" diff --git a/thys/Transition_Systems_and_Automata/ROOT b/thys/Transition_Systems_and_Automata/ROOT --- a/thys/Transition_Systems_and_Automata/ROOT +++ b/thys/Transition_Systems_and_Automata/ROOT @@ -1,26 +1,36 @@ chapter AFP session Transition_Systems_and_Automata (AFP) = "Collections" + options [timeout = 2400] sessions "DFS_Framework" "Gabow_SCC" + directories + "Automata" + "Automata/DBA" + "Automata/DCA" + "Automata/DFA" + "Automata/DRA" + "Automata/NBA" + "Automata/NFA" + "Basic" + "Transition_Systems" theories "Basic/Basic" "Basic/Sequence" "Basic/Sequence_Zip" "Basic/Sequence_LTL" "Basic/Maps" "Basic/Acceptance" "Transition_Systems/Transition_System" "Transition_Systems/Transition_System_Extra" "Transition_Systems/Transition_System_Construction" "Automata/DFA/DFA" "Automata/NFA/NFA" "Automata/NBA/NBA_Translate" "Automata/DBA/DBA_Combine" "Automata/DCA/DCA_Combine" "Automata/DRA/DRA_Combine" "Automata/DRA/DRA_Translate" document_files "root.tex" diff --git a/thys/UPF_Firewall/ROOT b/thys/UPF_Firewall/ROOT --- a/thys/UPF_Firewall/ROOT +++ b/thys/UPF_Firewall/ROOT @@ -1,11 +1,22 @@ chapter AFP session "UPF_Firewall" (AFP) = UPF + description "Formal Network Models and Their Application to Firewall Policies" options [timeout = 600] + directories + "Examples" + "Examples/DMZ" + "Examples/NAT-FW" + "Examples/PersonalFirewall" + "Examples/Transformation" + "Examples/Voice_over_IP" + "FWNormalisation" + "NAT" + "PacketFilter" + "StatefulFW" theories "Examples/Examples" document_files "root.tex" "introduction.tex" "root.bib" diff --git a/thys/UTP/ROOT b/thys/UTP/ROOT --- a/thys/UTP/ROOT +++ b/thys/UTP/ROOT @@ -1,38 +1,41 @@ (******************************************************************************) (* Project: The Isabelle/UTP Proof System *) (* File: ROOT *) (* Authors: Simon Foster and Frank Zeyda (University of York, UK) *) (* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *) (******************************************************************************) chapter AFP (* UTP Mathematical Toolkit *) session "UTP-Toolkit" (AFP) in "toolkit" = "HOL-Algebra" + options [timeout = 600] sessions Optics theories utp_toolkit document_files "root.tex" "root.bib" "document.sty" (* Core UTP Framework *) session "UTP" (AFP) = "UTP-Toolkit" + options [timeout = 600] + directories + "utp" + "utp/examples" theories [document = false] "utp/utp_parser_utils" theories "utp/utp" "utp/utp_full" "utp/utp_easy_parser" "utp/examples/sum_list" "utp/examples/utp_simple_time" document_files "root.bib" "root.tex" "document.sty" diff --git a/thys/VerifyThis2018/ROOT b/thys/VerifyThis2018/ROOT --- a/thys/VerifyThis2018/ROOT +++ b/thys/VerifyThis2018/ROOT @@ -1,15 +1,17 @@ chapter AFP session VerifyThis2018 (AFP) = Sepref_IICF + options [timeout = 600] + directories + "lib" theories [document = false] "lib/VTcomp" "lib/DF_System" Snippets theories Challenge1 Challenge1_short Challenge2 Challenge3 document_files "root.tex" diff --git a/thys/WebAssembly/ROOT b/thys/WebAssembly/ROOT --- a/thys/WebAssembly/ROOT +++ b/thys/WebAssembly/ROOT @@ -1,17 +1,18 @@ chapter AFP session WebAssembly (AFP) = "HOL-Library" + options [timeout=600] sessions "Native_Word" + directories + "Wasm_Printing" theories "Wasm_Soundness" "Wasm_Checker_Properties" "Wasm_Interpreter_Properties" theories [document = false] "Wasm_Printing/Wasm_Printing" "Wasm_Printing/Wasm_Interpreter_Printing_Pure" document_files "root.bib" "root.tex" - diff --git a/thys/pGCL/ROOT b/thys/pGCL/ROOT --- a/thys/pGCL/ROOT +++ b/thys/pGCL/ROOT @@ -1,12 +1,14 @@ chapter AFP session pGCL (AFP) = "HOL-Analysis" + options [timeout = 300] + directories + "Tutorial" theories pGCL "Tutorial/Primitives" "Tutorial/LoopExamples" "Tutorial/Monty" document_files "root.tex" "root.bib"