(* 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 _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";;
let port = Helm_registry.get_int "proofchecker.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 ~code:(`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 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);
let d_spec = Http_daemon.daemon_spec ~port ~mode:`Fork ~callback ~auto_close:true () in
Http_daemon.main d_spec;
printf "Proof Checker is terminating, bye!\n"