(* 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"