]> matita.cs.unibo.it Git - helm.git/blob - daemons/proofChecker/proofChecker.ml
Bug fixed: the script Menu was not locked as expected.
[helm.git] / daemons / proofChecker / proofChecker.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 open Printf;;
27
28 let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";;
29
30 let port = Helm_registry.get_int "proofchecker.port";;
31
32 let (html_preamble, html_postamble) =
33   ((fun uri ->
34     (sprintf
35 "<html>
36 <head>
37  <title>Proof-Checking %s</title>
38 </head>
39 <body bgcolor=\"white\">
40 <h3>Proof-Checking %s:</h3>
41 "
42       uri uri)),
43 ("<h3>Done.</h3>
44 </body>
45 </html>
46 END
47 "))
48 ;;
49
50 let bad_request outchan =
51   printf "INVALID REQUEST !!!!!\n\n";
52   flush stdout;
53   Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
54     outchan;
55   flush outchan
56 ;;
57
58 let usage_string =
59 "
60 <html>
61   <head>
62     <title>ProofChecker's help message</title>
63   </head>
64   <body>
65     <h1>ProofChecker</h1>
66     <h2>Usage</h2>
67     <p>
68     Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
69     </p>
70     <p>
71     Available commands:
72     </p>
73     <p>
74       <b><kbd>help</kbd></b><br />
75       display this help message
76     </p>
77     <p>
78       <b><kbd>proofCheck?uri=uri</kbd></b><br />
79       proof-checks the object whose URI is specified by <em>uri</em>
80     </p>
81   </body>
82 </html>
83 "
84 ;;
85
86 let outchan = ref stderr;;
87
88 let _ =
89  HelmLogger.register_log_callback
90   (fun ?append_NL msg ->
91     output_string !outchan (HelmLogger.html_of_html_msg msg) ;
92     flush !outchan)
93 ;;
94
95 let callback (req : Http_types.request) outchan' =
96   match req#path with
97   | "/proofCheck" ->
98       begin
99         outchan := outchan' ;
100         try
101           let uri = req#param "uri" in
102           Http_daemon.send_basic_headers ~code:(`Code 200) outchan' ;
103           Http_daemon.send_header "Content-type" "text/html" outchan' ; 
104           Http_daemon.send_CRLF outchan' ;
105           printf "Request to proof-check \"%s\"..." uri;
106           flush stdout;
107           fprintf outchan' "%s" (html_preamble uri);
108           flush outchan';
109           (try
110             ignore (CicTypeChecker.typecheck (UriManager.uri_of_string uri));
111            with e ->
112             fprintf outchan' "%s\n" (Printexc.to_string e);
113             flush outchan');
114           fprintf outchan' "%s" html_postamble;
115           flush outchan';
116           printf " done\n\n";
117           flush stdout
118         with Http_types.Param_not_found _ -> (* 'uri' argument not found *)
119           bad_request outchan'
120       end
121   | "/help" ->
122       Http_daemon.respond ~body:usage_string
123        ~headers:["Content-Type", "text/html"] outchan'
124   | req -> bad_request outchan'
125
126 in
127
128
129 printf "Proof Checker started and listening on port %d\n" port;
130 flush stdout;
131 CicEnvironment.set_trust (fun _ -> false);
132 let d_spec = Http_daemon.daemon_spec ~port ~mode:`Fork ~callback ~auto_close:true () in
133 Http_daemon.main d_spec;
134 printf "Proof Checker is terminating, bye!\n"
135