--- a/Admin/Release/CHECKLIST Sun Jan 13 20:57:48 2013 +0100
+++ b/Admin/Release/CHECKLIST Sun Jan 13 21:14:49 2013 +0100
@@ -53,16 +53,16 @@
Packaging
=========
-- hg up -r DISTNAME && isabelle makedist -r DISTNAME;
+- hg up -r DISTNAME && isabelle makedist -r DISTNAME
+
+- isabelle makedist_bundles
-- isabelle makedist_bundles;
+- ./makedist_library DISTNAME_linux.tar.gz
-- Mac OS X: hdiutil create -srcfolder DIR DMG;
+- Mac OS X: hdiutil create -srcfolder DIR DMG
- Windows: cat 7zsd_All.sfx sfx.txt Isabelle.7z > Isabelle.exe
-- makebin -l on fast machine, based on renamed bundle with deleted heaps;
-
Final release stage
===================
--- a/Admin/Release/makebin Sun Jan 13 20:57:48 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-#!/usr/bin/env bash
-#
-# makebin -- make Isabelle logic images for current platform
-
-
-## global settings
-
-TMP="/var/tmp/isabelle-makebin$$"
-
-
-## diagnostics
-
-PRG=$(basename "$0")
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] ARCHIVE"
- echo
- echo " Options are:"
- echo " -l produce library"
- echo
- echo " Precompile Isabelle for the current platform."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-DO_LIBRARY=""
-
-while getopts "l" OPT
-do
- case "$OPT" in
- l)
- DO_LIBRARY=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -gt 1 ] && usage
-
-ARCHIVE="$1"; shift
-
-
-## main
-
-[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
-ARCHIVE_BASE="$(basename "$ARCHIVE")"
-ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
-ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
-
-ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
-ISABELLE_HOME="$TMP/$ISABELLE_NAME"
-
-
-# build logics
-
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
-cd "$TMP"
-tar xzf "$ARCHIVE_FULL"
-cd "$ISABELLE_NAME"
-
-perl -pi \
- -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
- etc/settings
-
-if [ -n "$DO_LIBRARY" ]; then
- perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
- etc/settings
-fi
-
-ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
-
-COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
-PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
-
-if [ -n "$DO_LIBRARY" ]; then
- ./build -bait -m all
-else
- ./build -b HOL
-fi
-
-
-# prepare result
-
-cd "$TMP"
-
-chmod -R g=o "$TMP"
-chgrp -R isabelle "$TMP"
-
-if [ -n "$DO_LIBRARY" ]; then
- tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
-else
- tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
-fi
-
-
-# clean up
-rm -rf "$TMP"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Release/makedist_library Sun Jan 13 21:14:49 2013 +0100
@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+#
+# makedist_library -- build Isabelle HTML library from platform bundle
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] ARCHIVE"
+ echo
+ echo " Options are:"
+ echo " -j INT maximum number of parallel jobs (default 1)"
+ echo
+ echo " Build Isabelle HTML library from platform bundle."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+JOBS=""
+
+while getopts "j:" OPT
+do
+ case "$OPT" in
+ j)
+ JOBS="-j $OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+ARCHIVE_BASE="$(basename "$ARCHIVE")"
+ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
+ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
+
+
+## main
+
+export COPYFILE_DISABLE=true
+
+TMP="/var/tmp/isabelle-makedist$$"
+mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
+
+cd "$TMP"
+tar -x -z -f "$ARCHIVE_FULL"
+
+cd *
+ISABELLE_NAME="$(basename "$PWD")"
+
+echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
+echo "ISABELLE_FULL_TEST=true" >> etc/settings
+
+echo -n > src/Doc/ROOT
+
+env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
+ ./bin/isabelle build $JOBS -s -c -a -o browser_info \
+ -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
+RC="$?"
+
+cd ..
+
+if [ "$RC" = 0 ]; then
+ chmod -R g=o "$ISABELLE_NAME"
+ tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
+fi
+
+# clean up
+cd /tmp
+rm -rf "$TMP"
+
+exit "$RC"
--- a/Admin/java/build Sun Jan 13 20:57:48 2013 +0100
+++ b/Admin/java/build Sun Jan 13 21:14:49 2013 +0100
@@ -91,6 +91,8 @@
# content
+export COPYFILE_DISABLE=true
+
mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin"
tar -C "$DIR/x86-linux" -xf "$ARCHIVE_LINUX32"
--- a/Admin/lib/Tools/makedist Sun Jan 13 20:57:48 2013 +0100
+++ b/Admin/lib/Tools/makedist Sun Jan 13 21:14:49 2013 +0100
@@ -196,7 +196,7 @@
chmod -R g=o "$DISTNAME"
echo "$DISTBASE/$DISTNAME.tar.gz"
-tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
+env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
# cleanup dist
--- a/Admin/lib/Tools/makedist_bundles Sun Jan 13 20:57:48 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundles Sun Jan 13 21:14:49 2013 +0100
@@ -40,6 +40,8 @@
## main
+export COPYFILE_DISABLE=true
+
for PLATFORM_FAMILY in linux macos windows
do
--- a/src/Pure/PIDE/document.ML Sun Jan 13 20:57:48 2013 +0100
+++ b/src/Pure/PIDE/document.ML Sun Jan 13 21:14:49 2013 +0100
@@ -71,7 +71,7 @@
perspective: perspective, (*visible commands, last*)
entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*)
result: exec option} (*result of last execution*)
-and version = Version of node Graph.T (*development graph wrt. static imports*)
+and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
fun make_node (header, perspective, entries, result) =
@@ -134,9 +134,10 @@
fun set_result result =
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
-fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
-fun default_node name = Graph.default_node (name, empty_node);
-fun update_node name f = default_node name #> Graph.map_node name f;
+fun get_node nodes name = String_Graph.get_node nodes name
+ handle String_Graph.UNDEF _ => empty_node;
+fun default_node name = String_Graph.default_node (name, empty_node);
+fun update_node name f = default_node name #> String_Graph.map_node name f;
(* node edits and associated executions *)
@@ -182,7 +183,7 @@
(* version operations *)
-val empty_version = Version Graph.empty;
+val empty_version = Version String_Graph.empty;
fun nodes_of (Version nodes) = nodes;
val node_of = get_node o nodes_of;
@@ -204,12 +205,12 @@
|> default_node name
|> fold default_node imports;
val nodes2 = nodes1
- |> Graph.Keys.fold
- (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ |> String_Graph.Keys.fold
+ (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
val (nodes3, errors2) =
- (Graph.add_deps_acyclic (name, imports) nodes2, errors1)
- handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
- in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
+ (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
+ handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
+ in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
| Perspective perspective => update_node name (set_perspective perspective) nodes);
fun put_node (name, node) (Version nodes) =
@@ -294,7 +295,7 @@
val commands' =
(versions', Inttab.empty) |->
Inttab.fold (fn (_, version) => nodes_of version |>
- Graph.fold (fn (_, (node, _)) => node |>
+ String_Graph.fold (fn (_, (node, _)) => node |>
iterate_entries (fn ((_, id), _) =>
SOME o Inttab.insert (K true) (id, the_command state id))));
in (versions', commands', execution) end);
@@ -339,7 +340,7 @@
{name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
(fn () =>
(OS.Process.sleep (seconds 0.02);
- nodes_of (the_version state version_id) |> Graph.schedule
+ nodes_of (the_version state version_id) |> String_Graph.schedule
(fn deps => fn (name, node) =>
if not (visible_node node) andalso finished_theory node then
Future.value ()
@@ -366,13 +367,13 @@
fun make_required nodes =
let
val all_visible =
- Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
- |> Graph.all_preds nodes
+ String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
+ |> String_Graph.all_preds nodes
|> map (rpair ()) |> Symtab.make;
val required =
Symtab.fold (fn (a, ()) =>
- exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ?
+ exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
Symtab.update (a, ())) all_visible Symtab.empty;
in Symtab.defined required end;
@@ -476,7 +477,7 @@
val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
val updated = timeit "Document.update" (fn () =>
- nodes |> Graph.schedule
+ nodes |> String_Graph.schedule
(fn deps => fn (name, node) =>
(singleton o Future.forks)
{name = "Document.update", group = NONE,
--- a/src/Pure/Thy/thy_info.ML Sun Jan 13 20:57:48 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Jan 13 21:14:49 2013 +0100
@@ -55,11 +55,11 @@
(* derived graph operations *)
-fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
- handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
+fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
+ handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
fun new_entry name parents entry =
- Graph.new_node (name, entry) #> add_deps name parents;
+ String_Graph.new_node (name, entry) #> add_deps name parents;
(* thy database *)
@@ -74,7 +74,8 @@
fun base_name s = Path.implode (Path.base (Path.explode s));
local
- val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
+ val database =
+ Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T);
in
fun get_thys () = ! database;
fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
@@ -85,13 +86,13 @@
fun thy_graph f x = f (get_thys ()) x;
-fun get_names () = Graph.topological_order (get_thys ());
+fun get_names () = String_Graph.topological_order (get_thys ());
(* access thy *)
fun lookup_thy name =
- SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
+ SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE;
val known_thy = is_some o lookup_thy;
@@ -139,10 +140,10 @@
if is_finished name then error (loader_msg "attempt to change finished theory" [name])
else
let
- val succs = thy_graph Graph.all_succs [name];
+ val succs = thy_graph String_Graph.all_succs [name];
val _ = Output.urgent_message (loader_msg "removing" succs);
val _ = List.app (perform Remove) succs;
- val _ = change_thys (fold Graph.del_node succs);
+ val _ = change_thys (fold String_Graph.del_node succs);
in () end);
fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
@@ -179,13 +180,13 @@
(Thm.join_theory_proofs thy; Future.join present; commit (); thy);
val schedule_seq =
- Graph.schedule (fn deps => fn (_, task) =>
+ String_Graph.schedule (fn deps => fn (_, task) =>
(case task of
Task (parents, body) => finish_thy (body (task_parents deps parents))
| Finished thy => thy)) #> ignore;
val schedule_futures = uninterruptible (fn _ =>
- Graph.schedule (fn deps => fn (name, task) =>
+ String_Graph.schedule (fn deps => fn (name, task) =>
(case task of
Task (parents, body) =>
(singleton o Future.forks)
@@ -265,7 +266,7 @@
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
in
- (case try (Graph.get_node tasks) name of
+ (case try (String_Graph.get_node tasks) name of
SOME task => (task_finished task, tasks)
| NONE =>
let
@@ -305,7 +306,7 @@
(* use_thy *)
fun use_thys_wrt dir arg =
- schedule_tasks (snd (require_thys [] dir arg Graph.empty));
+ schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
val use_thys = use_thys_wrt Path.current;
val use_thy = use_thys o single;
@@ -340,6 +341,6 @@
(* finish all theories *)
-fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
+fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
end;