X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=744034e060ba1c7c7f4c638584cbd865448a4861;hb=08935b4293e1c78bbe2ac4b972dbe47023160919;hp=b8b3a1eb2111882740d602f527704714ee34c2e7;hpb=519eb28019e44a404bf62dbc5ff07ddd39556b17;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index b8b3a1eb2..744034e06 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -1,6 +1,18 @@ open Printf;; open Http_types;; +module Stack = Continuationals.Stack + +let rt_path () = Helm_registry.get "matita.rt_base_dir" + +let utf8_length = Netconversion.ustring_length `Enc_utf8 + +let utf8_parsed_text s floc = + let start, stop = HExtlib.loc_of_floc floc in + let len = stop - start in + let res = Netconversion.ustring_sub `Enc_utf8 start len s in + res, String.length res + (*** from matitaScript.ml ***) (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *) @@ -23,35 +35,80 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script | GrafiteAst.Comment (loc, _) -> loc in let _,lend = HExtlib.loc_of_floc floc in - let parsed_text, parsed_text_len = - MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + let parsed_text, _parsed_text_len = + utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + let byte_parsed_text_len = String.length parsed_text in + let unparsed_txt' = + String.sub unparsed_text byte_parsed_text_len + (String.length unparsed_text - byte_parsed_text_len) + in let status = MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) in - (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text - - -let status = ref (new MatitaEngine.status "cic:/matita");; -let history = ref [!status];; + (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) + utf8_length parsed_text -let include_paths = ["/home/barolo/matitaB/matita/lib"];; +let sequent_size = ref 40;; -(* lista [meta n., goal; meta n., goal; ... ] *) -(* "item1#item2#...#" *) +let include_paths = ref [];; +(* + * + * ... + * ... + * + * + * ... + * *) let output_status s = let _,_,metasenv,subst,_ = s#obj in - List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta) - in - (*let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt0 in*) - prerr_endline ("prima dell'encoding: BEGIN\n" ^ txt0 ^ "\nEND"); - let txt0 = Netencoding.Url.encode ~plus:false txt0 in - (string_of_int nmeta) ^ "|" ^ txt0 ^ "#" ^ acc) - "" metasenv + let render_switch = function + | Stack.Open i -> "?" ^ (string_of_int i) + | Stack.Closed i -> "?" ^ (string_of_int i) ^ "" + in + let int_of_switch = function + | Stack.Open i | Stack.Closed i -> i + in + let sequent = function + | Stack.Open i -> + let meta = List.assoc i metasenv in + snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta)) + | Stack.Closed _ -> "This goal has already been closed." + in + let render_sequent is_loc acc depth tag (pos,sw) = + let metano = int_of_switch sw in + let markup = + if is_loc then + (match depth, pos with + | 0, 0 -> "" ^ (render_switch sw) ^ "" + | 0, _ -> + Printf.sprintf "|%d: %s" pos (render_switch sw) + | 1, pos when Stack.head_tag s#stack = `BranchTag -> + Printf.sprintf "|%d : %s" pos (render_switch sw) + | _ -> render_switch sw) + else render_switch sw + in + prerr_endline "pippo1"; + let markup = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in + let markup = "" ^ markup ^ "" in + prerr_endline "pippo2"; + let sequent = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) + in + let txt0 = "" ^ sequent ^ "" in + "" ^ markup ^ + txt0 ^ "" ^ acc + in + let res = "" ^ + (Stack.fold + ~env:(render_sequent true) ~cont:(render_sequent false) + ~todo:(render_sequent false) "" s#stack) ^ + "" + in + prerr_endline ("sending metasenv:\n" ^ res); res ;; (* let html_of_status s = @@ -68,29 +125,14 @@ let output_status s = String.concat "\n\n" txt ;; *) -let advance text (* (?bos=false) *) = - let (st,new_statements),(* newtext TODO *) _,parsed_len = - (* try *) - eval_statement include_paths (*buffer*) !status (`Raw text) - (* with End_of_file -> raise Margin *) - in - status := st; - history := st :: !history; - let txt = output_status !status in - parsed_len, txt -;; +let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; -let retract () = - let new_history,new_status = - match !history with - _::(status::_ as history) -> - history, status - | [_] -> failwith "retract" - | _ -> assert false in - NCicLibrary.time_travel !status; - history := new_history; - status := new_status; - output_status !status +let first_line s = + let s = Pcre.replace ~rex:heading_nl_RE s in + try + let nl_pos = String.index s '\n' in + String.sub s 0 nl_pos + with Not_found -> s ;; let read_file fname = @@ -101,7 +143,7 @@ let read_file fname = lines := input_line chan :: !lines done; with End_of_file -> close_in chan); - String.concat "\r\n" (List.rev !lines) + String.concat "\n" (List.rev !lines) ;; let load_index outchan = @@ -109,102 +151,362 @@ let load_index outchan = Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan ;; -let call_service outchan = - try - (ignore(MatitaEngine.assert_ng - ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *) - "/home/barolo/matitaB/matita/lib/basics/pts.ma"); - prerr_endline "fatto"; - let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad" - in - Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan - ) +let load_doc filename outchan = + let s = read_file filename in + let is_png = + try String.sub filename (String.length filename - 4) 4 = ".png" + with Invalid_argument _ -> false + in + let contenttype = if is_png then "image/png" else "text/html" in + Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan +;; + +let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let filename = cgi # argument_value "file" in + prerr_endline ("reading file " ^ filename); + let body = + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (read_file filename) in + prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); + let body = "" ^ body ^ "" in + let baseuri, incpaths = + try + let root, baseuri, _fname, _tgt = + Librarian.baseuri_of_script ~include_paths:[] filename in + let includes = + try + Str.split (Str.regexp " ") + (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + with Not_found -> [] + in + let rc = root :: includes in + List.iter (HLog.debug) rc; baseuri, rc + with + Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in + include_paths := incpaths; + let status = MatitaAuthentication.get_status sid in + MatitaAuthentication.set_status sid (status#set_baseuri baseuri); + cgi#out_channel#output_string body; with - e -> Http_daemon.respond ~code:(`Code 500) outchan + | Not_found _ -> + cgi # set_header + ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + ()); + cgi#out_channel#commit_work() ;; +let advance0 sid text = + let status = MatitaAuthentication.get_status sid in + let history = MatitaAuthentication.get_history sid in + let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = + (* try *) + eval_statement !include_paths (*buffer*) status (`Raw text) + (* with End_of_file -> raise Margin *) + in + MatitaAuthentication.set_status sid st; + MatitaAuthentication.set_history sid (st::history); + parsed_len, new_unparsed, st -let callback req outchan = - let str = - (sprintf "request path = %s\n" req#path) ^ - (sprintf "request GET params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^ - (sprintf "request POST params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^ - (sprintf "request ALL params = %s\n" - (String.concat ";" - (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^ - (sprintf "cookies = %s\n" - (match req#cookies with - | None -> - "NO COOKIES " - ^ (if req#hasHeader ~name:"cookie" - then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')" - else "(No 'Cookie:' header received)") - | Some cookies -> - (String.concat ";" - (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^ - (sprintf "request BODY = '%s'\n\n" req#body) - in - (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *) - - prerr_endline str; - - match req#path with - | "/" -> load_index outchan - | "/matita" -> call_service outchan - | "/open" -> - prerr_endline "getting 'file' argument"; - let filename = List.assoc "file" req#params_GET in - prerr_endline ("reading file " ^ filename); - let body = read_file filename in - let _,baseuri,_,_ = - Librarian.baseuri_of_script ~include_paths:[] filename - in - status := (!status)#set_baseuri baseuri; - Http_daemon.respond ~code:(`Code 200) ~body outchan - | "/advance" -> - let script = req#body in - prerr_endline ("body length = " ^ (string_of_int (String.length script))); - let (parsed_len,txt), res, code = - try advance script, "OK", `Code 200 - with - | HExtlib.Localized(_,e) - | e -> - (prerr_endline ("exception: " ^ Printexc.to_string e); - (try - NTacStatus.pp_tac_status !status - with e -> prerr_endline ("inner exception: " ^ - Printexc.to_string e)); - prerr_endline "end status"; - let txt = output_status !status in - (0,txt), Printexc.to_string e, `Code 500) - in - prerr_endline ("server response:\n" ^ txt); - let body = (string_of_int parsed_len) ^ "@" ^ txt in - Http_daemon.respond ~code ~body outchan - | "/retract" -> - (try - let body = retract () in - Http_daemon.respond ~code:(`Code 200) ~body outchan - with e -> - (prerr_endline (Printexc.to_string e); - Http_daemon.respond ~code:(`Code 500) outchan)) - | url -> Http_daemon.respond_not_found ~url outchan +let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + + assert (cgi#arguments <> []); + let uid = cgi#argument_value "userid" in + let userpw = cgi#argument_value "password" in + (try + MatitaAuthentication.add_user uid userpw; + env#set_output_header_field "Location" "/index.html" + with + | MatitaAuthentication.UsernameCollision _ -> + cgi#set_header + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "Error: User id collision!" + | MatitaFilesystem.SvnError msg -> + cgi#set_header + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + ("

