slightly more robust bash exec, which fails on empty executable;
authorwenzelm
Sun Mar 13 19:27:39 2011 +0100 (2011-03-13)
changeset 41953994d088fbfbc
parent 41952 c7297638599b
child 41954 fb94df4505a0
slightly more robust bash exec, which fails on empty executable;
src/HOL/Matrix/Compute_Oracle/am_ghc.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 19:16:19 2011 +0100
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 19:27:39 2011 +0100
     1.3 @@ -227,7 +227,7 @@
     1.4          val module_file = tmp_file (module^".hs")
     1.5          val object_file = tmp_file (module^".o")
     1.6          val _ = writeTextFile module_file source
     1.7 -        val _ = bash ("\"$ISABELLE_GHC\" -c " ^ module_file)
     1.8 +        val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
     1.9          val _ =
    1.10            if not (fileExists object_file) then
    1.11              raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    1.12 @@ -311,7 +311,7 @@
    1.13          val term = print_term arity_of 0 t
    1.14          val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
    1.15          val _ = writeTextFile call_file call_source
    1.16 -        val _ = bash ("\"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    1.17 +        val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    1.18          val result = readResultFile result_file handle IO.Io _ =>
    1.19            raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    1.20          val t' = parse_result arity_of result
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 19:16:19 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 19:27:39 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 = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
     2.7 -        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
     2.8 +        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
     2.9            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    2.10            " -o " ^ executable ^ " && " ^ executable
    2.11        in