From: Stefano Zacchiroli Date: Wed, 13 Nov 2002 14:44:19 +0000 (+0000) Subject: switched to OCaml HTTP module X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc9aab4ebfab88492cbaef935c79221f648d8313;p=helm.git switched to OCaml HTTP module --- diff --git a/helm/proofChecker/Makefile b/helm/proofChecker/Makefile index 107d5699e..aada8a030 100644 --- a/helm/proofChecker/Makefile +++ b/helm/proofChecker/Makefile @@ -1,5 +1,5 @@ BIN_DIR = /usr/local/bin -REQUIRES = helm-cic_proof_checking +REQUIRES = helm-cic_proof_checking http PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index b5a2625c2..26d830994 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -1,4 +1,4 @@ -(* 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 @@ -23,41 +23,76 @@ * 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 +" + + Proof-Checking %s + + +

Proof-Checking %s:

+" + uri uri)), +("

Done.

+ + +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 ();; 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); -}