From: Claudio Sacerdoti Coen Date: Fri, 30 Nov 2001 16:44:30 +0000 (+0000) Subject: New implementation of the proof-checker daemon: there is now X-Git-Tag: mlminidom_0_2_2~42 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84e62facde0ee126b5f08dd376086acd861a9320;p=helm.git New implementation of the proof-checker daemon: there is now only one sequential (= non concurrent) proof-checker that process one request at a time. The next big step will be to make it re-entrant. --- diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 4dfcb70b3..1c7245164 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -24,21 +24,33 @@ *) let main () = - let uris = ref [] in - Arg.parse [] - (fun uri -> uris := uri :: !uris) + let usage_msg = " -usage: proofChecker uri ... +usage: proofChecker[.opt] +The proof-checker reads from the stdin one URI at a time and proof-checks it. -List of options:"; - uris := List.rev !uris; - List.iter - (function uri -> - try - CicTypeChecker.typecheck (UriManager.uri_of_string uri) - with - e -> print_newline () ; flush stdout ; raise e - ) !uris +List of options:" + in + Arg.parse [] + (fun _ -> + begin + prerr_string "Error: no options expected.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end + ) usage_msg ; + while true do + begin + try + CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ())) + with + e -> + print_newline() ; + flush stdout ; + raise e + end ; + print_endline "END" + done ;; CicCooking.init() ; diff --git a/helm/proofChecker/proofChecker.pl b/helm/proofChecker/proofChecker.pl new file mode 100755 index 000000000..680d260d8 --- /dev/null +++ b/helm/proofChecker/proofChecker.pl @@ -0,0 +1,69 @@ +#!/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 $_; + } + print $c < + +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); +}