From d8ae533d041cb600993ab2957111c105b6ded21d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 15 Jun 2011 12:49:01 +0000 Subject: [PATCH] Multi-user Matita (and Matitaweb): added user authentication (currently only tested on hard-coded accounts). Proof-objects are saved in a user-specific directory. --- matitaB/matita/Makefile | 11 +- matitaB/matita/login.html | 27 +++ matitaB/matita/matitaAuthentication.ml | 26 ++- matitaB/matita/matitaAuthentication.mli | 10 +- matitaB/matita/matitaEngine.ml | 15 +- matitaB/matita/matitadaemon.ml | 261 ++++++++++++++++-------- matitaB/matita/matitaweb.js | 47 +++-- matitaB/matita/netplex.conf | 7 + 8 files changed, 286 insertions(+), 118 deletions(-) create mode 100644 matitaB/matita/login.html diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index 3634caf65..a9018f16f 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -60,6 +60,15 @@ CMLI = \ matitaExcPp.mli \ matitaInit.mli \ $(NULL) +WMLI = \ + matitaTypes.mli \ + matitaMisc.mli \ + applyTransformation.mli \ + matitaEngine.mli \ + matitaExcPp.mli \ + matitaInit.mli \ + matitaAuthentication.mli \ + $(NULL) MAINCMLI = \ matitaclean.mli \ $(NULL) @@ -67,7 +76,7 @@ MAINCMLI = \ ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) # objects for matitac (batch compiler) CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) -WML = matitaAuthentication.ml $(CML) +WML = buildTimeConf.ml $(WMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ diff --git a/matitaB/matita/login.html b/matitaB/matita/login.html new file mode 100644 index 000000000..631bece70 --- /dev/null +++ b/matitaB/matita/login.html @@ -0,0 +1,27 @@ + + + + + + + + + + + + + diff --git a/matitaB/matita/matitaAuthentication.ml b/matitaB/matita/matitaAuthentication.ml index 06e7d9451..1b9a91b71 100644 --- a/matitaB/matita/matitaAuthentication.ml +++ b/matitaB/matita/matitaAuthentication.ml @@ -31,7 +31,7 @@ type user = string * (string * session_id option) let user_tbl = (ref [] : user list ref) (* session table: (user id, session id), matita status *) -type session = (string * session_id) * MatitaEngine.status +type session = session_id * (MatitaEngine.status * MatitaEngine.status list) let session_tbl = (ref [] : session list ref) @@ -39,24 +39,40 @@ exception UsernameCollision of string let lookup_user uid = List.assoc uid !user_tbl -let create_session uid status = +let create_session uid = + let status = new MatitaEngine.status (Some uid) "cic:/matita" in + let history = [status] in let pw,sid = List.assoc uid !user_tbl in let clean_utbl = List.remove_assoc uid !user_tbl in let new_session = Uuidm.create `V4 in user_tbl := (uid,(pw,Some new_session))::clean_utbl; let clean_stbl = match sid with | Some sid' -> - List.remove_assoc (uid,sid') !session_tbl + List.remove_assoc sid' !session_tbl | _ -> !session_tbl - in session_tbl := ((uid,new_session),status)::clean_stbl + in + session_tbl := (new_session,(status,history))::clean_stbl; + new_session ;; +let get_status sid = fst (List.assoc sid !session_tbl) + +let get_history sid = snd (List.assoc sid !session_tbl) + +let set_status sid st = + let oldst, hist = List.assoc sid !session_tbl in + session_tbl := (sid,(st,hist))::(List.remove_assoc sid !session_tbl) + +let set_history sid hist = + let st, oldhist = List.assoc sid !session_tbl in + session_tbl := (sid,(st,hist))::(List.remove_assoc sid !session_tbl) + let logout_user uid = match List.assoc uid !user_tbl with | _,None -> () | pw, Some sid -> user_tbl := (uid,(pw,None))::List.remove_assoc uid !user_tbl; - session_tbl := List.remove_assoc (uid,sid) !session_tbl + session_tbl := List.remove_assoc sid !session_tbl ;; let remove_user uid = diff --git a/matitaB/matita/matitaAuthentication.mli b/matitaB/matita/matitaAuthentication.mli index ffbb206b7..c1c2cf489 100644 --- a/matitaB/matita/matitaAuthentication.mli +++ b/matitaB/matita/matitaAuthentication.mli @@ -29,7 +29,15 @@ exception UsernameCollision of string val lookup_user : string -> (string * session_id option) -val create_session : string -> MatitaEngine.status -> unit +val create_session : string -> session_id + +val get_status : session_id -> MatitaEngine.status + +val get_history : session_id -> MatitaEngine.status list + +val set_status : session_id -> MatitaEngine.status -> unit + +val set_history : session_id -> MatitaEngine.status list -> unit val logout_user : string -> unit diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 9c86679bc..aa271b2a1 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -140,7 +140,7 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm = let already_included = NCicLibrary.get_transitively_included status in let asserted,_ = assert_ng ~already_included ~compiling ~asserted ~include_paths - mafilename + ?uid:status#user mafilename in asserted,cmd | cmd -> asserted,cmd @@ -168,7 +168,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status in loop asserted status -and compile ~compiling ~asserted ~include_paths ~outch fname = +and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = if List.mem fname compiling then raise (CircularDependency fname); let compiling = fname::compiling in let matita_debug = Helm_registry.get_bool "matita.debug" in @@ -178,7 +178,7 @@ and compile ~compiling ~asserted ~include_paths ~outch fname = activate_extraction baseuri fname ; (* MATITA 1.0: debbo fare time_travel sulla ng_library? *) (* FIXME: currently hardcoded to single user mode *) - let status = new status None baseuri in + let status = new status uid baseuri in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = Unix.times () @@ -263,6 +263,9 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid let baseuri = NUri.uri_of_string baseuri in let ngtime_of baseuri = let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in + let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in + prerr_endline ("uid = " ^ uid); + prerr_endline ("ngpath = " ^ ngpath); try Some (Unix.stat ngpath).Unix.st_mtime with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in @@ -280,7 +283,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid (fun (asserted,b) mapath -> let asserted,b1 = assert_ng ~already_included ~compiling ~asserted ~include_paths - mapath + ?uid mapath in asserted, b || b1 || let _,baseuri,_,_ = @@ -294,6 +297,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid asserted, children_bad || matime > ngtime | None -> asserted,true in + prerr_endline ("asserted = " ^ (String.concat "," asserted)); if not to_be_compiled then fullmapath::asserted,false else if List.mem baseuri already_included then @@ -305,7 +309,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid | None -> open_out (fullmapath ^ ".mad"), true | Some c -> c, false in - let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in + prerr_endline ("compiling " ^ fullmapath); + let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in if is_file_ch then close_out outch; fullmapath::asserted,true end diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 8dbfa4511..664a7301c 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -47,9 +47,6 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) utf8_length parsed_text -(* FIXME: currently hard coded to single user mode *) -let status = ref (new MatitaEngine.status (Some "ricciott") "cic:/matita");; -let history = ref [!status];; let sequent_size = ref 40;; let include_paths = ref [];; @@ -164,115 +161,191 @@ let load_doc filename outchan = let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi 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; - status := (!status)#set_baseuri baseuri; - cgi#out_channel#output_string body; + 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 + | 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 text = +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) + eval_statement !include_paths (*buffer*) status (`Raw text) (* with End_of_file -> raise Margin *) in - status := st; - history := st :: !history; - prerr_endline ("after advance0 history.length = " ^ string_of_int (List.length !history)); - parsed_len, new_unparsed + MatitaAuthentication.set_status sid st; + MatitaAuthentication.set_history sid (st::history); + parsed_len, new_unparsed, st +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 + + prerr_endline "1"; + assert (cgi#arguments <> []); + let uid = cgi#argument_value "userid" in + let userpw = cgi#argument_value "password" in + prerr_endline ("2: user = " ^ uid); + let pw,_ = MatitaAuthentication.lookup_user uid in + prerr_endline "3"; + + if pw = userpw then + begin + prerr_endline "4"; + let sid = MatitaAuthentication.create_session uid in + let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in + cgi#set_header ~status:`See_other ~cache:`No_cache ~set_cookies:[cookie] (); + env#set_output_header_field "Location" "/index.html" + end + else + begin + 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() + +;; + (* 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 - 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 = advance0 text in - let txt = output_status !status in - let body = - "" ^ txt - ^ "" - in - prerr_endline ("sending advance response:\n" ^ body); - cgi#out_channel#output_string body; + 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 gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = - let rec aux parsed_len text = - try - prerr_endline ("evaluating: " ^ first_line text); - let plen,new_unparsed = advance0 text in - aux (parsed_len+plen) new_unparsed - with - | _ -> parsed_len - in let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi 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 txt = output_status !status in - let body = - "" ^ txt - ^ "" - in - prerr_endline ("sending goto bottom response:\n" ^ body); - cgi#out_channel#output_string body; + 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 - cgi # set_header - ~cache:`No_cache - ~content_type:"text/xml; charset=\"utf-8\"" - (); - 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; - history := new_history; - status := new_status; - prerr_endline ("after retract history.length = " ^ string_of_int (List.length !history)); - let body = output_status !status in - cgi#out_channel#output_string body; + 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() ;; @@ -340,13 +413,21 @@ let start() = 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 nethttpd_factory = Nethttpd_plex.nethttpd_factory ~handlers:[ "advance", do_advance ; "retract", do_retract ; "bottom", goto_bottom - ; "open", retrieve ] + ; "open", retrieve + ; "login", do_login ] () in MatitaInit.initialize_all (); (* test begin *) diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 8f77fe4f8..0c661623b 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -15,22 +15,26 @@ var metasenv = ""; function initialize() { - locked = document.getElementById("locked"); - unlocked = document.getElementById("unlocked"); - workarea = document.getElementById("workarea"); - scriptcell = document.getElementById("scriptcell"); - goalcell = document.getElementById("goalcell"); - goals = document.getElementById("goals"); - goalview = document.getElementById("goalview"); - filename = document.getElementById("filename"); - logarea = document.getElementById("logarea"); - advanceButton = document.getElementById("advance"); - retractButton = document.getElementById("retract"); - cursorButton = document.getElementById("cursor"); - bottomButton = document.getElementById("bottom"); - - // hide sequent view at start - hideSequent(); + if (readCookie("session") == null) { + window.location = "/login.html" + } else { + locked = document.getElementById("locked"); + unlocked = document.getElementById("unlocked"); + workarea = document.getElementById("workarea"); + scriptcell = document.getElementById("scriptcell"); + goalcell = document.getElementById("goalcell"); + goals = document.getElementById("goals"); + goalview = document.getElementById("goalview"); + filename = document.getElementById("filename"); + logarea = document.getElementById("logarea"); + advanceButton = document.getElementById("advance"); + retractButton = document.getElementById("retract"); + cursorButton = document.getElementById("cursor"); + bottomButton = document.getElementById("bottom"); + + // hide sequent view at start + hideSequent(); + } } function debug(txt) @@ -499,3 +503,14 @@ function findNode(list, node, acc) { function test () { debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos())); } + +function readCookie(name) { + var nameEQ = name + "="; + var ca = document.cookie.split(';'); + for(var i=0;i < ca.length;i++) { + var c = ca[i]; + while (c.charAt(0)==' ') c = c.substring(1,c.length); + if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length); + } + return null; +} diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf index d7d403be9..a42f4c359 100644 --- a/matitaB/matita/netplex.conf +++ b/matitaB/matita/netplex.conf @@ -60,6 +60,13 @@ netplex { handler = "bottom"; } }; + uri { + path = "/login"; + service { + type = "dynamic"; + handler = "login"; + } + }; }; }; workload_manager { -- 2.39.2

User id:
Password: