allow spaces in executable names;
authorwenzelm
Sun Mar 13 14:51:38 2011 +0100 (2011-03-13)
changeset 41940a3b68a7a0e15
parent 41939 eb9fb5a4d27f
child 41941 f823f7fae9a2
allow spaces in executable names;
simplified generated bash scripts;
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 13:57:20 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 14:51:38 2011 +0100
     1.3 @@ -782,17 +782,16 @@
     1.4  fun prelude system =
     1.5    case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
     1.6  
     1.7 -fun invoke system file_name =
     1.8 +fun invoke system file =
     1.9    let
    1.10 -    val env_var =
    1.11 -      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
    1.12 -    val prog = getenv env_var
    1.13 -    val cmd =
    1.14 -      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
    1.15 +    val (env_var, cmd) =
    1.16 +      (case system of
    1.17 +        SWI_PROLOG => ("EXEC_SWIPL", "\"$EXEC_SWIPL\" -f ")
    1.18 +      | YAP => ("EXEC_YAP", "\"$EXEC_YAP\" -L "))
    1.19    in
    1.20 -    if prog = "" then
    1.21 +    if getenv env_var = "" then
    1.22        (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
    1.23 -    else fst (bash_output (cmd ^ file_name))
    1.24 +    else fst (bash_output (cmd ^ File.shell_path file))
    1.25    end
    1.26  
    1.27  (* parsing prolog solution *)
    1.28 @@ -857,7 +856,7 @@
    1.29      val _ = tracing ("Generated prolog program:\n" ^ prog)
    1.30      val solution = TimeLimit.timeLimit timeout (fn prog =>
    1.31        Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
    1.32 -        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
    1.33 +        (File.write prolog_file prog; invoke system prolog_file))) prog
    1.34      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
    1.35      val tss = parse_solutions solution
    1.36    in
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 13:57:20 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 14:51:38 2011 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4          val _ = File.write narrowing_engine_file narrowing_engine
     2.5          val _ = File.write main_file main
     2.6          val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
     2.7 -        val cmd = getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ 
     2.8 +        val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^
     2.9            (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^
    2.10            " -o " ^ executable ^ " && " ^ executable
    2.11        in
     3.1 --- a/src/Tools/Code/code_haskell.ML	Sun Mar 13 13:57:20 2011 +0100
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Mar 13 14:51:38 2011 +0100
     3.3 @@ -453,8 +453,9 @@
     3.4    Code_Target.add_target
     3.5      (target, { serializer = serializer, literals = literals,
     3.6        check = { env_var = "EXEC_GHC", make_destination = I,
     3.7 -        make_command = fn ghc => fn module_name =>
     3.8 -          ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
     3.9 +        make_command = fn module_name =>
    3.10 +          "\"$EXEC_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
    3.11 +            module_name ^ ".hs" } })
    3.12    #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    3.13        brackify_infix (1, R) fxy (
    3.14          print_typ (INFX (1, X)) ty1,
     4.1 --- a/src/Tools/Code/code_ml.ML	Sun Mar 13 13:57:20 2011 +0100
     4.2 +++ b/src/Tools/Code/code_ml.ML	Sun Mar 13 14:51:38 2011 +0100
     4.3 @@ -836,12 +836,14 @@
     4.4  val setup =
     4.5    Code_Target.add_target
     4.6      (target_SML, { serializer = serializer_sml, literals = literals_sml,
     4.7 -      check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     4.8 -        make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
     4.9 +      check = { env_var = "ISABELLE_PROCESS",
    4.10 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    4.11 +        make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
    4.12    #> Code_Target.add_target
    4.13      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    4.14 -      check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    4.15 -        make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
    4.16 +      check = { env_var = "EXEC_OCAML",
    4.17 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    4.18 +        make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } })
    4.19    #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    4.20        brackify_infix (1, R) fxy (
    4.21          print_typ (INFX (1, X)) ty1,
     5.1 --- a/src/Tools/Code/code_scala.ML	Sun Mar 13 13:57:20 2011 +0100
     5.2 +++ b/src/Tools/Code/code_scala.ML	Sun Mar 13 14:51:38 2011 +0100
     5.3 @@ -421,10 +421,8 @@
     5.4      (target, { serializer = serializer, literals = literals,
     5.5        check = { env_var = "SCALA_HOME",
     5.6          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
     5.7 -        make_command = fn scala_home => fn _ =>
     5.8 -          "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
     5.9 -            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac"))
    5.10 -            ^ " ROOT.scala" } })
    5.11 +        make_command = fn _ =>
    5.12 +          "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
    5.13    #> Code_Target.add_tyco_syntax target "fun"
    5.14       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    5.15          brackify_infix (1, R) fxy (
     6.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 13 13:57:20 2011 +0100
     6.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 13 14:51:38 2011 +0100
     6.3 @@ -35,8 +35,8 @@
     6.4    type serializer
     6.5    type literals = Code_Printer.literals
     6.6    val add_target: string * { serializer: serializer, literals: literals,
     6.7 -    check: { env_var: string, make_destination: Path.T -> Path.T,
     6.8 -      make_command: string -> string -> string } } -> theory -> theory
     6.9 +    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
    6.10 +    -> theory -> theory
    6.11    val extend_target: string *
    6.12        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    6.13      -> theory -> theory
    6.14 @@ -129,7 +129,7 @@
    6.15  datatype description = Fundamental of { serializer: serializer,
    6.16        literals: literals,
    6.17        check: { env_var: string, make_destination: Path.T -> Path.T,
    6.18 -        make_command: string -> string -> string } }
    6.19 +        make_command: string -> string } }
    6.20    | Extension of string *
    6.21        (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    6.22  
    6.23 @@ -392,18 +392,17 @@
    6.24      val module_name = "Code";
    6.25      val { env_var, make_destination, make_command } =
    6.26        (#check o the_fundamental thy) target;
    6.27 -    val env_param = getenv env_var;
    6.28      fun ext_check p =
    6.29        let 
    6.30          val destination = make_destination p;
    6.31          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    6.32            module_name args naming program names_cs);
    6.33 -        val cmd = make_command env_param module_name;
    6.34 +        val cmd = make_command module_name;
    6.35        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    6.36          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    6.37          else ()
    6.38        end;
    6.39 -  in if env_param = ""
    6.40 +  in if getenv env_var = ""
    6.41      then if strict
    6.42        then error (env_var ^ " not set; cannot check code for " ^ target)
    6.43        else warning (env_var ^ " not set; skipped checking code for " ^ target)