helm/proofChecker/proofChecker.pl

   1 #!/usr/bin/perl
   2
   3 use HTTP::Daemon;
   4 use HTTP::Status;
   5 use HTTP::Response;
   6 use URI::Escape;
   7 use CGI;
   8 use FindBin;
   9 use IPC::Open3;
  10
  11 chdir $FindBin::Bin; # chdir to the directory of this perl script
  12
  13 $proofcheckerport = $ENV{'PROOF_CHECKER_PORT'} || $proofcheckerport;
  14
  15 my $d = new HTTP::Daemon LocalPort => $proofcheckerport
  16  or die "Error: port $proofcheckerport not available.";
  17 print "Please contact me at: <URL:", $d->url, ">\n";
  18
  19 my $IsProofCheckerLiving = 0;
  20
  21 $SIG{CHLD} =
  22    sub {
  23       print stderr "\nERROR: The proof-checker died.\n";
  24       $IsProofCheckerLiving=0;
  25    };
  26 $| = 1;
  27
  28 while(true) {
  29    open3(*PC_IN, *PC_OUT, *PC_ERR, "./proofChecker.opt 2>&1");
  30    $IsProofCheckerLiving=1;
  31    print stderr "\nWARNING: A new proof-checker starts.\n";
  32    PC_IN->autoflush(1);
  33
  34   while (my $c = $d->accept) {
  35     my $r = $c->get_request;
  36     my $http_query = uri_unescape($r->url->query);
  37     my $cgi = new CGI("$http_query");
  38     my $uri = $cgi->param('uri');
  39
  40     if ($r->method eq 'GET' && $r->url->path eq "/proofCheck"){
  41        print "Request to proof-check \"$uri\"...";
  42        print PC_IN "$uri\n";
  43        print $c <<EOT;
  44 <html>
  45 <head>
  46  <title>Proof-Checking $uri</title>
  47 </head>
  48 <body bgcolor="white">
  49 <h1>Proof-Checking $uri:</h1>
  50 EOT
  51        while(chomp($_ = <PC_OUT>)) {
  52          last if ($_ eq "END");
  53          print $c $_."\n";
  54        }
  55        print $c <<EOT;
  56 <h1>Done.</h1>
  57 </body>
  58 </html>
  59 EOT
  60        print " done\n\n";
  61     } else {
  62         print "INVALID REQUEST \"$http_query\"!!!!!\n\n";
  63         $c->send_error(RC_FORBIDDEN);
  64     }
  65     $c->close;
  66     undef($c);
  67     last unless $IsProofCheckerLiving;
  68   }
  69   close(PC_IN);
  70   close(PC_OUT);
  71   close(PC_ERR);
  72 }