replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
--- a/src/HOL/Mirabelle/etc/settings Tue Mar 22 21:22:50 2011 +0100
+++ b/src/HOL/Mirabelle/etc/settings Wed Mar 23 09:15:49 2011 +0100
@@ -4,7 +4,6 @@
MIRABELLE_LOGIC=HOL
MIRABELLE_THEORY=Main
-MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Mar 22 21:22:50 2011 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Mar 23 09:15:49 2011 +0100
@@ -16,7 +16,7 @@
}
function usage() {
- out="$MIRABELLE_OUTPUT_PATH"
+ [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
timeout="$MIRABELLE_TIMEOUT"
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
@@ -102,8 +102,14 @@
# setup
+if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
+ MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
+ PURGE_OUTPUT="true"
+fi
+
mkdir -p "$MIRABELLE_OUTPUT_PATH"
+export MIRABELLE_OUTPUT_PATH
## main
@@ -112,3 +118,9 @@
perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
done
+
+## cleanup
+
+if [ -n "$PURGE_OUTPUT" ]; then
+ rm -rf "$MIRABELLE_OUTPUT_PATH"
+fi