1.1 --- a/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 09:49:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 13:21:19 2009 +0200
     1.3 @@ -3,10 +3,23 @@
     1.4  *)
     1.5  
     1.6  theory Mirabelle
     1.7 -imports Plain
     1.8 +imports Pure
     1.9  uses "Tools/mirabelle.ML"
    1.10  begin
    1.11  
    1.12 +(* no multithreading, no parallel proofs *)
    1.13 +ML {* Multithreading.max_threads := 1 *}
    1.14 +ML {* Goal.parallel_proofs := 0 *}
    1.15 +
    1.16 +ML {* Toplevel.add_hook Mirabelle.step_hook *}
    1.17 +
    1.18  setup Mirabelle.setup
    1.19  
    1.20 +ML {*
    1.21 +signature MIRABELLE_ACTION =
    1.22 +sig
    1.23 +  val invoke : (string * string) list -> theory -> theory
    1.24  end
    1.25 +*}
    1.26 +
    1.27 +end

     2.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Fri Aug 21 09:49:10 2009 +0200
     2.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Fri Aug 21 13:21:19 2009 +0200
     2.3 @@ -5,9 +5,7 @@
     2.4  signature MIRABELLE =
     2.5  sig
     2.6    type action
     2.7 -  type settings
     2.8 -  val register : string -> action -> theory -> theory
     2.9 -  val invoke : string -> settings -> theory -> theory
    2.10 +  val register : string * action -> theory -> theory
    2.11  
    2.12    val timeout : int Config.T
    2.13    val verbose : bool Config.T
    2.14 @@ -15,37 +13,34 @@
    2.15    val end_line : int Config.T
    2.16    val set_logfile : string -> theory -> theory
    2.17  
    2.18 -  val setup : theory -> theory
    2.19 -
    2.20 -  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    2.21 -    unit
    2.22 -
    2.23    val goal_thm_of : Proof.state -> thm
    2.24    val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
    2.25    val theorems_in_proof_term : Thm.thm -> Thm.thm list
    2.26 -  val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
    2.27 -  val get_setting : settings -> string * string -> string
    2.28 -  val get_int_setting : settings -> string * int -> int
    2.29 -
    2.30 -(* FIXME  val refute_action : action *)
    2.31 -  val quickcheck_action : action
    2.32 -  val arith_action : action
    2.33 -  val sledgehammer_action : action
    2.34 -  val metis_action : action
    2.35 +  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
    2.36 +  val get_setting : (string * string) list -> string * string -> string
    2.37 +  val get_int_setting : (string * string) list -> string * int -> int
    2.38  end
    2.39  
    2.40  
    2.41  
    2.42 -structure Mirabelle (*: MIRABELLE*) =
    2.43 +signature MIRABELLE_EXT =
    2.44 +sig
    2.45 +  include MIRABELLE
    2.46 +  val setup : theory -> theory
    2.47 +  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    2.48 +    unit
    2.49 +end
    2.50 +
    2.51 +
    2.52 +
    2.53 +structure Mirabelle : MIRABELLE_EXT =
    2.54  struct
    2.55  
    2.56  (* Mirabelle core *)
    2.57  
    2.58 -type settings = (string * string) list
    2.59 -type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
    2.60 -type action = settings -> invoked
    2.61 +type action = {pre: Proof.state, post: Toplevel.state option} -> string option
    2.62  
    2.63 -structure Registered = TheoryDataFun
    2.64 +structure Actions = TheoryDataFun
    2.65  (
    2.66    type T = action Symtab.table
    2.67    val empty = Symtab.empty
    2.68 @@ -54,26 +49,7 @@
    2.69    fun merge _ = Symtab.merge (K true)
    2.70  )
    2.71  
    2.72 -fun register name act = Registered.map (Symtab.update_new (name, act))
    2.73 -
    2.74 -
    2.75 -structure Invoked = TheoryDataFun
    2.76 -(
    2.77 -  type T = (string * invoked) list
    2.78 -  val empty = []
    2.79 -  val copy = I
    2.80 -  val extend = I
    2.81 -  fun merge _ = Library.merge (K true)
    2.82 -)
    2.83 -
    2.84 -fun invoke name sts thy = 
    2.85 -  let 
    2.86 -    val act = 
    2.87 -      (case Symtab.lookup (Registered.get thy) name of
    2.88 -        SOME act => act
    2.89 -      | NONE => error ("The invoked action " ^ quote name ^ 
    2.90 -          " is not registered."))
    2.91 -  in Invoked.map (cons (name, act sts)) thy end
    2.92 +val register = Actions.map o Symtab.update_new
    2.93  
    2.94  val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
    2.95  val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
    2.96 @@ -81,7 +57,7 @@
    2.97  val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
    2.98  val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
    2.99  
   2.100 -val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
   2.101 +val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
   2.102  
   2.103  fun set_logfile name =
   2.104    let val _ = File.write (Path.explode name) ""   (* erase file content *)
   2.105 @@ -104,8 +80,8 @@
   2.106  fun capture_exns verb f x =
   2.107    (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
   2.108  
   2.109 -fun apply_action (c as (verb, _)) st (name, invoked) =
   2.110 -  Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
   2.111 +fun apply_action (c as (verb, _)) st (name, action) =
   2.112 +  Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
   2.113  
   2.114  fun in_range _ _ NONE = true
   2.115    | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
   2.116 @@ -140,7 +116,8 @@
   2.117      val secs = Time.fromSeconds (Config.get_thy thy timeout)
   2.118      val st = {pre=pre, post=post}
   2.119    in
   2.120 -    Invoked.get thy
   2.121 +    Actions.get thy
   2.122 +    |> Symtab.dest
   2.123      |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
   2.124      |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
   2.125    end
   2.126 @@ -213,108 +190,4 @@
   2.127    | SOME NONE => error ("bad option: " ^ key)
   2.128    | NONE => default)
   2.129  
   2.130 -
   2.131 -
   2.132 -(* Mirabelle actions *)
   2.133 -
   2.134 -(* FIXME
   2.135 -fun refute_action settings {pre=st, ...} = 
   2.136 -  let
   2.137 -    val params   = [("minsize", "2") (*"maxsize", "2"*)]
   2.138 -    val subgoal = 0
   2.139 -    val thy     = Proof.theory_of st
   2.140 -    val thm = goal_thm_of st
   2.141 -
   2.142 -    val _ = Refute.refute_subgoal thy parms thm subgoal
   2.143 -  in
   2.144 -    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
   2.145 -    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
   2.146 -
   2.147 -    val r =
   2.148 -      if Substring.isSubstring "model found" writ_log
   2.149 -      then
   2.150 -        if Substring.isSubstring "spurious" warn_log
   2.151 -        then SOME "potential counterexample"
   2.152 -        else SOME "real counterexample (bug?)"
   2.153 -      else
   2.154 -        if Substring.isSubstring "time limit" writ_log
   2.155 -        then SOME "no counterexample (time out)"
   2.156 -        else if Substring.isSubstring "Search terminated" writ_log
   2.157 -        then SOME "no counterexample (normal termination)"
   2.158 -        else SOME "no counterexample (unknown)"
   2.159 -  in r end
   2.160 -*)
   2.161 -
   2.162 -fun quickcheck_action settings {pre=st, ...} =
   2.163 -  let
   2.164 -    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
   2.165 -    val args = filter has_valid_key settings
   2.166 -  in
   2.167 -    (case Quickcheck.quickcheck args 1 st of
   2.168 -      NONE => SOME "no counterexample"
   2.169 -    | SOME _ => SOME "counterexample found")
   2.170 -  end
   2.171 -
   2.172 -
   2.173 -fun arith_action _ {pre=st, ...} = 
   2.174 -  if can_apply Arith_Data.arith_tac st
   2.175 -  then SOME "succeeded"
   2.176 -  else NONE
   2.177 -
   2.178 -
   2.179 -fun sledgehammer_action settings {pre=st, ...} =
   2.180 -  let
   2.181 -    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
   2.182 -    val thy = Proof.theory_of st
   2.183 - 
   2.184 -    val prover = the (AtpManager.get_prover prover_name thy)
   2.185 -    val timeout = AtpManager.get_timeout () 
   2.186 -
   2.187 -    val (success, message) =
   2.188 -      let
   2.189 -        val (success, message, _, _, _) =
   2.190 -          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
   2.191 -      in (success, message) end
   2.192 -      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
   2.193 -           | ERROR msg => (false, "error: " ^ msg)
   2.194 -  in
   2.195 -    if success
   2.196 -    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
   2.197 -    else NONE
   2.198 -  end
   2.199 -
   2.200 -
   2.201 -fun metis_action settings {pre, post} =
   2.202 -  let
   2.203 -    val thms = theorems_of_sucessful_proof post
   2.204 -    val names = map Thm.get_name thms
   2.205 -
   2.206 -    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
   2.207 -
   2.208 -    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   2.209 -  in
   2.210 -    (if can_apply metis pre then "succeeded" else "failed")
   2.211 -    |> suffix (" (" ^ commas names ^ ")")
   2.212 -    |> SOME
   2.213 -  end
   2.214 -
   2.215 -
   2.216 -
   2.217 -(* Mirabelle setup *)
   2.218 -
   2.219 -val setup =
   2.220 -  setup_config #>
   2.221 -(* FIXME  register "refute" refute_action #> *)
   2.222 -  register "quickcheck" quickcheck_action #>
   2.223 -  register "arith" arith_action #>
   2.224 -  register "sledgehammer" sledgehammer_action #>
   2.225 -  register "metis" metis_action (* #> FIXME:
   2.226 -  Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
   2.227 -
   2.228  end
   2.229 -
   2.230 -val _ = Toplevel.add_hook Mirabelle.step_hook
   2.231 -
   2.232 -(* no multithreading, no parallel proofs *)
   2.233 -val _ = Multithreading.max_threads := 1
   2.234 -val _ = Goal.parallel_proofs := 0

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Fri Aug 21 13:21:19 2009 +0200
     3.3 @@ -0,0 +1,15 @@
     3.4 +(* Title:  mirabelle_arith.ML
     3.5 +   Author: Jasmin Blanchette and Sascha Boehme
     3.6 +*)
     3.7 +
     3.8 +structure Mirabelle_Arith : MIRABELLE_ACTION =
     3.9 +struct
    3.10 +
    3.11 +fun arith_action {pre=st, ...} =
    3.12 +  if Mirabelle.can_apply Arith_Data.arith_tac st
    3.13 +  then SOME "succeeded"
    3.14 +  else NONE
    3.15 +
    3.16 +fun invoke _ = Mirabelle.register ("arith", arith_action)
    3.17 +
    3.18 +end

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Fri Aug 21 13:21:19 2009 +0200
     4.3 @@ -0,0 +1,24 @@
     4.4 +(* Title:  mirabelle_metis.ML
     4.5 +   Author: Jasmin Blanchette and Sascha Boehme
     4.6 +*)
     4.7 +
     4.8 +structure Mirabelle_Metis : MIRABELLE_ACTION =
     4.9 +struct
    4.10 +
    4.11 +fun metis_action {pre, post} =
    4.12 +  let
    4.13 +    val thms = Mirabelle.theorems_of_sucessful_proof post
    4.14 +    val names = map Thm.get_name thms
    4.15 +
    4.16 +    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
    4.17 +
    4.18 +    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
    4.19 +  in
    4.20 +    (if Mirabelle.can_apply metis pre then "succeeded" else "failed")
    4.21 +    |> suffix (" (" ^ commas names ^ ")")
    4.22 +    |> SOME
    4.23 +  end
    4.24 +
    4.25 +fun invoke _ = Mirabelle.register ("metis", metis_action)
    4.26 +
    4.27 +end

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Aug 21 13:21:19 2009 +0200
     5.3 @@ -0,0 +1,19 @@
     5.4 +(* Title:  mirabelle_quickcheck.ML
     5.5 +   Author: Jasmin Blanchette and Sascha Boehme
     5.6 +*)
     5.7 +
     5.8 +structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     5.9 +struct
    5.10 +
    5.11 +fun quickcheck_action args {pre=st, ...} =
    5.12 +  let
    5.13 +    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    5.14 +  in
    5.15 +    (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
    5.16 +      NONE => SOME "no counterexample"
    5.17 +    | SOME _ => SOME "counterexample found")
    5.18 +  end
    5.19 +
    5.20 +fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
    5.21 +
    5.22 +end

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Fri Aug 21 13:21:19 2009 +0200
     6.3 @@ -0,0 +1,36 @@
     6.4 +(* Title:  mirabelle_refute.ML
     6.5 +   Author: Jasmin Blanchette and Sascha Boehme
     6.6 +*)
     6.7 +
     6.8 +structure Mirabelle_Refute : MIRABELLE_ACTION =
     6.9 +struct
    6.10 +
    6.11 +
    6.12 +fun refute_action args {pre=st, ...} = 
    6.13 +  let
    6.14 +    val subgoal = 0
    6.15 +    val thy     = Proof.theory_of st
    6.16 +    val thm = goal_thm_of st
    6.17 +
    6.18 +    val _ = Refute.refute_subgoal thy args thm subgoal
    6.19 +  in
    6.20 +    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
    6.21 +    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
    6.22 +
    6.23 +    val r =
    6.24 +      if Substring.isSubstring "model found" writ_log
    6.25 +      then
    6.26 +        if Substring.isSubstring "spurious" warn_log
    6.27 +        then SOME "potential counterexample"
    6.28 +        else SOME "real counterexample (bug?)"
    6.29 +      else
    6.30 +        if Substring.isSubstring "time limit" writ_log
    6.31 +        then SOME "no counterexample (time out)"
    6.32 +        else if Substring.isSubstring "Search terminated" writ_log
    6.33 +        then SOME "no counterexample (normal termination)"
    6.34 +        else SOME "no counterexample (unknown)"
    6.35 +  in r end
    6.36 +
    6.37 +fun invoke args = Mirabelle.register ("refute", refute_action args)
    6.38 +
    6.39 +end

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 21 13:21:19 2009 +0200
     7.3 @@ -0,0 +1,31 @@
     7.4 +(* Title:  mirabelle_sledgehammer.ML
     7.5 +   Author: Jasmin Blanchette and Sascha Boehme
     7.6 +*)
     7.7 +
     7.8 +structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
     7.9 +struct
    7.10 +
    7.11 +fun sledgehammer_action {pre=st, ...} =
    7.12 +  let
    7.13 +    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
    7.14 +    val thy = Proof.theory_of st
    7.15 + 
    7.16 +    val prover = the (AtpManager.get_prover prover_name thy)
    7.17 +    val timeout = AtpManager.get_timeout () 
    7.18 +
    7.19 +    val (success, message) =
    7.20 +      let
    7.21 +        val (success, message, _, _, _) =
    7.22 +          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
    7.23 +      in (success, message) end
    7.24 +      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
    7.25 +           | ERROR msg => (false, "error: " ^ msg)
    7.26 +  in
    7.27 +    if success
    7.28 +    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
    7.29 +    else NONE
    7.30 +  end
    7.31 +
    7.32 +fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action)
    7.33 +
    7.34 +end

     8.1 --- a/src/HOL/Tools/Mirabelle/etc/settings	Fri Aug 21 09:49:10 2009 +0200
     8.2 +++ b/src/HOL/Tools/Mirabelle/etc/settings	Fri Aug 21 13:21:19 2009 +0200
     8.3 @@ -1,6 +1,7 @@
     8.4  MIRABELLE_HOME="$COMPONENT"
     8.5  
     8.6  MIRABELLE_LOGIC=HOL
     8.7 +MIRABELLE_THEORY=Main
     8.8  MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
     8.9  MIRABELLE_TIMEOUT=30
    8.10  MIRABELLE_VERBOSE=false

     9.1 --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Fri Aug 21 09:49:10 2009 +0200
     9.2 +++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Fri Aug 21 13:21:19 2009 +0200
     9.3 @@ -7,14 +7,21 @@
     9.4  
     9.5  PRG="$(basename "$0")"
     9.6  
     9.7 +function action_names() {
     9.8 +  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
     9.9 +  ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
    9.10 +}
    9.11 +
    9.12  function usage() {
    9.13    out="$MIRABELLE_OUTPUT_PATH"
    9.14    timeout="$MIRABELLE_TIMEOUT"
    9.15 +  action_names
    9.16    echo
    9.17    echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
    9.18    echo
    9.19    echo "  Options are:"
    9.20    echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
    9.21 +  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
    9.22    echo "    -O DIR       output directory for test data (default $out)"
    9.23    echo "    -v           be verbose"
    9.24    echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
    9.25 @@ -23,7 +30,11 @@
    9.26    echo "  at all proof steps in the given theory files."
    9.27    echo
    9.28    echo "  ACTIONS is a colon-separated list of actions, where each action is"
    9.29 -  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]."
    9.30 +  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
    9.31 +  for NAME in $ACTION_NAMES
    9.32 +  do
    9.33 +    echo "    $NAME"
    9.34 +  done
    9.35    echo
    9.36    echo "  FILES is a space-separated list of theory files, where each file is"
    9.37    echo "  either NAME.thy or NAME.thy[START:END] and START and END are numbers"
    9.38 @@ -37,12 +48,15 @@
    9.39  
    9.40  # options
    9.41  
    9.42 -while getopts "L:O:vt:" OPT
    9.43 +while getopts "L:T:O:vt:" OPT
    9.44  do
    9.45    case "$OPT" in
    9.46      L)
    9.47        MIRABELLE_LOGIC="$OPTARG"
    9.48        ;;
    9.49 +    T)
    9.50 +      MIRABELLE_THEORY="$OPTARG"
    9.51 +      ;;
    9.52      O)
    9.53        MIRABELLE_OUTPUT_PATH="$OPTARG"
    9.54        ;;

    10.1 --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 09:49:10 2009 +0200
    10.2 +++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 13:21:19 2009 +0200
    10.3 @@ -11,6 +11,7 @@
    10.4  my $isabelle_home = $ENV{'ISABELLE_HOME'};
    10.5  my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
    10.6  my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
    10.7 +my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
    10.8  my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
    10.9  my $verbose = $ENV{'MIRABELLE_VERBOSE'};
   10.10  my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
   10.11 @@ -41,11 +42,23 @@
   10.12  my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
   10.13  my $log_file = $output_path . "/" . $thy_name . ".log";
   10.14  
   10.15 +my @action_files;
   10.16 +foreach (split(/:/, $actions)) {
   10.17 +  if (m/([^[]*)/) {
   10.18 +    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
   10.19 +  }
   10.20 +}
   10.21 +my $tools = "";
   10.22 +if ($#action_files >= 0) {
   10.23 +  $tools = "uses " . join(" ", @action_files);
   10.24 +}
   10.25 +
   10.26  open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
   10.27  
   10.28  print SETUP_FILE <<END;
   10.29  theory "$setup_thy_name"
   10.30 -imports "$mirabelle_thy"
   10.31 +imports "$mirabelle_thy" "$mirabelle_theory"
   10.32 +$tools
   10.33  begin
   10.34  
   10.35  setup {* 
   10.36 @@ -61,7 +74,8 @@
   10.37  foreach (split(/:/, $actions)) {
   10.38    if (m/([^[]*)(?:\[(.*)\])?/) {
   10.39      my ($name, $settings_str) = ($1, $2 || "");
   10.40 -    print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" [";
   10.41 +    $name =~ s/^([a-z])/\U$1/;
   10.42 +    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
   10.43      my $sep = "";
   10.44      foreach (split(/,/, $settings_str)) {
   10.45        if (m/\s*(.*)\s*=\s*(.*)\s*/) {