X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.pl;fp=helm%2FproofChecker%2FproofChecker.pl;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=fde4b43eaf3fa924a626d98f3ecff4a2b7102ce2;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/proofChecker/proofChecker.pl b/helm/proofChecker/proofChecker.pl deleted file mode 100755 index fde4b43ea..000000000 --- a/helm/proofChecker/proofChecker.pl +++ /dev/null @@ -1,70 +0,0 @@ -#!/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, ">\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 < - - Proof-Checking $uri - - -

Proof-Checking $uri:

-EOT - while(chomp($_ = )) { - last if ($_ eq "END"); - print $c $_."\n"; - } - print $c <Done. - - -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); -}