1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let default_port = 48084;;
32 int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
34 | Not_found -> default_port
35 | Failure "int_of_string" ->
36 prerr_endline "Warning: invalid port, reverting to default";
40 let (html_preamble, html_postamble) =
45 <title>Proof-Checking %s</title>
47 <body bgcolor=\"white\">
48 <h1>Proof-Checking %s:</h1>
58 let bad_request outchan =
59 printf "INVALID REQUEST !!!!!\n\n";
61 Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
65 let callback req outchan =
69 Logger.log_callback :=
71 ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
73 let uri = req#param "uri" in
74 printf "Request to proof-check \"%s\"..." uri;
76 fprintf outchan "%s" (html_preamble uri);
79 CicTypeChecker.typecheck (UriManager.uri_of_string uri);
81 fprintf outchan "%s\n" (Printexc.to_string e);
83 fprintf outchan "%s" html_postamble;
87 with Not_found -> (* 'uri' argument not found *)
90 | req -> bad_request outchan
95 printf "Proof Checker started and listening on port %d\n" port;
97 Http_daemon.start' ~port callback;
98 printf "Proof Checker is terminating, bye!\n"