-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* http://cs.unibo.it/helm/.
*)
-let main () =
- let usage_msg =
- "
-usage: proofChecker[.opt]
-The proof-checker reads from the stdin one URI at a time and proof-checks it.
-
-List of options:"
- in
- Arg.parse []
- (fun _ ->
- begin
- prerr_string "Error: no options expected.\n" ;
- Arg.usage [] usage_msg ;
- exit (-1)
- end
- ) usage_msg ;
+open Printf;;
+
+let default_port = 48084;;
+
+let port =
try
- while true do
- begin
- try
- CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
- with
- End_of_file -> raise End_of_file
- | e ->
- print_newline() ;
- flush stdout ;
- raise e
- end ;
- print_endline "END"
- done
+ int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
with
- End_of_file -> ()
-;;
+ | Not_found -> default_port
+ | Failure "int_of_string" ->
+ prerr_endline "Warning: invalid port, reverting to default";
+ default_port
+in
+
+let (html_preamble, html_postamble) =
+ ((fun uri ->
+ (sprintf
+"<html>
+<head>
+ <title>Proof-Checking %s</title>
+</head>
+<body bgcolor=\"white\">
+<h1>Proof-Checking %s:</h1>
+"
+ uri uri)),
+("<h1>Done.</h1>
+</body>
+</html>
+END
+"))
+in
+
+let bad_request outchan =
+ printf "INVALID REQUEST !!!!!\n\n";
+ flush stdout;
+ Http.Daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
+ flush outchan
+in
+
+let callback req outchan =
+ match req#path with
+ | "/proofCheck" ->
+ begin
+ Logger.log_callback :=
+ (Logger.log_to_html
+ ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
+ try
+ let uri = req#param "uri" in
+ printf "Request to proof-check \"%s\"..." uri;
+ flush stdout;
+ fprintf outchan "%s" (html_preamble uri);
+ flush outchan;
+ (try
+ CicTypeChecker.typecheck (UriManager.uri_of_string uri);
+ with e ->
+ fprintf outchan "%s\n" (Printexc.to_string e);
+ flush outchan);
+ fprintf outchan "%s" html_postamble;
+ flush outchan;
+ printf " done\n\n";
+ flush stdout
+ with Not_found -> (* 'uri' argument not found *)
+ bad_request outchan
+ end
+ | req -> bad_request outchan
+
+in
+
+printf "Proof Checker started and listening on port %d\n" port;
+flush stdout;
+Http.Daemon.start' ~port callback;
+printf "Proof Checker is terminating, bye!\n"
-Logger.log_callback :=
- (Logger.log_to_html
- ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-main ();;
+++ /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 / commitdiff