merged
authortraytel
Fri, 16 Sep 2016 16:37:11 +0200
changeset 63892 c17733350344
parent 63891 8947157ca830 (current diff)
parent 63890 3dd6bde2502d (diff)
child 63893 c181a84eb6de
merged
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 16:33:24 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 16:37:11 2016 +0200
@@ -4,7 +4,7 @@
   import isabelle._
 
   def threads = 8
-  def jobs = 2
+  def jobs = 1
   def include = Nil
   def select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks"))
 
@@ -12,6 +12,6 @@
   def post_hook(results: Build.Results) = {}
 
   def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
-    tree.selection()
+    tree.selection(session_groups = List("timing"))
 
 }
--- a/src/HOL/ROOT	Fri Sep 16 16:33:24 2016 +0200
+++ b/src/HOL/ROOT	Fri Sep 16 16:37:11 2016 +0200
@@ -14,7 +14,7 @@
     "root.bib"
     "root.tex"
 
-session "HOL-Proofs" = Pure +
+session "HOL-Proofs" (timing) = Pure +
   description {*
     HOL-Main with explicit proof terms.
   *}
@@ -26,7 +26,7 @@
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
-session "HOL-Library" (main) in Library = HOL +
+session "HOL-Library" (main timing) in Library = HOL +
   description {*
     Classical Higher-order Logic -- batteries included.
   *}
@@ -119,7 +119,7 @@
     Com
   document_files "root.tex"
 
-session "HOL-IMP" in IMP = HOL +
+session "HOL-IMP" (timing) in IMP = HOL +
   options [document_variants = document]
   theories [document = false]
     "~~/src/HOL/Library/While_Combinator"
@@ -176,7 +176,7 @@
   options [document = false]
   theories EvenOdd
 
-session "HOL-Data_Structures" in Data_Structures = HOL +
+session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   theories [document = false]
     "Less_False"
