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
 254     (* only .ma scripts, hidden files excluded *)
 255     let scripts =
 256       List.filter (fun x ->
 257         try
 258           let i = String.rindex x '.' in
 259           let len = String.length x - i in
 260           not (Sys.is_directory (gpath x)) &&
 261           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 262         with Not_found | Invalid_argument _ -> false) dirlist in
 263     let subdirtags =
 264       String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
 265     let scripttags =
 266       String.concat "\n"
 267        (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
 268     in
 269     branch path (subdirtags ^ "\n" ^ scripttags)
 270   in
 271
 272   let res = aux "." in
 273   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 274   res
 275 ;;
 276
 277 let reset_lib () =
 278   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 279   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 280 ;;
 281
 282 let update_user user =
 283   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 284   let _repo = Helm_registry.get "matita.weblib" in
 285
 286   let errno, outlines, errlines = exec_process
 287    ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/")
 288   in
 289   let files, anomalies =
 290     List.fold_left (fun (facc,eacc) line ->
 291       try
 292         (let fname,flags = up_classify line user in
 293          (fname, flags)::facc), eacc
 294       with
 295       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 296   in
 297   let added = count (fun (_,flags) -> List.mem Add flags) files in
 298   let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in
 299   let del = count (fun (_,flags) -> List.mem Delete flags) files in
 300   let upd = count (fun (_,flags) -> List.mem Update flags) files in
 301   let merged = count (fun (_,flags) -> List.mem Merge flags) files in
 302
 303   let files =
 304     List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files
 305   in
 306
 307   if errno = 0 then files, anomalies, (added,conflict,del,upd,merged)
 308   else raise (SvnError (string_of_output outlines errlines))
 309 ;;
 310
 311 let add_files user files =
 312   if (List.length files > 0) then
 313    (let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 314     let _repo = Helm_registry.get "matita.weblib" in
 315
 316     let files = String.concat " "
 317       (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 318
 319     let errno, outlines, errlines =
 320       if files <> "" then
 321         exec_process ("svn add --non-interactive " ^ files)
 322       else 0,[],[]
 323     in
 324     if errno = 0 then
 325       "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n"
 326     else raise (SvnError (string_of_output outlines errlines)))
 327   else ("ADD - nothing to do for " ^ user ^ "\n")
 328 ;;
 329
 330 (* this function should only be called by the server itself (or
 331  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 332  * also, svn should already be safe as far as concurrency is concerned *)
 333 let commit user files =
 334   if (List.length files > 0) then
 335     (let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 336     let _repo = Helm_registry.get "matita.weblib" in
 337
 338     let files = String.concat " "
 339       (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 340
 341     let errno, outlines, errlines = exec_process
 342       ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ files)
 343     in
 344     if errno = 0 then
 345       "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n"
 346     else raise (SvnError (string_of_output outlines errlines)))
 347   else ("COMMIT nothing to do for " ^ user ^ "\n")
 348 ;;
 349