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 ->
<title>Proof-Checking %s</title>
</head>
<body bgcolor=\"white\">
-<h1>Proof-Checking %s:</h1>
+<h3>Proof-Checking %s:</h3>
"
uri uri)),
-("<h1>Done.</h1>
+("<h3>Done.</h3>
</body>
</html>
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 =
+"
+<html>
+ <head>
+ <title>ProofChecker's help message</title>
+ </head>
+ <body>
+ <h1>ProofChecker</h1>
+ <h2>Usage</h2>
+ <p>
+ Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
+ </p>
+ <p>
+ Available commands:
+ </p>
+ <p>
+ <b><kbd>help</kbd></b><br />
+ display this help message
+ </p>
+ <p>
+ <b><kbd>proofCheck?uri=uri</kbd></b><br />
+ proof-checks the object whose URI is specified by <em>uri</em>
+ </p>
+ </body>
+</html>
+"
+;;
+
+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)
+ CicUniv.empty_ugraph);
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"