X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=e4f00fe3acf86c989b4e250af89000fda4942206;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=19df81c4ffb29eb5a3ded31d2280004312c8bf3e;hpb=ed6f2ada263b5137d139b45c772fbc010b412f26;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 19df81c4f..e4f00fe3a 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -25,17 +25,9 @@ open Printf;; -let default_port = 48084;; +let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";; -let port = - try - int_of_string (Sys.getenv "PROOF_CHECKER_PORT") - with - | Not_found -> default_port - | Failure "int_of_string" -> - prerr_endline "Warning: invalid port, reverting to default"; - default_port -in +let port = Helm_registry.get_int "proofchecker.port";; let (html_preamble, html_postamble) = ((fun uri -> @@ -45,55 +37,97 @@ let (html_preamble, html_postamble) = Proof-Checking %s -

Proof-Checking %s:

" uri uri)), -("

Done.

+("

Done.

END ")) -in +;; let bad_request outchan = printf "INVALID REQUEST !!!!!\n\n"; flush stdout; - Http.Daemon.respond_error ~status:(`Client_error `Bad_request) outchan; + Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) + outchan; flush outchan -in +;; + +let usage_string = +" + + + ProofChecker's help message + + +

ProofChecker

Usage

+ Usage: http://hostname:proofcheckerport/command +

+ Available commands: +

+ help
+ display this help message +

+ proofCheck?uri=uri
+ proof-checks the object whose URI is specified by uri +

+ + +" +;; + +let outchan = ref stderr;; + +let _ = + HelmLogger.register_log_callback + (fun ?append_NL msg -> + output_string !outchan (HelmLogger.html_of_html_msg msg) ; + flush !outchan) +;; -let callback req outchan = +let callback (req : Http_types.request) 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)); + outchan := outchan' ; try let uri = req#param "uri" in + Http_daemon.send_basic_headers ~code:(`Code 200) outchan' ; + Http_daemon.send_header "Content-type" "text/html" outchan' ; + Http_daemon.send_CRLF outchan' ; printf "Request to proof-check \"%s\"..." uri; flush stdout; - fprintf outchan "%s" (html_preamble uri); - flush outchan; + fprintf outchan' "%s" (html_preamble uri); + flush outchan'; (try - CicTypeChecker.typecheck (UriManager.uri_of_string uri); + ignore (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; + 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 + with Http_types.Param_not_found _ -> (* 'uri' argument not found *) + bad_request outchan' end - | req -> bad_request outchan + | "/help" -> + Http_daemon.respond ~body:usage_string + ~headers:["Content-Type", "text/html"] outchan' + | req -> bad_request outchan' in -CicCooking.init(); printf "Proof Checker started and listening on port %d\n" port; flush stdout; -Http.Daemon.start' ~port callback; +CicEnvironment.set_trust (fun _ -> false); +Http_daemon.start' ~port ~mode:`Fork callback ; printf "Proof Checker is terminating, bye!\n"