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
authorkrauss
Wed Mar 23 09:15:49 2011 +0100 (2011-03-23)
changeset 420696a147393c62a
parent 42068 b579e787b582
child 42070 d3404f32328a
child 42071 04577a7e0c51
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
src/HOL/Mirabelle/etc/settings
src/HOL/Mirabelle/lib/Tools/mirabelle
     1.1 --- a/src/HOL/Mirabelle/etc/settings	Tue Mar 22 21:22:50 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/etc/settings	Wed Mar 23 09:15:49 2011 +0100
     1.3 @@ -4,7 +4,6 @@
     1.4  
     1.5  MIRABELLE_LOGIC=HOL
     1.6  MIRABELLE_THEORY=Main
     1.7 -MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
     1.8  MIRABELLE_TIMEOUT=30
     1.9  
    1.10  ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
     2.1 --- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Mar 22 21:22:50 2011 +0100
     2.2 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Mar 23 09:15:49 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  }
     2.5  
     2.6  function usage() {
     2.7 -  out="$MIRABELLE_OUTPUT_PATH"
     2.8 +  [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
     2.9    timeout="$MIRABELLE_TIMEOUT"
    2.10    echo
    2.11    echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
    2.12 @@ -102,8 +102,14 @@
    2.13  
    2.14  # setup
    2.15  
    2.16 +if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
    2.17 +  MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
    2.18 +  PURGE_OUTPUT="true"
    2.19 +fi
    2.20 +
    2.21  mkdir -p "$MIRABELLE_OUTPUT_PATH"
    2.22  
    2.23 +export MIRABELLE_OUTPUT_PATH
    2.24  
    2.25  ## main
    2.26  
    2.27 @@ -112,3 +118,9 @@
    2.28    perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
    2.29  done
    2.30  
    2.31 +
    2.32 +## cleanup
    2.33 +
    2.34 +if [ -n "$PURGE_OUTPUT" ]; then
    2.35 +  rm -rf "$MIRABELLE_OUTPUT_PATH"
    2.36 +fi