matitaB/matita/matitaFilesystem.ml

   1 (* Copyright (C) 2004-2011, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 exception SvnError of string;;
  27
  28 let mutex = Mutex.create ();;
  29
  30 let to_be_committed = ref [];;
  31
  32 let exec_process cmd =
  33   let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in
  34   let outlines = ref [] in
  35   let errlines = ref [] in
  36   (try
  37      while true do
  38        outlines := input_line stdout :: !outlines;
  39      done;
  40      assert false
  41    with End_of_file ->
  42    (try
  43      while true do
  44        errlines := input_line stderr :: !errlines;
  45      done;
  46      assert false
  47     with End_of_file ->
  48      match (Unix.close_process_full chs) with
  49      | Unix.WEXITED errno -> errno, !outlines, !errlines
  50      | _ -> assert false))
  51
  52 let string_of_output outlines errlines =
  53   let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in
  54   let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in
  55   output ^ "\n\n" ^ errors
  56
  57 type svn_flag =
  58 | Add
  59 | Conflict
  60 | Modified
  61 | NotAdded
  62 | Delete
  63 | Update
  64 | Merge
  65
  66 type matita_flag =
  67 | MUnversioned
  68 | MSynchronized
  69 | MAdd
  70 | MModified
  71 | MConflict
  72
  73 let string_of_matita_flag = function
  74 | MUnversioned -> "unversioned"
  75 | MSynchronized -> "synchronized"
  76 | MAdd -> "new"
  77 | MModified -> "modified"
  78 | MConflict -> "conflict!"
  79
  80 exception SvnAnomaly of string
  81
  82 let stat_classify line =
  83   let rec aux n acc =
  84     match (line.[n], n) with
  85     | _, n when n = 7 -> String.sub line 8 ((String.length line) - 8), acc
  86     | ' ', _ -> aux (n+1) acc
  87     | 'A',0 -> aux (n+1) (Add::acc)
  88     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
  89 (*  | 'D',0 -> aux (n+1) (Delete::acc) *)
  90 (*  | 'I',0 -> aux (n+1) (Ignore::acc) *)
  91     | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc)
  92 (*  | 'R',0 -> aux (n+1) (Replaced::acc) *)
  93 (*  | 'X',0 -> aux (n+1) (UnversionedDir::acc) *)
  94     | '?',0 -> aux (n+1) (NotAdded::acc)
  95 (*  | '!',0 -> aux (n+1) (Missing::acc) *)
  96 (*  | '~',0 -> aux (n+1) (Obstructed::acc) *)
  97 (*  | 'L',2 -> aux (n+1) (Lock::acc) *)
  98 (*  | '+',3 -> aux (n+1) (History::acc) *)
  99 (*  | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *)
 100 (*  | 'X',4 -> aux (n+1) (External::acc) *)
 101 (*  | 'K',5 -> aux (n+1) (LockToken::acc) *)
 102 (*  | 'C',6 -> aux (n+1) (TreeConflict::acc) *)
 103     | _ -> raise (SvnAnomaly line)
 104   in aux 0 []
 105
 106 let count p l =
 107   List.length (List.filter p l)
 108
 109 let stat_user user =
 110   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 111   let repo = Helm_registry.get "matita.weblib" in
 112
 113   let errno, outlines, errlines = exec_process
 114     ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/")
 115   in
 116   let files, anomalies =
 117     List.fold_left (fun (facc,eacc) line ->
 118       try
 119         (stat_classify line::facc), eacc
 120       with
 121       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 122   in
 123   if errno = 0 then files, anomalies
 124   else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines)))
 125 ;;
 126
 127 (* update and checkout *)
 128 let up_classify line uid =
 129   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
 130   let rec aux n acc =
 131     match (line.[n], n) with
 132     | _, n when n = 4 ->
 133        let fn = String.sub line 5 ((String.length line) - 5) in
 134        let prefix_len = String.length basedir in
 135        let fn_len = String.length fn in
 136        if String.sub fn 0 prefix_len = basedir
 137           then String.sub fn prefix_len (fn_len - prefix_len), acc
 138           else fn, acc
 139     | ' ', _ -> aux (n+1) acc
 140     | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc)
 141     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
 142     | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc)
 143     | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc)
 144     | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc)
 145 (*  | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *)
 146     | _ -> raise (SvnAnomaly line)
 147   in aux 0 []
 148
 149 let matita_flag_of_update fs =
 150   if List.mem Conflict fs then Some MConflict
 151   else if List.mem Delete fs then None
 152   else if List.mem Merge fs then Some MModified
 153   else Some MSynchronized
 154
 155 (* this should be executed only for a freshly created user so no CS is needed *)
 156 let checkout user =
 157   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 158   let repo = Helm_registry.get "matita.weblib" in
 159
 160   let errno, outlines, errlines = exec_process
 161     ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
 162   in
 163   let files, anomalies =
 164     List.fold_left (fun (facc,eacc) line ->
 165       try
 166         (up_classify line user::facc), eacc
 167       with
 168       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 169   in
 170   if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files
 171   else raise (SvnError (string_of_output outlines errlines))
 172
 173 (* normalize qualified file name *)
 174 let normalize_qfn p =
 175   (* trim leading "./" *)
 176   let p =
 177     try
 178       if String.sub p 0 2 <> "./" then p
 179       else String.sub p 2 (String.length p - 2)
 180     with
 181     | Invalid_argument _ -> p
 182   in
 183   (* trim trailing "/" *)
 184   try
 185     if String.sub p (String.length p - 1) 1 <> "/" then p
 186     else String.sub p 0 (String.length p - 1)
 187   with
 188   | Invalid_argument _ -> p
 189
 190 let html_of_library uid ft =
 191   let i = ref 0 in
 192   let newid () = incr i; ("node" ^ string_of_int !i) in
 193
 194   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 195
 196
 197   let branch lpath children =
 198     let id = newid () in
 199     let name = Filename.basename lpath in
 200     let name = if name <> "." then name else "cic:/matita" in
 201     let flag =
 202       try List.assoc lpath ft
 203       with Not_found -> MSynchronized in
 204     let szflag = string_of_matita_flag flag in
 205     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
 206     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
 207     name ^ " " ^ szflag ^ "<br/></span>\n" ^
 208     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
 209     children ^ "\n</span>"
 210   in
 211   let leaf lpath =
 212     let flag =
 213       try List.assoc lpath ft
 214       with Not_found -> MSynchronized in
 215     let szflag = string_of_matita_flag flag in
 216     "<img src=\"treeview/doc.gif\"/>\n" ^
 217     "<a href=\"javascript:void(0)\" onClick=\"selectFile('" ^ lpath ^ "')\" onDblClick=\"dialogBox.callback('" ^ lpath ^ "')\">" ^
 218      (Filename.basename lpath) ^ " " ^ szflag ^ "</a><br/>"
 219   in
 220
 221   let rec aux path =
 222     let lpath filename = path ^ "/" ^ filename in
 223     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
 224
 225     (* hide hidden dirs ... including svn stuff *)
 226     let dirlist =
 227       List.filter (fun x -> String.sub x 0 1 <> ".")
 228         (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
 229     let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
 230
 231     (* only .ma scripts, hidden files excluded *)
 232     let scripts =
 233       List.filter (fun x ->
 234         try
 235           let i = String.rindex x '.' in
 236           let len = String.length x - i in
 237           not (Sys.is_directory (gpath x)) &&
 238           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 239         with Not_found | Invalid_argument _ -> false) dirlist in
 240     let subdirtags =
 241       String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
 242     let scripttags =
 243       String.concat "\n"
 244        (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
 245     in
 246     branch path (subdirtags ^ "\n" ^ scripttags)
 247   in
 248
 249   let res = aux "." in
 250   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 251   res
 252 ;;
 253
 254 let reset_lib () =
 255   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 256   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 257 ;;
 258
 259 (* adds a user to the commit queue; concurrent instances possible, so we
 260  * enclose the update in a CS
 261  *)
 262 let add_user uid =
 263   Mutex.lock mutex;
 264   to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
 265   Mutex.unlock mutex;
 266 ;;
 267
 268 let update_user user =
 269   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 270   let repo = Helm_registry.get "matita.weblib" in
 271
 272   let errno, outlines, errlines = exec_process
 273    ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/")
 274   in
 275   let files, anomalies =
 276     List.fold_left (fun (facc,eacc) line ->
 277       try
 278         (let fname,flags = up_classify line user in
 279          (fname, flags)::facc), eacc
 280       with
 281       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 282   in
 283   let added = count (fun (_,flags) -> List.mem Add flags) files in
 284   let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in
 285   let del = count (fun (_,flags) -> List.mem Delete flags) files in
 286   let upd = count (fun (_,flags) -> List.mem Update flags) files in
 287   let merged = count (fun (_,flags) -> List.mem Merge flags) files in
 288
 289   let files =
 290     List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files
 291   in
 292
 293   if errno = 0 then files, anomalies, (added,conflict,del,upd,merged)
 294   else raise (SvnError (string_of_output outlines errlines))
 295 ;;
 296
 297 (* this function and the next one should only be called by the server itself (or
 298  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 299  * also, svn should already be safe as far as concurrency is concerned *)
 300 let commit user =
 301   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 302   let repo = Helm_registry.get "matita.weblib" in
 303
 304   let errno, outlines, errlines = exec_process
 305     ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/")
 306   in
 307   if errno = 0 then
 308     "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n"
 309   else raise (SvnError (string_of_output outlines errlines))
 310 ;;
 311
 312 let do_global_commit () =
 313   prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
 314   List.fold_left
 315     (fun (acc,out) u ->
 316        try
 317          let newout = commit u in
 318          acc, out ^ newout
 319        with
 320        | SvnError outstr ->
 321            prerr_endline ("COMMIT OF " ^ user ^ "FAILED:" ^ outstr);
 322            u::acc,out)
 323   ([],"") (List.rev !to_be_committed)
 324 ;;