# HG changeset patch
# User boehmes
# Date 1253181456 -7200
# Node ID 3711565687a6d48f08ed4601982c1e447d98557a
# Parent  719426c9e1eb656340a73457066aaf663b5f873b
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
new "eproof" script written in Perl (hopefully more stable than the one coming with E)

diff -r 719426c9e1eb -r 3711565687a6 Admin/E/eproof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/E/eproof	Thu Sep 17 11:57:36 2009 +0200
@@ -0,0 +1,86 @@
+#!/usr/bin/perl -w
+#
+# eproof - run E and translate its output into TSTP format
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# This script is a port of a Bash script with the same name coming with
+# E 1.0-004 (written by Stephan Schulz).
+#
+
+
+use File::Basename qw/ dirname /;
+use File::Temp qw/ tempfile /;
+
+
+# E executables
+
+my $edir = dirname($0);
+my $eprover = "$edir/eprover";
+my $epclextract = "$edir/epclextract";
+
+
+# build E command from given commandline arguments
+
+my $format = "";
+my $eprover_cmd = $eprover;
+foreach (@ARGV) {
+  if (m/--tstp-out/) {
+    $format = $_;
+  }
+  else {
+    $eprover_cmd = "$eprover_cmd '$_'";
+  }
+}
+$eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact";
+
+
+# run E, redirecting output into a temporary file
+
+my ($fh, $filename) = tempfile(UNLINK => 1);
+my $r = system "$eprover_cmd > $filename";
+exit ($r >> 8) if $r != 0;
+
+
+# analyze E output
+
+my @lines = <$fh>;
+my $content = join "", @lines[-60 .. -1];
+  # Note: Like the original eproof, we only look at the last 60 lines.
+
+if ($content =~ m/Total time/) {
+  if ($content =~ m/No proof found!/) {
+    print "# Problem is satisfiable (or invalid), " .
+      "generating saturation derivation\n";
+  }
+  elsif ($content =~ m/Proof found!/) {
+    print "# Problem is unsatisfiable (or provable), " .
+      "constructing proof object\n";
+  }
+  elsif ($content =~ m/Watchlist is empty!/) {
+    print "# All watchlist clauses generated, constructing derivation\n";
+  }
+  else {
+    print "# Cannot determine problem status\n";
+    exit $r;
+  }
+}
+else {
+  print "# Cannot determine problem status within resource limit\n";
+  exit $r;
+}
+
+
+# extract E output
+
+foreach (@lines) {
+  print if (m/# SZS status/ or m/"# Failure"/);
+}
+$r = system "$epclextract $format -f --competition-framing $filename";
+  # Note: Before extraction, the original eproof invokes 'ulimit -S -t TIME'
+  # where TIME is the remaining time from the time limit given at the command
+  # line. This does not seem very reliable and is not implemented here. This
+  # is not a problem as long as extraction is reasonable fast or the invoking
+  # process enforces a time limit of its own.
+exit ($r >> 8);
+
diff -r 719426c9e1eb -r 3711565687a6 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Sep 15 15:29:11 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 17 11:57:36 2009 +0200
@@ -79,14 +79,17 @@
       preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
 
     (* write out problem file and call prover *)
-    val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
-    fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
-      [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
+    fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
+      [File.shell_path cmd, args, File.platform_path probfile] ^ " ; } 2>&1"
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n")
         val (proof, t) = s |> split |> split_last |> apfst cat_lines
-        val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
+        fun as_num f = f >> (fst o read_int)
+        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
+        val digit = Scan.one Symbol.is_ascii_digit
+        val num3 = as_num (digit ::: digit ::: (digit >> single))
+        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
       in (proof, as_time t) end
     fun run_on probfile =
@@ -97,7 +100,7 @@
       else error ("Bad executable: " ^ Path.implode cmd)
 
     (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
-    fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
+    fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE
     fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
 
diff -r 719426c9e1eb -r 3711565687a6 src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl
--- a/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Tue Sep 15 15:29:11 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-use POSIX qw(setsid);
-
-$SIG{'INT'} = "DEFAULT";
-
-defined (my $pid = fork) or die "$!";
-if (not $pid) {
-  POSIX::setsid or die $!;
-  exec @ARGV;
-}
-else {
-  wait;
-  my ($user, $system, $cuser, $csystem) = times;
-  my $time = ($user + $cuser) * 1000;
-  print "$time\n";
-}