X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=e4f00fe3acf86c989b4e250af89000fda4942206;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hpb=37adb260bc671a4615e2b3fa9fb1ae44999747d0;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 7c9c0f150..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 -;; +let port = Helm_registry.get_int "proofchecker.port";; let (html_preamble, html_postamble) = ((fun uri -> @@ -45,10 +37,10 @@ let (html_preamble, html_postamble) = Proof-Checking %s -

Proof-Checking %s:

+

Proof-Checking %s:

" uri uri)), -("

Done.

+("

Done.

END @@ -58,7 +50,8 @@ END 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 ;; @@ -90,39 +83,51 @@ let usage_string = " ;; -let callback (req : Http_types.request) outchan = +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 : 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 | "/help" -> Http_daemon.respond ~body:usage_string - ~headers:["Content-Type", "text/html"] outchan - | req -> bad_request outchan + ~headers:["Content-Type", "text/html"] outchan' + | req -> bad_request outchan' in 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" +