Ported to Http_registry and to HelmLogger.

diff --git a/helm/proofChecker/Makefile b/helm/proofChecker/Makefile
index aada8a03066a070dc3e32f94cfa50d1f0c7c5f4c..af48d0a5d1e941ec7d45a6831a6192fdb5be17c4 100644 (file)
--- a/helm/proofChecker/Makefile
+++ b/helm/proofChecker/Makefile
@@ -1,7 +1,7 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = helm-cic_proof_checking http
 PREDICATES =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g
 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
 OCAMLDEP = ocamldep

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 5529baa71e06b5ebbb9d73a439009ccd0b6dfabe..13704366084762d0a26750cd4db1a8a90d118b9f 100644 (file)
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -25,16 +25,13 @@
 
 open Printf;;
 
-let default_port = 48084;;
+let _ = Helm_registry.load_from "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
+ try
+  Helm_registry.get_int "proofchecker.port"
+ with
+  Helm_registry.Key_not_found _ -> 48084
 ;;
 
 let (html_preamble, html_postamble) =
@@ -90,39 +87,49 @@ 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
-        CicLogger.log_callback :=
-          (CicLogger.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: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);
            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;
+Http_daemon.start' ~port ~mode:`Fork callback ;
 printf "Proof Checker is terminating, bye!\n"