(* Copyright (C) 2002, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* Department, University of Bologna, Italy.
*
* HELM is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* HELM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with HELM; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston,
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
open Printf;;
let default_port = 48084;;
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 (html_preamble, html_postamble) =
((fun uri ->
(sprintf
"
Proof-Checking %s
Proof-Checking %s:
"
uri uri)),
("Done.
END
"))
;;
let bad_request outchan =
printf "INVALID REQUEST !!!!!\n\n";
flush stdout;
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
flush outchan
;;
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 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));
try
let uri = req#param "uri" in
printf "Request to proof-check \"%s\"..." uri;
flush stdout;
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;
printf " done\n\n";
flush stdout
with 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;
Http_daemon.start' ~port callback;
printf "Proof Checker is terminating, bye!\n"