# HG changeset patch # User wenzelm # Date 1355753919 -3600 # Node ID 8ccffe44d19344ee1c60be6b6de90430cec7204e # Parent cfbad2d08412a3f2e717c00988f0324706f7b4ad# Parent 9efc99c990d5857d41c96685585c04a95b5b7ed1 merged diff -r cfbad2d08412 -r 8ccffe44d193 Admin/Mercurial/Central/README --- a/Admin/Mercurial/Central/README Mon Dec 17 15:17:32 2012 +0100 +++ b/Admin/Mercurial/Central/README Mon Dec 17 15:18:39 2012 +0100 @@ -13,7 +13,9 @@ fncache * See http://mercurial.selenic.com/wiki/MultipleCommitters for old-fashioned - CVS-like multiple committers configuration, "The filesystem method": + CVS-like multiple committers configuration, "The filesystem method". + + A fresh multi-user clone is initialized like this: hg --config format.dotencode=0 init isabelle-clone cd isabelle-clone @@ -25,3 +27,26 @@ Now isabelle-clone is ready for push of repository data (without making a working directory). +* Addressing technical issues: according to + http://mercurial.selenic.com/wiki/PublishingRepositories our shared disk + configuration (after regular ssh login) is characterized as follows: + + Advantages: can use existing setup + + Disadvantages: generally restricted to intranets, not generally + recommended due to general issues with network filesystem reliability + + Due to NFS instabilities of unknown origin at TUM, drop-outs have + happened before. The following measures of last resort can be applied: + + (a) "hg verify" to find offending changesets + "hg strip REV" to remove parts of the public history by vivisection + + (b) fresh clone from known-good source as explained above + + Note that any such non-monotonic changes on the central push area work + under the assumption of sequential single-user mode!! + + See also http://mercurial.selenic.com/wiki/RepositoryCorruption for + further background information. + diff -r cfbad2d08412 -r 8ccffe44d193 README_REPOSITORY --- a/README_REPOSITORY Mon Dec 17 15:17:32 2012 +0100 +++ b/README_REPOSITORY Mon Dec 17 15:18:39 2012 +0100 @@ -10,27 +10,31 @@ 1b. Mac OS X and Linux: ensure that Mercurial (hg) is installed; see also http://www.selenic.com/mercurial -2. Create file $USER_HOME/.isabelle/etc/settings and insert the following +2. Create file $HOME/.isabelle/etc/settings and insert the following line near its beginning: - init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" + init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" 3. Execute bash shell commands as follows: hg clone http://isabelle.in.tum.de/repos/isabelle - ./isabelle/bin/isabelle components -a + cd isabelle - ./isabelle/bin/isabelle build -b HOL + ./bin/isabelle components -a - ./isabelle/bin/isabelle jedit + ./bin/isabelle jedit -l HOL -4. For later update replace "hg clone ..." above by: +4. To stay up-to-date later on, pull changes like this: cd isabelle hg pull -u + ./bin/isabelle components -a + + ./bin/isabelle jedit -l HOL + Introduction ------------ @@ -303,7 +307,12 @@ The Isabelle build process is managed as follows: - * regular "isabelle build" to build session images, e.g. HOL; + * regular "isabelle build" to build session images, for example: + + isabelle build -b HOL * administrative "isabelle build_doc" to populate the doc/ - directory, such that "isabelle doc" will find the results. + directory, such that "isabelle doc" will find the results, for example: + + isabelle build_doc IsarRef + diff -r cfbad2d08412 -r 8ccffe44d193 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Dec 17 15:17:32 2012 +0100 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Dec 17 15:18:39 2012 +0100 @@ -77,7 +77,7 @@ (s, SOME maximals) end) in - rev (map check all_thms) + rev (Par_List.map check all_thms) end @@ -86,14 +86,14 @@ local fun pretty_indexes is = - Pretty.block (separate (Pretty.str " and ") - (map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is)) - @ [Pretty.brk 1]) + Pretty.block + (flat (separate [Pretty.str " and", Pretty.brk 1] + (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) fun pretty_thm (s, set_of_indexes) = Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 :: Pretty.str "unnecessary assumption(s) " :: - separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes)) + separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) in @@ -106,11 +106,12 @@ val with_superfluous_assumptions = map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results - val msg = "Found " ^ string_of_int (length with_superfluous_assumptions) - ^ " theorem(s) with (potentially) superfluous assumptions" - val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions" - ^ " in the theory " ^ quote thy_name - ^ " with a total of " ^ string_of_int total ^ " theorem(s)" + val msg = + "Found " ^ string_of_int (length with_superfluous_assumptions) ^ + " theorems with (potentially) superfluous assumptions" + val end_msg = + "Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^ + string_of_int total ^ " total) in the theory " ^ quote thy_name in [Pretty.str (msg ^ ":"), Pretty.str ""] @ map pretty_thm with_superfluous_assumptions @ @@ -121,7 +122,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "find_unused_assms"} - "find theorems with superfluous assumptions" + "find theorems with (potentially) superfluous assumptions" (Scan.option Parse.name >> (fn opt_thy_name => Toplevel.no_timing o Toplevel.keep (fn state => diff -r cfbad2d08412 -r 8ccffe44d193 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Mon Dec 17 15:17:32 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Mon Dec 17 15:18:39 2012 +0100 @@ -69,7 +69,10 @@ def session_list(): List[String] = { val dirs = session_dirs().map((false, _)) - Build.find_sessions(PIDE.options.value, dirs).topological_order.map(_._1).sorted + val session_tree = Build.find_sessions(PIDE.options.value, dirs) + val (main_sessions, other_sessions) = + session_tree.topological_order.partition(p => p._2.groups.contains("main")) + main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted } def session_content(inlined_files: Boolean): Build.Session_Content = diff -r cfbad2d08412 -r 8ccffe44d193 src/ZF/ROOT --- a/src/ZF/ROOT Mon Dec 17 15:17:32 2012 +0100 +++ b/src/ZF/ROOT Mon Dec 17 15:18:39 2012 +0100 @@ -1,4 +1,4 @@ -session ZF = Pure + +session ZF (main) = Pure + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge