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