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 (* disable for debugging *)
  29 let prerr_endline _ = ()
  30
  31 let exec_process cmd =
  32   let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in
  33   let outlines = ref [] in
  34   let errlines = ref [] in
  35   (try
  36      while true do
  37        outlines := input_line stdout :: !outlines;
  38      done;
  39      assert false
  40    with End_of_file ->
  41    (try
  42      while true do
  43        errlines := input_line stderr :: !errlines;
  44      done;
  45      assert false
  46     with End_of_file ->
  47      match (Unix.close_process_full chs) with
  48      | Unix.WEXITED errno -> errno, !outlines, !errlines
  49      | _ -> assert false))
  50
  51 let string_of_output outlines errlines =
  52   let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in
  53   let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in
  54   output ^ "\n\n" ^ errors
  55
  56 type svn_flag =
  57 | Add
  58 | Conflict
  59 | Modified
  60 | NotAdded
  61 | Delete
  62 | Update
  63 | Merge
  64
  65 type matita_flag =
  66 | MUnversioned
  67 | MSynchronized
  68 | MAdd
  69 | MModified
  70 | MConflict
  71
  72 let string_of_matita_flag = function
  73 | MUnversioned -> "unversioned"
  74 | MSynchronized -> "synchronized"
  75 | MAdd -> "new"
  76 | MModified -> "modified"
  77 | MConflict -> "conflict!"
  78
  79 exception SvnAnomaly of string
  80
  81 let stat_classify line uid =
  82   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
  83   let rec aux n acc =
  84     match (line.[n], n) with
  85     | _, n when n = 7 ->
  86        let fn = String.sub line 8 ((String.length line) - 8) in
  87        let prefix_len = String.length basedir in
  88        let fn_len = String.length fn in
  89        if String.sub fn 0 prefix_len = basedir
  90           then String.sub fn prefix_len (fn_len - prefix_len), acc
  91           else fn, acc
  92     | ' ', _ -> aux (n+1) acc
  93     | 'A',0 -> aux (n+1) (Add::acc)
  94     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
  95 (*  | 'D',0 -> aux (n+1) (Delete::acc) *)
  96 (*  | 'I',0 -> aux (n+1) (Ignore::acc) *)
  97     | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc)
  98 (*  | 'R',0 -> aux (n+1) (Replaced::acc) *)
  99 (*  | 'X',0 -> aux (n+1) (UnversionedDir::acc) *)
 100     | '?',0 -> aux (n+1) (NotAdded::acc)
 101 (*  | '!',0 -> aux (n+1) (Missing::acc) *)
 102 (*  | '~',0 -> aux (n+1) (Obstructed::acc) *)
 103 (*  | 'L',2 -> aux (n+1) (Lock::acc) *)
 104 (*  | '+',3 -> aux (n+1) (History::acc) *)
 105 (*  | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *)
 106 (*  | 'X',4 -> aux (n+1) (External::acc) *)
 107 (*  | 'K',5 -> aux (n+1) (LockToken::acc) *)
 108 (*  | 'C',6 -> aux (n+1) (TreeConflict::acc) *)
 109     | _ -> raise (SvnAnomaly line)
 110   in aux 0 []
 111
 112 let count p l =
 113   List.length (List.filter p l)
 114
 115 exception Unimplemented
 116
 117 let matita_flag_of_stat fs =
 118   if List.mem Conflict fs then MConflict
 119   else if List.mem Modified fs then MModified
 120   else if List.mem Add fs then MAdd
 121   else if List.mem Delete fs then raise Unimplemented
 122   else if List.mem NotAdded fs then MUnversioned
 123   else MSynchronized
 124
 125 let stat_user user =
 126   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 127   let _repo = Helm_registry.get "matita.weblib" in
 128
 129   let errno, outlines, errlines = exec_process
 130     ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/")
 131   in
 132   let files, anomalies =
 133     List.fold_left (fun (facc,eacc) line ->
 134       try
 135         (stat_classify line user::facc), eacc
 136       with
 137       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 138   in
 139   let files =
 140     List.map (fun (fname,flags) -> fname,Some (matita_flag_of_stat flags)) files
 141   in
 142
 143   if errno = 0 then files, anomalies
 144   else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines)))
 145 ;;
 146
 147 (* update and checkout *)
 148 let up_classify line uid =
 149   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
 150   let rec aux n acc =
 151     match (line.[n], n) with
 152     | _, n when n = 4 ->
 153        let fn = String.sub line 5 ((String.length line) - 5) in
 154        let prefix_len = String.length basedir in
 155        let fn_len = String.length fn in
 156        if String.sub fn 0 prefix_len = basedir
 157           then String.sub fn prefix_len (fn_len - prefix_len), acc
 158           else fn, acc
 159     | ' ', _ -> aux (n+1) acc
 160     | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc)
 161     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
 162     | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc)
 163     | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc)
 164     | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc)
 165 (*  | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *)
 166     | _ -> raise (SvnAnomaly line)
 167   in aux 0 []
 168
 169 let matita_flag_of_update fs =
 170   if List.mem Conflict fs then Some MConflict
 171   else if List.mem Delete fs then None
 172   else if List.mem Merge fs then Some MModified
 173   else Some MSynchronized
 174
 175 (* this should be executed only for a freshly created user so no CS is needed *)
 176 let checkout user =
 177   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 178   let repo = Helm_registry.get "matita.weblib" in
 179
 180   let errno, outlines, errlines =
 181     prerr_endline
 182     ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/");
 183      exec_process
 184     ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
 185   in
 186   let files, anomalies =
 187     List.fold_left (fun (facc,eacc) line ->
 188       try
 189         (up_classify line user::facc), eacc
 190       with
 191       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 192   in
 193   if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files
 194   else raise (SvnError (string_of_output outlines errlines))
 195
 196 (* normalize qualified file name *)
 197 let normalize_qfn p =
 198   (* trim leading "./" *)
 199   let p =
 200     try
 201       if String.sub p 0 2 <> "./" then p
 202       else String.sub p 2 (String.length p - 2)
 203     with
 204     | Invalid_argument _ -> p
 205   in
 206   (* trim trailing "/" *)
 207   try
 208     if String.sub p (String.length p - 1) 1 <> "/" then p
 209     else String.sub p 0 (String.length p - 1)
 210   with
 211   | Invalid_argument _ -> p
 212
 213 let html_of_library uid ft =
 214   let i = ref 0 in
 215   let newid () = incr i; ("node" ^ string_of_int !i) in
 216
 217   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 218
 219
 220   let branch lpath children =
 221     let id = newid () in
 222     let name = Filename.basename lpath in
 223     let name = if name <> "." then name else "cic:/matita" in
 224     let flag =
 225       try List.assoc lpath ft
 226       with Not_found -> MSynchronized in
 227     let szflag = string_of_matita_flag flag in
 228     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
 229     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
 230     name ^ " " ^ szflag ^ "<br/></span>\n" ^
 231     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
 232     children ^ "\n</span>"
 233   in
 234   let leaf lpath =
 235     let flag =
 236       try List.assoc lpath ft
 237       with Not_found -> MSynchronized in
 238     let szflag = string_of_matita_flag flag in
 239     "<img src=\"treeview/doc.gif\"/>\n" ^
 240     "<a href=\"javascript:void(0)\" onClick=\"selectFile('" ^ lpath ^ "')\" onDblClick=\"dialogBox.callback('" ^ lpath ^ "')\">" ^
 241      (Filename.basename lpath) ^ " " ^ szflag ^ "</a><br/>"
 242   in
 243
 244   let rec aux path =
 245     let lpath filename = path ^ "/" ^ filename in
 246     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
 247
 248     (* hide hidden dirs ... including svn stuff *)
 249     let dirlist =
 250       List.filter (fun x -> String.sub x 0 1 <> ".")
 251         (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
 252     let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
 253     let subdirs = List.sort String.compare subdirs in
 254
 255     (* only .ma scripts, hidden files excluded *)
 256     let scripts =
 257       List.filter (fun x ->
 258         try
 259           let i = String.rindex x '.' in
 260           let len = String.length x - i in
 261           not (Sys.is_directory (gpath x)) &&
 262           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 263         with Not_found | Invalid_argument _ -> false) dirlist in
 264     let scripts = List.sort String.compare scripts in
 265     let subdirtags =
 266       String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
 267     let scripttags =
 268       String.concat "\n"
 269        (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
 270     in
 271     branch path (subdirtags ^ "\n" ^ scripttags)
 272   in
 273
 274   let res = aux "." in
 275   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 276   res
 277 ;;
 278
 279 let reset_lib () =
 280   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 281   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 282 ;;
 283
 284 let update_user user =
 285   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 286   let _repo = Helm_registry.get "matita.weblib" in
 287
 288   let errno, outlines, errlines = exec_process
 289    ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/")
 290   in
 291   let files, anomalies =
 292     List.fold_left (fun (facc,eacc) line ->
 293       try
 294         (let fname,flags = up_classify line user in
 295          (fname, flags)::facc), eacc
 296       with
 297       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 298   in
 299   let added = count (fun (_,flags) -> List.mem Add flags) files in
 300   let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in
 301   let del = count (fun (_,flags) -> List.mem Delete flags) files in
 302   let upd = count (fun (_,flags) -> List.mem Update flags) files in
 303   let merged = count (fun (_,flags) -> List.mem Merge flags) files in
 304
 305   let files =
 306     List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files
 307   in
 308
 309   if errno = 0 then files, anomalies, (added,conflict,del,upd,merged)
 310   else raise (SvnError (string_of_output outlines errlines))
 311 ;;
 312
 313 let add_files user files =
 314   if (List.length files > 0) then
 315    (let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 316     let _repo = Helm_registry.get "matita.weblib" in
 317
 318     let files = String.concat " "
 319       (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 320
 321     let errno, outlines, errlines =
 322       if files <> "" then
 323         exec_process ("svn add --non-interactive " ^ files)
 324       else 0,[],[]
 325     in
 326     if errno = 0 then
 327       "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n"
 328     else raise (SvnError (string_of_output outlines errlines)))
 329   else ("ADD - nothing to do for " ^ user ^ "\n")
 330 ;;
 331
 332 (* this function should only be called by the server itself (or
 333  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 334  * also, svn should already be safe as far as concurrency is concerned *)
 335 let commit user files =
 336   if (List.length files > 0) then
 337     (let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 338     let _repo = Helm_registry.get "matita.weblib" in
 339
 340     let files = String.concat " "
 341       (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 342
 343     let errno, outlines, errlines = exec_process
 344       ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ files)
 345     in
 346     if errno = 0 then
 347       "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n"
 348     else raise (SvnError (string_of_output outlines errlines)))
 349   else ("COMMIT nothing to do for " ^ user ^ "\n")
 350 ;;
 351