+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
+ 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';
+ (try
+ 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';
+ printf " done\n\n";
+ flush stdout
+ 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'
+
+in
+
+printf "Proof Checker started and listening on port %d\n" port;
+flush stdout;
+CicEnvironment.set_trust (fun _ -> false);
+Http_daemon.start' ~port ~mode:`Fork callback ;
+printf "Proof Checker is terminating, bye!\n"
+