]> matita.cs.unibo.it Git - helm.git/commitdiff
switched to OCaml HTTP module
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 13 Nov 2002 14:44:19 +0000 (14:44 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 13 Nov 2002 14:44:19 +0000 (14:44 +0000)
helm/proofChecker/Makefile
helm/proofChecker/proofChecker.ml
helm/proofChecker/proofChecker.pl [deleted file]

index 107d5699e4295fe025c1470fe18ace5aab84d55e..aada8a03066a070dc3e32f94cfa50d1f0c7c5f4c 100644 (file)
@@ -1,5 +1,5 @@
 BIN_DIR = /usr/local/bin
-REQUIRES = helm-cic_proof_checking
+REQUIRES = helm-cic_proof_checking http
 PREDICATES =
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g
index b5a2625c26f8d436f2356600e18317134d291c7e..26d8309940539a4c4d37de5fd588ccb88d06b395 100644 (file)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
  * http://cs.unibo.it/helm/.
  *)
 
-let main () =
- let usage_msg =
-  "
-usage: proofChecker[.opt]
-The proof-checker reads from the stdin one URI at a time and proof-checks it.
-
-List of options:"
- in
-  Arg.parse []
-   (fun _ -> 
-     begin
-      prerr_string "Error: no options expected.\n" ;
-      Arg.usage [] usage_msg ;
-      exit (-1)
-     end
-  ) usage_msg ;
+open Printf;;
+
+let default_port = 48084;;
+
+let port =
   try
-   while true do
-    begin
-     try
-      CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
-     with
-        End_of_file -> raise End_of_file
-      | e ->
-       print_newline() ;
-       flush stdout ;
-       raise e
-    end ;
-    print_endline "END"
-   done
+    int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
   with
-   End_of_file -> ()
-;;
+  | Not_found -> default_port
+  | Failure "int_of_string" ->
+      prerr_endline "Warning: invalid port, reverting to default";
+      default_port
+in
+
+let (html_preamble, html_postamble) =
+  ((fun uri ->
+    (sprintf
+"<html>
+<head>
+ <title>Proof-Checking %s</title>
+</head>
+<body bgcolor=\"white\">
+<h1>Proof-Checking %s:</h1>
+"
+      uri uri)),
+("<h1>Done.</h1>
+</body>
+</html>
+END
+"))
+in
+
+let bad_request outchan =
+  printf "INVALID REQUEST !!!!!\n\n";
+  flush stdout;
+  Http.Daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
+  flush outchan
+in
+
+let callback req outchan =
+  match req#path with
+  | "/proofCheck" ->
+      begin
+        Logger.log_callback :=
+          (Logger.log_to_html
+            ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
+        try
+          let uri = req#param "uri" in
+          printf "Request to proof-check \"%s\"..." uri;
+          flush stdout;
+          fprintf outchan "%s" (html_preamble uri);
+          flush outchan;
+          (try
+            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 Not_found -> (* 'uri' argument not found *)
+          bad_request outchan
+      end
+  | req -> bad_request outchan
+
+in
+
+printf "Proof Checker started and listening on port %d\n" port;
+flush stdout;
+Http.Daemon.start' ~port callback;
+printf "Proof Checker is terminating, bye!\n"
 
-Logger.log_callback :=
- (Logger.log_to_html
-   ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-main ();;
diff --git a/helm/proofChecker/proofChecker.pl b/helm/proofChecker/proofChecker.pl
deleted file mode 100755 (executable)
index fde4b43..0000000
+++ /dev/null
@@ -1,70 +0,0 @@
-#!/usr/bin/perl
-
-use HTTP::Daemon;
-use HTTP::Status;
-use HTTP::Response;
-use URI::Escape;
-use CGI;
-use FindBin;
-use IPC::Open3;
-
-chdir $FindBin::Bin; # chdir to the directory of this perl script
-
-my $d = new HTTP::Daemon LocalPort => 8085
- or die "Error: port 8085 not available.";
-print "Please contact me at: <URL:", $d->url, ">\n";
-
-my $IsProofCheckerLiving = 0;
-
-$SIG{CHLD} =
-   sub {
-      print stderr "\nERROR: The proof-checker died.\n";
-      $IsProofCheckerLiving=0;
-   };
-$| = 1;
-
-while(true) {
-   open3(*PC_IN, *PC_OUT, *PC_ERR, "./proofChecker.opt 2>&1");
-   $IsProofCheckerLiving=1;
-   print stderr "\nWARNING: A new proof-checker starts.\n";
-   PC_IN->autoflush(1);
-
-  while (my $c = $d->accept) {
-    my $r = $c->get_request;
-    my $http_query = uri_unescape($r->url->query);
-    my $cgi = new CGI("$http_query");
-    my $uri = $cgi->param('uri');
-
-    if ($r->method eq 'GET' && $r->url->path eq "/proofCheck"){
-       print "Request to proof-check \"$uri\"...";
-       print PC_IN "$uri\n";
-       print $c <<EOT;
-<html>
-<head>
- <title>Proof-Checking $uri</title>
-</head>
-<body bgcolor="white">
-<h1>Proof-Checking $uri:</h1> 
-EOT
-       while(chomp($_ = <PC_OUT>)) {
-         last if ($_ eq "END");
-         print $c $_."\n";
-       }
-       print $c <<EOT;
-<h1>Done.</h1>
-</body>
-</html>
-EOT
-       print " done\n\n";
-    } else {
-        print "INVALID REQUEST \"$http_query\"!!!!!\n\n";
-        $c->send_error(RC_FORBIDDEN);
-    }
-    $c->close;
-    undef($c);
-    last unless $IsProofCheckerLiving;
-  }
-  close(PC_IN);
-  close(PC_OUT);
-  close(PC_ERR);
-}