merged
authorwenzelm
Mon Dec 17 15:18:39 2012 +0100 (2012-12-17)
changeset 505798ccffe44d193
parent 50577 cfbad2d08412
parent 50578 9efc99c990d5
child 50580 fbb973a53106
merged
     1.1 --- a/Admin/Mercurial/Central/README	Mon Dec 17 15:17:32 2012 +0100
     1.2 +++ b/Admin/Mercurial/Central/README	Mon Dec 17 15:18:39 2012 +0100
     1.3 @@ -13,7 +13,9 @@
     1.4      fncache
     1.5  
     1.6  * See http://mercurial.selenic.com/wiki/MultipleCommitters for old-fashioned
     1.7 -  CVS-like multiple committers configuration, "The filesystem method":
     1.8 +  CVS-like multiple committers configuration, "The filesystem method".
     1.9 +
    1.10 +  A fresh multi-user clone is initialized like this:
    1.11  
    1.12      hg --config format.dotencode=0 init isabelle-clone
    1.13      cd isabelle-clone
    1.14 @@ -25,3 +27,26 @@
    1.15    Now isabelle-clone is ready for push of repository data (without making
    1.16    a working directory).
    1.17  
    1.18 +* Addressing technical issues: according to
    1.19 +  http://mercurial.selenic.com/wiki/PublishingRepositories our shared disk
    1.20 +  configuration (after regular ssh login) is characterized as follows:
    1.21 +
    1.22 +    Advantages: can use existing setup
    1.23 +
    1.24 +    Disadvantages: generally restricted to intranets, not generally
    1.25 +    recommended due to general issues with network filesystem reliability
    1.26 +
    1.27 +  Due to NFS instabilities of unknown origin at TUM, drop-outs have
    1.28 +  happened before. The following measures of last resort can be applied:
    1.29 +
    1.30 +    (a) "hg verify" to find offending changesets
    1.31 +        "hg strip REV" to remove parts of the public history by vivisection
    1.32 +
    1.33 +    (b) fresh clone from known-good source as explained above
    1.34 +
    1.35 +  Note that any such non-monotonic changes on the central push area work
    1.36 +  under the assumption of sequential single-user mode!!
    1.37 +
    1.38 +  See also http://mercurial.selenic.com/wiki/RepositoryCorruption for
    1.39 +  further background information.
    1.40 +
     2.1 --- a/README_REPOSITORY	Mon Dec 17 15:17:32 2012 +0100
     2.2 +++ b/README_REPOSITORY	Mon Dec 17 15:18:39 2012 +0100
     2.3 @@ -10,27 +10,31 @@
     2.4  1b. Mac OS X and Linux: ensure that Mercurial (hg) is installed; see
     2.5     also http://www.selenic.com/mercurial
     2.6  
     2.7 -2. Create file $USER_HOME/.isabelle/etc/settings and insert the following
     2.8 +2. Create file $HOME/.isabelle/etc/settings and insert the following
     2.9     line near its beginning:
    2.10  
    2.11 -    init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
    2.12 +    init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
    2.13  
    2.14  3. Execute bash shell commands as follows:
    2.15  
    2.16      hg clone http://isabelle.in.tum.de/repos/isabelle
    2.17  
    2.18 -    ./isabelle/bin/isabelle components -a
    2.19 +    cd isabelle
    2.20  
    2.21 -    ./isabelle/bin/isabelle build -b HOL
    2.22 +    ./bin/isabelle components -a
    2.23  
    2.24 -    ./isabelle/bin/isabelle jedit
    2.25 +    ./bin/isabelle jedit -l HOL
    2.26  
    2.27 -4. For later update replace "hg clone ..." above by:
    2.28 +4. To stay up-to-date later on, pull changes like this:
    2.29  
    2.30      cd isabelle
    2.31  
    2.32      hg pull -u
    2.33  
    2.34 +    ./bin/isabelle components -a
    2.35 +
    2.36 +    ./bin/isabelle jedit -l HOL
    2.37 +
    2.38  
    2.39  Introduction
    2.40  ------------
    2.41 @@ -303,7 +307,12 @@
    2.42  
    2.43  The Isabelle build process is managed as follows:
    2.44  
    2.45 -  * regular "isabelle build" to build session images, e.g. HOL;
    2.46 +  * regular "isabelle build" to build session images, for example:
    2.47 +
    2.48 +      isabelle build -b HOL
    2.49  
    2.50    * administrative "isabelle build_doc" to populate the doc/
    2.51 -    directory, such that "isabelle doc" will find the results.
    2.52 +    directory, such that "isabelle doc" will find the results, for example:
    2.53 +
    2.54 +      isabelle build_doc IsarRef
    2.55 +
     3.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Dec 17 15:17:32 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Dec 17 15:18:39 2012 +0100
     3.3 @@ -77,7 +77,7 @@
     3.4              (s, SOME maximals)
     3.5            end)
     3.6    in
     3.7 -    rev (map check all_thms)
     3.8 +    rev (Par_List.map check all_thms)
     3.9    end
    3.10  
    3.11  
    3.12 @@ -86,14 +86,14 @@
    3.13  local
    3.14  
    3.15  fun pretty_indexes is =
    3.16 -  Pretty.block (separate (Pretty.str " and ")
    3.17 -      (map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is))
    3.18 -     @ [Pretty.brk 1])
    3.19 +  Pretty.block
    3.20 +    (flat (separate [Pretty.str " and", Pretty.brk 1]
    3.21 +      (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
    3.22  
    3.23  fun pretty_thm (s, set_of_indexes) =
    3.24    Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
    3.25      Pretty.str "unnecessary assumption(s) " ::
    3.26 -    separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes))
    3.27 +    separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
    3.28  
    3.29  in
    3.30  
    3.31 @@ -106,11 +106,12 @@
    3.32      val with_superfluous_assumptions =
    3.33        map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results
    3.34  
    3.35 -    val msg = "Found " ^ string_of_int (length with_superfluous_assumptions)
    3.36 -      ^ " theorem(s) with (potentially) superfluous assumptions"
    3.37 -    val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
    3.38 -      ^ " in the theory " ^ quote thy_name
    3.39 -      ^ " with a total of " ^ string_of_int total ^ " theorem(s)"
    3.40 +    val msg =
    3.41 +      "Found " ^ string_of_int (length with_superfluous_assumptions) ^
    3.42 +      " theorems with (potentially) superfluous assumptions"
    3.43 +    val end_msg =
    3.44 +      "Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^
    3.45 +      string_of_int total ^ " total) in the theory " ^ quote thy_name
    3.46    in
    3.47      [Pretty.str (msg ^ ":"), Pretty.str ""] @
    3.48      map pretty_thm with_superfluous_assumptions @
    3.49 @@ -121,7 +122,7 @@
    3.50  
    3.51  val _ =
    3.52    Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
    3.53 -    "find theorems with superfluous assumptions"
    3.54 +    "find theorems with (potentially) superfluous assumptions"
    3.55      (Scan.option Parse.name
    3.56        >> (fn opt_thy_name =>
    3.57          Toplevel.no_timing o Toplevel.keep (fn state =>
     4.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Dec 17 15:17:32 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Dec 17 15:18:39 2012 +0100
     4.3 @@ -69,7 +69,10 @@
     4.4    def session_list(): List[String] =
     4.5    {
     4.6      val dirs = session_dirs().map((false, _))
     4.7 -    Build.find_sessions(PIDE.options.value, dirs).topological_order.map(_._1).sorted
     4.8 +    val session_tree = Build.find_sessions(PIDE.options.value, dirs)
     4.9 +    val (main_sessions, other_sessions) =
    4.10 +      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
    4.11 +    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
    4.12    }
    4.13  
    4.14    def session_content(inlined_files: Boolean): Build.Session_Content =
     5.1 --- a/src/ZF/ROOT	Mon Dec 17 15:17:32 2012 +0100
     5.2 +++ b/src/ZF/ROOT	Mon Dec 17 15:18:39 2012 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -session ZF = Pure +
     5.5 +session ZF (main) = Pure +
     5.6    description {*
     5.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1995  University of Cambridge