*)
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() ;
--- /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 $_;
+ }
+ print $c <<EOT;
+</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 / commitdiff