1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Oct 10 14:43:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Oct 10 15:35:29 2005 +0200
     1.3 @@ -29,6 +29,17 @@
     1.4  val destdir = ref "";   (*Empty means write files to /tmp*)
     1.5  val problem_name = ref "prob";
     1.6  
     1.7 +(*Return the path to a "helper" like SPASS or tptp2X, first checking that
     1.8 +  it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
     1.9 +fun helper_path evar base =
    1.10 +  case getenv evar of
    1.11 +      "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    1.12 +    | home => 
    1.13 +        let val path = home ^ "/" ^ base
    1.14 +        in  if File.exists (File.unpack_platform_path path) then path 
    1.15 +	    else error ("Could not find the file " ^ path)
    1.16 +	end;  
    1.17 +
    1.18  fun probfile_nosuffix _ = 
    1.19    if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    1.20    else if File.exists (File.unpack_platform_path (!destdir))
    1.21 @@ -106,7 +117,7 @@
    1.22                             "%-DocProof%-TimeLimit=" ^ time
    1.23                        else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    1.24                    val _ = debug ("SPASS option string is " ^ optionline)
    1.25 -                  val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.26 +                  val _ = helper_path "SPASS_HOME" "SPASS"
    1.27                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.28                in 
    1.29                    ([("spass", 
    1.30 @@ -116,14 +127,14 @@
    1.31                end
    1.32              else if !prover = "vampire"
    1.33  	    then 
    1.34 -              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
    1.35 +              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.36                in
    1.37                  ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
    1.38                   (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.39                end
    1.40        	     else if !prover = "E"
    1.41        	     then
    1.42 -	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    1.43 +	       let val Eprover = helper_path "E_HOME" "eproof"
    1.44  	       in
    1.45  		  ([("E", Eprover, 
    1.46  		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    1.47 @@ -172,7 +183,7 @@
    1.48      (case !last_watcher_pid of 
    1.49           NONE => ()
    1.50         | SOME (_, childout, pid, files) => 
    1.51 -	  (debug ("Killing old watcher, pid = " ^ Int.toString (ResLib.intOfPid pid));
    1.52 +	  (debug ("Killing old watcher, pid = " ^ string_of_pid pid);
    1.53  	   Watcher.killWatcher pid;  
    1.54  	   ignore (map (try OS.FileSys.remove) files)))
    1.55       handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    1.56 @@ -190,7 +201,7 @@
    1.57      in
    1.58        last_watcher_pid := SOME (childin, childout, pid, files);
    1.59        debug ("problem files: " ^ space_implode ", " files); 
    1.60 -      debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
    1.61 +      debug ("pid: " ^ string_of_pid pid);
    1.62        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    1.63      end);
    1.64