open Printf;;
-let _ = Helm_registry.load_from "proofChecker.conf.xml";;
+let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";;
-let port =
- try
- Helm_registry.get_int "proofchecker.port"
- with
- Helm_registry.Key_not_found _ -> 48084
-;;
+let port = Helm_registry.get_int "proofchecker.port";;
let (html_preamble, html_postamble) =
((fun uri ->
<title>Proof-Checking %s</title>
</head>
<body bgcolor=\"white\">
-<h1>Proof-Checking %s:</h1>
+<h3>Proof-Checking %s:</h3>
"
uri uri)),
-("<h1>Done.</h1>
+("<h3>Done.</h3>
</body>
</html>
END
let bad_request outchan =
printf "INVALID REQUEST !!!!!\n\n";
flush stdout;
- Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
+ Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
+ outchan;
flush outchan
;;
outchan := outchan' ;
try
let uri = req#param "uri" in
- Http_daemon.send_basic_headers ~code:200 outchan' ;
+ 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;
fprintf outchan' "%s" (html_preamble uri);
flush outchan';
(try
- CicTypeChecker.typecheck (UriManager.uri_of_string uri);
+ ignore (CicTypeChecker.typecheck (UriManager.uri_of_string uri)
+ CicUniv.empty_ugraph);
with e ->
fprintf outchan' "%s\n" (Printexc.to_string e);
flush outchan');
printf "Proof Checker started and listening on port %d\n" port;
flush stdout;
+CicEnvironment.set_trust (fun _ -> false);
Http_daemon.start' ~port ~mode:`Fork callback ;
printf "Proof Checker is terminating, bye!\n"
+