Streamlined the signal handler in watcher.ML
authorquigley
Mon Jul 04 15:51:56 2005 +0200 (2005-07-04)
changeset 1667596bdc59afc05
parent 16674 bf2cd93cc245
child 16676 671bd433b9eb
Streamlined the signal handler in watcher.ML
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Mon Jul 04 15:15:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Mon Jul 04 15:51:56 2005 +0200
     1.3 @@ -184,16 +184,36 @@
     1.4                   Posix.Process.sleep(Time.fromSeconds 1);
     1.5                   true
     1.6                 end)
     1.7 -            else if (thisLine = "% Proof not found.\n")
     1.8 +            else if (thisLine = "% Proof not found. Time limit expired.\n")
     1.9              then
    1.10 -              (
    1.11 -               Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.12 -               TextIO.output (toParent,childCmd^"\n" );
    1.13 -               TextIO.flushOut toParent;
    1.14 -               TextIO.output (toParent, thisLine);
    1.15 -               TextIO.flushOut toParent;
    1.16 +              (let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.17 +                           val _ = TextIO.output (outfile, (thisLine))
    1.18 +
    1.19 +                           val _ =  TextIO.closeOut outfile
    1.20 +               in
    1.21  
    1.22 -               true)
    1.23 +                 TextIO.output (toParent,childCmd^"\n" );
    1.24 +                 TextIO.flushOut toParent;
    1.25 +                 TextIO.output (vamp_proof_file, (thisLine));
    1.26 +                 TextIO.flushOut vamp_proof_file;
    1.27 +                 TextIO.closeOut vamp_proof_file;
    1.28 +                 (*TextIO.output (toParent, thisLine);
    1.29 +                  TextIO.flushOut toParent;
    1.30 +                  TextIO.output (toParent, "bar\n");
    1.31 +                  TextIO.flushOut toParent;*)
    1.32 +
    1.33 +                 TextIO.output (toParent, thisLine^"\n");
    1.34 +                 TextIO.flushOut toParent;
    1.35 +                 TextIO.output (toParent, thmstring^"\n");
    1.36 +                 TextIO.flushOut toParent;
    1.37 +                 TextIO.output (toParent, goalstring^"\n");
    1.38 +                 TextIO.flushOut toParent;
    1.39 +                 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.40 +                 (* Attempt to prevent several signals from turning up simultaneously *)
    1.41 +                 Posix.Process.sleep(Time.fromSeconds 1);
    1.42 +                 true
    1.43 +               end
    1.44 +              )
    1.45  
    1.46              else
    1.47                (TextIO.output (vamp_proof_file, (thisLine));
    1.48 @@ -238,7 +258,7 @@
    1.49               (reconstr, thmstring, goalstring)
    1.50             end
    1.51               )
    1.52 -        else  if (thisLine = "% Proof not found.\n")
    1.53 +        else  if (thisLine = "% Proof not found. Time limit expired.\n")
    1.54          then
    1.55            (
    1.56             let val reconstr = thisLine
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Jul 04 15:15:55 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Jul 04 15:51:56 2005 +0200
     2.3 @@ -165,8 +165,8 @@
     2.4                               (prover^thmstring^goalstring^proverCmd^settings^
     2.5                                clasimpfile^hypsfile^probfile)
     2.6        in sendOutput (toWatcherStr,    
     2.7 -            (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
     2.8 -             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
     2.9 +            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
    2.10 +             settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n"));
    2.11           goals_being_watched := (!goals_being_watched) + 1;
    2.12  	 TextIO.flushOut toWatcherStr;
    2.13  	 callResProvers (toWatcherStr,args)
    2.14 @@ -213,33 +213,33 @@
    2.15    let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
    2.16        val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
    2.17        val _ =  TextIO.closeOut outfile
    2.18 -      val (prover, rest) = takeUntil "*" str []
    2.19 +      val (prover, rest) = takeUntil "$" str []
    2.20        val prover = implode prover
    2.21  
    2.22 -      val (thmstring, rest) =  takeUntil "*" rest []
    2.23 +      val (thmstring, rest) =  takeUntil "$" rest []
    2.24        val thmstring = implode thmstring
    2.25  
    2.26 -      val (goalstring, rest) =  takeUntil "*" rest []
    2.27 +      val (goalstring, rest) =  takeUntil "$" rest []
    2.28        val goalstring = implode goalstring
    2.29  
    2.30 -      val (proverCmd, rest ) =  takeUntil "*" rest []
    2.31 +      val (proverCmd, rest ) =  takeUntil "$" rest []
    2.32        val proverCmd = implode proverCmd
    2.33        
    2.34 -      val (settings, rest) =  takeUntil "*" rest []
    2.35 +      val (settings, rest) =  takeUntil "$" rest []
    2.36        val settings = getSettings settings []
    2.37  
    2.38 -      val (clasimpfile, rest ) =  takeUntil "*" rest []
    2.39 +      val (clasimpfile, rest ) =  takeUntil "$" rest []
    2.40        val clasimpfile = implode clasimpfile
    2.41        
    2.42 -      val (hypsfile, rest ) =  takeUntil "*" rest []
    2.43 +      val (hypsfile, rest ) =  takeUntil "$" rest []
    2.44        val hypsfile = implode hypsfile
    2.45  
    2.46 -      val (file, rest) =  takeUntil "*" rest []
    2.47 +      val (file, rest) =  takeUntil "$" rest []
    2.48        val file = implode file
    2.49  
    2.50        val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    2.51                    ("Sep comms are: "^(implode str)^"**"^
    2.52 -                   prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n")
    2.53 +                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^" \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
    2.54    in
    2.55       (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
    2.56    end
    2.57 @@ -289,6 +289,7 @@
    2.58      val newfile =   if !SpassComm.spass 
    2.59  		    then 
    2.60  			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    2.61 +
    2.62  		    else
    2.63  			    (File.platform_path wholefile)
    2.64      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    2.65 @@ -813,6 +814,8 @@
    2.66                             VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
    2.67                            
    2.68  
    2.69 +
    2.70 +
    2.71  fun spass_proofHandler (n) = (
    2.72                                   let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    2.73                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    2.74 @@ -844,9 +847,8 @@
    2.75                                                                   else
    2.76                                                                      ()
    2.77                                                              )
    2.78 -                                                    (* if there's no proof, but a message from Spass *)
    2.79 -                                                    else if ((substring (reconstr, 0,5))= "SPASS")
    2.80 -                                                         then
    2.81 +                                                    (* if there's no proof, but a some sort of  message from Spass *)
    2.82 +                                                    else 
    2.83                                                                   (
    2.84                                                                       goals_being_watched := (!goals_being_watched) -1;
    2.85                                                                       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    2.86 @@ -862,67 +864,7 @@
    2.87                                                                             end )
    2.88                                                                        else
    2.89                                                                           ()
    2.90 -                                                                ) 
    2.91 -						   (* print out a list of rules used from clasimpset*)
    2.92 -                                                    else if ((substring (reconstr, 0,5))= "Rules")
    2.93 -                                                         then
    2.94 -                                                                 (
    2.95 -                                                                     goals_being_watched := (!goals_being_watched) -1;
    2.96 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    2.97 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
    2.98 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
    2.99 -                                                                      if (!goals_being_watched = 0)
   2.100 -                                                                      then 
   2.101 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   2.102 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.103 -                                                                               val _ =  TextIO.closeOut outfile
   2.104 -                                                                           in
   2.105 -                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.106 -                                                                           end )
   2.107 -                                                                      else
   2.108 -                                                                         ()
   2.109 -                                                                )
   2.110 -							
   2.111 -                                                          (* if proof translation failed *)
   2.112 -                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   2.113 -                                                               then 
   2.114 -                                                                   (
   2.115 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   2.116 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.117 -                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   2.118 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   2.119 -                                                                       if (!goals_being_watched = 0)
   2.120 -                                                                       then 
   2.121 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   2.122 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.123 -                                                                               val _ =  TextIO.closeOut outfile
   2.124 -                                                                            in
   2.125 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.126 -                                                                            end )
   2.127 -                                                                       else
   2.128 -                                                                          ( )
   2.129 -                                                                      )
   2.130 -
   2.131 -
   2.132 -                                                                else  (* add something here ?*)
   2.133 -                                                                   (
   2.134 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   2.135 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.136 -                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   2.137 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   2.138 -                                                                       if (!goals_being_watched = 0)
   2.139 -                                                                       then 
   2.140 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   2.141 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.142 -                                                                               val _ =  TextIO.closeOut outfile
   2.143 -                                                                            in
   2.144 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.145 -                                                                            end )
   2.146 -                                                                       else
   2.147 -                                                                          ( )
   2.148 -                                                                      )
   2.149 -                                                                     
   2.150 -                                                                           
   2.151 +                                                                )						               
   2.152                                                              
   2.153                                         end)
   2.154  
     3.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jul 04 15:15:55 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jul 04 15:51:56 2005 +0200
     3.3 @@ -48,7 +48,6 @@
     3.4  (*val spass = ref true;*)
     3.5  
     3.6  val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
     3.7 -
     3.8  val vampire = ref false;
     3.9  
    3.10  val trace_res = ref false;
    3.11 @@ -209,7 +208,7 @@
    3.12       else
    3.13         let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    3.14         in  
    3.15 -	   ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", 
    3.16 +	   ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", 
    3.17  	      clasimpfile, axfile, hypsfile, probfile)] @ 
    3.18  	    (make_atp_list xs sign (n+1)))
    3.19         end