Merge branch 'integration' into stable

.gitignore

@@ -20,3 +20,7 @@ core/heaps
 /gui/bin/
 *~
 *#
+.ensime
+.ensime_lucene
+lib_managed/
+*.gen.ML

README.git

@@ -22,3 +22,4 @@ At appropriate points, current "stable" will be tagged for release.  The
 tag will be of the form "vx.y[.z]".  eg: "v2.0" or "v2.1.3".  These will
 be packaged up for download.
 
+

README.release

@@ -0,0 +1,35 @@
+
+Preparing a release for QuantoDerive
+====================================
+
+Releases should be prepared on the target OS. First, ensure the heap is built
+for the version of poly that is going to be shipped with the bundle. This can be
+done on OS X or Linux by running:
+
+    make clean
+    make heap-(osx|linux)-dist
+
+...and on Windows, run the following at a DOS prompt:
+
+    buildheap
+
+Next, from the scala directory, run the appropriate command to build the bundle.
+
+    dist/mk-osx.sh
+    dist/mk-linux.sh
+    dist/mk-windows.bat
+
+For Linux/OS X, you are done. For Windows, there is one more step. Open the AIP
+file in dist/windows-dist in Advanced Installer, update the paths as necessary
+and build an MSI.
+
+
+If dependencies change
+======================
+
+If the dependencies change, certain pieces of the bundling code need to be
+updated. "dist/osx-dist/Info.plist" needs to be updated in include any new
+JARs, as well as "dist/mk-linux-generic.sh". Also, the launcher executable
+"QuantoDerive.exe" will need to be regenerated using launch4j.
+
+

core/Makefile

@@ -1,73 +1,4 @@
-################################
-# variables you might want to set in your own profile setup...
-################################
-### your local install of PolyML and isaplib
-# POLYML_HOME=/home/ldixon/local/polyml-cvs-version
-ISAPLIB_SOURCES=../../isaplib
+# build the quantomatic heap (for development setup)
 