Error: Svn checkout failed!

")); + cgi#out_channel#commit_work() +;; +let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + + assert (cgi#arguments <> []); + let uid = cgi#argument_value "userid" in + let userpw = cgi#argument_value "password" in + let pw,_ = MatitaAuthentication.lookup_user uid in + + if pw = userpw then + begin + let _ = MatitaFilesystem.html_of_library uid in + let sid = MatitaAuthentication.create_session uid in + (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in + cgi#set_header ~set_cookies:[cookie] (); *) + env#set_output_header_field + "Set-Cookie" ("session=" ^ (Uuidm.to_string sid)); + env#set_output_header_field "Location" "/index.html" + end + else + begin + prerr_endline ("ERROR: received " ^ userpw ^ "but the password is " ^ pw); + cgi#set_header + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "Authentication error" + end; + + cgi#out_channel#commit_work() + ;; -let spec = - { Http_daemon.default_spec with - callback = callback; - port = 9999; - mode = `Single; - } +let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + MatitaAuthentication.logout_user sid; + cgi # set_header + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + (); + let text = read_file (rt_path () ^ "/logout.html") in + cgi#out_channel#output_string text + with + | Not_found _ -> + cgi # set_header + ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + ()); + cgi#out_channel#commit_work() +;; + +(* returns the length of the executed text and an html representation of the + * current metasenv*) +let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let text = cgi#argument_value "body" in + prerr_endline ("body =\n" ^ text); + let parsed_len, new_unparsed, new_status = advance0 sid text in + let txt = output_status new_status in + let body = + "" ^ txt + ^ "" + in + prerr_endline ("sending advance response:\n" ^ body); + cgi#out_channel#output_string body + with + | Not_found _ -> + cgi # set_header + ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + ()); + cgi#out_channel#commit_work() ;; -let _ = +let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + + let rec aux parsed_len text = + try + prerr_endline ("evaluating: " ^ first_line text); + let plen,new_unparsed,_new_status = advance0 sid text in + aux (parsed_len+plen) new_unparsed + with + | _ -> parsed_len + in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let text = cgi#argument_value "body" in + prerr_endline ("body =\n" ^ text); + let parsed_len = aux 0 text in + let status = MatitaAuthentication.get_status sid in + let txt = output_status status in + let body = + "" ^ txt + ^ "" + in + prerr_endline ("sending goto bottom response:\n" ^ body); + cgi#out_channel#output_string body + with Not_found -> cgi#set_header ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" ()); + cgi#out_channel#commit_work() +;; + +let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + let history = MatitaAuthentication.get_history sid in + let new_history,new_status = + match history with + _::(status::_ as history) -> + history, status + | [_] -> (prerr_endline "singleton";failwith "retract") + | _ -> (prerr_endline "nil"; assert false) in + NCicLibrary.time_travel new_status; + MatitaAuthentication.set_history sid new_history; + MatitaAuthentication.set_status sid new_status; + prerr_endline ("after retract history.length = " ^ + string_of_int (List.length new_history)); + let body = output_status new_status in + cgi#out_channel#output_string body + with _ -> cgi#set_header ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" ()); + cgi#out_channel#commit_work() +;; + + +open Netcgi1_compat.Netcgi_types;; + +(**********************************************************************) +(* Create the webserver *) +(**********************************************************************) + + +let start() = + let (opt_list, cmdline_cfg) = Netplex_main.args() in + + let use_mt = ref true in + + let opt_list' = + [ "-mt", Arg.Set use_mt, + " Use multi-threading instead of multi-processing" + ] @ opt_list in + + Arg.parse + opt_list' + (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s))) + "usage: netplex [options]"; + let parallelizer = + if !use_mt then + Netplex_mt.mt() (* multi-threading *) + else + Netplex_mp.mp() in (* multi-processing *) +(* + let adder = + { Nethttpd_services.dyn_handler = (fun _ -> process1); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in +*) + let do_advance = + { Nethttpd_services.dyn_handler = (fun _ -> advance); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let do_retract = + { Nethttpd_services.dyn_handler = (fun _ -> retract); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let goto_bottom = + { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let retrieve = + { Nethttpd_services.dyn_handler = (fun _ -> retrieve); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let do_register = + { Nethttpd_services.dyn_handler = (fun _ -> register); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let do_login = + { Nethttpd_services.dyn_handler = (fun _ -> login); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + let do_logout = + { Nethttpd_services.dyn_handler = (fun _ -> logout); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in + + let nethttpd_factory = + Nethttpd_plex.nethttpd_factory + ~handlers:[ "advance", do_advance + ; "retract", do_retract + ; "bottom", goto_bottom + ; "open", retrieve + ; "register", do_register + ; "login", do_login + ; "logout", do_logout ] + () in MatitaInit.initialize_all (); - Http_daemon.main spec + MatitaAuthentication.deserialize (); + Netplex_main.startup + parallelizer + Netplex_log.logger_factories (* allow all built-in logging styles *) + Netplex_workload.workload_manager_factories (* ... all ways of workload management *) + [ nethttpd_factory ] (* make this nethttpd available *) + cmdline_cfg ;; + +Sys.set_signal Sys.sigpipe Sys.Signal_ignore; +start();;