--- 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.
+
--- 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
+
--- 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 =>
--- 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 =
--- 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