From b160adf65c1f6b68f0f86d080a9d4ab7858bbcd5 Mon Sep 17 00:00:00 2001
From: Eli Barzilay <eli@barzilay.org>
Date: Sun, 13 Jan 2013 19:26:51 -0500
Subject: [PATCH] Very simple job server.

Kept here in case it's useful for other things.
(cherry picked from commit df850724e17472e829088002c62c13912ad0b92a)
---
 collects/meta/build/dmg/run | 88 +++++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)
 create mode 100755 collects/meta/build/dmg/run

diff --git a/collects/meta/build/dmg/run b/collects/meta/build/dmg/run
new file mode 100755
index 0000000000..fe84ad7603
--- /dev/null
+++ b/collects/meta/build/dmg/run
@@ -0,0 +1,88 @@
+#!/bin/sh
+
+# This is a very simple job server which can be used to run commands in
+# a different context.  For example, for things that need to run from
+# inside an OSX session rather than in the ssh-ed context.
+
+here="$(cd $(dirname "$0"); pwd)"
+pidfile="$here/pid"
+
+unset LD_LIBRARY_PATH
+
+###############################################################################
+server() {
+  case "$serverstatus" in
+  ( running ) echo "Server already running" 1>&2; exit 1 ;;
+  ( stopped ) ;;
+  ( dead    ) echo "Cleaning up after dead server" 1>&2; rm -f "$pidfile" ;;
+  ( *       ) echo "Unknown server status" 1>&2; exit 1 ;;
+  esac
+  echo "Server started, pid=$$"
+  echo "$$" > "$pidfile"
+  trap cleanup 0 3 9 15
+  while true; do
+    cd "$here"
+    jobs="$(find * -name "*.job")"
+    if [[ "$jobs" = "" ]]; then sleep 2; continue; fi
+    echo "$jobs" | \
+    while read job; do
+      n="${job%.job}"
+      echo "Running job #$n..."
+      cd "$HOME"
+      . "$here/$job" > "$here/$n.out" 2>&1
+      echo "$?" > "$here/$n.ret"
+      cd "$here"
+      echo "Done"
+      rm -f "$here/$job"
+    done
+  done
+}
+
+cleanup() { rm -f "$pidfile"; }
+
+###############################################################################
+client() {
+  case "$serverstatus" in
+  ( running ) ;;
+  ( stopped ) echo "No server running" 1>&2; exit 1 ;;
+  ( dead    ) echo "Server died" 1>&2; exit 1 ;;
+  ( *       ) echo "Unknown server status" 1>&2; exit 1 ;;
+  esac
+  c="0"
+  if [[ -e "$here/counter" ]]; then c="$(cat "$here/counter")"; fi
+  c=$(( (c+1) % 10000 ))
+  echo "$c" > "$here/counter"
+  c="$here/$c"
+  echo "cd \"$(pwd)\"" > "$c.tmp"
+  if [[ "x$1" = "x-" ]]; then cat; else echo "$@"; fi >> "$c.tmp"
+  mv "$c.tmp" "$c.job"
+  while [[ -e "$c.job" ]]; do sleep 1; done
+  cat "$c.out"; rm -f "$c.out"
+  stat="$(cat "$c.ret")"; rm -f "$c.ret"
+  exit "$stat"
+}
+
+###############################################################################
+status() {
+  echo "$serverstatus"
+}
+
+if [[ ! -e "$pidfile" ]]; then serverstatus="stopped"
+else
+  pid="$(cat "$pidfile")"
+  if ps -p "$pid" | grep -q "$pid"; then serverstatus="running"
+  else serverstatus="dead"; fi
+fi
+
+###############################################################################
+
+case "x$1" in
+( "x--help"   ) echo "--start:  start server"
+                echo "--status: find the status of the running server, if any"
+                echo "Anything else, run it on the server; use \`-' to read"
+                echo "  shell code from stdin"
+                exit ;;
+( "x--start"  ) shift; server "$@" ;;
+( "x--status" ) shift; status "$@" ;;
+( *           )        client "$@" ;;
+esac