@@ -199,7 +199,7 @@
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
-session "HOL-Number_Theory" in Number_Theory = HOL +
+session "HOL-Number_Theory" (timing) in Number_Theory = HOL +
   description {*
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
@@ -247,7 +247,7 @@
   theories Hoare
   document_files "root.bib" "root.tex"
 
-session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
+session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
   description {*
     Verification of shared-variable imperative programs a la Owicki-Gries.
     (verification conditions are generated automatically).
@@ -276,7 +276,7 @@
   theories [condition = "ISABELLE_SMLNJ"]
     Code_Test_SMLNJ
 
-session "HOL-Metis_Examples" in Metis_Examples = HOL +
+session "HOL-Metis_Examples" (timing) in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
@@ -303,7 +303,7 @@
   options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
-session "HOL-Algebra" (main) in Algebra = HOL +
+session "HOL-Algebra" (main timing) in Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
@@ -327,7 +327,7 @@
     UnivPoly             (* Polynomials *)
   document_files "root.bib" "root.tex"
 
-session "HOL-Auth" in Auth = HOL +
+session "HOL-Auth" (timing) in Auth = HOL +
   description {*
     A new approach to verifying authentication protocols.
   *}
@@ -339,7 +339,7 @@
     "Guard/Auth_Guard_Public"
   document_files "root.tex"
 
-session "HOL-UNITY" in UNITY = "HOL-Auth" +
+session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -401,7 +401,7 @@
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
-session "HOL-Decision_Procs" in Decision_Procs = HOL +
+session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL +
   description {*
     Various decision procedures, typically involving reflection.
   *}
@@ -415,7 +415,7 @@
     Proof_Terms
     XML_Data
 
-session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
+session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
@@ -433,7 +433,7 @@
     Euclid
   document_files "root.bib" "root.tex"
 
-session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
+session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   description {*
     Lambda Calculus in de Bruijn's Notation.
 
@@ -467,7 +467,7 @@
   options [document = false]
   theories Test Type
 
-session "HOL-MicroJava" in MicroJava = HOL +
+session "HOL-MicroJava" (timing) in MicroJava = HOL +
   description {*
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
@@ -489,7 +489,7 @@
   theories Example
   document_files "root.bib" "root.tex"
 
-session "HOL-Bali" in Bali = HOL +
+session "HOL-Bali" (timing) in Bali = HOL +
   theories
     AxExample
     AxSound
@@ -671,7 +671,7 @@
     Examples
     Examples_FOL
 
-session "HOL-SET_Protocol" in SET_Protocol = HOL +
+session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   description {*
     Verification of the SET Protocol.
   *}
@@ -723,7 +723,7 @@
   theories
     ATP_Problem_Import
 
-session "HOL-Analysis" (main) in Analysis = HOL +
+session "HOL-Analysis" (main timing) in Analysis = HOL +
   theories
     Analysis
   document_files
@@ -733,7 +733,7 @@
   theories
     Approximations
 
-session "HOL-Probability" in "Probability" = "HOL-Analysis" +
+session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
@@ -744,7 +744,7 @@
     Probability
   document_files "root.tex"
 
-session "HOL-Probability-ex" in "Probability/ex" = "HOL-Probability" +
+session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   theories
     "Dining_Cryptographers"
     "Koepf_Duermuth_Countermeasure"
@@ -754,7 +754,7 @@
   options [document = false]
   theories Nominal
 
-session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
+session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   options [document = false]
   theories
     Class3
@@ -780,7 +780,7 @@
   theories [quick_and_dirty]
     VC_Condition
 
-session "HOL-Cardinals" in Cardinals = HOL +
+session "HOL-Cardinals" (timing) in Cardinals = HOL +
   description {*
     Ordinals and Cardinals, Full Theories.
   *}
@@ -793,7 +793,7 @@
     "root.tex"
     "root.bib"
 
-session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
+session "HOL-Datatype_Examples" (timing) in Datatype_Examples = HOL +
   description {*
     (Co)datatype Examples.
   *}
@@ -814,7 +814,7 @@
     Misc_Primcorec
     Misc_Primrec
 
-session "HOL-Corec_Examples" in Corec_Examples = HOL +
+session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL +
   description {*
     Corecursion Examples.
   *}
@@ -835,7 +835,7 @@
     "Tests/TLList_Friends"
     "Tests/Type_Class"
 
-session "HOL-Word" (main) in Word = HOL +
+session "HOL-Word" (main timing) in Word = HOL +
   theories Word
   document_files "root.bib" "root.tex"
 
@@ -848,7 +848,7 @@
     StateSpaceEx
   document_files "root.tex"
 
-session "HOL-Nonstandard_Analysis" in Nonstandard_Analysis = HOL +
+session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL +
   description {*
     Nonstandard analysis.
   *}
@@ -856,7 +856,7 @@
     Nonstandard_Analysis
   document_files "root.tex"
 
-session "HOL-Nonstandard_Analysis-Examples" in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
+session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   options [document = false]
   theories NSPrimes
 
@@ -868,7 +868,7 @@
   options [document = false, timeout = 60]
   theories Ex
 
-session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
+session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]
   theories
     Boogie
@@ -977,7 +977,7 @@
   options [document = false]
   theories MutabelleExtra
 
-session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
   options [document = false]
   theories
     Quickcheck_Examples
@@ -989,7 +989,7 @@
     Hotel_Example
     Quickcheck_Narrowing_Examples
 
-session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
@@ -1007,7 +1007,7 @@
     Int_Pow
     Lifting_Code_Dt_Test
 
-session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
   options [document = false]
   theories
     Examples
@@ -1029,7 +1029,7 @@
   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
     Reg_Exp_Example
 
-session HOLCF (main) in HOLCF = HOL +
+session HOLCF (main timing) in HOLCF = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
@@ -1105,7 +1105,7 @@
     FOCUS
     Buffer_adm
 
-session IOA in "HOLCF/IOA" = HOLCF +
+session IOA (timing) in "HOLCF/IOA" = HOLCF +
   description {*
     Author:     Olaf Mueller
     Copyright   1997 TU M√ľnchen
--- a/src/Pure/General/completion.scala	Fri Sep 16 16:33:24 2016 +0200
+++ b/src/Pure/General/completion.scala	Fri Sep 16 16:37:11 2016 +0200
@@ -264,8 +264,7 @@
     private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
 
     private val word_regex = "[a-zA-Z0-9_'.]+".r
-    private def word: Parser[String] = word_regex
-    private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
+    private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
     private def underscores: Parser[String] = "_*".r
 
     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
@@ -280,13 +279,12 @@
       }
     }
 
-    def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] =
+    def read_word(in: CharSequence): Option[(String, String)] =
     {
-      val parse_word = if (explicit) word else word3
       val reverse_in = new Library.Reverse(in)
       val parser =
         (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
-        underscores ~ parse_word ~ opt("?") ^^
+        underscores ~ word2 ~ opt("?") ^^
         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
       parse(parser, reverse_in) match {
         case Success(result, _) => Some(result)
@@ -448,7 +446,7 @@
         val result =
           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
             case Some(symbol) => Some((symbol, ""))
-            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
+            case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret))
           }
         result.map(
           {
--- a/src/ZF/ROOT	Fri Sep 16 16:33:24 2016 +0200
+++ b/src/ZF/ROOT	Fri Sep 16 16:37:11 2016 +0200
@@ -1,6 +1,6 @@
 chapter ZF
 
-session ZF (main ZF) = Pure +
+session ZF (main timing ZF) = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -198,7 +198,7 @@
   options [document = false]
   theories Confluence
 
-session "ZF-UNITY" (ZF) in UNITY = ZF +
+session "ZF-UNITY" (timing ZF) in UNITY = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge