(* Copyright (C) 2004-2011, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) exception SvnError of string;; (* disable for debugging *) let prerr_endline _ = () let exec_process cmd = let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in let outlines = ref [] in let errlines = ref [] in (try while true do outlines := input_line stdout :: !outlines; done; assert false with End_of_file -> (try while true do errlines := input_line stderr :: !errlines; done; assert false with End_of_file -> match (Unix.close_process_full chs) with | Unix.WEXITED errno -> errno, !outlines, !errlines | _ -> assert false)) let string_of_output outlines errlines = let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in output ^ "\n\n" ^ errors type svn_flag = | Add | Conflict | Modified | NotAdded | Delete | Update | Merge type matita_flag = | MUnversioned | MSynchronized | MAdd | MModified | MConflict let string_of_matita_flag = function | MUnversioned -> "unversioned" | MSynchronized -> "synchronized" | MAdd -> "new" | MModified -> "modified" | MConflict -> "conflict!" exception SvnAnomaly of string let stat_classify line uid = let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in let rec aux n acc = match (line.[n], n) with | _, n when n = 7 -> let fn = String.sub line 8 ((String.length line) - 8) in let prefix_len = String.length basedir in let fn_len = String.length fn in if String.sub fn 0 prefix_len = basedir then String.sub fn prefix_len (fn_len - prefix_len), acc else fn, acc | ' ', _ -> aux (n+1) acc | 'A',0 -> aux (n+1) (Add::acc) | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc) (* | 'D',0 -> aux (n+1) (Delete::acc) *) (* | 'I',0 -> aux (n+1) (Ignore::acc) *) | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc) (* | 'R',0 -> aux (n+1) (Replaced::acc) *) (* | 'X',0 -> aux (n+1) (UnversionedDir::acc) *) | '?',0 -> aux (n+1) (NotAdded::acc) (* | '!',0 -> aux (n+1) (Missing::acc) *) (* | '~',0 -> aux (n+1) (Obstructed::acc) *) (* | 'L',2 -> aux (n+1) (Lock::acc) *) (* | '+',3 -> aux (n+1) (History::acc) *) (* | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *) (* | 'X',4 -> aux (n+1) (External::acc) *) (* | 'K',5 -> aux (n+1) (LockToken::acc) *) (* | 'C',6 -> aux (n+1) (TreeConflict::acc) *) | _ -> raise (SvnAnomaly line) in aux 0 [] let count p l = List.length (List.filter p l) exception Unimplemented let matita_flag_of_stat fs = if List.mem Conflict fs then MConflict else if List.mem Modified fs then MModified else if List.mem Add fs then MAdd else if List.mem Delete fs then raise Unimplemented else if List.mem NotAdded fs then MUnversioned else MSynchronized let stat_user user = let rt_dir = Helm_registry.get "matita.rt_base_dir" in let _repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = exec_process ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/") in let files, anomalies = List.fold_left (fun (facc,eacc) line -> try (stat_classify line user::facc), eacc with | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines in let files = List.map (fun (fname,flags) -> fname,Some (matita_flag_of_stat flags)) files in if errno = 0 then files, anomalies else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines))) ;; (* update and checkout *) let up_classify line uid = let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in let rec aux n acc = match (line.[n], n) with | _, n when n = 4 -> let fn = String.sub line 5 ((String.length line) - 5) in let prefix_len = String.length basedir in let fn_len = String.length fn in if String.sub fn 0 prefix_len = basedir then String.sub fn prefix_len (fn_len - prefix_len), acc else fn, acc | ' ', _ -> aux (n+1) acc | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc) | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc) | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc) | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc) | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc) (* | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *) | _ -> raise (SvnAnomaly line) in aux 0 [] let matita_flag_of_update fs = if List.mem Conflict fs then Some MConflict else if List.mem Delete fs then None else if List.mem Merge fs then Some MModified else Some MSynchronized (* this should be executed only for a freshly created user so no CS is needed *) let checkout user = let rt_dir = Helm_registry.get "matita.rt_base_dir" in let repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = prerr_endline ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/"); exec_process ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/") in let files, anomalies = List.fold_left (fun (facc,eacc) line -> try (up_classify line user::facc), eacc with | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines in if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files else raise (SvnError (string_of_output outlines errlines)) (* normalize qualified file name *) let normalize_qfn p = (* trim leading "./" *) let p = try if String.sub p 0 2 <> "./" then p else String.sub p 2 (String.length p - 2) with | Invalid_argument _ -> p in (* trim trailing "/" *) try if String.sub p (String.length p - 1) 1 <> "/" then p else String.sub p 0 (String.length p - 1) with | Invalid_argument _ -> p let html_of_library uid ft = let i = ref 0 in let newid () = incr i; ("node" ^ string_of_int !i) in let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in let branch lpath children = let id = newid () in let name = Filename.basename lpath in let name = if name <> "." then name else "cic:/matita" in let flag = try List.assoc lpath ft with Not_found -> MSynchronized in let szflag = string_of_matita_flag flag in "\n" ^ "\n" ^ name ^ " " ^ szflag ^ "
\n" ^ "\n" ^ children ^ "\n" in let leaf lpath = let flag = try List.assoc lpath ft with Not_found -> MSynchronized in let szflag = string_of_matita_flag flag in "\n" ^ "" ^ (Filename.basename lpath) ^ " " ^ szflag ^ "
" in let rec aux path = let lpath filename = path ^ "/" ^ filename in let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in (* hide hidden dirs ... including svn stuff *) let dirlist = List.filter (fun x -> String.sub x 0 1 <> ".") (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in let subdirs = List.sort String.compare subdirs in (* only .ma scripts, hidden files excluded *) let scripts = List.filter (fun x -> try let i = String.rindex x '.' in let len = String.length x - i in not (Sys.is_directory (gpath x)) && (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma") with Not_found | Invalid_argument _ -> false) dirlist in let scripts = List.sort String.compare scripts in let subdirtags = String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in let scripttags = String.concat "\n" (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts) in branch path (subdirtags ^ "\n" ^ scripttags) in let res = aux "." in prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE"; res ;; let reset_lib () = let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in ignore (Sys.command ("rm -rf " ^ to_be_removed)) ;; let update_user user = let rt_dir = Helm_registry.get "matita.rt_base_dir" in let _repo = Helm_registry.get "matita.weblib" in let errno, outlines, errlines = exec_process ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/") in let files, anomalies = List.fold_left (fun (facc,eacc) line -> try (let fname,flags = up_classify line user in (fname, flags)::facc), eacc with | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines in let added = count (fun (_,flags) -> List.mem Add flags) files in let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in let del = count (fun (_,flags) -> List.mem Delete flags) files in let upd = count (fun (_,flags) -> List.mem Update flags) files in let merged = count (fun (_,flags) -> List.mem Merge flags) files in let files = List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files in if errno = 0 then files, anomalies, (added,conflict,del,upd,merged) else raise (SvnError (string_of_output outlines errlines)) ;; let add_files user files = if (List.length files > 0) then (let rt_dir = Helm_registry.get "matita.rt_base_dir" in let _repo = Helm_registry.get "matita.weblib" in let files = String.concat " " (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in let errno, outlines, errlines = if files <> "" then exec_process ("svn add --non-interactive " ^ files) else 0,[],[] in if errno = 0 then "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n" else raise (SvnError (string_of_output outlines errlines))) else ("ADD - nothing to do for " ^ user ^ "\n") ;; (* this function should only be called by the server itself (or * the admin) at a scheduled time, so no concurrent instances and no CS needed * also, svn should already be safe as far as concurrency is concerned *) let commit user files = if (List.length files > 0) then (let rt_dir = Helm_registry.get "matita.rt_base_dir" in let _repo = Helm_registry.get "matita.weblib" in let files = String.concat " " (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in let errno, outlines, errlines = exec_process ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ files) in if errno = 0 then "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n" else raise (SvnError (string_of_output outlines errlines))) else ("COMMIT nothing to do for " ^ user ^ "\n") ;;