--- 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