+++ /dev/null
-#!/usr/bin/perl
-
-use HTTP::Daemon;
-use HTTP::Status;
-use HTTP::Response;
-use URI::Escape;
-use CGI;
-use FindBin;
-use IPC::Open3;
-
-chdir $FindBin::Bin; # chdir to the directory of this perl script
-
-my $d = new HTTP::Daemon LocalPort => 8085
- or die "Error: port 8085 not available.";
-print "Please contact me at: <URL:", $d->url, ">\n";
-
-my $IsProofCheckerLiving = 0;
-
-$SIG{CHLD} =
- sub {
- print stderr "\nERROR: The proof-checker died.\n";
- $IsProofCheckerLiving=0;
- };
-$| = 1;
-
-while(true) {
- open3(*PC_IN, *PC_OUT, *PC_ERR, "./proofChecker.opt 2>&1");
- $IsProofCheckerLiving=1;
- print stderr "\nWARNING: A new proof-checker starts.\n";
- PC_IN->autoflush(1);
-
- while (my $c = $d->accept) {
- my $r = $c->get_request;
- my $http_query = uri_unescape($r->url->query);
- my $cgi = new CGI("$http_query");
- my $uri = $cgi->param('uri');
-
- if ($r->method eq 'GET' && $r->url->path eq "/proofCheck"){
- print "Request to proof-check \"$uri\"...";
- print PC_IN "$uri\n";
- print $c <<EOT;
-<html>
-<head>
- <title>Proof-Checking $uri</title>
-</head>
-<body bgcolor="white">
-<h1>Proof-Checking $uri:</h1>
-EOT
- while(chomp($_ = <PC_OUT>)) {
- last if ($_ eq "END");
- print $c $_."\n";
- }
- print $c <<EOT;
-<h1>Done.</h1>
-</body>
-</html>
-EOT
- print " done\n\n";
- } else {
- print "INVALID REQUEST \"$http_query\"!!!!!\n\n";
- $c->send_error(RC_FORBIDDEN);
- }
- $c->close;
- undef($c);
- last unless $IsProofCheckerLiving;
- }
- close(PC_IN);
- close(PC_OUT);
- close(PC_ERR);
-}
projects / helm.git / blobdiff