--- a/etc/components Wed Sep 02 20:49:04 2009 +0200
+++ b/etc/components Wed Sep 02 21:34:13 2009 +0200
@@ -13,5 +13,5 @@
#misc components
src/Tools/Code
src/HOL/Tools/ATP_Manager
-src/HOL/Tools/Mirabelle
+src/HOL/Mirabelle
src/HOL/Library/Sum_Of_Squares
--- a/src/HOL/IsaMakefile Wed Sep 02 20:49:04 2009 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 02 21:34:13 2009 +0200
@@ -31,6 +31,7 @@
HOL-Matrix \
HOL-MetisExamples \
HOL-MicroJava \
+ HOL-Mirabelle \
HOL-Modelcheck \
HOL-NanoJava \
HOL-Nominal-Examples \
@@ -1119,6 +1120,20 @@
@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
+## HOL-Mirabelle
+
+HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
+
+$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
+ Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
+ Mirabelle/Tools/mirabelle_arith.ML \
+ Mirabelle/Tools/mirabelle_metis.ML \
+ Mirabelle/Tools/mirabelle_quickcheck.ML \
+ Mirabelle/Tools/mirabelle_refute.ML \
+ Mirabelle/Tools/mirabelle_sledgehammer.ML
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
+
+
## clean
clean:
@@ -1140,4 +1155,5 @@
$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz \
$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \
$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \
- $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
+ $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \
+ $(LOG)/HOL-Mirabelle.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,25 @@
+(* Title: Mirabelle.thy
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+theory Mirabelle
+imports Pure
+uses "Tools/mirabelle.ML"
+begin
+
+(* no multithreading, no parallel proofs *)
+ML {* Multithreading.max_threads := 1 *}
+ML {* Goal.parallel_proofs := 0 *}
+
+ML {* Toplevel.add_hook Mirabelle.step_hook *}
+
+setup Mirabelle.setup
+
+ML {*
+signature MIRABELLE_ACTION =
+sig
+ val invoke : (string * string) list -> theory -> theory
+end
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/MirabelleTest.thy Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,22 @@
+(* Title: MirabelleTest.thy
+ Author: Sascha Boehme
+*)
+
+header {* Simple test theory for Mirabelle actions *}
+
+theory MirabelleTest
+imports Main Mirabelle
+uses
+ "Tools/mirabelle_arith.ML"
+ "Tools/mirabelle_metis.ML"
+ "Tools/mirabelle_quickcheck.ML"
+ "Tools/mirabelle_refute.ML"
+ "Tools/mirabelle_sledgehammer.ML"
+begin
+
+(*
+ only perform type-checking of the actions,
+ any reasonable test would be too complicated
+*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/ROOT.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,1 @@
+use_thy "MirabelleTest";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,192 @@
+(* Title: mirabelle.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+signature MIRABELLE =
+sig
+ (* configuration *)
+ val logfile : string Config.T
+ val timeout : int Config.T
+ val start_line : int Config.T
+ val end_line : int Config.T
+ val setup : theory -> theory
+
+ (* core *)
+ type action
+ val register : string * action -> theory -> theory
+ val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
+ unit
+
+ (* utility functions *)
+ val goal_thm_of : Proof.state -> thm
+ val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
+ Proof.state -> bool
+ val theorems_in_proof_term : Thm.thm -> Thm.thm list
+ val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
+ val get_setting : (string * string) list -> string * string -> string
+ val get_int_setting : (string * string) list -> string * int -> int
+ val cpu_time : ('a -> 'b) -> 'a -> 'b * int
+end
+
+
+
+structure Mirabelle : MIRABELLE =
+struct
+
+(* Mirabelle configuration *)
+
+val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
+val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
+val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
+val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
+
+val setup = setup1 #> setup2 #> setup3 #> setup4
+
+
+
+(* Mirabelle core *)
+
+type action = {pre: Proof.state, post: Toplevel.state option,
+ timeout: Time.time, log: string -> unit} -> unit
+
+structure Actions = TheoryDataFun
+(
+ type T = action Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ = Symtab.merge (K true)
+)
+
+val register = Actions.map o Symtab.update_new
+
+local
+
+fun log thy s =
+ let fun append_to n = if n = "" then K () else File.append (Path.explode n)
+ in append_to (Config.get_thy thy logfile) (s ^ "\n") end
+ (* FIXME: with multithreading and parallel proofs enabled, we might need to
+ encapsulate this inside a critical section *)
+
+fun log_sep thy = log thy "------------------"
+
+fun try_with f NONE = SOME ()
+ | try_with f (SOME e) = (f e; try (fn () => reraise e) ())
+
+fun capture_exns thy name f x =
+ (case try_with I (Exn.get_exn (Exn.capture f x)) of
+ NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
+ | SOME _ => log_sep thy)
+
+fun apply_actions thy info (pre, post, time) actions =
+ let
+ fun apply (name, action) =
+ {pre=pre, post=post, timeout=time, log=log thy}
+ |> capture_exns thy name action
+ in (log thy info; log_sep thy; List.app apply actions) end
+
+fun in_range _ _ NONE = true
+ | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
+
+fun only_within_range thy pos f x =
+ let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
+ in if in_range l r (Position.line_of pos) then f x else () end
+
+in
+
+fun basic_hook tr pre post =
+ let
+ val thy = Proof.theory_of pre
+ val pos = Toplevel.pos_of tr
+ val name = Toplevel.name_of tr
+ val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
+
+ val str0 = string_of_int o the_default 0
+ val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
+ val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
+ in
+ Actions.get thy
+ |> Symtab.dest
+ |> only_within_range thy pos (apply_actions thy info st)
+ end
+
+end
+
+val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
+
+fun step_hook tr pre post =
+ (* FIXME: might require wrapping into "interruptible" *)
+ if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
+ not (member (op =) blacklist (Toplevel.name_of tr))
+ then basic_hook tr (Toplevel.proof_of pre) (SOME post)
+ else () (* FIXME: add theory_hook here *)
+
+
+
+(* Mirabelle utility functions *)
+
+val goal_thm_of = snd o snd o Proof.get_goal
+
+fun can_apply time tac st =
+ let
+ val (ctxt, (facts, goal)) = Proof.get_goal st
+ val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
+ in
+ (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
+ SOME (thm, _) => true
+ | NONE => false)
+ end
+
+local
+
+fun fold_body_thms f =
+ let
+ fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
+ fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body
+ val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
+ (x, Inttab.update (i, ()) seen)
+ in (x' |> n = 0 ? f (name, prop, body'), seen') end)
+ in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
+
+in
+
+fun theorems_in_proof_term thm =
+ let
+ val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
+ fun collect (s, _, _) = if s <> "" then insert (op =) s else I
+ fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
+ fun resolve_thms names = map_filter (member_of names) all_thms
+ in
+ resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
+ end
+
+end
+
+fun theorems_of_sucessful_proof state =
+ (case state of
+ NONE => []
+ | SOME st =>
+ if not (Toplevel.is_proof st) then []
+ else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
+
+fun get_setting settings (key, default) =
+ the_default default (AList.lookup (op =) settings key)
+
+fun get_int_setting settings (key, default) =
+ (case Option.map Int.fromString (AList.lookup (op =) settings key) of
+ SOME (SOME i) => i
+ | SOME NONE => error ("bad option: " ^ key)
+ | NONE => default)
+
+fun cpu_time f x =
+ let
+ val start = start_timing ()
+ val result = Exn.capture (fn () => f x) ()
+ val time = Time.toMilliseconds (#cpu (end_timing start))
+ in (Exn.release result, time) end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,16 @@
+(* Title: mirabelle_arith.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Arith : MIRABELLE_ACTION =
+struct
+
+fun arith_action {pre, timeout, log, ...} =
+ if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
+ then log "arith: succeeded"
+ else ()
+ handle TimeLimit.TimeOut => log "arith: time out"
+
+fun invoke _ = Mirabelle.register ("arith", arith_action)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,27 @@
+(* Title: mirabelle_metis.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Metis : MIRABELLE_ACTION =
+struct
+
+fun metis_action {pre, post, timeout, log} =
+ let
+ val thms = Mirabelle.theorems_of_sucessful_proof post
+ val names = map Thm.get_name thms
+ val add_info = if null names then I else suffix (":\n" ^ commas names)
+
+ val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
+
+ fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
+ in
+ (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
+ |> prefix "metis: "
+ |> add_info
+ |> log
+ end
+ handle TimeLimit.TimeOut => log "metis: time out"
+
+fun invoke _ = Mirabelle.register ("metis", metis_action)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,21 @@
+(* Title: mirabelle_quickcheck.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
+struct
+
+fun quickcheck_action args {pre, timeout, log, ...} =
+ let
+ val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+ val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
+ in
+ (case TimeLimit.timeLimit timeout quickcheck pre of
+ NONE => log "quickcheck: no counterexample"
+ | SOME _ => log "quickcheck: counterexample found")
+ end
+ handle TimeLimit.TimeOut => log "quickcheck: time out"
+
+fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,39 @@
+(* Title: mirabelle_refute.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Refute : MIRABELLE_ACTION =
+struct
+
+
+(* FIXME:
+fun refute_action args timeout {pre=st, ...} =
+ let
+ val subgoal = 0
+ val thy = Proof.theory_of st
+ val thm = goal_thm_of st
+
+ val refute = Refute.refute_subgoal thy args thm
+ val _ = TimeLimit.timeLimit timeout refute subgoal
+ in
+ val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
+ val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
+
+ val r =
+ if Substring.isSubstring "model found" writ_log
+ then
+ if Substring.isSubstring "spurious" warn_log
+ then SOME "potential counterexample"
+ else SOME "real counterexample (bug?)"
+ else
+ if Substring.isSubstring "time limit" writ_log
+ then SOME "no counterexample (time out)"
+ else if Substring.isSubstring "Search terminated" writ_log
+ then SOME "no counterexample (normal termination)"
+ else SOME "no counterexample (unknown)"
+ in r end
+*)
+
+fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,105 @@
+(* Title: mirabelle_sledgehammer.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
+struct
+
+fun thms_of_name ctxt name =
+ let
+ val lex = OuterKeyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source {do_recover=false}
+ |> OuterLex.source {do_recover=SOME false} lex Position.start
+ |> OuterLex.source_proper
+ |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun safe init done f x =
+ let
+ val y = init x
+ val z = Exn.capture f y
+ val _ = done y
+ in Exn.release z end
+
+fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
+ | with_time false t = "failed (" ^ string_of_int t ^ ")"
+
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+
+
+local
+
+fun init NONE = !AtpWrapper.destdir
+ | init (SOME path) =
+ let
+ (* Warning: we implicitly assume single-threaded execution here! *)
+ val old = !AtpWrapper.destdir
+ val _ = AtpWrapper.destdir := path
+ in old end
+
+fun done path = AtpWrapper.destdir := path
+
+fun run prover_name timeout st _ =
+ let
+ val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
+ val atp_timeout = AtpManager.get_timeout ()
+ val atp = prover atp_timeout NONE NONE prover_name 1
+ val (success, (message, thm_names), _, _, _) =
+ TimeLimit.timeLimit timeout atp (Proof.get_goal st)
+ in (success, message, SOME thm_names) end
+ handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
+ | TimeLimit.TimeOut => (false, "time out", NONE)
+ | ERROR msg => (false, "error: " ^ msg, NONE)
+
+in
+
+fun run_sledgehammer (args, st, timeout, log) =
+ let
+ val prover_name =
+ AList.lookup (op =) args proverK
+ |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+ val dir = AList.lookup (op =) args keepK
+ val ((success, msg, thm_names), time) =
+ safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir
+ fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^
+ prover_name ^ "]" ^ s)
+ val _ = if success then sh_log (":\n" ^ msg) else sh_log ""
+ in if success then thm_names else NONE end
+
+end
+
+
+fun run_metis (args, st, timeout, log) thm_names =
+ let
+ fun get_thms ctxt = maps (thms_of_name ctxt)
+ fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+ fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+ fun timed_metis thms =
+ uncurry with_time (Mirabelle.cpu_time apply_metis thms)
+ handle TimeLimit.TimeOut => "time out"
+ fun log_metis s = log ("-----\nmetis (sledgehammer): " ^ s)
+ in
+ if not (AList.defined (op =) args metisK) then ()
+ else if is_none thm_names then ()
+ else
+ these thm_names
+ |> get_thms (Proof.context_of st)
+ |> timed_metis
+ |> log_metis
+ end
+
+
+fun sledgehammer_action args {pre, timeout, log, ...} =
+ run_sledgehammer (args, pre, timeout, log)
+ |> run_metis (args, pre, timeout, log)
+
+fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/doc/options.txt Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,6 @@
+Options for sledgehammer:
+
+ * prover=NAME: name of the external prover to call
+ * keep=PATH: path where to keep temporary files created by sledgehammer
+ * metis=X: apply metis with the theorems found by sledgehammer (X may be any
+ non-empty string)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/etc/settings Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,8 @@
+MIRABELLE_HOME="$COMPONENT"
+
+MIRABELLE_LOGIC=HOL
+MIRABELLE_THEORY=Main
+MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
+MIRABELLE_TIMEOUT=30
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,88 @@
+#!/usr/bin/env bash
+#
+# Author: Sascha Boehme
+#
+# DESCRIPTION: testing tool for automated proof tools
+
+
+PRG="$(basename "$0")"
+
+function print_action_names() {
+ TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
+ for NAME in $TOOLS
+ do
+ echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/'
+ done
+}
+
+function usage() {
+ out="$MIRABELLE_OUTPUT_PATH"
+ timeout="$MIRABELLE_TIMEOUT"
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
+ echo
+ echo " Options are:"
+ echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)"
+ echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
+ echo " -O DIR output directory for test data (default $out)"
+ echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
+ echo
+ echo " Apply the given actions (i.e., automated proof tools)"
+ echo " at all proof steps in the given theory files."
+ echo
+ echo " ACTIONS is a colon-separated list of actions, where each action is"
+ echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+ print_action_names
+ echo
+ echo " FILES is a list of theory files, where each file is either NAME.thy"
+ echo " or NAME.thy[START:END] and START and END are numbers indicating the"
+ echo " range the given actions are to be applied."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+# options
+
+while getopts "L:T:O:t:?" OPT
+do
+ case "$OPT" in
+ L)
+ MIRABELLE_LOGIC="$OPTARG"
+ ;;
+ T)
+ MIRABELLE_THEORY="$OPTARG"
+ ;;
+ O)
+ MIRABELLE_OUTPUT_PATH="$OPTARG"
+ ;;
+ t)
+ MIRABELLE_TIMEOUT="$OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+ACTIONS="$1"
+
+shift
+
+
+# setup
+
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
+
+
+## main
+
+for FILE in "$@"
+do
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+done
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,141 @@
+#
+# Author: Jasmin Blanchette and Sascha Boehme
+#
+# Testing tool for automated proof tools.
+#
+
+use File::Basename;
+
+# environment
+
+my $isabelle_home = $ENV{'ISABELLE_HOME'};
+my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
+my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
+my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
+my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
+my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
+
+my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
+
+
+# arguments
+
+my $actions = $ARGV[0];
+
+my $thy_file = $ARGV[1];
+my $start_line = "0";
+my $end_line = "~1";
+if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
+ $thy_file = $1;
+ $start_line = $2;
+ $end_line = $3;
+}
+my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
+my $new_thy_name = $thy_name . "_Mirabelle";
+my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
+
+
+# setup
+
+my $setup_thy_name = $thy_name . "_Setup";
+my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
+my $log_file = $output_path . "/" . $thy_name . ".log";
+
+my @action_files;
+my @action_names;
+foreach (split(/:/, $actions)) {
+ if (m/([^[]*)/) {
+ push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+ push @action_names, $1;
+ }
+}
+my $tools = "";
+if ($#action_files >= 0) {
+ $tools = "uses " . join(" ", @action_files);
+}
+
+open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
+
+print SETUP_FILE <<END;
+theory "$setup_thy_name"
+imports "$mirabelle_thy" "$mirabelle_theory"
+$tools
+begin
+
+setup {*
+ Config.put_thy Mirabelle.logfile "$log_file" #>
+ Config.put_thy Mirabelle.timeout $timeout #>
+ Config.put_thy Mirabelle.start_line $start_line #>
+ Config.put_thy Mirabelle.end_line $end_line
+*}
+
+END
+
+foreach (split(/:/, $actions)) {
+ if (m/([^[]*)(?:\[(.*)\])?/) {
+ my ($name, $settings_str) = ($1, $2 || "");
+ $name =~ s/^([a-z])/\U$1/;
+ print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
+ my $sep = "";
+ foreach (split(/,/, $settings_str)) {
+ if (m/\s*(.*)\s*=\s*(.*)\s*/) {
+ print SETUP_FILE "$sep(\"$1\", \"$2\")";
+ $sep = ", ";
+ }
+ }
+ print SETUP_FILE "] *}\n";
+ }
+}
+
+print SETUP_FILE "\nend";
+close SETUP_FILE;
+
+
+# modify target theory file
+
+open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
+my @lines = <OLD_FILE>;
+close(OLD_FILE);
+
+my $thy_text = join("", @lines);
+my $old_len = length($thy_text);
+$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
+$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
+die "No 'imports' found" if length($thy_text) == $old_len;
+
+open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
+print NEW_FILE $thy_text;
+close(NEW_FILE);
+
+my $root_file = "$output_path/ROOT_$thy_name.ML";
+open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
+print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
+close(ROOT_FILE);
+
+
+# run isabelle
+
+open(LOG_FILE, ">$log_file");
+print LOG_FILE "Run of $new_thy_file with:\n";
+foreach $name (@action_names) {
+ print LOG_FILE " $name\n";
+}
+close(LOG_FILE);
+
+my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
+ "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
+
+
+# produce report
+
+if ($result == 0) {
+ system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\"";
+}
+
+
+# cleanup
+
+unlink $root_file;
+unlink $setup_file;
+
+exit $result;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl Wed Sep 02 21:34:13 2009 +0200
@@ -0,0 +1,69 @@
+#
+# Author: Sascha Boehme
+#
+# Reports for Mirabelle
+#
+
+my $log_file = $ARGV[0];
+
+open(FILE, "<$log_file") || die "Cannot open file '$log_file'";
+my @lines = <FILE>;
+close(FILE);
+
+my $unhandled = 0;
+
+my $sh_calls = 0;
+my $sh_succeeded = 0;
+my $sh_time = 0;
+
+my $metis_calls = 0;
+my $metis_succeeded = 0;
+my $metis_time = 0;
+
+foreach (@lines) {
+ if (m/^unhandled exception/) {
+ $unhandled++;
+ }
+ if (m/^sledgehammer:/) {
+ $sh_calls++;
+ }
+ if (m/^sledgehammer: succeeded \(([0-9]+)\)/) {
+ $sh_succeeded++;
+ $sh_time += $1;
+ }
+ if (m/^metis \(sledgehammer\):/) {
+ $metis_calls++;
+ }
+ if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
+ $metis_succeeded++;
+ $metis_time += $1;
+ }
+}
+
+open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
+
+print FILE "\n\n\n";
+
+if ($unhandled > 0) {
+ print FILE "Number of unhandled exceptions: $unhandled\n\n";
+}
+
+if ($sh_calls > 0) {
+ my $percent = $sh_succeeded / $sh_calls * 100;
+ my $time = $sh_time / 1000;
+ print FILE "Total number of sledgehammer calls: $sh_calls\n";
+ print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
+ printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
+ print FILE "Total time for successful sledgehammer calls: $time seconds\n\n";
+}
+
+if ($metis_calls > 0) {
+ my $percent = $metis_succeeded / $metis_calls * 100;
+ my $time = $metis_time / 1000;
+ print FILE "Total number of metis calls: $metis_calls\n";
+ print FILE "Number of successful metis calls: $metis_succeeded\n";
+ printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
+ print FILE "Total time for successful metis calls: $time seconds\n";
+}
+
+close(FILE);
--- a/src/HOL/Tools/Mirabelle/Mirabelle.thy Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: Mirabelle.thy
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-theory Mirabelle
-imports Pure
-uses "Tools/mirabelle.ML"
-begin
-
-(* no multithreading, no parallel proofs *)
-ML {* Multithreading.max_threads := 1 *}
-ML {* Goal.parallel_proofs := 0 *}
-
-ML {* Toplevel.add_hook Mirabelle.step_hook *}
-
-setup Mirabelle.setup
-
-ML {*
-signature MIRABELLE_ACTION =
-sig
- val invoke : (string * string) list -> theory -> theory
-end
-*}
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,185 +0,0 @@
-(* Title: mirabelle.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-signature MIRABELLE =
-sig
- type action
- val register : string * action -> theory -> theory
-
- val logfile : string Config.T
- val timeout : int Config.T
- val start_line : int Config.T
- val end_line : int Config.T
-
- val goal_thm_of : Proof.state -> thm
- val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
- Proof.state -> bool
- val theorems_in_proof_term : Thm.thm -> Thm.thm list
- val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
- val get_setting : (string * string) list -> string * string -> string
- val get_int_setting : (string * string) list -> string * int -> int
-end
-
-
-
-signature MIRABELLE_EXT =
-sig
- include MIRABELLE
- val setup : theory -> theory
- val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
- unit
-end
-
-
-
-structure Mirabelle : MIRABELLE_EXT =
-struct
-
-(* Mirabelle core *)
-
-type action = {pre: Proof.state, post: Toplevel.state option,
- timeout: Time.time, log: string -> unit} -> unit
-
-structure Actions = TheoryDataFun
-(
- type T = action Symtab.table
- val empty = Symtab.empty
- val copy = I
- val extend = I
- fun merge _ = Symtab.merge (K true)
-)
-
-val register = Actions.map o Symtab.update_new
-
-val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
-val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
-val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
-val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
-
-val setup = setup1 #> setup2 #> setup3 #> setup4
-
-local
-
-fun log thy s =
- let fun append_to n = if n = "" then K () else File.append (Path.explode n)
- in append_to (Config.get_thy thy logfile) (s ^ "\n") end
- (* FIXME: with multithreading and parallel proofs enabled, we might need to
- encapsulate this inside a critical section *)
-
-fun log_block thy msg = log thy (msg ^ "\n------------------")
-fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)
-
-fun capture_exns logf f x =
- let
- fun f' x = f x
- handle TimeLimit.TimeOut => logf "time out"
- | ERROR msg => logf ("error: " ^ msg)
- in (case try f' x of NONE => logf "exception" | _ => ()) end
-
-fun apply_actions thy info (pre, post, time) actions =
- let
- val _ = log_block thy info
- fun apply (name, action) =
- let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
- in capture_exns (log_action thy name) action st end
- in List.app apply actions end
-
-fun in_range _ _ NONE = true
- | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
-
-fun only_within_range thy pos f x =
- let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
- in if in_range l r (Position.line_of pos) then f x else () end
-
-in
-
-fun basic_hook tr pre post =
- let
- val thy = Proof.theory_of pre
- val pos = Toplevel.pos_of tr
- val name = Toplevel.name_of tr
- val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
-
- val str0 = string_of_int o the_default 0
- val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
- val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
- in
- Actions.get thy
- |> Symtab.dest
- |> only_within_range thy pos (apply_actions thy info st)
- end
-
-end
-
-val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
-
-fun step_hook tr pre post =
- (* FIXME: might require wrapping into "interruptible" *)
- if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
- not (member (op =) blacklist (Toplevel.name_of tr))
- then basic_hook tr (Toplevel.proof_of pre) (SOME post)
- else () (* FIXME: add theory_hook here *)
-
-
-
-(* Mirabelle utility functions *)
-
-val goal_thm_of = snd o snd o Proof.get_goal
-
-fun can_apply time tac st =
- let
- val (ctxt, (facts, goal)) = Proof.get_goal st
- val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
- in
- (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
- SOME (thm, _) => true
- | NONE => false)
- end
-
-local
-
-fun fold_body_thms f =
- let
- fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
- fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
- else
- let
- val body' = Future.join body
- val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
- (x, Inttab.update (i, ()) seen)
- in (x' |> n = 0 ? f (name, prop, body'), seen') end)
- in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
-
-in
-
-fun theorems_in_proof_term thm =
- let
- val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
- fun collect (s, _, _) = if s <> "" then insert (op =) s else I
- fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
- fun resolve_thms names = map_filter (member_of names) all_thms
- in
- resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
- end
-
-end
-
-fun theorems_of_sucessful_proof state =
- (case state of
- NONE => []
- | SOME st =>
- if not (Toplevel.is_proof st) then []
- else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
-
-fun get_setting settings (key, default) =
- the_default default (AList.lookup (op =) settings key)
-
-fun get_int_setting settings (key, default) =
- (case Option.map Int.fromString (AList.lookup (op =) settings key) of
- SOME (SOME i) => i
- | SOME NONE => error ("bad option: " ^ key)
- | NONE => default)
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: mirabelle_arith.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-structure Mirabelle_Arith : MIRABELLE_ACTION =
-struct
-
-fun arith_action {pre, timeout, log, ...} =
- if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
- then log "succeeded"
- else ()
-
-fun invoke _ = Mirabelle.register ("arith", arith_action)
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: mirabelle_metis.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-structure Mirabelle_Metis : MIRABELLE_ACTION =
-struct
-
-fun metis_action {pre, post, timeout, log} =
- let
- val thms = Mirabelle.theorems_of_sucessful_proof post
- val names = map Thm.get_name thms
- val add_info = if null names then I else suffix (":\n" ^ commas names)
-
- val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
-
- fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
- in
- (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> add_info
- |> log
- end
-
-fun invoke _ = Mirabelle.register ("metis", metis_action)
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: mirabelle_quickcheck.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
-struct
-
-fun quickcheck_action limit args {pre=st, ...} =
- let
- val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
- val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
- in
- (case TimeLimit.timeLimit limit quickcheck st of
- NONE => SOME "no counterexample"
- | SOME _ => SOME "counterexample found")
- end
-
-fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: mirabelle_refute.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-structure Mirabelle_Refute : MIRABELLE_ACTION =
-struct
-
-
-(* FIXME:
-fun refute_action args timeout {pre=st, ...} =
- let
- val subgoal = 0
- val thy = Proof.theory_of st
- val thm = goal_thm_of st
-
- val refute = Refute.refute_subgoal thy args thm
- val _ = TimeLimit.timeLimit timeout refute subgoal
- in
- val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
- val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
-
- val r =
- if Substring.isSubstring "model found" writ_log
- then
- if Substring.isSubstring "spurious" warn_log
- then SOME "potential counterexample"
- else SOME "real counterexample (bug?)"
- else
- if Substring.isSubstring "time limit" writ_log
- then SOME "no counterexample (time out)"
- else if Substring.isSubstring "Search terminated" writ_log
- then SOME "no counterexample (normal termination)"
- else SOME "no counterexample (unknown)"
- in r end
-*)
-
-fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
-
-end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(* Title: mirabelle_sledgehammer.ML
- Author: Jasmin Blanchette and Sascha Boehme
-*)
-
-structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
-struct
-
-fun thms_of_name ctxt name =
- let
- val lex = OuterKeyword.get_lexicons
- val get = maps (ProofContext.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source {do_recover=false}
- |> OuterLex.source {do_recover=SOME false} lex Position.start
- |> OuterLex.source_proper
- |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-fun safe init done f x =
- let
- val y = init x
- val z = Exn.capture f y
- val _ = done y
- in Exn.release z end
-
-val proverK = "prover"
-val keepK = "keep"
-val metisK = "metis"
-
-fun sledgehammer_action args {pre=st, timeout, log, ...} =
- let
- val prover_name =
- AList.lookup (op =) args proverK
- |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
-
- val thy = Proof.theory_of st
-
- val prover = the (AtpManager.get_prover prover_name thy)
- val atp_timeout = AtpManager.get_timeout ()
-
- (* run sledgehammer *)
- fun init NONE = !AtpWrapper.destdir
- | init (SOME path) =
- let
- (* Warning: we implicitly assume single-threaded execution here! *)
- val old = !AtpWrapper.destdir
- val _ = AtpWrapper.destdir := path
- in old end
- fun done path = AtpWrapper.destdir := path
- fun sh _ =
- let
- val atp = prover atp_timeout NONE NONE prover_name 1
- val (success, (message, thm_names), _, _, _) =
- TimeLimit.timeLimit timeout atp (Proof.get_goal st)
- in (success, message, SOME thm_names) end
- handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
- val (success, message, thm_names) = safe init done sh
- (AList.lookup (op =) args keepK)
- val _ =
- if success then log (quote prover_name ^ " succeeded:\n" ^ message)
- else log (prover_name ^ " failed")
-
- (* try metis *)
- fun get_thms ctxt = maps (thms_of_name ctxt)
- fun metis thms ctxt = MetisTools.metis_tac ctxt thms
- fun log_metis s =
- log ("applying metis: " ^ s)
- fun apply_metis thms =
- if Mirabelle.can_apply timeout (metis thms) st
- then "succeeded" else "failed"
- val _ =
- if not (AList.defined (op =) args metisK) then ()
- else
- these thm_names
- |> get_thms (Proof.context_of st)
- |> apply_metis
- |> log_metis
- in () end
-
-fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
-
-end
--- a/src/HOL/Tools/Mirabelle/doc/options.txt Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-Options for sledgehammer:
-
- * prover=NAME: name of the external prover to call
- * keep=PATH: path where to keep temporary files created by sledgehammer
- * metis=X: apply metis with the theorems found by sledgehammer (X may be any
- non-empty string)
--- a/src/HOL/Tools/Mirabelle/etc/settings Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-MIRABELLE_HOME="$COMPONENT"
-
-MIRABELLE_LOGIC=HOL
-MIRABELLE_THEORY=Main
-MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
-MIRABELLE_TIMEOUT=30
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Sascha Boehme
-#
-# DESCRIPTION: testing tool for automated proof tools
-
-
-PRG="$(basename "$0")"
-
-function print_action_names() {
- TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
- for NAME in $TOOLS
- do
- echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/'
- done
-}
-
-function usage() {
- out="$MIRABELLE_OUTPUT_PATH"
- timeout="$MIRABELLE_TIMEOUT"
- echo
- echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
- echo
- echo " Options are:"
- echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)"
- echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
- echo " -O DIR output directory for test data (default $out)"
- echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
- echo
- echo " Apply the given actions (i.e., automated proof tools)"
- echo " at all proof steps in the given theory files."
- echo
- echo " ACTIONS is a colon-separated list of actions, where each action is"
- echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
- print_action_names
- echo
- echo " FILES is a list of theory files, where each file is either NAME.thy"
- echo " or NAME.thy[START:END] and START and END are numbers indicating the"
- echo " range the given actions are to be applied."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-while getopts "L:T:O:t:?" OPT
-do
- case "$OPT" in
- L)
- MIRABELLE_LOGIC="$OPTARG"
- ;;
- T)
- MIRABELLE_THEORY="$OPTARG"
- ;;
- O)
- MIRABELLE_OUTPUT_PATH="$OPTARG"
- ;;
- t)
- MIRABELLE_TIMEOUT="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-ACTIONS="$1"
-
-shift
-
-
-# setup
-
-mkdir -p "$MIRABELLE_OUTPUT_PATH"
-
-
-## main
-
-for FILE in "$@"
-do
- perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
-done
-
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Wed Sep 02 20:49:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-#
-# Author: Jasmin Blanchette and Sascha Boehme
-#
-# Testing tool for automated proof tools.
-#
-
-use File::Basename;
-
-# environment
-
-my $isabelle_home = $ENV{'ISABELLE_HOME'};
-my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
-my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
-my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
-my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
-my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
-
-my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
-
-
-# arguments
-
-my $actions = $ARGV[0];
-
-my $thy_file = $ARGV[1];
-my $start_line = "0";
-my $end_line = "~1";
-if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
- $thy_file = $1;
- $start_line = $2;
- $end_line = $3;
-}
-my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
-my $new_thy_name = $thy_name . "_Mirabelle";
-my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
-
-
-# setup
-
-my $setup_thy_name = $thy_name . "_Setup";
-my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
-my $log_file = $output_path . "/" . $thy_name . ".log";
-
-my @action_files;
-my @action_names;
-foreach (split(/:/, $actions)) {
- if (m/([^[]*)/) {
- push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
- push @action_names, $1;
- }
-}
-my $tools = "";
-if ($#action_files >= 0) {
- $tools = "uses " . join(" ", @action_files);
-}
-
-open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
-
-print SETUP_FILE <<END;
-theory "$setup_thy_name"
-imports "$mirabelle_thy" "$mirabelle_theory"
-$tools
-begin
-
-setup {*
- Config.put_thy Mirabelle.logfile "$log_file" #>
- Config.put_thy Mirabelle.timeout $timeout #>
- Config.put_thy Mirabelle.start_line $start_line #>
- Config.put_thy Mirabelle.end_line $end_line
-*}
-
-END
-
-foreach (split(/:/, $actions)) {
- if (m/([^[]*)(?:\[(.*)\])?/) {
- my ($name, $settings_str) = ($1, $2 || "");
- $name =~ s/^([a-z])/\U$1/;
- print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
- my $sep = "";
- foreach (split(/,/, $settings_str)) {
- if (m/\s*(.*)\s*=\s*(.*)\s*/) {
- print SETUP_FILE "$sep(\"$1\", \"$2\")";
- $sep = ", ";
- }
- }
- print SETUP_FILE "] *}\n";
- }
-}
-
-print SETUP_FILE "\nend";
-close SETUP_FILE;
-
-
-# modify target theory file
-
-open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
-my @lines = <OLD_FILE>;
-close(OLD_FILE);
-
-my $thy_text = join("", @lines);
-my $old_len = length($thy_text);
-$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
-$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
-die "No 'imports' found" if length($thy_text) == $old_len;
-
-open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
-print NEW_FILE $thy_text;
-close(NEW_FILE);
-
-my $root_file = "$output_path/ROOT_$thy_name.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
-print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
-close(ROOT_FILE);
-
-
-# run isabelle
-
-open(LOG_FILE, ">$log_file");
-print LOG_FILE "Run of $new_thy_file with:\n";
-foreach $name (@action_names) {
- print LOG_FILE " $name\n";
-}
-close(LOG_FILE);
-
-my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
-
-
-# cleanup
-
-unlink $root_file;
-unlink $setup_file;
-
-exit $r;
-