-################################
-# general variables
-################################
-
-# polyml executable
-POLYML_HOME=$(shell ../tools/findpoly.sh)
-POLYML=$(POLYML_HOME)/bin/poly
-POLYFLAGS=-H 200 $(if $(FAST),--disable-tests) $(if $(V),--test-log-level=$(V))
-
-
-################################
-# dynamic variables checked on call to make. 
-################################
-ML_SRC_FILES = $(shell find . | grep ".ML$$" | grep -v "test/protocol/" | grep -v "test/PROTOCOLTEST.ML$$" | grep -v "toplevel/")
-COSY_ML_SRC_FILES = $(shell find ../cosy | grep ".ML$$")
-ISAP_ML_SRC_FILES = $(ISAPLIB_SOURCES)/Makefile $(shell find $(ISAPLIB_SOURCES)/* | grep ".ML$$")
-
-################################
-# Fixed file locations
-################################
-# quanto heap file
-QUANTO_HEAP=heaps/quanto.heap
-# binary file to produce
-CORE_BIN=bin/quanto-core
-ALL_BINS=$(CORE_BIN) bin/quanto-xml-to-json
-
-################################
-# Targets:
-################################
-default: all
-
-$(QUANTO_HEAP): $(ML_SRC_FILES) $(ISAP_ML_SRC_FILES) $(COSY_ML_SRC_FILES)
-	@mkdir -p heaps
-	POLYFLAGS="$(POLYFLAGS)" ../tools/poly-build-heap -p -o $@ ROOT.ML
-
-heap: $(QUANTO_HEAP)
-
-bin/%: toplevel/%.ML $(QUANTO_HEAP) $(shell find "toplevel/$%" | grep ".ML$$")
-	@mkdir -p bin
-	POLYFLAGS="$(POLYFLAGS)" ../tools/polyc -l $(QUANTO_HEAP) -o $@ $<
-
-all: $(ALL_BINS)
-
-protocol-tests: $(CORE_BIN)
-	$(POLYML) $(POLYFLAGS) -q --use "test/PROTOCOLTEST.ML" --core "$(CORE_BIN)" --log "test/protocol-tests.log"
-
-test check: protocol-tests
-
-# startup an ML shell using the quanto heap
-ml-shell: $(QUANTO_HEAP)
-	@../tools/polyml-toplevel -l $<
-
-run: ml-shell
-
-# 
-localclean:
-	rm -f heaps/*.heap
-	rm -f bin/*.o
-	find . -type d -name .polysave | xargs rm -rf
-	rm -f $(ALL_BINS)
-
-clean: localclean
-	$(MAKE) -C $(ISAPLIB_SOURCES) clean
-
-veryclean: clean
-vclean: veryclean
+all:
+	cat build_heap.ML | poly

core/Pure/Concurrent/bash.ML

@@ -0,0 +1,107 @@
+(*  Title:      Pure/Concurrent/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts.
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+  let
+    datatype result = Wait | Signal | Result of int;
+    val result = Synchronized.var "bash_result" Wait;
+
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+    fun cleanup_files () =
+     (try File.rm script_path;
+      try File.rm out_path;
+      try File.rm err_path;
+      try File.rm pid_path);
+    val _ = cleanup_files ();
+
+    val system_thread =
+      Simple_Thread.fork false (fn () =>
+        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+          let
+            val _ = File.write script_path script;
+            val bash_script =
+              "exec bash " ^
+                File.shell_path script_path ^
+                " > " ^ File.shell_path out_path ^
+                " 2> " ^ File.shell_path err_path;
+            val _ = getenv_strict "EXEC_PROCESS";
+            val status =
+              OS.Process.system
+                ("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script);
+            val res =
+              (case Posix.Process.fromStatus status of
+                Posix.Process.W_EXITED => Result 0
+              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+              | Posix.Process.W_SIGNALED s =>
+                  if s = Posix.Signal.int then Signal
+                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+              | Posix.Process.W_STOPPED s =>
+                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+          in Synchronized.change result (K res) end
+          handle exn =>
+            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+
+    fun read_pid 0 = NONE
+      | read_pid count =
+          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+          | some => some);
+
+    fun terminate NONE = ()
+      | terminate (SOME pid) =
+          let
+            val sig_test = Posix.Signal.fromWord 0w0;
+
+            fun kill_group pid s =
+              (Posix.Process.kill
+                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
+              handle OS.SysErr _ => false;
+
+            fun kill s = (kill_group pid s; kill_group pid sig_test);
+
+            fun multi_kill count s =
+              count = 0 orelse
+                kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+            val _ =
+              multi_kill 10 Posix.Signal.int andalso
+              multi_kill 10 Posix.Signal.term andalso
+              multi_kill 10 Posix.Signal.kill;
+          in () end;
+
+    fun cleanup () =
+     (Simple_Thread.interrupt_unsynchronized system_thread;
+      cleanup_files ());
+  in
+    let
+      val _ =
+        restore_attributes (fn () =>
+          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
+      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val pid = read_pid 1;
+      val _ = cleanup ();
+    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+  end);
+
+end;
+

core/Pure/Concurrent/bash_sequential.ML

@@ -0,0 +1,47 @@
+(*  Title:      Pure/Concurrent/bash_sequential.ML
+    Author:     Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+fun process script =
+  let
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
+  in
+    let
+      val _ = File.write script_path script;
+      val status =
+        OS.Process.system
+          ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+            " script \"exec bash " ^ File.shell_path script_path ^
+            " > " ^ File.shell_path out_path ^
+            " 2> " ^ File.shell_path err_path ^ "\"");
+      val rc =
+        (case Posix.Process.fromStatus status of
+          Posix.Process.W_EXITED => 0
+        | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+        | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+        | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
+      val _ = cleanup ();
+    in {out = out, err = err, rc = rc, terminate = fn () => ()} end
+    handle exn => (cleanup (); reraise exn)
+  end;
+
+end;
+

core/Pure/Concurrent/cache.ML

@@ -0,0 +1,32 @@
+(*  Title:      Pure/Concurrent/cache.ML
+    Author:     Makarius
+
+Concurrently cached values, with minimal locking time and singleton
+evaluation due to lazy storage.
+*)
+
+signature CACHE =
+sig
+  val create: 'table -> ('table -> 'key -> 'value lazy option) ->
+    ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value
+end;
+
+structure Cache: CACHE =
+struct
+
+fun create empty lookup update f =
+  let
+    val cache = Synchronized.var "cache" empty;
+    fun apply x =
+      Synchronized.change_result cache
+        (fn tab =>
+          (case lookup tab x of
+            SOME y => (y, tab)
+          | NONE =>
+              let val y = Lazy.lazy (fn () => f x)
+              in (y, update (x, y) tab) end))
+      |> Lazy.force;
+  in apply end;
+
+end;
+