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