diff --git a/thys/CakeML/ROOT b/thys/CakeML/ROOT --- a/thys/CakeML/ROOT +++ b/thys/CakeML/ROOT @@ -1,66 +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] + options [timeout = 3600] 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/Collections/ROOT b/thys/Collections/ROOT --- a/thys/Collections/ROOT +++ b/thys/Collections/ROOT @@ -1,189 +1,189 @@ chapter AFP session Collections (AFP) = Refine_Monadic + - options [timeout = 1200, document_variants = "document:outline=/proof,/ML:userguide"] + options [timeout = 2100, document_variants = "document:outline=/proof,/ML:userguide"] sessions "Binomial-Heaps" "Finger-Trees" Native_Word Trie directories "GenCF" "GenCF/Gen" "GenCF/Impl" "GenCF/Intf" "ICF" "ICF/gen_algo" "ICF/impl" "ICF/spec" "ICF/tools" "Iterator" "Lib" "Userguides" theories [document = false] (* Prerequisites *) "HOL-Library.Code_Target_Numeral" "HOL-Library.While_Combinator" "Binomial-Heaps.BinomialHeap" "Binomial-Heaps.SkewBinomialHeap" "Finger-Trees.FingerTree" Automatic_Refinement.Automatic_Refinement Refine_Monadic.Refine_Monadic (* Libraries and Tools *) "Lib/Sorted_List_Operations" "Lib/HashCode" "Lib/Code_Target_ICF" "Lib/RBT_add" "Lib/Dlist_add" "Lib/Assoc_List" "Lib/Diff_Array" "Lib/Partial_Equivalence_Relation" "Lib/Robdd" "ICF/tools/Locale_Code" "ICF/tools/ICF_Tools" "ICF/tools/Locale_Code_Ex" "ICF/tools/Record_Intf" "ICF/tools/Ord_Code_Preproc" (* Deprecated *) "ICF/DatRef" (* Iterators *) "Iterator/Idx_Iterator" "Iterator/SetIteratorOperations" "Iterator/Iterator" "Iterator/Proper_Iterator" "Iterator/Gen_Iterator" "Iterator/SetIteratorGA" "Iterator/SetAbstractionIterator" "Iterator/SetIterator" "Iterator/It_to_It" (* GenCF *) theories "GenCF/GenCF_Chapter" "GenCF/Intf/GenCF_Intf_Chapter" "GenCF/Intf/Intf_Map" "GenCF/Intf/Intf_Set" "GenCF/Intf/Intf_Hash" "GenCF/Intf/Intf_Comp" "GenCF/Gen/GenCF_Gen_Chapter" "GenCF/Gen/Gen_Set" "GenCF/Gen/Gen_Map" "GenCF/Gen/Gen_Map2Set" "GenCF/Gen/Gen_Comp" "GenCF/Impl/GenCF_Impl_Chapter" "GenCF/Impl/Impl_Array_Stack" "GenCF/Impl/Impl_List_Set" "GenCF/Impl/Impl_Array_Hash_Map" "GenCF/Impl/Impl_RBT_Map" "GenCF/Impl/Impl_List_Map" "GenCF/Impl/Impl_Cfun_Set" "GenCF/Impl/Impl_Array_Map" theories [document = false] "GenCF/GenCF" (* ICF *) theories "ICF/ICF_Chapter" "ICF/spec/ICF_Spec_Chapter" "ICF/spec/MapSpec" "ICF/spec/SetSpec" "ICF/spec/ListSpec" "ICF/spec/AnnotatedListSpec" "ICF/spec/PrioSpec" "ICF/spec/PrioUniqueSpec" "ICF/gen_algo/ICF_Gen_Algo_Chapter" "ICF/gen_algo/MapGA" "ICF/gen_algo/SetGA" "ICF/gen_algo/SetByMap" "ICF/gen_algo/ListGA" "ICF/gen_algo/SetIndex" "ICF/gen_algo/Algos" "ICF/gen_algo/PrioByAnnotatedList" "ICF/gen_algo/PrioUniqueByAnnotatedList" "ICF/impl/ICF_Impl_Chapter" "ICF/impl/MapStdImpl" "ICF/impl/SetStdImpl" "ICF/impl/Fifo" "ICF/impl/BinoPrioImpl" "ICF/impl/SkewPrioImpl" "ICF/impl/FTAnnotatedListImpl" "ICF/impl/FTPrioImpl" "ICF/impl/FTPrioUniqueImpl" theories [document = false] "ICF/ICF_Refine_Monadic" "ICF/ICF_Autoref" theories "ICF/ICF_Entrypoints_Chapter" "ICF/Collections" "ICF/CollectionsV1" (* Overall Entry-Points *) Collections_Entrypoints_Chapter Refine_Dflt Refine_Dflt_ICF Refine_Dflt_Only_ICF (* Userguides *) "Userguides/Userguides_Chapter" "Userguides/Refine_Monadic_Userguide" "Userguides/ICF_Userguide" document_files "conclusion.tex" "documentation.tex" "intro.tex" "root.bib" "root.tex" "root_userguide.bib" "root_userguide.tex" session Collections_Examples (AFP) in "Examples" = Collections + options [timeout = 1200] sessions CAVA_Automata Containers directories "Autoref" "Refine_Monadic" "ICF" (* Examples *) theories "Examples_Chapter" "Autoref/Collection_Autoref_Examples_Chapter" "Autoref/Collection_Autoref_Examples" "Refine_Monadic/Refine_Monadic_Examples_Chapter" "Refine_Monadic/Refine_Monadic_Examples" "ICF/ICF_Examples_Chapter" "ICF/ICF_Examples" theories [document = false] "ICF/PerformanceTest" theories [document = false] (* Just in case we forgot something *) "Collection_Examples" document_files (in "../document") "conclusion.tex" "documentation.tex" "intro.tex" "root.bib" "root.tex" "root_userguide.bib" "root_userguide.tex" diff --git a/thys/Linear_Programming/ROOT b/thys/Linear_Programming/ROOT --- a/thys/Linear_Programming/ROOT +++ b/thys/Linear_Programming/ROOT @@ -1,15 +1,15 @@ chapter AFP session Linear_Programming (AFP) = Jordan_Normal_Form + - options [timeout = 600] + options [timeout = 1200] sessions Farkas Linear_Inequalities theories "More_Jordan_Normal_Forms" "Matrix_LinPoly" "LP_Preliminaries" "Linear_Programming" document_files "root.tex" "root.bib" diff --git a/thys/Native_Word/ROOT b/thys/Native_Word/ROOT --- a/thys/Native_Word/ROOT +++ b/thys/Native_Word/ROOT @@ -1,37 +1,37 @@ chapter AFP session "Native_Word" (AFP) = "HOL-Word" + - options [timeout = 1200] + options [timeout = 2400] sessions "HOL-Imperative_HOL" theories Code_Target_Bits_Int Uint64 Uint32 Uint16 Uint8 Uint Native_Cast Native_Cast_Uint Native_Word_Imperative_HOL Native_Word_Test_Emu Native_Word_Test_PolyML Native_Word_Test_PolyML2 Native_Word_Test_PolyML64 Native_Word_Test_Scala theories [condition = ISABELLE_GHC] Native_Word_Test_GHC theories [condition = ISABELLE_MLTON] Native_Word_Test_MLton Native_Word_Test_MLton2 theories [condition = ISABELLE_OCAMLFIND] Native_Word_Test_OCaml Native_Word_Test_OCaml2 theories [condition = ISABELLE_SMLNJ] Native_Word_Test_SMLNJ Native_Word_Test_SMLNJ2 theories Uint_Userguide document_files "root.tex" "root.bib"