--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Jun 20 21:41:59 2017 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Jun 21 22:48:55 2017 +0200
@@ -28,11 +28,12 @@
echo
echo " Options are:"
echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)"
+ echo " -O DIR output directory for test data (default $out)"
+ echo " -S FILE user-provided setup file (no actions required)"
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
- echo " -O DIR output directory for test data (default $out)"
+ echo " -d DIR include session directory"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
- echo " -q be quiet (suppress output of Isabelle process)"
- echo " -S FILE user-provided setup file (no actions required)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
@@ -64,9 +65,10 @@
[ $# -eq 0 ] && usage
+MIRABELLE_DIR=
MIRABELLE_SETUP_FILE=
-while getopts "L:T:O:t:S:q?" OPT
+while getopts "L:T:O:d:t:S:q?" OPT
do
case "$OPT" in
L)
@@ -78,6 +80,9 @@
O)
MIRABELLE_OUTPUT_PATH="$OPTARG"
;;
+ d)
+ MIRABELLE_DIR="$OPTARG"
+ ;;
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
@@ -93,6 +98,7 @@
esac
done
+export MIRABELLE_DIR
export MIRABELLE_SETUP_FILE
export MIRABELLE_QUIET
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Jun 20 21:41:59 2017 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Jun 21 22:48:55 2017 +0200
@@ -10,6 +10,7 @@
my $isabelle_home = $ENV{'ISABELLE_HOME'};
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
+my $mirabelle_dir = $ENV{'MIRABELLE_DIR'};
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
@@ -160,7 +161,9 @@
my $cmd =
"isabelle process -o quick_and_dirty -o threads=1" .
- " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet;
+ " -T \"$path/$new_thy_name\" " .
+ ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") .
+ "-l $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;
if ($output_log) {